awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ (y : P.B a), f y = x
h₁ : ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
⊢ ∀ ⦃p : α → Prop⦄,
    Liftp (F := (↑P : (α : Type u) → Type (max u uA uB))) p (Sigma.mk (β := fun (x : P.A) ↦ P.B x → α) a f) → p x

Tactic:
simp only [liftp_iff']

Premises used: PFunctor.liftp_iff'
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ (y : P.B a), f y = x
h₁ : ∀ (w : P.B a), f w = x → ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Tactic:
cases h
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
w : P.B a
h_1 : f w = x
h : ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w)
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p x

Tactic:
subst x
-- Module: Mathlib.Data.PFunctor.Univariate.Basic
Goal:
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
w : P.B a
h h₁ h₂ h₃ h₄ h₅ h₆ h₇ : ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w)
⊢ ∀ ⦃p : α → Prop⦄, (∀ (i : P.B a), p (f i)) → p (f w)

Tactic:
tauto
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
x : CofixA F (n + 1)
intro :
  ∀ (a : F.A) (a_1 : F.B a → CofixA F n),
    CofixA.intro a a_1 = CofixA.intro (head' (CofixA.intro a a_1)) (children' (CofixA.intro a a_1))
⊢ x = CofixA.intro (head' x) (children' x)

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n : ℕ
a : F.A
a_1 : F.B a → CofixA F n
⊢ CofixA.intro a a_1 = CofixA.intro (head' (CofixA.intro a a_1)) (children' (CofixA.intro a a_1))

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F 1
⊢ Agree x y

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

Tactic:
obtain - | ⟨_, _, hagree⟩ := h₁
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
intro : Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') i)
⊢ Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') j)

Tactic:
cases h₀
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))
⊢ Agree (children' (CofixA.intro a x) i) (children' (CofixA.intro a x') i)

Tactic:
apply hagree
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : CofixA F 0
y : CofixA F (succ 0)
h : Agree x y
zero : ∀ (h : Agree CofixA.continue y), truncate y = CofixA.continue
⊢ truncate y = x

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
y : CofixA F (succ 0)
h : Agree CofixA.continue y
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
⊢ truncate y = CofixA.continue

Tactic:
cases y
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
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:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
succ : (CofixA.intro a fun (x : F.B a) ↦ truncate (y x)) = CofixA.intro a f
⊢ truncate (CofixA.intro a y) = CofixA.intro a f

Tactic:
simp only [truncate, Function.comp_def]

Premises used: Function.comp_def, PFunctor.Approx.truncate
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
succ : ∀ (y_1 : F.B a), truncate (y y_1) = f y_1
⊢ (CofixA.intro a fun (x : F.B a) ↦ truncate (y x)) = CofixA.intro a f

Tactic:
congr with y
-- Module: Mathlib.Data.PFunctor.Univariate.M
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_1 : F.B a → CofixA F (n + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y_1 i)
y : F.B a
⊢ truncate (y_1 y) = f y

Tactic:
n_ih _ _ (h₁ y)
-- Module: Mathlib.Data.PFunctor.Univariate.M
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_1 : F.B a → CofixA F (n + 1)
h₁ : ∀ (i : F.B a), Agree (f i) (y_1 i)
y : F.B a
⊢ truncate (y_1 y) = f y

Tactic:
exact n_ih _ _ (h₁ y)
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
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
⊢ truncate y = x

Tactic:
cases h with | intro f y h₁ =>
    simp only [truncate, Function.comp_def]
    congr with y
    exact n_ih _ _ (h₁ y)

Premises used: Function.comp_def, PFunctor.Approx.truncate
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 (Nat.succ 0)) (h : Agree x y), truncate y = x
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
⊢ 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)

Premises used: Function.comp_def, PFunctor.Approx.truncate, Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
i : X
⊢ Agree (n := 0) (sCorec f i 0) (sCorec f i (succ 0))

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
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:
.intro _ _ fun _ => n_ih _

Premises used: PFunctor.Approx.sCorec, Sigma.snd, PFunctor.Approx.Agree.intro
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
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:
exact .intro _ _ fun _ => n_ih _
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 (Nat.succ 0))
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)
⊢ Agree (sCorec f i n) (sCorec f i n.succ)

Tactic:
induction n generalizing i with
  | zero => constructor
  | succ n n_ih => exact .intro _ _ fun _ => n_ih _

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type w
f : X → (↑F : (α : Type w) → Type (max w uA uB)) X
⊢ Eq (α := CofixA F 0) «continue» «continue»

Tactic:
rfl
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
this : ∀ (n : ℕ), head' (n := n) (x n.succ) = head' (n := 0) (x 1)
⊢ head' (n := n) (x n.succ) = head' (n := m) (x m.succ)

Tactic:
simp [this]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
suffices : ∀ (n : ℕ), head' (n := n) (x n.succ) = head' (n := 0) (x 1)
⊢ head' (n := n) (x n.succ) = head' (n := m) (x m.succ)

Tactic:
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (n := 0) (x (succ 0)) = head' (n := 0) (x 1)

Tactic:
grind
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n_1 m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
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:
grind +splitIndPred [Hconsistent (succ n), head']

Premises used: Nat.succ, PFunctor.Approx.head'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n_1 m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
zero : head' (n := 0) (x (Nat.succ 0)) = head' (n := 0) (x 1)
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)
⊢ head' (n := n) (x n.succ) = head' (n := 0) (x 1)

Tactic:
induction n with
  | zero => grind
  | succ n n_ih => grind +splitIndPred [Hconsistent (succ n), head']

Premises used: Nat.zero, Nat.succ, PFunctor.Approx.head'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x y : F.M
H : ∀ (i : ℕ), x.approx i = y.approx i
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
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
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 }
⊢ { approx := approx, consistent := consistent : F.MIntl } = y

Tactic:
cases y
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
mk : ∀ (n : ℕ), approx n = approx_1 n
⊢ { approx := approx, consistent := consistent : F.MIntl } = { approx := approx_1, consistent := consistent_1 }

Tactic:
congr with n
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
n : ℕ
⊢ approx n = approx_1 n

Tactic:
apply H
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 : ℕ
⊢ x.head = head' (n := n) (x.approx n.succ)

Tactic:
simp only [head, H]

Premises used: PFunctor.M.head
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 (n := n.succ) (x.approx n.succ) (x.approx n.succ.succ)

