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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x : S
this : ∀ x ∈ adjoin R ↑(EssFiniteType.finset R S), (D R S) x ∈ Submodule.span S ↑s
t : S
ht : t ∈ adjoin R ↑(EssFiniteType.finset R S)
ht' : IsUnit t
hxt : x * t ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ (D R S) x ∈ ↑(Submodule.span S ↑s)

Tactic:
rw [show D R S x =
    ht'.unit⁻¹ • (D R S (x * t) - x • D R S t) by simp [smul_smul, Units.smul_def]]

Goal state after:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
M : Type u_1
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
inst✝ : EssFiniteType R S
s : Finset Ω[S⁄R] := Finset.image (fun s ↦ (D R S) s) (EssFiniteType.finset R S)
x : S
this : ∀ x ∈ adjoin R ↑(EssFiniteType.finset R S), (D R S) x ∈ Submodule.span S ↑s
t : S
ht : t ∈ adjoin R ↑(EssFiniteType.finset R S)
ht' : IsUnit t
hxt : x * t ∈ adjoin R ↑(EssFiniteType.finset R S)
⊢ ht'.unit⁻¹ • ((D R S) (x * t) - x • (D R S) t) ∈ ↑(Submodule.span S ↑s)
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:
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✝ : ι
inst✝ : K.HasHomology i
A : C
k : A ⟶ K.X i
hk : k ≫ K.d i (c.next i) = 0
⊢ k ≫ (K.sc i).g = 0

Tactic:
exact hk

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✝ : ι
inst✝ : K.HasHomology i
A : C
k : K.X i ⟶ A
hk : K.d (c.prev i) i ≫ k = 0
⊢ (K.sc i).f ≫ k = 0

Tactic:
exact hk

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 : ι
inst✝¹ : K.HasHomology i
hi : c.prev j = i
inst✝ : K.HasHomology j
⊢ IsColimit (CokernelCofork.ofπ (K.pOpcycles j) ⋯)

Tactic:
obtain rfl := 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
inst✝ : K.HasHomology (c.prev j)
⊢ IsColimit (CokernelCofork.ofπ (K.pOpcycles 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 : 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:
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
⊢ IsIso (K.pOpcycles j)

Tactic:
obtain rfl := hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
j : ι
inst✝ : K.HasHomology j
h : K.d (c.prev j) j = 0
⊢ IsIso (K.pOpcycles 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 : 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:
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
h : Function.Surjective ⇑(algebraMap A B)
⊢ (map R R A B).ker =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
rw [ker_map, ← kerTotal_map' R A B h, Submodule.comap_map_eq, Submodule.map_sup,
    Submodule.map_sup, ← kerTotal_eq, ← Submodule.comap_bot,
    Submodule.map_comap_eq_of_surjective (linearCombination_surjective _ _),
    bot_sup_eq, Submodule.map_span, ← Set.range_comp]
  convert! bot_sup_eq _
  rw [Submodule.span_eq_bot]; simp

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 ℤ
⊢ (ofHoms fun p ↦ 0) = 0

Tactic:
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:
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:
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:
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:
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:
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 : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
⊢ d φ i j ≫ sndX φ j = fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
by
  dsimp [d]
  split_ifs with hij <;> simp

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:
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 φ
⊢ (Cochain.ofHom (inr φ)).comp (snd φ) ⋯ = Cochain.ofHom (𝟙 G)

Tactic:
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ inr φ ≫ desc φ α hα = α

Tactic:
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
p q : ℤ
hpq : p + i = q
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Tactic:
simp only [Cochain.comp_zero_cochain_v] at h₂

Goal state after:
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
p q : ℤ
hpq : p + i = q
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯
h₂ : γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯
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
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
x✝ : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
⊢ ((fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
          ((fun x ↦
              match x with
              | ⟨α, hα⟩ => desc φ α hα)
            ⟨α, hα⟩)).fst =
      ⟨α, hα⟩.fst ∧
    ∀ (i j : ι),
      c.Rel j i →
        ((fun f ↦ ⟨inr φ ≫ f, (Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯))⟩)
                  ((fun x ↦
                      match x with
                      | ⟨α, hα⟩ => desc φ α hα)
                    ⟨α, hα⟩)).snd.hom
            i j =
          ⟨α, hα⟩.snd.hom i j

Tactic:
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 φ).homOf = φ

Tactic:
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:
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:
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:
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:
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:
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 : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = ho.hom i j

Tactic:
ho.zero i j (fun h' => h (by dsimp at h'; lia))

Goal state after:
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 : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos.h₀
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

Tactic:
simp [ι₀]

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:
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:
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:
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:
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:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
f : (functor r).obj X ⟶ (functor r).obj Y
⊢ 1 • f = f

Tactic:
obtain ⟨f, rfl⟩ := (functor r).map_surjective f
      dsimp [smul]
      rw [one_smul]

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:
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:
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.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r (τ.hom ≫ τ.inv) = 𝟙 F

Tactic:
τ.hom_inv_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ≅ functor r ⋙ G
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F
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:
cat_disch

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)

Tactic:
← (quotient V c).map_comp,

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.hom ≫ f.inv) = 𝟙 ((quotient V c).obj C)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)

Tactic:
← (quotient V c).map_comp,

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.inv ≫ f.hom) = 𝟙 ((quotient V c).obj D)
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:
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:
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:
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:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      F.map (𝟙 X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app (F.obj X)

Tactic:
rw [F.map_id, id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p + n = p'
⊢ (γ.rightShift a n' hn').v p q hpq = γ.v p p' hp' ≫ (L.shiftFunctorObjXIso a q p' ⋯).inv

Tactic:
subst hp'
  dsimp only [rightShift]
  simp only [mk_v]

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 : ℤ
⊢ ∀ (a_1 b : Cochain K L n), (a_1 + b).shift a = a_1.shift a + b.shift a

Tactic:
by intros; simp only [shift_add]

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:
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:
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
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:
cat_disch

Goal state after: