-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem ext [Inhabited (M F)] (x y : M F) (H : ∀ ps : Path F, iselect ps x = iselect ps y) :
    x = y

Proof state:
case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Tactic:
cases H'

Result:
case H.succ.hrec.refl
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
ps : Path F
i_ih : x.approx (length ps) = y.approx (length ps)
⊢ iselect ps x = iselect ps y

Proof state:
case H.zero.continue.continue
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = CofixA.continue

Tactic:
constructor

Result:
no goals

Proof state:
case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y

Tactic:
introv H'

Result:
case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Proof state:
case H.zero.continue
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = y.approx 0

Tactic:
cases y.approx 0

Result:
case H.zero.continue.continue
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = CofixA.continue

Proof state:
case H
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), x.approx i = y.approx i

Tactic:
intro i

Result:
case H
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
⊢ x.approx i = y.approx i

Proof state:
case H.succ.hx
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (x.approx (i + 1))

Tactic:
apply x.consistent

Result:
no goals

Proof state:
case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Tactic:
dsimp only [iselect] at H

Result:
case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
i : ℕ
i_ih : x.approx i = y.approx i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y

Proof state:
case H.succ.hy
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (y.approx i) (y.approx (i + 1))

Tactic:
apply y.consistent

Result:
no goals

Proof state:
case H.succ.hx
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

Tactic:
rw [← agree_iff_agree']

Result:
case H.succ.hx
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (x.approx i) (x.approx (i + 1))

Proof state:
case H.succ.hrec.refl
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), (isubtree ps x).head = (isubtree ps y).head
ps : Path F
i_ih : x.approx (length ps) = y.approx (length ps)
⊢ iselect ps x = iselect ps y

Tactic:
apply H ps

Result:
no goals

Proof state:
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x = y

Tactic:
apply ext'

Result:
case H
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), x.approx i = y.approx i

Proof state:
case H.succ.hy
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

Tactic:
rw [← agree_iff_agree', i_ih]

Result:
case H.succ.hy
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree (y.approx i) (y.approx (i + 1))

Proof state:
case H.succ
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ x.approx (i + 1) = y.approx (i + 1)

Tactic:
apply ext_aux x y x

Result:
case H.succ.hx
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

case H.succ.hy
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

case H.succ.hrec
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y

Proof state:
case H
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
⊢ x.approx i = y.approx i

Tactic:
induction' i with i i_ih

Result:
case H.zero
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x.approx 0 = y.approx 0

case H.succ
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ x.approx (i + 1) = y.approx (i + 1)

Proof state:
case H.zero
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x.approx 0 = y.approx 0

Tactic:
cases x.approx 0

Result:
case H.zero.continue
F : PFunctor.{u}
inst✝ : Inhabited F.M
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = y.approx 0