[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : ModularForm Γ k
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
bdd_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSlashInvariantForm
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
bdd_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
bdd_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsBoundedAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_infty' := bdd_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_infty' := bdd_at_infty'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : CuspForm Γ k
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ } =
    (fun f => f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
zero_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toSlashInvariantForm
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝¹
zero_at_infty'✝¹ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝¹ ∣[k] A)
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑toSlashInvariantForm✝
zero_at_infty'✝ : ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑toSlashInvariantForm✝ ∣[k] A)
h :
  (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_infty' := zero_at_infty'✝¹ } =
    (fun f => f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_infty' := zero_at_infty'✝ }
⊢ toSlashInvariantForm✝¹ = toSlashInvariantForm✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty
    (↑({ toFun := ↑f, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑f ∣[k] γ = ↑f) } +
          { toFun := ↑g, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑g ∣[k] γ = ↑g) }) ∣[k]
      A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).add (g.bdd_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑0 ∣[k] A)
[PROOFSTEP]
simpa using zero_form_isBoundedAtImInfty
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : ModularForm Γ k
⊢ MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑(c • f.toSlashInvariantForm)
[PROOFSTEP]
simpa using f.holo'.const_smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(c • f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).const_smul_left (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : ModularForm Γ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(-f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.bdd_at_infty' A).neg
[GOAL]
F : Type u_1
Γ✝ : Subgroup SL(2, ℤ)
k k_1 k_2 : ℤ
Γ : Subgroup SL(2, ℤ)
f : ModularForm Γ k_1
g : ModularForm Γ k_2
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑(SlashInvariantForm.mul f.toSlashInvariantForm g.toSlashInvariantForm) ∣[k_1 + k_2] A)
[PROOFSTEP]
rw [SlashInvariantForm.coe_mul, mul_slash_SL2]
[GOAL]
F : Type u_1
Γ✝ : Subgroup SL(2, ℤ)
k k_1 k_2 : ℤ
Γ : Subgroup SL(2, ℤ)
f : ModularForm Γ k_1
g : ModularForm Γ k_2
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑f.toSlashInvariantForm ∣[k_1] A * ↑g.toSlashInvariantForm ∣[k_2] A)
[PROOFSTEP]
exact (f.bdd_at_infty' A).mul (g.bdd_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (↑1 ∣[0] A)
[PROOFSTEP]
simpa only [SlashInvariantForm.one_coe_eq_one, ModularForm.is_invariant_one] using
  atImInfty.const_boundedAtFilter (1 : ℂ)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f g : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty
    (↑({ toFun := ↑f, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑f ∣[k] γ = ↑f) } +
          { toFun := ↑g, slash_action_eq' := (_ : ∀ (γ : { x // x ∈ Γ }), ↑g ∣[k] γ = ↑g) }) ∣[k]
      A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).add (g.zero_at_infty' A)
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
⊢ ∀ (A : SL(2, ℤ)), IsZeroAtImInfty (↑0 ∣[k] A)
[PROOFSTEP]
simpa using Filter.zero_zeroAtFilter _
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : CuspForm Γ k
⊢ MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) ↑(c • f.toSlashInvariantForm)
[PROOFSTEP]
simpa using f.holo'.const_smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty (↑(c • f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).smul (c • (1 : ℂ))
[GOAL]
F : Type u_1
Γ : Subgroup SL(2, ℤ)
k : ℤ
f : CuspForm Γ k
A : SL(2, ℤ)
⊢ IsZeroAtImInfty (↑(-f.toSlashInvariantForm) ∣[k] A)
[PROOFSTEP]
simpa using (f.zero_at_infty' A).neg


[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
let α := N.mapIso (Γ₂N₂.app P)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
let β := N₂Γ₂.app (N.obj P)
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P) = 𝟙 (N.obj P)
[PROOFSTEP]
symm
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ 𝟙 (N.obj P) = N.map (NatTrans.app Γ₂N₂.hom P) ≫ NatTrans.app N₂Γ₂.hom (N.obj P)
[PROOFSTEP]
change 𝟙 _ = α.hom ≫ β.hom
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ 𝟙 (N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P)) = α.hom ≫ β.hom
[PROOFSTEP]
rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]
[GOAL]
C : Type u_1
inst✝² : Category.{?u.1346, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
α : N.obj ((𝟭 (Karoubi (SimplicialObject C))).obj P) ≅ N.obj ((N₂ ⋙ Γ₂).obj P) := N.mapIso (Γ₂N₂.app P)
β : (Γ₂ ⋙ N₂).obj (N.obj P) ≅ (𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P) := N₂Γ₂.app (N.obj P)
⊢ β.inv ≫ α.inv = 𝟙 ((𝟭 (Karoubi (ChainComplex C ℕ))).obj (N.obj P))
[PROOFSTEP]
exact AlgebraicTopology.DoldKan.identity_N₂_objectwise P


[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq ((π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p))
    ((π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q))
[PROOFSTEP]
simp only [map_eq, ← Path.Homotopic.map_lift]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (↑f x₀) (↑f x₁)) (Path.map p (_ : Continuous ↑f)))
    (Quotient.mk (Path.Homotopic.setoid (↑g x₂) (↑g x₃)) (Path.map q (_ : Continuous ↑g)))
[PROOFSTEP]
apply Path.Homotopic.hpath_hext
[GOAL]
case hp
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ∀ (t : ↑I), ↑(Path.map p (_ : Continuous ↑f)) t = ↑(Path.map q (_ : Continuous ↑g)) t
[PROOFSTEP]
exact hfg
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ↑f x₀ = ↑g x₂
[PROOFSTEP]
convert hfg 0
[GOAL]
case h.e'_2.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₀ = ↑p 0
[PROOFSTEP]
simp only [Path.source]
[GOAL]
case h.e'_3.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₂ = ↑q 0
[PROOFSTEP]
simp only [Path.source]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ ↑f x₁ = ↑g x₃
[PROOFSTEP]
convert hfg 1
[GOAL]
case h.e'_2.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₁ = ↑p 1
[PROOFSTEP]
simp only [Path.target]
[GOAL]
case h.e'_3.h.e'_6
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ x₃ = ↑q 1
[PROOFSTEP]
simp only [Path.target]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ (π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p) =
    hcast (_ : ↑f x₀ = ↑g x₂) ≫ (π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q) ≫ hcast (_ : ↑g x₃ = ↑f x₁)
[PROOFSTEP]
rw [Functor.conj_eqToHom_iff_heq ((πₘ f).map ⟦p⟧) ((πₘ g).map ⟦q⟧) (start_path hfg) (end_path hfg)]
[GOAL]
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), ↑f (↑p t) = ↑g (↑q t)
⊢ HEq ((π.map f).map (Quotient.mk (Path.Homotopic.setoid x₀ x₁) p))
    ((π.map g).map (Quotient.mk (Path.Homotopic.setoid x₂ x₃) q))
[PROOFSTEP]
exact heq_path_of_eq_image hfg
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ (π.map f).map (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p') =
    hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (π.map (uliftMap H)).map
          (prodToProdTopI (𝟙 (fromTop { down := 0 }))
            (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p')) ≫
        hcast (_ : ↑H (0, x₁) = ↑f x₁)
[PROOFSTEP]
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑(uliftMap H) (↑(Path.prod (Path.refl { down := 0 }) p') t)
[PROOFSTEP]
rw [Path.prod_coe]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑(uliftMap H) ((fun t => (↑(Path.refl { down := 0 }) t, ↑p' t)) t)
[PROOFSTEP]
simp_rw [ulift_apply]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑f (↑p' t) = ↑H ((↑(Path.refl { down := 0 }) t).down, ↑p' t)
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ (π.map g).map (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p') =
    hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
      (π.map (uliftMap H)).map
          (prodToProdTopI (𝟙 (fromTop { down := 1 }))
            (Quotient.mk (Path.Homotopic.setoid (fromTop x₀) (fromTop x₁)) p')) ≫
        hcast (_ : ↑H (1, x₁) = ↑g x₁)
[PROOFSTEP]
apply @eq_path_of_eq_image _ _ _ _ H.uliftMap _ _ _ _ _ ((Path.refl (ULift.up _)).prod p')
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑(uliftMap H) (↑(Path.prod (Path.refl { down := 1 }) p') t)
[PROOFSTEP]
rw [Path.prod_coe]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑(uliftMap H) ((fun t => (↑(Path.refl { down := 1 }) t, ↑p' t)) t)
[PROOFSTEP]
simp_rw [ulift_apply]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
p' : Path (fromTop x₀) (fromTop x₁)
⊢ ∀ (t : ↑I), ↑g (↑p' t) = ↑H ((↑(Path.refl { down := 1 }) t).down, ↑p' t)
[PROOFSTEP]
simp
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x) =
    hcast (_ : ↑f x = ↑H (0, x)) ≫
      (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x)) ≫ hcast (_ : ↑H (1, x) = ↑g x)
[PROOFSTEP]
dsimp only [prodToProdTopI, uhpath01, hcast]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x) =
    eqToHom (_ : ↑f x = ↑H (0, x)) ≫
      (π.map (uliftMap H)).map
          ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
            (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
              𝟙 x)) ≫
        eqToHom (_ : ↑H (1, x) = ↑g x)
[PROOFSTEP]
refine' (@Functor.conj_eqToHom_iff_heq (πₓ Y) _ _ _ _ _ _ _ _ (H.apply_one x).symm).mpr _
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x))
    ((π.map (uliftMap H)).map
      ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
        (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
          𝟙 x)))
[PROOFSTEP]
simp only [id_eq_path_refl, prodToProdTop_map, Path.Homotopic.prod_lift, map_eq, ← Path.Homotopic.map_lift]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ HEq (Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x)) (fromTop (↑g x))) (evalAt H x))
    (Path.Homotopic.Quotient.mapFn
      ((prodToProdTop (TopCat.of (ULift ↑I)) X).map
        (Quotient.mk (Path.Homotopic.setoid (fromTop { down := 0 }) (fromTop { down := 1 })) unitInterval.upath01,
          Quotient.mk (Path.Homotopic.setoid x x) (Path.refl x)))
      (uliftMap H))
[PROOFSTEP]
apply Path.Homotopic.hpath_hext
[GOAL]
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
⊢ ∀ (t : ↑I),
    ↑(evalAt H x) t =
      ↑((fun q => Path.map q (_ : Continuous ↑(uliftMap H))) (Path.prod unitInterval.upath01 (Path.refl x))) t
[PROOFSTEP]
intro
[GOAL]
case hp
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
x : ↑X
t✝ : ↑I
⊢ ↑(evalAt H x) t✝ =
    ↑((fun q => Path.map q (_ : Continuous ↑(uliftMap H))) (Path.prod unitInterval.upath01 (Path.refl x))) t✝
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (π.map f).map p ≫ Quotient.mk (Path.Homotopic.setoid ((π.map f).obj (fromTop x₁)) (↑g x₁)) (evalAt H x₁) =
      diagonalPath' H p ∧
    Quotient.mk (Path.Homotopic.setoid (fromTop (↑f x₀)) (↑g x₀)) (evalAt H x₀) ≫ (π.map g).map p = diagonalPath' H p
[PROOFSTEP]
rw [H.apply_zero_path, H.apply_one_path, H.evalAt_eq]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        Quotient.mk (Path.Homotopic.setoid ((π.map f).obj (fromTop x₁)) (↑g x₁)) (evalAt H x₁) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x₀)) ≫ hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
erw [H.evalAt_eq]
  -- Porting note: `rw` didn't work, so using `erw`
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₁))) ≫
            hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI uhpath01 (𝟙 x₀)) ≫ hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
dsimp only [prodToProdTopI]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
        hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
            hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
      diagonalPath' H p ∧
    (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
            hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
        hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
            hcast (_ : ↑H (1, x₁) = ↑g x₁) =
      diagonalPath' H p
[PROOFSTEP]
constructor
[GOAL]
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
          hcast (_ : ↑H (0, x₁) = ↑f x₁)) ≫
      hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁))) ≫
          hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 =>
  rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    hcast (_ : ↑H (0, x₁) = ↑f x₁) ≫ hcast (_ : ↑f (fromTop x₁) = ↑H (0, fromTop x₁))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
  -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case left
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (((π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
            𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁)))) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))) ≫
        hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁)) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 0 }), p)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 0 }, x₁))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 (fromTop x₁)))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, fromTop x₁) = ↑g (fromTop x₁))
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
          hcast (_ : ↑H (1, x₀) = ↑g x₀)) ≫
      hcast (_ : ↑g x₀ = ↑H (1, x₀)) ≫
        (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p)) ≫
          hcast (_ : ↑H (1, x₁) = ↑g x₁) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 =>
  rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
    -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    hcast (_ : ↑H (1, x₀) = ↑g x₀) ≫ hcast (_ : ↑g x₀ = ↑H (1, x₀))
