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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x + y) = D2 (x + y)

Tactic:
by simp only [map_add, *]

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

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) → ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z

Tactic:
rintro ⟨s, rfl⟩

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = zeroLocus s
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z) → ∃ s, zeroLocus s = Z

Tactic:
rintro ⟨s, rfl⟩

Goal state after:
case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set R
⊢ ∃ s_1, zeroLocus s_1 = zeroLocus (⇑(algebraMap R S) '' s)
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0

Tactic:
apply hd

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (f_inv (x + y) - (f_inv x + f_inv y)) = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : R
y : M
⊢ f (d (f_inv (x • y) - x • f_inv y)) = 0

Tactic:
apply hd

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : R
y : M
⊢ f (f_inv (x • y) - x • f_inv y) = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
⊢ f (d (f_inv 1 - 1)) = 0

Tactic:
apply hd

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
⊢ f (f_inv 1 - 1) = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x * y) - f_inv x * f_inv y)) = 0

Tactic:
apply hd

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (f_inv (x * y) - f_inv x * f_inv y) = 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (d (f_inv (f x) - x)) = 0

Tactic:
apply hd

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x : A
⊢ f (f_inv (f x) - x) = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥
⊢ r ∉ x.asIdeal

Tactic:
h₂

Goal state after:
case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥
h₂ : r ∈ x.asIdeal
⊢ False
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: a : ℤ
⊢ (AddSubgroup.zmultiples a).index = a.natAbs

Tactic:
by
  rw [AddSubgroup.index, Nat.card_congr (quotientZMultiplesEquivZMod a).toEquiv, Nat.card_zmod]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
by
  by_cases hn : n = 0
  · simp [hn]
  by_cases ha : a = 0
  · simp [ha, zero_zpow n hn]
  rcases Int.natAbs_eq n with h | h
  · rw [h]
    simp only [zpow_natCast, leibniz_pow, natCast_zsmul]
    rw [← zpow_natCast]
    congr
    lia
  · rw [h, zpow_neg, zpow_natCast, leibniz_inv, leibniz_pow, inv_pow, ← pow_mul, ← zpow_natCast,
      ← zpow_natCast, ← Nat.cast_smul_eq_nsmul K, ← Int.cast_smul_eq_zsmul K, smul_smul, smul_smul,
      smul_smul]
    trans (-n.natAbs * (a ^ ((n.natAbs - 1 : ℕ) : ℤ) / (a ^ ((n.natAbs * 2 : ℕ) : ℤ)))) • D a
    · ring_nf
    rw [← zpow_sub₀ ha]
    congr 3
    · norm_cast
    lia

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ 0 = sInf ∅

Tactic:
Nat.sInf_empty

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ 0 = 0
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ IsOpenMap (sigmaToPi R)

Tactic:
isOpenMap_sigma

Goal state after:
case refine_3
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
⊢ ∀ (i : ι), IsOpenMap fun a ↦ sigmaToPi R ⟨i, a⟩
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
⊢ g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
zpow_mul

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
⊢ (g ^ ↑(Nat.find hex)) ^ (k / ↑(Nat.find hex)) ∈ H
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
g : G
H : Subgroup G
⊢ (∃ n, H = zpowers (g ^ n)) → H ≤ zpowers g

Tactic:
· rintro ⟨k, rfl⟩
    exact zpowers_le_of_mem <| npow_mem_zpowers g k

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

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
⊢ (∀ (I : Ideal R) (h : I ∈ minimalPrimes R), { asIdeal := I, isPrime := ⋯ } ∈ Set.range (comap f)) →
    DenseRange (comap f)

Tactic:
· intro H p
    obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
    exact ((le_iff_specializes ⟨q, hq.1.1⟩ p).mp hq').mem_closed isClosed_closure
      (subset_closure (H q hq))

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval₂ (algebraMap R S) r (b.reverse * X ^ (1 + c.natDegree)) = 0

Tactic:
eval₂_eq_eval_map,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (map (algebraMap R S) (b.reverse * X ^ (1 + c.natDegree))) = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : h • (g • P).subtype h2 = P.subtype h1
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n

Tactic:
simp_rw [smul_subtype, Subgroup.smul_def, smul_smul] at hh

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
hy : g⁻¹ * x * g ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
h2 : ↑(g • P) ≤ centralizer ↑(zpowers x)
h : ↥(centralizer ↑(zpowers x))
hh : ((↑h * g) • P).subtype ⋯ = P.subtype h1
⊢ ∃ n ∈ normalizer ↑P, g⁻¹ * x * g = n⁻¹ * x * n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

Tactic:
obtain ⟨g, h⟩ := isCyclic_iff_exists_zpowers_eq_top.mp hG

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 ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card (↥(normalizer ↑H) ⧸ comap (normalizer ↑H).subtype H) ≡ Nat.card (G ⧸ H) [MOD p]

Tactic:
rw [← Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H)]

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↑(MulAction.fixedPoints (↥H) (G ⧸ H)) ≡ Nat.card (G ⧸ H) [MOD p]
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
x✝ : IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)
hM : IsCyclic M
hN : IsCyclic N
h : (Nat.card M).Coprime (Nat.card N)
f : M × N →* N := MonoidHom.snd M N
⊢ ↥f.ker ≃* M

