-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem mk_dest (x : M F) : M.mk (dest x) = x

Proof state:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (x.approx n.succ))), HEq a a'' → children' (x.approx n.succ) a'' = ch a

Tactic:
rw [h]

Result:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    HEq a a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a

Proof state:
case Hconsistent
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : 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

Result:
no goals

Proof state:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    HEq a a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a

Tactic:
intros _ hh

Result:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a''✝ : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))
hh : HEq a a''✝
⊢ children' (CofixA.intro (head' (x.approx 1)) ch) a''✝ = ch a

Proof state:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a'' : F.B (head' (x.approx n.succ))
hh : HEq a a''
⊢ children' (x.approx n.succ) a'' = ch a

Tactic:
revert a''

Result:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (x.approx n.succ))), HEq a a'' → children' (x.approx n.succ) a'' = ch a

Proof state:
case H
F : PFunctor.{u}
x : F.M
⊢ ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i

Tactic:
intro n

Result:
case H
F : PFunctor.{u}
x : F.M
n : ℕ
⊢ (M.mk x.dest).approx n = x.approx n

Proof state:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a''✝ : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))
hh : HEq a a''✝
⊢ children' (CofixA.intro (head' (x.approx 1)) ch) a''✝ = ch a

Tactic:
cases hh

Result:
case H.succ.intro.e_a.h.refl
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ children' (CofixA.intro (head' (x.approx 1)) ch) a = ch a

Proof state:
case H
F : PFunctor.{u}
x : F.M
n : ℕ
⊢ Approx.sMk x.dest n = x.approx n

Tactic:
induction' n with n

Result:
case H.zero
F : PFunctor.{u}
x : F.M
⊢ Approx.sMk x.dest 0 = x.approx 0

case H.succ
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
⊢ Approx.sMk x.dest (n + 1) = x.approx (n + 1)

Proof state:
F : PFunctor.{u}
x : F.M
⊢ M.mk x.dest = x

Tactic:
apply ext'

Result:
case H
F : PFunctor.{u}
x : F.M
⊢ ∀ (i : ℕ), (M.mk x.dest).approx i = x.approx i

Proof state:
case H.zero
F : PFunctor.{u}
x : F.M
⊢ Approx.sMk x.dest 0 = x.approx 0

Tactic:
apply @Subsingleton.elim _ CofixA.instSubsingleton

Result:
no goals

Proof state:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ children' (x.approx n.succ) (cast ⋯ a) = ch a

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

Result:
case H.succ.intro.e_a.h
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a'' : F.B (head' (x.approx n.succ))
hh : cast ⋯ a = a''
⊢ children' (x.approx n.succ) a'' = ch a