awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
have this : Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
  (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
Tactic: have := mk_inj ‹_›
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
this :
  Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
have succ : ∀ (y : F.B a → F.M),
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y) →
    (∀ (i : F.B a), Agree' n (x i) (y i)) →
      M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) →
        Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
          ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
Tactic: cases this
Cleared hypotheses: a_1, x_1, y_1, h_1, h_3, h_4, this
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
f : F.B a_1 → F.M
h_1 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
y_1 : F.B a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
h_3 : ∀ (i : F.B a), Agree' n (x i) (y_1 i)
h_4 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1)).approx (n + 1 + 1))
have this : Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
  (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
Tactic: have := mk_inj ‹_›
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
inst_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_1 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
a_2 : F.A
f : F.B a_2 → F.M
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y)
a_3 : F.A
f_1 : F.B a_3 → F.M
h_3 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) =
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_1)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1))
h_4 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
have succ : ∀ (y : F.B a → F.M),
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y) →
    (∀ (i : F.B a), Agree' n (x i) (y i)) →
      M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x) →
        Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f)).approx (n + 1 + 1))
          ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_3 f_1)).approx (n + 1 + 1))
Tactic: iterate 3 (have := mk_inj ‹_›; cases this)
Cleared hypotheses: a_1, x_1, y_1, h_1, h_3, h_4
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
⊢ Eq (α := CofixA F (n + 1 + 1)) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)).approx (n + 1 + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1)).approx (n + 1 + 1))
have succ : Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
  (CofixA.intro a_2 fun (j : F.B a_2) ↦ (f_1 j).approx (n + 1))
Tactic: simp only [approx_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a_2 fun (j : F.B a_2) ↦ (f_1 j).approx (n + 1))
have this : Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
  (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
Tactic: have := mk_inj h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
a_2 : F.A
f_1 : F.B a_2 → F.M
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1))
f₁ : F.B a → F.M
h₁ :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
this :
  Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_2 f_1) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a_2 fun (j : F.B a_2) ↦ (f_1 j).approx (n + 1))
have succ : ∀
  (hrec :
    ∀ (ps : Path F),
      n + 1 = length ps →
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
          iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)))
  (h₁ :
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁)),
  Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
Tactic: cases this
Cleared hypotheses: a_2, f_1, hrec, h₁, this
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
have this : Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
  (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
Tactic: have := mk_inj h₂
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
a_1 : F.A
f : F.B a_1 → F.M
h₂ : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
this :
  Eq (α := (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M)
    (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
have succ : ∀
  (h₂ :
    M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂))
  (hrec :
    ∀ (ps : Path F),
      n + 1 = length ps →
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
          iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))),
  Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a fun (j : F.B a) ↦ (f₂ j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
Tactic: cases this
Cleared hypotheses: a_1, f, h₂, hrec, this
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
⊢ Eq (α := CofixA F (n + 1 + 1)) (CofixA.intro a fun (j : F.B a) ↦ (f₂ j).approx (n + 1))
    (CofixA.intro a fun (j : F.B a) ↦ (f₁ j).approx (n + 1))
have succ : Eq (α := F.B a → CofixA F (n + 1)) (fun (j : F.B a) ↦ (f₂ j).approx (n + 1)) fun (j : F.B a) ↦ (f₁ j).approx (n + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
⊢ Eq (α := F.B a → CofixA F (n + 1)) (fun (j : F.B a) ↦ (f₂ j).approx (n + 1)) fun (j : F.B a) ↦ (f₁ j).approx (n + 1)
have succ : ∀ (i : F.B a), Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
⊢ Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
have succ : Agree' n (f₃ i) (f₂ i)
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
succ : Agree' n (f₃ i) (f₂ i)
⊢ Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
have succ₁ : Agree' n (f₃ i) (f₁ i)
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
succ : Agree' n (f₃ i) (f₂ i)
succ₁ : Agree' n (f₃ i) (f₁ i)
⊢ Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
have succ₂ : ∀ (ps : Path F), n = length ps → iselect ps (f₂ i) = iselect ps (f₁ i)
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
succ : Agree' n (f₃ i) (f₂ i)
succ₁ : Agree' n (f₃ i) (f₁ i)
succ₂ : ∀ (ps : Path F), n = length ps → iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ Eq (α := CofixA F (n + 1)) ((f₂ i).approx (n + 1)) ((f₁ i).approx (n + 1))
have succ₃ : F.M
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
inst : Inhabited F.M
n_ih_1 : DecidableEq F.A
n : ℕ
n_ih :
  ∀ (x y z : F.M) (hx : Agree' n z x) (hy : Agree' n z y)
    (hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y),
    Eq (α := CofixA F (n + 1)) (x.approx (n + 1)) (y.approx (n + 1))
a : F.A
f₃ f₂ : F.B a → F.M
hAgree₂ : ∀ (i : F.B a), Agree' n (f₃ i) (f₂ i)
f₁ : F.B a → F.M
hAgree₁ : ∀ (i : F.B a), Agree' n (f₃ i) (f₁ i)
clr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₃)
hrec :
  ∀ (ps : Path F),
    n + 1 = length ps →
      iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
        iselect ps (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
i : F.B a
ps : Path F
h : n = length ps
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
have hrec₁ : iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₂)) =
  iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f₁))
Tactic: specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
Cleared hypotheses: hrec