Tactic:
have P' := x.2 (succ n)
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
apply : HEq (cast ⋯ i) (β := F.B (head' (n := n + 1) (x.approx n.succ.succ))) (cast ⋯ i)
⊢ 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)

Tactic:
apply agree_children _ _ _ P'

Premises used: PFunctor.Approx.agree_children
-- Module: Mathlib.Data.PFunctor.Univariate.M
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
trans₁ : HEq i (β := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast ⋯ i)
⊢ HEq (cast ⋯ i) (β := F.B (head' (n := n + 1) (x.approx n.succ.succ))) (cast ⋯ i)

Tactic:
trans i
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
⊢ cast ⋯ i ≍ i

Tactic:
apply cast_heq

Premises used: cast_heq
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
symm : HEq (α := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast ⋯ i) i
⊢ HEq i (β := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast ⋯ i)

Tactic:
symm
-- Module: Mathlib.Data.PFunctor.Univariate.M
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 (α := F.B (head' (n := n.succ) (x.approx n.succ.succ))) (cast ⋯ i) i

Tactic:
apply cast_heq

Premises used: cast_heq
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
X : Type u_1
f : X → (↑F : (α : Type u_1) → Type (max u_1 uA uB)) X
inst : Inhabited F.M
inst_1 : DecidableEq F.A
i : F.Idx
x : F.M
H' : i.fst (β := fun (x : F.A) ↦ F.B x) = x.head
⊢ i.fst (β := fun (x : F.A) ↦ F.B x) = x.head

Tactic:
simp only [head, H']

Premises used: PFunctor.M.head
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
n m : ℕ
x : F.M
⊢ head' (n := n) (x.approx n.succ) = head' (n := m) (x.approx m.succ)

Tactic:
head_succ' n m _ x.consistent

Premises used: PFunctor.MIntl.consistent, PFunctor.Approx.head_succ'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
⊢ truncate (x.approx (n + 1)) = x.approx n

Tactic:
truncate_eq_of_agree _ _ (x.consistent _)

Premises used: PFunctor.MIntl.consistent, PFunctor.Approx.truncate_eq_of_agree
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
⊢ Agree (n := 0) (Approx.sMk x 0) (Approx.sMk x (succ 0))

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
n : ℕ
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))
⊢ Agree (n := n.succ) (Approx.sMk x n.succ) (Approx.sMk x n.succ.succ)

Tactic:
constructor
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
n : ℕ
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:
apply (x.2 i).consistent

Premises used: PFunctor.MIntl.consistent, Sigma.snd
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : (↑F : (α : Type (max uB uA)) → Type (max (max uB uA) uA uB)) F.M
⊢ (M.mk x).dest = x

Tactic:
rfl

Premises used: PFunctor.Obj, PFunctor.M, cast, PFunctor.M.children, PFunctor.M.dest, PFunctor.M.head, PFunctor.Approx.children', rfl, PFunctor.M.Approx.sMk, PFunctor.Approx.head'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
H : ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i
⊢ M.mk x.dest = x

Tactic:
apply ext'

Premises used: PFunctor.M.ext'
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
H : Approx.sMk x.dest n = x.approx n
⊢ (M.mk x.dest).approx n = x.approx n

Tactic:
dsimp only [M.mk]

Premises used: PFunctor.M.mk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
⊢ Eq (α := CofixA F 0) (Approx.sMk x.dest 0) (x.approx 0)

Tactic:
apply @Subsingleton.elim _ CofixA.instSubsingleton

Premises used: Subsingleton.elim
-- Module: Mathlib.Data.PFunctor.Univariate.M
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))

Tactic:
?_
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
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))
⊢ Approx.sMk x.dest n = x.approx n

Tactic:
induction n with
  | zero => apply @Subsingleton.elim _ CofixA.instSubsingleton
  | succ n => ?_

Premises used: Nat.zero, Subsingleton.elim, Nat.succ
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h : Approx.sMk x.dest n = x.approx n
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))
⊢ Eq (α := CofixA F (n + 1)) (Approx.sMk x.dest (n + 1)) (x.approx (n + 1))

Tactic:
dsimp only [Approx.sMk, dest, head]

Premises used: PFunctor.M.dest, PFunctor.M.head, PFunctor.M.Approx.sMk
-- Module: Mathlib.Data.PFunctor.Univariate.M
Goal:
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
h : Approx.sMk x.dest n = x.approx n
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
⊢ 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:
rcases h : x.approx (succ n) with - | ⟨hd, ch⟩

Premises used: PFunctor.MIntl.approx, Nat.succ
-- 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
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
Hconsistent : AllAgree x.approx
⊢ hd = head' (n := 0) (x.approx 1)

Tactic:
rw [← head_succ' n, h, head']

Premises used: PFunctor.Approx.head_succ', PFunctor.Approx.head'
-- 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
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ AllAgree x.approx

Tactic:
apply x.consistent

Premises used: PFunctor.MIntl.consistent
-- 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
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
⊢ 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
-- 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
ch : F.B hd → CofixA F n
h : x.approx n.succ = CofixA.intro hd ch
h' : hd = head' (n := 0) (x.approx 1)
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
⊢ (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
-- Module: Mathlib.Data.PFunctor.Univariate.M
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)
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
⊢ ∀ (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:
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
H : (fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) = 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:
congr
-- 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
H : ∀ (a : F.B (head' (n := 0) (x.approx 1))), (x.children a).approx n = ch a
⊢ (fun (i : F.B (head' (n := 0) (x.approx 1))) ↦ (x.children i).approx n) = ch

Tactic:
ext 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 : children' (x.approx n.succ) (cast ⋯ a) = ch a
⊢ (x.children a).approx n = ch a

Tactic:
dsimp only [children]

Premises used: PFunctor.M.children