case a.a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
rw [eqToHom_trans, eqToHom_refl]
  -- Porting note: this ↓ `simp` didn't do this
[GOAL]
case right
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ hcast (_ : ↑f x₀ = ↑H (0, x₀)) ≫
      (((π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
            𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀)))) ≫
          (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))) ≫
        hcast (_ : ↑H (1, x₁) = ↑g x₁) =
    diagonalPath' H p
[PROOFSTEP]
slice_lhs 2 4 => simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (uhpath01, 𝟙 x₀)) ≫
    𝟙 ((π.map (uliftMap H)).obj ((prodToProdTop (TopCat.of (ULift ↑I)) X).obj ({ down := 1 }, x₀))) ≫
      (π.map (uliftMap H)).map ((prodToProdTop (TopCat.of (ULift ↑I)) X).map (𝟙 (fromTop { down := 1 }), p))
case a.a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑H (1, x₁) = ↑g x₁)
case a
X Y : TopCat
f g : C(↑X, ↑Y)
H : Homotopy f g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
| hcast (_ : ↑f x₀ = ↑H (0, x₀))
[PROOFSTEP]
simp [← CategoryTheory.Functor.map_comp]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
x y : ↑(π.obj X)
p : x ⟶ y
⊢ (π.map f).map p ≫
      (fun x =>
          Quotient.mk (Path.Homotopic.setoid ((π.map f).obj x) ((π.map g).obj x)) (ContinuousMap.Homotopy.evalAt H x))
        y =
    (fun x =>
          Quotient.mk (Path.Homotopic.setoid ((π.map f).obj x) ((π.map g).obj x)) (ContinuousMap.Homotopy.evalAt H x))
        x ≫
      (π.map g).map p
