awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n.succ
y : CofixA F (n.succ + 1)
i : F.B (head' x)
j : F.B (head' y)
h₀ : i ≍ j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)
have intro : ∀ {n_1 : ℕ} {a : F.A} (x : F.B a → CofixA F n) (x' : F.B a → CofixA F (n + 1))
  (hagree : ∀ (i : F.B a), Agree (x i) (x' i)) {i : F.B (head' (CofixA.intro a x))}
  {j : F.B (head' (CofixA.intro a x'))} (h₀ : i ≍ j),
  Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') j)
Tactic: obtain - | ⟨_, _, hagree⟩ := h₁
Cleared hypotheses: x, y, i, j, h₀, h₁
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 n : ℕ
a : F.A
x : F.B a → CofixA F n_1
x' : F.B a → CofixA F (n_1 + 1)
hagree : ∀ (i : F.B a), Agree (x i) (x' i)
i : F.B (head' (CofixA.intro a x))
j : F.B (head' (CofixA.intro a x'))
h₀ : i ≍ j
⊢ Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') j)
have intro : Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') i)
Tactic: cases h₀
Cleared hypotheses: j, h₀
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F (succ 0)
h : Agree x y
⊢ truncate y = x
have zero : ∀ (h : Agree CofixA.continue y), truncate y = CofixA.continue
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
y : CofixA F (succ 0)
h : Agree CofixA.continue y
⊢ truncate y = CofixA.continue
have zero : ∀ (a : F.A) (a_1 : F.B a → CofixA F 0) (h : Agree CofixA.continue (CofixA.intro a a_1)),
  truncate (CofixA.intro a a_1) = CofixA.continue
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ) (h : Agree x y), truncate y = x
a : F.A
f : F.B a → CofixA F n
y : F.B a → CofixA F (n + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ truncate (CofixA.intro a y) = CofixA.intro a f
have succ : (CofixA.intro a fun (x : F.B a) ↦ truncate (y x)) = CofixA.intro a f
Tactic: simp only [truncate, Function.comp_def]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ) (h : Agree x y), truncate y = x
a : F.A
f : F.B a → CofixA F n
y : F.B a → CofixA F (n + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y i)
⊢ (CofixA.intro a fun (x : F.B a) ↦ truncate (y x)) = CofixA.intro a f
have succ : ∀ (y_1 : F.B a), truncate (y y_1) = f y_1
Tactic: congr with y
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ) (h : Agree x y), truncate y = x
x : CofixA F (n + 1)
y : CofixA F (n + 1).succ
h : Agree x y
⊢ truncate y = x
have succ : ∀ {a : F.A} (f : F.B a → CofixA F n) (y : F.B a → CofixA F (n + 1)) (h₁ : ∀ (i : F.B a), Agree (f i) (y i)),
  truncate (CofixA.intro a y) = CofixA.intro a f
Tactic: cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)
Cleared hypotheses: x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n
y : CofixA F n.succ
h : Agree x y
⊢ truncate y = x
have zero : ∀ (x : CofixA F 0) (y : CofixA F (succ 0)) (h : Agree x y), truncate y = x
Tactic: induction n with
  | zero =>
    cases x
    cases y
    rfl
  | succ n n_ih =>
    cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F n
y : CofixA F n.succ
h : Agree x y
zero : ∀ (x : CofixA F 0) (y : CofixA F (succ 0)) (h : Agree x y), truncate y = x
⊢ truncate y = x
have succ : ∀ (n : ℕ) (n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ) (h : Agree x y), truncate y = x) (x : CofixA F (n + 1))
  (y : CofixA F (n + 1).succ) (h : Agree x y), truncate y = x
Tactic: induction n with
  | zero =>
    cases x
    cases y
    rfl
  | succ n n_ih =>
    cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i n.succ)
have zero : ∀ (i : X), Agree (n := 0) (sCorec f i 0) (sCorec f i (succ 0))
Tactic: induction n generalizing i with
  | zero => constructor
  | succ n n_ih => exact .intro _ _ fun _ => n_ih _
