mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
r : R
n : ℕ
⊢ basicOpen r ≤ basicOpen (r ^ n)

Tactic:
cases n

Goal state after:
case zero
R : Type u
inst✝ : CommSemiring R
r : R
⊢ basicOpen r ≤ basicOpen (r ^ 0)

case succ
R : Type u
inst✝ : CommSemiring R
r : R
n✝ : ℕ
⊢ basicOpen r ≤ basicOpen (r ^ (n✝ + 1))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1

Tactic:
by
  by_contra! h
  have hcon : exponent G ≤ m := exponent_min' m hpos h
  lia

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (Nat.card ↥H₁).Coprime (Nat.card ↥H₂)

Tactic:
rw [heq₁]

Goal state after:
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Finite ↥H₁
inst✝ : Finite ↥H₂
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
n₁ : ℕ
heq₁ : Nat.card ↥H₁ = p₁ ^ n₁
⊢ (p₁ ^ n₁).Coprime (Nat.card ↥H₂)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ orderOf g / (orderOf g).gcd d = Nat.card G / (Nat.card G).gcd d

Tactic:
orderOf_eq_card_of_zpowers_eq_top h

Goal state after:
G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ Nat.card G / (Nat.card G).gcd d = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card ↑(mk ⁻¹' t) = Nat.card (↥s × ↑t)

Tactic:
Nat.card_congr (preimageMkEquivSubgroupProdSet _ _)

Goal state after:
G : Type u
inst✝ : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card (↥s × ↑t) = Nat.card (↥s × ↑t)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : (n⁻¹ * x)⁻¹ * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H

Tactic:
rw [mul_inv_rev, inv_inv] at this

Goal state after:
G : Type u
inst✝¹ : Group G
H : Subgroup G
inst✝ : Finite ↑↑H
x : G
hx : ↑x ∈ MulAction.fixedPoints (↥H) (G ⧸ H)
ha : ∀ {y : G ⧸ H}, y ∈ orbit ↥H ↑x → y = ↑x
n : G
hn : n ∈ H
this : x⁻¹ * n * x ∈ H
⊢ x⁻¹ * n * x⁻¹⁻¹ ∈ H
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ a' ∈ t, Pi.single (Exists.choose h) (↑(μ a)) a' + ∑ x ∈ t, ↑(μ x) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1

Tactic:
← Finset.sum_add_distrib

Goal state after:
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ✝ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
hμ : ∑ x ∈ t, (Pi.single (Exists.choose h) (↑(μ a)) x + ↑(μ x)) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ⋯⟩ + fun i ↦ ⟨↑(μ i), ⋯⟩) i) = 1
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
m : M
hm : m ≠ 0
⊢ Function.Surjective ⇑(toSpanSingleton R M m)

Tactic:
by
  rw [← range_eq_top, ← span_singleton_eq_range, span_singleton_eq_top R hm]

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsSemisimpleModule R M
inst✝ : Nontrivial M
⊢ ∃ m, IsSimpleModule R ↥m

Tactic:
simpa only [isSimpleModule_iff_isAtom] using IsAtomic.exists_atom _

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso
    (s.toFun (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)),
      (snoc s x₁ hsat₁).toFun (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length).succ))
    ((snoc s x₂ hsat₂).toFun (Fin.last (s.length + 1)),
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last (s.length + 1)).succ)

Tactic:
last_snoc',

Goal state after:
case refine_2.refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso (s.toFun (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)), x₁)
    ((snoc s x₂ hsat₂).toFun (Fin.last (s.length + 1)),
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last (s.length + 1)).succ)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2.refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso (s.toFun (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)), x₁)
    ((snoc s x₂ hsat₂).toFun (Fin.last (s.length + 1)),
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last (s.length + 1)).succ)

Tactic:
last_snoc',

Goal state after:
case refine_2.refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso (s.toFun (Fin.last (s.length + (RelSeries.singleton {(x, y) | IsMaximal x y} x₁).length)), x₁)
    (x₂, ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (Fin.last (s.length + 1)).succ)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) (p • q) = Polynomial.eval r p • (eval r) q

Tactic:
induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn✝ : N.FG
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ n ∈ N, r • n = 0
n : M
hn : n ∈ N
⊢ -(r - 1) • n = n

Tactic:
by simpa [sub_smul] using hr' n 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 F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ (r • f).coeff i ∈ F.N i

Tactic:
by
    rw [Subalgebra.smul_def, PolynomialModule.smul_apply]
    apply Submodule.sum_mem
    rintro ⟨j, k⟩ e
    rw [Finset.mem_antidiagonal] at e
    subst e
    exact F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))

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

Goal state before:
pp: case refine_1
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
x y : I.Cotangent
e : (fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) x = (fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) y
⊢ x = y

Tactic:
replace e := congr_arg Subtype.val e

Goal state after:
case refine_1
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
x y : I.Cotangent
e : ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) x) = ↑((fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩) y)
⊢ x = y
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ M N : PresheafOfModules R
f : M ⟶ N
s : M.sections
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ (ConcreteCategory.hom (N.map g)) ((ConcreteCategory.hom (f.app X)) (↑s X)) = (ConcreteCategory.hom (f.app Y)) (↑s Y)