[PROOFSTEP]
erw [(H.eq_diag_path p).1, (H.eq_diag_path p).2]
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
⊢ IsIso (homotopicMapsNatIso H)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app
[GOAL]
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ ↑(π.obj X) ≌ ↑(π.obj Y)
[PROOFSTEP]
apply CategoryTheory.Equivalence.mk (πₘ hequiv.toFun : πₓ X ⥤ πₓ Y) (πₘ hequiv.invFun : πₓ Y ⥤ πₓ X)
[GOAL]
case η
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟭 ↑(π.obj X) ≅ π.map hequiv.toFun ⋙ π.map hequiv.invFun
[PROOFSTEP]
simp only [Grpd.hom_to_functor, Grpd.id_to_functor]
[GOAL]
case ε
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun ≅ 𝟭 ↑(π.obj Y)
[PROOFSTEP]
simp only [Grpd.hom_to_functor, Grpd.id_to_functor]
[GOAL]
case η
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj X) ≅ π.map hequiv.toFun ⋙ π.map hequiv.invFun
[PROOFSTEP]
convert (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm
[GOAL]
case h.e'_3
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj X) = π.map (ContinuousMap.id ↑X)
case h.e'_4
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.toFun ⋙ π.map hequiv.invFun = π.map (ContinuousMap.comp hequiv.invFun hequiv.toFun)
[PROOFSTEP]
exacts [((π).map_id X).symm, ((π).map_comp _ _).symm]
[GOAL]
case ε
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun ≅ 𝟙 (π.obj Y)
[PROOFSTEP]
convert asIso (homotopicMapsNatIso hequiv.right_inv.some)
[GOAL]
case h.e'_3
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ π.map hequiv.invFun ⋙ π.map hequiv.toFun = π.map (ContinuousMap.comp hequiv.toFun hequiv.invFun)
case h.e'_4
X Y : TopCat
f g : C(↑X, ↑Y)
H : ContinuousMap.Homotopy f g
hequiv : ↑X ≃ₕ ↑Y
⊢ 𝟙 (π.obj Y) = π.map (ContinuousMap.id ↑Y)
[PROOFSTEP]
exacts [((π).map_comp _ _).symm, ((π).map_id Y).symm]


[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ HomologicalComplex.Hom.f (P Nat.zero) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
rfl
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
hq : HomologicalComplex.Hom.f (P q) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
⊢ HomologicalComplex.Hom.f (P (Nat.succ q)) 0 = 𝟙 (HomologicalComplex.X K[X] 0)
[PROOFSTEP]
simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f, HomologicalComplex.id_f, id_comp, hq,
  Hσ_eq_zero, add_zero]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + Q q = 𝟙 K[X]
[PROOFSTEP]
rw [Q]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q (q + 1) = Q q - P q ≫ Hσ q
[PROOFSTEP]
simp only [Q, P_succ, comp_add, comp_id]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] - (P q + P q ≫ Hσ q) = 𝟙 K[X] - P q - P q ≫ Hσ q
[PROOFSTEP]
abel
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (Q q) 0 = 0
[PROOFSTEP]
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
⊢ HomologicalComplex.Hom.f (P 0) (n + 1) ≫ δ X (Fin.succ j) = 0
[PROOFSTEP]
exfalso
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
⊢ False
[PROOFSTEP]
have hj₂ := Fin.is_lt j
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ ↑j + 0
hj₂ : ↑j < n + 1
⊢ False
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) (HomologicalComplex.Hom.f (P (q + 1)) (n + 1))
[PROOFSTEP]
simp only [P_succ]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HigherFacesVanish (q + 1) (HomologicalComplex.Hom.f (P q ≫ (𝟙 K[X] + Hσ q)) (n + 1))
[PROOFSTEP]
exact (of_P q n).induction
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v : HigherFacesVanish q φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (P Nat.zero) (n + 1) = φ
[PROOFSTEP]
simp only [P_zero]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q φ
v : HigherFacesVanish Nat.zero φ
⊢ φ ≫ HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1) = φ
[PROOFSTEP]
apply comp_id
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (P (Nat.succ q)) (n + 1) = φ
[PROOFSTEP]
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, ← assoc, hq v.of_succ,
  add_right_eq_self]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
