-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem liftr_iff {α : Type u} (r : α → α → Prop) (x y : F α) :
    Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ i, r (f₀ i) (f₁ i)

Proof state:
case h.right
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i => (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
constructor

Result:
case h.right.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i => (↑(f i)).2⟩

case h.right.right
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2

Proof state:
case h.right.right
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), r (↑(f i)).1 (↑(f i)).2

Tactic:
intro i

Result:
case h.right.right
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
i : (P F).B a
⊢ r (↑(f i)).1 (↑(f i)).2

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y ↔ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
constructor

Result:
case mp
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

case mpr
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)) → Liftr r x y

Proof state:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ (fun t => (↑t).1) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x

Tactic:
rw [xeq, ← abs_map]

Result:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
a : (P F).A
f₀ f₁ : (P F).B a → α
xeq : x = abs ⟨a, f₀⟩
yeq : y = abs ⟨a, f₁⟩
h : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ abs ((P F).map (fun t => (↑t).1) ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₀⟩

Proof state:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ x = abs ⟨a, fun i => (↑(f i)).1⟩

Tactic:
rw [← xeq, ← abs_repr u, h, ← abs_map]

Result:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((P F).map (fun t => (↑t).1) ⟨a, f⟩) = abs ⟨a, fun i => (↑(f i)).1⟩

Proof state:
case h.right.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ y = abs ⟨a, fun i => (↑(f i)).2⟩

Tactic:
rw [← yeq, ← abs_repr u, h, ← abs_map]

Result:
case h.right.left
F : Type u → Type u
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
u : F { p // r p.1 p.2 }
xeq : (fun t => (↑t).1) <$> u = x
yeq : (fun t => (↑t).2) <$> u = y
a : (P F).A
f : (P F).B a → { p // r p.1 p.2 }
h : repr u = ⟨a, f⟩
⊢ abs ((P F).map (fun t => (↑t).2) ⟨a, f⟩) = abs ⟨a, fun i => (↑(f i)).2⟩