[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
n : ℕ
f : C ⟶ D
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => n • Hom.f f i) i ≫ d D i j = d C i j ≫ (fun i => n • Hom.f f i) j
[PROOFSTEP]
simp [Preadditive.nsmul_comp, Preadditive.comp_nsmul]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
n : ℤ
f : C ⟶ D
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => n • Hom.f f i) i ≫ d D i j = d C i j ≫ (fun i => n • Hom.f f i) j
[PROOFSTEP]
simp [Preadditive.zsmul_comp, Preadditive.comp_zsmul]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ 0.f = 0
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x y : C ⟶ D), (x + y).f = x.f + y.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D), (-x).f = -x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x y : C ⟶ D), (x - y).f = x.f - y.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℕ), (n • x).f = n • x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
⊢ ∀ (x : C ⟶ D) (n : ℤ), (n • x).f = n • x.f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
⊢ (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f ((f + f') ≫ g) i✝ = Hom.f (f ≫ g + f' ≫ g) i✝
[PROOFSTEP]
simp only [comp_f, add_f_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f f' : x✝² ⟶ x✝¹
g : x✝¹ ⟶ x✝
i✝ : ι
⊢ (Hom.f f i✝ + Hom.f f' i✝) ≫ Hom.f g i✝ = Hom.f f i✝ ≫ Hom.f g i✝ + Hom.f f' i✝ ≫ Hom.f g i✝
[PROOFSTEP]
rw [Preadditive.add_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
⊢ f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f (f ≫ (g + g')) i✝ = Hom.f (f ≫ g + f ≫ g') i✝
[PROOFSTEP]
simp only [comp_f, add_f_apply]
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
x✝² x✝¹ x✝ : HomologicalComplex V c
f : x✝² ⟶ x✝¹
g g' : x✝¹ ⟶ x✝
i✝ : ι
⊢ Hom.f f i✝ ≫ (Hom.f g i✝ + Hom.f g' i✝) = Hom.f f i✝ ≫ Hom.f g i✝ + Hom.f f i✝ ≫ Hom.f g' i✝
[PROOFSTEP]
rw [Preadditive.comp_add]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ (homologyFunctor V c i).map (f + g) = (homologyFunctor V c i).map f + (homologyFunctor V c i).map g
[PROOFSTEP]
dsimp [homologyFunctor]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (f + g) i)
      (Hom.sqFrom (f + g) i) (_ : (Hom.sqTo (f + g) i).right = (Hom.sqTo (f + g) i).right) =
    homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
        (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) +
      homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
        (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right)
[PROOFSTEP]
ext
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ homology.π (dTo x✝¹ i) (dFrom x✝¹ i) (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) ≫
      homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo (f + g) i)
        (Hom.sqFrom (f + g) i) (_ : (Hom.sqTo (f + g) i).right = (Hom.sqTo (f + g) i).right) =
    homology.π (dTo x✝¹ i) (dFrom x✝¹ i) (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) ≫
      (homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
          (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right) +
        homology.map (_ : dTo x✝¹ i ≫ dFrom x✝¹ i = 0) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
          (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right))
[PROOFSTEP]
simp only [homology.π_map, Preadditive.comp_add, ← Preadditive.add_comp]
[GOAL]
case p
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) ≫ homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0) =
    (kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)) ≫
      homology.π (dTo x✝ i) (dFrom x✝ i) (_ : dTo x✝ i ≫ dFrom x✝ i = 0)
[PROOFSTEP]
congr
[GOAL]
case p.e_a
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) = kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)
[PROOFSTEP]
ext
[GOAL]
case p.e_a.h
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h k : D ⟶ E
i : ι
inst✝³ : HasImages V
inst✝² : HasImageMaps V
inst✝¹ : HasEqualizers V
inst✝ : HasCokernels V
x✝¹ x✝ : HomologicalComplex V c
f g : x✝¹ ⟶ x✝
⊢ kernelSubobjectMap (Hom.sqFrom (f + g) i) ≫ Subobject.arrow (kernelSubobject (dFrom x✝ i)) =
    (kernelSubobjectMap (Hom.sqFrom f i) + kernelSubobjectMap (Hom.sqFrom g i)) ≫
      Subobject.arrow (kernelSubobject (dFrom x✝ i))
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
w : ¬ComplexShape.Rel c i j
⊢ (fun i j => F.map (d C i j)) i j = 0
[PROOFSTEP]
dsimp only
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
w : ¬ComplexShape.Rel c i j
⊢ F.map (d C i j) = 0
[PROOFSTEP]
rw [C.shape _ _ w, F.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C✝ D E : HomologicalComplex V c✝
f g : C✝ ⟶ D
h k✝ : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
x✝¹ : ComplexShape.Rel c i j
x✝ : ComplexShape.Rel c j k
⊢ (fun i j => F.map (d C i j)) i j ≫ (fun i j => F.map (d C i j)) j k = 0
[PROOFSTEP]
rw [← F.map_comp, C.d_comp_d, F.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ (fun i => F.map (Hom.f f i)) i ≫
      d ((fun C => HomologicalComplex.mk (fun i => F.obj (X C i)) fun i j => F.map (d C i j)) Y✝) i j =
    d ((fun C => HomologicalComplex.mk (fun i => F.obj (X C i)) fun i j => F.map (d C i j)) X✝) i j ≫
      (fun i => F.map (Hom.f f i)) j
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
W : Type u_2
inst✝² : Category.{?u.55346, u_2} W
inst✝¹ : Preadditive W
F : V ⥤ W
inst✝ : Additive F
c : ComplexShape ι
X✝ Y✝ : HomologicalComplex V c
f : X✝ ⟶ Y✝
i j : ι
x✝ : ComplexShape.Rel c i j
⊢ F.map (Hom.f f i) ≫ F.map (d Y✝ i j) = F.map (d X✝ i j) ≫ F.map (Hom.f f j)
[PROOFSTEP]
rw [← F.map_comp, ← F.map_comp, f.comm]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.91619, u_2} W
inst✝² : Preadditive W
F : V ⥤ W
inst✝¹ : Additive F
inst✝ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
⊢ ∀ [inst : IsIso ((mapHomologicalComplex F c).map f)], IsIso f
[PROOFSTEP]
intro
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
  IsIso.of_iso ((HomologicalComplex.eval W c n).mapIso (asIso ((F.mapHomologicalComplex c).map f)))
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
this : ∀ (n : ι), IsIso (F.map (Hom.f f n))
⊢ IsIso f
[PROOFSTEP]
haveI := fun n => isIso_of_reflects_iso (f.f n) F
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{?u.91619, u_2} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : Additive F
inst✝¹ : ReflectsIsomorphisms F
c : ComplexShape ι
A✝ B✝ : HomologicalComplex V c
f : A✝ ⟶ B✝
inst✝ : IsIso ((mapHomologicalComplex F c).map f)
this✝ : ∀ (n : ι), IsIso (F.map (Hom.f f n))
this : ∀ (n : ι), IsIso (Hom.f f n)
⊢ IsIso f
[PROOFSTEP]
exact HomologicalComplex.Hom.isIso_of_components f
[GOAL]
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝² : Category.{u_3, u_2} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : Functor.Additive F
⊢ mapHomologicalComplex (𝟙 F) c = 𝟙 (Functor.mapHomologicalComplex F c)
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁴ : Category.{u_3, u_2} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
⊢ mapHomologicalComplex (α ≫ β) c = mapHomologicalComplex α c ≫ mapHomologicalComplex β c
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C✝ D✝ E : HomologicalComplex V c✝
f✝ g : C✝ ⟶ D✝
h k : D✝ ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
c : ComplexShape ι
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ⟶ G
C D : HomologicalComplex V c
f : C ⟶ D
⊢ (Functor.mapHomologicalComplex F c).map f ≫ app (mapHomologicalComplex α c) D =
    app (mapHomologicalComplex α c) C ≫ (Functor.mapHomologicalComplex G c).map f
[PROOFSTEP]
aesop_cat
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.106581, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ≅ G
c : ComplexShape ι
⊢ NatTrans.mapHomologicalComplex α.hom c ≫ NatTrans.mapHomologicalComplex α.inv c =
    𝟙 (Functor.mapHomologicalComplex F c)
[PROOFSTEP]
simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id, NatTrans.mapHomologicalComplex_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝³ : Category.{?u.106581, u_2} W
inst✝² : Preadditive W
F G : V ⥤ W
inst✝¹ : Functor.Additive F
inst✝ : Functor.Additive G
α : F ≅ G
c : ComplexShape ι
⊢ NatTrans.mapHomologicalComplex α.inv c ≫ NatTrans.mapHomologicalComplex α.hom c =
    𝟙 (Functor.mapHomologicalComplex G c)
[PROOFSTEP]
simp only [← NatTrans.mapHomologicalComplex_comp, α.inv_hom_id, NatTrans.mapHomologicalComplex_id]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{?u.119648, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0
[PROOFSTEP]
rw [← F.map_comp, sq n, Functor.map_zero]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ (Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq) =
    of (fun n => F.obj (X n)) (fun n => F.map (d n))
      (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0)
[PROOFSTEP]
refine' HomologicalComplex.ext rfl _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ ∀ (i j : α),
    ComplexShape.Rel (ComplexShape.down α) i j →
      HomologicalComplex.d ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) i j ≫
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) j =
                HomologicalComplex.X
                  (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                    (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
                  j) =
        eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) i =
                HomologicalComplex.X
                  (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                    (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
                  i) ≫
          HomologicalComplex.d
            (of (fun n => F.obj (X n)) (fun n => F.map (d n))
              (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
            i j
[PROOFSTEP]
rintro i j (rfl : j + 1 = i)
[GOAL]
ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
W : Type u_2
inst✝⁵ : Category.{u_4, u_2} W
inst✝⁴ : Preadditive W
α : Type u_3
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : V ⥤ W
inst✝ : Functor.Additive F
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
j : α
⊢ HomologicalComplex.d ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) (j + 1) j ≫
      eqToHom
        (_ :
          HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) j =
            HomologicalComplex.X
              (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
              j) =
    eqToHom
        (_ :
          HomologicalComplex.X ((Functor.mapHomologicalComplex F (ComplexShape.down α)).obj (of X d sq)) (j + 1) =
            HomologicalComplex.X
              (of (fun n => F.obj (X n)) (fun n => F.map (d n))
                (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
              (j + 1)) ≫
      HomologicalComplex.d
        (of (fun n => F.obj (X n)) (fun n => F.map (d n))
          (_ : ∀ (n : α), (fun n => F.map (d n)) (n + 1) ≫ (fun n => F.map (d n)) n = 0))
        (j + 1) j
[PROOFSTEP]
simp only [CategoryTheory.Functor.mapHomologicalComplex_obj_d, of_d, eqToHom_refl, comp_id, id_comp]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) i =
    HomologicalComplex.X ((F ⋙ single W c j).obj X) i
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ HomologicalComplex.X ((F ⋙ single W c j).obj X) i =
    HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) i
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
⊢ ((Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
        else 0) ≫
      Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
        else 0) =
    𝟙 ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ Hom.f
      ((Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                  HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
          else 0) ≫
        Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                  HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
          else 0)
      i =
    Hom.f (𝟙 ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X)) i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ ((if h : i = j then eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) else 0) ≫
      if h : i = j then eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) else 0) =
    𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) ≫
      eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) =
    𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (F.obj (if i = j then X else 0))
[PROOFSTEP]
rw [zero_comp, if_neg h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 = 𝟙 (F.obj 0)
[PROOFSTEP]
exact (zero_of_source_iso_zero _ F.mapZeroObject).symm
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
⊢ ((Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
        else 0) ≫
      Hom.mk fun i =>
        if h : i = j then
          eqToHom
            (_ :
              HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
        else 0) =
    𝟙 ((F ⋙ single W c j).obj X)
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ Hom.f
      ((Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                  HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
          else 0) ≫
        Hom.mk fun i =>
          if h : i = j then
            eqToHom
              (_ :
                HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                  HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
          else 0)
      i =
    Hom.f (𝟙 ((F ⋙ single W c j).obj X)) i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
⊢ ((if h : i = j then eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) else 0) ≫
      if h : i = j then eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) else 0) =
    𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : i = j
⊢ eqToHom (_ : (if i = j then F.obj X else 0) = F.obj (if i = j then X else 0)) ≫
      eqToHom (_ : F.obj (if i = j then X else 0) = if i = j then F.obj X else 0) =
    𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 ≫ 0 = 𝟙 (if i = j then F.obj X else 0)
[PROOFSTEP]
rw [zero_comp, if_neg h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X : V
i : ι
h : ¬i = j
⊢ 0 = 𝟙 0
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single V c j ⋙ Functor.mapHomologicalComplex F c).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                else 0)
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                else 0))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                else 0)
              (Hom.mk fun i =>
                if h : i = j then
                  eqToHom
                    (_ :
                      HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                else 0))
          X✝).hom ≫
      (F ⋙ single W c j).map f
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
⊢ Hom.f
      ((single V c j ⋙ Functor.mapHomologicalComplex F c).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                          HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                  else 0)
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                          HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                  else 0))
            Y✝).hom)
      i =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i =
                          HomologicalComplex.X ((single W c j).obj (F.obj X)) i)
                  else 0)
                (Hom.mk fun i =>
                  if h : i = j then
                    eqToHom
                      (_ :
                        HomologicalComplex.X ((single W c j).obj (F.obj X)) i =
                          HomologicalComplex.X ((Functor.mapHomologicalComplex F c).obj ((single V c j).obj X)) i)
                  else 0))
            X✝).hom ≫
        (F ⋙ single W c j).map f)
      i
[PROOFSTEP]
dsimp
[GOAL]
case h
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
⊢ (F.map
        (if h : i = j then
          eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) X✝) i = X✝) ≫
            f ≫ eqToHom (_ : Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) Y✝) i)
        else 0) ≫
      if h : i = j then eqToHom (_ : F.obj (if i = j then Y✝ else 0) = if i = j then F.obj Y✝ else 0) else 0) =
    (if h : i = j then eqToHom (_ : F.obj (if i = j then X✝ else 0) = if i = j then F.obj X✝ else 0) else 0) ≫
      if h : i = j then
        eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj X✝)) i = F.obj X✝) ≫
          F.map f ≫
            eqToHom (_ : F.obj Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj Y✝)) i)
      else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ F.map
        (eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) X✝) i = X✝) ≫
          f ≫ eqToHom (_ : Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) Y✝) i)) ≫
      eqToHom (_ : F.obj (if i = j then Y✝ else 0) = if i = j then F.obj Y✝ else 0) =
    eqToHom (_ : F.obj (if i = j then X✝ else 0) = if i = j then F.obj X✝ else 0) ≫
      eqToHom (_ : X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj X✝)) i = F.obj X✝) ≫
        F.map f ≫
          eqToHom (_ : F.obj Y✝ = X ((fun A => mk (fun i => if i = j then A else 0) fun i j_1 => 0) (F.obj Y✝)) i)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c✝ : ComplexShape ι