Cleared hypotheses: i, n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
i : X
n : ℕ
zero : ∀ (i : X), Agree (n := 0) (sCorec f i 0) (sCorec f i (succ 0))
⊢ Agree (sCorec f i n) (sCorec f i n.succ)
have succ : ∀ (n : ℕ) (n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i n.succ)) (i : X),
  Agree (n := n + 1) (sCorec f i (n + 1)) (sCorec f i (n + 1).succ)
Tactic: induction n generalizing i with
  | zero => constructor
  | succ n n_ih => exact .intro _ _ fun _ => n_ih _
Cleared hypotheses: i, n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (n := n) (x n.succ) = head' (n := m) (x m.succ)
have suffices : ∀ (n : ℕ), head' (n := n) (x n.succ) = head' (n := 0) (x 1)
Tactic: suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
⊢ head' (n := n) (x n.succ) = head' (n := 0) (x 1)
have zero : head' (n := 0) (x (succ 0)) = head' (n := 0) (x 1)
Tactic: induction n with
  | zero => grind
  | succ n n_ih => grind +splitIndPred [Hconsistent (succ n), head']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
zero : head' (n := 0) (x (succ 0)) = head' (n := 0) (x 1)
⊢ head' (n := n) (x n.succ) = head' (n := 0) (x 1)
have succ : ∀ (n : ℕ) (n_ih : head' (n := n) (x n.succ) = head' (n := 0) (x 1)),
  head' (n := n + 1) (x (n + 1).succ) = head' (n := 0) (x 1)
Tactic: induction n with
  | zero => grind
  | succ n n_ih => grind +splitIndPred [Hconsistent (succ n), head']
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x y : F.M
H : ∀ (i : ℕ), x.approx i = y.approx i
⊢ x = y
have mk : ∀ (approx : (n : ℕ) → CofixA F n) (consistent : AllAgree approx)
  (H : ∀ (i : ℕ), { approx := approx, consistent := consistent : F.MIntl }.approx i = y.approx i),
  { approx := approx, consistent := consistent : F.MIntl } = y
Tactic: cases x
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
y : F.M
approx : (n : ℕ) → CofixA F n
consistent : AllAgree approx
H : ∀ (i : ℕ), { approx := approx, consistent := consistent : F.MIntl }.approx i = y.approx i
⊢ { approx := approx, consistent := consistent : F.MIntl } = y
have mk : ∀ (approx_1 : (n : ℕ) → CofixA F n) (consistent_1 : AllAgree approx_1)
  (H :
    ∀ (i : ℕ),
      { approx := approx, consistent := consistent : F.MIntl }.approx i =
        { approx := approx_1, consistent := consistent_1 }.approx i),
  { approx := approx, consistent := consistent : F.MIntl } = { approx := approx_1, consistent := consistent_1 }
Tactic: cases y
Cleared hypotheses: y, H
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
approx : (n : ℕ) → CofixA F n
consistent : AllAgree approx
approx_1 : (n : ℕ) → CofixA F n
consistent_1 : AllAgree approx_1
H :
  ∀ (i : ℕ),
    { approx := approx, consistent := consistent : F.MIntl }.approx i =
      { approx := approx_1, consistent := consistent_1 }.approx i
⊢ { approx := approx, consistent := consistent : F.MIntl } = { approx := approx_1, consistent := consistent_1 }
have mk : ∀ (n : ℕ), approx n = approx_1 n
Tactic: congr with n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (n := n) (x.approx n.succ) = head' (n := 0) (x.approx (succ 0))
n : ℕ
⊢ Agree.{uA, uB} (F := F) (n := n) ((fun (n : ℕ) ↦ children' (x.approx n.succ) (cast ⋯ i)) n)
    ((fun (n : ℕ) ↦ children' (x.approx n.succ) (cast ⋯ i)) n.succ)
have P' : Agree (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)
Tactic: have P' := x.2 (succ n)
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (n := n) (x.approx n.succ) = head' (n := 0) (x.approx (succ 0))
n : ℕ
P' : Agree (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)
⊢ Agree.{uA, uB} (F := F) (n := n) ((fun (n : ℕ) ↦ children' (x.approx n.succ) (cast ⋯ i)) n)
    ((fun (n : ℕ) ↦ children' (x.approx n.succ) (cast ⋯ i)) n.succ)
have apply : HEq (cast sorry i) (β := F.B (head' (n := n + 1) (x.approx n.succ.succ))) (cast sorry i)
Tactic: apply agree_children _ _ _ P'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (n := n) (x.approx n.succ) = head' (n := 0) (x.approx (succ 0))
n : ℕ
P' : Agree (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)
⊢ HEq (cast ⋯ i) (β := F.B (head' (n := n + 1) (x.approx n.succ.succ))) (cast ⋯ i)
have trans : cast sorry i ≍ i
Tactic: trans i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (n := n) (x.approx n.succ) = head' (n := 0) (x.approx (succ 0))
n : ℕ
P' : Agree (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)
trans : cast ⋯ i ≍ i
⊢ HEq (cast ⋯ i) (β := F.B (head' (n := n + 1) (x.approx n.succ.succ))) (cast ⋯ i)
have trans₁ : HEq i (β := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast sorry i)
Tactic: trans i
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
x : F.M
i : F.B x.head
H : ∀ (n : ℕ), head' (n := n) (x.approx n.succ) = head' (n := 0) (x.approx (succ 0))
n : ℕ
P' : Agree (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)
⊢ HEq i (β := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast ⋯ i)
have symm : HEq (α := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast sorry i) i
Tactic: symm
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
n : ℕ
⊢ Agree (n := n.succ) (Approx.sMk x n.succ) (Approx.sMk x n.succ.succ)
have a : ∀ (i : F.B (x.fst (β := fun (x : F.A) ↦ F.B x → F.M))),
  Agree ((x.snd (β := fun (x : F.A) ↦ F.B x → F.M) i).approx n)
    ((x.snd (β := fun (x : F.A) ↦ F.B x → F.M) i).approx (n + 1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
⊢ M.mk x.dest = x
have H : ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ (M.mk x.dest).approx n = x.approx n
have H : Approx.sMk x.dest n = x.approx n
Tactic: dsimp only [M.mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ Approx.sMk x.dest n = x.approx n
have H : ∀ (n : ℕ), Approx.sMk x.dest n = x.approx n → Eq (α := CofixA F (n + 1)) (Approx.sMk x.dest (n + 1)) (x.approx (n + 1))
Tactic: induction n with
  | zero => apply @Subsingleton.elim _ CofixA.instSubsingleton
  | succ n => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h : Approx.sMk x.dest n = x.approx n
⊢ Eq (α := CofixA F (n + 1)) (Approx.sMk x.dest (n + 1)) (x.approx (n + 1))
have H : Eq (α := CofixA F (n + 1))
  (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n)
  (x.approx (n + 1))
Tactic: dsimp only [Approx.sMk, dest, head]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h : Approx.sMk x.dest n = x.approx n
⊢ Eq (α := CofixA F (n + 1))
    (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n)
    (x.approx (n + 1))
have H : ∀ (hd : F.A) (ch : F.B hd → CofixA F n) (h : x.approx n.succ = CofixA.intro hd ch),
  (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro hd ch
Tactic: rcases h : x.approx (succ n) with - | ⟨hd, ch⟩
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ hd = head' (n := 0) (x.approx 1)
have Hconsistent : AllAgree x.approx
Tactic: rw [← head_succ' n, h, head']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro hd ch
have h' : hd = head' (n := 0) (x.approx 1)
Tactic: have h' : hd = head' (x.approx 1) := by
    rw [← head_succ' n, h, head']
    apply x.consistent
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
h' : hd = head' (n := 0) (x.approx 1)
⊢ (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro hd ch
have H : ∀ (ch : F.B hd → CofixA F n) (h : x.approx n.succ = CofixA.intro hd ch),
  (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro hd ch
Tactic: revert ch
Cleared hypotheses: ch, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
⊢ ∀ (ch : F.B hd → CofixA F n) (h : x.approx n.succ = CofixA.intro hd ch),
    (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
      CofixA.intro hd ch
have H : ∀ (ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n)
  (h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch),
  (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro (head' (n := 0) (x.approx 1)) ch
Tactic: rw [h']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
⊢ (CofixA.intro (head' (n := 0) (x.approx 1)) fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) =
    CofixA.intro (head' (n := 0) (x.approx 1)) ch
have H : (fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) = ch
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
⊢ (fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) = ch
have H : ∀ (a : F.B (head' (n := 0) (x.approx 1))), (x.children a).approx n = ch a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
⊢ (x.children a).approx n = ch a
have H : children' (x.approx n.succ) (cast sorry a) = ch a
Tactic: dsimp only [children]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
⊢ children' (x.approx n.succ) (cast ⋯ a) = ch a
have H : ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : cast sorry a = a''), children' (x.approx n.succ) a'' = ch a
Tactic: generalize hh : cast _ a = a''
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
a'' : F.B (head' (n := n) (x.approx n.succ))
hh : cast ⋯ a = a''
⊢ children' (x.approx n.succ) a'' = ch a
have hh₁ : a ≍ a''
Tactic: rw [cast_eq_iff_heq] at hh
Cleared hypotheses: hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
a'' : F.B (head' (n := n) (x.approx n.succ))
hh : a ≍ a''
⊢ children' (x.approx n.succ) a'' = ch a
have H : ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : a ≍ a''), children' (x.approx n.succ) a'' = ch a
Tactic: revert a''
Cleared hypotheses: a'', hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
⊢ ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : a ≍ a''), children' (x.approx n.succ) a'' = ch a
have H : ∀ (a'' : F.B (head' (CofixA.intro (head' (n := 0) (x.approx 1)) ch))) (hh : a ≍ a''),
  children' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a'' = ch a
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h_1 : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (n := 0) (x.approx 1)
ch : F.B (head' (n := 0) (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (n := 0) (x.approx 1)) ch
a : F.B (head' (n := 0) (x.approx 1))
a'' : F.B (head' (CofixA.intro (head' (n := 0) (x.approx 1)) ch))
hh : a ≍ a''
⊢ children' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a'' = ch a
have H : children' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a = ch a
Tactic: cases hh
Cleared hypotheses: a'', hh
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x y : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
h : M.mk x = M.mk y
⊢ x = y
have rw : (M.mk x).dest = y
Tactic: rw [← dest_mk x, h, dest_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x y : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
h : M.mk x = M.mk y
rw : (M.mk x).dest = y
⊢ x = y
have rw₁ : (M.mk y).dest = y
Tactic: rw [← dest_mk x, h, dest_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x y : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
h : M.mk x = M.mk y
rw : (M.mk x).dest = y
rw₁ : (M.mk y).dest = y
⊢ x = y
have rw₂ : y = y
Tactic: rw [← dest_mk x, h, dest_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x
have zero : ∀ (x : F.M), Agree' 0 x x
Tactic: induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : F.M
zero : ∀ (x : F.M), Agree' 0 x x
⊢ Agree' n x x
have succ : ∀ (n : ℕ) (n_ih : ∀ (x : F.M), Agree' n x x) (x : F.M), Agree' (n + 1) x x
Tactic: induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x
have zero : ∀ (a : F.A) (f : F.B a → F.M),
  Agree' 0 (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))
Tactic: induction x using PFunctor.M.casesOn'
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
x : F.M
⊢ Agree' (n + 1) x x
have succ : ∀ (a : F.A) (f : F.B a → F.M),
  Agree' (n + 1) (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))
Tactic: induction x using PFunctor.M.casesOn'
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
a : F.A
f : F.B a → F.M
⊢ Agree' (n + 1) (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))
have succ : 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
a : F.A
f : F.B a → F.M
succ succ₁ :
  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)
⊢ Agree' (n + 1) (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))
have succ₂ : ∀ (i : F.B a), Agree' n (f i) (f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y
have mp : Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
mp : Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y
have mpr : Agree' n x y → Agree (x.approx n) (y.approx (n + 1))
Tactic: constructor