awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
pos :
  ∀ (h'' : a = x_a),
    Eq.{uA + 1} (α := F.A)
      (head
        ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
          fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
      (head default)
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)
have neg : ∀ (h'' : ¬a = x_a),
  Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast sorry i)) else default))
    (head default)
Tactic: by_cases h'' : a = x_a
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_a : F.A
x_f : F.B x_a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f))
h'' : a = x_a
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)
have pos : ∀ (x_f : F.B a → F.M)
  (h :
    ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
        (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))),
  Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast sorry i)) else default))
    (head default)
Tactic: subst x_a
Cleared hypotheses: x_a, x_f, h, h''
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
⊢ Eq.{uA + 1} (α := F.A)
    (head
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)).casesOn' (r := fun (x : F.M) ↦ F.M)
        fun (a' : F.A) (f : F.B a' → F.M) ↦ if h : a = a' then isubtree ps_tail (f (cast ⋯ i)) else default))
    (head default)
have pos : (isubtree ps_tail (x_f (cast sorry i))).head = head default
Tactic: simp only [dif_pos, casesOn_mk']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
⊢ (isubtree ps_tail (x_f (cast ⋯ i))).head = head default
have pos : ¬IsPath ps_tail (x_f (cast sorry i))
Tactic: rw [ps_ih]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ False
have pos : IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
    (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
have pos : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), (isubtree ps_tail x).head = head default
a : F.A
i : F.B a
x_f : F.B a → F.M
h :
  ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
      (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
h' : IsPath ps_tail (x_f (cast ⋯ i))
pos :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f)
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail)
    (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_f))
have pos₁ : IsPath ps_tail (x_f i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
x : F.M
h : ¬IsPath ps x
⊢ iselect ps x = head default
have nil : ∀ (x : F.M) (h : ¬IsPath [] x), iselect [] x = head default
Tactic: induction ps generalizing x with
  | nil =>
    exfalso
    apply h
    constructor
  | cons ps_hd ps_tail ps_ih =>
    obtain ⟨a, i⟩ := ps_hd
    induction x using PFunctor.M.casesOn' with | _ x_a x_f
    simp only [iselect, isubtree] at ps_ih ⊢
    by_cases h'' : a = x_a
    · subst x_a
      simp only [dif_pos, casesOn_mk']
      rw [ps_ih]
      intro h'
      apply h
      constructor <;> try rfl
      apply h'
    · simp [*]
Cleared hypotheses: ps, x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
x : F.M
h : ¬IsPath ps x
nil : ∀ (x : F.M) (h : ¬IsPath [] x), iselect [] x = head default
⊢ iselect ps x = head default
have cons : ∀ (ps_hd : F.Idx) (ps_tail : List F.Idx) (ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = head default)
  (x : F.M) (h : ¬IsPath (ps_hd :: ps_tail) x), iselect (ps_hd :: ps_tail) x = head default
Tactic: induction ps generalizing x with
  | nil =>
    exfalso
    apply h
    constructor
  | cons ps_hd ps_tail ps_ih =>
    obtain ⟨a, i⟩ := ps_hd
    induction x using PFunctor.M.casesOn' with | _ x_a x_f
    simp only [iselect, isubtree] at ps_ih ⊢
    by_cases h'' : a = x_a
    · subst x_a
      simp only [dif_pos, casesOn_mk']
      rw [ps_ih]
      intro h'
      apply h
      constructor <;> try rfl
      apply h'
    · simp [*]
Cleared hypotheses: ps, x, h
-- 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
⊢ x.fst (β := fun (x : F.A) ↦ F.B x → F.M) = (M.mk x).dest.fst (β := fun (x : F.A) ↦ F.B x → F.M)
have rw : x.fst (β := fun (x : F.A) ↦ F.B x → F.M) = x.fst (β := fun (x : F.A) ↦ F.B x → F.M)
Tactic: rw [dest_mk]
-- 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
a : F.A
x : F.B a → F.M
i : F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head
⊢ F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head = F.B a
have rw : F.B (Sigma.fst (β := fun (x : F.A) ↦ F.B x → F.M) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)) = F.B a
Tactic: rw [head_mk]
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
a : F.A
x : F.B a → F.M
i : F.B (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).head
⊢ (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).children i = x (cast ⋯ i)
have H : ∀ (i_1 : ℕ),
  ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)).children i).approx i_1 = (x (cast sorry i)).approx i_1
Tactic: apply ext'
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
inst : DecidableEq F.A
inst_1 : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree (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)) =
    isubtree ps (f i)
have simp : isubtree ps (f (cast sorry i)) = isubtree ps (f i)
Tactic: simp only [isubtree, dif_pos, isubtree, M.casesOn_mk']
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := ⋯ : F.MIntl } =
    { approx := Approx.sMk (F.map (M.corec f) (f x₀)), consistent := ⋯ }
have e_approx : ∀ (n : ℕ), sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n
Tactic: congr with n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n
have e_approx : Eq (α := CofixA F 0) (sCorec f x₀ 0) (Approx.sMk (F.map (M.corec f) (f x₀)) 0)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
e_approx : Eq (α := CofixA F 0) (sCorec f x₀ 0) (Approx.sMk (F.map (M.corec f) (f x₀)) 0)
⊢ sCorec f x₀ n = Approx.sMk (F.map (M.corec f) (f x₀)) n
have e_approx₁ : ∀ (n : ℕ), Eq (α := CofixA F (n + 1)) (sCorec f x₀ (n + 1)) (Approx.sMk (F.map (M.corec f) (f x₀)) (n + 1))
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
⊢ Eq (α := CofixA F (n + 1))
    (CofixA.intro ((f x₀).fst (β := fun (x : F.A) ↦ F.B x → X))
      fun (i : F.B ((f x₀).fst (β := fun (x : F.A) ↦ F.B x → X))) ↦
      sCorec f ((f x₀).snd (β := fun (x : F.A) ↦ F.B x → X) i) n)
    (CofixA.intro ((F.map (M.corec f) (f x₀)).fst (β := fun (x : F.A) ↦ F.B x → F.M))
      fun (i : F.B ((F.map (M.corec f) (f x₀)).fst (β := fun (x : F.A) ↦ F.B x → F.M))) ↦
      ((F.map (M.corec f) (f x₀)).snd (β := fun (x : F.A) ↦ F.B x → F.M) i).approx n)
have e_approx : ∀ (fst : F.A) (snd : F.B fst → X),
  Eq (α := CofixA F (n + 1))
    (CofixA.intro (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))
      fun (i : F.B (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))) ↦
      sCorec f (Sigma.snd (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd) i) n)
    (CofixA.intro
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦ F.B x → F.M))
      fun
        (i :
          F.B
            ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦
              F.B x → F.M))) ↦
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).snd (β := fun (x : F.A) ↦ F.B x → F.M)
            i).approx
        n)
Tactic: cases f x₀
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_2
f : X → (↑F : (α : Type u_2) → Type (max u_2 uA uB)) X
x₀ : X
n : ℕ
fst : F.A
snd : F.B fst → X
⊢ Eq (α := CofixA F (n + 1))
    (CofixA.intro (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))
      fun (i : F.B (Sigma.fst (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd))) ↦
      sCorec f (Sigma.snd (β := fun (x : F.A) ↦ F.B x → X) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd) i) n)
    (CofixA.intro
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦ F.B x → F.M))
      fun
        (i :
          F.B
            ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).fst (β := fun (x : F.A) ↦
              F.B x → F.M))) ↦
      ((F.map (M.corec f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → X) fst snd)).snd (β := fun (x : F.A) ↦ F.B x → F.M)
            i).approx
        n)
have e_approx : Eq (α := CofixA F (n + 1)) (CofixA.intro fst fun (i : F.B fst) ↦ sCorec f (snd i) n)
  (CofixA.intro fst fun (i : F.B fst) ↦ ((M.corec f ∘ snd) i).approx n)
Tactic: dsimp only [PFunctor.map]
-- 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
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : ∀ (ps : Path F), 0 = length ps → iselect ps x = iselect ps y
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1)) (x.approx (HAdd.hAdd (α := ℕ) 0 1)) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
have hrec₁ : iselect [] x = iselect [] y
Tactic: specialize hrec [] rfl
Cleared hypotheses: hrec
-- 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
x y z : F.M
hx : Agree' 0 z x
hy : Agree' 0 z y
hrec : iselect [] x = iselect [] y
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1)) (x.approx (HAdd.hAdd (α := ℕ) 0 1)) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
have zero : ∀ (a : F.A) (f : F.B a → F.M) (hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)))
  (hrec : iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect [] y),
  Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    (y.approx (HAdd.hAdd (α := ℕ) 0 1))