C D E : HomologicalComplex V c✝
f✝ g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.125669, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : ¬i = j
⊢ F.map 0 ≫ 0 = 0 ≫ 0
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.161257, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) j =
    HomologicalComplex.X ((F ⋙ single W c j).obj X) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).hom X) j =
    eqToHom (_ : F.obj (if j = j then X else 0) = if j = j then F.obj X else 0)
[PROOFSTEP]
simp [singleMapHomologicalComplex]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
i j : ι
h : i ≠ j
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).hom X) i = 0
[PROOFSTEP]
simp [singleMapHomologicalComplex, h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.177119, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ HomologicalComplex.X ((F ⋙ single W c j).obj X) j =
    HomologicalComplex.X ((single V c j ⋙ Functor.mapHomologicalComplex F c).obj X) j
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
j : ι
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).inv X) j =
    eqToHom (_ : (if j = j then F.obj X else 0) = F.obj (if j = j then X else 0))
[PROOFSTEP]
simp [singleMapHomologicalComplex]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{u_3, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
i j : ι
h : i ≠ j
X : V
⊢ Hom.f (NatTrans.app (singleMapHomologicalComplex F c j).inv X) i = 0
[PROOFSTEP]
simp [singleMapHomologicalComplex, h]
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) =
    𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      Nat.zero =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) =
    𝟙 ((F ⋙ single₀ W).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      Nat.zero =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (isZero_zero _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          X✝).hom ≫
      (F ⋙ single₀ W).map f
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      Nat.zero =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.192981, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
n✝ : ℕ
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      (Nat.succ n✝) =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙
                      (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.down ℕ)).obj X)
                        0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      (Nat.succ n✝)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) =
    𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      Nat.zero =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (IsZero.of_iso (isZero_zero _) F.mapZeroObject) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ ((Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
      Hom.mk fun i =>
        match i with
        | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
        | Nat.succ n => (Functor.mapZeroObject F).hom) =
    𝟙 ((F ⋙ single₀ W).obj X)
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      Nat.zero =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X : V
n✝ : ℕ
⊢ Hom.f
      ((Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).inv) ≫
        Hom.mk fun i =>
          match i with
          | 0 => 𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
          | Nat.succ n => (Functor.mapZeroObject F).hom)
      (Nat.succ n✝) =
    Hom.f (𝟙 ((F ⋙ single₀ W).obj X)) (Nat.succ n✝)
[PROOFSTEP]
exact IsZero.eq_of_src (isZero_zero _) _ _
[GOAL]
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ (single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
      ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          Y✝).hom =
    ((fun X =>
            Iso.mk
              (Hom.mk fun i =>
                match i with
                | 0 =>
                  𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).hom)
              (Hom.mk fun i =>
                match i with
                | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                | Nat.succ n => (Functor.mapZeroObject F).inv))
          X✝).hom ≫
      (F ⋙ single₀ W).map f
