-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem liftp_iff {α : Type u} (p : α → Prop) (x : F α) :
    Liftp p x ↔ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ i, p (f i)

Proof state:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun 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
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((P F).map Subtype.val ⟨a, f⟩) = abs ⟨a, fun i => ↑(f i)⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.right
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
i : (P F).B a
⊢ p ↑(f i)

Tactic:
apply (f i).property

Result:
no goals

Proof state:
case h.right
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), p ↑(f i)

Tactic:
intro i

Result:
case h.right
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
i : (P F).B a
⊢ p ↑(f i)

Proof state:
case mp
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ Liftp p x → ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Tactic:
rintro ⟨y, hy⟩

Result:
case mp.intro
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

Proof state:
case mpr.intro.intro.intro
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x

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

Result:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x

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

Tactic:
constructor

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

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

Proof state:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Subtype.val <$> abs ⟨a, fun i => ⟨f i, ⋯⟩⟩ = x

Tactic:
rw [← abs_map, h₀]

Result:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ abs ((P F).map Subtype.val ⟨a, fun i => ⟨f i, ⋯⟩⟩) = abs ⟨a, f⟩

Proof state:
case mpr
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
⊢ (∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)) → Liftp p x

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

Result:
case mpr.intro.intro.intro
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
a : (P F).A
f : (P F).B a → α
h₀ : x = abs ⟨a, f⟩
h₁ : ∀ (i : (P F).B a), p (f i)
⊢ Liftp p x

Proof state:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i => ↑(f i)⟩

Tactic:
rw [← hy, ← abs_repr y, h, ← abs_map]

Result:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ abs ((P F).map Subtype.val ⟨a, f⟩) = abs ⟨a, fun i => ↑(f i)⟩

Proof state:
case mp.intro.mk
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

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

Result:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i => ↑(f i)⟩ ∧ ∀ (i : (P F).B a), p ((fun i => ↑(f i)) i)

Proof state:
case h
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i => ↑(f i)⟩ ∧ ∀ (i : (P F).B a), p ((fun i => ↑(f i)) i)

Tactic:
constructor

Result:
case h.left
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ x = abs ⟨a, fun i => ↑(f i)⟩

case h.right
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∀ (i : (P F).B a), p ↑(f i)

Proof state:
case mp.intro
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)

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

Result:
case mp.intro.mk
F : Type u → Type u
q : QPF F
α : Type u
p : α → Prop
x : F α
y : F (Subtype p)
hy : Subtype.val <$> y = x
a : (P F).A
f : (P F).B a → Subtype p
h : repr y = ⟨a, f⟩
⊢ ∃ a f, x = abs ⟨a, f⟩ ∧ ∀ (i : (P F).B a), p (f i)