fixing easy error in Mathbin

Stream: mathlib4

[Kevin Buzzard]

So the autoport suggests this:

protected theorem Symmetric.iff (H : Symmetric r) (x y : α) : r x y ↔ r y x :=
  ⟨fun h => H h, fun h => H h⟩

theorem Symmetric.flip_eq (h : Symmetric r) : flip r = r :=
  funext₂ fun _ _ => propext <| h.Iff _ _

and the thing I want to flag is that the very end of the proof contains h.Iff which here should be h.iff if the previous theorem is anything to go by. My understanding is that Symmetric.iff is correctly named and the porting program has incorrectly changed h.iff into h.Iff. But what do I do as the manual porter? Do I just change h.Iff to h.iff and move on? Am I supposed to #align something to ensure that this never happens again? Or will this happen again regardless of what I do? Or have I misunderstood and I should be doing something else?

[Mario Carneiro]

this is an issue due to mathport not having enough context to resolve the name

[Mario Carneiro]

it would be nice to fix but it's not easy

[Mario Carneiro]

As a porter, you should just fix it. The reason it is being capitalized is because mathport guesses that it could be a reference to the global constant iff -> Iff