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)
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))
suffices ∀ n, head' (x (succ n)) = head' (x 1) by simp [this]
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)
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)
clear m n
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)
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)
intro n
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)
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)
cases' h₀ : x (succ n) with _ i₀ f₀
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₁)
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)
cases' h₁ : x 1 with _ i₁ f₁
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₁
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₁)
dsimp only [head']
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₁

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₁
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₁
induction' n with n n_ih
no goals
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))
simp [this]
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₁
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₁
rw [h₁] at h₀
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₀
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₁
cases h₀
no goals
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₀
trivial
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₁
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₁
have H := Hconsistent (succ n)
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₁
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₁
cases' h₂ : x (succ n) with _ i₂ f₂
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₁
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₁
rw [h₀, h₂] at H
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₀)
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₁
apply n_ih (truncate ∘ f₀)
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₀)
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₀)
rw [h₂]
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₀)
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₀)
cases' H with _ _ _ _ _ _ hagree
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₀
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₀)
congr
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
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₀
funext j
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)
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
dsimp only [comp_apply]
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)
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)
rw [truncate_eq_of_agree]
no goals
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)
apply hagree