Tactic:
← naturality_apply,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ M N : PresheafOfModules R
f : M ⟶ N
s : M.sections
X Y : Cᵒᵖ
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (M.map g)) (↑s X)) = (ConcreteCategory.hom (f.app Y)) (↑s Y)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (M.map f✝)) ((ConcreteCategory.hom (f.app X✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1

Tactic:
← naturality_apply,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (f.app Y✝)) ((ConcreteCategory.hom ((unit R).map f✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' n' : M
f : m ⟶ m'
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map f).app X) ≫ (μ F m' n').app X =
    (μ F m n).app X ≫ (F.map (f ⊗ₘ g)).app X

Tactic:
have := congr_app (μ_natural F f g) X
  dsimp at this
  simpa using this

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y = (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y

Tactic:
← cancel_epi ((ε F).app _),

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m : M
X Y : C
f : X ⟶ (F.obj m).obj Y
inst✝ : F.Monoidal
⊢ (ε F).app X ≫ (F.obj (𝟙_ M)).map f ≫ (μ F m (𝟙_ M)).app Y = (ε F).app X ≫ (η F).app X ≫ f ≫ (F.map (ρ_ m).inv).app Y
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_3
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 y : S ⊗[R] S
⊢ ∀ (x y_1 : S ⊗[R] S),
    D.tensorProductTo (x * y) =
        (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x →
      D.tensorProductTo (y_1 * y) =
          (TensorProduct.lmul' R) y_1 • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y_1 →
        D.tensorProductTo ((x + y_1) * y) =
          (TensorProduct.lmul' R) (x + y_1) • D.tensorProductTo y +
            (TensorProduct.lmul' R) y • D.tensorProductTo (x + y_1)

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 y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)

Tactic:
· intro x₁ y₁ h₁ h₂
    rw [add_mul, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]

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 y : S ⊗[R] S
⊢ ∀ (x y_1 : S),
    D.tensorProductTo (x ⊗ₜ[R] y_1 * y) =
      (TensorProduct.lmul' R) (x ⊗ₜ[R] y_1) • D.tensorProductTo y +
        (TensorProduct.lmul' R) y • D.tensorProductTo (x ⊗ₜ[R] y_1)
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: case e'_1.e'_3
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

pp: case e'_1.e'_4
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
⊢ (if i✝ = j then A else 0) = 0

pp: case e'_2.e'_3.e'_2.e'_4
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

pp: case e'_2.e'_3.e'_2.e'_5
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝¹ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
e_1✝ :
  ({ X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ ⟶
      { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝) =
    (0 ⟶ 0)
⊢ { X := fun i ↦ if i = j then A else 0, d := fun x x_1 ↦ 0, shape := ⋯, d_comp_d' := ⋯ }.X i✝ = 0

pp: case e'_3
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i✝ : ι
h : ¬i✝ = j
e_1✝ : ((if i✝ = j then A else 0) ⟶ if i✝ = j then A else 0) = (0 ⟶ 0)
⊢ (if i✝ = j then A else 0) = 0

Tactic:
all_goals simp [if_neg h]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ g.f i = h.f i

Tactic:
rw [← cancel_epi (φ.f i)]

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
K L : HomologicalComplex V c
φ : K ⟶ L
hφ : ∀ (i : ι), Epi (φ.f i)
Z✝ : HomologicalComplex V c
g h : L ⟶ Z✝
eq : φ ≫ g = φ ≫ h
i : ι
⊢ φ.f i ≫ g.f i = φ.f i ≫ h.f i
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁹ : Category.{v, u} V
inst✝⁸ : Preadditive V
W : Type u_2
inst✝⁷ : Category.{v_1, u_2} W
inst✝⁶ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁵ : Category.{v_2, u_3} W₁
inst✝⁴ : Category.{v_3, u_4} W₂
inst✝³ : HasZeroMorphisms W₁
inst✝² : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C D : HomologicalComplex V c✝
f : C ⟶ D
i : ι
F : V ⥤ W
inst✝¹ : F.Additive
c : ComplexShape ι
inst✝ : F.Faithful
K L : HomologicalComplex V c
f₁ f₂ : K ⟶ L
h : (F.mapHomologicalComplex c).map f₁ = (F.mapHomologicalComplex c).map f₂
⊢ f₁ = f₂

Tactic:
ext
    exact F.map_injective ((HomologicalComplex.eval W c _).congr_map h)

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

Goal state before:
pp: W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
⊢ (F.mapHomologicalComplex (ComplexShape.down α)).obj (of X d sq) = of (fun n ↦ F.obj (X n)) (fun n ↦ F.map (d n)) ⋯

Tactic:
by
  refine HomologicalComplex.ext rfl ?_
  rintro i j (rfl : j + 1 = i)
  simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
j : J
⊢ { f := fun i ↦ (hs i).lift ((eval C c i).mapCone t), comm' := ⋯ } ≫ s.π.app j = t.π.app j

Tactic:
ext i
    apply (hs i).fac

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (if h : n + 3 = n + 2 + 1 then eqToHom ⋯ ≫ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g else 0) =
    (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst

Tactic:
rw [dif_pos (by rfl), eqToHom_refl, id_comp]

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
eq :
  (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst =
    eqToHom ⋯ ≫
      (succ
            { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
              X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
              g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).snd.fst
⊢ (mkAux X₀ X₁ X₂ d₀ d₁ s succ (n + 2)).g = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).snd.fst
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
j : J
⊢ s.ι.app j ≫ { f := fun i ↦ (hs i).desc ((eval C c i).mapCocone t), comm' := ⋯ } = t.ι.app j

Tactic:
ext i
    apply (hs i).fac

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
n : A
X : C
⊢ F.map ((add hF s i 0 n).hom.app X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))

Tactic:
have := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)

Goal state after:
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
n : A
X : C
this : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ F.map ((add hF s i 0 n).hom.app X) = F.map (eqToHom ⋯ ≫ (s n).map ((zero hF s i).inv.app X))