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

Proof state:
case H.succ
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = x.approx (n + 1)

Tactic:
rcases h : x.approx (succ n) with - | ⟨hd, ch⟩

Result:
case H.succ.intro
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
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Proof state:
case H.succ.intro.e_a
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
⊢ (fun i => (x.children i).approx n) = ch

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

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

Tactic:
dsimp only [M.mk]

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

Proof state:
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)

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

Result:
case H.succ
F : PFunctor.{u}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = x.approx (n + 1)

Proof state:
case H.succ.intro
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),
    x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch →
      (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

Tactic:
intros ch h

Result:
case H.succ.intro
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
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

Proof state:
case H.succ.intro
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
h' : hd = head' (x.approx 1)
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Tactic:
revert ch

Result:
case H.succ.intro
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 hd → CofixA F n),
    x.approx n.succ = CofixA.intro hd ch →
      (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Proof state:
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
⊢ hd = head' (x.approx 1)

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

Result:
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

Proof state:
case H.succ.intro
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 hd → CofixA F n),
    x.approx n.succ = CofixA.intro hd ch →
      (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Tactic:
rw [h']

Result:
case H.succ.intro
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),
    x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch →
      (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

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))
⊢ (x.children a).approx n = ch a

Tactic:
dsimp only [children]

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

Proof state:
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

Tactic:
rfl

Result:
no goals

Proof state:
case H.succ.intro
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
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Tactic:
have h' : hd = head' (x.approx 1) := by
  rw [← head_succ' n, h, head']
  apply x.consistent

Result:
case H.succ.intro
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
h' : hd = head' (x.approx 1)
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro hd ch

Proof state:
case H.succ.intro
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
⊢ (CofixA.intro (head' (x.approx 1)) fun i => (x.children i).approx n) = CofixA.intro (head' (x.approx 1)) ch

Tactic:
congr

Result:
case H.succ.intro.e_a
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
⊢ (fun i => (x.children i).approx n) = ch

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

Tactic:
rw [cast_eq_iff_heq] at 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' (x.approx n.succ))
hh : HEq a a''
⊢ children' (x.approx n.succ) a'' = ch a