mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y) =
    x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
      y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x

Tactic:
have : (f x - algebraMap A B x) * (f y - algebraMap A B y) = 0 := by
      rw [← Ideal.mem_bot, ← hI, pow_two]
      convert! Ideal.mul_mem_mul (F x).2 (F y).2 using 1

Goal state after:
case refine_3
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f = IsScalarTower.toAlgHom R A (B ⧸ I)
x y : A
F : A →ₗ[R] ↥I := diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯
this : (f x - (algebraMap A B) x) * (f y - (algebraMap A B) y) = 0
⊢ (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) (x * y) =
    x • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) y +
      y • (diffToIdealOfQuotientCompEq I f (IsScalarTower.toAlgHom R A B) ⋯) x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ IsIrreducible (zeroLocus ↑I) ↔ I.IsPrime

Tactic:
rw [Ideal.isPrime_iff, IsIrreducible]
  apply and_congr
  · rw [Set.nonempty_iff_ne_empty, Ne, zeroLocus_empty_iff_eq_top]
  · trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
    · simp_rw [isPreirreducible_iff_isClosed_union_isClosed, isClosed_iff_zeroLocus_ideal]
      constructor
      · rintro h x y
        exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
      · rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
        exact h x y
    · simp_rw [← zeroLocus_inf, subset_zeroLocus_iff_le_vanishingIdeal,
        vanishingIdeal_zeroLocus_eq_radical, hI.radical]
      constructor
      · simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ←
          Ideal.span_singleton_mul_span_singleton]
        refine fun h x y h' => h _ _ ?_
        rw [← hI.radical_le_iff] at h' ⊢
        simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'
      · simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
        rintro h s t h' ⟨x, hx, hx'⟩ y hy
        exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
n : ℕ
⊢ exponent G ∣ n ↔ ∀ (g : G), g ^ n = 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp
  constructor
  · intro h g
    rw [Nat.dvd_iff_mod_eq_zero] at h
    rw [pow_eq_mod_exponent, h, pow_zero]
  · intro hG
    by_contra h
    rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h
    have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
    have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG
    exact h₂.not_ge h₃

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) = ⊤
a : ↑(Set.range f)
⊢ ↑(basicOpen ↑a) = {(Equiv.ofInjective f ⋯).symm a}

Tactic:
← hf,

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) = ⊤
a : ↑(Set.range f)
⊢ ↑(basicOpen ↑a) = ↑(basicOpen (f ((Equiv.ofInjective f ⋯).symm a)))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
⊢ False

Tactic:
suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_ge (le_csSup hfin.bddAbove <| Set.mem_range_self _)

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
⊢ orderOf t < orderOf (t ^ p ^ k * g)
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
n : ℕ
h : IsPGroup (p ^ n) G
g : G
⊢ ∀ (a : ℕ), g ^ (p ^ n) ^ a = 1 → g ^ p ^ (n * a) = 1

Tactic:
simp [pow_mul]

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
by
  have := Fintype.ofFinite α
  have := Fintype.ofFinite (fixedPoints G α)
  rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
  classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x + 0 = c • x
⊢ (c % n) • x = c • x

Tactic:
add_zero

Goal state after:
n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n) • x = c • x
⊢ (c % n) • x = c • x
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:

Tactic:
c = ∑ m ∈ c.divisors, #{a : α | orderOf a = m} := by
      simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
      apply congr_arg card
      simp [c]
    _ = ∑ m ∈ c.divisors.erase d, #{a : α | orderOf a = m} := by
      rw [eq_comm]
      refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
      have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
      simp [this, h0]
    _ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
      gcongr with m hm
      have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
      obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
      · simp [h1]
      · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
    _ < ∑ m ∈ c.divisors, φ m :=
      sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0))
    _ = c := sum_totient _

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : (↑P).relIndex (normalizer ↑P) ≠ 0
⊢ ¬p ∣ (↑P).index

Tactic:
by
  rw [← relIndex_mul_index le_normalizer, P.coe_coe, ← card_eq_index_normalizer]
  have : (P.subtype le_normalizer).Normal :=
    Subgroup.normal_in_normalizer
  have : (P.subtype le_normalizer).FiniteIndex := ⟨hP⟩
  replace hP := not_dvd_index_aux (P.subtype le_normalizer)
  exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
⊢ IsMulTorsionFree G ↔ torsion G = ⊥

Tactic:
isMulTorsionFree_iff_not_isOfFinOrder,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
⊢ (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) ↔ torsion G = ⊥
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℕ
hn : n ≠ 0
⊢ IsMulTorsion (G ⧸ (powMonoidHom n).range)

Tactic:
simp only [IsMulTorsion, isOfFinOrder_iff_pow_eq_one]
  refine fun g ↦ QuotientGroup.induction_on g fun a ↦ ⟨n, hn.pos, ?_⟩
  rw [← QuotientGroup.mk_pow, QuotientGroup.eq_one_iff]
  simp

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ ⟨y, ⋯⟩ ∈ H.subgroupOf (normalizer ↑H)

Tactic:
simpa using! hy

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
_hp✝ : Fact (Nat.Prime p)
n m : ℕ
hdvd : p ^ m ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
hnm✝ : n ≤ m
hnm : n = m
⊢ Nat.card ↥H = p ^ m ∧ H ≤ H

Tactic:
simp [hH, hnm]

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

Goal state before:
pp: case refine_2.mpr.refine_1
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : i = a
⊢ v ∈ ⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j

Tactic:
simp only [mem_iInf] at hv ⊢
      intro j hj ij
      rw [Finset.mem_cons, ← hi] at hj
      exact hv _ (hj.resolve_left ij)

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

Goal state before:
pp: M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (Module.annihilator R M).IsRadical

