case H
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), MIntl.approx x i = MIntl.approx y i
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ x = y
apply ext'
case H
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
⊢ MIntl.approx x i = MIntl.approx y i
case H
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ ∀ (i : ℕ), MIntl.approx x i = MIntl.approx y i
intro i
case H.zero
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ MIntl.approx x zero = MIntl.approx y zero

case H.succ
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ MIntl.approx x (succ i) = MIntl.approx y (succ i)
case H
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
⊢ MIntl.approx x i = MIntl.approx y i
induction' i with i i_ih
case H.zero.continue
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = MIntl.approx y zero
case H.zero
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ MIntl.approx x zero = MIntl.approx y zero
cases x.approx 0
case H.zero.continue.continue
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = CofixA.continue
case H.zero.continue
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = MIntl.approx y zero
cases y.approx 0
no goals
case H.zero.continue.continue
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
⊢ CofixA.continue = CofixA.continue
constructor
case H.succ.hx
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree' i x x

case H.succ.hy
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree' i x y

case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
case H.succ
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ MIntl.approx x (succ i) = MIntl.approx y (succ i)
apply ext_aux x y x
case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y
case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
introv H'
case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), head (isubtree ps x) = head (isubtree ps y)
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y
case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y
dsimp only [iselect] at H
case H.succ.hrec.refl
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), head (isubtree ps x) = head (isubtree ps y)
ps : Path F
i_ih : MIntl.approx x (length ps) = MIntl.approx y (length ps)
⊢ iselect ps x = iselect ps y
case H.succ.hrec
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), head (isubtree ps x) = head (isubtree ps y)
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
ps : Path F
H' : i = length ps
⊢ iselect ps x = iselect ps y
cases H'
no goals
case H.succ.hrec.refl
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), head (isubtree ps x) = head (isubtree ps y)
ps : Path F
i_ih : MIntl.approx x (length ps) = MIntl.approx y (length ps)
⊢ iselect ps x = iselect ps y
apply H ps
case H.succ.hx
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree (MIntl.approx x i) (MIntl.approx x (i + 1))
case H.succ.hx
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree' i x x
rw [← agree_iff_agree']
no goals
case H.succ.hx
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree (MIntl.approx x i) (MIntl.approx x (i + 1))
apply x.consistent
case H.succ.hy
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree (MIntl.approx y i) (MIntl.approx y (i + 1))
case H.succ.hy
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree' i x y
rw [← agree_iff_agree', i_ih]
no goals
case H.succ.hy
F : PFunctor
X : Type ?u.33413
f : X → Obj F X
inst✝ : Inhabited (M F)
x y : M F
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : MIntl.approx x i = MIntl.approx y i
⊢ Agree (MIntl.approx y i) (MIntl.approx y (i + 1))
apply y.consistent