-- 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 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

Tactic:
rintro ⟨a, f₀, f₁, xeq, yeq, h⟩

Result:
case mpr.intro.intro.intro.intro.intro
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)
⊢ Liftr r x y

Proof state:
case h.right
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).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

Tactic:
rw [yeq, ← abs_map]

Result:
case h.right
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).2) ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩

Proof state:
case mpr.intro.intro.intro.intro.intro
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)
⊢ Liftr r x y

Tactic:
use abs ⟨a, fun i => ⟨(f₀ i, f₁ i), h i⟩⟩

Result:
case h
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 ∧
    (fun t => (↑t).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

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:
exact (f i).property

Result:
no goals

Proof state:
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)

Tactic:
rintro ⟨u, xeq, yeq⟩

Result:
case mp.intro.intro
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 f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), 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 α
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).2) ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₁⟩

Tactic:
rfl

Result:
no goals

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)
⊢ abs ((P F).map (fun t => (↑t).1) ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩) = abs ⟨a, f₀⟩

Tactic:
rfl

Result:
no goals

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⟩
⊢ abs ((P F).map (fun t => (↑t).2) ⟨a, f⟩) = abs ⟨a, fun i => (↑(f i)).2⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mp.intro.intro.mk
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⟩
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
use a, fun i => (f i).val.fst, fun i => (f i).val.snd

Result:
case h
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⟩ ∧
    y = abs ⟨a, fun i => (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 ((fun i => (↑(f i)).2) i)

Proof state:
case h
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⟩ ∧
    y = abs ⟨a, fun i => (↑(f i)).2⟩ ∧ ∀ (i : (P F).B a), r (↑(f i)).1 ((fun i => (↑(f i)).2) i)

Tactic:
constructor

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⟩
⊢ x = abs ⟨a, fun i => (↑(f i)).1⟩

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

Proof state:
case h
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 ∧
    (fun t => (↑t).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

Tactic:
constructor

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)
⊢ (fun t => (↑t).1) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = x

case h.right
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).2) <$> abs ⟨a, fun i => ⟨(f₀ i, f₁ i), ⋯⟩⟩ = y

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⟩
⊢ abs ((P F).map (fun t => (↑t).1) ⟨a, f⟩) = abs ⟨a, fun i => (↑(f i)).1⟩

Tactic:
rfl

Result:
no goals

Proof state:
case mp.intro.intro
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 f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

Tactic:
rcases h : repr u with ⟨a, f⟩

Result:
case mp.intro.intro.mk
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⟩
⊢ ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)