by_cases hqn : n < q
[GOAL]
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
exact v.of_succ.comp_Hσ_eq_zero hqn
[GOAL]
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
obtain ⟨a, ha⟩ := Nat.le.dest (not_lt.mp hqn)
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
have hnaq : n = a + q := by linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
⊢ n = a + q
[PROOFSTEP]
linarith
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1) = 0
[PROOFSTEP]
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
[PROOFSTEP]
have eq :=
  v ⟨a, by linarith⟩
    (by
      simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
      rfl)
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a < n + 1
[PROOFSTEP]
linarith
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ n + 1 ≤ ↑{ val := a, isLt := (_ : a < n + 1) } + Nat.succ q
[PROOFSTEP]
simp only [hnaq, Nat.succ_eq_add_one, add_assoc]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)
[PROOFSTEP]
rfl
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X (Fin.succ { val := a, isLt := (_ : a < n + 1) }) = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
[PROOFSTEP]
simp only [Fin.succ_mk] at eq
[GOAL]
case neg.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q✝ : ℕ
φ : Y ⟶ X.obj (op [n + 1])
v✝ : HigherFacesVanish q✝ φ
q : ℕ
hq : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (Nat.succ q) φ
hqn : ¬n < q
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) } = 0
⊢ (φ ≫ δ X { val := a + 1, isLt := (_ : Nat.succ a < Nat.succ (n + 1)) }) ≫
      σ X { val := a, isLt := (_ : a < Nat.succ n) } =
    0
[PROOFSTEP]
simp only [eq, zero_comp]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
[PROOFSTEP]
intro hφ
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q φ
[PROOFSTEP]
rw [← hφ]
[GOAL]
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
[PROOFSTEP]
apply HigherFacesVanish.of_comp
[GOAL]
case mp.v
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish q (HomologicalComplex.Hom.f (P q) (n + 1))
[PROOFSTEP]
apply HigherFacesVanish.of_P
[GOAL]
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n q : ℕ
φ : Y ⟶ X.obj (op [n + 1])
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
[PROOFSTEP]
exact HigherFacesVanish.comp_P_eq_self
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q) n ≫ HomologicalComplex.Hom.f (P q) n = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
rcases n with (_ | n)
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ HomologicalComplex.Hom.f (P q) Nat.zero ≫ HomologicalComplex.Hom.f (P q) Nat.zero =
    HomologicalComplex.Hom.f (P q) Nat.zero
[PROOFSTEP]
rw [P_f_0_eq q, comp_id]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q) (Nat.succ n) ≫ HomologicalComplex.Hom.f (P q) (Nat.succ n) =
    HomologicalComplex.Hom.f (P q) (Nat.succ n)
[PROOFSTEP]
exact (HigherFacesVanish.of_P q n).comp_P_eq_self
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q ≫ P q = P q
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (P q ≫ P q) n = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
exact P_f_idem q n
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ Q q ≫ Q q = Q q
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q n : ℕ
⊢ HomologicalComplex.Hom.f (Q q ≫ Q q) n = HomologicalComplex.Hom.f (Q q) n
[PROOFSTEP]
exact Q_f_idem q n
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P Nat.zero) x✝ =
    (fun X => P Nat.zero) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
dsimp [alternatingFaceMapComplex]
[GOAL]
case zero
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ AlternatingFaceMapComplex.map f ≫ P 0 = P 0 ≫ AlternatingFaceMapComplex.map f
[PROOFSTEP]
simp only [P_zero, id_comp, comp_id]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ (alternatingFaceMapComplex C).map f ≫ (fun X => P (Nat.succ q)) x✝ =
    (fun X => P (Nat.succ q)) x✝¹ ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ (alternatingFaceMapComplex C).map f ≫ Hσ q =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
erw [(natTransHσ q).naturality f]
[GOAL]
case succ
C : Type u_1
inst✝¹ : Category.{?u.247062, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
q : ℕ
hq : (alternatingFaceMapComplex C).map f ≫ (fun X => P q) x✝ = (fun X => P q) x✝¹ ≫ (alternatingFaceMapComplex C).map f
⊢ P q ≫ (alternatingFaceMapComplex C).map f +
      P q ≫ NatTrans.app (natTransHσ q) x✝¹ ≫ (alternatingFaceMapComplex C).map f =
    P q ≫ (alternatingFaceMapComplex C).map f + P q ≫ Hσ q ≫ (alternatingFaceMapComplex C).map f
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ HomologicalComplex.Hom.f (Q q) n =
    HomologicalComplex.Hom.f (Q q) n ≫ NatTrans.app f (op [n])
[PROOFSTEP]
simp only [Q, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, comp_sub, P_f_naturality, sub_comp, sub_left_inj]
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ 𝟙 (HomologicalComplex.X K[Y] n) = 𝟙 (HomologicalComplex.X K[X] n) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X✝ : SimplicialObject C
q n : ℕ
X Y : SimplicialObject C
f : X ⟶ Y
⊢ NatTrans.app f (op [n]) ≫ 𝟙 (Y.obj (op [n])) = 𝟙 (X.obj (op [n])) ≫ NatTrans.app f (op [n])
[PROOFSTEP]
simp only [comp_id, id_comp]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
[PROOFSTEP]
induction' q with q hq
[GOAL]
case zero
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (P Nat.zero) n) = HomologicalComplex.Hom.f (P Nat.zero) n
[PROOFSTEP]
simp only [P_zero]
[GOAL]
case zero
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (𝟙 K[X]) n) = HomologicalComplex.Hom.f (𝟙 K[((whiskering C D).obj G).obj X]) n
[PROOFSTEP]
apply G.map_id
[GOAL]
case succ
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
n q : ℕ
hq : G.map (HomologicalComplex.Hom.f (P q) n) = HomologicalComplex.Hom.f (P q) n
⊢ G.map (HomologicalComplex.Hom.f (P (Nat.succ q)) n) = HomologicalComplex.Hom.f (P (Nat.succ q)) n
[PROOFSTEP]
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply, comp_id, Functor.map_add,
  Functor.map_comp, hq, map_Hσ]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (HomologicalComplex.Hom.f (Q q) n) = HomologicalComplex.Hom.f (Q q) n
