mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ZMod.Aut

Goal state before:
pp: n : ℕ
h : ∀ (f : AddAut (ZMod n)) (x : ZMod n), f 1 * x = f x
g : AddAut (ZMod n)
⊢ (fun x ↦ AddAut.mulLeft (Additive.toMul x)) ((fun f ↦ Additive.ofMul (Units.mkOfMulEqOne (f 1) ((-f) 1) ⋯)) g) = g

Tactic:
by simp [DFunLike.ext_iff, Units.smul_def, h]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inl
b : ℕ
⊢ factorizationLCMLeft 0 b ∣ 0

Tactic:
simp only [dvd_zero]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inl
a : ℕ
ha : a ≠ 0
⊢ a.factorizationLCMRight 0 ∣ 0

Tactic:
simp only [dvd_zero]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Surjective ⇑f
s : Set (PrimeSpectrum S)
F : Set R
hF : comap f ⁻¹' zeroLocus F = sᶜ
⊢ ∃ s_1, sᶜ = zeroLocus s_1

Tactic:
exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(r • D);
    { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) =
    (RingHom.id A) r •
      let __LinearMap := ↑R f ∘ₗ ↑D;
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

Tactic:
by ext; dsimp; simp only [_root_.map_smul]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : p ∉ zeroLocus s
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U

Tactic:
mem_zeroLocus,

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ¬s ⊆ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), p ∈ v ∧ v ⊆ U
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h₂
G : Type u
inst✝ : Monoid G
h_congr_thm✝ :
  ∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c), (∀ (h : c), x_1 ⋯ = u h) → (∀ (h : ¬c), y ⋯ = v h) → dite b x_1 y = dite c u v
h✝ : ∃ n, 0 < n ∧ ∀ (g : G), g ^ n = 1
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

Tactic:
exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h₁
G : Type u
inst✝ : Monoid G
x✝ : ℕ
⊢ (∀ (g : Gᵐᵒᵖ), g ^ x✝ = 1) ↔ ∀ (g : G), g ^ x✝ = 1

Tactic:
exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D D1✝ D2✝ : Derivation R A M
r : R
a✝ b✝ : A
D1 D2 : Derivation R A M
a b : A
⊢ (↑D1 - ↑D2) (a * b) = a • (↑D1 - ↑D2) b + b • (↑D1 - ↑D2) a

Tactic:
by
      simp only [LinearMap.sub_apply, leibniz, coeFn_coe, smul_sub, add_sub_add_comm]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ p ∈ zeroLocus ↑(RingHom.ker (Pi.evalRingHom R i))

Tactic:
mem_zeroLocus,

Goal state after:
ι : Type u_1
R : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (R i)
inst✝ : DecidableEq ι
i : ι
f : R i
p : PrimeSpectrum ((i : ι) → R i)
hp : p ∈ ↑(basicOpen (Pi.single i f))
⊢ ↑(RingHom.ker (Pi.evalRingHom R i)) ⊆ ↑p.asIdeal
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
inst✝ : Group G
p : ℕ
hp : Fact (Nat.Prime p)
h : Nat.card G = p
g g' : G
hg : g ≠ 1
⊢ g' ∈ Submonoid.powers g

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
  rw [mem_powers_iff_mem_zpowers]
  exact mem_zpowers_of_prime_card h hg

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
I : PrimeSpectrum R
this : (algE (e I)).symm ((algebraMap R (Localization.Away ↑(e I))) r) = x (e.symm (e I))
⊢ (toPiLocalization R) r I = x I

Tactic:
AlgEquiv.commutes,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
r : R
eq : ∀ (a : ↑(Set.range f)), (algebraMap R (Localization.Away ↑a)) r = (algE a) (x (e.symm a))
I : PrimeSpectrum R
this : (algebraMap R (Localization.AtPrime (e.symm (e I)).asIdeal)) r = x (e.symm (e I))
⊢ (toPiLocalization R) r I = x I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x.asIdeal ≤ y.asIdeal ↔ y ∈ zeroLocus ↑(vanishingIdeal {x})

Tactic:
mem_zeroLocus,

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y : PrimeSpectrum R
⊢ x.asIdeal ≤ y.asIdeal ↔ ↑(vanishingIdeal {x}) ⊆ ↑y.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
⊢ comap f '' zeroLocus ↑I ⊆ zeroLocus ↑(Ideal.comap f I)

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I

Tactic:
· rintro _ ⟨q, hq, rfl⟩
    exact Ideal.comap_mono hq

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (comap f '' zeroLocus ↑I)
p : PrimeSpectrum R
hp : p ∈ zeroLocus ↑(Ideal.comap f I)
⊢ p ∈ comap f '' zeroLocus ↑I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
⊢ Function.Surjective (comap (algebraMap R S))

Tactic:
intro ⟨p, hp⟩
  have hinj : Function.Injective (algebraMap R S) := FaithfulSMul.algebraMap_injective _ _
  obtain ⟨Q, _, hQ, rfl⟩ := Ideal.exists_ideal_over_prime_of_isIntegral p (⊥ : Ideal S)
    (by simp [Ideal.comap_bot_of_injective (algebraMap R S) hinj])
  exact ⟨⟨Q, hQ⟩, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
⊢ 0 < #{a | orderOf a = Nat.card α}

Tactic:
rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]
      apply Fintype.card_pos

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
⊢ Subgroup.zpowers (g ^ n) = ⊥ → orderOf g ∣ n

pp: case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)

Tactic:
· simp [orderOf_dvd_iff_pow_eq_one]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
n : ℕ
h : Subgroup.zpowers (g ^ n) = ⊤
⊢ n.Coprime (orderOf g)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
⊢ False

Tactic:
have h := IsPGroup.of_card (((Nat.card_zpowers x).trans hx).trans (pow_one p).symm)

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
⊢ False
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
m : M
x✝ : m ∈ (AddCommGroup.torsion M).carrier
n : ℕ
hn : n > 0
hn' : Function.IsPeriodicPt (fun x ↦ m + x) n 0
⊢ Function.IsPeriodicPt (fun x ↦ r • m + x) n 0

Tactic:
{ simp only [Function.IsPeriodicPt, Function.IsFixedPt, add_left_iterate, add_zero,
      smul_comm n] at hn' ⊢; simp only [hn', smul_zero] }

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
⊢ f₁ = f₂ ↔ f₁ g = f₂ g

Tactic:
rw [DFunLike.ext_iff]
  refine ⟨fun H ↦ H g, fun H x ↦ ?_⟩
  obtain ⟨n, hn⟩ := mem_zpowers_iff.mp <| hg x
  rw [← hn, map_zpow, map_zpow, H]

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
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ ∀ i ∈ Set.univ, IsSemisimpleModule R ↥(f i)

Tactic:
rintro (_ | _) _

Goal state after:
case false
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
a✝ : false ∈ Set.univ
⊢ IsSemisimpleModule R ↥(f false)

case true
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
a✝ : true ∈ Set.univ
⊢ IsSemisimpleModule R ↥(f true)
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
n : ℕ
⊢ single R n 0 = 0

Tactic:
simp [single]

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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N

Tactic:
refine ⟨1, ?_, ?_, ?_⟩

Goal state after:
case refine_1
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ 1 - 1 ∈ I

case refine_2
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • span R s)

case refine_3
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ s ⊆ ↑N
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}
j k : ℕ
⊢ (↑r).coeff (j, k).1 • f.coeff (j, k).2 ∈ F.N ((j, k).1 + (j, k).2)

Tactic:
exact F.pow_smul_le j k (Submodule.smul_mem_smul (r.2 j) (hf k))

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 M₁ M₂ : PresheafOfModules R
⊢ ∀ (a : M₁ ⟶ M₂), a + 0 = a

Tactic:
intros; ext1; simp only [add_app, zero_app, add_zero]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: case neg
I : Type u_1
J : Type u_2
C : Type u_4
inst✝⁴ : Category.{v_1, u_4} C
X Y : GradedObject I C
φ : X ⟶ Y
p : I → J
inst✝³ : X.HasMap p
inst✝² : Y.HasMap p
inst✝¹ : HasZeroMorphisms C
inst✝ : DecidableEq J
i : I
j : J
h : ¬p i = j
⊢ X.ιMapObjOrZero p i j ≫ mapMap φ p j = φ i ≫ Y.ιMapObjOrZero p i j

Tactic:
simp only [ιMapObjOrZero_eq_zero _ _ _ _ h, zero_comp, comp_zero]

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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
A : V
i : ι
⊢ ((single V c i).obj A).X i = A

Tactic:
simp [single]

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 ι
C : HomologicalComplex V c
j : ι
r : c.Rel (c.prev j) j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d (c.prev j) j

Tactic:
exact (Category.id_comp _).symm

Goal state after:
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 : ι
inst✝⁵ : HasZeroObject W₁
inst✝⁴ : HasZeroObject W₂
W : Type u_5
inst✝³ : Category.{v_4, u_5} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
inst✝ : DecidableEq ι
j : ι
x✝¹ x✝ : W
f g : x✝¹ ⟶ x✝
⊢ ((single W c j).map (f + g)).f j = ((single W c j).map f + (single W c j).map g).f j

Tactic:
simp [single]

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

Goal state before:
pp: case refine_2.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 y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ 0 + (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0

Tactic:
ey,

Goal state after:
case refine_2.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 y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ 0 + 0 = 0
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ f 0 = f' 0

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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (x y : Ω[S⁄R]),
    x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) →
      y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f y = f' y → f (x + y) = f' (x + y)

pp: case refine_4
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (a : S), ∀ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)), f x = f' x → f (a • x) = f' (a • x)

Tactic:
· rw [map_zero, map_zero]

Goal state after:
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (x y : Ω[S⁄R]),
    x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) →
      y ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) → f x = f' x → f y = f' y → f (x + y) = f' (x + y)

case refine_4
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
f f' : Ω[S⁄R] →ₗ[S] M
hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
x : Ω[S⁄R]
this : x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S))
⊢ ∀ (a : S), ∀ x ∈ Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)), f x = f' x → f (a • x) = f' (a • 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
r : R
x y : S
this : SMulZeroClass R S := inferInstance
⊢ ((y * (algebraMap R S) r)𝖣x) = (kerTotal R S).mkQ (r • single x y)

Tactic:
Finsupp.smul_single,

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.HomologicalComplexBiprod

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
M : HomologicalComplex C c
α : K ⟶ M
β : L ⟶ M
i : ι
⊢ biprod.inl.f i ≫ (biprod.desc α β).f i = α.f i

Tactic:
by
  rw [← comp_f, biprod.inl_desc]

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₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₂ + n₂

Tactic:
← h₁,

Goal state after:
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₁₂
p₁ p₂ p₃ : ℤ
h₁ : p₁ + n₁ = p₂
h₂ : p₂ + n₂ = p₃
⊢ p₁ + n₁₂ = p₁ + n₁ + n₂
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 : ι
hi : ¬c.Rel i (c.next i)
A : C
f g : X φ i ⟶ A
h : inrX φ i ≫ f = inrX φ i ≫ g
⊢ f = g

Tactic:
by
  rw [← cancel_epi (XIso φ i hi).inv]
  simpa only [inrX, dif_neg hi] using h

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
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₂
⊢ m₁ + n₂ = n₁₂ + 1

Tactic:
← h₁,

Goal state after:
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₁ + 1 + n₂ = n₁₂ + 1
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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
⊢ i + -1 = j

Tactic:
← hij,

Goal state after:
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 : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : j + 1 = i
⊢ j + 1 + -1 = j
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 ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
n' : ℤ
hn' : n + 1 = n'
⊢ δ n n' (descCochain φ α β h) =
    (↑(fst φ)).comp (δ m n α + n'.negOnePow • (Cochain.ofHom φ).comp β ⋯) ⋯ + (snd φ).comp (δ n n' β) ⋯

Tactic:
dsimp only [descCochain]
  simp only [δ_add, Cochain.comp_add, δ_comp (fst φ).1 α _ 2 n n' hn' (by lia) (by lia),
    Cocycle.δ_eq_zero, Cochain.zero_comp, smul_zero, add_zero,
    δ_comp (snd φ) β (zero_add n) 1 n' n' hn' (zero_add 1) hn', δ_snd, Cochain.neg_comp,
    smul_neg, Cochain.comp_assoc_of_second_is_zero_cochain, Cochain.comp_units_smul, ← hn',
    Int.negOnePow_succ, Units.neg_smul, Cochain.comp_neg]
  abel

Goal state after: