More issues with normalization to pp'able equalities

Stream: mathlib4

[Arien Malec]

Sorry for the bad subject name, but I'm not sure exactly how to describe this problem.

In mathlib4#1179 there are a number of theorems that fail to solve post migration, where one side of an equality is "less reduced" than another, with lots of bare Exists and such rather than expressed in forms that pp effectively.

After thinking about this rather than sleeping last night, I decided to make the rhs of one of the simpler of these cases "worse" and lo and behold, I close the proof.

In mem_prod_lift, the following that used to work in Lean 3, fails to close:

theorem mem_prod_lift {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
    y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x := by
  trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
  · simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]
  · simpa only [exists_and_left, exists_and_right]

where the goal state is:

((Exists fun x_1 ↦ Part.get (f x) (_ : (f x).Dom) = y.fst) ∧ Exists fun x_1 ↦ Part.get (g x) x_1 = y.snd) ↔ y.fst ∈ f x ∧ y.snd ∈ g x

To my eye, through the relevant definitions of \in that are being used here for partial functions, this should still close.

(de-pp'd for those for whom this means something):

Iff
  (And
    (@Exists.{0} (@Part.Dom.{u_2} β (f x))
      fun (x_1 : @Part.Dom.{u_2} β (f x)) ↦
        @Eq.{u_2 + 1} β
          (@Part.get.{u_2} β (f x)
            (@Iff.mpr (@Part.Dom.{u_2} β (f x)) (@Part.Dom.{u_2} β (f x))
              (@Iff.of_eq (@Part.Dom.{u_2} β (f x)) (@Part.Dom.{u_2} β (f x))
                (@Eq.refl.{1} Prop (@Part.Dom.{u_2} β (f x))))
              x_1))
          (@Prod.fst.{u_2, u_3} β γ y))
    (@Exists.{0} (@Part.Dom.{u_3} γ (g x))
      fun (x_1 : @Part.Dom.{u_3} γ (g x)) ↦ @Eq.{u_3 + 1} γ (@Part.get.{u_3} γ (g x) x_1) (@Prod.snd.{u_2, u_3} β γ y)))
  (And
    (@Membership.mem.{u_2, u_2} β (Part.{u_2} β) (@Part.instMembershipPart.{u_2} β) (@Prod.fst.{u_2, u_3} β γ y) (f x))
    (@Membership.mem.{u_3, u_3} γ (Part.{u_3} γ) (@Part.instMembershipPart.{u_3} γ) (@Prod.snd.{u_2, u_3} β γ y) (g x)))

If, instead, I make the rhs worse by walking back the nice representation on the rhs, I can close the goal:

theorem mem_prod_lift {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
    y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x := by
  trans ∃ hp hq, (f x).get hp = y.1 ∧ (g x).get hq = y.2
  · simp only [prodLift, Part.mem_mk_iff, And.exists, Prod.ext_iff]
  · simp only [exists_and_left, exists_and_right, (· ∈ ·), Part.Mem]

Before I go try this with the other proofs that don't close, I think the desired state is for the lhs to normalize to a point where Lean 4 believes they are equal, yes?

[Arien Malec]

This may also be: https://github.com/leanprover/lean4/issues/1937

[Arien Malec]

?