proof review in mathlib4#728

Stream: mathlib4

[Arien Malec]

I'm down to two issues in mathlib4#728 that are stumping me.

first issue in max_lt_max -- the simps that worked in Lean 3 don't work post-port, and I'm sure this is a trivial fix, but I'm not seeing it...

Second two issues are weirder -- the mathlib proof has a typing issue post port -- I've played around with parentheses, etc to see if I can ; I have a tactic proof that works when the theorem is named Max.left_comm' but if I changed the name to Max.left_comm with the same proof I get an "issues with structural recursion" error -- it's possible here that Lean is getting confused between the version of left_comm that's defined in Init.Logic but I don't know how to provide a scoped name here for a top level opened term....

[Ruben Van de Velde]

Not sure why simp fails, but this works

theorem max_lt_max (h₁ : a < c) (h₂ : b < d) : max a b < max c d := by
  rw [max_lt_iff, lt_max_iff, lt_max_iff]
  exact ⟨Or.inl h₁, Or.inr h₂⟩

[Ruben Van de Velde]

Or

theorem max_lt_max (h₁ : a < c) (h₂ : b < d) : max a b < max c d :=
max_lt (lt_max_of_lt_left h₁) (lt_max_of_lt_right h₂)

[Ruben Van de Velde]

And

theorem Max.left_comm (a b c : α) : max a (max b c) = max b (max a c) :=
  _root_.left_comm max max_comm max_assoc a b c
theorem Max.right_comm (a b c : α) : max (max a b) c = max (max a c) b :=
  _root_.right_comm max max_comm max_assoc a b c

[Ruben Van de Velde]

@Arien Malec I pushed those changes ^

[Arien Malec]

Perfect!

[Ruben Van de Velde]

Maybe someone wants to figure out why simp no longer works, but at least you're unblocked now

[Kevin Buzzard]

I think these things are important to note -- someone should add a porting note

[Arien Malec]

@Ruben Van de Velde did.

[Arien Malec]

His constructive solution is prettier than the original simp, but the particular failure mode of simp here is odd. Why does repeating lt_max_iff work here?

[Ruben Van de Velde]

I haven't verified, but my hypothesis is that the different lemmas were applied in a different order

[Ruben Van de Velde]

Which would be why controlling the order by using rw instead of simp helped

[Arien Malec]

Oh, missed that you did rw!

[Scott Morrison]

You can see what order the simp lemmas are being applied with set_option trace.Meta.Tactic.simp.rewrite true.