case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
by_cases h₁ : Δ = Δ'
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
by_cases h₂ : Δ' = Δ''
case neg.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case neg.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
have eq : Δ.len = Δ''.len + (k + k' + 2) := by linarith
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0

C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''

C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
rw [mapMono_eq_zero K (i' ≫ i) _ _]
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''

C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)

case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0

C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''

C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
rotate_left
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0

case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
case neg.intro.intro
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ mapMono K i ≫ mapMono K i' = 0
by_cases h₃ : Isδ₀ i
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : Δ = Δ'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
subst h₁
no goals
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K, eqToHom_refl]
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝¹ : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst✝ : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
subst h₂
no goals
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝¹ : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst✝ : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K, eqToHom_refl]
no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
⊢ len Δ = len Δ'' + (k + k' + 2)
linarith
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Δ = Δ''
⊢ False
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ Δ ≠ Δ''
by_contra h
no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Δ = Δ''
⊢ False
simp only [self_eq_add_right, h, add_eq_zero_iff, and_false] at eq
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
⊢ ¬Isδ₀ (i' ≫ i)
by_contra h
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ False
simp only [h.1, add_right_inj] at eq
no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False
linarith
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0

case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
by_cases h₄ : Isδ₀ i'
no goals
case pos
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]
no goals
case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : ¬Isδ₀ i'
⊢ mapMono K i ≫ mapMono K i' = 0
simp only [mapMono_eq_zero K i' h₂ h₄, comp_zero]
no goals
case neg
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : len Δ = len Δ' + k + 1
k' : ℕ
hk' : len Δ' = len Δ'' + k' + 1
eq : len Δ = len Δ'' + (k + k' + 2)
h₃ : ¬Isδ₀ i
⊢ mapMono K i ≫ mapMono K i' = 0
simp only [mapMono_eq_zero K i h₁ h₃, zero_comp]