[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ kernel.lift g f w ≫ kernel.ι g = f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ Mono (imageToKernel f g w)
[PROOFSTEP]
dsimp only [imageToKernel]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ Mono (Subobject.ofLE (imageSubobject f) (kernelSubobject g) (_ : imageSubobject f ≤ kernelSubobject g))
[PROOFSTEP]
infer_instance
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ Subobject.arrow (kernelSubobject g) = Subobject.arrow (imageSubobject f)
[PROOFSTEP]
simp [imageToKernel]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝² : HasImage f
g : B ⟶ C
inst✝¹ : HasKernel g
inst✝ : ConcreteCategory V
w : f ≫ g = 0
x : (forget V).obj (Subobject.underlying.obj (imageSubobject f))
⊢ ↑(Subobject.arrow (kernelSubobject g)) (↑(imageToKernel f g w) x) = ↑(Subobject.arrow (imageSubobject f)) x
[PROOFSTEP]
rw [← comp_apply, imageToKernel_arrow]
  -- This is less useful as a `simp` lemma than it initially appears,
  -- as it "loses" the information the morphism factors through the image.
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ imageToKernel f g w = factorThruKernelSubobject g f w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ (factorThruImageSubobject f ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g) =
    factorThruKernelSubobject g f w ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w = 0
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasZeroObject V
w : 0 ≫ g = 0
⊢ imageToKernel 0 g w ≫ Subobject.arrow (kernelSubobject g) = 0 ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w = Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝ : HasImages V
w : f ≫ 0 = 0
⊢ imageToKernel f 0 w ≫ Subobject.arrow (kernelSubobject 0) =
    (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0))) ≫
      Subobject.arrow (kernelSubobject 0)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0