Tactic:
by
  rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]
  exact Ideal.isRadical_iInf _ fun i ↦ (i.2.annihilator_isMaximal).isPrime.isRadical

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

Goal state before:
pp: case refine_2.mpr.refine_3
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) + ↑⟨v, ⋯⟩ = ∑ i ∈ t, u * ↑(μ i) + v

Tactic:
congr 1

Goal state after:
case refine_2.mpr.refine_3.e_a
ι : 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 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = ∑ i ∈ t, u * ↑(μ i)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f ((of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f ((of R M a).symm x)
m : AEval R M a
⊢ f ((of R M a).symm ((C k * X ^ n) • X • m)) = (C k * X ^ n) • X • f ((of R M a).symm m)

Tactic:
← hf,

Goal state after:
R : Type ?u.5
A : Type ?u.7
M : Type ?u.13
inst✝¹⁰ : CommSemiring R
inst✝⁹ : Semiring A
a : A
inst✝⁸ : Algebra R A
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module A M
inst✝⁵ : Module R M
inst✝⁴ : IsScalarTower R A M
N : Type ?u.26
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module R[X] N
inst✝ : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), f (a • m) = X • f m
p : R[X]
n : ℕ
k : R
h : ∀ (x : AEval R M a), f ((of R M a).symm ((C k * X ^ n) • x)) = (C k * X ^ n) • f ((of R M a).symm x)
m : AEval R M a
⊢ f ((of R M a).symm ((C k * X ^ n) • X • m)) = (C k * X ^ n) • f (a • (of R M a).symm m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case monomial
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ((monomial f_n) f_a • g).coeff n = ∑ x ∈ Finset.antidiagonal n, ((monomial f_n) f_a).coeff x.1 • g.coeff x.2

Tactic:
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j =>
      (monomial f_n f_a).coeff i • g.coeff j, monomial_smul_apply]
    simp [Polynomial.coeff_monomial]

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
i : ℕ
⊢ ((algebraMap R R[X]) r).coeff i ∈ I ^ i

Tactic:
by
    rw [algebraMap_apply, coeff_C]
    split_ifs with h
    · subst h
      simp
    · simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
r : R
hM : IsTorsionBy R M r
⊢ IsTorsionBySet R M ↑(Ideal.span {r})

Tactic:
rwa [← isTorsionBySet_span_singleton_iff r] at hM

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 : Ideal R
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
⊢ N ⊔ I • N' ≤ N ⊔ N'

Tactic:
simpa using le_trans smul_le_right le_sup_right

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ (CommRingCat.Hom.hom f) a • d b + 0 = a • d b

Tactic:
add_zero

Goal state after:
A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ (CommRingCat.Hom.hom f) a • d b = a • d b
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
M : ModuleCat ↑B
f : A ⟶ B
d : ↑B → ↑M
d_add : ∀ (b b' : ↑B), d (b + b') = d b + d b'
d_mul : ∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b
d_map : ∀ (a : ↑A), d ((ConcreteCategory.hom f) a) = 0
this✝ : Algebra ↑A ↑B := (CommRingCat.Hom.hom f).toAlgebra
this : Module ↑A ↑M := Module.compHom (↑M) (CommRingCat.Hom.hom f)
a : ↑A
b : ↑B
⊢ d (a • b) = (RingHom.id ↑A) a • d b

Tactic:
dsimp
      rw [RingHom.smul_toAlgebra, d_mul, d_map, smul_zero, add_zero]
      rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α = β

Tactic:
by
  rw [← sub_eq_zero]
  have : ⊤ ≤ LinearMap.ker (α - β).hom := by
    rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
    rintro _ ⟨y, rfl⟩
    rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]
    apply h
  rw [top_le_iff, LinearMap.ker_eq_top] at this
  ext : 1
  exact this

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y - 0 ∈ I ^ 2

Tactic:
sub_zero,

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x : R
hx : x ∈ ↑I
y : R
hy : y ∈ ↑I
⊢ (fun x1 x2 ↦ x1 * x2) x y ∈ I ^ 2
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
convert! I.iInf_pow_smul_eq_bot_of_isTorsionFree (M := R) h

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsDomain R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤
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_1 : X ⟶ Y),
    (ConcreteCategory.hom (M.map f_1)) ((ConcreteCategory.hom (f.app X)) 1) = (ConcreteCategory.hom (f.app Y)) 1

Tactic:
by intros; rw [← naturality_apply, unit_map_one]

Goal state after:
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
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
⊢ 0 = 0 + 0

Tactic:
add_zero

Goal state after:
case refine_1
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
⊢ 0 = 0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_1
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₁ x₂ : S
⊢ 0 = 0 + 0

Tactic:
add_zero

Goal state after:
case refine_2.refine_1
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₁ x₂ : S
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F (n + 0)).obj X = (F n).obj X

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
assoc_hom_app :
  ∀ (m₁ m₂ m₃ : A) (X : C),
    (add (m₁ + m₂) m₃).hom.app X ≫ (F m₃).map ((add m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (add m₁ (m₂ + m₃)).hom.app X ≫ (add m₂ m₃).hom.app ((F m₁).obj X)
zero_add_hom_app : ∀ (n : A) (X : C), (add 0 n).hom.app X = eqToHom ⋯ ≫ (F n).map (zero.inv.app X)
n : A
X : C
⊢ (F n).obj X = (F n).obj X
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
n : A
X : C
⊢ (h.F n).obj X = (h.F (n + 0)).obj X

Tactic:
add_zero

Goal state after:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
n : A
X : C
⊢ (h.F n).obj X = (h.F n).obj X
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
⊢ g = h

Tactic:
by
    ext i
    rw [← cancel_epi (φ.f i)]
    exact congr_hom eq i

Goal state after: