awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ Liftp p (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
have mk : ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 → Fix F),
  Eq (α := F (Fix F)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
      (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a_1 f_1)) ∧
    ∀ (i : (P F).B a_1), p (f_1 i)
Tactic: rw [liftp_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
p : Fix F → Prop
h : ∀ (x : F (Fix F)), Liftp p x → p (mk x)
x : Fix F
a : (P F).A
f : (P F).B a → WType (α := (P F).A) (P F).B
ih : ∀ (a : (P F).B a), p (Quot.mk (⇑Wsetoid : (P F).W → (P F).W → Prop) (f a))
⊢ ∃ (a_1 : (P F).A) (f_1 : (P F).B a_1 → Fix F),
    Eq (α := F (Fix F)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a fun (x : (P F).B a) ↦ ⟦f x⟧))
        (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Fix F) a_1 f_1)) ∧
      ∀ (i : (P F).B a_1), p (f_1 i)
have mk : ∀ (i : (P F).B a), p ⟦f i⟧
Tactic: refine ⟨_, _, rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
g : α → F α
x : α
⊢ Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    (PFunctor.M.dest (corecF g x)) ((P F).map (corecF g) (repr (g x)))
have rw : Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
  (PFunctor.M.dest (PFunctor.M.corec (fun (x : α) ↦ repr (g x)) x))
  ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
Tactic: rw [corecF, PFunctor.M.dest_corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
g : α → F α
x : α
rw :
  Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    (PFunctor.M.dest (PFunctor.M.corec (fun (x : α) ↦ repr (g x)) x))
    ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
⊢ Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
    (PFunctor.M.dest (corecF g x)) ((P F).map (corecF g) (repr (g x)))
have rw₁ : Eq (α := (↑(P F) : (α : Type (max u_1 u)) → Type (max (max u_1 u) u u_1)) (PFunctor.M.{u, u_1} (P F)))
  ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
  ((P F).map (PFunctor.M.corec fun (x : α) ↦ repr (g x)) (repr (g x)))
Tactic: rw [corecF, PFunctor.M.dest_corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
⊢ Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs x.dest) (Quot.mk Mcongr <$> abs y.dest)
have this : ∀ (x y : (P F).M), r x y → Mcongr x y
Tactic: have : ∀ x y, r x y → Mcongr x y := by
        intro x y h
        exact ⟨r, pr, h⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs x.dest) (Quot.mk Mcongr <$> abs y.dest)
have rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Tactic: rw [← Quot.factor_mk_eq _ _ this]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
have lhs : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest
have rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Tactic: rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
| (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
have rw : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Tactic: lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
⊢ (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
have conv : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Tactic: conv =>
        lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
x y : (P F).M
r : (P F).M → (P F).M → Prop
pr : IsPrecongr r
rxy : r x y
this : ∀ (x y : (P F).M), r x y → Mcongr x y
conv : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
⊢ (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs x.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
have conv₁ : (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest = (Quot.factor r Mcongr this ∘ Quot.mk r) <$> abs y.dest
Tactic: conv =>
        lhs
        rw [comp_map, ← abs_map, pr rxy, abs_map, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)
have lhs : dest (corec g x)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| dest (corec g x)
have rw : Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) sorry (Quot.mk Mcongr (corecF g x))
Tactic: rw [Cofix.dest, Cofix.corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
| Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)
have rw : Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) sorry (Quot.mk Mcongr (corecF g x))
Tactic: lhs
    rw [Cofix.dest, Cofix.corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Eq (α := F (Cofix F)) (dest (corec g x)) (corec g <$> g x)
have conv : Eq (α := F (Cofix F))
  (Quot.lift (r := Mcongr) (fun (x : (P F).M) ↦ Quot.mk Mcongr <$> abs x.dest) sorry (Quot.mk Mcongr (corecF g x)))
  (corec g <$> g x)
Tactic: conv =>
    lhs
    rw [Cofix.dest, Cofix.corec]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u
g : α → F α
x : α
⊢ Eq (α := F (Cofix F)) (Quot.mk Mcongr <$> abs (PFunctor.M.dest (corecF g x))) (corec g <$> g x)
have rw : Eq (α := F (Cofix F)) ((Quot.mk Mcongr ∘ corecF g) <$> g x) (corec g <$> g x)
Tactic: rw [corecF_eq, abs_map, abs_repr, ← comp_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
⊢ x = y
have h' : ∀ (x : Cofix F), r' x x
Tactic: apply Cofix.bisim_aux r'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
h' : ∀ (x : Cofix F), r' x x
⊢ x = y
have h₁ : ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
Tactic: apply Cofix.bisim_aux r'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x y : Cofix F
rxy : r x y
h' : ∀ (x : Cofix F), r' x x
h₁ : ∀ (x y : Cofix F), r' x y → Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
⊢ x = y
have a : r' x y
Tactic: apply Cofix.bisim_aux r'
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y : Cofix F
rxy : r x_1 y
x : Cofix F
⊢ r' x x
have h' : x = x
Tactic: left
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r' x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
have h₁ : ∀ (r'xy : x = y), Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
Tactic: rcases r'xy with r'xy | r'xy
Cleared hypotheses: r'xy
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r' x y
h₁ : ∀ (r'xy : x = y), Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
have h₂ : ∀ (r'xy : r x y), Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
Tactic: rcases r'xy with r'xy | r'xy
Cleared hypotheses: r'xy
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : x = y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
have h₁ : Quot.mk r' <$> y.dest = Quot.mk r' <$> y.dest
Tactic: rw [r'xy]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
have this : ∀ (x y : Cofix F), r x y → r' x y
Tactic: have : ∀ x y, r x y → r' x y := fun x y h => Or.inr h
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.mk r' <$> x.dest = Quot.mk r' <$> y.dest
have h₁ : (Quot.factor r r' this ∘ Quot.mk r) <$> x.dest = (Quot.factor r r' this ∘ Quot.mk r) <$> y.dest
Tactic: rw [← Quot.factor_mk_eq _ _ this]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> x.dest =
    (Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this ∘ Quot.mk r) <$> y.dest
have h₁ : Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
  Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
Tactic: rw [@comp_map _ q _ _ _ (Quot.mk r), @comp_map _ q _ _ _ (Quot.mk r)]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
r' : (x y : Cofix F) → Prop := fun (x y : Cofix F) ↦ x = y ∨ r x y
x_1 y_1 : Cofix F
rxy : r x_1 y_1
x y : Cofix F
r'xy : r x y
this : ∀ (x y : Cofix F), r x y → r' x y
⊢ Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> x.dest =
    Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
have h₁ : Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest =
  Quot.factor r (fun (x y : Cofix F) ↦ x = y ∨ r x y) this <$> Quot.mk r <$> y.dest
Tactic: rw [h _ _ r'xy]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
⊢ ∀ (x y : Cofix F), r x y → x = y
have h₁ : ∀ (x y : Cofix F), r x y → Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
Tactic: apply Cofix.bisim_rel
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
have h₁ : ∀ (a : (P F).A) (f₀ f₁ : (P F).B a → Cofix F)
  (dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀))
  (dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁))
  (h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)), Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
Tactic: rcases (liftr_iff r _ _).mp (h x y rxy) with ⟨a, f₀, f₁, dxeq, dyeq, h'⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Quot.mk r <$> x.dest = Quot.mk r <$> y.dest
have h₁ : Eq (α := F (Quot r)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₀)))
  (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₁)))
Tactic: rw [dxeq, dyeq, ← abs_map, ← abs_map, PFunctor.map_eq, PFunctor.map_eq]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
⊢ Eq (α := F (Quot r)) (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₀)))
    (abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Quot r) a (Quot.mk r ∘ f₁)))
