mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ x ∈ eraseLast s ↔ x ≠ last s ∧ x ∈ s

Tactic:
simp only [RelSeries.mem_def, eraseLast]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
h : 0 < s.length
⊢ (x ∈ range fun i ↦ s.toFun ⟨↑i, ⋯⟩) ↔ x ≠ last s ∧ x ∈ range s.toFun
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ ⊥.jacobson
⊢ N = ⊥

Tactic:
by
  rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
have hNN' : N ⊔ N' = N ⊔ I • N' :=
    le_antisymm (sup_le le_sup_left hNN)
    (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
by
  have hNN' : N ⊔ N' = N ⊔ I • N' :=
    le_antisymm (sup_le le_sup_left hNN)
    (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
  have h_comap :=
    comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
  have : (I • N').map N.mkQ = N'.map N.mkQ := by
    simpa only [← h_comap.eq_iff, comap_map_mkQ, sup_comm, eq_comm] using hNN'
  have :=
    @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _)
      (by rw [← map_smul'', this]) hIJ
  rwa [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm,
    sup_comm (b := N)] at this

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • sSup (N '' S) i ≤ sSup (N '' S) (i + 1)

Tactic:
by
        rw [sSup_eq_iSup', iSup_apply, Submodule.smul_iSup, iSup_apply]
        apply iSup_mono _
        rintro ⟨_, F, hF, rfl⟩
        exact F.smul_le i

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝ : AddCommMonoid M
⊢ IsAddTorsion M ↔ IsTorsion ℕ M

Tactic:
refine ⟨fun h x => ?_, fun h x => ?_⟩
  · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero
    exact ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt h0⟩, hn⟩
  · rw [isOfFinAddOrder_iff_nsmul_eq_zero]
    obtain ⟨n, hn⟩ := @h x
    exact ⟨n, Nat.pos_of_ne_zero (nonZeroDivisors.coe_ne_zero _), hn⟩

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span ↥(reesAlgebra I) ↑(AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))) = F.submodule

Tactic:
submodule_closure_single,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span ↥(reesAlgebra I) ↑F.submodule.toAddSubmonoid = F.submodule
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
rw [eq_bot_iff]
  intro x hx
  obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).mp hx
  have := isUnit_of_sub_one_mem_jacobson_bot (1 - r.1) (by simpa using h r.2)
  apply this.smul_left_cancel.mp
  simp [sub_smul, hr]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom (M.map (i ≫ j))) x = (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)

Tactic:
M.map_comp

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : ↑(M.obj U)
⊢ (ConcreteCategory.hom
        (M.map i ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).map (M.map j) ≫
            (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map i)) (RingCat.Hom.hom (R.map j))
                    (RingCat.Hom.hom (R.map (i ≫ j))) ⋯).inv.app
              (M.obj W)))
      x =
    (ConcreteCategory.hom (M.map j)) ((ConcreteCategory.hom (M.map i)) x)
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
a : S
⊢ 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ ideal R S

Tactic:
by simp [RingHom.mem_ker]

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

Goal state before:
pp: case refine_2
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
D : Derivation R S M
x : ↥(KaehlerDifferential.ideal R S)
hx : x ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
⊢ x ∈ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))).ker

Tactic:
LinearMap.mem_ker