Tactic: induction x using PFunctor.M.casesOn'
Cleared hypotheses: x, hx, hrec
-- 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
y z : F.M
hy : Agree' 0 z y
a : F.A
f : F.B a → F.M
hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
hrec : iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) = iselect [] y
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    (y.approx (HAdd.hAdd (α := ℕ) 0 1))
have zero : ∀ (a_1 : F.A) (f_1 : F.B a_1 → F.M) (hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)))
  (hrec :
    iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) =
      iselect [] (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1))),
  Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)).approx (HAdd.hAdd (α := ℕ) 0 1))
Tactic: induction y using PFunctor.M.casesOn'
Cleared hypotheses: y, hy, hrec
-- 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
z : F.M
a : F.A
f : F.B a → F.M
hx : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f))
a_1 : F.A
f_1 : F.B a_1 → F.M
hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1))
hrec : a = a_1
⊢ Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)).approx (HAdd.hAdd (α := ℕ) 0 1))
have zero : ∀ (f_2 : F.B a → F.M) (hy : Agree' 0 z (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_2))),
  Eq (α := CofixA F (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (HAdd.hAdd (α := ℕ) 0 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_2)).approx (HAdd.hAdd (α := ℕ) 0 1))
Tactic: subst hrec
Cleared hypotheses: a_1, f_1, hy, hrec
-- 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))
x y z : F.M
hx : Agree' (n + 1) z x
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
have succ : ∀ {a : F.A} (x_1 y_1 : F.B a → F.M),
  (∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)) →
    z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1) →
      x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1) →
        Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
Tactic: cases hx
Cleared hypotheses: hx
-- 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))
x y z : F.M
hy : Agree' (n + 1) z y
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
a : F.A
x_1 y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1)
h_2 : x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
have succ : ∀ {a : F.A} (x_2 y_2 : F.B a → F.M),
  (∀ (i : F.B a), Agree' n (x_2 i) (y_2 i)) →
    z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_2) →
      y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_2) →
        Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
Tactic: cases hy
Cleared hypotheses: hy
-- 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))
x y z : F.M
hrec : ∀ (ps : Path F), n + 1 = length ps → iselect ps x = iselect ps y
a : F.A
x_1 y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x_1 i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x_1)
h_2 : x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y_1)
a_1 : F.A
x_2 y_2 : F.B a_1 → F.M
h_3 : ∀ (i : F.B a_1), Agree' n (x_2 i) (y_2 i)
h_4 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_2)
h_5 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2)
⊢ Eq (α := CofixA F (n + 1 + 1)) (x.approx (n + 1 + 1)) (y.approx (n + 1 + 1))
have succ : ∀ (a_2 : F.A) (f : 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_2 f)) = iselect ps y),
  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_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))
      (y.approx (n + 1 + 1))
Tactic: induction x using PFunctor.M.casesOn'
Cleared hypotheses: x, hrec, h_2
-- 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))
y z : F.M
a : F.A
x y_1 : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y_1 i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
a_1 : F.A
x_1 y_2 : F.B a_1 → F.M
h_2 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_2 i)
h_3 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
h_4 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2)
a_2 : F.A
f : 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_2 f)) = iselect ps y
h_5 :
  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_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))
    (y.approx (n + 1 + 1))
have succ : ∀ (a : F.A) (f_1 : F.B a → F.M),
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f_1) =
      M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 y_2) →
    ∀
      (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 f_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 f_1)).approx (n + 1 + 1))
Tactic: induction y using PFunctor.M.casesOn'
Cleared hypotheses: y, h_4, hrec
-- 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))
z : F.M
a : F.A
x y : F.B a → F.M
h : ∀ (i : F.B a), Agree' n (x i) (y i)
h_1 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x)
a_1 : F.A
x_1 y_1 : F.B a_1 → F.M
h_2 : ∀ (i : F.B a_1), Agree' n (x_1 i) (y_1 i)
h_3 : z = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 x_1)
a_2 : F.A
f : F.B a_2 → F.M
h_4 : 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_5 :
  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))
⊢ 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 a : 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)
Tactic: subst z
Cleared hypotheses: z, h_1, h_3