[GOAL]
α : Type u_1
inst✝ : StrictOrderedSemiring α
n : ℕ
⊢ ↑n < ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
α : Type u_1
inst✝ : StrictOrderedSemiring α
n : ℕ
⊢ ↑n < ↑n + 1
[PROOFSTEP]
apply lt_add_one


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ ↑f a
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ ↑f 0 ≤ ↑f a
[PROOFSTEP]
exact OrderHomClass.mono _ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ 0
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommMonoid α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : OrderAddMonoidHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ ↑f a ≤ ↑f 0
[PROOFSTEP]
exact OrderHomClass.mono _ ha
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → 0 ≤ ↑f a
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : Monotone ↑f
a : α
⊢ 0 ≤ a → ↑f 0 ≤ ↑f a
[PROOFSTEP]
apply h
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
rw [← sub_add_cancel b a, map_add f]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : OrderedAddCommGroup α
inst✝¹ : OrderedAddCommMonoid β
inst✝ : AddMonoidHomClass F α β
f : F
h : ∀ (a : α), 0 ≤ a → 0 ≤ ↑f a
a b : α
hl : a ≤ b
⊢ ↑f a ≤ ↑f (b - a) + ↑f a
[PROOFSTEP]
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
⊢ StrictMono ↑f ↔ ∀ (a : α), 0 < a → 0 < ↑f a
[PROOFSTEP]
refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → 0 < ↑f a
[PROOFSTEP]
rw [← map_zero f]
[GOAL]
case refine_1
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : StrictMono ↑f
a : α
⊢ 0 < a → ↑f 0 < ↑f a
[PROOFSTEP]
apply h
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f b
[PROOFSTEP]
rw [← sub_add_cancel b a, map_add f]
[GOAL]
case refine_2
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OrderedAddCommGroup α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : AddMonoidHomClass F α β
f : F
inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x < x_1
h : ∀ (a : α), 0 < a → 0 < ↑f a
a b : α
hl : a < b
⊢ ↑f a < ↑f (b - a) + ↑f a
[PROOFSTEP]
exact lt_add_of_pos_left _ (h _ <| sub_pos.2 hl)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ g : α →*o β
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
monotone'✝ : Monotone (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g : α →*o β
toFun✝¹ : α → β
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } x *
        OneHom.toFun { toFun := toFun✝¹, map_one' := map_one'✝¹ } y
monotone'✝¹ : Monotone (↑{ toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := toFun✝, map_one' := map_one'✝ } y
monotone'✝ : Monotone (↑{ toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ }
⊢ { toMonoidHom := { toOneHom := { toFun := toFun✝¹, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
      monotone' := monotone'✝¹ } =
    { toMonoidHom := { toOneHom := { toFun := toFun✝, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
⊢ { toMonoidHom := ↑f, monotone' := h } = f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g f : α →*o β
h : Monotone (↑↑f).toFun
a✝ : α
⊢ ↑{ toMonoidHom := ↑f, monotone' := h } a✝ = ↑f a✝
[PROOFSTEP]
rfl
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : f.toMonoidHom = g.toMonoidHom
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g✝ f g : α →*o β
h : toOrderHom f = toOrderHom g
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f✝ g : α →*o β
g₁ g₂ : β →*o γ
f : α →*o β
hf : Surjective ↑f
x✝ : g₁ = g₂
⊢ comp g₁ f = comp g₂ f
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : MulOneClass γ
inst✝ : MulOneClass δ
f g✝ : α →*o β
g : β →*o γ
f₁ f₂ : α →*o β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ g : α →*₀o β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } x *
        ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } y
monotone'✝ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ } =
    (fun f => f.toFun) g
⊢ {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g : α →*₀o β
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } x *
        ZeroHom.toFun { toFun := toFun✝¹, map_zero' := map_zero'✝¹ } y
monotone'✝¹ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹,
          map_mul' := map_mul'✝¹ }).toFun
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } (x * y) =
      ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } x *
        ZeroHom.toFun { toFun := toFun✝, map_zero' := map_zero'✝ } y
monotone'✝ :
  Monotone
    (↑{ toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun
h :
  (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹,
            map_mul' := map_mul'✝¹ },
        monotone' := monotone'✝¹ } =
    (fun f => f.toFun)
      {
        toMonoidWithZeroHom :=
          { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
        monotone' := monotone'✝ }
⊢ {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ },
      monotone' := monotone'✝¹ } =
    {
      toMonoidWithZeroHom :=
        { toZeroHom := { toFun := toFun✝, map_zero' := map_zero'✝ }, map_one' := map_one'✝, map_mul' := map_mul'✝ },
      monotone' := monotone'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : toOrderMonoidHom f = toOrderMonoidHom g
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g✝ f g : α →*₀o β
h : f.toMonoidWithZeroHom = g.toMonoidWithZeroHom
⊢ ∀ (a : α), ↑f a = ↑g a
[PROOFSTEP]
convert FunLike.ext_iff.1 h using 0
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f✝ g : α →*₀o β
g₁ g₂ : β →*₀o γ
f : α →*₀o β
hf : Surjective ↑f
x✝ : g₁ = g₂
⊢ comp g₁ f = comp g₂ f
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : Preorder δ
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
f g✝ : α →*₀o β
g : β →*₀o γ
f₁ f₂ : α →*₀o β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
hα : Preorder α
hα' : MulZeroOneClass α
hβ : Preorder β
hβ' : MulZeroOneClass β
f : α →*₀o β
⊢ f.toMonoidWithZeroHom = ↑f
[PROOFSTEP]
rfl


[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
ι✝ : Type ?u.1725
v : ComplexShape ι✝
⊢ Category.{?u.1722, max (max u v) ?u.1725} (HomotopyCategory V v)
[PROOFSTEP]
dsimp only [HomotopyCategory]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
ι✝ : Type ?u.1725
v : ComplexShape ι✝
⊢ Category.{?u.1722, max (max u v) ?u.1725} (CategoryTheory.Quotient (homotopic V v))
[PROOFSTEP]
infer_instance
  -- TODO the homotopy_category is preadditive
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
⊢ Homotopy (Quot.out ((quotient V c).map f)) f
[PROOFSTEP]
apply homotopyOfEq
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (quotient V c).map (Quot.out ((quotient V c).map f)) = (quotient V c).map f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomotopyCategory V c
f : C ⟶ D
g : D ⟶ E
⊢ (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)
[PROOFSTEP]
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.hom ≫ f.inv) = (quotient V c).map (𝟙 C)
[PROOFSTEP]
exact eq_of_homotopy _ _ f.homotopyHomInvId
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)
[PROOFSTEP]
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.inv ≫ f.hom) = (quotient V c).map (𝟙 D)
[PROOFSTEP]
exact eq_of_homotopy _ _ f.homotopyInvHomId
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.hom ≫ Quot.out i.inv) = (quotient V c).map (𝟙 C)
[PROOFSTEP]
rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.inv ≫ Quot.out i.hom) = (quotient V c).map (𝟙 D)
[PROOFSTEP]
rw [quotient_map_out_comp_out, i.inv_hom_id, (quotient V c).map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝³ : Category.{?u.46796, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
c : ComplexShape ι
⊢ ∀ ⦃X Y : HomotopyCategory V c⦄ (f : X ⟶ Y),
    (Functor.mapHomotopyCategory F c).map f ≫
        (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) Y =
      (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) X ≫
        (Functor.mapHomotopyCategory G c).map f
[PROOFSTEP]
rintro ⟨C⟩ ⟨D⟩ ⟨f : C ⟶ D⟩
[GOAL]
case mk.mk.mk
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝³ : Category.{?u.46796, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : { as := C } ⟶ { as := D }
f : C ⟶ D
⊢ (Functor.mapHomotopyCategory F c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f) ≫
      (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) { as := D } =
    (fun C => (HomotopyCategory.quotient W c).map (app (mapHomologicalComplex α c) C.as)) { as := C } ≫
      (Functor.mapHomotopyCategory G c).map (Quot.mk (Quotient.CompClosure (homotopic V c)) f)
[PROOFSTEP]
simp only [HomotopyCategory.quot_mk_eq_quotient_map, Functor.mapHomotopyCategory_map, ← Functor.map_comp,
  NatTrans.naturality]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : Functor.Additive F
⊢ mapHomotopyCategory (𝟙 F) c = 𝟙 (Functor.mapHomotopyCategory F c)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
W : Type u_2
inst✝⁴ : Category.{u_3, u_2} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
⊢ mapHomotopyCategory (α ≫ β) c = mapHomotopyCategory α c ≫ mapHomotopyCategory β c
[PROOFSTEP]
aesop_cat


[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
⊢ f 0 ≤ f 1
[PROOFSTEP]
simp only [zero, one, zero_le_one]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f (c * a) ≤ f (c * b)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f c * f a ≤ f c * f b
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_left h _
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f (a * c) ≤ f (b * c)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ f a * f c ≤ f b * f c
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right h _
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : OrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝¹ : OrderedAddCommMonoid β := orderedAddCommMonoid f hf zero add nsmul
src✝ : Semiring β := Injective.semiring f hf zero one add mul nsmul npow nat_cast
a b c : β
h : a ≤ b
hc : 0 ≤ c
⊢ 0 ≤ f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ f 0 ≤ f (a * b)
[PROOFSTEP]
rw [zero, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f a * f b
[PROOFSTEP]
apply mul_nonneg
[GOAL]
case ha
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f a
[PROOFSTEP]
rwa [← zero]
[GOAL]
case hb
α : Type u
β : Type u_1
inst✝¹¹ : OrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ f b
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ f (c * a) < f (c * b)
[PROOFSTEP]
simpa only [mul, zero] using mul_lt_mul_of_pos_left ‹f a < f b› (by rwa [← zero])
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ 0 < f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ f (a * c) < f (b * c)
[PROOFSTEP]
simpa only [mul, zero] using mul_lt_mul_of_pos_right ‹f a < f b› (by rwa [← zero])
[GOAL]
α : Type u
β : Type u_1
inst✝⁷ : StrictOrderedSemiring α
inst✝⁶ : Zero β
inst✝⁵ : One β
inst✝⁴ : Add β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : SMul ℕ β
inst✝ : NatCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
src✝² : OrderedCancelAddCommMonoid β := orderedCancelAddCommMonoid f hf zero add nsmul
src✝¹ : OrderedSemiring β := Injective.orderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Nontrivial β := pullback_nonzero f zero one
a b c : β
h : a < b
hc : 0 < c
⊢ 0 < f c
[PROOFSTEP]
rwa [← zero]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ f 0 < f (a * b)
[PROOFSTEP]
rw [zero, mul]
[GOAL]
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f a * f b
[PROOFSTEP]
apply mul_pos
[GOAL]
case ha
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f a
[PROOFSTEP]
rwa [← zero]
[GOAL]
case hb
α : Type u
β : Type u_1
inst✝¹¹ : StrictOrderedRing α
inst✝¹⁰ : Zero β
inst✝⁹ : One β
inst✝⁸ : Add β
inst✝⁷ : Mul β
inst✝⁶ : Neg β
inst✝⁵ : Sub β
inst✝⁴ : SMul ℕ β
inst✝³ : SMul ℤ β
inst✝² : Pow β ℕ
inst✝¹ : NatCast β
inst✝ : IntCast β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
neg : ∀ (x : β), f (-x) = -f x
sub : ∀ (x y : β), f (x - y) = f x - f y
nsmul : ∀ (x : β) (n : ℕ), f (n • x) = n • f x
zsmul : ∀ (x : β) (n : ℤ), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
nat_cast : ∀ (n : ℕ), f ↑n = ↑n
int_cast : ∀ (n : ℤ), f ↑n = ↑n
src✝¹ : StrictOrderedSemiring β := Injective.strictOrderedSemiring f hf zero one add mul nsmul npow nat_cast
src✝ : Ring β := Injective.ring f hf zero one add mul neg sub nsmul zsmul npow nat_cast int_cast
a b : β
a0 : 0 < a
b0 : 0 < b
⊢ 0 < f b
[PROOFSTEP]
rwa [← zero]


[GOAL]
ι : Type u_1
c : ComplexShape ι
⊢ symm (symm c) = c
[PROOFSTEP]
ext
[GOAL]
case Rel.h.h.a
ι : Type u_1
c : ComplexShape ι
x✝¹ x✝ : ι
⊢ Rel (symm (symm c)) x✝¹ x✝ ↔ Rel c x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
obtain ⟨k, w₁, w₂⟩ := w
[GOAL]
case intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i✝ j'✝
k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
⊢ j✝ = j'✝
[PROOFSTEP]
obtain ⟨k', w₁', w₂'⟩ := w'
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
k' : ι
w₁' : Rel c₁ i✝ k'
w₂' : Rel c₂ k' j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
rw [c₁.next_eq w₁ w₁'] at w₂
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ j✝ j'✝ k : ι
w₁ : Rel c₁ i✝ k
k' : ι
w₂ : Rel c₂ k' j✝
w₁' : Rel c₁ i✝ k'
w₂' : Rel c₂ k' j'✝
⊢ j✝ = j'✝
[PROOFSTEP]
exact c₂.next_eq w₂ w₂'
[GOAL]
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w : Relation.Comp c₁.Rel c₂.Rel i✝ j✝
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
⊢ i✝ = i'✝
[PROOFSTEP]
obtain ⟨k, w₁, w₂⟩ := w
[GOAL]
case intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ : ι
w' : Relation.Comp c₁.Rel c₂.Rel i'✝ j✝
k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
⊢ i✝ = i'✝
[PROOFSTEP]
obtain ⟨k', w₁', w₂'⟩ := w'
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₁ : Rel c₁ i✝ k
w₂ : Rel c₂ k j✝
k' : ι
w₁' : Rel c₁ i'✝ k'
w₂' : Rel c₂ k' j✝
⊢ i✝ = i'✝
[PROOFSTEP]
rw [c₂.prev_eq w₂ w₂'] at w₁
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
c₁ c₂ : ComplexShape ι
i✝ i'✝ j✝ k : ι
w₂ : Rel c₂ k j✝
k' : ι
w₁ : Rel c₁ i✝ k'
w₁' : Rel c₁ i'✝ k'
w₂' : Rel c₂ k' j✝
⊢ i✝ = i'✝
[PROOFSTEP]
exact c₁.prev_eq w₁ w₁'
[GOAL]
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ Subsingleton { j // Rel c i j }
[PROOFSTEP]
constructor
[GOAL]
case allEq
ι : Type u_1
c : ComplexShape ι
i : ι
⊢ ∀ (a b : { j // Rel c i j }), a = b
[PROOFSTEP]
rintro ⟨j, rij⟩ ⟨k, rik⟩
[GOAL]
case allEq.mk.mk
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : Rel c i j
k : ι
rik : Rel c i k
⊢ { val := j, property := rij } = { val := k, property := rik }
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_val
ι : Type u_1
c : ComplexShape ι
i j : ι
rij : Rel c i j
k : ι
rik : Rel c i k
⊢ j = k
[PROOFSTEP]
exact c.next_eq rij rik
[GOAL]
ι : Type u_1
c : ComplexShape ι
j : ι
⊢ Subsingleton { i // Rel c i j }
[PROOFSTEP]
constructor
[GOAL]
case allEq
ι : Type u_1
c : ComplexShape ι
j : ι
⊢ ∀ (a b : { i // Rel c i j }), a = b
[PROOFSTEP]
rintro ⟨i, rik⟩ ⟨j, rjk⟩
[GOAL]
case allEq.mk.mk
ι : Type u_1
c : ComplexShape ι
j✝ i : ι
rik : Rel c i j✝
j : ι
rjk : Rel c j j✝
⊢ { val := i, property := rik } = { val := j, property := rjk }
[PROOFSTEP]
congr
[GOAL]
case allEq.mk.mk.e_val
ι : Type u_1
c : ComplexShape ι
j✝ i : ι
rik : Rel c i j✝
j : ι
rjk : Rel c j j✝
⊢ i = j
[PROOFSTEP]
exact c.prev_eq rik rjk
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ next c i = j
[PROOFSTEP]
apply c.next_eq _ h
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (next c i)
[PROOFSTEP]
rw [next]
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (if h : ∃ j, Rel c i j then Exists.choose h else i)
[PROOFSTEP]
rw [dif_pos]
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c i (Exists.choose ?hc)
case hc ι : Type u_1 c : ComplexShape ι i j : ι h : Rel c i j ⊢ ∃ j, Rel c i j
[PROOFSTEP]
exact Exists.choose_spec ⟨j, h⟩
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ prev c j = i
[PROOFSTEP]
apply c.prev_eq _ h
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (prev c j) j
[PROOFSTEP]
rw [prev, dif_pos]
[GOAL]
ι : Type u_1
c : ComplexShape ι
i j : ι
h : Rel c i j
⊢ Rel c (Exists.choose ?hc) j
case hc ι : Type u_1 c : ComplexShape ι i j : ι h : Rel c i j ⊢ ∃ i, Rel c i j
[PROOFSTEP]
exact Exists.choose_spec (⟨i, h⟩ : ∃ k, c.Rel k j)


[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
have := C.shape _ _ h
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
this : d C i j = 0
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
rw [NatTrans.ext_iff, Function.funext_iff] at this
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j : ι
h : ¬ComplexShape.Rel c i j
this : ∀ (a : T), NatTrans.app (d C i j) a = NatTrans.app 0 a
⊢ (fun i j => NatTrans.app (d C i j) t) i j = 0
[PROOFSTEP]
exact this t
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
have := C.d_comp_d i j k
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
this : d C i j ≫ d C j k = 0
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
rw [NatTrans.ext_iff, Function.funext_iff] at this
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
this : ∀ (a : T), NatTrans.app (d C i j ≫ d C j k) a = NatTrans.app 0 a
⊢ (fun i j => NatTrans.app (d C i j) t) i j ≫ (fun i j => NatTrans.app (d C i j) t) j k = 0
[PROOFSTEP]
exact this t
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
⊢ { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
          map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
      (𝟙 t) =
    𝟙
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.obj
        t)
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        (𝟙 t))
      i =
    Hom.f
      (𝟙
        ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.obj
          t))
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ (X C i).map (𝟙 t) = 𝟙 ((X C i).obj t)
[PROOFSTEP]
rw [(C.X i).map_id]
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
⊢ { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
          map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
      (h₁ ≫ h₂) =
    { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        h₁ ≫
      { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        h₂
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
            map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
        (h₁ ≫ h₂))
      i =
    Hom.f
      ({ obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
          h₁ ≫
        { obj := fun t => mk (fun i => (X C i).obj t) fun i j => NatTrans.app (d C i j) t,
              map := fun {X Y} h => Hom.mk fun i => (HomologicalComplex.X C i).map h }.map
          h₂)
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.78, u_2} T
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ (X C i).map (h₁ ≫ h₂) = (X C i).map h₁ ≫ (X C i).map h₂
[PROOFSTEP]
rw [Functor.map_comp]
[GOAL]
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.4445, u_2} T
X✝ Y✝ : HomologicalComplex (T ⥤ V) c
f : X✝ ⟶ Y✝
t t' : T
g : t ⟶ t'
⊢ ((fun C => asFunctor C) X✝).map g ≫ (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t' =
    (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t ≫ ((fun C => asFunctor C) Y✝).map g
[PROOFSTEP]
ext i
[GOAL]
case h
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
ι : Type u_1
c : ComplexShape ι
T : Type u_2
inst✝ : Category.{?u.4445, u_2} T
X✝ Y✝ : HomologicalComplex (T ⥤ V) c
f : X✝ ⟶ Y✝
t t' : T
g : t ⟶ t'
i : ι
⊢ Hom.f (((fun C => asFunctor C) X✝).map g ≫ (fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t') i =
    Hom.f ((fun t => Hom.mk fun i => NatTrans.app (Hom.f f i) t) t ≫ ((fun C => asFunctor C) Y✝).map g) i
[PROOFSTEP]
exact (f.f i).naturality g


[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ cycles C i = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ⊤ ≤ cycles C i
[PROOFSTEP]
apply le_kernelSubobject
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ Subobject.arrow ⊤ ≫ dFrom C i = 0
[PROOFSTEP]
rw [C.dFrom_eq_zero h, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ boundaries C j ≤ ⊥
[PROOFSTEP]
refine' imageSubobject_le _ 0 _
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasZeroObject V
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ 0 ≫ Subobject.arrow ⊥ = dTo C j
[PROOFSTEP]
rw [C.dTo_eq_zero h, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (xPrevIso C hij).hom ≫ (Arrow.mk (d C i j)).hom = (Arrow.mk (dTo C j)).hom ≫ (Iso.refl (Arrow.mk (dTo C j)).right).hom
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (xPrevIso C hij).hom ≫ d C i j = dTo C j ≫ 𝟙 (X C j)
[PROOFSTEP]
rw [C.dTo_eq hij, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ (Iso.refl (Arrow.mk (dFrom C j)).left).hom ≫ (Arrow.mk (d C j k)).hom =
    (Arrow.mk (dFrom C j)).hom ≫ (xNextIso C hjk).hom
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ 𝟙 (X C j) ≫ d C j k = dFrom C j ≫ (xNextIso C hjk).hom
[PROOFSTEP]
rw [C.dFrom_comp_xNextIso hjk, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ (Arrow.mk (HomologicalComplex.d C 1 0)).hom =
    (Arrow.mk (HomologicalComplex.dTo C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right).hom
[PROOFSTEP]
rw [C.dTo_eq rfl]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ (Arrow.mk (HomologicalComplex.d C 1 0)).hom =
    (Arrow.mk ((HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ HomologicalComplex.d C (0 + 1) 0)).hom ≫
      (Iso.refl
          (Arrow.mk
              ((HomologicalComplex.xPrevIso C (_ : 0 + 1 = 0 + 1)).hom ≫ HomologicalComplex.d C (0 + 1) 0)).right).hom
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
⊢ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left).hom ≫ (Arrow.mk 0).hom =
    (Arrow.mk (HomologicalComplex.dFrom C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).right).hom
[PROOFSTEP]
simp [C.dFrom_eq_zero fun h : _ = _ => one_ne_zero <| by rwa [ChainComplex.next_nat_zero, Nat.zero_add] at h ]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
C : ChainComplex V ℕ
inst✝ : Epi (factorThruImage (HomologicalComplex.d C 1 0))
h : ComplexShape.next (ComplexShape.down ℕ) ?m.17177 + 1 = ?m.17177
⊢ 1 = 0
[PROOFSTEP]
rwa [ChainComplex.next_nat_zero, Nat.zero_add] at h
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0
[PROOFSTEP]
rw [CochainComplex.prev_nat_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (HomologicalComplex.xPrevIsoSelf C
          (_ : ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0)).hom ≫
      (Arrow.mk 0).hom =
    (Arrow.mk (HomologicalComplex.dTo C 0)).hom ≫ (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left).hom ≫ (Arrow.mk (HomologicalComplex.d C 0 1)).hom =
    (Arrow.mk (HomologicalComplex.dFrom C 0)).hom ≫ (HomologicalComplex.xNextIso C (_ : 0 + 1 = 0 + 1)).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C✝ : HomologicalComplex V c
inst✝³ : HasZeroObject V
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
C : CochainComplex V ℕ
⊢ (Arrow.isoMk
          (HomologicalComplex.xPrevIsoSelf C
            (_ : ¬ComplexShape.Rel (ComplexShape.up ℕ) (ComplexShape.prev (ComplexShape.up ℕ) 0) 0))
          (Iso.refl (Arrow.mk (HomologicalComplex.dTo C 0)).right)).hom.right =
    (Arrow.isoMk (Iso.refl (Arrow.mk (HomologicalComplex.dFrom C 0)).left)
          (HomologicalComplex.xNextIso C (_ : 0 + 1 = 0 + 1))).hom.left
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
i : ι
⊢ (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i) ≫ dFrom C₂ i = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap f i ≫ Subobject.arrow (cycles C₂ i) = Subobject.arrow (cycles C₁ i) ≫ Hom.f f i
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap (𝟙 C₁) i = 𝟙 (Subobject.underlying.obj (cycles C₁ i))
[PROOFSTEP]
dsimp only [cyclesMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ Subobject.factorThru (cycles C₁ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₁ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (𝟙 C₁) i)) =
    𝟙 (Subobject.underlying.obj (cycles C₁ i))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ cyclesMap (f ≫ g) i = cyclesMap f i ≫ cyclesMap g i
[PROOFSTEP]
dsimp only [cyclesMap]
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
g : C₂ ⟶ C₃
i : ι
⊢ Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)
      (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f (f ≫ g) i)) =
    Subobject.factorThru (cycles C₂ i) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₂ i)) (Subobject.arrow (cycles C₁ i) ≫ Hom.f f i)) ≫
      Subobject.factorThru (cycles C₃ i) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i)
        (_ : Subobject.Factors (kernelSubobject (dFrom C₃ i)) (Subobject.arrow (cycles C₂ i) ≫ Hom.f g i))
[PROOFSTEP]
simp [Subobject.factorThru_right]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ boundariesMap f i ≫ boundariesToCycles C₂ i = boundariesToCycles C₁ i ≫ cyclesMap f i
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ (boundariesMap f i ≫ boundariesToCycles C₂ i) ≫ Subobject.arrow (cycles C₂ i) =
    (boundariesToCycles C₁ i ≫ cyclesMap f i) ≫ Subobject.arrow (cycles C₂ i)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ { obj := fun C => HomologicalComplex.homology C i,
          map := fun {C₁ C₂} f =>
            homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
              (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.obj
        x✝)
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ homology.map (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (𝟙 x✝) i) (Hom.sqFrom (𝟙 x✝) i)
      (_ : (Hom.sqTo (𝟙 x✝) i).right = (Hom.sqTo (𝟙 x✝) i).right) =
    𝟙 (HomologicalComplex.homology x✝ i)
[PROOFSTEP]
ext1
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
x✝ : HomologicalComplex V c
⊢ homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) ≫
      homology.map (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (𝟙 x✝) i)
        (Hom.sqFrom (𝟙 x✝) i) (_ : (Hom.sqTo (𝟙 x✝) i).right = (Hom.sqTo (𝟙 x✝) i).right) =
    homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) ≫ 𝟙 (HomologicalComplex.homology x✝ i)
[PROOFSTEP]
simp only [homology.π_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun C => HomologicalComplex.homology C i,
          map := fun {C₁ C₂} f =>
            homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
              (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
        x✝¹ ≫
      { obj := fun C => HomologicalComplex.homology C i,
            map := fun {C₁ C₂} f =>
              homology.map (_ : dTo C₁ i ≫ dFrom C₁ i = 0) (_ : dTo C₂ i ≫ dFrom C₂ i = 0) (Hom.sqTo f i)
                (Hom.sqFrom f i) (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) }.map
        x✝
[PROOFSTEP]
simp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo (x✝¹ ≫ x✝) i)
      (Hom.sqFrom (x✝¹ ≫ x✝) i) (_ : (Hom.sqTo (x✝¹ ≫ x✝) i).right = (Hom.sqTo (x✝¹ ≫ x✝) i).right) =
    homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (Hom.sqTo x✝¹ i) (Hom.sqFrom x✝¹ i)
        (_ : (Hom.sqTo x✝¹ i).right = (Hom.sqTo x✝¹ i).right) ≫
      homology.map (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo x✝ i) (Hom.sqFrom x✝ i)
        (_ : (Hom.sqTo x✝ i).right = (Hom.sqTo x✝ i).right)
[PROOFSTEP]
ext1
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
i : ι
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ homology.π (dTo X✝ i) (dFrom X✝ i) (_ : dTo X✝ i ≫ dFrom X✝ i = 0) ≫
      homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo (x✝¹ ≫ x✝) i)
        (Hom.sqFrom (x✝¹ ≫ x✝) i) (_ : (Hom.sqTo (x✝¹ ≫ x✝) i).right = (Hom.sqTo (x✝¹ ≫ x✝) i).right) =
    homology.π (dTo X✝ i) (dFrom X✝ i) (_ : dTo X✝ i ≫ dFrom X✝ i = 0) ≫
      homology.map (_ : dTo X✝ i ≫ dFrom X✝ i = 0) (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (Hom.sqTo x✝¹ i) (Hom.sqFrom x✝¹ i)
          (_ : (Hom.sqTo x✝¹ i).right = (Hom.sqTo x✝¹ i).right) ≫
        homology.map (_ : dTo Y✝ i ≫ dFrom Y✝ i = 0) (_ : dTo Z✝ i ≫ dFrom Z✝ i = 0) (Hom.sqTo x✝ i) (Hom.sqFrom x✝ i)
          (_ : (Hom.sqTo x✝ i).right = (Hom.sqTo x✝ i).right)
[PROOFSTEP]
simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝ : HomologicalComplex V c
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.obj
        x✝)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (𝟙 x✝¹) x✝ =
    𝟙
      ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.obj
        x✝¹)
      x✝
[PROOFSTEP]
simp only [GradedObject.categoryOfGradedObjects_id]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ (homologyFunctor V c x✝).map (𝟙 x✝¹) = 𝟙 (HomologicalComplex.homology x✝¹ x✝)
[PROOFSTEP]
ext
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
x✝¹ : HomologicalComplex V c
x✝ : ι
⊢ homology.π (dTo x✝¹ x✝) (dFrom x✝¹ x✝) (_ : dTo x✝¹ x✝ ≫ dFrom x✝¹ x✝ = 0) ≫ (homologyFunctor V c x✝).map (𝟙 x✝¹) =
    homology.π (dTo x✝¹ x✝) (dFrom x✝¹ x✝) (_ : dTo x✝¹ x✝ ≫ dFrom x✝¹ x✝ = 0) ≫ 𝟙 (HomologicalComplex.homology x✝¹ x✝)
[PROOFSTEP]
simp only [homology.π_map, homologyFunctor_map, kernelSubobjectMap_id, Hom.sqFrom_id, Category.id_comp,
  Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (x✝¹ ≫ x✝) =
    { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
        x✝¹ ≫
      { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ { obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
      (x✝² ≫ x✝¹) x✝ =
    ({ obj := fun C i => HomologicalComplex.homology C i, map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
          x✝² ≫
        { obj := fun C i => HomologicalComplex.homology C i,
              map := fun {C C'} f i => (homologyFunctor V c i).map f }.map
          x✝¹)
      x✝
[PROOFSTEP]
simp only [GradedObject.categoryOfGradedObjects_comp]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ (homologyFunctor V c x✝).map (x✝² ≫ x✝¹) = (homologyFunctor V c x✝).map x✝² ≫ (homologyFunctor V c x✝).map x✝¹
[PROOFSTEP]
ext
[GOAL]
case h.p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝³ : HasEqualizers V
inst✝² : HasImages V
inst✝¹ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : HasCokernels V
X✝ Y✝ Z✝ : HomologicalComplex V c
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : ι
⊢ homology.π (dTo X✝ x✝) (dFrom X✝ x✝) (_ : dTo X✝ x✝ ≫ dFrom X✝ x✝ = 0) ≫ (homologyFunctor V c x✝).map (x✝² ≫ x✝¹) =
    homology.π (dTo X✝ x✝) (dFrom X✝ x✝) (_ : dTo X✝ x✝ ≫ dFrom X✝ x✝ = 0) ≫
      (homologyFunctor V c x✝).map x✝² ≫ (homologyFunctor V c x✝).map x✝¹
[PROOFSTEP]
simp only [Hom.sqFrom_comp, kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, homologyFunctor_map,
  Category.assoc]