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

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✝²
F : PFunctor
n : ℕ
x : CofixA F n
y : CofixA F (succ n)
h : Agree x y
⊢ truncate y = x
induction n <;> cases x <;> cases y
no goals
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
rfl
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✝¹
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✝²
cases h
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✝¹
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✝¹
simp only [truncate, Function.comp, true_and_iff, eq_self_iff_true, heq_iff_eq]
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
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✝¹
rename_i n_ih a f y h₁
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
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
suffices (fun x => truncate (y x)) = f
  by simp [this]; try (exact HEq.rfl;)
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
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
funext y
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)
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
apply n_ih
no goals
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)
apply h₁
no goals
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
simp [this]