awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
H : ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : cast ⋯ a = a''), children' (x.approx n.succ) a'' = ch a
⊢ children' (x.approx n.succ) (cast ⋯ a) = ch a

Tactic:
generalize hh : cast _ a = a''

Premises used: cast
-- Module: Mathlib.Data.PFunctor.Univariate.M
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''
⊢ a ≍ a''

Tactic:
rw [cast_eq_iff_heq] at hh

Premises used: cast_eq_iff_heq
-- Module: Mathlib.Data.PFunctor.Univariate.M
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''
H : ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : a ≍ a''), children' (x.approx n.succ) a'' = ch a
⊢ children' (x.approx n.succ) a'' = ch a

Tactic:
revert a''
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
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
⊢ ∀ (a'' : F.B (head' (n := n) (x.approx n.succ))) (hh : a ≍ a''), children' (x.approx n.succ) a'' = ch a

Tactic:
rw [h]
-- Module: Mathlib.Data.PFunctor.Univariate.M
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''
H : children' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a = ch a
⊢ children' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a'' = ch a

Tactic:
cases hh
-- Module: Mathlib.Data.PFunctor.Univariate.M
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' (CofixA.intro (head' (n := 0) (x.approx 1)) ch) a = ch a

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
rw₂ rw₃ : y = y
⊢ x = y

Tactic:
rw [← dest_mk x, h, dest_mk]

Premises used: PFunctor.M.dest_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f_1 : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
r : F.M → Sort w
f : (x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M) → r (M.mk x)
x : F.M
this rw : r (M.mk x.dest)
⊢ r x

Tactic:
rw [← mk_dest x]

Premises used: PFunctor.M.mk_dest
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f_1 : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
r : F.M → Sort w
f : (x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M) → r (M.mk x)
x : F.M
this : r (M.mk x.dest)
⊢ r (M.mk x.dest)

Tactic:
exact this
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
a : F.A
f : F.B a → F.M
i : ℕ
⊢ Eq (α := CofixA F i.succ) ((M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)).approx i.succ)
    (CofixA.intro a fun (j : F.B a) ↦ (f j).approx i)

Tactic:
rfl

Premises used: rfl, PFunctor.M.Approx.sMk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
⊢ Agree' 0 x x

Tactic:
?_
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
x : F.M
⊢ Agree' (n + 1) x x

Tactic:
?_
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : F.M
zero : ∀ (x : F.M), Agree' 0 x x
succ : ∀ (n : ℕ) (n_ih : ∀ (x : F.M), Agree' n x x) (x : F.M), Agree' (n + 1) x x
⊢ Agree' n x x

Tactic:
induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
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))
⊢ Agree' 0 x x

Tactic:
induction x using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
x : F.M
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))
⊢ Agree' (n + 1) x x

Tactic:
induction x using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
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:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
succ₂ : ∀ (i : F.B a), Agree' n (f i) (f i)
succ₃ : F.A
succ₄ succ₅ : 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:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
a : F.A
f : F.B a → F.M
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
a : F.A
f : F.B a → F.M
⊢ 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:
try rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : F.M), Agree' n x x
a : F.A
f : F.B a → F.M
i : F.B a
⊢ Agree' n (f i) (f i)

Tactic:
apply n_ih
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
mp : Agree (x.approx n) (y.approx (n + 1)) → Agree' n x y
mpr : Agree' n x y → Agree (x.approx n) (y.approx (n + 1))
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x y : F.M
h : Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))
⊢ Agree' 0 x y

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
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
⊢ Agree' (n + 1) x y

Tactic:
induction x using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
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))
⊢ Agree' (n + 1) (M.mk (Sigma.mk (β := fun (x : F.A) ↦ F.B x → F.M) a f)) y

Tactic:
induction y using PFunctor.M.casesOn'

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
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))
⊢ 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:
obtain - | ⟨_, _, hagree⟩ := h
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
mp₂ : ∀ (i : F.B a), Agree' n_1 (f i) (f_1 i)
mp₃ : F.A
mp₄ mp₅ : F.B a → F.M
⊢ 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))

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
⊢ 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:
try rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
⊢ 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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
⊢ 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:
try rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
mp : Agree ((f i).approx n_1) ((f_1 i).approx (n_1 + 1))
⊢ Agree' n_1 (f i) (f_1 i)

Tactic:
apply n_ih
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 ((f i).approx n_1) ((f_1 i).approx (n_1 + 1))

Tactic:
apply hagree
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
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
⊢ Agree' n 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

Premises used: PFunctor.M.casesOn', PFunctor.M.approx_mk, Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x y : F.M
h : Agree' 0 x y
⊢ Agree (n := 0) (x.approx 0) (y.approx (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
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))
⊢ Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))

Tactic:
obtain - | @⟨_, a, x', y'⟩ := h
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
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))
⊢ Agree (n := n + 1) (x.approx (n + 1)) (y.approx (n + 1 + 1))

Tactic:
induction x using PFunctor.M.casesOn' with | _ x_a x_f

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
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))
⊢ 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 y using PFunctor.M.casesOn' with | _ y_a y_f

Premises used: PFunctor.M.casesOn'
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
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))
⊢ 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:
simp only [approx_mk]

Premises used: PFunctor.M.approx_mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
⊢ 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'⟩›
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
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))
⊢ 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:
cases h_a_1
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
⊢ 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'⟩›
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
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))
⊢ 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_2
-- Module: Mathlib.Data.PFunctor.Univariate.M
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')
mpr : ∀ (i : F.B a), Agree ((x' i).approx n) ((y' i).approx (n + 1))
⊢ 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:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
mpr : Agree' n (x' i) (y' i)
⊢ Agree ((x' i).approx n) ((y' i).approx (n + 1))

Tactic:
apply n_ih
-- Module: Mathlib.Data.PFunctor.Univariate.M
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' n (x' i) (y' i)

Tactic:
simp [*]