Tactic:
rw [MonoidHom.ker_snd]
      exact ((Subgroup.prodEquiv ..).trans .prodUnique).trans Subgroup.topEquiv

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
p₁ : ℕ
hp₁ : p₁ ∈ ps
p₂ : ℕ
hp₂ : p₂ ∈ ps
hne : ⟨p₁, hp₁⟩ ≠ ⟨p₂, hp₂⟩
hp₁' : Fact (Nat.Prime p₁)
hp₂' : Fact (Nat.Prime p₂)
hne' : p₁ ≠ p₂
⊢ _root_.Disjoint ↑(P p₁) ↑(P p₂)

Tactic:
apply IsPGroup.disjoint_of_ne p₁ p₂ hne' _ _ (P p₁).isPGroup' (P p₂).isPGroup'

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module S N
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] N
hl : Function.Bijective ⇑l
⊢ IsSimpleModule R M ↔ IsSimpleModule S N

Tactic:
isSimpleModule_iff,

Goal state after:
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module S N
σ : R →+* S
inst✝ : RingHomSurjective σ
l : M →ₛₗ[σ] N
hl : Function.Bijective ⇑l
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleOrder (Submodule S N)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleModule R M ↔ IsSimpleModule S M

Tactic:
isSimpleModule_iff,

Goal state after:
S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleModule S M
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleModule S M

Tactic:
isSimpleModule_iff,

Goal state after:
S : Type u_3
inst✝⁶ : Ring S
M : Type u_4
inst✝⁵ : AddCommGroup M
R : Type u_6
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
h : Function.Surjective ⇑(algebraMap R S)
⊢ IsSimpleOrder (Submodule R M) ↔ IsSimpleOrder (Submodule S M)
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
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
x✝ : ∃ a, IsAtom a ∧ a ≤ ⊤
m : Submodule R ↥N
h : IsSimpleModule R ↥m
right✝ : m ≤ ⊤
⊢ IsSimpleModule R ↥(Submodule.map N.subtype m)

Tactic:
exact .congr (m.equivMapOfInjective _ N.subtype_injective).symm

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

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁸ : Ring R✝
inst✝⁷ : Ring S
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R✝ M
m : Submodule R✝ M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
ι : Type u_7
inst✝² : Finite ι
R : ι → Type u_6
inst✝¹ : (i : ι) → Ring (R i)
inst✝ : ∀ (i : ι), IsSemisimpleRing (R i)
⊢ IsSemisimpleRing ((i : ι) → R i)

Tactic:
let _ (i) : Module (Π i, R i) (R i) := Module.compHom _ (Pi.evalRingHom R i)
  let e (i) : R i →ₛₗ[Pi.evalRingHom R i] R i :=
    { AddMonoidHom.id (R i) with map_smul' := fun _ _ ↦ rfl }
  have (i : _) : IsSemisimpleModule (Π i, R i) (R i) :=
    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance
  infer_instance

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

Goal state before:
pp: case succ.e_a.e_a
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m) =
    single R (1 + j) m

Tactic:
rw [Nat.one_add]

Goal state after:
case succ.e_a.e_a
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m) =
    single R j.succ m
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∏ i ∈ S, ↑⋯.choose ∈ ⊤.annihilator

Tactic:
← hS,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∏ i ∈ S, ↑⋯.choose ∈ (span R ↑S).annihilator
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'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ I • map N.mkQ N'

Tactic:
← map_smul'',

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'
h_comap : Function.Injective (comap N.mkQ)
this : map N.mkQ (I • N') = map N.mkQ N'
⊢ map N.mkQ N' ≤ map N.mkQ (I • 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'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = J • map N.mkQ N'
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
← map_smul'',

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'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : map N.mkQ N' = map N.mkQ (J • N')
⊢ N ⊔ N' = N ⊔ J • 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
S : Set (I.Filtration M)
i : ℕ
⊢ I • sInf (N '' S) i ≤ sInf (N '' S) (i + 1)

Tactic:
by
        rw [sInf_eq_iInf', iInf_apply, iInf_apply]
        refine smul_iInf_le.trans ?_
        apply iInf_mono _
        rintro ⟨_, F, hF, rfl⟩
        exact F.smul_le i

Goal state after:
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 x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁
⊢ D.tensorProductTo (y₁ * y) =
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y₁ →
    D.tensorProductTo ((x₁ + y₁) * y) =
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ + y₁)

Tactic:
h₂

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
D : Derivation R S M
x y x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁ * y) =
    (TensorProduct.lmul' R) x₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x₁
h₂ :
  D.tensorProductTo (y₁ * y) =
    (TensorProduct.lmul' R) y₁ • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo y₁
⊢ D.tensorProductTo ((x₁ + y₁) * y) =
    (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo (x₁ + y₁)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.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₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
      (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
        (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂) →
    D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * (x₁ + y₁)) =
      (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
        (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)

Tactic:
h₂

Goal state after:
case refine_2.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₁✝ x₂ : S
x₁ y₁ : S ⊗[R] S
h₁ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * x₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo x₁ +
      (TensorProduct.lmul' R) x₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
h₂ :
  D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * y₁) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo y₁ +
      (TensorProduct.lmul' R) y₁ • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)
⊢ D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂ * (x₁ + y₁)) =
    (TensorProduct.lmul' R) (x₁✝ ⊗ₜ[R] x₂) • D.tensorProductTo (x₁ + y₁) +
      (TensorProduct.lmul' R) (x₁ + y₁) • D.tensorProductTo (x₁✝ ⊗ₜ[R] x₂)