Goal state after:
case refine_2
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
D : Derivation R S M
x : ↥(KaehlerDifferential.ideal R S)
hx : x ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
⊢ (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
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
x : S
⊢ (TensorProduct.lmul' R) (TensorProduct.includeLeft x) = x

Tactic:
← AlgHom.comp_apply,

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
x : S
⊢ ((TensorProduct.lmul' R).comp TensorProduct.includeLeft) x = 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
X✝ Y : C
f : X✝ ⟶ Y
m n : A
hmn : m + n = 0
X : C
⊢ m + n = 0

Tactic:
hmn

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X✝ Y : C
f : X✝ ⟶ Y
m n : A
hmn : m + n = 0
X : C
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
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
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
by
  dsimp [add]
  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
D : Type u_2
inst✝² : Category.{v_1, u_2} D
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
a b : A
X : C
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Tactic:
by
  dsimp [add]
  simp

Goal state after:
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
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣r • x) = r • y𝖣x

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ (y𝖣(algebraMap R S) r * x) = r • y𝖣x
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
⊢ Epi (K.pOpcycles i)

Tactic:
by
  dsimp only [pOpcycles]
  infer_instance

Goal state after:
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
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R A
inst✝¹ : Algebra A B
inst✝ : Algebra S B
r : A
x : ↥(RingHom.ker (algebraMap A B))
⊢ 1 ⊗ₜ[A] (D R A) ↑(r • x) = (RingHom.id A) r • 1 ⊗ₜ[A] (D R A) ↑x

Tactic:
by simp only [SetLike.val_smul, smul_eq_mul, Derivation.leibniz,
    TensorProduct.tmul_add, TensorProduct.tmul_smul, TensorProduct.smul_tmul', ←
    algebraMap_eq_smul_one, RingHom.mem_ker.mp x.prop, TensorProduct.zero_tmul, add_zero,
    RingHom.id_apply]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
C D : CochainComplex V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
⊢ (prevD i) f = f i (i - 1) ≫ D.d (i - 1) i

Tactic:
dsimp [prevD]
  cases i
  · simp
  · congr <;> simp

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 L : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ (lift φ α β eq).f n ≫ (desc φ α' β' eq').f n = (↑α).v n n' hnn' ≫ α'.v n' n ⋯ + β.v n n ⋯ ≫ β'.f n

Tactic:
simp only [lift, desc, Cocycle.homOf_f, liftCocycle_coe, descCocycle_coe, Cocycle.ofHom_coe,
    liftCochain_v_descCochain_v φ α.1 β α' (Cochain.ofHom β') (zero_add 1) (neg_add_cancel 1) 0
    (add_zero 0) n n n (add_zero n) (add_zero n) n' hnn', Cochain.ofHom_v]

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)
a b : R
f : X ⟶ Y
⊢ (a * b) • (functor r).map f = a • b • (functor r).map f

Tactic:
dsimp [smul]

Goal state after:
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)
a b : R
f : X ⟶ Y
⊢ (functor r).map ((a * b) • f) = (functor r).map (a • b • f)
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 : X ⟶ Y
⊢ 1 • (functor r).map f = (functor r).map f

Tactic:
dsimp [smul]

Goal state after:
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 : X ⟶ Y
⊢ (functor r).map (1 • f) = (functor r).map f
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)
a : R
f g : X ⟶ Y
⊢ a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (functor r).map g

Tactic:
dsimp [smul]

Goal state after:
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)
a : R
f g : X ⟶ Y
⊢ a • ((functor r).map f + (functor r).map g) = (functor r).map (a • f) + (functor r).map (a • g)
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)
a b : R
f : X ⟶ Y
⊢ (a + b) • (functor r).map f = a • (functor r).map f + b • (functor r).map f

Tactic:
dsimp [smul]

Goal state after:
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)
a b : R
f : X ⟶ Y
⊢ (functor r).map ((a + b) • f) = (functor r).map (a • f) + (functor r).map (b • f)
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 : X ⟶ Y
⊢ 0 • (functor r).map f = 0

Tactic:
dsimp [smul]

Goal state after:
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 : X ⟶ Y
⊢ (functor r).map (0 • f) = 0
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
⊢ Functor.Linear R (functor r)

Tactic:
(Term.byTactic
 "by"
 (Tactic.tacticSeq
  (Tactic.tacticSeq1Indented
   [(Tactic.tacticLet__
     "let"
     (Term.letConfig [])
     (Term.letDecl (Term.letIdDecl (Term.letId (hygieneInfo `[anonymous])) [] [] ":=" (Term.app `linear [`R `r `hr]))))
    ";"
    (Tactic.exact
     "exact"
     (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))])))

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
⊢ (add F s i a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
have h : whiskerLeft F (add F s i a b).inv = _ :=
    ((whiskeringLeft C D D).obj F).map_preimage _
  exact (NatTrans.congr_app h X).trans (by simp)

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 : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ q = p + n' + a

Tactic:
by rw [← hpq, add_assoc, hn]

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 : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ q = p' + a

Tactic:
by rw [← hpq, ← hn, ← add_assoc, hp']

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 : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
x : R
⊢ (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'

Tactic:
by
  ext p q hpq
  dsimp
  simp only [rightShift_v _ a n' hn' p q hpq _ rfl, smul_v, Linear.smul_comp]

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₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₂ ≫ iso₃.inv = iso₂.inv ≫ A.mor₂

Tactic:
simp only [← cancel_mono iso₃.hom, assoc, Iso.inv_hom_id, comp_id,
      comm₂, Iso.inv_hom_id_assoc]

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 : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
        ((shiftFunctorAdd' D a b (a + b) ⋯).inv.app (F.obj X) ≫ (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X)) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)

Tactic:
simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc,
    ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map (((shiftFunctorAdd C a b).symm ≪≫ shiftFunctorAdd' C b a (a + b) ⋯).hom.app X) =
    F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (commShiftIso F (a + b)).hom.app X ≫
        (shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
hnm : ¬n + 1 = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
    rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles

Tactic:
by
  refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_
  exact Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _)
    (by simp) (by simp)
    (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])

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

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
⊢ IsIso T.mor₂

Tactic:
obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, zero_comp])

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
⊢ IsIso T.mor₂