[PROOFSTEP]
rw [← add_right_inj (G.map ((P q : K[X] ⟶ _).f n)), ← G.map_add, map_P G X q n, P_add_Q_f, P_add_Q_f]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Preadditive C
X✝ : SimplicialObject C
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : Functor.Additive G
X : SimplicialObject C
q n : ℕ
⊢ G.map (𝟙 (X.obj (op [n]))) = 𝟙 ((((whiskering C D).obj G).obj X).obj (op [n]))
[PROOFSTEP]
apply G.map_id


[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₁ hF).counitIso = equivalence₁CounitIso hF
[PROOFSTEP]
ext Y
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (equivalence₁ hF).counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
dsimp [equivalence₁]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (Functor.asEquivalence F).counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
unfold Functor.asEquivalence
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app (Equivalence.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).counitIso.hom
      Y =
    NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
dsimp [equivalence₀, IsEquivalence.inverse, IsEquivalence.ofEquivalence]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.10521, u_3} B
inst✝ : Category.{u_5, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y : B'
⊢ NatTrans.app IsEquivalence.counitIso.hom Y = NatTrans.app (equivalence₁CounitIso hF).hom Y
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₁ hF).unitIso = equivalence₁UnitIso hF
[PROOFSTEP]
ext X
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₁ hF).unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
dsimp [equivalence₁]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (Functor.asEquivalence F).unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
unfold Functor.asEquivalence
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (Equivalence.mk' F (IsEquivalence.inverse F) IsEquivalence.unitIso IsEquivalence.counitIso).unitIso.hom
      X =
    NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
dsimp [NatIso.hcomp, IsEquivalence.ofEquivalence]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{?u.21328, u_3} B
inst✝ : Category.{u_6, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app IsEquivalence.unitIso.hom X = NatTrans.app (equivalence₁UnitIso hF).hom X
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF
[PROOFSTEP]
ext Y'
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y' : B
⊢ NatTrans.app (equivalence₂ eB hF).counitIso.hom Y' = NatTrans.app (equivalence₂CounitIso eB hF).hom Y'
[PROOFSTEP]
dsimp [equivalence₂, Iso.refl]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
Y' : B
⊢ eB.inverse.map (NatTrans.app (equivalence₁ hF).counitIso.hom (eB.functor.obj Y')) ≫ NatTrans.app eB.unitIso.inv Y' =
    NatTrans.app (equivalence₂CounitIso eB hF).hom Y'
[PROOFSTEP]
simp only [equivalence₁CounitIso_eq, equivalence₂CounitIso_hom_app, equivalence₁CounitIso_hom_app, Functor.map_comp,
  assoc]
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF
[PROOFSTEP]
ext X
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X = NatTrans.app (equivalence₂UnitIso eB hF).hom X
[PROOFSTEP]
dsimp [equivalence₂]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app (equivalence₁ hF).unitIso.hom X ≫
      (equivalence₁ hF).inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)) =
    NatTrans.app (equivalence₂UnitIso eB hF).hom X
[PROOFSTEP]
simp only [equivalence₂UnitIso_hom_app, equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, assoc,
  NatIso.cancel_natIso_hom_left]
[GOAL]
case w.w.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
X : A
⊢ NatTrans.app eA.unitIso.hom X ≫
      eA.inverse.map (NatTrans.app e'.unitIso.hom (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (NatTrans.app hF.hom X)) ≫
          (equivalence₁ hF).inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)) =
    NatTrans.app eA.unitIso.hom X ≫
      eA.inverse.map (NatTrans.app e'.unitIso.hom (eA.functor.obj X)) ≫
        eA.inverse.map (e'.inverse.map (NatTrans.app hF.hom X)) ≫
          eA.inverse.map (e'.inverse.map (NatTrans.app eB.counitIso.inv (F.obj X)))
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.46977, u_1} A
inst✝² : Category.{?u.46981, u_2} A'
inst✝¹ : Category.{?u.46985, u_3} B
inst✝ : Category.{?u.46989, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ IsEquivalence G
[PROOFSTEP]
refine' IsEquivalence.ofIso _ (IsEquivalence.ofEquivalence (equivalence₂ eB hF).symm)
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.46977, u_1} A
inst✝² : Category.{?u.46981, u_2} A'
inst✝¹ : Category.{?u.46985, u_3} B
inst✝ : Category.{?u.46989, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
⊢ (CategoryTheory.Equivalence.symm (equivalence₂ eB hF)).functor ≅ G
[PROOFSTEP]
calc
  eB.functor ⋙ e'.inverse ⋙ eA.inverse ≅ (eB.functor ⋙ e'.inverse) ⋙ eA.inverse := Iso.refl _
  _ ≅ (G ⋙ eA.functor) ⋙ eA.inverse := (isoWhiskerRight hG _)
  _ ≅ G ⋙ 𝟭 A := (isoWhiskerLeft _ eA.unitIso.symm)
  _ ≅ G := Functor.rightUnitor G
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{?u.52568, u_1} A
inst✝² : Category.{?u.52572, u_2} A'
inst✝¹ : Category.{?u.52576, u_3} B
inst✝ : Category.{?u.52580, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
⊢ (G ⋙ eA.functor) ⋙ e'.functor ≅ G ⋙ eA.functor ⋙ e'.functor
[PROOFSTEP]
rfl
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso = equivalenceCounitIso η
[PROOFSTEP]
ext1
[GOAL]
case w
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso.hom = (equivalenceCounitIso η).hom
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case w.app
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
⊢ (equivalence hF hG).counitIso.hom.app = (equivalenceCounitIso η).hom.app
[PROOFSTEP]
ext Y
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app (equivalence hF hG).counitIso.hom Y = NatTrans.app (equivalenceCounitIso η).hom Y
[PROOFSTEP]
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app IsEquivalence.unitIso.inv Y = NatTrans.app (equivalenceCounitIso η).hom Y
[PROOFSTEP]
rw [equivalenceCounitIso_hom_app, IsEquivalence.ofIso_unitIso_inv_app]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ (IsEquivalence.inverse (equivalence₂ eB hF).inverse).map
        (NatTrans.app
          (((Iso.refl (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ≪≫ isoWhiskerRight hG eA.inverse) ≪≫
                isoWhiskerLeft G eA.unitIso.symm) ≪≫
              Functor.rightUnitor G).inv
          Y) ≫
      NatTrans.app IsEquivalence.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (F.map
          (𝟙 (G.obj Y) ≫
            NatTrans.app eA.unitIso.hom (G.obj Y) ≫
              eA.inverse.map (NatTrans.app hG.inv Y) ≫ 𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))))) ≫
      NatTrans.app (equivalence₂ eB hF).counitIso.hom Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
simp only [comp_id, id_comp, F.map_comp, assoc, equivalence₂CounitIso_eq, equivalence₂CounitIso_hom_app, ←
  eB.inverse.map_comp_assoc, ← τ₀_hom_app, hη, τ₁_hom_app]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (F.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
          F.map (eA.inverse.map (NatTrans.app hG.inv Y)) ≫
            NatTrans.app hF.inv (eA.inverse.obj (e'.inverse.obj (eB.functor.obj Y))) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
erw [hF.inv.naturality_assoc, hF.inv.naturality_assoc]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (NatTrans.app hF.inv (G.obj Y) ≫
          (eA.functor ⋙ e'.functor).map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            (eA.functor ⋙ e'.functor).map (eA.inverse.map (NatTrans.app hG.inv Y)) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ eB.inverse.map
        (NatTrans.app hF.inv (G.obj Y) ≫
          e'.functor.map (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y))) ≫
            e'.functor.map (eA.functor.map (eA.inverse.map (NatTrans.app hG.inv Y))) ≫
              e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
                e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y) ≫
      NatTrans.app eB.unitIso.inv Y =
    eB.inverse.map (NatTrans.app η.hom Y) ≫ NatTrans.app eB.unitIso.inv Y
[PROOFSTEP]
congr 2
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y))) ≫
        e'.functor.map (eA.functor.map (eA.inverse.map (NatTrans.app hG.inv Y))) ≫
          e'.functor.map (NatTrans.app eA.counitIso.hom (e'.inverse.obj (eB.functor.obj Y))) ≫
            e'.functor.map (NatTrans.app hG.hom Y) ≫ NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
simp only [assoc, ← e'.functor.map_comp_assoc, Equivalence.fun_inv_map, Iso.inv_hom_id_app_assoc, hG.inv_hom_id_app]
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            NatTrans.app (Equivalence.counit eA) (eA.functor.obj (G.obj Y)) ≫ 𝟙 ((G ⋙ eA.functor).obj Y)) ≫
        NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h.e_a.e_a
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_6, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_5, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
Y : B
⊢ NatTrans.app hF.inv (G.obj Y) ≫
      e'.functor.map
          (eA.functor.map (NatTrans.app eA.unitIso.hom (G.obj Y)) ≫
            NatTrans.app (Equivalence.counit eA) (eA.functor.obj (G.obj Y)) ≫ 𝟙 (eA.functor.obj (G.obj Y))) ≫
        NatTrans.app hF.hom (G.obj Y) ≫ NatTrans.app η.hom Y =
    NatTrans.app η.hom Y
[PROOFSTEP]
rw [comp_id, eA.functor_unitIso_comp, e'.functor.map_id, id_comp, hF.inv_hom_id_app_assoc]
[GOAL]
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso = equivalenceUnitIso hG ε
[PROOFSTEP]
ext1
[GOAL]
case w
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom = (equivalenceUnitIso hG ε).hom
[PROOFSTEP]
apply NatTrans.ext
[GOAL]
case w.app
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
⊢ (equivalence hF hG).unitIso.hom.app = (equivalenceUnitIso hG ε).hom.app
[PROOFSTEP]
ext X
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence hF hG).unitIso.hom X = NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
dsimp [equivalence, Functor.asEquivalence, IsEquivalence.ofEquivalence, IsEquivalence.inverse]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app IsEquivalence.counitIso.inv X = NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
rw [IsEquivalence.ofIso_counitIso_inv_app]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app IsEquivalence.counitIso.inv X ≫
      NatTrans.app
        (((Iso.refl (eB.functor ⋙ e'.inverse ⋙ eA.inverse) ≪≫ isoWhiskerRight hG eA.inverse) ≪≫
              isoWhiskerLeft G eA.unitIso.symm) ≪≫
            Functor.rightUnitor G).hom
        ((IsEquivalence.inverse (equivalence₂ eB hF).inverse).obj X) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
dsimp
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X ≫
      ((𝟙 (eA.inverse.obj (e'.inverse.obj (eB.functor.obj (eB.inverse.obj (F.obj X))))) ≫
            eA.inverse.map (NatTrans.app hG.hom (eB.inverse.obj (F.obj X)))) ≫
          NatTrans.app eA.unitIso.inv (G.obj (eB.inverse.obj (F.obj X)))) ≫
        𝟙 (G.obj (eB.inverse.obj (F.obj X))) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
erw [id_comp, comp_id]
[GOAL]
case w.app.h
A : Type u_1
A' : Type u_2
B : Type u_3
B' : Type u_4
inst✝³ : Category.{u_5, u_1} A
inst✝² : Category.{u_7, u_2} A'
inst✝¹ : Category.{u_6, u_3} B
inst✝ : Category.{u_8, u_4} B'
eA : A ≌ A'
eB : B ≌ B'
e' : A' ≌ B'
F : A ⥤ B'
hF : eA.functor ⋙ e'.functor ≅ F
G : B ⥤ A
hG : eB.functor ⋙ e'.inverse ≅ G ⋙ eA.functor
η : G ⋙ F ≅ eB.functor
hη : τ₀ = τ₁ hF hG η
ε : eA.functor ≅ F ⋙ e'.inverse
hε : υ hF = ε
X : A
⊢ NatTrans.app (equivalence₂ eB hF).unitIso.hom X ≫
      eA.inverse.map (NatTrans.app hG.hom (eB.inverse.obj (F.obj X))) ≫
        NatTrans.app eA.unitIso.inv (G.obj (eB.inverse.obj (F.obj X))) =
    NatTrans.app (equivalenceUnitIso hG ε).hom X
[PROOFSTEP]
simp only [equivalence₂UnitIso_eq eB hF, equivalence₂UnitIso_hom_app, assoc, equivalenceUnitIso_hom_app, ←
  eA.inverse.map_comp_assoc, ← hε, υ_hom_app]


[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
let F : SimplicialObject A ⥤ _ := Idempotents.DoldKan.N
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
let hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
letI : IsEquivalence (N : SimplicialObject A ⥤ _) := IsEquivalence.ofIso comparisonN.symm hF
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.183203, u_1} A
inst✝ : Abelian A
F : SimplicialObject A ⥤ ChainComplex A ℕ := Idempotents.DoldKan.N
hF : IsEquivalence F := IsEquivalence.ofEquivalence Idempotents.DoldKan.equivalence
this : IsEquivalence N := IsEquivalence.ofIso comparisonN.symm hF
⊢ SimplicialObject A ≌ ChainComplex A ℕ
[PROOFSTEP]
exact N.asEquivalence