mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).ker ≤ kerTotal R S

Tactic:
conv_rhs => rw [← (KaehlerDifferential.kerTotal R S).ker_mkQ]
    rw [← KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination]
    exact LinearMap.ker_le_ker_comp _ _

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ ∀ {X Y : HomologicalComplex C c} (f : X ⟶ Y),
    (shortComplexFunctor C c j).map f ≫
        (ShortComplex.isoMk (Y.XIsoOfEq hi) (Iso.refl ((shortComplexFunctor C c j).obj Y).X₂) (Y.XIsoOfEq hk) ⋯ ⋯).hom =
      (ShortComplex.isoMk (X.XIsoOfEq hi) (Iso.refl ((shortComplexFunctor C c j).obj X).X₂) (X.XIsoOfEq hk) ⋯ ⋯).hom ≫
        (shortComplexFunctor' C c i j k).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
hi : c.prev j = i
inst✝ : K.HasHomology j
⊢ IsColimit (CokernelCofork.ofπ (K.homologyπ j) ⋯)

Tactic:
subst hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
j k : ι
inst✝ : K.HasHomology j
⊢ IsColimit (CokernelCofork.ofπ (K.homologyπ j) ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
hi : c.next i = j
⊢ IsLimit (KernelFork.ofι (K.homologyι i) ⋯)

Tactic:
subst hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i k : ι
inst✝ : K.HasHomology i
⊢ IsLimit (KernelFork.ofι (K.homologyι i) ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ homologyMap (φ ≫ ψ) i = homologyMap φ i ≫ homologyMap ψ i

Tactic:
by
  dsimp [homologyMap]
  rw [Functor.map_comp, ShortComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst✝ : K.HasHomology i
⊢ (K.sc i).g = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst✝ : K.HasHomology j
⊢ (K.sc j).f = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
| (mapBaseChange R A B) (x ⊗ₜ[A] y)

Tactic:
rw [← mul_one x, ← smul_eq_mul, ← TensorProduct.smul_tmul', map_smul]

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B
y : Ω[A⁄R]
| x • (mapBaseChange R A B) (1 ⊗ₜ[A] y)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
⊢ (ofHoms fun p ↦ 0) = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : 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 : ι
⊢ Function.LeftInverse (fun h ↦ { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }) fun h ↦
    { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : 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 : ι
⊢ Function.RightInverse (fun h ↦ { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }) fun h ↦
    { hom := fun i j ↦ h.hom i j, zero := ⋯, comm := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ + φ₂) = ofHom φ₁ + ofHom φ₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
⊢ ofHom (φ₁ - φ₂) = ofHom φ₁ - ofHom φ₂

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ ofHom (-φ) = -ofHom φ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
φ : (p : ℤ) → F.X p ⟶ G.X p
ψ : (p : ℤ) → G.X p ⟶ K.X p
⊢ (ofHoms φ).comp (ofHoms ψ) ⋯ = ofHoms fun p ↦ φ p ≫ ψ p

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
nullHomotopicMap_f r₂₁ r₁₀

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) + (dite (c.Rel k₂ k₁) (h k₁ k₂) fun x ↦ 0) ≫ D.d k₂ k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (Cochain.ofHom (inr φ)).comp (snd φ) ⋯ = Cochain.ofHom (𝟙 G)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
α β : Cochain F G n
h : ¬n + 1 = m
⊢ δ n m (α + β) = δ n m α + δ n m β

Tactic:
· simp only [δ_shape _ _ h, add_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ inr φ ≫ desc φ α hα = α

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
⊢ γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯ → γ₁ = γ₂

Tactic:
rintro ⟨h₁, h₂⟩
    ext p q hpq
    rw [ext_to_iff φ q (q + 1) rfl]
    replace h₁ := Cochain.congr_v h₁ p (q + 1) (by lia)
    replace h₂ := Cochain.congr_v h₂ p q hpq
    simp only [Cochain.comp_v _ _ _ p q (q + 1) hpq rfl] at h₁
    simp only [Cochain.comp_zero_cochain_v] at h₂
    exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ (ofHom φ).homOf = φ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cocycle F G 0
⊢ ofHom z.homOf = z

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
⊢ ∀ (x y : F ⟶ G), ofHom (x + y) = ofHom x + ofHom y

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
⊢ AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n) ≫ (K.HomComplex L).d n m = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
⊢ ∀ (s : Fork ((K.HomComplex L).d n m) 0),
    AddCommGrpCat.ofHom { toFun := fun x ↦ ⟨(ConcreteCategory.hom s.ι) x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
        Fork.ι (KernelFork.ofι (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n)) ⋯) =
      s.ι

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
α : Cochain F K (-1)
β : G ⟶ K
eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)
⊢ inr φ ≫ desc φ α β eq = β

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ≅ Arrow.mk φ'
⊢ mapArrowHom φ' φ H α.inv ≫ mapArrowHom φ φ' H α.hom = 𝟙 (homotopyCofiber φ')

Tactic:
rw [← mapArrowHom_comp, Iso.inv_hom_id, mapArrowHom_id]

Goal state after:
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : 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✝ Z✝ : HomologicalComplex V c
x✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ homotopyEquivalences V c x✝ → homotopyEquivalences V c (x✝ ≫ g) → homotopyEquivalences V c g

Tactic:
rintro ⟨f, rfl⟩ ⟨e, he⟩
    refine (f.symm.trans e).homotopyEquivalences_hom.of_homotopy ?_
    simp only [HomotopyEquiv.trans_hom, HomotopyEquiv.symm_hom, he, ← Category.assoc]
    exact f.homotopyInvHomId.compRightId g

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z z' : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z + z').map Φ = z.map Φ + z'.map Φ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (-z).map Φ = -z.map Φ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z z' : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z - z').map Φ = z.map Φ - z'.map Φ

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ map 0 Φ = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
f : K ⟶ L
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (ofHom f).map Φ = ofHom ((Φ.mapHomologicalComplex (ComplexShape.up ℤ)).map f)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G H : Quotient r ⥤ D
τ : functor r ⋙ F ⟶ functor r ⋙ G
τ' : functor r ⋙ G ⟶ functor r ⋙ H
⊢ natTransLift r τ ≫ natTransLift r τ' = natTransLift r (τ ≫ τ')

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : Quotient r ⥤ D
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X✝ Y✝ : Quotient r ⥤ D
f :
  ((whiskeringLeft C (Quotient r) D).obj (functor r)).obj X✝ ⟶
    ((whiskeringLeft C (Quotient r) D).obj (functor r)).obj Y✝
⊢ ((whiskeringLeft C (Quotient r) D).obj (functor r)).map (natTransLift r f) = f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
x✝ : Nonempty (Homotopy f 0)
h : Homotopy f 0
⊢ (quotient V c).map f = 0

Tactic:
by simpa using eq_of_homotopy _ _ h

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
W : Type u_3
inst✝² : Category.{v_1, u_3} W
inst✝¹ : Preadditive W
c : ComplexShape ι
F : V ⥤ W
inst✝ : F.Additive
⊢ mapHomotopyCategory (𝟙 F) c = 𝟙 (F.mapHomotopyCategory c)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝⁶ : Category.{v, u} V
inst✝⁵ : Preadditive V
W : Type u_3
inst✝⁴ : Category.{v_1, u_3} W
inst✝³ : Preadditive W
c : ComplexShape ι
F G H : V ⥤ W
inst✝² : F.Additive
inst✝¹ : G.Additive
inst✝ : H.Additive
α : F ⟶ G
β : G ⟶ H
⊢ mapHomotopyCategory (α ≫ β) c = mapHomotopyCategory α c ≫ mapHomotopyCategory β c

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_3
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
g : L ⟶ K
hg : (quotient V c).map g = inv ((quotient V c).map f)
⊢ (quotient V c).map (f ≫ g) = (quotient V c).map (𝟙 K)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_3
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
g : L ⟶ K
hg : (quotient V c).map g = inv ((quotient V c).map f)
⊢ (quotient V c).map (g ≫ f) = (quotient V c).map (𝟙 L)

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: ι : Type u_3
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
⊢ IsIso ((quotient V c).map f) ↔ homotopyEquivalences V c f

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences V c f hf⟩
  obtain ⟨g, hg⟩ := (quotient V c).map_surjective (inv ((quotient V c).map f))
  let e : HomotopyEquiv K L :=
    { hom := f
      inv := g
      homotopyHomInvId := HomotopyCategory.homotopyOfEq _ _ (by cat_disch)
      homotopyInvHomId := HomotopyCategory.homotopyOfEq _ _ (by cat_disch) }
  exact ⟨e, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n a n' : ℤ
hn' : n + a = n'
γ : Cochain K L n
⊢ (fun γ ↦ γ.leftUnshift n hn') ((fun γ ↦ γ.leftShift a n' hn') γ) = γ

Tactic:
simp only [leftUnshift_leftShift]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f : T₁ ⟶ T₂
⊢ 0 • f = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ ∀ (a : T₁ ⟶ T₂), 0 • a = 0

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : F₁.CommShift A
inst✝ : F₂.CommShift A
a : A
hτ : CommShiftCore τ a
X : C
⊢ (shiftFunctor D a).map (τ.app X) =
    (Functor.commShiftIso F₁ a).inv.app X ≫ τ.app ((shiftFunctor C a).obj X) ≫ (Functor.commShiftIso F₂ a).hom.app X

Tactic:
rw [← hτ.shift_app_comm, Iso.inv_hom_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
X₁ X₂ : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X₁ X₂
⊢ (binaryProductTriangle X₁ X₂).mor₁ ≫ (biprod.isoProd X₁ X₂).symm.hom =
    (Iso.refl (binaryProductTriangle X₁ X₂).obj₁).hom ≫ (binaryBiproductTriangle X₁ X₂).mor₁

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
s : Fan T
j : J
⊢ lift T s.proj ≫ (fan T).proj j = s.proj j

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
⊢ ∀ {X Y : Triangle C} (f : X ⟶ Y),
    (shiftFunctor C 0).map f ≫
        (((shiftFunctor C 0).obj Y).isoMk ((𝟭 (Triangle C)).obj Y) ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₁)
            ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₂) ((CategoryTheory.shiftFunctorZero C ℤ).app Y.obj₃) ⋯ ⋯
            ⋯).hom =
      (((shiftFunctor C 0).obj X).isoMk ((𝟭 (Triangle C)).obj X) ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₁)
            ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₂) ((CategoryTheory.shiftFunctorZero C ℤ).app X.obj₃) ⋯ ⋯
            ⋯).hom ≫
        (𝟭 (Triangle C)).map f

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₁)

Tactic:
Functor.map_units_smul,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (a.negOnePow • (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁))
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₂)

Tactic:
Functor.map_units_smul,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    b.negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (a.negOnePow • (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂))