awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n) (y.approx (n + 1))), Agree' n x y
x y : F.M
h : Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
⊢ Agree' (n + 1) x y
have mp : ∀ (a : F.A) (f : F.B a → F.M)
  (h :
    Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (n + 1))
      (y.approx (n + 1 + 1))),
  Agree' (n + 1) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) y
Tactic: induction x using PFunctor.M.casesOn'
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n) (y.approx (n + 1))), Agree' n x y
y : F.M
a : F.A
f : F.B a → F.M
h : Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (n + 1)) (y.approx (n + 1 + 1))
⊢ Agree' (n + 1) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) y
have mp : ∀ (a_1 : F.A) (f_1 : F.B a_1 → F.M)
  (h :
    Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx (n + 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a_1 f_1)).approx (n + 1 + 1))),
  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_1 f_1))
Tactic: induction y using PFunctor.M.casesOn'
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n) (y.approx (n + 1))), Agree' n x y
a : F.A
f : F.B a → F.M
a_1 : F.A
f_1 : F.B a_1 → F.M
h :
  Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (f j).approx n)
    (CofixA.intro a_1 fun (j : F.B a_1) ↦ (f_1 j).approx (n + 1))
⊢ 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_1 f_1))
have mp : ∀ {n_1 : ℕ} (f_2 : F.B a → F.M)
  (hagree :
    ∀ (i : F.B a),
      Agree.{uA, uB} (F := F) (n := n) ((fun (j : F.B a) ↦ (f j).approx n) i)
        ((fun (j : F.B a) ↦ ((f_2 j).approx (n + 1) : CofixA F (n + 1))) i)),
  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_2))
Tactic: obtain - | ⟨_, _, hagree⟩ := h
Cleared hypotheses: a_1, f_1, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n_1) (y.approx (n_1 + 1))), Agree' n_1 x y
a : F.A
f : F.B a → F.M
n : ℕ
f_1 : F.B a → F.M
hagree :
  ∀ (i : F.B a),
    Agree.{uA, uB} (F := F) (n := n_1) ((fun (j : F.B a) ↦ (f j).approx n_1) i)
      ((fun (j : F.B a) ↦ ((f_1 j).approx (n_1 + 1) : CofixA F (n_1 + 1))) i)
⊢ Agree' (n_1 + 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_1))
have mp : 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_1 : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n_1) (y.approx (n_1 + 1))), Agree' n_1 x y
a : F.A
f : F.B a → F.M
n : ℕ
f_1 : F.B a → F.M
hagree :
  ∀ (i : F.B a),
    Agree.{uA, uB} (F := F) (n := n_1) ((fun (j : F.B a) ↦ (f j).approx n_1) i)
      ((fun (j : F.B a) ↦ ((f_1 j).approx (n_1 + 1) : CofixA F (n_1 + 1))) i)
mp : 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 + 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_1))
have mp₁ : 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 f_1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n_1) (y.approx (n_1 + 1))), Agree' n_1 x y
a : F.A
f : F.B a → F.M
n : ℕ
f_1 : F.B a → F.M
hagree :
  ∀ (i : F.B a),
    Agree.{uA, uB} (F := F) (n := n_1) ((fun (j : F.B a) ↦ (f j).approx n_1) i)
      ((fun (j : F.B a) ↦ ((f_1 j).approx (n_1 + 1) : CofixA F (n_1 + 1))) i)
mp : 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)
mp₁ :
  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 f_1)
⊢ Agree' (n_1 + 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_1))
have mp₂ : ∀ (i : F.B a), Agree' n_1 (f i) (f_1 i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n_1 : ℕ
n_ih : ∀ (x y : F.M) (h : Agree (x.approx n_1) (y.approx (n_1 + 1))), Agree' n_1 x y
a : F.A
f : F.B a → F.M
n : ℕ
f_1 : F.B a → F.M
hagree :
  ∀ (i : F.B a),
    Agree.{uA, uB} (F := F) (n := n_1) ((fun (j : F.B a) ↦ (f j).approx n_1) i)
      ((fun (j : F.B a) ↦ ((f_1 j).approx (n_1 + 1) : CofixA F (n_1 + 1))) i)
i : F.B a
⊢ Agree' n_1 (f i) (f_1 i)
have mp : Agree ((f i).approx n_1) ((f_1 i).approx (n_1 + 1))
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
⊢ Agree' n x y
have mp : ∀ (x y : F.M) (h : Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))), Agree' 0 x y
Tactic: induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
mp : ∀ (x y : F.M) (h : Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))), Agree' 0 x y
⊢ Agree' n x y
have mp₁ : ∀ (n : ℕ) (n_ih : ∀ (x y : F.M) (h : Agree (x.approx n) (y.approx (n + 1))), Agree' n x y) (x y : F.M)
  (h : Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))), Agree' (n + 1) x y
Tactic: induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      induction x using PFunctor.M.casesOn'
      induction y using PFunctor.M.casesOn'
      simp only [approx_mk] at h
      obtain - | ⟨_, _, hagree⟩ := h
      constructor <;> try rfl
      intro i
      apply n_ih
      apply hagree
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (y.approx (n + 1))
x y : F.M
h : Agree' (n + 1) x y
⊢ Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
have mpr : ∀ {a : F.A} (x' y' : F.B a → F.M),
  (∀ (i : F.B a), Agree' n (x' i) (y' i)) →
    x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x') →
      y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') →
        Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
Tactic: obtain - | @⟨_, a, x', y'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (y.approx (n + 1))
x y : 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 : x = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
h_2 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
⊢ Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
have mpr : ∀ (x_a : F.A) (x_f : F.B x_a → F.M),
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x') →
    Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).approx (n + 1))
      (y.approx (n + 1 + 1))
Tactic: induction x using PFunctor.M.casesOn' with | _ x_a x_f
Cleared hypotheses: x, h_1
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (y.approx (n + 1))
y : 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 : y = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
x_a : F.A
x_f : F.B x_a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
⊢ Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).approx (n + 1))
    (y.approx (n + 1 + 1))
have mpr : ∀ (y_a : F.A) (y_f : F.B y_a → F.M),
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') →
    Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).approx (n + 1))
      ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f)).approx (n + 1 + 1))
Tactic: induction y using PFunctor.M.casesOn' with | _ y_a y_f
Cleared hypotheses: y, h_1
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
x_a : F.A
x_f : F.B x_a → F.M
h_1 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
y_a : F.A
y_f : F.B y_a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
⊢ Agree (n := n + 1) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f)).approx (n + 1))
    ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f)).approx (n + 1 + 1))
have mpr : Agree (n := n + 1) (CofixA.intro x_a fun (j : F.B x_a) ↦ (x_f j).approx n)
  (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f 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}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
x_a : F.A
x_f : F.B x_a → F.M
h_1 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
y_a : F.A
y_f : F.B y_a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
⊢ Agree (n := n + 1) (CofixA.intro x_a fun (j : F.B x_a) ↦ (x_f j).approx n)
    (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f j).approx (n + 1))
have h_a_1 : 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) x_a x_f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
Tactic: have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
x_a : F.A
x_f : F.B x_a → F.M
h_1 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) x_a x_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
y_a : F.A
y_f : F.B y_a → F.M
h_2 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
h_a_1 :
  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) x_a x_f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a x')
⊢ Agree (n := n + 1) (CofixA.intro x_a fun (j : F.B x_a) ↦ (x_f j).approx n)
    (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f j).approx (n + 1))
have mpr : 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') →
  Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (x' j).approx n)
    (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f j).approx (n + 1))
Tactic: cases h_a_1
Cleared hypotheses: x_a, x_f, h_1, h_a_1
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
y_a : F.A
y_f : F.B y_a → F.M
h_1 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
h_2 : 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')
⊢ Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (x' j).approx n)
    (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f j).approx (n + 1))
have h_a_2 : 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) y_a y_f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
Tactic: replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
y_a : F.A
y_f : F.B y_a → F.M
h_1 :
  M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) y_a y_f) = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