have h₁ : ∀ (i : (P F).B a), (Quot.mk r ∘ f₀) i = (Quot.mk r ∘ f₁) i
Tactic: congr 2 with i
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
r : Cofix F → Cofix F → Prop
h : ∀ (x y : Cofix F), r x y → Liftr r x.dest y.dest
x y : Cofix F
rxy : r x y
a : (P F).A
f₀ f₁ : (P F).B a → Cofix F
dxeq : x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀)
dyeq : y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁)
h' : ∀ (i : (P F).B a), r (f₀ i) (f₁ i)
i : (P F).B a
⊢ (Quot.mk r ∘ f₀) i = (Quot.mk r ∘ f₁) i
have h₁ : r (f₀ i) (f₁ i)
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
⊢ Liftr R x.dest y.dest
have rcases : ∀ (a : (P F).A) (f f' : (P F).B a → Cofix F)
  (ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f))
  (vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f'))
  (h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'), Liftr R x.dest y.dest
Tactic: rcases h x' Qx' with ⟨a, f, f', ux'eq, vx'eq, h'⟩
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF F
α : Type u_1
Q : α → Prop
u v : α → Cofix F
h :
  ∀ (x : α),
    Q x →
      ∃ (a : (P F).A) (f : (P F).B a → Cofix F) (f' : (P F).B a → Cofix F),
        (u x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f) ∧
          (v x).dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f') ∧
            ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
x_1 : α
Qx : Q x_1
R : (w z : Cofix F) → Prop := fun (w z : Cofix F) ↦ ∃ (x' : α), Q x' ∧ w = u x' ∧ z = v x'
x y : Cofix F
h_1 : R x y
x' : α
Qx' : Q x'
xeq : x = u x'
yeq : y = v x'
a : (P F).A
f f' : (P F).B a → Cofix F
ux'eq : (u x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f)
vx'eq : (v x').dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f')
h' : ∀ (i : (P F).B a), ∃ (x' : α), Q x' ∧ f i = u x' ∧ f' i = v x'
⊢ Liftr R x.dest y.dest
have rw : ∃ (a : (P F).A) (f₀ : (P F).B a → Cofix F) (f₁ : (P F).B a → Cofix F),
  x.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₀) ∧
    y.dest = abs (Sigma.mk (β := fun (x : (P F).A) ↦ (P F).B x → Cofix F) a f₁) ∧ ∀ (i : (P F).B a), R (f₀ i) (f₁ i)
Tactic: rw [liftr_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α : Type u
x : G α
⊢ FG_abs (abs.{u, u_1, u} (repr (FG_repr x))) = x
have rw : FG_abs (FG_repr x) = x
Tactic: rw [abs_repr, FG_abs_repr]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α : Type u
x : G α
rw : FG_abs (FG_repr x) = x
⊢ FG_abs (abs.{u, u_1, u} (repr (FG_repr x))) = x
have rw₁ : x = x
Tactic: rw [abs_repr, FG_abs_repr]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : (↑(P F) : (α : Type u) → Type (max u u_1)) α
⊢ FG_abs (abs ((P F).map f x)) = f <$> FG_abs (abs x)
have rw : FG_abs (f <$> abs x) = f <$> FG_abs (abs x)
Tactic: rw [abs_map, FG_abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
G : Type u → Type u
inst : Functor G
FG_abs : {α : Type u} → F α → G α
FG_repr : {α : Type u} → G α → F α
FG_abs_repr : ∀ {α : Type u} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : Type u} (f : α → β) (x : F α), FG_abs (f <$> x) = f <$> FG_abs x
α β : Type u
f : α → β
x : (↑(P F) : (α : Type u) → Type (max u u_1)) α
rw : FG_abs (f <$> abs x) = f <$> FG_abs (abs x)
⊢ FG_abs (abs ((P F).map f x)) = f <$> FG_abs (abs x)
have rw₁ : f <$> FG_abs (abs x) = f <$> FG_abs (abs x)
Tactic: rw [abs_map, FG_abs_map]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) ↔
    ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
have mp : (∀ ⦃p : α → Prop⦄, Liftp p x → p u) →
  ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
mp :
  (∀ ⦃p : α → Prop⦄, Liftp p x → p u) →
    ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
⊢ (∀ ⦃p : α → Prop⦄, Liftp p x → p u) ↔
    ∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
      abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ
have mpr : (∀ (a : PFunctor.A.{u, u_1} (P F)) (f : (P F).B a → α),
    abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x → u ∈ f '' univ) →
  ∀ ⦃p : α → Prop⦄, Liftp p x → p u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (goal)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
⊢ Liftp (fun (u : α) ↦ u ∈ f '' univ) x
have rw : ∃ (a_1 : PFunctor.A.{u, u_1} (P F)) (f_1 : (P F).B a_1 → α),
  x = abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a_1 f_1) ∧
    ∀ (i : (P F).B a_1), f_1 i ∈ f '' univ
Tactic: rw [liftp_iff]
-- Lean 4 proof step from Mathlib.Data.QPF.Univariate.Basic (hypothesis)
Goal:
F : Type u → Type u
q : QPF.{u, u_1, u} F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : PFunctor.A.{u, u_1} (P F)
f : (P F).B a → α
haf : abs (Sigma.mk (β := fun (x : PFunctor.A.{u, u_1} (P F)) ↦ (P F).B x → α) a f) = x
⊢ u ∈ f '' univ
have this : Liftp (fun (u : α) ↦ u ∈ f '' univ) x
Tactic: have : Liftp (fun u => u ∈ f '' univ) x := by
      rw [liftp_iff]
      exact ⟨a, f, haf.symm, fun i => mem_image_of_mem _ (mem_univ _)⟩