mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x : I.Cotangent
⊢ (lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯)
      ((lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun x) =
    x

Tactic:
subst hIJ
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I J : Ideal R
hIJ : I = J
x : J.Cotangent
⊢ (lift (J.toCotangent ∘ₗ ↑(LinearEquiv.ofEq I J hIJ)) ⋯).toFun
      ((lift (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) ⋯) x) =
    x

Tactic:
subst hIJ
    obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    simp

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj X) ≫
        (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as X.as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor X).hom

Tactic:
rintro ⟨n⟩

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
⊢ (MonoidalCategoryStruct.leftUnitor ((Discrete.functor h.F).obj { as := n })).hom =
    MonoidalCategoryStruct.whiskerRight h.zero.symm.hom ((Discrete.functor h.F).obj { as := n }) ≫
      (h.add (MonoidalCategoryStruct.tensorUnit (Discrete A)).as { as := n }.as).symm.hom ≫
        (Discrete.functor h.F).map (MonoidalCategoryStruct.leftUnitor { as := n }).hom
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
⊢ ∀ (X : Discrete A),
    (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj X)).hom =
      MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj X) h.zero.symm.hom ≫
        (h.add X.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
          (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor X).hom

Tactic:
rintro ⟨n⟩

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
⊢ (MonoidalCategoryStruct.rightUnitor ((Discrete.functor h.F).obj { as := n })).hom =
    MonoidalCategoryStruct.whiskerLeft ((Discrete.functor h.F).obj { as := n }) h.zero.symm.hom ≫
      (h.add { as := n }.as (MonoidalCategoryStruct.tensorUnit (Discrete A)).as).symm.hom ≫
        (Discrete.functor h.F).map (MonoidalCategoryStruct.rightUnitor { as := n }).hom
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ ∃ (hx : (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x ∈ ideal R S),
    (fromIdeal R S) ⟨(fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
refine ⟨KaehlerDifferential.one_smul_sub_smul_one_mem_ideal R x, ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ : S ⊗[R] S
hx✝ : x✝ ∈ ideal R S
hx : x✝ ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
x : S
⊢ (fromIdeal R S) ⟨(fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) x, ⋯⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).inv.app ((shiftFunctor C n').obj X) ≫
                (shiftFunctorAdd' C n' 0 n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
Iso.hom_inv_id_app_assoc,

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫ (shiftFunctorAdd' C n' 0 n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctorCompIsoId C n' n hn).hom.app X ≫
            (shiftFunctorCompIsoId C n' n hn).inv.app X ≫
              (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
                (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
                  (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Iso.hom_inv_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p' ⋙ shiftFunctor C p).obj X) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).hom.app ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C n).map ((shiftFunctorCompIsoId C m' m hm).inv.app ((shiftFunctor C n').obj X)) ≫
            (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
              (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctorAdd' C m n p h).hom.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
        (shiftFunctorAdd' C m n p h).inv.app ((shiftFunctor C m').obj ((shiftFunctor C n').obj X)) ≫
          (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)

Tactic:
Iso.hom_inv_id_app_assoc,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C p).obj ((shiftFunctor C p').obj X)) =
    (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).hom.app X) ≫
      (shiftFunctor C p).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).hom.app X =
    (shiftFunctorCompIsoId C m n hmn).hom.app X ≫ (shiftFunctorCompIsoId C n m ⋯).inv.app X

Tactic:
by
  simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m n : A
hmn : m + n = 0
X : C
⊢ (shiftFunctorComm C m n).inv.app X =
    (shiftFunctorCompIsoId C n m ⋯).hom.app X ≫ (shiftFunctorCompIsoId C m n hmn).inv.app X

Tactic:
by
  simp [shiftFunctorCompIsoId, shiftFunctorComm_eq C m n 0 hmn]

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 ℤ
⊢ ofHom 0 = 0

Tactic:
by
  simp only [ofHom, HomologicalComplex.zero_f_apply, ofHoms_zero]

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 ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (-z₂) h = -z₁.comp z₂ h

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), neg_v, comp_neg]

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

Goal state before:
pp: case neg
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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j

Tactic:
· rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]

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 ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
⊢ (inl φ).comp ((↑(fst φ)).comp γ he) ⋯ = γ

Tactic:
by
  rw [← Cochain.comp_assoc _ _ _ (neg_add_cancel 1) (by lia) (by lia), inl_fst,
    Cochain.id_comp]

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
j k : ι
hjk : c.Rel j k
⊢ (if hj : c.Rel j (c.next j) then fstX φ j (c.next j) hj ≫ hα.hom (c.next j) j + sndX φ j ≫ α.f j
      else sndX φ j ≫ α.f j) ≫
      K.d j k =
    (homotopyCofiber φ).d j k ≫
      if hj : c.Rel k (c.next k) then fstX φ k (c.next k) hj ≫ hα.hom (c.next k) k + sndX φ k ≫ α.f k
      else sndX φ k ≫ α.f k

Tactic:
obtain rfl := c.next_eq' hjk
    simp [dif_pos hjk]
    have H := hα.comm (c.next j)
    simp only [comp_f, zero_f, add_zero, prevD_eq _ hjk] at H
    split_ifs with hj
    · simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H,
        d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext, AddMonoidHom.mk'_apply]
      abel
    · simp only [d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, dNext_eq_zero _ _ hj, zero_add]

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 n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
m₁ m₂ m₁₂ : ℤ
h₁₂ : n₁₂ + 1 = m₁₂
h₁ : n₁ + 1 = m₁
h₂ : n₂ + 1 = m₂
⊢ n₁ + m₂ = m₁₂

Tactic:
by rw [← h₁₂, ← h₂, ← h, add_assoc]

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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq

Tactic:
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
h₂ : (inr φ).f p ≫ γ₁.v p q ⋯ = (inr φ).f p ≫ γ₂.v p q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ f 0 ((ComplexShape.up ℕ).prev 0) ≫ Q.d ((ComplexShape.up ℕ).prev 0) 0 = 0

Tactic:
rw [Q.shape, comp_zero]

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0
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 ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
⊢ δ n m (single f n) = single (f ≫ L.d q q') m + m.negOnePow • single (K.d p' p ≫ f) m

Tactic:
by
  ext p'' q'' hpq''
  rw [δ_v n m hm (single f n) p'' q'' (by lia) (q'' - 1) (p'' + 1) rfl (by lia),
    add_v, units_smul_v]
  congr 1
  · by_cases h : p'' = p
    · subst h
      by_cases h : q = q'' - 1
      · subst h
        obtain rfl : q' = q'' := by lia
        simp only [single_v]
      · rw [single_v_eq_zero', single_v_eq_zero', zero_comp]
        all_goals lia
    · rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]
  · subst hm
    by_cases h : q'' = q
    · subst h
      by_cases h : p'' = p'
      · subst h
        obtain rfl : p = p'' + 1 := by lia
        simp
      · rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]
        lia
    · simp [single_v_eq_zero' _ _ _ _ _ h]

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
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) {g g' : Y ⟶ Z}, CompClosure r g g' → CompClosure r (f ≫ g) (f ≫ g')

Tactic:
rintro a b e f _ _ ⟨c, d, g, h₁, h₂, i, h⟩

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b e : C
f : a ⟶ b
X Y c d : C
h₁ h₂ : c ⟶ d
h : r h₁ h₂
g : b ⟶ c
i : d ⟶ e
⊢ CompClosure r (f ≫ g ≫ h₁ ≫ i) (f ≫ g ≫ h₂ ≫ i)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
inst✝ : Unique C
a : Quotient r
⊢ a = default

Tactic:
by ext; subsingleton

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 ι
⊢ (MorphismProperty.isomorphisms (HomotopyCategory V c)).inverseImage (quotient V c) = homotopyEquivalences V c

Tactic:
by
  ext K L f
  simp only [MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
  refine ⟨fun _ ↦ ?_, fun hf ↦ quotient_inverts_homotopyEquivalences _ _ _ hf⟩
  obtain ⟨g, hg⟩ := (quotient V c).map_surjective (inv ((quotient _ _).map f))
  exact ⟨{
    hom := f
    inv := g
    homotopyHomInvId := homotopyOfEq _ _ (by simp [hg])
    homotopyInvHomId := homotopyOfEq _ _ (by simp [hg]) }, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K : CochainComplex C ℤ
a b p : ℤ
⊢ p + b + a = p + a + b

Tactic:
rw [add_assoc, add_comm b, add_assoc]

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

Goal state before:
pp: case e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ (a * (n' + m)).negOnePow = (a * m).negOnePow * (a * n').negOnePow

Tactic:
rw [add_comm n', mul_add, Int.negOnePow_add]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
A : Type u_4
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
this : HasShift C A := hF.hasShift s i
a b : A
⊢ i (a + b) = isoAdd (i a) (i b)

Tactic:
ext X
      simp [ShiftMkCore.shiftFunctorAdd_eq, ShiftMkCore.shiftFunctor_eq,
        ← Functor.map_comp_assoc]

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
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    (CategoryTheory.shiftFunctor C n).map f.hom₃ ≫
      (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)

Tactic:
Linear.units_smul_comp,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ n.negOnePow •
      ((CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctor C n).map f.hom₁) =
    (CategoryTheory.shiftFunctor C n).map f.hom₃ ≫
      (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)
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.shiftFunctor C (a + b)).map T.mor₁) ≫
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₁))

Tactic:
Linear.units_smul_comp,

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.shiftFunctor C (a + b)).map T.mor₁ ≫
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (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.shiftFunctor C (a + b)).map T.mor₂) ≫
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₂))

Tactic:
Linear.units_smul_comp,

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.shiftFunctor C (a + b)).map T.mor₂ ≫
        (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
      (b.negOnePow • (CategoryTheory.shiftFunctor C b).map (a.negOnePow • (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.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
      (b.negOnePow •
        (CategoryTheory.shiftFunctor C b).map
            (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁))

Tactic:
Linear.units_smul_comp,

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.shiftFunctor C (a + b)).map T.mor₃ ≫ (shiftFunctorComm C 1 (a + b)).hom.app T.obj₁) ≫
        (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁) =
    (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₃ ≫
      (b.negOnePow •
        (CategoryTheory.shiftFunctor C b).map
            (a.negOnePow • (CategoryTheory.shiftFunctor C a).map T.mor₃ ≫ (shiftFunctorComm C 1 a).hom.app T.obj₁) ≫
          (shiftFunctorComm C 1 b).hom.app ((CategoryTheory.shiftFunctor C a).obj T.obj₁))