[GOAL]
F : PFunctor
n : ℕ
x : CofixA F (n + 1)
⊢ x = CofixA.intro (head' x) (children' x)
[PROOFSTEP]
cases x
[GOAL]
case intro
F : PFunctor
n : ℕ
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F (Nat.add n 0)
⊢ CofixA.intro a✝¹ a✝ = CofixA.intro (head' (CofixA.intro a✝¹ a✝)) (children' (CofixA.intro a✝¹ a✝))
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
x : CofixA F 0
y : CofixA F 1
⊢ Agree x y
[PROOFSTEP]
constructor
[GOAL]
F : PFunctor
n : ℕ
x : CofixA F (succ n)
y : CofixA F (succ n + 1)
i : B F (head' x)
j : B F (head' y)
h₀ : HEq i j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)
[PROOFSTEP]
cases' h₁ with _ _ _ _ _ _ hagree
[GOAL]
case intro
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
j : B F (head' (CofixA.intro a✝ x'✝))
h₀ : HEq i j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)
[PROOFSTEP]
cases h₀
[GOAL]
case intro.refl
F : PFunctor
n : ℕ
a✝ : F.A
x✝ : B F a✝ → CofixA F n
x'✝ : B F a✝ → CofixA F (n + 1)
hagree : ∀ (i : B F a✝), Agree (x✝ i) (x'✝ i)
i : B F (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)
[PROOFSTEP]
apply hagree
[GOAL]
F : PFunctor
n : ℕ
x : CofixA F n
y : CofixA F (succ n)
h : Agree x y
⊢ truncate y = x
[PROOFSTEP]
induction n
[GOAL]
case zero
F : PFunctor
x : CofixA F zero
y : CofixA F (succ zero)
h : Agree x y
⊢ truncate y = x
[PROOFSTEP]
cases x
[GOAL]
case succ
F : PFunctor
n✝ : ℕ
n_ih✝ : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
x : CofixA F (succ n✝)
y : CofixA F (succ (succ n✝))
h : Agree x y
⊢ truncate y = x
[PROOFSTEP]
cases x
[GOAL]
case zero.continue
F : PFunctor
y : CofixA F (succ zero)
h : Agree CofixA.continue y
⊢ truncate y = CofixA.continue
[PROOFSTEP]
cases y
[GOAL]
case succ.intro
F : PFunctor
n✝ : ℕ
n_ih✝ : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
y : CofixA F (succ (succ n✝))
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F n✝
h : Agree (CofixA.intro a✝¹ a✝) y
⊢ truncate y = CofixA.intro a✝¹ a✝
[PROOFSTEP]
cases y
[GOAL]
case zero.continue.intro
F : PFunctor
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F 0
h : Agree CofixA.continue (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.continue
[PROOFSTEP]
rfl
[GOAL]
case succ.intro.intro
F : PFunctor
n✝ : ℕ
n_ih✝ : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a✝³ : F.A
a✝² : B F a✝³ → CofixA F n✝
a✝¹ : F.A
a✝ : B F a✝¹ → CofixA F (succ n✝)
h : Agree (CofixA.intro a✝³ a✝²) (CofixA.intro a✝¹ a✝)
⊢ truncate (CofixA.intro a✝¹ a✝) = CofixA.intro a✝³ a✝²
[PROOFSTEP]
cases h
[GOAL]
case succ.intro.intro.intro
F : PFunctor
n✝ : ℕ
n_ih✝ : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : B F a✝² → CofixA F n✝
x'✝ : B F a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : B F a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ truncate (CofixA.intro a✝² x'✝) = CofixA.intro a✝² a✝¹
[PROOFSTEP]
simp only [truncate, Function.comp, true_and_iff, eq_self_iff_true, heq_iff_eq]
  -- porting note: used to be `ext y`
[GOAL]
case succ.intro.intro.intro
F : PFunctor
n✝ : ℕ
n_ih✝ : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a✝² : F.A
a✝¹ : B F a✝² → CofixA F n✝
x'✝ : B F a✝² → CofixA F (n✝ + 1)
a✝ : ∀ (i : B F a✝²), Agree (a✝¹ i) (x'✝ i)
⊢ (CofixA.intro a✝² fun x => truncate (x'✝ x)) = CofixA.intro a✝² a✝¹
[PROOFSTEP]
rename_i n_ih a f y h₁
[GOAL]
case succ.intro.intro.intro
F : PFunctor
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a : F.A
f : B F a → CofixA F n✝
y : B F a → CofixA F (n✝ + 1)
h₁ : ∀ (i : B F a), Agree (f i) (y i)
⊢ (CofixA.intro a fun x => truncate (y x)) = CofixA.intro a f
[PROOFSTEP]
suffices (fun x => truncate (y x)) = f by simp [this]; try (exact HEq.rfl; )
[GOAL]
F : PFunctor
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a : F.A
f : B F a → CofixA F n✝
y : B F a → CofixA F (n✝ + 1)
h₁ : ∀ (i : B F a), Agree (f i) (y i)
this : (fun x => truncate (y x)) = f
⊢ (CofixA.intro a fun x => truncate (y x)) = CofixA.intro a f
[PROOFSTEP]
simp [this]
[GOAL]

[PROOFSTEP]
try (exact HEq.rfl; )
[GOAL]

[PROOFSTEP]
exact HEq.rfl
[GOAL]
case succ.intro.intro.intro
F : PFunctor
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a : F.A
f : B F a → CofixA F n✝
y : B F a → CofixA F (n✝ + 1)
h₁ : ∀ (i : B F a), Agree (f i) (y i)
⊢ (fun x => truncate (y x)) = f
[PROOFSTEP]
funext y
[GOAL]
case succ.intro.intro.intro.h
F : PFunctor
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a : F.A
f : B F a → CofixA F n✝
y✝ : B F a → CofixA F (n✝ + 1)
h₁ : ∀ (i : B F a), Agree (f i) (y✝ i)
y : B F a
⊢ truncate (y✝ y) = f y
[PROOFSTEP]
apply n_ih
[GOAL]
case succ.intro.intro.intro.h.h
F : PFunctor
n✝ : ℕ
n_ih : ∀ (x : CofixA F n✝) (y : CofixA F (succ n✝)), Agree x y → truncate y = x
a : F.A
f : B F a → CofixA F n✝
y✝ : B F a → CofixA F (n✝ + 1)
h₁ : ∀ (i : B F a), Agree (f i) (y✝ i)
y : B F a
⊢ Agree (f y) (y✝ y)
[PROOFSTEP]
apply h₁
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
i : X
n : ℕ
⊢ Agree (sCorec f i n) (sCorec f i (succ n))
[PROOFSTEP]
induction' n with n n_ih generalizing i
[GOAL]
case zero
F : PFunctor
X : Type w
f : X → Obj F X
i✝ i : X
⊢ Agree (sCorec f i zero) (sCorec f i (succ zero))
case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
[PROOFSTEP]
constructor
[GOAL]
case succ
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
[PROOFSTEP]
cases' h : f i with y g
[GOAL]
case succ.mk
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ Agree (sCorec f i (succ n)) (sCorec f i (succ (succ n)))
[PROOFSTEP]
constructor
[GOAL]
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i : X
y : F.A
g : B F y → X
h : f i = { fst := y, snd := g }
⊢ ∀ (i_1 : B F (f i).fst), Agree (sCorec f (Sigma.snd (f i) i_1) n) (sCorec f (Sigma.snd (f i) i_1) (succ n))
[PROOFSTEP]
introv
[GOAL]
case succ.mk.a
F : PFunctor
X : Type w
f : X → Obj F X
i✝¹ : X
n : ℕ
n_ih : ∀ (i : X), Agree (sCorec f i n) (sCorec f i (succ n))
i✝ : X
y : F.A
g : B F y → X
h : f i✝ = { fst := y, snd := g }
i : B F (f i✝).fst
⊢ Agree (sCorec f (Sigma.snd (f i✝) i) n) (sCorec f (Sigma.snd (f i✝) i) (succ n))
[PROOFSTEP]
apply n_ih
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
⊢ ∀ (a b : CofixA F 0), a = b
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩
[GOAL]
case continue.continue
F : PFunctor
X : Type w
f : X → Obj F X
⊢ continue = continue
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ head' (x (succ n)) = head' (x (succ m))
[PROOFSTEP]
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
this : ∀ (n : ℕ), head' (x (succ n)) = head' (x 1)
⊢ head' (x (succ n)) = head' (x (succ m))
[PROOFSTEP]
simp [this]
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
n m : ℕ
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ ∀ (n : ℕ), head' (x (succ n)) = head' (x 1)
[PROOFSTEP]
clear m n
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
⊢ ∀ (n : ℕ), head' (x (succ n)) = head' (x 1)
[PROOFSTEP]
intro n
[GOAL]
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
⊢ head' (x (succ n)) = head' (x 1)
[PROOFSTEP]
cases' h₀ : x (succ n) with _ i₀ f₀
[GOAL]
case intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀ : B F i₀ → CofixA F n
h₀ : x (succ n) = CofixA.intro i₀ f₀
⊢ head' (CofixA.intro i₀ f₀) = head' (x 1)
[PROOFSTEP]
cases' h₁ : x 1 with _ i₁ f₁
[GOAL]
case intro.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀ : B F i₀ → CofixA F n
h₀ : x (succ n) = CofixA.intro i₀ f₀
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
⊢ head' (CofixA.intro i₀ f₀) = head' (CofixA.intro i₁ f₁)
[PROOFSTEP]
dsimp only [head']
[GOAL]
case intro.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀ : B F i₀ → CofixA F n
h₀ : x (succ n) = CofixA.intro i₀ f₀
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
⊢ i₀ = i₁
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case intro.intro.zero
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n
h₀✝ : x (succ n) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
f₀ : B F i₀ → CofixA F zero
h₀ : x (succ zero) = CofixA.intro i₀ f₀
⊢ i₀ = i₁
[PROOFSTEP]
rw [h₁] at h₀
[GOAL]
case intro.intro.zero
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n
h₀✝ : x (succ n) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
f₀ : B F i₀ → CofixA F zero
h₀ : CofixA.intro i₁ f₁ = CofixA.intro i₀ f₀
⊢ i₀ = i₁
[PROOFSTEP]
cases h₀
[GOAL]
case intro.intro.zero.refl
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n
h₀ : x (succ n) = CofixA.intro i₀ f₀✝
f₀ : B F i₀ → CofixA F zero
h₁ : x 1 = CofixA.intro i₀ f₀
⊢ i₀ = i₀
[PROOFSTEP]
trivial
[GOAL]
case intro.intro.succ
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
⊢ i₀ = i₁
[PROOFSTEP]
have H := Hconsistent (succ n)
[GOAL]
case intro.intro.succ
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
H : Agree (x (succ n)) (x (succ (succ n)))
⊢ i₀ = i₁
[PROOFSTEP]
cases' h₂ : x (succ n) with _ i₂ f₂
[GOAL]
case intro.intro.succ.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
H : Agree (x (succ n)) (x (succ (succ n)))
i₂ : F.A
f₂ : B F i₂ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₂ f₂
⊢ i₀ = i₁
[PROOFSTEP]
rw [h₀, h₂] at H
[GOAL]
case intro.intro.succ.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
i₂ : F.A
f₂ : B F i₂ → CofixA F n
H : Agree (CofixA.intro i₂ f₂) (CofixA.intro i₀ f₀)
h₂ : x (succ n) = CofixA.intro i₂ f₂
⊢ i₀ = i₁
[PROOFSTEP]
apply n_ih (truncate ∘ f₀)
[GOAL]
case intro.intro.succ.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
i₂ : F.A
f₂ : B F i₂ → CofixA F n
H : Agree (CofixA.intro i₂ f₂) (CofixA.intro i₀ f₀)
h₂ : x (succ n) = CofixA.intro i₂ f₂
⊢ x (succ n) = CofixA.intro i₀ (truncate ∘ f₀)
[PROOFSTEP]
rw [h₂]
[GOAL]
case intro.intro.succ.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
i₂ : F.A
f₂ : B F i₂ → CofixA F n
H : Agree (CofixA.intro i₂ f₂) (CofixA.intro i₀ f₀)
h₂ : x (succ n) = CofixA.intro i₂ f₂
⊢ CofixA.intro i₂ f₂ = CofixA.intro i₀ (truncate ∘ f₀)
[PROOFSTEP]
cases' H with _ _ _ _ _ _ hagree
[GOAL]
case intro.intro.succ.intro.intro
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
f₂ : B F i₀ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₀ f₂
hagree : ∀ (i : B F i₀), Agree (f₂ i) (f₀ i)
⊢ CofixA.intro i₀ f₂ = CofixA.intro i₀ (truncate ∘ f₀)
[PROOFSTEP]
congr
[GOAL]
case intro.intro.succ.intro.intro.e_a
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
f₂ : B F i₀ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₀ f₂
hagree : ∀ (i : B F i₀), Agree (f₂ i) (f₀ i)
⊢ f₂ = truncate ∘ f₀
[PROOFSTEP]
funext j
[GOAL]
case intro.intro.succ.intro.intro.e_a.h
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
f₂ : B F i₀ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₀ f₂
hagree : ∀ (i : B F i₀), Agree (f₂ i) (f₀ i)
j : B F i₀
⊢ f₂ j = (truncate ∘ f₀) j
[PROOFSTEP]
dsimp only [comp_apply]
[GOAL]
case intro.intro.succ.intro.intro.e_a.h
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
f₂ : B F i₀ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₀ f₂
hagree : ∀ (i : B F i₀), Agree (f₂ i) (f₀ i)
j : B F i₀
⊢ f₂ j = truncate (f₀ j)
[PROOFSTEP]
rw [truncate_eq_of_agree]
[GOAL]
case intro.intro.succ.intro.intro.e_a.h.h
F : PFunctor
X : Type w
f : X → Obj F X
x : (n : ℕ) → CofixA F n
Hconsistent : AllAgree x
n✝ : ℕ
i₀ : F.A
f₀✝ : B F i₀ → CofixA F n✝
h₀✝ : x (succ n✝) = CofixA.intro i₀ f₀✝
i₁ : F.A
f₁ : B F i₁ → CofixA F 0
h₁ : x 1 = CofixA.intro i₁ f₁
n : ℕ
n_ih : ∀ (f₀ : B F i₀ → CofixA F n), x (succ n) = CofixA.intro i₀ f₀ → i₀ = i₁
f₀ : B F i₀ → CofixA F (succ n)
h₀ : x (succ (succ n)) = CofixA.intro i₀ f₀
f₂ : B F i₀ → CofixA F n
h₂ : x (succ n) = CofixA.intro i₀ f₂
hagree : ∀ (i : B F i₀), Agree (f₂ i) (f₀ i)
j : B F i₀
⊢ Agree (f₂ j) (f₀ j)
[PROOFSTEP]
apply hagree
[GOAL]
F : PFunctor
inst✝ : Inhabited F.A
⊢ Inhabited (M F)
[PROOFSTEP]
infer_instance
[GOAL]
F : PFunctor
x y : M F
H : ∀ (i : ℕ), MIntl.approx x i = MIntl.approx y i
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk
F : PFunctor
y : M F
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H : ∀ (i : ℕ), MIntl.approx { approx := approx✝, consistent := consistent✝ } i = MIntl.approx y i
⊢ { approx := approx✝, consistent := consistent✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
⊢ { approx := approx✝¹, consistent := consistent✝¹ } = { approx := approx✝, consistent := consistent✝ }
[PROOFSTEP]
congr with n
[GOAL]
case mk.mk.e_approx.h
F : PFunctor
approx✝¹ : (n : ℕ) → CofixA F n
consistent✝¹ : AllAgree approx✝¹
approx✝ : (n : ℕ) → CofixA F n
consistent✝ : AllAgree approx✝
H :
  ∀ (i : ℕ),
    MIntl.approx { approx := approx✝¹, consistent := consistent✝¹ } i =
      MIntl.approx { approx := approx✝, consistent := consistent✝ } i
n : ℕ
⊢ approx✝¹ n = approx✝ n
[PROOFSTEP]
apply H
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
⊢ head x = head' (MIntl.approx x (succ n))
[PROOFSTEP]
simp only [head, H]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
⊢ AllAgree fun n =>
    children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i)
[PROOFSTEP]
intro n
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
⊢ Agree
    ((fun n => children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i))
      n)
    ((fun n => children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i))
      (succ n))
[PROOFSTEP]
have P' := x.2 (succ n)
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ Agree
    ((fun n => children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i))
      n)
    ((fun n => children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i))
      (succ n))
[PROOFSTEP]
apply agree_children _ _ _ P'
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ HEq (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i)
    (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ (succ n))))) i)
[PROOFSTEP]
trans i
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ HEq (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) i) i
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ HEq i (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ (succ n))))) i)
[PROOFSTEP]
apply cast_heq
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ HEq i (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ (succ n))))) i)
[PROOFSTEP]
symm
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
i : B F (head x)
H : ∀ (n : ℕ), head' (MIntl.approx x (succ n)) = head' (MIntl.approx x (succ 0)) :=
  fun n => head_succ' n 0 x.approx x.consistent
n : ℕ
P' : Agree (MIntl.approx x (succ n)) (MIntl.approx x (succ (succ n)))
⊢ HEq (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ (succ n))))) i) i
[PROOFSTEP]
apply cast_heq
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
i : IdxCat F
x : M F
H' : i.fst = head x
⊢ i.fst = head x
[PROOFSTEP]
simp only [head, H']
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
⊢ Agree (Approx.sMk x 0) (Approx.sMk x (succ 0))
[PROOFSTEP]
constructor
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
n : ℕ
⊢ Agree (Approx.sMk x (succ n)) (Approx.sMk x (succ (succ n)))
[PROOFSTEP]
constructor
[GOAL]
case a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
n : ℕ
⊢ ∀ (i : B F x.fst), Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
[PROOFSTEP]
introv
[GOAL]
case a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
n : ℕ
i : B F x.fst
⊢ Agree (MIntl.approx (Sigma.snd x i) n) (MIntl.approx (Sigma.snd x i) (succ n))
[PROOFSTEP]
apply (x.2 i).consistent
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
⊢ dest (M.mk x) = x
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
⊢ M.mk (dest x) = x
[PROOFSTEP]
apply ext'
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
⊢ ∀ (i : ℕ), MIntl.approx (M.mk (dest x)) i = MIntl.approx x i
[PROOFSTEP]
intro n
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
⊢ MIntl.approx (M.mk (dest x)) n = MIntl.approx x n
[PROOFSTEP]
dsimp only [M.mk]
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
⊢ Approx.sMk (dest x) n = MIntl.approx x n
[PROOFSTEP]
induction' n with n
[GOAL]
case H.zero
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
⊢ Approx.sMk (dest x) zero = MIntl.approx x zero
[PROOFSTEP]
apply @Subsingleton.elim _ CofixA.instSubsingleton
[GOAL]
case H.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
⊢ Approx.sMk (dest x) (succ n) = MIntl.approx x (succ n)
[PROOFSTEP]
dsimp only [Approx.sMk, dest, head]
[GOAL]
case H.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
⊢ (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) = MIntl.approx x (succ n)
[PROOFSTEP]
cases' h : x.approx (succ n) with _ hd ch
[GOAL]
case H.succ.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
ch : B F hd → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro hd ch
⊢ (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) = CofixA.intro hd ch
[PROOFSTEP]
have h' : hd = head' (x.approx 1) := by
  rw [← head_succ' n, h, head']
  apply x.consistent
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
ch : B F hd → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro hd ch
⊢ hd = head' (MIntl.approx x 1)
[PROOFSTEP]
rw [← head_succ' n, h, head']
[GOAL]
case Hconsistent
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
ch : B F hd → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro hd ch
⊢ AllAgree x.approx
[PROOFSTEP]
apply x.consistent
[GOAL]
case H.succ.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
ch : B F hd → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro hd ch
h' : hd = head' (MIntl.approx x 1)
⊢ (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) = CofixA.intro hd ch
[PROOFSTEP]
revert ch
[GOAL]
case H.succ.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
⊢ ∀ (ch : B F hd → CofixA F n),
    MIntl.approx x (succ n) = CofixA.intro hd ch →
      (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) = CofixA.intro hd ch
[PROOFSTEP]
rw [h']
[GOAL]
case H.succ.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
⊢ ∀ (ch : B F (head' (MIntl.approx x 1)) → CofixA F n),
    MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch →
      (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) =
        CofixA.intro (head' (MIntl.approx x 1)) ch
[PROOFSTEP]
intros ch h
[GOAL]
case H.succ.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
⊢ (CofixA.intro (head' (MIntl.approx x 1)) fun i => MIntl.approx (children x i) n) =
    CofixA.intro (head' (MIntl.approx x 1)) ch
[PROOFSTEP]
congr
[GOAL]
case H.succ.intro.e_a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
⊢ (fun i => MIntl.approx (children x i) n) = ch
[PROOFSTEP]
ext a
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
⊢ MIntl.approx (children x a) n = ch a
[PROOFSTEP]
dsimp only [children]
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
⊢ children' (MIntl.approx x (succ n)) (cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) a) = ch a
[PROOFSTEP]
generalize hh : cast _ a = a''
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
a'' : B F (head' (MIntl.approx x (succ n)))
hh : cast (_ : B F (head x) = B F (head' (MIntl.approx x (succ n)))) a = a''
⊢ children' (MIntl.approx x (succ n)) a'' = ch a
[PROOFSTEP]
rw [cast_eq_iff_heq] at hh
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
a'' : B F (head' (MIntl.approx x (succ n)))
hh : HEq a a''
⊢ children' (MIntl.approx x (succ n)) a'' = ch a
[PROOFSTEP]
revert a''
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
⊢ ∀ (a'' : B F (head' (MIntl.approx x (succ n)))), HEq a a'' → children' (MIntl.approx x (succ n)) a'' = ch a
[PROOFSTEP]
rw [h]
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
⊢ ∀ (a'' : B F (head' (CofixA.intro (head' (MIntl.approx x 1)) ch))),
    HEq a a'' → children' (CofixA.intro (head' (MIntl.approx x 1)) ch) a'' = ch a
[PROOFSTEP]
intros _ hh
[GOAL]
case H.succ.intro.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
a''✝ : B F (head' (CofixA.intro (head' (MIntl.approx x 1)) ch))
hh : HEq a a''✝
⊢ children' (CofixA.intro (head' (MIntl.approx x 1)) ch) a''✝ = ch a
[PROOFSTEP]
cases hh
[GOAL]
case H.succ.intro.e_a.h.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n : ℕ
n_ih✝ : Approx.sMk (dest x) n = MIntl.approx x n
hd : F.A
h' : hd = head' (MIntl.approx x 1)
ch : B F (head' (MIntl.approx x 1)) → CofixA F n
h : MIntl.approx x (succ n) = CofixA.intro (head' (MIntl.approx x 1)) ch
a : B F (head' (MIntl.approx x 1))
⊢ children' (CofixA.intro (head' (MIntl.approx x 1)) ch) a = ch a
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x y : Obj F (M F)
h : M.mk x = M.mk y
⊢ x = y
[PROOFSTEP]
rw [← dest_mk x, h, dest_mk]
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort w
f : (x : Obj F (M F)) → r (M.mk x)
x : M F
this : r (M.mk (dest x))
⊢ r x
[PROOFSTEP]
rw [← mk_dest x]
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort w
f : (x : Obj F (M F)) → r (M.mk x)
x : M F
this : r (M.mk (dest x))
⊢ r (M.mk (dest x))
[PROOFSTEP]
exact this
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x : M F
⊢ Agree' n x x
[PROOFSTEP]
induction' n with _ n_ih generalizing x
[GOAL]
case zero
F : PFunctor
X : Type u_1
f : X → Obj F X
x✝ x : M F
⊢ Agree' zero x x
[PROOFSTEP]
induction x using PFunctor.M.casesOn'
[GOAL]
case succ
F : PFunctor
X : Type u_1
f : X → Obj F X
x✝ : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
x : M F
⊢ Agree' (succ n✝) x x
[PROOFSTEP]
induction x using PFunctor.M.casesOn'
[GOAL]
case zero.f
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
a✝ : F.A
f✝ : B F a✝ → M F
⊢ Agree' zero (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f✝ })
[PROOFSTEP]
constructor
[GOAL]
case succ.f
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ Agree' (succ n✝) (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f✝ })
[PROOFSTEP]
constructor
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := ?succ.f.a, snd := ?succ.f.x }
[PROOFSTEP]
try rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := ?succ.f.a, snd := ?succ.f.x }
[PROOFSTEP]
rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a✝, snd := ?succ.f.y }
[PROOFSTEP]
try rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a✝, snd := ?succ.f.y }
[PROOFSTEP]
rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
[PROOFSTEP]
try rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
[PROOFSTEP]
rfl
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝ i) (f✝ i)
[PROOFSTEP]
intros
[GOAL]
case succ.f.a
F : PFunctor
X : Type u_1
f : X → Obj F X
x : M F
n✝ : ℕ
n_ih : ∀ (x : M F), Agree' n✝ x x
a✝ : F.A
f✝ : B F a✝ → M F
i✝ : B F a✝
⊢ Agree' n✝ (f✝ i✝) (f✝ i✝)
[PROOFSTEP]
apply n_ih
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
⊢ Agree (MIntl.approx x n) (MIntl.approx y (n + 1)) ↔ Agree' n x y
[PROOFSTEP]
constructor
[GOAL]
case mp
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
⊢ Agree (MIntl.approx x n) (MIntl.approx y (n + 1)) → Agree' n x y
[PROOFSTEP]
intro h
[GOAL]
case mpr
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
⊢ Agree' n x y → Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
[PROOFSTEP]
intro h
[GOAL]
case mp
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
⊢ Agree' n x y
[PROOFSTEP]
induction' n with _ n_ih generalizing x y
[GOAL]
case mp.zero
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree (MIntl.approx x✝ n) (MIntl.approx y✝ (n + 1))
x y : M F
h : Agree (MIntl.approx x zero) (MIntl.approx y (zero + 1))
⊢ Agree' zero x y
case mp.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree (MIntl.approx x✝ n) (MIntl.approx y✝ (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
x y : M F
h : Agree (MIntl.approx x (succ n✝)) (MIntl.approx y (succ n✝ + 1))
⊢ Agree' (succ n✝) x y
[PROOFSTEP]
constructor
[GOAL]
case mp.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree (MIntl.approx x✝ n) (MIntl.approx y✝ (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
x y : M F
h : Agree (MIntl.approx x (succ n✝)) (MIntl.approx y (succ n✝ + 1))
⊢ Agree' (succ n✝) x y
[PROOFSTEP]
induction x using PFunctor.M.casesOn'
[GOAL]
case mp.succ.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y✝ : M F
h✝ : Agree (MIntl.approx x n) (MIntl.approx y✝ (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
y : M F
a✝ : F.A
f✝ : B F a✝ → M F
h : Agree (MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (succ n✝)) (MIntl.approx y (succ n✝ + 1))
⊢ Agree' (succ n✝) (M.mk { fst := a✝, snd := f✝ }) y
[PROOFSTEP]
induction y using PFunctor.M.casesOn'
[GOAL]
case mp.succ.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h✝ : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
a✝ : F.A
f✝ : B F a✝ → M F
h :
  Agree (MIntl.approx (M.mk { fst := a✝¹, snd := f✝¹ }) (succ n✝))
    (MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (succ n✝ + 1))
⊢ Agree' (succ n✝) (M.mk { fst := a✝¹, snd := f✝¹ }) (M.mk { fst := a✝, snd := f✝ })
[PROOFSTEP]
simp only [approx_mk] at h
[GOAL]
case mp.succ.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h✝ : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
a✝ : F.A
f✝ : B F a✝ → M F
h : Agree (CofixA.intro a✝¹ fun j => MIntl.approx (f✝¹ j) n✝) (CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n✝ + 1))
⊢ Agree' (succ n✝) (M.mk { fst := a✝¹, snd := f✝¹ }) (M.mk { fst := a✝, snd := f✝ })
[PROOFSTEP]
cases' h with _ _ _ _ _ _ hagree
[GOAL]
case mp.succ.f.f.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ Agree' (succ n✝) (M.mk { fst := a✝, snd := f✝¹ }) (M.mk { fst := a✝, snd := f✝ })
[PROOFSTEP]
constructor
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ M.mk { fst := a✝, snd := f✝¹ } = M.mk { fst := ?mp.succ.f.f.intro.a, snd := ?mp.succ.f.f.intro.x }
[PROOFSTEP]
try rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ M.mk { fst := a✝, snd := f✝¹ } = M.mk { fst := ?mp.succ.f.f.intro.a, snd := ?mp.succ.f.f.intro.x }
[PROOFSTEP]
rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a✝, snd := ?mp.succ.f.f.intro.y }
[PROOFSTEP]
try rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a✝, snd := ?mp.succ.f.f.intro.y }
[PROOFSTEP]
rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝¹ i) (f✝ i)
[PROOFSTEP]
try rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝¹ i) (f✝ i)
[PROOFSTEP]
rfl
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
⊢ ∀ (i : B F a✝), Agree' n✝ (f✝¹ i) (f✝ i)
[PROOFSTEP]
intro i
[GOAL]
case mp.succ.f.f.intro.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
i : B F a✝
⊢ Agree' n✝ (f✝¹ i) (f✝ i)
[PROOFSTEP]
apply n_ih
[GOAL]
case mp.succ.f.f.intro.a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1)) → Agree' n✝ x y
a✝ : F.A
f✝¹ f✝ : B F a✝ → M F
hagree : ∀ (i : B F a✝), Agree ((fun j => MIntl.approx (f✝¹ j) n✝) i) ((fun j => MIntl.approx (f✝ j) (n✝ + 1)) i)
i : B F a✝
⊢ Agree (MIntl.approx (f✝¹ i) n✝) (MIntl.approx (f✝ i) (n✝ + 1))
[PROOFSTEP]
apply hagree
[GOAL]
case mpr
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x y : M F
h : Agree' n x y
⊢ Agree (MIntl.approx x n) (MIntl.approx y (n + 1))
[PROOFSTEP]
induction' n with _ n_ih generalizing x y
[GOAL]
case mpr.zero
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree' n x✝ y✝
x y : M F
h : Agree' zero x y
⊢ Agree (MIntl.approx x zero) (MIntl.approx y (zero + 1))
case mpr.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
h : Agree' (succ n✝) x y
⊢ Agree (MIntl.approx x (succ n✝)) (MIntl.approx y (succ n✝ + 1))
[PROOFSTEP]
constructor
[GOAL]
case mpr.succ
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h✝ : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
h : Agree' (succ n✝) x y
⊢ Agree (MIntl.approx x (succ n✝)) (MIntl.approx y (succ n✝ + 1))
[PROOFSTEP]
cases' h with _ _ _ a x' y'
[GOAL]
case mpr.succ.step
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝² : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝¹ : x = M.mk { fst := a, snd := x' }
a✝ : y = M.mk { fst := a, snd := y' }
⊢ Agree (MIntl.approx x (succ n✝)) (MIntl.approx y (succ n✝ + 1))
[PROOFSTEP]
induction' x using PFunctor.M.casesOn' with x_a x_f
[GOAL]
case mpr.succ.step.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝³ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝² : x = M.mk { fst := a, snd := x' }
a✝¹ : y = M.mk { fst := a, snd := y' }
x_a : F.A
x_f : B F x_a → M F
a✝ : M.mk { fst := x_a, snd := x_f } = M.mk { fst := a, snd := x' }
⊢ Agree (MIntl.approx (M.mk { fst := x_a, snd := x_f }) (succ n✝)) (MIntl.approx y (succ n✝ + 1))
[PROOFSTEP]
induction' y using PFunctor.M.casesOn' with y_a y_f
[GOAL]
case mpr.succ.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
x_a : F.A
x_f : B F x_a → M F
a✝¹ : M.mk { fst := x_a, snd := x_f } = M.mk { fst := a, snd := x' }
y_a : F.A
y_f : B F y_a → M F
a✝ : M.mk { fst := y_a, snd := y_f } = M.mk { fst := a, snd := y' }
⊢ Agree (MIntl.approx (M.mk { fst := x_a, snd := x_f }) (succ n✝))
    (MIntl.approx (M.mk { fst := y_a, snd := y_f }) (succ n✝ + 1))
[PROOFSTEP]
simp only [approx_mk]
[GOAL]
case mpr.succ.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
x_a : F.A
x_f : B F x_a → M F
a✝¹ : M.mk { fst := x_a, snd := x_f } = M.mk { fst := a, snd := x' }
y_a : F.A
y_f : B F y_a → M F
a✝ : M.mk { fst := y_a, snd := y_f } = M.mk { fst := a, snd := y' }
⊢ Agree (CofixA.intro x_a fun j => MIntl.approx (x_f j) n✝) (CofixA.intro y_a fun j => MIntl.approx (y_f j) (n✝ + 1))
[PROOFSTEP]
have h_a_1 := mk_inj ‹M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩›
[GOAL]
case mpr.succ.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
x_a : F.A
x_f : B F x_a → M F
a✝¹ : M.mk { fst := x_a, snd := x_f } = M.mk { fst := a, snd := x' }
y_a : F.A
y_f : B F y_a → M F
a✝ : M.mk { fst := y_a, snd := y_f } = M.mk { fst := a, snd := y' }
h_a_1 : { fst := x_a, snd := x_f } = { fst := a, snd := x' }
⊢ Agree (CofixA.intro x_a fun j => MIntl.approx (x_f j) n✝) (CofixA.intro y_a fun j => MIntl.approx (y_f j) (n✝ + 1))
[PROOFSTEP]
cases h_a_1
[GOAL]
case mpr.succ.step.f.f.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
y_a : F.A
y_f : B F y_a → M F
a✝¹ : M.mk { fst := y_a, snd := y_f } = M.mk { fst := a, snd := y' }
a✝ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
⊢ Agree (CofixA.intro a fun j => MIntl.approx (x' j) n✝) (CofixA.intro y_a fun j => MIntl.approx (y_f j) (n✝ + 1))
[PROOFSTEP]
replace h_a_2 := mk_inj ‹M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩›
[GOAL]
case mpr.succ.step.f.f.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
y_a : F.A
y_f : B F y_a → M F
a✝¹ : M.mk { fst := y_a, snd := y_f } = M.mk { fst := a, snd := y' }
a✝ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
h_a_2 : { fst := y_a, snd := y_f } = { fst := a, snd := y' }
⊢ Agree (CofixA.intro a fun j => MIntl.approx (x' j) n✝) (CofixA.intro y_a fun j => MIntl.approx (y_f j) (n✝ + 1))
[PROOFSTEP]
cases h_a_2
[GOAL]
case mpr.succ.step.f.f.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
a✝¹ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
a✝ : M.mk { fst := a, snd := y' } = M.mk { fst := a, snd := y' }
⊢ Agree (CofixA.intro a fun j => MIntl.approx (x' j) n✝) (CofixA.intro a fun j => MIntl.approx (y' j) (n✝ + 1))
[PROOFSTEP]
constructor
[GOAL]
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
a✝¹ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
a✝ : M.mk { fst := a, snd := y' } = M.mk { fst := a, snd := y' }
⊢ ∀ (i : B F a), Agree (MIntl.approx (x' i) n✝) (MIntl.approx (y' i) (n✝ + 1))
[PROOFSTEP]
intro i
[GOAL]
case mpr.succ.step.f.f.refl.refl.a
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
a✝¹ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
a✝ : M.mk { fst := a, snd := y' } = M.mk { fst := a, snd := y' }
i : B F a
⊢ Agree (MIntl.approx (x' i) n✝) (MIntl.approx (y' i) (n✝ + 1))
[PROOFSTEP]
apply n_ih
[GOAL]
case mpr.succ.step.f.f.refl.refl.a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
n : ℕ
x✝ y✝ : M F
h : Agree' n x✝ y✝
n✝ : ℕ
n_ih : ∀ (x y : M F), Agree' n✝ x y → Agree (MIntl.approx x n✝) (MIntl.approx y (n✝ + 1))
x y : M F
a : F.A
x' y' : B F a → M F
a✝⁴ : ∀ (i : B F a), Agree' n✝ (x' i) (y' i)
a✝³ : x = M.mk { fst := a, snd := x' }
a✝² : y = M.mk { fst := a, snd := y' }
a✝¹ : M.mk { fst := a, snd := x' } = M.mk { fst := a, snd := x' }
a✝ : M.mk { fst := a, snd := y' } = M.mk { fst := a, snd := y' }
i : B F a
⊢ Agree' n✝ (x' i) (y' i)
[PROOFSTEP]
simp [*]
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
x : Obj F (M F)
f : (x : Obj F (M F)) → r (M.mk x)
⊢ M.cases f (M.mk x) = f x
[PROOFSTEP]
dsimp only [M.mk, PFunctor.M.cases, dest, head, Approx.sMk, head']
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
x : Obj F (M F)
f : (x : Obj F (M F)) → r (M.mk x)
⊢ Eq.mpr
      (_ :
        r
            {
              approx := fun x_1 =>
                match x_1 with
                | 0 => CofixA.continue
                | succ n => CofixA.intro x.fst fun i => MIntl.approx (Sigma.snd x i) n,
              consistent := (_ : AllAgree (Approx.sMk x)) } =
          r
            {
              approx := fun x_1 =>
                match x_1 with
                | 0 => CofixA.continue
                | succ n =>
                  CofixA.intro x.fst fun i =>
                    MIntl.approx
                      (children
                        {
                          approx := fun x_2 =>
                            match x_2 with
                            | 0 => CofixA.continue
                            | succ n => CofixA.intro x.fst fun i => MIntl.approx (Sigma.snd x i) n,
                          consistent := (_ : AllAgree (Approx.sMk x)) }
                        i)
                      n,
              consistent :=
                (_ :
                  AllAgree
                    (Approx.sMk
                      { fst := x.fst,
                        snd := fun i =>
                          children
                            {
                              approx := fun x_1 =>
                                match x_1 with
                                | 0 => CofixA.continue
                                | succ n => CofixA.intro x.fst fun i => MIntl.approx (Sigma.snd x i) n,
                              consistent := (_ : AllAgree (Approx.sMk x)) }
                            i })) })
      (f
        { fst := x.fst,
          snd := fun i =>
            children
              {
                approx := fun x_1 =>
                  match x_1 with
                  | 0 => CofixA.continue
                  | succ n => CofixA.intro x.fst fun i => MIntl.approx (Sigma.snd x i) n,
                consistent := (_ : AllAgree (Approx.sMk x)) }
              i }) =
    f x
[PROOFSTEP]
cases x
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
f : (x : Obj F (M F)) → r (M.mk x)
fst✝ : F.A
snd✝ : B F fst✝ → M F
⊢ Eq.mpr
      (_ :
        r
            {
              approx := fun x =>
                match x with
                | 0 => CofixA.continue
                | succ n =>
                  CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i =>
                    MIntl.approx (Sigma.snd { fst := fst✝, snd := snd✝ } i) n,
              consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) } =
          r
            {
              approx := fun x =>
                match x with
                | 0 => CofixA.continue
                | succ n =>
                  CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i =>
                    MIntl.approx
                      (children
                        {
                          approx := fun x =>
                            match x with
                            | 0 => CofixA.continue
                            | succ n =>
                              CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i =>
                                MIntl.approx (Sigma.snd { fst := fst✝, snd := snd✝ } i) n,
                          consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
                        i)
                      n,
              consistent :=
                (_ :
                  AllAgree
                    (Approx.sMk
                      { fst := { fst := fst✝, snd := snd✝ }.fst,
                        snd := fun i =>
                          children
                            {
                              approx := fun x =>
                                match x with
                                | 0 => CofixA.continue
                                | succ n =>
                                  CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i =>
                                    MIntl.approx (Sigma.snd { fst := fst✝, snd := snd✝ } i) n,
                              consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
                            i })) })
      (f
        { fst := { fst := fst✝, snd := snd✝ }.fst,
          snd := fun i =>
            children
              {
                approx := fun x =>
                  match x with
                  | 0 => CofixA.continue
                  | succ n =>
                    CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i =>
                      MIntl.approx (Sigma.snd { fst := fst✝, snd := snd✝ } i) n,
                consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
              i }) =
    f { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
dsimp only [Approx.sMk]
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
f : (x : Obj F (M F)) → r (M.mk x)
fst✝ : F.A
snd✝ : B F fst✝ → M F
⊢ Eq.mpr
      (_ :
        r
            {
              approx := fun x =>
                match x with
                | 0 => CofixA.continue
                | succ n => CofixA.intro fst✝ fun i => MIntl.approx (snd✝ i) n,
              consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) } =
          r
            {
              approx := fun x =>
                match x with
                | 0 => CofixA.continue
                | succ n =>
                  CofixA.intro fst✝ fun i =>
                    MIntl.approx
                      (children
                        {
                          approx := fun x =>
                            match x with
                            | 0 => CofixA.continue
                            | succ n => CofixA.intro fst✝ fun i => MIntl.approx (snd✝ i) n,
                          consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
                        i)
                      n,
              consistent :=
                (_ :
                  AllAgree
                    (Approx.sMk
                      { fst := fst✝,
                        snd := fun i =>
                          children
                            {
                              approx := fun x =>
                                match x with
                                | 0 => CofixA.continue
                                | succ n => CofixA.intro fst✝ fun i => MIntl.approx (snd✝ i) n,
                              consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
                            i })) })
      (f
        { fst := fst✝,
          snd := fun i =>
            children
              {
                approx := fun x =>
                  match x with
                  | 0 => CofixA.continue
                  | succ n => CofixA.intro fst✝ fun i => MIntl.approx (snd✝ i) n,
                consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
              i }) =
    f { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp only [Eq.mpr]
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
f : (x : Obj F (M F)) → r (M.mk x)
fst✝ : F.A
snd✝ : B F fst✝ → M F
⊢ f
      { fst := fst✝,
        snd := fun i =>
          children
            {
              approx := fun x =>
                match x with
                | 0 => CofixA.continue
                | succ n => CofixA.intro fst✝ fun i => MIntl.approx (snd✝ i) n,
              consistent := (_ : AllAgree (Approx.sMk { fst := fst✝, snd := snd✝ })) }
            i } =
    f { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
apply congrFun
[GOAL]
case mk.h
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
r : M F → Sort u_2
f : (x : Obj F (M F)) → r (M.mk x)
fst✝ : F.A
snd✝ : B F fst✝ → M F
⊢ f = f
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a a' : F.A
f : B F a → M F
i : B F a'
⊢ IsPath ({ fst := a', snd := i } :: xs) (M.mk { fst := a, snd := f }) → a = a'
[PROOFSTEP]
generalize h : M.mk ⟨a, f⟩ = x
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a a' : F.A
f : B F a → M F
i : B F a'
x : M F
h : M.mk { fst := a, snd := f } = x
⊢ IsPath ({ fst := a', snd := i } :: xs) x → a = a'
[PROOFSTEP]
rintro (_ | ⟨_, _, _, _, rfl, _⟩)
[GOAL]
case cons
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
xs : Path F
a a' : F.A
f : B F a → M F
i : B F a'
f✝ : B F a' → M F
a✝ : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a', snd := f✝ }
⊢ a = a'
[PROOFSTEP]
cases mk_inj h
[GOAL]
case cons.refl
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
a✝ : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ IsPath ({ fst := a, snd := i } :: xs) (M.mk { fst := a, snd := f }) → IsPath xs (f i)
[PROOFSTEP]
generalize h : M.mk ⟨a, f⟩ = x
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
x : M F
h : M.mk { fst := a, snd := f } = x
⊢ IsPath ({ fst := a, snd := i } :: xs) x → IsPath xs (f i)
[PROOFSTEP]
rintro (_ | ⟨_, _, _, _, rfl, hp⟩)
[GOAL]
case cons
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
f✝ : B F a → M F
hp : IsPath xs (f✝ i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f✝ }
⊢ IsPath xs (f i)
[PROOFSTEP]
cases mk_inj h
[GOAL]
case cons.refl
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
xs : Path F
a : F.A
f : B F a → M F
i : B F a
hp : IsPath xs (f i)
h : M.mk { fst := a, snd := f } = M.mk { fst := a, snd := f }
⊢ IsPath xs (f i)
[PROOFSTEP]
exact hp
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
a : F.A
i : B F a
ps : List (IdxCat F)
x : M F
a' : F.A
f : B F a' → M F
h : a = a'
⊢ B F a = B F a'
[PROOFSTEP]
rw [h]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x : M F
h : ¬IsPath ps x
⊢ iselect ps x = head default
[PROOFSTEP]
induction' ps with ps_hd ps_tail ps_ih generalizing x
[GOAL]
case nil
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ iselect [] x = head default
[PROOFSTEP]
exfalso
[GOAL]
case nil.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case nil.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
x : M F
h : ¬IsPath [] x
⊢ IsPath [] x
[PROOFSTEP]
constructor
[GOAL]
case cons
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_hd : IdxCat F
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
h : ¬IsPath (ps_hd :: ps_tail) x
⊢ iselect (ps_hd :: ps_tail) x = head default
[PROOFSTEP]
cases' ps_hd with a i
[GOAL]
case cons.mk
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
⊢ iselect ({ fst := a, snd := i } :: ps_tail) x = head default
[PROOFSTEP]
induction' x using PFunctor.M.casesOn' with x_a x_f
[GOAL]
case cons.mk.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → iselect ps_tail x = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ iselect ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f }) = head default
[PROOFSTEP]
simp only [iselect, isubtree] at ps_ih ⊢
[GOAL]
case cons.mk.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
[PROOFSTEP]
by_cases h'' : a = x_a
[GOAL]
case pos
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
case neg
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
[PROOFSTEP]
subst x_a
[GOAL]
case pos
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head
      (M.casesOn' (M.mk { fst := a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
[PROOFSTEP]
simp only [dif_pos, eq_self_iff_true, casesOn_mk']
[GOAL]
case pos
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ head (isubtree ps_tail (x_f (cast (_ : B F a = B F a) i))) = head default
[PROOFSTEP]
rw [ps_ih]
[GOAL]
case pos.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
⊢ ¬IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
[PROOFSTEP]
intro h'
[GOAL]
case pos.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case pos.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
[PROOFSTEP]
constructor
[GOAL]
case pos.h.a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ M.mk { fst := a, snd := x_f } = M.mk { fst := a, snd := ?pos.h.f✝ }
[PROOFSTEP]
try rfl
[GOAL]
case pos.h.a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ M.mk { fst := a, snd := x_f } = M.mk { fst := a, snd := ?pos.h.f✝ }
[PROOFSTEP]
rfl
[GOAL]
case pos.h.a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
[PROOFSTEP]
try rfl
[GOAL]
case pos.h.a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
[PROOFSTEP]
rfl
[GOAL]
case pos.h.a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_f : B F a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := a, snd := x_f })
h' : IsPath ps_tail (x_f (cast (_ : B F a = B F a) i))
⊢ IsPath ps_tail (x_f i)
[PROOFSTEP]
apply h'
[GOAL]
case neg
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
x✝ : M F
h✝¹ : ¬IsPath ps x✝
ps_tail : List (IdxCat F)
ps_ih : ∀ (x : M F), ¬IsPath ps_tail x → head (isubtree ps_tail x) = head default
x : M F
a : F.A
i : B F a
h✝ : ¬IsPath ({ fst := a, snd := i } :: ps_tail) x
x_a : F.A
x_f : B F x_a → M F
h : ¬IsPath ({ fst := a, snd := i } :: ps_tail) (M.mk { fst := x_a, snd := x_f })
h'' : ¬a = x_a
⊢ head
      (M.casesOn' (M.mk { fst := x_a, snd := x_f }) fun a' f =>
        if h : a = a' then isubtree ps_tail (f (cast (_ : B F a = B F a') i)) else default) =
    head default
[PROOFSTEP]
simp [*]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
⊢ x.fst = (dest (M.mk x)).fst
[PROOFSTEP]
rw [dest_mk]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
x : Obj F (M F)
⊢ (dest (M.mk x)).fst = head (M.mk x)
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ B F (head (M.mk { fst := a, snd := x })) = B F a
[PROOFSTEP]
rw [head_mk]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ children (M.mk { fst := a, snd := x }) i = x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)
[PROOFSTEP]
apply ext'
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
⊢ ∀ (i_1 : ℕ),
    MIntl.approx (children (M.mk { fst := a, snd := x }) i) i_1 =
      MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) i_1
[PROOFSTEP]
intro n
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
a : F.A
x : B F a → M F
i : B F (head (M.mk { fst := a, snd := x }))
n : ℕ
⊢ MIntl.approx (children (M.mk { fst := a, snd := x }) i) n =
    MIntl.approx (x (cast (_ : B F (head (M.mk { fst := a, snd := x })) = B F a) i)) n
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
x : Obj F (M F)
i : IdxCat F
⊢ ichildren i (M.mk x) = Obj.iget x i
[PROOFSTEP]
dsimp only [ichildren, PFunctor.Obj.iget]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
x : Obj F (M F)
i : IdxCat F
⊢ (if H' : i.fst = head (M.mk x) then children (M.mk x) (cast (_ : B F i.fst = B F (head (M.mk x))) i.snd)
    else default) =
    if h : i.fst = x.fst then Sigma.snd x (cast (_ : B F i.fst = B F x.fst) i.snd) else default
[PROOFSTEP]
congr with h
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = isubtree ps (f i)
[PROOFSTEP]
simp only [isubtree, ichildren_mk, PFunctor.Obj.iget, dif_pos, isubtree, M.casesOn_mk']
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ isubtree ps (f (cast (_ : B F a = B F a) i)) = isubtree ps (f i)
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
a : F.A
f : B F a → M F
⊢ iselect [] (M.mk { fst := a, snd := f }) = a
[PROOFSTEP]
rfl
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited (M F)
ps : Path F
a : F.A
f : B F a → M F
i : B F a
⊢ iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = iselect ps (f i)
[PROOFSTEP]
simp only [iselect, isubtree_cons]
[GOAL]
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
⊢ M.corec f x₀ = M.mk (M.corec f <$> f x₀)
[PROOFSTEP]
dsimp only [M.corec, M.mk]
[GOAL]
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
⊢ { approx := sCorec f x₀, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f x₀ n) (sCorec f x₀ (succ n))) } =
    {
      approx :=
        Approx.sMk
          ((fun i =>
              { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
            f x₀),
      consistent :=
        (_ :
          AllAgree
            (Approx.sMk
              ((fun i =>
                  { approx := sCorec f i,
                    consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
                f x₀))) }
[PROOFSTEP]
congr with n
[GOAL]
case e_approx.h
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ n =
    Approx.sMk
      ((fun i =>
          { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
        f x₀)
      n
[PROOFSTEP]
cases' n with n
[GOAL]
case e_approx.h.zero
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
⊢ sCorec f x₀ zero =
    Approx.sMk
      ((fun i =>
          { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
        f x₀)
      zero
[PROOFSTEP]
dsimp only [sCorec, Approx.sMk]
[GOAL]
case e_approx.h.succ
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
n : ℕ
⊢ sCorec f x₀ (succ n) =
    Approx.sMk
      ((fun i =>
          { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
        f x₀)
      (succ n)
[PROOFSTEP]
dsimp only [sCorec, Approx.sMk]
[GOAL]
case e_approx.h.succ
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
n : ℕ
⊢ (CofixA.intro (f x₀).fst fun i => sCorec f (Sigma.snd (f x₀) i) n) =
    CofixA.intro
      ((fun i =>
            { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
          f x₀).fst
      fun i =>
      MIntl.approx
        (Sigma.snd
          ((fun i =>
              { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
            f x₀)
          i)
        n
[PROOFSTEP]
cases h : f x₀
[GOAL]
case e_approx.h.succ.mk
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : B F fst✝ → X
h : f x₀ = { fst := fst✝, snd := snd✝ }
⊢ (CofixA.intro { fst := fst✝, snd := snd✝ }.fst fun i => sCorec f (Sigma.snd { fst := fst✝, snd := snd✝ } i) n) =
    CofixA.intro
      ((fun i =>
            { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
          { fst := fst✝, snd := snd✝ }).fst
      fun i =>
      MIntl.approx
        (Sigma.snd
          ((fun i =>
              { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) <$>
            { fst := fst✝, snd := snd✝ })
          i)
        n
[PROOFSTEP]
dsimp only [(· <$> ·), PFunctor.map]
[GOAL]
case e_approx.h.succ.mk
F : PFunctor
X✝ : Type u_1
f✝ : X✝ → Obj F X✝
X : Type u
f : X → Obj F X
x₀ : X
n : ℕ
fst✝ : F.A
snd✝ : B F fst✝ → X
h : f x₀ = { fst := fst✝, snd := snd✝ }
⊢ (CofixA.intro fst✝ fun i => sCorec f (snd✝ i) n) =
    CofixA.intro fst✝ fun i =>
      MIntl.approx
        (((fun i =>
              { approx := sCorec f i, consistent := (_ : ∀ (n : ℕ), Agree (sCorec f i n) (sCorec f i (succ n))) }) ∘
            snd✝)
          i)
        n
[PROOFSTEP]
congr
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x y z : M F
hx : Agree' n z x
hy : Agree' n z y
hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
⊢ MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
[PROOFSTEP]
induction' n with n n_ih generalizing x y z
[GOAL]
case zero
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x✝ y✝ z✝ : M F
hx✝ : Agree' n z✝ x✝
hy✝ : Agree' n z✝ y✝
hrec✝ : ∀ (ps : Path F), n = length ps → iselect ps x✝ = iselect ps y✝
x y z : M F
hx : Agree' zero z x
hy : Agree' zero z y
hrec : ∀ (ps : Path F), zero = length ps → iselect ps x = iselect ps y
⊢ MIntl.approx x (zero + 1) = MIntl.approx y (zero + 1)
[PROOFSTEP]
specialize hrec [] rfl
[GOAL]
case zero
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x✝ y✝ z✝ : M F
hx✝ : Agree' n z✝ x✝
hy✝ : Agree' n z✝ y✝
hrec✝ : ∀ (ps : Path F), n = length ps → iselect ps x✝ = iselect ps y✝
x y z : M F
hx : Agree' zero z x
hy : Agree' zero z y
hrec : iselect [] x = iselect [] y
⊢ MIntl.approx x (zero + 1) = MIntl.approx y (zero + 1)
[PROOFSTEP]
induction x using PFunctor.M.casesOn'
[GOAL]
case zero.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x y✝ z✝ : M F
hx✝ : Agree' n z✝ x
hy✝ : Agree' n z✝ y✝
hrec✝ : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y✝
y z : M F
hy : Agree' zero z y
a✝ : F.A
f✝ : B F a✝ → M F
hx : Agree' zero z (M.mk { fst := a✝, snd := f✝ })
hrec : iselect [] (M.mk { fst := a✝, snd := f✝ }) = iselect [] y
⊢ MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (zero + 1) = MIntl.approx y (zero + 1)
[PROOFSTEP]
induction y using PFunctor.M.casesOn'
[GOAL]
case zero.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x y z✝ : M F
hx✝ : Agree' n z✝ x
hy✝ : Agree' n z✝ y
hrec✝ : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
z : M F
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
hx : Agree' zero z (M.mk { fst := a✝¹, snd := f✝¹ })
a✝ : F.A
f✝ : B F a✝ → M F
hy : Agree' zero z (M.mk { fst := a✝, snd := f✝ })
hrec : iselect [] (M.mk { fst := a✝¹, snd := f✝¹ }) = iselect [] (M.mk { fst := a✝, snd := f✝ })
⊢ MIntl.approx (M.mk { fst := a✝¹, snd := f✝¹ }) (zero + 1) = MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (zero + 1)
[PROOFSTEP]
simp only [iselect_nil] at hrec
[GOAL]
case zero.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x y z✝ : M F
hx✝ : Agree' n z✝ x
hy✝ : Agree' n z✝ y
hrec✝ : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
z : M F
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
hx : Agree' zero z (M.mk { fst := a✝¹, snd := f✝¹ })
a✝ : F.A
f✝ : B F a✝ → M F
hy : Agree' zero z (M.mk { fst := a✝, snd := f✝ })
hrec : a✝¹ = a✝
⊢ MIntl.approx (M.mk { fst := a✝¹, snd := f✝¹ }) (zero + 1) = MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (zero + 1)
[PROOFSTEP]
subst hrec
[GOAL]
case zero.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n : ℕ
x y z✝ : M F
hx✝ : Agree' n z✝ x
hy✝ : Agree' n z✝ y
hrec : ∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y
z : M F
a✝ : F.A
f✝¹ : B F a✝ → M F
hx : Agree' zero z (M.mk { fst := a✝, snd := f✝¹ })
f✝ : B F a✝ → M F
hy : Agree' zero z (M.mk { fst := a✝, snd := f✝ })
⊢ MIntl.approx (M.mk { fst := a✝, snd := f✝¹ }) (zero + 1) = MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (zero + 1)
[PROOFSTEP]
simp only [approx_mk, true_and_iff, eq_self_iff_true, heq_iff_eq, zero_eq, CofixA.intro.injEq, heq_eq_eq,
  eq_iff_true_of_subsingleton, and_self]
[GOAL]
case succ
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x✝ y✝ z✝ : M F
hx✝ : Agree' n✝ z✝ x✝
hy✝ : Agree' n✝ z✝ y✝
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x✝ = iselect ps y✝
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
x y z : M F
hx : Agree' (succ n) z x
hy : Agree' (succ n) z y
hrec : ∀ (ps : Path F), succ n = length ps → iselect ps x = iselect ps y
⊢ MIntl.approx x (succ n + 1) = MIntl.approx y (succ n + 1)
[PROOFSTEP]
cases hx
[GOAL]
case succ.step
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x✝¹ y✝¹ z✝ : M F
hx : Agree' n✝ z✝ x✝¹
hy✝ : Agree' n✝ z✝ y✝¹
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x✝¹ = iselect ps y✝¹
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
x y z : M F
hy : Agree' (succ n) z y
hrec : ∀ (ps : Path F), succ n = length ps → iselect ps x = iselect ps y
a✝³ : F.A
x✝ y✝ : B F a✝³ → M F
a✝² : ∀ (i : B F a✝³), Agree' n (x✝ i) (y✝ i)
a✝¹ : z = M.mk { fst := a✝³, snd := x✝ }
a✝ : x = M.mk { fst := a✝³, snd := y✝ }
⊢ MIntl.approx x (succ n + 1) = MIntl.approx y (succ n + 1)
[PROOFSTEP]
cases hy
[GOAL]
case succ.step.step
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x✝² y✝² z✝ : M F
hx : Agree' n✝ z✝ x✝²
hy : Agree' n✝ z✝ y✝²
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x✝² = iselect ps y✝²
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
x y z : M F
hrec : ∀ (ps : Path F), succ n = length ps → iselect ps x = iselect ps y
a✝⁷ : F.A
x✝¹ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁵ : z = M.mk { fst := a✝⁷, snd := x✝¹ }
a✝⁴ : x = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
x✝ y✝ : B F a✝³ → M F
a✝² : ∀ (i : B F a✝³), Agree' n (x✝ i) (y✝ i)
a✝¹ : z = M.mk { fst := a✝³, snd := x✝ }
a✝ : y = M.mk { fst := a✝³, snd := y✝ }
⊢ MIntl.approx x (succ n + 1) = MIntl.approx y (succ n + 1)
[PROOFSTEP]
induction x using PFunctor.M.casesOn'
[GOAL]
case succ.step.step.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y✝² z✝ : M F
hx : Agree' n✝ z✝ x
hy : Agree' n✝ z✝ y✝²
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y✝²
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
y z : M F
a✝⁸ : F.A
x✝¹ y✝¹ : B F a✝⁸ → M F
a✝⁷ : ∀ (i : B F a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : z = M.mk { fst := a✝⁸, snd := x✝¹ }
a✝⁵ : F.A
x✝ y✝ : B F a✝⁵ → M F
a✝⁴ : ∀ (i : B F a✝⁵), Agree' n (x✝ i) (y✝ i)
a✝³ : z = M.mk { fst := a✝⁵, snd := x✝ }
a✝² : y = M.mk { fst := a✝⁵, snd := y✝ }
a✝¹ : F.A
f✝ : B F a✝¹ → M F
hrec : ∀ (ps : Path F), succ n = length ps → iselect ps (M.mk { fst := a✝¹, snd := f✝ }) = iselect ps y
a✝ : M.mk { fst := a✝¹, snd := f✝ } = M.mk { fst := a✝⁸, snd := y✝¹ }
⊢ MIntl.approx (M.mk { fst := a✝¹, snd := f✝ }) (succ n + 1) = MIntl.approx y (succ n + 1)
[PROOFSTEP]
induction y using PFunctor.M.casesOn'
[GOAL]
case succ.step.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z✝ : M F
hx : Agree' n✝ z✝ x
hy : Agree' n✝ z✝ y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
z : M F
a✝⁹ : F.A
x✝¹ y✝¹ : B F a✝⁹ → M F
a✝⁸ : ∀ (i : B F a✝⁹), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁷ : z = M.mk { fst := a✝⁹, snd := x✝¹ }
a✝⁶ : F.A
x✝ y✝ : B F a✝⁶ → M F
a✝⁵ : ∀ (i : B F a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : z = M.mk { fst := a✝⁶, snd := x✝ }
a✝³ : F.A
f✝¹ : B F a✝³ → M F
a✝² : M.mk { fst := a✝³, snd := f✝¹ } = M.mk { fst := a✝⁹, snd := y✝¹ }
a✝¹ : F.A
f✝ : B F a✝¹ → M F
a✝ : M.mk { fst := a✝¹, snd := f✝ } = M.mk { fst := a✝⁶, snd := y✝ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝³, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝¹, snd := f✝ })
⊢ MIntl.approx (M.mk { fst := a✝³, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝¹, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
subst z
[GOAL]
case succ.step.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : B F a✝⁸ → M F
a✝⁷ : ∀ (i : B F a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : B F a✝⁶ → M F
a✝⁵ : ∀ (i : B F a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : B F a✝⁴ → M F
a✝³ : M.mk { fst := a✝⁴, snd := f✝¹ } = M.mk { fst := a✝⁸, snd := y✝¹ }
a✝² : F.A
f✝ : B F a✝² → M F
a✝¹ : M.mk { fst := a✝², snd := f✝ } = M.mk { fst := a✝⁶, snd := y✝ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁴, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝², snd := f✝ })
a✝ : M.mk { fst := a✝⁸, snd := x✝¹ } = M.mk { fst := a✝⁶, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁴, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝², snd := f✝ }) (succ n + 1)
[PROOFSTEP]
iterate 3 (have := mk_inj ‹_›; cases this)
[GOAL]
case succ.step.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : B F a✝⁸ → M F
a✝⁷ : ∀ (i : B F a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : B F a✝⁶ → M F
a✝⁵ : ∀ (i : B F a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : B F a✝⁴ → M F
a✝³ : M.mk { fst := a✝⁴, snd := f✝¹ } = M.mk { fst := a✝⁸, snd := y✝¹ }
a✝² : F.A
f✝ : B F a✝² → M F
a✝¹ : M.mk { fst := a✝², snd := f✝ } = M.mk { fst := a✝⁶, snd := y✝ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁴, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝², snd := f✝ })
a✝ : M.mk { fst := a✝⁸, snd := x✝¹ } = M.mk { fst := a✝⁶, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁴, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝², snd := f✝ }) (succ n + 1)
[PROOFSTEP]
have := mk_inj ‹_›
[GOAL]
case succ.step.step.f.f
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁸ : F.A
x✝¹ y✝¹ : B F a✝⁸ → M F
a✝⁷ : ∀ (i : B F a✝⁸), Agree' n (x✝¹ i) (y✝¹ i)
a✝⁶ : F.A
x✝ y✝ : B F a✝⁶ → M F
a✝⁵ : ∀ (i : B F a✝⁶), Agree' n (x✝ i) (y✝ i)
a✝⁴ : F.A
f✝¹ : B F a✝⁴ → M F
a✝³ : M.mk { fst := a✝⁴, snd := f✝¹ } = M.mk { fst := a✝⁸, snd := y✝¹ }
a✝² : F.A
f✝ : B F a✝² → M F
a✝¹ : M.mk { fst := a✝², snd := f✝ } = M.mk { fst := a✝⁶, snd := y✝ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁴, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝², snd := f✝ })
a✝ : M.mk { fst := a✝⁸, snd := x✝¹ } = M.mk { fst := a✝⁶, snd := x✝ }
this : { fst := a✝⁸, snd := x✝¹ } = { fst := a✝⁶, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁴, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝², snd := f✝ }) (succ n + 1)
[PROOFSTEP]
cases this
[GOAL]
case succ.step.step.f.f.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : B F a✝⁵ → M F
a✝⁴ : M.mk { fst := a✝⁵, snd := f✝¹ } = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
f✝ : B F a✝³ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁵, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝³, snd := f✝ })
y✝ : B F a✝⁷ → M F
a✝² : M.mk { fst := a✝³, snd := f✝ } = M.mk { fst := a✝⁷, snd := y✝ }
a✝¹ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk { fst := a✝⁷, snd := x✝ } = M.mk { fst := a✝⁷, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁵, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝³, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
have := mk_inj ‹_›
[GOAL]
case succ.step.step.f.f.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : B F a✝⁵ → M F
a✝⁴ : M.mk { fst := a✝⁵, snd := f✝¹ } = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
f✝ : B F a✝³ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁵, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝³, snd := f✝ })
y✝ : B F a✝⁷ → M F
a✝² : M.mk { fst := a✝³, snd := f✝ } = M.mk { fst := a✝⁷, snd := y✝ }
a✝¹ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk { fst := a✝⁷, snd := x✝ } = M.mk { fst := a✝⁷, snd := x✝ }
this : { fst := a✝⁷, snd := x✝ } = { fst := a✝⁷, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁵, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝³, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
cases this
[GOAL]
case succ.step.step.f.f.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : B F a✝⁵ → M F
a✝⁴ : M.mk { fst := a✝⁵, snd := f✝¹ } = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
f✝ : B F a✝³ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁵, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝³, snd := f✝ })
y✝ : B F a✝⁷ → M F
a✝² : M.mk { fst := a✝³, snd := f✝ } = M.mk { fst := a✝⁷, snd := y✝ }
a✝¹ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk { fst := a✝⁷, snd := x✝ } = M.mk { fst := a✝⁷, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁵, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝³, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
have := mk_inj ‹_›
[GOAL]
case succ.step.step.f.f.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : B F a✝⁵ → M F
a✝⁴ : M.mk { fst := a✝⁵, snd := f✝¹ } = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
f✝ : B F a✝³ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁵, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝³, snd := f✝ })
y✝ : B F a✝⁷ → M F
a✝² : M.mk { fst := a✝³, snd := f✝ } = M.mk { fst := a✝⁷, snd := y✝ }
a✝¹ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk { fst := a✝⁷, snd := x✝ } = M.mk { fst := a✝⁷, snd := x✝ }
this : { fst := a✝⁷, snd := x✝ } = { fst := a✝⁷, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁵, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝³, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
cases this
[GOAL]
case succ.step.step.f.f.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
hrec✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a✝⁷ : F.A
x✝ y✝¹ : B F a✝⁷ → M F
a✝⁶ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝¹ i)
a✝⁵ : F.A
f✝¹ : B F a✝⁵ → M F
a✝⁴ : M.mk { fst := a✝⁵, snd := f✝¹ } = M.mk { fst := a✝⁷, snd := y✝¹ }
a✝³ : F.A
f✝ : B F a✝³ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝⁵, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝³, snd := f✝ })
y✝ : B F a✝⁷ → M F
a✝² : M.mk { fst := a✝³, snd := f✝ } = M.mk { fst := a✝⁷, snd := y✝ }
a✝¹ : ∀ (i : B F a✝⁷), Agree' n (x✝ i) (y✝ i)
a✝ : M.mk { fst := a✝⁷, snd := x✝ } = M.mk { fst := a✝⁷, snd := x✝ }
⊢ MIntl.approx (M.mk { fst := a✝⁵, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝³, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
rename_i n_ih a f₃ f₂ hAgree₂ _ _ h₂ _ _ f₁ h₁ hAgree₁ clr
[GOAL]
case succ.step.step.f.f.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
h₂ : M.mk { fst := a✝¹, snd := f✝¹ } = M.mk { fst := a, snd := f₂ }
a✝ : F.A
f✝ : B F a✝ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝¹, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝, snd := f✝ })
f₁ : B F a → M F
h₁ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₁ }
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
⊢ MIntl.approx (M.mk { fst := a✝¹, snd := f✝¹ }) (succ n + 1) =
    MIntl.approx (M.mk { fst := a✝, snd := f✝ }) (succ n + 1)
[PROOFSTEP]
simp only [approx_mk, true_and_iff, eq_self_iff_true, heq_iff_eq]
[GOAL]
case succ.step.step.f.f.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
h₂ : M.mk { fst := a✝¹, snd := f✝¹ } = M.mk { fst := a, snd := f₂ }
a✝ : F.A
f✝ : B F a✝ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝¹, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝, snd := f✝ })
f₁ : B F a → M F
h₁ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₁ }
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
⊢ (CofixA.intro a✝¹ fun j => MIntl.approx (f✝¹ j) (n + 1)) = CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n + 1)
[PROOFSTEP]
have := mk_inj h₁
[GOAL]
case succ.step.step.f.f.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝¹ : F.A
f✝¹ : B F a✝¹ → M F
h₂ : M.mk { fst := a✝¹, snd := f✝¹ } = M.mk { fst := a, snd := f₂ }
a✝ : F.A
f✝ : B F a✝ → M F
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝¹, snd := f✝¹ }) = iselect ps (M.mk { fst := a✝, snd := f✝ })
f₁ : B F a → M F
h₁ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₁ }
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
this : { fst := a✝, snd := f✝ } = { fst := a, snd := f₁ }
⊢ (CofixA.intro a✝¹ fun j => MIntl.approx (f✝¹ j) (n + 1)) = CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n + 1)
[PROOFSTEP]
cases this
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : B F a✝ → M F
h₂ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₂ }
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝, snd := f✝ }) = iselect ps (M.mk { fst := a, snd := f₁ })
h₁ : M.mk { fst := a, snd := f₁ } = M.mk { fst := a, snd := f₁ }
⊢ (CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n + 1)) = CofixA.intro a fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
clear h₁
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : B F a✝ → M F
h₂ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₂ }
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝, snd := f✝ }) = iselect ps (M.mk { fst := a, snd := f₁ })
⊢ (CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n + 1)) = CofixA.intro a fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
have := mk_inj h₂
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
a✝ : F.A
f✝ : B F a✝ → M F
h₂ : M.mk { fst := a✝, snd := f✝ } = M.mk { fst := a, snd := f₂ }
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a✝, snd := f✝ }) = iselect ps (M.mk { fst := a, snd := f₁ })
this : { fst := a✝, snd := f✝ } = { fst := a, snd := f₂ }
⊢ (CofixA.intro a✝ fun j => MIntl.approx (f✝ j) (n + 1)) = CofixA.intro a fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
cases this
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
h₂ : M.mk { fst := a, snd := f₂ } = M.mk { fst := a, snd := f₂ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
⊢ (CofixA.intro a fun j => MIntl.approx (f₂ j) (n + 1)) = CofixA.intro a fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
clear h₂
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
⊢ (CofixA.intro a fun j => MIntl.approx (f₂ j) (n + 1)) = CofixA.intro a fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
congr
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
⊢ (fun j => MIntl.approx (f₂ j) (n + 1)) = fun j => MIntl.approx (f₁ j) (n + 1)
[PROOFSTEP]
ext i
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
i : B F a
⊢ MIntl.approx (f₂ i) (n + 1) = MIntl.approx (f₁ i) (n + 1)
[PROOFSTEP]
apply n_ih
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hx
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
i : B F a
⊢ Agree' n ?succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.z (f₂ i)
[PROOFSTEP]
solve_by_elim
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hy
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
i : B F a
⊢ Agree' n (f₃ i) (f₁ i)
[PROOFSTEP]
solve_by_elim
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
i : B F a
⊢ ∀ (ps : Path F), n = length ps → iselect ps (f₂ i) = iselect ps (f₁ i)
[PROOFSTEP]
introv h
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
hrec :
  ∀ (ps : Path F),
    succ n = length ps → iselect ps (M.mk { fst := a, snd := f₂ }) = iselect ps (M.mk { fst := a, snd := f₁ })
i : B F a
ps : Path F
h : n = length ps
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
[PROOFSTEP]
specialize hrec (⟨_, i⟩ :: ps) (congr_arg _ h)
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
i : B F a
ps : Path F
h : n = length ps
hrec :
  iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f₂ }) =
    iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f₁ })
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
[PROOFSTEP]
simp only [iselect_cons] at hrec
[GOAL]
case succ.step.step.f.f.refl.refl.refl.refl.refl.e_a.h.hrec
F : PFunctor
X : Type u_1
f : X → Obj F X
inst✝¹ : Inhabited (M F)
inst✝ : DecidableEq F.A
n✝ : ℕ
x y z : M F
hx : Agree' n✝ z x
hy : Agree' n✝ z y
n_ih✝ : ∀ (ps : Path F), n✝ = length ps → iselect ps x = iselect ps y
n : ℕ
n_ih :
  ∀ (x y z : M F),
    Agree' n z x →
      Agree' n z y →
        (∀ (ps : Path F), n = length ps → iselect ps x = iselect ps y) → MIntl.approx x (n + 1) = MIntl.approx y (n + 1)
a : F.A
f₃ f₂ : B F a → M F
hAgree₂ : ∀ (i : B F a), Agree' n (f₃ i) (f₂ i)
f₁ : B F a → M F
hAgree₁ : ∀ (i : B F a), Agree' n (f₃ i) (f₁ i)
clr : M.mk { fst := a, snd := f₃ } = M.mk { fst := a, snd := f₃ }
i : B F a
ps : Path F
h : n = length ps
hrec : iselect ps (f₂ i) = iselect ps (f₁ i)
⊢ iselect ps (f₂ i) = iselect ps (f₁ i)
[PROOFSTEP]
exact hrec
[GOAL]
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
apply ext'
[GOAL]
case H
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
intro i
[GOAL]
case H
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
induction' i with i i_ih
[GOAL]
case H.zero
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
cases x.approx 0
[GOAL]
case H.zero.continue
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
cases y.approx 0
[GOAL]
case H.zero.continue.continue
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
constructor
[GOAL]
case H.succ
F : PFunctor
X : Type u_1
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)
[PROOFSTEP]
apply ext_aux x y x
[GOAL]
case H.succ.hx
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
rw [← agree_iff_agree']
[GOAL]
case H.succ.hx
F : PFunctor
X : Type u_1
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))
[PROOFSTEP]
apply x.consistent
[GOAL]
case H.succ.hy
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
rw [← agree_iff_agree', i_ih]
[GOAL]
case H.succ.hy
F : PFunctor
X : Type u_1
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))
[PROOFSTEP]
apply y.consistent
[GOAL]
case H.succ.hrec
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
introv H'
[GOAL]
case H.succ.hrec
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
dsimp only [iselect] at H
[GOAL]
case H.succ.hrec
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
cases H'
[GOAL]
case H.succ.hrec.refl
F : PFunctor
X : Type u_1
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
[PROOFSTEP]
apply H ps
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
⊢ R s₁ s₂ →
    IsPath ps s₁ ∨ IsPath ps s₂ →
      iselect ps s₁ = iselect ps s₂ ∧
        ∃ a f f',
          isubtree ps s₁ = M.mk { fst := a, snd := f } ∧
            isubtree ps s₂ = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
intro h₀ hh
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₀ : R s₁ s₂
hh : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f',
      isubtree ps s₁ = M.mk { fst := a, snd := f } ∧
        isubtree ps s₂ = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
induction' s₁ using PFunctor.M.casesOn' with a f
[GOAL]
case f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₀✝ : R s₁ s₂
hh✝ : IsPath ps s₁ ∨ IsPath ps s₂
a : F.A
f : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) s₂
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps s₂
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps s₂ ∧
    ∃ a_1 f_1 f',
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps s₂ = M.mk { fst := a_1, snd := f' } ∧ ∀ (i : B F a_1), R (f_1 i) (f' i)
[PROOFSTEP]
rename_i h₁ hh₁
[GOAL]
case f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁ : R s₁ s₂
hh₁ : IsPath ps s₁ ∨ IsPath ps s₂
a : F.A
f : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) s₂
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps s₂
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps s₂ ∧
    ∃ a_1 f_1 f',
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps s₂ = M.mk { fst := a_1, snd := f' } ∧ ∀ (i : B F a_1), R (f_1 i) (f' i)
[PROOFSTEP]
induction' s₂ using PFunctor.M.casesOn' with a' f'
[GOAL]
case f.f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁✝ : R s₁ s₂
hh₁✝ : IsPath ps s₁ ∨ IsPath ps s₂
a : F.A
f : B F a → M F
h₀✝ : R (M.mk { fst := a, snd := f }) s₂
hh✝ : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps s₂
a' : F.A
f' : B F a' → M F
h₁ : R s₁ (M.mk { fst := a', snd := f' })
hh₁ : IsPath ps s₁ ∨ IsPath ps (M.mk { fst := a', snd := f' })
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a', snd := f' })
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a', snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps (M.mk { fst := a', snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
rename_i h₁' hh₁' h₂ hh₂
[GOAL]
case f.f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁' : R s₁ s₂
hh₁' : IsPath ps s₁ ∨ IsPath ps s₂
a : F.A
f : B F a → M F
h₂ : R (M.mk { fst := a, snd := f }) s₂
hh₂ : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps s₂
a' : F.A
f' : B F a' → M F
h₁ : R s₁ (M.mk { fst := a', snd := f' })
hh₁ : IsPath ps s₁ ∨ IsPath ps (M.mk { fst := a', snd := f' })
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a', snd := f' })
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a', snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps (M.mk { fst := a', snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
clear h₁ hh₁ h₂ hh₂ hh₁'
[GOAL]
case f.f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁' : R s₁ s₂
a : F.A
f : B F a → M F
a' : F.A
f' : B F a' → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a', snd := f' })
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a', snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps (M.mk { fst := a', snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
obtain rfl : a = a' := bisim.head h₀
[GOAL]
case f.f
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁' : R s₁ s₂
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
hh : IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' })
⊢ iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
induction' ps with i ps ps_ih generalizing a f f'
[GOAL]
case f.f.nil
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps (M.mk { fst := a✝, snd := f'✝ })
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
hh : IsPath [] (M.mk { fst := a, snd := f }) ∨ IsPath [] (M.mk { fst := a, snd := f' })
⊢ iselect [] (M.mk { fst := a, snd := f }) = iselect [] (M.mk { fst := a, snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree [] (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree [] (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
exists rfl, a, f, f', rfl, rfl
[GOAL]
case f.f.nil
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps (M.mk { fst := a✝, snd := f'✝ })
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
hh : IsPath [] (M.mk { fst := a, snd := f }) ∨ IsPath [] (M.mk { fst := a, snd := f' })
⊢ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
apply bisim.tail h₀
[GOAL]
case f.f.cons
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
i : IdxCat F
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
hh : IsPath (i :: ps) (M.mk { fst := a, snd := f }) ∨ IsPath (i :: ps) (M.mk { fst := a, snd := f' })
⊢ iselect (i :: ps) (M.mk { fst := a, snd := f }) = iselect (i :: ps) (M.mk { fst := a, snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree (i :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree (i :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
cases' i with a' i
[GOAL]
case f.f.cons.mk
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
a' : F.A
i : B F a'
hh :
  IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ iselect ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f }) =
      iselect ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
obtain rfl : a = a' := by rcases hh with hh | hh <;> cases isPath_cons hh <;> rfl
[GOAL]
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
a' : F.A
i : B F a'
hh :
  IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ a = a'
[PROOFSTEP]
rcases hh with hh | hh
[GOAL]
case inl
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
a' : F.A
i : B F a'
hh : IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f })
⊢ a = a'
[PROOFSTEP]
cases isPath_cons hh
[GOAL]
case inr
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
a' : F.A
i : B F a'
hh : IsPath ({ fst := a', snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ a = a'
[PROOFSTEP]
cases isPath_cons hh
[GOAL]
case inl.refl
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh : IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f })
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case inr.refl
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh : IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ a = a
[PROOFSTEP]
rfl
[GOAL]
case f.f.cons.mk
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        iselect ps (M.mk { fst := a, snd := f }) = iselect ps (M.mk { fst := a, snd := f' }) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) =
      iselect ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
dsimp only [iselect] at ps_ih ⊢
[GOAL]
case f.f.cons.mk
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
⊢ head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f })) =
      head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
have h₁ := bisim.tail h₀ i
[GOAL]
case f.f.cons.mk
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
h₁ : R (f i) (f' i)
⊢ head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f })) =
      head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
induction' h : f i using PFunctor.M.casesOn' with a₀ f₀
[GOAL]
case f.f.cons.mk.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
h₁ : R (f i) (f' i)
x✝ : M F
h✝ : f i = x✝
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
⊢ head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f })) =
      head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
induction' h' : f' i using PFunctor.M.casesOn' with a₁ f₁
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
h₁ : R (f i) (f' i)
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
a₁ : F.A
f₁ : B F a₁ → M F
h' : f' i = M.mk { fst := a₁, snd := f₁ }
⊢ head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f })) =
      head (isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })) ∧
    ∃ a_1 f_1 f'_1,
      isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
        isubtree ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
          ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
[PROOFSTEP]
simp only [h, h', isubtree_cons] at ps_ih ⊢
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
h₁ : R (f i) (f' i)
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
a₁ : F.A
f₁ : B F a₁ → M F
h' : f' i = M.mk { fst := a₁, snd := f₁ }
⊢ head (isubtree ps (M.mk { fst := a₀, snd := f₀ })) = head (isubtree ps (M.mk { fst := a₁, snd := f₁ })) ∧
    ∃ a f f',
      isubtree ps (M.mk { fst := a₀, snd := f₀ }) = M.mk { fst := a, snd := f } ∧
        isubtree ps (M.mk { fst := a₁, snd := f₁ }) = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
rw [h, h'] at h₁
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
a₁ : F.A
f₁ : B F a₁ → M F
h₁ : R (M.mk { fst := a₀, snd := f₀ }) (M.mk { fst := a₁, snd := f₁ })
h' : f' i = M.mk { fst := a₁, snd := f₁ }
⊢ head (isubtree ps (M.mk { fst := a₀, snd := f₀ })) = head (isubtree ps (M.mk { fst := a₁, snd := f₁ })) ∧
    ∃ a f f',
      isubtree ps (M.mk { fst := a₀, snd := f₀ }) = M.mk { fst := a, snd := f } ∧
        isubtree ps (M.mk { fst := a₁, snd := f₁ }) = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
obtain rfl : a₀ = a₁ := bisim.head h₁
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
f₁ : B F a₀ → M F
h₁ : R (M.mk { fst := a₀, snd := f₀ }) (M.mk { fst := a₀, snd := f₁ })
h' : f' i = M.mk { fst := a₀, snd := f₁ }
⊢ head (isubtree ps (M.mk { fst := a₀, snd := f₀ })) = head (isubtree ps (M.mk { fst := a₀, snd := f₁ })) ∧
    ∃ a f f',
      isubtree ps (M.mk { fst := a₀, snd := f₀ }) = M.mk { fst := a, snd := f } ∧
        isubtree ps (M.mk { fst := a₀, snd := f₁ }) = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
[PROOFSTEP]
apply ps_ih _ _ _ h₁
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
f₁ : B F a₀ → M F
h₁ : R (M.mk { fst := a₀, snd := f₀ }) (M.mk { fst := a₀, snd := f₁ })
h' : f' i = M.mk { fst := a₀, snd := f₁ }
⊢ IsPath ps (M.mk { fst := a₀, snd := f₀ }) ∨ IsPath ps (M.mk { fst := a₀, snd := f₁ })
[PROOFSTEP]
rw [← h, ← h']
[GOAL]
case f.f.cons.mk.f.f
F : PFunctor
X : Type u_1
f✝¹ : X → Obj F X
R : M F → M F → Prop
inst✝ : Inhabited (M F)
bisim : IsBisimulation R
s₁ s₂ : M F
ps✝ : Path F
h₁' : R s₁ s₂
a✝ : F.A
f✝ f'✝ : B F a✝ → M F
h₀✝ : R (M.mk { fst := a✝, snd := f✝ }) (M.mk { fst := a✝, snd := f'✝ })
hh✝ : IsPath ps✝ (M.mk { fst := a✝, snd := f✝ }) ∨ IsPath ps✝ (M.mk { fst := a✝, snd := f'✝ })
ps : List (IdxCat F)
ps_ih :
  ∀ (a : F.A) (f f' : B F a → M F),
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) →
      IsPath ps (M.mk { fst := a, snd := f }) ∨ IsPath ps (M.mk { fst := a, snd := f' }) →
        head (isubtree ps (M.mk { fst := a, snd := f })) = head (isubtree ps (M.mk { fst := a, snd := f' })) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk { fst := a, snd := f }) = M.mk { fst := a_1, snd := f_1 } ∧
              isubtree ps (M.mk { fst := a, snd := f' }) = M.mk { fst := a_1, snd := f'_1 } ∧
                ∀ (i : B F a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : B F a → M F
h₀ : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B F a
hh :
  IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f }) ∨
    IsPath ({ fst := a, snd := i } :: ps) (M.mk { fst := a, snd := f' })
x✝¹ : M F
h✝ : f i = x✝¹
a₀ : F.A
f₀ : B F a₀ → M F
h : f i = M.mk { fst := a₀, snd := f₀ }
x✝ : M F
h'✝ : f' i = x✝
f₁ : B F a₀ → M F
h₁ : R (M.mk { fst := a₀, snd := f₀ }) (M.mk { fst := a₀, snd := f₁ })
h' : f' i = M.mk { fst := a₀, snd := f₁ }
⊢ IsPath ps (f i) ∨ IsPath ps (f' i)
[PROOFSTEP]
apply Or.imp isPath_cons' isPath_cons' hh
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
⊢ ∀ (s₁ s₂ : M F), R s₁ s₂ → s₁ = s₂
[PROOFSTEP]
inhabit M F
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
⊢ ∀ (s₁ s₂ : M F), R s₁ s₂ → s₁ = s₂
[PROOFSTEP]
introv Hr
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ s₁ = s₂
[PROOFSTEP]
apply ext
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
⊢ ∀ (ps : Path F), iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
introv
[GOAL]
case H
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
by_cases h : IsPath ps s₁ ∨ IsPath ps s₂
[GOAL]
case pos
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
have H := nth_of_bisim R bisim _ _ ps Hr h
[GOAL]
case pos
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : IsPath ps s₁ ∨ IsPath ps s₂
H :
  iselect ps s₁ = iselect ps s₂ ∧
    ∃ a f f',
      isubtree ps s₁ = M.mk { fst := a, snd := f } ∧
        isubtree ps s₂ = M.mk { fst := a, snd := f' } ∧ ∀ (i : B F a), R (f i) (f' i)
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
exact H.left
[GOAL]
case neg
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬(IsPath ps s₁ ∨ IsPath ps s₂)
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
rw [not_or] at h
[GOAL]
case neg
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h : ¬IsPath ps s₁ ∧ ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
cases' h with h₀ h₁
[GOAL]
case neg.intro
F : PFunctor
X : Type u_1
f : X → Obj F X
R : M F → M F → Prop
inst✝ : Nonempty (M F)
bisim : IsBisimulation R
inhabited_h : Inhabited (M F)
s₁ s₂ : M F
Hr : R s₁ s₂
ps : Path F
h₀ : ¬IsPath ps s₁
h₁ : ¬IsPath ps s₂
⊢ iselect ps s₁ = iselect ps s₂
[PROOFSTEP]
simp only [iselect_eq_default, *, not_false_iff]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
x : α
⊢ dest (M.corec g x) = M.corec g <$> g x
[PROOFSTEP]
rw [corec_def, dest_mk]
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
⊢ ∀ (x y : M P), R x y → x = y
[PROOFSTEP]
introv h'
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
⊢ x = y
[PROOFSTEP]
haveI := Inhabited.mk x.head
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ x = y
[PROOFSTEP]
apply eq_of_bisim R _ _ _ h'
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
x y : M P
h' : R x y
this : Inhabited P.A
⊢ IsBisimulation R
[PROOFSTEP]
clear h' x y
[GOAL]
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
⊢ IsBisimulation R
[PROOFSTEP]
constructor
[GOAL]
case head
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a a' : P.A} {f : B P a → M P} {f' : B P a' → M P},
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' }) → a = a'
[PROOFSTEP]
introv ih
[GOAL]
case tail
F : PFunctor
X : Type u_1
f : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
⊢ ∀ {a : P.A} {f f' : B P a → M P},
    R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' }) → ∀ (i : B P a), R (f i) (f' i)
[PROOFSTEP]
introv ih
[GOAL]
case head
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
⊢ a = a'
[PROOFSTEP]
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩
[GOAL]
case tail
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
⊢ R (f i) (f' i)
[PROOFSTEP]
rcases h _ _ ih with ⟨a'', g, g', h₀, h₁, h₂⟩
[GOAL]
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ a = a'
[PROOFSTEP]
clear h
[GOAL]
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
h :
  ∀ (x y : M P),
    R x y → ∃ a f f', dest x = { fst := a, snd := f } ∧ dest y = { fst := a, snd := f' } ∧ ∀ (i : B P a), R (f i) (f' i)
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a, snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
[PROOFSTEP]
clear h
[GOAL]
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ a = a'
[PROOFSTEP]
replace h₀ := congr_arg Sigma.fst h₀
[GOAL]
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₁ : dest (M.mk { fst := a', snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
⊢ a = a'
[PROOFSTEP]
replace h₁ := congr_arg Sigma.fst h₁
[GOAL]
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : (dest (M.mk { fst := a, snd := f })).fst = { fst := a'', snd := g }.fst
h₁ : (dest (M.mk { fst := a', snd := f' })).fst = { fst := a'', snd := g' }.fst
⊢ a = a'
[PROOFSTEP]
simp only [dest_mk] at h₀ h₁
[GOAL]
case head.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a a' : P.A
f : B P a → M P
f' : B P a' → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a', snd := f' })
a'' : P.A
g g' : B P a'' → M P
h₂ : ∀ (i : B P a''), R (g i) (g' i)
h₀ : a = a''
h₁ : a' = a''
⊢ a = a'
[PROOFSTEP]
rw [h₀, h₁]
[GOAL]
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : dest (M.mk { fst := a, snd := f }) = { fst := a'', snd := g }
h₁ : dest (M.mk { fst := a, snd := f' }) = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
[PROOFSTEP]
simp only [dest_mk] at h₀ h₁
[GOAL]
case tail.intro.intro.intro.intro.intro
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
a'' : P.A
g g' : B P a'' → M P
h₀ : { fst := a, snd := f } = { fst := a'', snd := g }
h₁ : { fst := a, snd := f' } = { fst := a'', snd := g' }
h₂ : ∀ (i : B P a''), R (g i) (g' i)
⊢ R (f i) (f' i)
[PROOFSTEP]
cases h₀
[GOAL]
case tail.intro.intro.intro.intro.intro.refl
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
g' : B P a → M P
h₁ : { fst := a, snd := f' } = { fst := a, snd := g' }
h₂ : ∀ (i : B P a), R (f i) (g' i)
⊢ R (f i) (f' i)
[PROOFSTEP]
cases h₁
[GOAL]
case tail.intro.intro.intro.intro.intro.refl.refl
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
R : M P → M P → Prop
this : Inhabited P.A
a : P.A
f f' : B P a → M P
ih : R (M.mk { fst := a, snd := f }) (M.mk { fst := a, snd := f' })
i : B P a
h₂ : ∀ (i : B P a), R (f i) (f' i)
⊢ R (f i) (f' i)
[PROOFSTEP]
apply h₂
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
⊢ f = M.corec g
[PROOFSTEP]
ext x
[GOAL]
case h
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ f x = M.corec g x
[PROOFSTEP]
apply bisim' (fun _ => True) _ _ _ _ trivial
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
clear x
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
⊢ ∀ (x : α),
    (fun x => True) x →
      ∃ a f_1 f',
        dest (f x) = { fst := a, snd := f_1 } ∧
          dest (M.corec g x) = { fst := a, snd := f' } ∧
            ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
intro x _
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
cases' gxeq : g x with a f'
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
have h₀ : M.dest (f x) = ⟨a, f ∘ f'⟩ := by rw [hyp, gxeq, PFunctor.map_eq]
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
⊢ dest (f x) = { fst := a, snd := f ∘ f' }
[PROOFSTEP]
rw [hyp, gxeq, PFunctor.map_eq]
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
have h₁ : M.dest (M.corec g x) = ⟨a, M.corec g ∘ f'⟩ := by rw [dest_corec, gxeq, PFunctor.map_eq]
[GOAL]
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
⊢ dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
[PROOFSTEP]
rw [dest_corec, gxeq, PFunctor.map_eq]
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∃ a f_1 f',
    dest (f x) = { fst := a, snd := f_1 } ∧
      dest (M.corec g x) = { fst := a, snd := f' } ∧
        ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ f_1 i = f x' ∧ f' i = M.corec g x'
[PROOFSTEP]
refine' ⟨_, _, _, h₀, h₁, _⟩
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
⊢ ∀ (i : B P a), ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
[PROOFSTEP]
intro i
[GOAL]
case mk
F : PFunctor
X : Type u_1
f✝ : X → Obj F X
P : PFunctor
α : Type u
g : α → Obj P α
f : α → M P
hyp : ∀ (x : α), dest (f x) = f <$> g x
x : α
a✝ : True
a : P.A
f' : B P a → α
gxeq : g x = { fst := a, snd := f' }
h₀ : dest (f x) = { fst := a, snd := f ∘ f' }
h₁ : dest (M.corec g x) = { fst := a, snd := M.corec g ∘ f' }
i : B P a
⊢ ∃ x', (fun x => True) x' ∧ (f ∘ f') i = f x' ∧ (M.corec g ∘ f') i = M.corec g x'
[PROOFSTEP]
exact ⟨f' i, trivial, rfl, rfl⟩