MeasureTheory.PiSystem !4#2160

Stream: mathlib4

[Johan Commelin]

https://github.com/leanprover-community/mathlib4/pull/2160/files#diff-d4cb986b8baeedf848bbc2c9b99deb631e8fdc6625dbaf17e5be2d0ebe48b7eeR155-R173

-- porting note: changed `max`/`min` to `⊔`/`⊓`

Is this what we want?

[Pol'tta / Miyahara Kō]

When we used max/min, the a₁ ⊔ a₂ =?= max a₁ a₂ at isPiSystem_Icc_mem and isPiSystem_Icc failed, so we changed max/min to ⊔/⊓ in the theorems. Should we wait for a core-PR to fix this?

[Johan Commelin]

Did the definition of either of the two change?

[Johan Commelin]

@Pol'tta / Kô Miyahara Do you mean that the statement no longer typechecked? Or was it just the proof that broke?

[Pol'tta / Miyahara Kō]

The statement was typechecked, but Lean couldn't match Icc_inter_Icc : Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂) to Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂).

[Johan Commelin]

If the statement typechecks, then we should fix the proof. Rewrite with a lemma max_eq_sup or something like that.