[PROOFSTEP]
simp [reassoc_of% w]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) =
    imageToKernel f g w ≫
      Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h)) (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ imageToKernel f (g ≫ h) (_ : f ≫ g ≫ h = 0) ≫ Subobject.arrow (kernelSubobject (g ≫ h)) =
    (imageToKernel f g w ≫
        Subobject.ofLE (kernelSubobject g) (kernelSubobject (g ≫ h))
          (_ : kernelSubobject g ≤ kernelSubobject (g ≫ h))) ≫
      Subobject.arrow (kernelSubobject (g ≫ h))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ (h ≫ f) ≫ g = 0
[PROOFSTEP]
simp [w]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g (_ : (h ≫ f) ≫ g = 0) =
    Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
      imageToKernel f g w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g (_ : (h ≫ f) ≫ g = 0) ≫ Subobject.arrow (kernelSubobject g) =
    (Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
        imageToKernel f g w) ≫
      Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ (f ≫ g) ≫ h = 0 ≫ h
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w =
    imageToKernel f g (_ : f ≫ g = 0) ≫
      (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
          (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).inv
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ imageToKernel f (g ≫ h) w ≫ Subobject.arrow (kernelSubobject (g ≫ h)) =
    (imageToKernel f g (_ : f ≫ g = 0) ≫
        (Subobject.isoOfEq (kernelSubobject (g ≫ h)) (kernelSubobject g)
            (_ : kernelSubobject (g ≫ h) = kernelSubobject g)).inv) ≫
      Subobject.arrow (kernelSubobject (g ≫ h))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ h ≫ f ≫ g = h ≫ 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w =
    Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
      imageToKernel f g (_ : f ≫ g = 0)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ imageToKernel (h ≫ f) g w ≫ Subobject.arrow (kernelSubobject g) =
    (Subobject.ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f) ≫
        imageToKernel f g (_ : f ≫ g = 0)) ≫
      Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ f ≫ g = 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w =
    (imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ imageToKernel (f ≫ i.hom) (i.inv ≫ g) w ≫ Subobject.arrow (kernelSubobject (i.inv ≫ g)) =
    ((imageSubobjectCompIso f i.hom).hom ≫ imageToKernel f g (_ : f ≫ g = 0) ≫ (kernelSubobjectIsoComp i.inv g).inv) ≫
      Subobject.arrow (kernelSubobject (i.inv ≫ g))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasZeroObject V
inst✝ : Mono g
⊢ 0 ≫ g = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ f ≫ 0 = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ Epi (imageToKernel f 0 (_ : f ≫ 0 = 0))
[PROOFSTEP]
simp only [imageToKernel_zero_right]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
⊢ Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
haveI := epi_image_of_epi f
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi (Subobject.arrow (imageSubobject f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
rw [← imageSubobject_arrow]
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi (((imageSubobjectIso f).hom ≫ image.ι f) ≫ inv (Subobject.arrow (kernelSubobject 0)))
[PROOFSTEP]
refine' @epi_comp _ _ _ _ _ _ (epi_comp _ _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝² : HasImage f
g : B ⟶ C
inst✝¹ : HasKernel g
w : f ≫ g = 0
inst✝ : HasCokernel (imageToKernel f g w)
D : V
k : Subobject.underlying.obj (kernelSubobject g) ⟶ D
p : imageToKernel f g w ≫ k = 0
⊢ π f g w ≫ desc f g w k p = k
[PROOFSTEP]
simp [homology.π, homology.desc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝⁶ : HasImage f
g : B ⟶ C
inst✝⁵ : HasKernel g
w : f ≫ g = 0
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f 0 (_ : f ≫ 0 = 0))
inst✝² : HasCokernel f
inst✝¹ : HasCokernel (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ imageToKernel f 0 (_ : f ≫ 0 = 0) ≫ (kernelSubobjectIso 0 ≪≫ kernelZeroIsoSource).hom =
    (imageSubobjectIso f).hom ≫ image.ι f
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝⁵ : HasImage f
g : B ⟶ C
inst✝⁴ : HasKernel g
w : f ≫ g = 0
inst✝³ : HasCokernel (imageToKernel f g w)
inst✝² : HasZeroObject V
inst✝¹ : HasImage 0
inst✝ : HasCokernel (imageToKernel 0 0 (_ : 0 ≫ 0 = 0))
⊢ imageToKernel 0 0 (_ : 0 ≫ 0 = 0) ≫ Subobject.arrow (kernelSubobject 0) = 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹² : HasImage f
g : B ⟶ C
inst✝¹¹ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁰ : HasImage f'
g' : B' ⟶ C'
inst✝⁹ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝⁸ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝⁷ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝⁶ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝⁵ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁴ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝³ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝² : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝¹ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p : α.right = β.left
⊢ imageToKernel f g w ≫ kernelSubobjectMap β = imageSubobjectMap α ≫ imageToKernel f' g' w'
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹⁴ : Category.{v, u} V
inst✝¹³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹² : HasImage f
g : B ⟶ C
inst✝¹¹ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁰ : HasImage f'
g' : B' ⟶ C'
inst✝⁹ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝⁸ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝⁷ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝⁶ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝⁵ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁴ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝³ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝² : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝¹ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p : α.right = β.left
⊢ (imageToKernel f g w ≫ kernelSubobjectMap β) ≫ Subobject.arrow (kernelSubobject g') =
    (imageSubobjectMap α ≫ imageToKernel f' g' w') ≫ Subobject.arrow (kernelSubobject g')
[PROOFSTEP]
simp [p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ imageToKernel f g w ≫ kernelSubobjectMap β ≫ cokernel.π (imageToKernel f' g' w') = 0
[PROOFSTEP]
rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ imageSubobjectMap α ≫ imageToKernel f' g' w' ≫ cokernel.π (imageToKernel f' g' w') = 0
[PROOFSTEP]
simp only [cokernel.condition, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
⊢ π f g w ≫ map w w' α β p = kernelSubobjectMap β ≫ π f' g' w'
[PROOFSTEP]
simp only [homology.π, homology.map, cokernel.π_desc]
[GOAL]
ι : Type u_1
V : Type u
inst✝²⁰ : Category.{v, u} V
inst✝¹⁹ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁸ : HasImage f
g : B ⟶ C
inst✝¹⁷ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁶ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁵ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹⁴ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹³ : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹² : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹¹ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝¹⁰ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁹ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁸ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁷ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁶ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁵ : HasCokernel (imageToKernel f g w)
inst✝⁴ : HasCokernel (imageToKernel f' g' w')
inst✝³ : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝² : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝¹ : HasCokernel (imageToKernel f₃ g₃ w₃)
inst✝ : ConcreteCategory V
p : α.right = β.left
x : (forget V).obj (Subobject.underlying.obj (kernelSubobject g))
⊢ ↑(map w w' α β p) (↑(π f g w) x) = ↑(π f' g' w') (↑(kernelSubobjectMap β) x)
[PROOFSTEP]
simp only [← comp_apply, homology.π_map w w' α β p]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0
[PROOFSTEP]
simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ map w w' α β p ≫ desc f' g' w' k z =
    desc f g w (kernelSubobjectMap β ≫ k) (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p : α.right = β.left
D : V
k : Subobject.underlying.obj (kernelSubobject g') ⟶ D
z : imageToKernel f' g' w' ≫ k = 0
⊢ π f g w ≫ map w w' α β p ≫ desc f' g' w' k z =
    π f g w ≫ desc f g w (kernelSubobjectMap β ≫ k) (_ : imageToKernel f g w ≫ kernelSubobjectMap β ≫ k = 0)
[PROOFSTEP]
simp only [homology.π_desc, homology.π_map_assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
⊢ map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right) = 𝟙 (homology f g w)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
⊢ π f g w ≫ map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right) =
    π f g w ≫ 𝟙 (homology f g w)
[PROOFSTEP]
simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
[GOAL]
ι : Type u_1
V✝ : Type u
inst✝²⁰ : Category.{v, u} V✝
inst✝¹⁹ : HasZeroMorphisms V✝
A B C : V✝
f : A ⟶ B
inst✝¹⁸ : HasImage f
g : B ⟶ C
inst✝¹⁷ : HasKernel g
w : f ≫ g = 0
A' B' C' : V✝
f' : A' ⟶ B'
inst✝¹⁶ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁵ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹⁴ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁✝ B₁✝ C₁✝ : V✝
f₁✝ : A₁✝ ⟶ B₁✝
inst✝¹³ : HasImage f₁✝
g₁✝ : B₁✝ ⟶ C₁✝
inst✝¹² : HasKernel g₁✝
w₁ : f₁✝ ≫ g₁✝ = 0
A₂✝ B₂✝ C₂✝ : V✝
f₂✝ : A₂✝ ⟶ B₂✝
inst✝¹¹ : HasImage f₂✝
g₂✝ : B₂✝ ⟶ C₂✝
inst✝¹⁰ : HasKernel g₂✝
w₂ : f₂✝ ≫ g₂✝ = 0
A₃✝ B₃✝ C₃✝ : V✝
f₃✝ : A₃✝ ⟶ B₃✝
inst✝⁹ : HasImage f₃✝
g₃✝ : B₃✝ ⟶ C₃✝
inst✝⁸ : HasKernel g₃✝
w₃ : f₃✝ ≫ g₃✝ = 0
α₁✝ : Arrow.mk f₁✝ ⟶ Arrow.mk f₂✝
inst✝⁷ : HasImageMap α₁✝
β₁✝ : Arrow.mk g₁✝ ⟶ Arrow.mk g₂✝
α₂✝ : Arrow.mk f₂✝ ⟶ Arrow.mk f₃✝
inst✝⁶ : HasImageMap α₂✝
β₂✝ : Arrow.mk g₂✝ ⟶ Arrow.mk g₃✝
inst✝⁵ : HasCokernel (imageToKernel f g w)
inst✝⁴ : HasCokernel (imageToKernel f' g' w')
inst✝³ : HasCokernel (imageToKernel f₁✝ g₁✝ w₁)
inst✝² : HasCokernel (imageToKernel f₂✝ g₂✝ w₂)
inst✝¹ : HasCokernel (imageToKernel f₃✝ g₃✝ w₃)
V : Type u_2
inst✝ : Category.{u_3, u_2} V
A₁ B₁ C₁ A₂ B₂ C₂ A₃ B₃ C₃ : V
f₁ : A₁ ⟶ B₁
g₁ : B₁ ⟶ C₁
f₂ : A₂ ⟶ B₂
g₂ : B₂ ⟶ C₂
f₃ : A₃ ⟶ B₃
g₃ : B₃ ⟶ C₃
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ (α₁ ≫ α₂).right = (β₁ ≫ β₂).left
[PROOFSTEP]
simp only [Arrow.comp_left, Arrow.comp_right, p₁, p₂]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ map w₁ w₂ α₁ β₁ p₁ ≫ map w₂ w₃ α₂ β₂ p₂ = map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (_ : (α₁ ≫ α₂).right = (β₁ ≫ β₂).left)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α
β : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
p₁ : α₁.right = β₁.left
p₂ : α₂.right = β₂.left
⊢ π f₁ g₁ w₁ ≫ map w₁ w₂ α₁ β₁ p₁ ≫ map w₂ w₃ α₂ β₂ p₂ =
    π f₁ g₁ w₁ ≫ map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (_ : (α₁ ≫ α₂).right = (β₁ ≫ β₂).left)
[PROOFSTEP]
simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.inv.right = β.inv.left
[PROOFSTEP]
rw [← cancel_mono α.hom.right, ← Comma.comp_right, α.inv_hom_id, Comma.id_right, p, ← Comma.comp_left, β.inv_hom_id,
  Comma.id_left]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ 𝟙 (Arrow.mk f₂).right = 𝟙 (Arrow.mk g₂).left
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₁ w₂ α.hom β.hom p ≫ map w₂ w₁ α.inv β.inv (_ : α.inv.right = β.inv.left) = 𝟙 (homology f₁ g₁ w₁)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₁ w₁ (α.hom ≫ α.inv) (β.hom ≫ β.inv) (_ : (α.hom ≫ α.inv).right = (β.hom ≫ β.inv).left) =
    map w₁ w₁ (𝟙 (Arrow.mk f₁)) (𝟙 (Arrow.mk g₁)) (_ : (𝟙 (Arrow.mk f₁)).right = (𝟙 (Arrow.mk f₁)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.hom ≫ α.inv = 𝟙 (Arrow.mk f₁)
[PROOFSTEP]
simp only [Iso.hom_inv_id]
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ β.hom ≫ β.inv = 𝟙 (Arrow.mk g₁)
[PROOFSTEP]
simp only [Iso.hom_inv_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₂ w₁ α.inv β.inv (_ : α.inv.right = β.inv.left) ≫ map w₁ w₂ α.hom β.hom p = 𝟙 (homology f₂ g₂ w₂)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ map w₂ w₂ (α.inv ≫ α.hom) (β.inv ≫ β.hom) (_ : (α.inv ≫ α.hom).right = (β.inv ≫ β.hom).left) =
    map w₂ w₂ (𝟙 (Arrow.mk f₂)) (𝟙 (Arrow.mk g₂)) (_ : (𝟙 (Arrow.mk f₂)).right = (𝟙 (Arrow.mk f₂)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ α.inv ≫ α.hom = 𝟙 (Arrow.mk f₂)
[PROOFSTEP]
simp only [Iso.inv_hom_id]
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝¹⁹ : Category.{v, u} V
inst✝¹⁸ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹⁷ : HasImage f
g : B ⟶ C
inst✝¹⁶ : HasKernel g
w : f ≫ g = 0
A' B' C' : V
f' : A' ⟶ B'
inst✝¹⁵ : HasImage f'
g' : B' ⟶ C'
inst✝¹⁴ : HasKernel g'
w' : f' ≫ g' = 0
α✝ : Arrow.mk f ⟶ Arrow.mk f'
inst✝¹³ : HasImageMap α✝
β✝ : Arrow.mk g ⟶ Arrow.mk g'
A₁ B₁ C₁ : V
f₁ : A₁ ⟶ B₁
inst✝¹² : HasImage f₁
g₁ : B₁ ⟶ C₁
inst✝¹¹ : HasKernel g₁
w₁ : f₁ ≫ g₁ = 0
A₂ B₂ C₂ : V
f₂ : A₂ ⟶ B₂
inst✝¹⁰ : HasImage f₂
g₂ : B₂ ⟶ C₂
inst✝⁹ : HasKernel g₂
w₂ : f₂ ≫ g₂ = 0
A₃ B₃ C₃ : V
f₃ : A₃ ⟶ B₃
inst✝⁸ : HasImage f₃
g₃ : B₃ ⟶ C₃
inst✝⁷ : HasKernel g₃
w₃ : f₃ ≫ g₃ = 0
α₁ : Arrow.mk f₁ ⟶ Arrow.mk f₂
inst✝⁶ : HasImageMap α₁
β₁ : Arrow.mk g₁ ⟶ Arrow.mk g₂
α₂ : Arrow.mk f₂ ⟶ Arrow.mk f₃
inst✝⁵ : HasImageMap α₂
β₂ : Arrow.mk g₂ ⟶ Arrow.mk g₃
inst✝⁴ : HasCokernel (imageToKernel f g w)
inst✝³ : HasCokernel (imageToKernel f' g' w')
inst✝² : HasCokernel (imageToKernel f₁ g₁ w₁)
inst✝¹ : HasCokernel (imageToKernel f₂ g₂ w₂)
inst✝ : HasCokernel (imageToKernel f₃ g₃ w₃)
α : Arrow.mk f₁ ≅ Arrow.mk f₂
β : Arrow.mk g₁ ≅ Arrow.mk g₂
p : α.hom.right = β.hom.left
⊢ β.inv ≫ β.hom = 𝟙 (Arrow.mk g₂)
[PROOFSTEP]
simp only [Iso.inv_hom_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk f).left) ≫ (Arrow.mk f').hom = (Arrow.mk f).hom ≫ (𝟭 V).map (𝟙 (Arrow.mk f).right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk g).left) ≫ (Arrow.mk g').hom = (Arrow.mk g).hom ≫ (𝟭 V).map (𝟙 (Arrow.mk g).right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk f').left) ≫ (Arrow.mk f).hom = (Arrow.mk f').hom ≫ (𝟭 V).map (𝟙 (Arrow.mk f').right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ (𝟭 V).map (𝟙 (Arrow.mk g').left) ≫ (Arrow.mk g).hom = (Arrow.mk g').hom ≫ (𝟭 V).map (𝟙 (Arrow.mk g').right)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
obtain rfl := pf
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
g' : B ⟶ C
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pg : g = g'
w' : f ≫ g' = 0
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
obtain rfl := pg
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w)
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w w
      (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
      (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
      (_ :
        (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
          (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right)).left) =
    map w w (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) =
    𝟙 (Arrow.mk f)
[PROOFSTEP]
aesop_cat
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) =
    𝟙 (Arrow.mk g)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
f' : A ⟶ B
g' : B ⟶ C
w' : f' ≫ g' = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pf : f = f'
pg : g = g'
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f').left) (𝟙 (Arrow.mk f').right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f' g' w')
[PROOFSTEP]
obtain rfl := pf
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
g' : B ⟶ C
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
pg : g = g'
w' : f ≫ g' = 0
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g').left) (𝟙 (Arrow.mk g').right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g' w')
[PROOFSTEP]
obtain rfl := pg
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w' w (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) ≫
      map w w' (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
        (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
        (_ :
          (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
            (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right) =
    𝟙 (homology f g w')
[PROOFSTEP]
rw [homology.map_comp, ← homology.map_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ map w' w'
      (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right))
      (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
        CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right))
      (_ :
        (CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right)).right =
          (CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
              CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right)).left) =
    map w' w' (𝟙 (Arrow.mk f)) (𝟙 (Arrow.mk g)) (_ : (𝟙 (Arrow.mk f)).right = (𝟙 (Arrow.mk f)).right)
[PROOFSTEP]
congr
[GOAL]
case e_α
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk f).left) (𝟙 (Arrow.mk f).right) =
    𝟙 (Arrow.mk f)
[PROOFSTEP]
aesop_cat
[GOAL]
case e_β
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasCokernels V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
w' : f ≫ g = 0
⊢ CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) ≫
      CommaMorphism.mk (𝟙 (Arrow.mk g).left) (𝟙 (Arrow.mk g).right) =
    𝟙 (Arrow.mk g)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ image.ι f ≫ g = 0
[PROOFSTEP]
ext
[GOAL]
case w
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = factorThruImage f ≫ 0
[PROOFSTEP]
simpa using w
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ ((imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 =
    (imageToKernel f g w ≫ (kernelSubobjectIso g).hom) ≫ equalizer.ι g 0
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageToKernel' f g w ≫ (kernelSubobjectIso g).inv) ≫ Subobject.arrow (kernelSubobject g) =
    ((imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫ Subobject.arrow (kernelSubobject g)
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w
[PROOFSTEP]
simp only [imageSubobjectIso_imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w
[PROOFSTEP]
simp only [imageToKernel'_kernelSubobjectIso]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
        (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫
      cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
        (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) =
    𝟙 (homology f g w)
[PROOFSTEP]
apply coequalizer.hom_ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ coequalizer.π (imageToKernel f g w) 0 ≫
      cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
          (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w) ≫
        cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
          (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) =
    coequalizer.π (imageToKernel f g w) 0 ≫ 𝟙 (homology f g w)
[PROOFSTEP]
simp only [Iso.hom_inv_id_assoc, cokernel.π_desc, cokernel.π_desc_assoc, Category.assoc, coequalizer_as_cokernel]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ cokernel.π (imageToKernel f g w) = cokernel.π (imageToKernel f g w) ≫ 𝟙 (homology f g w)
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
        (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫
      cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
        (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w) =
    𝟙 (cokernel (imageToKernel' f g w))
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝² : HasKernels V
inst✝¹ : HasImages V
inst✝ : HasCokernels V
w : f ≫ g = 0
⊢ coequalizer.π (imageToKernel' f g w) 0 ≫
      cokernel.map (imageToKernel' f g w) (imageToKernel f g w) (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
          (_ : imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w) ≫
        cokernel.map (imageToKernel f g w) (imageToKernel' f g w) (imageSubobjectIso f).hom (kernelSubobjectIso g).hom
          (_ : imageToKernel f g w ≫ (kernelSubobjectIso g).hom = (imageSubobjectIso f).hom ≫ imageToKernel' f g w) =
    coequalizer.π (imageToKernel' f g w) 0 ≫ 𝟙 (cokernel (imageToKernel' f g w))
[PROOFSTEP]
simp only [Iso.inv_hom_id_assoc, cokernel.π_desc, Category.comp_id, cokernel.π_desc_assoc, Category.assoc]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ homology f g w ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
refine' homologyIsoCokernelImageToKernel' f g w ≪≫ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ cokernel (imageToKernel' f g w) ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
have p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w :=
  by
  ext
  simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
⊢ (factorThruImage f ≫ imageToKernel' f g w) ≫ equalizer.ι g 0 = kernel.lift g f w ≫ equalizer.ι g 0
[PROOFSTEP]
simp [imageToKernel']
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝³ : HasKernels V
inst✝² : HasImages V
inst✝¹ : HasCokernels V
inst✝ : HasEqualizers V
w : f ≫ g = 0
p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w
⊢ cokernel (imageToKernel' f g w) ≅ cokernel (kernel.lift g f w)
[PROOFSTEP]
exact (cokernelEpiComp _ _).symm ≪≫ cokernelIsoOfEq p


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : p ∣ Multiset.prod s → ∃ a, a ∈ s ∧ p ∣ a
h : p ∣ Multiset.prod (a ::ₘ s)
⊢ p ∣ a * Multiset.prod s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoidWithZero α
p : α
hp : Prime p
s : Multiset β
f : β → α
h : p ∣ Multiset.prod (Multiset.map f s)
⊢ ∃ a, a ∈ s ∧ p ∣ f a
[PROOFSTEP]
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using hp.exists_mem_multiset_dvd h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s : Multiset α
⊢ (∀ (r : α), r ∈ 0 → Prime r) → p ∣ Multiset.prod 0 → ∃ q, q ∈ 0 ∧ p ~ᵤ q
[PROOFSTEP]
simp [mt isUnit_iff_dvd_one.2 hp.not_unit]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
rw [Multiset.prod_cons] at hps
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
cases' hp.dvd_or_dvd hps with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ a
hap : Prime a
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
p : α
hp : Prime p
s✝ : Multiset α
a : α
s : Multiset α
ih : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ p ~ᵤ q
hs : ∀ (r : α), r ∈ a ::ₘ s → Prime r
hps : p ∣ a * Multiset.prod s
h : p ∣ Multiset.prod s
q : α
hq₁ : q ∈ s
hq₂ : p ~ᵤ q
⊢ ∃ q, q ∈ a ::ₘ s ∧ p ~ᵤ q
[PROOFSTEP]
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s : Multiset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
uniq : ∀ (a : α), countp (Associated a) s ≤ 1
⊢ prod s ∣ n
[PROOFSTEP]
induction' s using Multiset.induction_on with a s induct n primes divs generalizing n
[GOAL]
case empty
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s → Prime a
div✝ : ∀ (a : α), a ∈ s → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s ≤ 1
n : α
h : ∀ (a : α), a ∈ 0 → Prime a
div : ∀ (a : α), a ∈ 0 → a ∣ n
uniq : ∀ (a : α), countp (Associated a) 0 ≤ 1
⊢ prod 0 ∣ n
[PROOFSTEP]
simp only [Multiset.prod_zero, one_dvd]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
n : α
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ n
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
⊢ prod (a ::ₘ s) ∣ n
[PROOFSTEP]
rw [Multiset.prod_cons]
[GOAL]
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n✝ : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n✝
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
n : α
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ n
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
⊢ a * prod s ∣ n
[PROOFSTEP]
obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
⊢ a * prod s ∣ a * k
[PROOFSTEP]
apply mul_dvd_mul_left a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
⊢ prod s ∣ k
[PROOFSTEP]
refine
  induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_) fun a =>
    (Multiset.countp_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
⊢ b ∣ k
[PROOFSTEP]
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
⊢ b ∣ k
[PROOFSTEP]
have a_prime := h a (Multiset.mem_cons_self a s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
⊢ b ∣ k
[PROOFSTEP]
have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
⊢ b ∣ k
[PROOFSTEP]
refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
⊢ False
[PROOFSTEP]
have assoc := b_prime.associated_of_dvd a_prime b_div_a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
⊢ False
[PROOFSTEP]
have := uniq a
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : countp (Associated a) (a ::ₘ s) ≤ 1
⊢ False
[PROOFSTEP]
rw [Multiset.countp_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt, Multiset.countp_pos] at this
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : (a : α) → DecidablePred (Associated a)
s✝ : Multiset α
n : α
h✝ : ∀ (a : α), a ∈ s✝ → Prime a
div✝ : ∀ (a : α), a ∈ s✝ → a ∣ n
uniq✝ : ∀ (a : α), countp (Associated a) s✝ ≤ 1
a : α
s : Multiset α
induct :
  ∀ (n : α),
    (∀ (a : α), a ∈ s → Prime a) → (∀ (a : α), a ∈ s → a ∣ n) → (∀ (a : α), countp (Associated a) s ≤ 1) → prod s ∣ n
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → Prime a_1
uniq : ∀ (a_1 : α), countp (Associated a_1) (a ::ₘ s) ≤ 1
k : α
div : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → a_1 ∣ a * k
b : α
b_in_s : b ∈ s
b_div_n : b ∣ a * k
a_prime : Prime a
b_prime : Prime b
b_div_a : b ∣ a
assoc : b ~ᵤ a
this : ¬∃ a_1, a_1 ∈ s ∧ a ~ᵤ a_1
⊢ False
[PROOFSTEP]
exact this ⟨b, b_in_s, assoc.symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
[PROOFSTEP]
classical exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      -- POrting note: was
                -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter, ←
                --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
      intro a
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
      change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
      apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
      apply Multiset.nodup_iff_count_le_one.mp
      exact s.nodup)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∏ p in s, p ∣ n
[PROOFSTEP]
exact
  Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
    (by simpa only [Multiset.map_id', Finset.mem_def] using div)
    (by
      -- POrting note: was
                -- `simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter, ←
                --    Multiset.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup]`
      intro a
      simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
      change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
      apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
      apply Multiset.nodup_iff_count_le_one.mp
      exact s.nodup)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → Prime a
[PROOFSTEP]
simpa only [Multiset.map_id', Finset.mem_def] using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), a ∈ Multiset.map (fun p => p) s.val → a ∣ n
[PROOFSTEP]
simpa only [Multiset.map_id', Finset.mem_def] using div
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
⊢ ∀ (a : α), Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.countp (Associated a) (Multiset.map (fun p => p) s.val) ≤ 1
[PROOFSTEP]
simp only [Multiset.map_id', associated_eq_eq, Multiset.countp_eq_card_filter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (Eq a) s.val) ≤ 1
[PROOFSTEP]
change Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ ↑Multiset.card (Multiset.filter (fun b => a = b) s.val) ≤ 1
[PROOFSTEP]
apply le_of_eq_of_le (Multiset.count_eq_card_filter_eq _ _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.count a s.val ≤ 1
[PROOFSTEP]
apply Multiset.nodup_iff_count_le_one.mp
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Unique αˣ
s : Finset α
n : α
h : ∀ (a : α), a ∈ s → Prime a
div : ∀ (a : α), a ∈ s → a ∣ n
a : α
⊢ Multiset.Nodup s.val
[PROOFSTEP]
exact s.nodup
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset α
⊢ Multiset.prod (Multiset.map Associates.mk 0) = Associates.mk (Multiset.prod 0)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset α
a : α
s : Multiset α
ih : Multiset.prod (Multiset.map Associates.mk s) = Associates.mk (Multiset.prod s)
⊢ Multiset.prod (Multiset.map Associates.mk (a ::ₘ s)) = Associates.mk (Multiset.prod (a ::ₘ s))
[PROOFSTEP]
simp [ih, Associates.mk_mul_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Finset β
f : β → α
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
[PROOFSTEP]
have : (fun i => Associates.mk (f i)) = Associates.mk ∘ f := funext <| fun x => Function.comp_apply
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Finset β
f : β → α
this : (fun i => Associates.mk (f i)) = Associates.mk ∘ f
⊢ ∏ i in p, Associates.mk (f i) = Associates.mk (∏ i in p, f i)
[PROOFSTEP]
rw [Finset.prod_eq_multiset_prod, this, ← Multiset.map_map, prod_mk, ← Finset.prod_eq_multiset_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
[PROOFSTEP]
rw [← Multiset.rel_eq, Multiset.rel_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset α
⊢ Multiset.Rel Associated p q ↔ Multiset.Rel (fun a b => Associates.mk a = Associates.mk b) p q
[PROOFSTEP]
simp only [mk_eq_mk_iff_associated]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ Multiset.prod 0 = 1 ↔ ∀ (a : Associates α), a ∈ 0 → a = 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p : Multiset (Associates α)
⊢ ∀ ⦃a : Associates α⦄ {s : Multiset (Associates α)},
    (Multiset.prod s = 1 ↔ ∀ (a : Associates α), a ∈ s → a = 1) →
      (Multiset.prod (a ::ₘ s) = 1 ↔ ∀ (a_2 : Associates α), a_2 ∈ a ::ₘ s → a_2 = 1)
[PROOFSTEP]
simp (config := { contextual := true }) [mul_eq_one_iff, or_imp, forall_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
haveI := Classical.decEq (Associates α)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
haveI := Classical.decEq α
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p ≤ Multiset.prod (p + (q - p))
⊢ Multiset.prod p ≤ Multiset.prod q
[PROOFSTEP]
rwa [add_tsub_cancel_of_le h] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
[PROOFSTEP]
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
⊢ Multiset.prod p ≤ Multiset.prod (p + (q - p))
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ Multiset.prod p * 1 ≤ Multiset.prod p * Multiset.prod (q - p)
[PROOFSTEP]
exact mul_mono (le_refl p.prod) one_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝ : CancelCommMonoidWithZero α
s✝ : Multiset (Associates α)
p : Associates α
hp : Prime p
a : Associates α
s : Multiset (Associates α)
ih : p ≤ Multiset.prod s → ∃ a, a ∈ s ∧ p ≤ a
h : p ≤ Multiset.prod (a ::ₘ s)
⊢ p ≤ a * Multiset.prod s
[PROOFSTEP]
simpa using h


[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{?u.33371, u_2} D
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
⊢ π₁Toπ₂ ≫ π₂Toπ₃ = 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.36094, u_1} C
inst✝³ : Category.{?u.36098, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
⊢ F.map S.f ≫ F.map S.g = 0
[PROOFSTEP]
rw [← F.map_comp, S.zero, F.map_zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₁ ≫ ((fun S => map S F) Y✝).f = ((fun S => map S F) X✝).f ≫ F.map φ.τ₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₁ ≫ F.map Y✝.f = F.map X✝.f ≫ F.map φ.τ₂
[PROOFSTEP]
simp only [← F.map_comp, φ.comm₁₂]
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₂ ≫ ((fun S => map S F) Y✝).g = ((fun S => map S F) X✝).g ≫ F.map φ.τ₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.44556, u_1} C
inst✝³ : Category.{?u.44560, u_2} D
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Functor.PreservesZeroMorphisms F
X✝ Y✝ : ShortComplex C
φ : X✝ ⟶ Y✝
⊢ F.map φ.τ₂ ≫ F.map Y✝.g = F.map X✝.g ≫ F.map φ.τ₃
[PROOFSTEP]
simp only [← F.map_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.52069, u_1} C
inst✝² : Category.{?u.52073, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝
comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝
⊢ e₁.inv ≫ S₁.f = S₂.f ≫ e₂.inv
[PROOFSTEP]
rw [← cancel_mono e₂.hom, assoc, assoc, e₂.inv_hom_id, comp_id, ← comm₁₂, e₁.inv_hom_id_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.52069, u_1} C
inst✝² : Category.{?u.52073, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
e₁ : S₁.X₁ ≅ S₂.X₁
e₂ : S₁.X₂ ≅ S₂.X₂
e₃ : S₁.X₃ ≅ S₂.X₃
comm₁₂ : autoParam (e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) _auto✝
comm₂₃ : autoParam (e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) _auto✝
⊢ e₂.inv ≫ S₁.g = S₂.g ≫ e₃.inv
[PROOFSTEP]
rw [← cancel_mono e₃.hom, assoc, assoc, e₃.inv_hom_id, comp_id, ← comm₂₃, e₂.inv_hom_id_assoc]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.62853, u_1} C
inst✝² : Category.{?u.62857, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
⊢ S.g.op ≫ S.f.op = 0
[PROOFSTEP]
simp only [← op_comp, S.zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.62853, u_1} C
inst✝² : Category.{?u.62857, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
⊢ 0.op = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₃.op ≫ (op S₁).f = (op S₂).f ≫ φ.τ₂.op
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₃.op ≫ S₁.g.op = S₂.g.op ≫ φ.τ₂.op
[PROOFSTEP]
simp only [← op_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₂.op ≫ (op S₁).g = (op S₂).g ≫ φ.τ₁.op
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.63553, u_1} C
inst✝² : Category.{?u.63557, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
φ : S₁ ⟶ S₂
⊢ φ.τ₂.op ≫ S₁.f.op = S₂.f.op ≫ φ.τ₁.op
[PROOFSTEP]
simp only [← op_comp, φ.comm₁₂]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.64969, u_1} C
inst✝² : Category.{?u.64973, u_2} D
inst✝¹ : HasZeroMorphisms C
S✝ S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S : ShortComplex Cᵒᵖ
⊢ S.g.unop ≫ S.f.unop = 0
[PROOFSTEP]
simp only [← unop_comp, S.zero]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.64969, u_1} C
inst✝² : Category.{?u.64973, u_2} D
inst✝¹ : HasZeroMorphisms C
S✝ S₁ S₂ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S : ShortComplex Cᵒᵖ
⊢ 0.unop = 0
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₃.unop ≫ (unop S₁).f = (unop S₂).f ≫ φ.τ₂.unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₃.unop ≫ S₁.g.unop = S₂.g.unop ≫ φ.τ₂.unop
[PROOFSTEP]
simp only [← unop_comp, φ.comm₂₃]
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ (unop S₁).g = (unop S₂).g ≫ φ.τ₁.unop
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
D : Type u_2
inst✝³ : Category.{?u.65733, u_1} C
inst✝² : Category.{?u.65737, u_2} D
inst✝¹ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
inst✝ : HasZeroMorphisms D
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ S₁.f.unop = S₂.f.unop ≫ φ.τ₁.unop
[PROOFSTEP]
simp only [← unop_comp, φ.comm₁₂]


[GOAL]
α : Type u_1
inst✝ : CommMonoid α
s : Multiset α
a✝ : α
l : List α
a : α
h : a ∈ Quotient.mk (List.isSetoid α) l
⊢ a ∣ prod (Quotient.mk (List.isSetoid α) l)
[PROOFSTEP]
simpa using List.dvd_prod h
[GOAL]
α : Type u_1
inst✝ : CanonicallyOrderedMonoid α
m : Multiset α
l : List α
⊢ prod (Quotient.mk (List.isSetoid α) l) = 1 ↔ ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l → x = 1
[PROOFSTEP]
simpa using List.prod_eq_one_iff l
[GOAL]
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
⊢ 0 < Multiset.prod m ↔ ∀ (x : R), x ∈ m → 0 < x
[PROOFSTEP]
rcases m with ⟨l⟩
[GOAL]
case mk
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < Multiset.prod (Quot.mk Setoid.r l) ↔ ∀ (x : R), x ∈ Quot.mk Setoid.r l → 0 < x
[PROOFSTEP]
rw [Multiset.quot_mk_to_coe'', Multiset.coe_prod]
[GOAL]
case mk
α : Type u_1
R : Type u_2
inst✝¹ : CanonicallyOrderedCommSemiring R
inst✝ : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < List.prod l ↔ ∀ (x : R), x ∈ ↑l → 0 < x
[PROOFSTEP]
exact CanonicallyOrderedCommSemiring.list_prod_pos
[GOAL]
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
h : ∀ (b : α), b ∈ s → Commute a b
⊢ Commute a (sum s)
[PROOFSTEP]
induction s using Quotient.inductionOn
[GOAL]
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (sum (Quotient.mk (List.isSetoid α) a✝))
[PROOFSTEP]
rw [quot_mk_to_coe, coe_sum]
[GOAL]
case h
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
s : Multiset α
a : α
a✝ : List α
h : ∀ (b : α), b ∈ Quotient.mk (List.isSetoid α) a✝ → Commute a b
⊢ Commute a (List.sum a✝)
[PROOFSTEP]
exact Commute.list_sum_right _ _ h


[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s : Finset γ
f : γ → α
g : γ → β
this : DecidableEq γ
⊢ ∀ ⦃a : γ⦄ {s : Finset γ},
    ¬a ∈ s →
      (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x) →
        (∏ x in insert a s, f x, ∏ x in insert a s, g x) = ∏ x in insert a s, (f x, g x)
[PROOFSTEP]
simp (config := { contextual := true }) [Prod.ext_iff]
[GOAL]
I : Type u_1
inst✝² : DecidableEq I
Z : I → Type u_2
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
⊢ ∏ i : I, Pi.mulSingle i (f i) = f
[PROOFSTEP]
ext a
[GOAL]
case h
I : Type u_1
inst✝² : DecidableEq I
Z : I → Type u_2
inst✝¹ : (i : I) → CommMonoid (Z i)
inst✝ : Fintype I
f : (i : I) → Z i
a : I
⊢ Finset.prod univ (fun i => Pi.mulSingle i (f i)) a = f a
[PROOFSTEP]
simp
[GOAL]
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
⊢ g = h
[PROOFSTEP]
cases nonempty_fintype I
[GOAL]
case intro
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
⊢ g = h
[PROOFSTEP]
ext k
[GOAL]
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ↑g k = ↑h k
[PROOFSTEP]
rw [← Finset.univ_prod_mulSingle k, g.map_prod, h.map_prod]
[GOAL]
case intro.h
I : Type u_1
inst✝³ : DecidableEq I
Z : I → Type u_2
inst✝² : (i : I) → CommMonoid (Z i)
inst✝¹ : Finite I
G : Type u_3
inst✝ : CommMonoid G
g h : ((i : I) → Z i) →* G
H : ∀ (i : I) (x : Z i), ↑g (Pi.mulSingle i x) = ↑h (Pi.mulSingle i x)
val✝ : Fintype I
k : (i : I) → Z i
⊢ ∏ x : I, ↑g (Pi.mulSingle x (k x)) = ∏ x : I, ↑h (Pi.mulSingle x (k x))
[PROOFSTEP]
simp only [H]