[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
s : Multiset R
t : Multiset M
⊢ sum s • sum t = sum (map (fun p => p.fst • p.snd) (s ×ˢ t))
[PROOFSTEP]
induction' s using Multiset.induction with a s ih
[GOAL]
case empty
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
t : Multiset M
⊢ sum 0 • sum t = sum (map (fun p => p.fst • p.snd) (0 ×ˢ t))
[PROOFSTEP]
simp
[GOAL]
case cons
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
t : Multiset M
a : R
s : Multiset R
ih : sum s • sum t = sum (map (fun p => p.fst • p.snd) (s ×ˢ t))
⊢ sum (a ::ₘ s) • sum t = sum (map (fun p => p.fst • p.snd) ((a ::ₘ s) ×ˢ t))
[PROOFSTEP]
simp [add_smul, ih, ← Multiset.smul_sum]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ (∑ i in s, f i) • ∑ i in t, g i = ∑ p in s ×ˢ t, f p.fst • g p.snd
[PROOFSTEP]
rw [Finset.sum_product, Finset.sum_smul, Finset.sum_congr rfl]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
⊢ ∀ (x : α), x ∈ s → f x • ∑ i in t, g i = ∑ y in t, f (x, y).fst • g (x, y).snd
[PROOFSTEP]
intros
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s✝ : R
x y : M
f : α → R
g : β → M
s : Finset α
t : Finset β
x✝ : α
a✝ : x✝ ∈ s
⊢ f x✝ • ∑ i in t, g i = ∑ y in t, f (x✝, y).fst • g (x✝, y).snd
[PROOFSTEP]
rw [Finset.smul_sum]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
M : Type u_4
ι : Type u_5
inst✝ : CommSemiring R
s : Finset α
⊢ ↑(card s) = ∑ a in s, 1
[PROOFSTEP]
rw [Finset.sum_const, Nat.smul_one_eq_coe]


[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (r_1 s : (i : I) → f i) (x : (i : I) → g i), (r_1 + s) • x = r_1 • x + s • x
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝ : (i : I) → g i
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
[PROOFSTEP]
ext1
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
r✝ s✝ : (i : I) → f i
x✝¹ : (i : I) → g i
x✝ : I
⊢ ((r✝ + s✝) • x✝¹) x✝ = (r✝ • x✝¹ + s✝ • x✝¹) x✝
[PROOFSTEP]
apply add_smul
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
⊢ ∀ (x : (i : I) → g i), 0 • x = 0
[PROOFSTEP]
intros
[GOAL]
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝ : (i : I) → g i
⊢ 0 • x✝ = 0
[PROOFSTEP]
ext1
  -- Porting note: not sure why `apply zero_smul` fails here.
[GOAL]
case h
I : Type u
f : I → Type v
x y : (i : I) → f i
i : I
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst✝ : (i : I) → Module (f i) (g i)
x✝¹ : (i : I) → g i
x✝ : I
⊢ (0 • x✝¹) x✝ = OfNat.ofNat 0 x✝
[PROOFSTEP]
rw [zero_smul]


[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
by_cases hjk : c.Rel j k
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ComplexShape.Rel c j k
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
exact C.d_comp_d' i j k hij hjk
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ComplexShape.Rel c i j
hjk : ¬ComplexShape.Rel c j k
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
rw [C.shape j k hjk, comp_zero]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬ComplexShape.Rel c i j
⊢ d C i j ≫ d C j k = 0
[PROOFSTEP]
rw [C.shape i j hij, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
h_X : C₁.X = C₂.X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j → d C₁ i j ≫ eqToHom (_ : X C₁ j = X C₂ j) = eqToHom (_ : X C₁ i = X C₂ i) ≫ d C₂ i j
⊢ C₁ = C₂
[PROOFSTEP]
obtain ⟨X₁, d₁, s₁, h₁⟩ := C₁
[GOAL]
case mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₂ : HomologicalComplex V c
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
h_X : (mk X₁ d₁).X = C₂.X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X C₂ j) = eqToHom (_ : X (mk X₁ d₁) i = X C₂ i) ≫ d C₂ i j
⊢ mk X₁ d₁ = C₂
[PROOFSTEP]
obtain ⟨X₂, d₂, s₂, h₂⟩ := C₂
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_X : (mk X₁ d₁).X = (mk X₂ d₂).X
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₂ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₂ d₂) i) ≫ d (mk X₂ d₂) i j
⊢ mk X₁ d₁ = mk X₂ d₂
[PROOFSTEP]
dsimp at h_X
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_X : X₁ = X₂
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₂ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₂ d₂) i) ≫ d (mk X₂ d₂) i j
⊢ mk X₁ d₁ = mk X₂ d₂
[PROOFSTEP]
subst h_X
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
⊢ mk X₁ d₁ = mk X₁ d₂
[PROOFSTEP]
simp only [mk.injEq, heq_eq_eq, true_and]
[GOAL]
case mk.mk
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
⊢ d₁ = d₂
[PROOFSTEP]
ext i j
[GOAL]
case mk.mk.h.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
hij : ComplexShape.Rel c i j
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
simpa only [comp_id, id_comp, eqToHom_refl] using h_d i j hij
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬ComplexShape.Rel c i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), ComplexShape.Rel c i j → ComplexShape.Rel c j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    ComplexShape.Rel c i j →
      d (mk X₁ d₁) i j ≫ eqToHom (_ : X (mk X₁ d₁) j = X (mk X₁ d₂) j) =
        eqToHom (_ : X (mk X₁ d₁) i = X (mk X₁ d₂) i) ≫ d (mk X₁ d₂) i j
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ d₁ i j = d₂ i j
[PROOFSTEP]
rw [s₁ i j hij, s₂ i j hij]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p q : ι
h : p = q
⊢ X K p = X K q
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ (XIsoOfEq K h₁₂).hom ≫ (XIsoOfEq K h₂₃).hom = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₂₃ : p₂ = p₃
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ (XIsoOfEq K h₁₂).hom ≫ (XIsoOfEq K h₃₂).inv = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₁₂ : p₁ = p₂
h₃₂ : p₃ = p₂
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ (XIsoOfEq K h₂₁).inv ≫ (XIsoOfEq K h₂₃).hom = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₂₃ : p₂ = p₃
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ (XIsoOfEq K h₂₁).inv ≫ (XIsoOfEq K h₃₂).inv = (XIsoOfEq K (_ : p₁ = p₃)).hom
[PROOFSTEP]
dsimp [XIsoOfEq]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ p₃ : ι
h₂₁ : p₂ = p₁
h₃₂ : p₃ = p₂
⊢ eqToHom (_ : X K p₁ = X K p₂) ≫ eqToHom (_ : X K p₂ = X K p₃) = eqToHom (_ : X K p₁ = X K p₃)
[PROOFSTEP]
simp only [eqToHom_trans]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₂ : ι
h : p₁ = p₂
p₃ : ι
⊢ (XIsoOfEq K h).hom ≫ d K p₂ p₃ = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₁ p₃ : ι
⊢ (XIsoOfEq K (_ : p₁ = p₁)).hom ≫ d K p₁ p₃ = d K p₁ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
h : p₂ = p₁
p₃ : ι
⊢ (XIsoOfEq K h).inv ≫ d K p₂ p₃ = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
⊢ (XIsoOfEq K (_ : p₂ = p₂)).inv ≫ d K p₂ p₃ = d K p₂ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₂ = p₃
p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K h).hom = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K (_ : p₂ = p₂)).hom = d K p₁ p₂
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₂ p₃ : ι
h : p₃ = p₂
p₁ : ι
⊢ d K p₁ p₂ ≫ (XIsoOfEq K h).inv = d K p₁ p₃
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K : HomologicalComplex V c
p₃ p₁ : ι
⊢ d K p₁ p₃ ≫ (XIsoOfEq K (_ : p₃ = p₃)).inv = d K p₁ p₃
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
[PROOFSTEP]
classical
refine' dif_neg _
push_neg
intro
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.next (ComplexShape.down ℕ) 0 = 0
[PROOFSTEP]
refine' dif_neg _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ j, ComplexShape.Rel (ComplexShape.down ℕ) 0 j
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ∀ (j : ℕ), ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
j✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) 0 j✝
[PROOFSTEP]
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.prev (ComplexShape.up ℕ) 0 = 0
[PROOFSTEP]
classical
refine' dif_neg _
push_neg
intro
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ComplexShape.prev (ComplexShape.up ℕ) 0 = 0
[PROOFSTEP]
refine' dif_neg _
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ¬∃ i, ComplexShape.Rel (ComplexShape.up ℕ) i 0
[PROOFSTEP]
push_neg
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
⊢ ∀ (i : ℕ), ¬ComplexShape.Rel (ComplexShape.up ℕ) i 0
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
i✝ : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) i✝ 0
[PROOFSTEP]
apply Nat.noConfusion
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
by_cases hij : c.Rel i j
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
exact f.comm' i j hij
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C A B : HomologicalComplex V c
f : Hom A B
i j : ι
hij : ¬ComplexShape.Rel c i j
⊢ HomologicalComplex.Hom.f f i ≫ d B i j = d A i j ≫ HomologicalComplex.Hom.f f j
[PROOFSTEP]
rw [A.shape i j hij, B.shape i j hij, comp_zero, zero_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
⊢ f = g
[PROOFSTEP]
apply Hom.ext
[GOAL]
case f
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
⊢ f.f = g.f
[PROOFSTEP]
funext
[GOAL]
case f.h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C✝ C D : HomologicalComplex V c
f g : C ⟶ D
h : ∀ (i : ι), Hom.f f i = Hom.f g i
x✝ : ι
⊢ Hom.f f x✝ = Hom.f g x✝
[PROOFSTEP]
apply h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ : HomologicalComplex V c
h : C₁ = C₂
n : ι
⊢ Hom.f (eqToHom h) n = eqToHom (_ : X C₁ n = X C₂ n)
[PROOFSTEP]
subst h
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ : HomologicalComplex V c
n : ι
⊢ Hom.f (eqToHom (_ : C₁ = C₁)) n = eqToHom (_ : X C₁ n = X C₁ n)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ : HomologicalComplex V c
⊢ Function.Injective fun f => f.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
⊢ IsZero zero
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default
case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
[PROOFSTEP]
all_goals
  ext
  dsimp [zero]
  apply Subsingleton.elim
[GOAL]
case refine'_1
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_1.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
[PROOFSTEP]
dsimp [zero]
[GOAL]
case refine'_1.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : zero ⟶ X
i✝ : ι
⊢ Hom.f f i✝ = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_2
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = Hom.f default i✝
[PROOFSTEP]
dsimp [zero]
[GOAL]
case refine'_2.h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasZeroObject V
X : HomologicalComplex V c
f : X ⟶ zero
i✝ : ι
⊢ Hom.f f i✝ = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j j' : ι
rij : ComplexShape.Rel c i j
rij' : ComplexShape.Rel c i j'
⊢ d C i j' ≫ eqToHom (_ : X C j' = X C j) = d C i j
[PROOFSTEP]
obtain rfl := c.next_eq rij rij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ d C i j ≫ eqToHom (_ : X C j = X C j) = d C i j
[PROOFSTEP]
simp only [eqToHom_refl, comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i i' j : ι
rij : ComplexShape.Rel c i j
rij' : ComplexShape.Rel c i' j
⊢ eqToHom (_ : X C i = X C i') ≫ d C i' j = d C i j
[PROOFSTEP]
obtain rfl := c.prev_eq rij rij'
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : ComplexShape.Rel c i j
⊢ eqToHom (_ : X C i = X C i) ≫ d C i j = d C i j
[PROOFSTEP]
simp only [eqToHom_refl, 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
i j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j) = kernelSubobject (d C i j')
[PROOFSTEP]
rw [← d_comp_eqToHom C r r']
[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 j j' : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i j'
⊢ kernelSubobject (d C i j' ≫ eqToHom (_ : X C j' = X C j)) = kernelSubobject (d C i j')
[PROOFSTEP]
apply kernelSubobject_comp_mono
[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✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (d C i j) = imageSubobject (d C i' j)
[PROOFSTEP]
rw [← eqToHom_comp_d C r r']
[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✝ : HasEqualizers V
i i' j : ι
r : ComplexShape.Rel c i j
r' : ComplexShape.Rel c i' j
⊢ imageSubobject (eqToHom (_ : X C i = X C i') ≫ d C i' j) = imageSubobject (d C i' j)
[PROOFSTEP]
apply imageSubobject_iso_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ xPrev C j = X C i
[PROOFSTEP]
rw [← c.prev_eq' r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ComplexShape.prev c j = j
[PROOFSTEP]
dsimp [ComplexShape.prev]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ (if h : ∃ i, ComplexShape.Rel c i j then Exists.choose h else j) = j
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ¬∃ i, ComplexShape.Rel c i j
[PROOFSTEP]
push_neg
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ∀ (i : ι), ¬ComplexShape.Rel c i j
[PROOFSTEP]
intro i hi
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
i : ι
hi : ComplexShape.Rel c i j
⊢ False
[PROOFSTEP]
have : c.prev j = i := c.prev_eq' hi
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
i : ι
hi : ComplexShape.Rel c i j
this : ComplexShape.prev c j = i
⊢ False
[PROOFSTEP]
rw [this] at h
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j i : ι
h : ¬ComplexShape.Rel c i j
hi : ComplexShape.Rel c i j
this : ComplexShape.prev c j = i
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ xNext C i = X C j
[PROOFSTEP]
rw [← c.next_eq' r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ComplexShape.next c i = i
[PROOFSTEP]
dsimp [ComplexShape.next]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ (if h : ∃ j, ComplexShape.Rel c i j then Exists.choose h else i) = i
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ¬∃ j, ComplexShape.Rel c i j
[PROOFSTEP]
rintro ⟨j, hj⟩
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
j : ι
hj : ComplexShape.Rel c i j
⊢ False
[PROOFSTEP]
have : c.next i = j := c.next_eq' hj
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
j : ι
hj : ComplexShape.Rel c i j
this : ComplexShape.next c i = j
⊢ False
[PROOFSTEP]
rw [this] at h
[GOAL]
case hnc.intro
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
h : ¬ComplexShape.Rel c i j
hj : ComplexShape.Rel c i j
this : ComplexShape.next c i = j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dTo C j = (xPrevIso C r).hom ≫ d C i j
[PROOFSTEP]
obtain rfl := c.prev_eq' r
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
r : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ dTo C j = (xPrevIso C r).hom ≫ d C (ComplexShape.prev c j) j
[PROOFSTEP]
exact (Category.id_comp _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dFrom C i = d C i j ≫ (xNextIso C r).inv
[PROOFSTEP]
obtain rfl := c.next_eq' r
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
r : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ dFrom C i = d C i (ComplexShape.next c i) ≫ (xNextIso C r).inv
[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
i j : ι
r : ComplexShape.Rel c i j
⊢ (xPrevIso C r).inv ≫ dTo C j = d C i j
[PROOFSTEP]
simp [C.dTo_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ (xPrevIsoSelf C h).inv ≫ dTo C j = 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dFrom C i ≫ (xNextIso C r).hom = d C i j
[PROOFSTEP]
simp [C.dFrom_eq r]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ dFrom C i ≫ (xNextIsoSelf C h).hom = 0
[PROOFSTEP]
simp [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
i j : ι
r : ComplexShape.Rel c i j
⊢ kernelSubobject (dFrom C i) = kernelSubobject (d C i j)
[PROOFSTEP]
rw [C.dFrom_eq r]
[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 j : ι
r : ComplexShape.Rel c i j
⊢ kernelSubobject (d C i j ≫ (xNextIso C r).inv) = kernelSubobject (d C i j)
[PROOFSTEP]
apply kernelSubobject_comp_mono
[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✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject (dTo C j) = imageSubobject (d C i j)
[PROOFSTEP]
rw [C.dTo_eq r]
[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✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject ((xPrevIso C r).hom ≫ d C i j) = imageSubobject (d C i j)
[PROOFSTEP]
apply imageSubobject_iso_comp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ d C₁ i j = (f i).inv ≫ (d C₁ i j ≫ (f j).hom) ≫ (f j).inv
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ (d C₁ i j ≫ (f j).hom) ≫ (f j).inv = (f i).inv ≫ ((f i).hom ≫ d C₂ i j) ≫ (f j).inv
[PROOFSTEP]
rw [hf i j hij]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i j : ι
hij : ComplexShape.Rel c i j
⊢ (f i).inv ≫ ((f i).hom ≫ d C₂ i j) ≫ (f j).inv = d C₂ i j ≫ (f j).inv
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
⊢ ((mk fun i => (f i).hom) ≫ mk fun i => (f i).inv) = 𝟙 C₁
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i : ι
⊢ HomologicalComplex.Hom.f ((mk fun i => (f i).hom) ≫ mk fun i => (f i).inv) i = HomologicalComplex.Hom.f (𝟙 C₁) i
[PROOFSTEP]
exact (f i).hom_inv_id
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
⊢ ((mk fun i => (f i).inv) ≫ mk fun i => (f i).hom) = 𝟙 C₂
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : autoParam (∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom) _auto✝
i : ι
⊢ HomologicalComplex.Hom.f ((mk fun i => (f i).inv) ≫ mk fun i => (f i).hom) i = HomologicalComplex.Hom.f (𝟙 C₂) i
[PROOFSTEP]
exact (f i).inv_hom_id
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f) i = f i
[PROOFSTEP]
ext
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → X C₁ i ≅ X C₂ i
hf : ∀ (i j : ι), ComplexShape.Rel c i j → (f i).hom ≫ d C₂ i j = d C₁ i j ≫ (f j).hom
i : ι
⊢ (isoApp (isoOfComponents f) i).hom = (f i).hom
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i j : ι
w : ComplexShape.Rel c i j
⊢ prev f j = (xPrevIso C₁ w).hom ≫ HomologicalComplex.Hom.f f i ≫ (xPrevIso C₂ w).inv
[PROOFSTEP]
obtain rfl := c.prev_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
j : ι
w : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ prev f j = (xPrevIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.prev c j) ≫ (xPrevIso C₂ w).inv
[PROOFSTEP]
simp only [xPrevIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i j : ι
w : ComplexShape.Rel c i j
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f j ≫ (xNextIso C₂ w).inv
[PROOFSTEP]
obtain rfl := c.next_eq' w
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : Hom C₁ C₂
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ next f i = (xNextIso C₁ w).hom ≫ HomologicalComplex.Hom.f f (ComplexShape.next c i) ≫ (xNextIso C₂ w).inv
[PROOFSTEP]
simp only [xNextIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i = j + 1
⊢ X i = X (j + 1)
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.down α) i j
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.down α) i j
⊢ (if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) = 0
[PROOFSTEP]
rw [dif_neg (Ne.symm w)]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : ComplexShape.Rel (ComplexShape.down α) i j
hjk : ComplexShape.Rel (ComplexShape.down α) j k
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) j k =
    0
[PROOFSTEP]
dsimp at hij hjk
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j k : α
hij : j + 1 = i
hjk : k + 1 = j
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) i j ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) j k =
    0
[PROOFSTEP]
substs hij hjk
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
k : α
⊢ (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) (k + 1 + 1) (k + 1) ≫
      (fun i j => if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) (k + 1) k =
    0
[PROOFSTEP]
simp only [eqToHom_refl, id_comp, dite_eq_ite, ite_true, sq]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ HomologicalComplex.d (of X d sq) (j + 1) j = d j
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ (if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ HomologicalComplex.d (of X d sq) i j = 0
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
i j : α
h : i ≠ j + 1
⊢ (if h : i = j + 1 then eqToHom (_ : X i = X (j + 1)) ≫ d j else 0) = 0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
by_cases h : n = m + 1
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
m : α
⊢ ComplexShape.Rel (ComplexShape.down α) (m + 1) m →
    f (m + 1) ≫ HomologicalComplex.d (of Y d_Y sq_Y) (m + 1) m = HomologicalComplex.d (of X d_X sq_X) (m + 1) m ≫ f m
[PROOFSTEP]
simpa using comm m
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : ¬n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X (n + 1) ⟶ X n
sq_X : ∀ (n : α), d_X (n + 1) ≫ d_X n = 0
Y : α → V
d_Y : (n : α) → Y (n + 1) ⟶ Y n
sq_Y : ∀ (n : α), d_Y (n + 1) ≫ d_Y n = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f (i + 1) ≫ d_Y i = d_X i ≫ f i
n m : α
h : ¬n = m + 1
⊢ ComplexShape.Rel (ComplexShape.down α) n m → f n ≫ 0 = 0 ≫ f m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 1 0 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 2 1 = d₁
[PROOFSTEP]
change ite (2 = 1 + 1) (𝟙 X₂ ≫ d₁) 0 = d₁
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
⊢ (if 2 = 1 + 1 then 𝟙 X₂ ≫ d₁ else 0) = d₁
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) → (X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' d ≫ t.snd.snd = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ succ') 1 0 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (𝟙 X₁ ≫ d₀) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₁ ⟶ X₀) ×' (d₁ : X₂ ⟶ X₁) ×' d₁ ≫ d₀ = 0) →
    (X₃ : V) ×' (d₂ : X₃ ⟶ t.snd.snd.fst) ×' d₂ ≫ t.snd.snd.snd.snd.fst = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₁ ⟶ X₀)) → (X₂ : V) ×' (d : X₂ ⟶ t.snd.fst) ×' d ≫ t.snd.snd = 0
⊢ (if 1 = 0 + 1 then 𝟙 X₁ ≫ d₀ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n m : ℕ
⊢ ComplexShape.Rel (ComplexShape.down ℕ) n m →
    (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n m =
      HomologicalComplex.d P n m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
rintro (rfl : m + 1 = n)
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
m : ℕ
⊢ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (m + 1) ≫ HomologicalComplex.d Q (m + 1) m =
    HomologicalComplex.d P (m + 1) m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
exact (mkHomAux P Q zero one one_zero_comm succ m).2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : ChainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : one ≫ HomologicalComplex.d Q 1 0 = HomologicalComplex.d P 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f' ≫ HomologicalComplex.d Q (n + 1) n = HomologicalComplex.d P (n + 1) n ≫ f) →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        f'' ≫ HomologicalComplex.d Q (n + 2) (n + 1) = HomologicalComplex.d P (n + 2) (n + 1) ≫ p.snd.fst
n : ℕ
⊢ HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 2) =
    (succ n
        { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n,
          snd :=
            { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1),
              snd :=
                (_ :
                  HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1) ≫
                      HomologicalComplex.d Q (n + 1) n =
                    HomologicalComplex.d P (n + 1) n ≫
                      HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n) } }).fst
[PROOFSTEP]
dsimp [mkHom, mkHomAux]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 = j
⊢ X (i + 1) = X j
[PROOFSTEP]
rw [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) i j = 0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
[PROOFSTEP]
rw [dif_neg]
[GOAL]
case hnc
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
w : ¬ComplexShape.Rel (ComplexShape.up α) i j
⊢ ¬i + 1 = j
[PROOFSTEP]
exact w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ ComplexShape.Rel (ComplexShape.up α) i j →
    ComplexShape.Rel (ComplexShape.up α) j k →
      (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) i j ≫
          (fun i j => if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) j k =
        0
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
⊢ i + 1 = j →
    j + 1 = k →
      ((if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) ≫
          if h : j + 1 = k then d j ≫ eqToHom (_ : X (j + 1) = X k) else 0) =
        0
[PROOFSTEP]
split_ifs with h h' h'
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
[PROOFSTEP]
substs h h'
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i : α
⊢ i + 1 = i + 1 →
    i + 1 + 1 = i + 1 + 1 →
      (d i ≫ eqToHom (_ : X (i + 1) = X (i + 1))) ≫ d (i + 1) ≫ eqToHom (_ : X (i + 1 + 1) = X (i + 1 + 1)) = 0
[PROOFSTEP]
simp [sq]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ 0 = 0
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ 0 = 0
[PROOFSTEP]
all_goals simp
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom (_ : X (i + 1) = X j)) ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ d j ≫ eqToHom (_ : X (j + 1) = X k) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → 0 ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ HomologicalComplex.d (of X d sq) j (j + 1) = d j
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
j : α
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ HomologicalComplex.d (of X d sq) i j = 0
[PROOFSTEP]
dsimp [of]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j : α
h : i + 1 ≠ j
⊢ (if h : i + 1 = j then d i ≫ eqToHom (_ : X (i + 1) = X j) else 0) = 0
[PROOFSTEP]
rw [dif_neg h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
by_cases h : n + 1 = m
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
subst h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n : α
⊢ ComplexShape.Rel (ComplexShape.up α) n (n + 1) →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n (n + 1) = HomologicalComplex.d (of X d_X sq_X) n (n + 1) ≫ f (n + 1)
[PROOFSTEP]
simpa using comm n
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : ¬n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m →
    f n ≫ HomologicalComplex.d (of Y d_Y sq_Y) n m = HomologicalComplex.d (of X d_X sq_X) n m ≫ f m
[PROOFSTEP]
rw [of_d_ne X _ _ h, of_d_ne Y _ _ h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d_X : (n : α) → X n ⟶ X (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y : α → V
d_Y : (n : α) → Y n ⟶ Y (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
f : (i : α) → X i ⟶ Y i
comm : ∀ (i : α), f i ≫ d_Y i = d_X i ≫ f (i + 1)
n m : α
h : ¬n + 1 = m
⊢ ComplexShape.Rel (ComplexShape.up α) n m → f n ≫ 0 = 0 ≫ f m
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 0 1 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ HomologicalComplex.d (mk X₀ X₁ X₂ d₀ d₁ s succ) 1 2 = d₁
[PROOFSTEP]
change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
⊢ (if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ succ') 0 1 = d₀
[PROOFSTEP]
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ :
  (t : (X₀ : V) ×' (X₁ : V) ×' (X₂ : V) ×' (d₀ : X₀ ⟶ X₁) ×' (d₁ : X₁ ⟶ X₂) ×' d₀ ≫ d₁ = 0) →
    (X₃ : V) ×' (d₂ : t.snd.snd.fst ⟶ X₃) ×' t.snd.snd.snd.snd.fst ≫ d₂ = 0
succ' : (t : (X₀ : V) × (X₁ : V) × (X₀ ⟶ X₁)) → (X₂ : V) ×' (d : t.snd.fst ⟶ X₂) ×' t.snd.snd ≫ d = 0
⊢ (if 1 = 0 + 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
[PROOFSTEP]
rw [if_pos rfl, Category.comp_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n m : ℕ
⊢ ComplexShape.Rel (ComplexShape.up ℕ) n m →
    (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n m =
      HomologicalComplex.d P n m ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) m
[PROOFSTEP]
rintro (rfl : n + 1 = m)
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) n ≫ HomologicalComplex.d Q n (n + 1) =
    HomologicalComplex.d P n (n + 1) ≫ (fun n => (mkHomAux P Q zero one one_zero_comm succ n).fst) (n + 1)
[PROOFSTEP]
exact (mkHomAux P Q zero one one_zero_comm succ n).2.2
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : HomologicalComplex.X P 0 ⟶ HomologicalComplex.X Q 0
one : HomologicalComplex.X P 1 ⟶ HomologicalComplex.X Q 1
one_zero_comm : zero ≫ HomologicalComplex.d Q 0 1 = HomologicalComplex.d P 0 1 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : HomologicalComplex.X P n ⟶ HomologicalComplex.X Q n) ×'
          (f' : HomologicalComplex.X P (n + 1) ⟶ HomologicalComplex.X Q (n + 1)) ×'
            f ≫ HomologicalComplex.d Q n (n + 1) = HomologicalComplex.d P n (n + 1) ≫ f') →
      (f'' : HomologicalComplex.X P (n + 2) ⟶ HomologicalComplex.X Q (n + 2)) ×'
        p.snd.fst ≫ HomologicalComplex.d Q (n + 1) (n + 2) = HomologicalComplex.d P (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 2) =
    (succ n
        { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n,
          snd :=
            { fst := HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1),
              snd :=
                (_ :
                  HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) n ≫
                      HomologicalComplex.d Q n (n + 1) =
                    HomologicalComplex.d P n (n + 1) ≫
                      HomologicalComplex.Hom.f (mkHom P Q zero one one_zero_comm succ) (n + 1)) } }).fst
[PROOFSTEP]
dsimp [mkHom, mkHomAux]


[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
let P := factors I
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
have prime_of_mem := fun p (hp : p ∈ P.toFinset) => prime_of_factor p (Multiset.mem_toFinset.mp hp)
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))
[PROOFSTEP]
apply @torsionBySet_isInternal _ _ _ _ _ _ _ _ (fun p => p ^ P.count p) _
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P)
[PROOFSTEP]
convert hM
[GOAL]
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ⨅ (i : Ideal R) (_ : i ∈ Multiset.toFinset (factors I)), i ^ Multiset.count i P = I
[PROOFSTEP]
rw [← Finset.inf_eq_iInf, IsDedekindDomain.inf_prime_pow_eq_prod, ← Finset.prod_multiset_count, ← associated_iff_eq]
[GOAL]
case h.e'_6.h.e'_4
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Associated (Multiset.prod (factors I)) I
[PROOFSTEP]
exact factors_prod hI
[GOAL]
case h.e'_6.h.e'_4.prime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R), i ∈ Multiset.toFinset (factors I) → Prime i
[PROOFSTEP]
exact prime_of_mem
[GOAL]
case h.e'_6.h.e'_4.coprime
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ ∀ (i : Ideal R),
    i ∈ Multiset.toFinset (factors I) → ∀ (j : Ideal R), j ∈ Multiset.toFinset (factors I) → i ≠ j → i ≠ j
[PROOFSTEP]
exact fun _ _ _ _ ij => ij
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
⊢ Set.Pairwise ↑(Multiset.toFinset (factors I)) fun i j =>
    (fun p => p ^ Multiset.count p P) i ⊔ (fun p => p ^ Multiset.count p P) j = ⊤
[PROOFSTEP]
intro p hp q hq pq
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ (fun p => p ^ Multiset.count p P) p ⊔ (fun p => p ^ Multiset.count p P) q = ⊤
[PROOFSTEP]
dsimp
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ Multiset.count p (factors I) ⊔ q ^ Multiset.count q (factors I) = ⊤
[PROOFSTEP]
rw [irreducible_pow_sup]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
[PROOFSTEP]
suffices (normalizedFactors _).count p = 0 by rw [this, zero_min, pow_zero, Ideal.one_eq_top]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
this : Multiset.count p (normalizedFactors ?m.97629) = 0
⊢ p ^ min (Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I)))) (Multiset.count p (factors I)) = ⊤
[PROOFSTEP]
rw [this, zero_min, pow_zero, Ideal.one_eq_top]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Multiset.count p (normalizedFactors (q ^ Multiset.count q (factors I))) = 0
[PROOFSTEP]
rw [Multiset.count_eq_zero, normalizedFactors_of_irreducible_pow (prime_of_mem q hq).irreducible,
  Multiset.mem_replicate]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ ¬(Multiset.count q (factors I) ≠ 0 ∧ p = ↑normalize q)
[PROOFSTEP]
exact fun H => pq <| H.2.trans <| normalize_eq q
[GOAL]
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ ⊥
[PROOFSTEP]
rw [← Ideal.zero_eq_bot]
[GOAL]
case hI
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ^ Multiset.count q (factors I) ≠ 0
[PROOFSTEP]
apply pow_ne_zero
[GOAL]
case hI.h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ q ≠ 0
[PROOFSTEP]
exact (prime_of_mem q hq).ne_zero
[GOAL]
case hJ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ (p : Ideal R), p ∈ Multiset.toFinset P → Prime p
p : Ideal R
hp : p ∈ ↑(Multiset.toFinset (factors I))
q : Ideal R
hq : q ∈ ↑(Multiset.toFinset (factors I))
pq : p ≠ q
⊢ Irreducible p
[PROOFSTEP]
exact (prime_of_mem p hp).irreducible
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
have hM' := Module.isTorsionBySet_annihilator_top R M
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ DirectSum.IsInternal fun p => torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors (annihilator ⊤)))
[PROOFSTEP]
refine' isInternal_prime_power_torsion_of_is_torsion_by_ideal _ hM'
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : ↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R) ≠ ∅
⊢ annihilator ⊤ ≠ ⊥
[PROOFSTEP]
rw [← Set.nonempty_iff_ne_empty] at hI
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ annihilator ⊤ ≠ ⊥
[PROOFSTEP]
rw [Submodule.ne_bot_iff]
[GOAL]
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
hI : Set.Nonempty (↑(annihilator ⊤) ∩ ↑(nonZeroDivisors R))
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
[PROOFSTEP]
obtain ⟨x, H, hx⟩ := hI
[GOAL]
case intro.intro
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDedekindDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑(annihilator ⊤)
x : R
H : x ∈ ↑(annihilator ⊤)
hx : x ∈ ↑(nonZeroDivisors R)
⊢ ∃ x, x ∈ annihilator ⊤ ∧ x ≠ 0
[PROOFSTEP]
exact ⟨x, H, nonZeroDivisors.ne_zero hx⟩