[PROOFSTEP]
ext (_ | _)
[GOAL]
case h.zero
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      Nat.zero =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h.succ
ι : Type u_1
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g : C ⟶ D
h k : D ⟶ E
i : ι
inst✝⁴ : HasZeroObject V
W : Type u_2
inst✝³ : Category.{?u.241808, u_2} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
X✝ Y✝ : V
f : X✝ ⟶ Y✝
n✝ : ℕ
⊢ Hom.f
      ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).map f ≫
        ((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            Y✝).hom)
      (Nat.succ n✝) =
    Hom.f
      (((fun X =>
              Iso.mk
                (Hom.mk fun i =>
                  match i with
                  | 0 =>
                    𝟙 (HomologicalComplex.X ((single₀ V ⋙ Functor.mapHomologicalComplex F (ComplexShape.up ℕ)).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).hom)
                (Hom.mk fun i =>
                  match i with
                  | 0 => 𝟙 (HomologicalComplex.X ((F ⋙ single₀ W).obj X) 0)
                  | Nat.succ n => (Functor.mapZeroObject F).inv))
            X✝).hom ≫
        (F ⋙ single₀ W).map f)
      (Nat.succ n✝)
[PROOFSTEP]
simp


[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ MulActionHom.toFun
      { toFun := src✝.toFun,
        map_smul' :=
          (_ :
            ∀ (r : R) (x : A), AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
      0 =
    0
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(MulActionHom.toFun
          { toFun := src✝.toFun,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : A),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
          0)
      a =
    ↑0 a
[PROOFSTEP]
exact zero_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (x y : A),
    MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        (x * y) =
      MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          x *
        MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b : A
⊢ MulActionHom.toFun
      {
          toMulActionHom :=
            { toFun := src✝.toFun,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : A),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
          map_zero' :=
            (_ :
              MulActionHom.toFun
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                  0 =
                0),
          map_add' :=
            (_ :
              ∀ (x y : A),
                AddHom.toFun src✝.toAddHom (x + y) =
                  AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
      (a * b) =
    MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        a *
      MulActionHom.toFun
        {
            toMulActionHom :=
              { toFun := src✝.toFun,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : A),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
            map_zero' :=
              (_ :
                MulActionHom.toFun
                    { toFun := src✝.toFun,
                      map_smul' :=
                        (_ :
                          ∀ (r : R) (x : A),
                            AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) =
                    AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
        b
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b c : A
⊢ ↑(MulActionHom.toFun
          {
              toMulActionHom :=
                { toFun := src✝.toFun,
                  map_smul' :=
                    (_ :
                      ∀ (r : R) (x : A),
                        AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
              map_zero' :=
                (_ :
                  MulActionHom.toFun
                      { toFun := src✝.toFun,
                        map_smul' :=
                          (_ :
                            ∀ (r : R) (x : A),
                              AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) =
                      AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
          (a * b))
      c =
    ↑(MulActionHom.toFun
            {
                toMulActionHom :=
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
                map_zero' :=
                  (_ :
                    MulActionHom.toFun
                        { toFun := src✝.toFun,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : A),
                                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
            a *
          MulActionHom.toFun
            {
                toMulActionHom :=
                  { toFun := src✝.toFun,
                    map_smul' :=
                      (_ :
                        ∀ (r : R) (x : A),
                          AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) },
                map_zero' :=
                  (_ :
                    MulActionHom.toFun
                        { toFun := src✝.toFun,
                          map_smul' :=
                            (_ :
                              ∀ (r : R) (x : A),
                                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) }.toMulActionHom
            b)
      c
[PROOFSTEP]
exact mul_assoc a b c
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ Commute (mulLeft R a) (mulRight R b)
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b c : A
⊢ ↑(mulLeft R a * mulRight R b) c = ↑(mulRight R b * mulLeft R a) c
[PROOFSTEP]
exact (mul_assoc a c b).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulLeft R (a * b) = comp (mulLeft R a) (mulLeft R b)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulLeft R (a * b)) x✝ = ↑(comp (mulLeft R a) (mulLeft R b)) x✝
[PROOFSTEP]
simp only [mulLeft_apply, comp_apply, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b : A
⊢ mulRight R (a * b) = comp (mulRight R b) (mulRight R a)
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : SMulCommClass R A A
inst✝ : IsScalarTower R A A
a b x✝ : A
⊢ ↑(mulRight R (a * b)) x✝ = ↑(comp (mulRight R b) (mulRight R a)) x✝
[PROOFSTEP]
simp only [mulRight_apply, comp_apply, mul_assoc]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ AddHom.toFun src✝.toAddHom 1 = 1
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(AddHom.toFun src✝.toAddHom 1) a = ↑1 a
[PROOFSTEP]
exact one_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (x y : A),
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (x * y) =
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } x *
        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } y
[PROOFSTEP]
intro a b
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b : A
⊢ OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b
[PROOFSTEP]
ext c
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a b c : A
⊢ ↑(OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b)) c =
    ↑(OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b)
      c
[PROOFSTEP]
exact mul_assoc a b c
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : A),
                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                  OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
      0 =
    0
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
a : A
⊢ ↑(OneHom.toFun
          (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (a b : A),
                    OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
          0)
      a =
    ↑0 a
[PROOFSTEP]
exact zero_mul a
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
⊢ ∀ (r : R),
    OneHom.toFun
        (↑↑{
              toMonoidHom :=
                { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                  map_mul' :=
                    (_ :
                      ∀ (a b : A),
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                            (a * b) =
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                            OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                              b) },
              map_zero' :=
                (_ :
                  OneHom.toFun
                      (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                          map_mul' :=
                            (_ :
                              ∀ (a b : A),
                                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                    (a * b) =
                                  OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                                    OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
                      0 =
                    0),
              map_add' :=
                (_ :
                  ∀ (x y : A),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
        (↑(algebraMap R A) r) =
      ↑(algebraMap R (End R A)) r
[PROOFSTEP]
intro r
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
r : R
⊢ OneHom.toFun
      (↑↑{
            toMonoidHom :=
              { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (a b : A),
                      OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } (a * b) =
                        OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) },
            map_zero' :=
              (_ :
                OneHom.toFun
                    (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                        map_mul' :=
                          (_ :
                            ∀ (a b : A),
                              OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                  (a * b) =
                                OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                    a *
                                  OneHom.toFun
                                    { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } b) })
                    0 =
                  0),
            map_add' :=
              (_ :
                ∀ (x y : A),
                  AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
      (↑(algebraMap R A) r) =
    ↑(algebraMap R (End R A)) r
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
src✝ : A →ₗ[R] A →ₗ[R] A := mul R A
r : R
a : A
⊢ ↑(OneHom.toFun
          (↑↑{
                toMonoidHom :=
                  { toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                    map_mul' :=
                      (_ :
                        ∀ (a b : A),
                          OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                              (a * b) =
                            OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                              OneHom.toFun { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                b) },
                map_zero' :=
                  (_ :
                    OneHom.toFun
                        (↑{ toOneHom := { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) },
                            map_mul' :=
                              (_ :
                                ∀ (a b : A),
                                  OneHom.toFun
                                      { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                      (a * b) =
                                    OneHom.toFun
                                        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) } a *
                                      OneHom.toFun
                                        { toFun := src✝.toFun, map_one' := (_ : AddHom.toFun src✝.toAddHom 1 = 1) }
                                        b) })
                        0 =
                      0),
                map_add' :=
                  (_ :
                    ∀ (x y : A),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) })
          (↑(algebraMap R A) r))
      a =
    ↑(↑(algebraMap R (End R A)) r) a
[PROOFSTEP]
exact (Algebra.smul_def r a).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulLeft R a = 0 ↔ a = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulLeft R a = 0 → a = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a = 0 → mulLeft R a = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulLeft R a = 0
⊢ a = 0
[PROOFSTEP]
rw [← mul_one a, ← @mulLeft_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R a = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulLeft R 0 = 0
[PROOFSTEP]
exact mulLeft_zero_eq_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulRight R a = 0 ↔ a = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ mulRight R a = 0 → a = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
⊢ a = 0 → mulRight R a = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : mulRight R a = 0
⊢ a = 0
[PROOFSTEP]
rw [← one_mul a, ← @mulRight_apply R _ _ _ _ _ _ a 1, h, LinearMap.zero_apply]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulRight R a = 0
[PROOFSTEP]
rw [h]
[GOAL]
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
h : a = 0
⊢ mulRight R 0 = 0
[PROOFSTEP]
exact mulRight_zero_eq_zero
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mulLeft R 1 = id
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulLeft R 1) x✝ = ↑id x✝
[PROOFSTEP]
simp only [LinearMap.id_coe, one_mul, id.def, mulLeft_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ mulRight R 1 = id
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x✝ : A
⊢ ↑(mulRight R 1) x✝ = ↑id x✝
[PROOFSTEP]
simp only [LinearMap.id_coe, mul_one, id.def, mulRight_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulLeft R a ^ n = mulLeft R (a ^ n)
[PROOFSTEP]
simpa only [mulLeft, ← Algebra.coe_lmul_eq_mul] using ((Algebra.lmul R A).map_pow a n).symm
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ mulRight R a ^ n = mulRight R (a ^ n)
[PROOFSTEP]
simp only [mulRight, ← Algebra.coe_lmul_eq_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
n : ℕ
⊢ ↑(flip (mul R A)) a ^ n = ↑(flip (mul R A)) (a ^ n)
[PROOFSTEP]
exact LinearMap.coe_injective (((mulRight R a).coe_pow n).symm ▸ mul_right_iterate a n)
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(mulLeft R x)
[PROOFSTEP]
exact mul_right_injective₀ hx
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(mulRight R x)
[PROOFSTEP]
exact mul_left_injective₀ hx
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
letI : Nontrivial A := ⟨⟨x, 0, hx⟩⟩
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
letI := NoZeroDivisors.to_isDomain A
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : NoZeroDivisors A
x : A
hx : x ≠ 0
this✝ : Nontrivial A := { exists_pair_ne := Exists.intro x (Exists.intro 0 hx) }
this : IsDomain A := NoZeroDivisors.to_isDomain A
⊢ Function.Injective ↑(↑(mul R A) x)
[PROOFSTEP]
exact mul_right_injective₀ hx


[GOAL]
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
⊢ r • pi s t ⊆ pi s (r • t)
[PROOFSTEP]
rintro x ⟨y, h, rfl⟩ i hi
[GOAL]
case intro.intro
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
y : (i : ι) → R i
h : y ∈ pi s t
i : ι
hi : i ∈ s
⊢ (fun x => r • x) y i ∈ (r • t) i
[PROOFSTEP]
exact smul_mem_smul_set (h i hi)
[GOAL]
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
⊢ x ∈ r • pi univ t
[PROOFSTEP]
refine' ⟨fun i ↦ Classical.choose (h i <| Set.mem_univ _), fun i _ ↦ _, funext fun i ↦ _⟩
[GOAL]
case refine'_1
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
i : ι
x✝ : i ∈ univ
⊢ (fun i => Classical.choose (_ : x i ∈ (r • t) i)) i ∈ t i
[PROOFSTEP]
exact (Classical.choose_spec (h i <| Set.mem_univ i)).left
[GOAL]
case refine'_2
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
i : ι
⊢ (fun x => r • x) (fun i => Classical.choose (_ : x i ∈ (r • t) i)) i = x i
[PROOFSTEP]
exact (Classical.choose_spec (h i <| Set.mem_univ i)).right


[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T ≤ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
rw [Submodule.mul_le]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ∀ (m : A), m ∈ ↑toSubmodule S → ∀ (n : A), n ∈ ↑toSubmodule T → m * n ∈ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
intro y hy z hz
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
show y * z ∈ S ⊔ T
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
y : A
hy : y ∈ ↑toSubmodule S
z : A
hz : z ∈ ↑toSubmodule T
⊢ y * z ∈ S ⊔ T
[PROOFSTEP]
exact mul_mem (Algebra.mem_sup_left hy) (Algebra.mem_sup_right hz)
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S = ↑toSubmodule S
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule S ≤ ↑toSubmodule S
[PROOFSTEP]
refine' (mul_toSubmodule_le _ _).trans_eq _
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ S) = ↑toSubmodule S
[PROOFSTEP]
rw [sup_idem]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ ↑toSubmodule S ≤ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
intro x hx1
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
x : A
hx1 : x ∈ ↑toSubmodule S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule S
[PROOFSTEP]
exact Submodule.mul_mem_mul hx1 (show (1 : A) ∈ S from one_mem S)
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule S * ↑toSubmodule T = ↑toSubmodule (S ⊔ T)
[PROOFSTEP]
refine' le_antisymm (mul_toSubmodule_le _ _) _
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
⊢ ↑toSubmodule (S ⊔ T) ≤ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rintro x (hx : x ∈ Algebra.adjoin R (S ∪ T : Set A))
[GOAL]
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
refine' Algebra.adjoin_induction hx (fun x hx => _) (fun r => _) (fun _ _ => Submodule.add_mem _) fun x y hx hy => _
[GOAL]
case refine'_1
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hx : x ∈ ↑S ∪ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
cases' hx with hxS hxT
[GOAL]
case refine'_1.inl
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← mul_one x]
[GOAL]
case refine'_1.inl
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x * 1 ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)
[GOAL]
case refine'_1.inr
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← one_mul x]
[GOAL]
case refine'_1.inr
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxT : x ∈ ↑T
⊢ 1 * x ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) hxT
[GOAL]
case refine'_2
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rw [← one_mul (algebraMap _ _ _)]
[GOAL]
case refine'_2
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x : A
hx : x ∈ Algebra.adjoin R (↑S ∪ ↑T)
r : R
⊢ 1 * ↑(algebraMap R A) r ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
exact Submodule.mul_mem_mul (show (1 : A) ∈ S from one_mem S) (algebraMap_mem T _)
[GOAL]
case refine'_3
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
have := Submodule.mul_mem_mul hx hy
[GOAL]
case refine'_3
R✝ : Type u_1
A✝ : Type u_2
inst✝⁵ : CommSemiring R✝
inst✝⁴ : Semiring A✝
inst✝³ : Algebra R✝ A✝
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx✝ : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x y : A
hx : x ∈ ↑toSubmodule S * ↑toSubmodule T
hy : y ∈ ↑toSubmodule S * ↑toSubmodule T
this : x * y ∈ ↑toSubmodule S * ↑toSubmodule T * (↑toSubmodule S * ↑toSubmodule T)
⊢ x * y ∈ ↑toSubmodule S * ↑toSubmodule T
[PROOFSTEP]
rwa [mul_assoc, mul_comm _ (Subalgebra.toSubmodule T), ← mul_assoc _ _ (Subalgebra.toSubmodule S), mul_self,
  mul_comm (Subalgebra.toSubmodule T), ← mul_assoc, mul_self] at this


[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ ↑(algebraMap R A) x ∈ U.carrier
[PROOFSTEP]
rw [algebraMap_apply R S A]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U : Subalgebra S A
x : R
⊢ ↑(algebraMap S A) (↑(algebraMap R S) x) ∈ U.carrier
[PROOFSTEP]
exact U.algebraMap_mem _
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
⊢ ↑(restrictScalars R ⊤) = ↑⊤
[PROOFSTEP]
dsimp
  -- porting note: why does `rfl` not work instead of `by dsimp`?
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S B
inst✝² : Algebra R B
inst✝¹ : IsScalarTower R S A
inst✝ : IsScalarTower R S B
U V : Subalgebra S A
H : restrictScalars R U = restrictScalars R V
x : A
⊢ x ∈ U ↔ x ∈ V
[PROOFSTEP]
rw [← mem_restrictScalars R, H, mem_restrictScalars]
[GOAL]
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
⊢ LinearMap.range (toAlgHom R { x // x ∈ S } A) = ↑toSubmodule S
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ LinearMap.range (toAlgHom R { x // x ∈ S } A) ↔ x✝ ∈ ↑toSubmodule S
[PROOFSTEP]
simp only [← Submodule.range_subtype (Subalgebra.toSubmodule S), LinearMap.mem_range, IsScalarTower.coe_toAlgHom',
  Subalgebra.mem_toSubmodule]
[GOAL]
case h
R : Type u
S✝ : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ (∃ y, ↑(algebraMap { x // x ∈ S } A) y = x✝) ↔ ∃ y, ↑(Submodule.subtype (↑toSubmodule S)) y = x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ z ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ↑(algebraMap S A) ∪ t)
[PROOFSTEP]
suffices Set.range (algebraMap (toAlgHom R S A).range A) = Set.range (algebraMap S A) by rw [this]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
this : Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) = Set.range ↑(algebraMap S A)
⊢ z ∈ Subsemiring.closure (Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ∪ t) ↔
    z ∈ Subsemiring.closure (Set.range ↑(algebraMap S A) ∪ t)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z : A
⊢ Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) = Set.range ↑(algebraMap S A)
[PROOFSTEP]
ext z
[GOAL]
case h
R : Type u
S : Type v
A : Type w
B : Type u₁
M : Type v₁
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : CommSemiring A
inst✝³ : Algebra R S
inst✝² : Algebra S A
inst✝¹ : Algebra R A
inst✝ : IsScalarTower R S A
t : Set A
z✝ z : A
⊢ z ∈ Set.range ↑(algebraMap { x // x ∈ AlgHom.range (toAlgHom R S A) } A) ↔ z ∈ Set.range ↑(algebraMap S A)
[PROOFSTEP]
exact ⟨fun ⟨⟨_, y, h1⟩, h2⟩ ↦ ⟨y, h2 ▸ h1⟩, fun ⟨y, hy⟩ ↦ ⟨⟨z, y, hy⟩, rfl⟩⟩