h_2 : 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')
h_a_2 :
  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) y_a y_f) (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
⊢ Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (x' j).approx n)
    (CofixA.intro y_a fun (j : F.B y_a) ↦ (y_f j).approx (n + 1))
have mpr : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') →
  Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (x' j).approx n)
    (CofixA.intro a fun (j : F.B a) ↦ (y' j).approx (n + 1))
Tactic: cases h_a_2
Cleared hypotheses: y_a, y_f, h_1, h_a_2
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
h_1 : 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')
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
⊢ Agree (n := n + 1) (CofixA.intro a fun (j : F.B a) ↦ (x' j).approx n)
    (CofixA.intro a fun (j : F.B a) ↦ (y' j).approx (n + 1))
have mpr : ∀ (i : F.B a), Agree ((x' i).approx n) ((y' i).approx (n + 1))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (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)
h_1 : 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')
h_2 : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y') = M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a y')
i : F.B a
⊢ Agree ((x' i).approx n) ((y' i).approx (n + 1))
have mpr : Agree' n (x' i) (y' i)
Tactic: apply n_ih
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree' n x y
⊢ Agree (x.approx n) (y.approx (n + 1))
have mpr : ∀ (x y : F.M) (h : Agree' 0 x y), Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
Tactic: induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree' n x y
mpr : ∀ (x y : F.M) (h : Agree' 0 x y), Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
⊢ Agree (x.approx n) (y.approx (n + 1))
have mpr₁ : ∀ (n : ℕ) (n_ih : ∀ (x y : F.M) (h : Agree' n x y), Agree (x.approx n) (y.approx (n + 1))) (x y : F.M)
  (h : Agree' (n + 1) x y), Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))
Tactic: induction n generalizing x y with
    | zero => constructor
    | succ _ n_ih =>
      obtain - | @⟨_, a, x', y'⟩ := h
      induction x using PFunctor.M.casesOn' with | _ x_a x_f
      induction y using PFunctor.M.casesOn' with | _ y_a y_f
      simp only [approx_mk]
      have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
      cases h_a_1
      replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
      cases h_a_2
      constructor
      intro i
      apply n_ih
      simp [*]
Cleared hypotheses: n, x, y, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a' i :: xs) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) →
    a = a'
have generalize : ∀ (x : F.M) (h : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f) = x),
  IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a' i :: xs) x → a = a'
Tactic: generalize h : M.mk ⟨a, f⟩ = x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a a' : F.A
f : F.B a → F.M
i : F.B a'
f_1 : F.B a' → F.M
h_1 : IsPath xs (f_1 i)
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_1)
⊢ a = a'
have cons : ∀ {i : F.B a},
  IsPath xs (f i) →
    ∀
      (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)),
      a = a
Tactic: cases mk_inj h
Cleared hypotheses: a', i, f_1, h_1, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: xs) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) →
    IsPath xs (f i)
have generalize : ∀ (x : F.M) (h : M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f) = x),
  IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: xs) x → IsPath xs (f i)
Tactic: generalize h : M.mk ⟨a, f⟩ = x
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (hypothesis)
Goal:
F : PFunctor.{uA, uB}
xs : Path F
a : F.A
f : F.B a → F.M
i : F.B a
f_1 : F.B a → F.M
hp : IsPath xs (f_1 i)
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_1)
hp₁ : IsPath xs (f i)
⊢ IsPath xs (f i)
have 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)
Tactic: cases mk_inj h
Cleared hypotheses: f_1, hp, h
-- Lean 4 proof step from Mathlib.Data.PFunctor.Univariate.M (goal)
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f_1 : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
inst : DecidableEq F.A
inst_1 : Inhabited F.M
a : F.A
i : F.B a
ps : List F.Idx
x : F.M
a' : F.A
f : F.B a' → F.M
h : a = a'
⊢ F.B a = F.B a'
have rw : F.B a' = F.B a'
Tactic: rw [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
x : F.M
h : ¬IsPath [] x
⊢ iselect [] x = head default
have nil : False
Tactic: exfalso
-- 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
x : F.M
h : ¬IsPath [] x
⊢ False
have nil : IsPath [] x
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_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
have cons : ∀ (a : F.A) (i : F.B a) (h : ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x),
  iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x = head default
Tactic: obtain ⟨a, i⟩ := ps_hd
Cleared hypotheses: ps_hd, 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), iselect ps_tail x = head default
x : F.M
a : F.A
i : F.B a
h : ¬IsPath (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x
⊢ iselect (Sigma.mk (β := fun (x : F.A) ↦ F.B x) a i :: ps_tail) x = head default
have cons : ∀ (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))),
  iselect (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)) =
    head default
Tactic: induction x using PFunctor.M.casesOn' with | _ x_a x_f
Cleared hypotheses: 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_tail : List F.Idx
ps_ih : ∀ (x : F.M) (h : ¬IsPath ps_tail x), iselect ps_tail x = 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))
⊢ iselect (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)) =
    head default
have cons : 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: simp only [iselect, isubtree] at 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_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))
⊢ 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 : ∀ (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