mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ α ∈ S (p + 1) i, bminor A i j α =
    ∑ α ∈ S (p + 1) i, (pminor A α * A i j - ∑ t, bminor A i (α t) (t.removeNth α) * A (α t) j)

Tactic:
by
      exact Finset.sum_congr rfl <| by simp [det_bordered_expand]

Goal state after:
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case inl
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : ↑(derivedSeries k L 1) = ⊤
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
obtain _ | _ := subsingleton_or_nontrivial L

Goal state after:
case inl.inl
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Subsingleton L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

case inl.inr
k : Type u_1
inst✝¹² : Field k
V : Type u_3
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module k V
inst✝⁹ : CharZero k
inst✝⁸ : Module.Finite k V
inst✝⁷ : Nontrivial V
L : Type u_4
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra k L
inst✝⁴ : LieRingModule L V
inst✝³ : LieModule k L V
inst✝² : IsSolvable L
inst✝¹ : IsTriangularizable k L V
inst✝ : Module.Finite k L
H : ↑(derivedSeries k L 1) = ⊤
h✝ : Nontrivial L
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: k : Type u_1
inst✝¹¹ : Field k
L : Type u_2
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
V : Type u_3
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module k V
inst✝⁶ : LieRingModule L V
inst✝⁵ : LieModule k L V
inst✝⁴ : CharZero k
inst✝³ : Module.Finite k V
inst✝² : Nontrivial V
inst✝¹ : IsSolvable L
inst✝ : IsTriangularizable k L V
⊢ ∃ χ, Nontrivial ↥(weightSpace V ⇑χ)

Tactic:
let imL := (toEnd k L V).range
  let toEndo : L →ₗ[k] imL := LinearMap.codRestrict imL.toSubmodule (toEnd k L V)
      (fun x ↦ LinearMap.mem_range.mpr ⟨x, rfl⟩ : ∀ x : L, (toEnd k L V) x ∈ imL)
  have ⟨χ, h⟩ := exists_forall_lie_eq_smul_of_isSolvable_of_finite k V imL
  use χ.comp toEndo
  obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)
  refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
  · rw [mem_weightSpace] at hv ⊢
    intro x
    apply hv (toEndo x)
  · simpa using hv0

Goal state after:
Module: Mathlib.Algebra.LinearRecurrence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
E : LinearRecurrence R
⊢ E.charPoly.Monic

Tactic:
by
  nontriviality R
  rw [Monic, leadingCoeff, natDegree_eq_of_degree_eq_some <| charPoly_degree_eq_order _, charPoly,
    coeff_sub, coeff_monomial_same, finsetSum_coeff, sub_eq_self]
  refine sum_eq_zero fun _ _ ↦ coeff_eq_zero_of_degree_lt ?_
  grw [degree_monomial_le]
  simp

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n✝ : ℕ
hn : n✝ + 1 ≠ 0
c : Fin (n✝ + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ (Finset.image (fun m ↦ c 1 ^ ↑m) Finset.univ).card = Finset.univ.card

Tactic:
Finset.card_image_iff

Goal state after:
case succ
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
n✝ : ℕ
hn : n✝ + 1 ≠ 0
c : Fin (n✝ + 1 + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
⊢ Set.InjOn (fun m ↦ c 1 ^ ↑m) ↑Finset.univ
Module: Mathlib.RingTheory.FractionalIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : FractionalIdeal S P
⊢ 0 ≤ I

Tactic:
intro x hx
  convert! zero_mem I
  rw [(mem_zero_iff _).mp hx]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

Goal state before:
pp: M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : d x = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ b = ⊥

Tactic:
rw [this, OrderIso.map_bot d] at hx

Goal state after:
M : Type u_1
inst✝⁴ : CommMonoidWithZero M
inst✝³ : IsCancelMulZero M
N : Type u_2
inst✝² : CommMonoidWithZero N
inst✝¹ : UniqueFactorizationMonoid N
inst✝ : UniqueFactorizationMonoid M
m p : Associates M
n : Associates N
hn : n ≠ 0
hp : p ∈ normalizedFactors m
d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)
b : Associates N
this✝² : b ≤ n
x : ↑(Set.Iic m)
hb : ↑(d x) < ↑(d ⟨p, ⋯⟩)
hx : ⊥ = ⟨b, this✝²⟩
this✝¹ : OrderBot { l // l ≤ m } := Subtype.orderBot ⋯
this✝ : OrderBot { l // l ≤ n } := Subtype.orderBot ⋯
this : x = ⊥
⊢ b = ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
P : Type u_2
inst✝³ : CommRing P
inst✝² : Algebra R P
P' : Type u_3
inst✝¹ : CommRing P'
inst✝ : Algebra R P'
I : FractionalIdeal S P'
g : P ≃ₐ[R] P'
⊢ map (↑g) (map (↑g.symm) I) = I

Tactic:
by
  rw [← map_comp, g.comp_symm, map_id]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I : Ideal A
hI0 : I ≠ ⊥
hI1 : I ≠ ⊤
hNF : ¬IsField A
this : ∀ {I : Ideal A}, I ≠ ⊥ → I ≠ ⊤ → I.IsMaximal → ¬(↑I)⁻¹ ≤ 1
hM : ¬I.IsMaximal
⊢ ¬(↑I)⁻¹ ≤ 1

Tactic:
rcases I.exists_le_maximal hI1 with ⟨M, hmax, hIM⟩
    have hMbot : M ≠ ⊥ := (M.bot_lt_of_maximal hNF).ne'
    refine mt (le_trans <| inv_anti_mono ?_ ?_ ?_) (this hMbot hmax.ne_top hmax) <;>
      simpa only [coeIdeal_ne_zero, coeIdeal_le_coeIdeal]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • (b * (algebraMap R₁ K) y')

Tactic:
mul_comm b,

Goal state after:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J : Submodule R₁ K
aI : R₁
haI : aI ∈ R₁⁰
hI : ∀ b ∈ I, IsInteger R₁ (aI • b)
aJ : R₁
haJ : aJ ∈ R₁⁰
hJ : ∀ b ∈ J, IsInteger R₁ (aJ • b)
h : J ≠ 0
y : K
mem_J : y ∈ J
notMem_zero : y ∉ 0
y' : R₁
hy' : (algebraMap R₁ K) y' = aJ • y
b : K
hb : b ∈ I / J
⊢ (aI * y') • b = aI • ((algebraMap R₁ K) y' * b)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mp
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsFractionRing K L
I : FractionalIdeal K⁰ L
hI : ¬I = 0
n : K
d : ↥K⁰
x_mem : mk' L n d ∈ I
⊢ (algebraMap K L) (n / ↑d) = mk' L n d

Tactic:
rw [map_div₀, IsFractionRing.mk'_eq_div]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
a' : ↥R₁⁰
ha' : ∀ i ∈ s, IsInteger R₁ (↑a' • f i)
x : K
hx : x ∈ span R₁ (f '' ↑s)
⊢ ∀ (a : R₁), ∀ x ∈ span R₁ (f '' ↑s), IsInteger R₁ (↑a' • x) → IsInteger R₁ (↑a' • a • x)

Tactic:
intro c x _ hx
      rw [smul_comm]
      exact IsLocalization.isInteger_smul hx

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case inr
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
a : A
ha : a ≠ 0
⊢ Prime (span {a}) ↔ Prime a

Tactic:
· have ha' : span {a} ≠ ⊥ := by simpa only [ne_eq, span_singleton_eq_bot] using ha
    rw [prime_iff_isPrime ha', span_singleton_prime ha]

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

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ 1 • x = x

Tactic:
suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from DFunLike.congr_fun this x

Goal state after:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ (smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ιB), M i)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : J ≠ ⊥
this : (normalizedFactors I ∩ normalizedFactors J).prod ≠ 0
⊢ I ⊔ J ≤ (normalizedFactors I ∩ normalizedFactors J).prod

Tactic:
rw [sup_le_iff, ← dvd_iff_le, ← dvd_iff_le]
    constructor <;>
      rw [dvd_iff_normalizedFactors_le_normalizedFactors this (by assumption),
        normalizedFactors_prod_inter_eq_inter]
    exacts [inf_le_left, inf_le_right]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : Semiring K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : AddCommMonoid V₂
inst✝² : Module K V₂
inst✝¹ : AddCommMonoid V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
h : u.HasNoetherianRange
v : V₂ →ₗ[K] V₃
⊢ (v ∘ₗ u).HasNoetherianRange

Tactic:
rw [LinearMap.HasNoetherianRange, LinearMap.range_comp] at *
  infer_instance

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
u' : V₂ →ₗ[K] V
w : V₃ →ₗ[K] V
hu : u'.IsRightQuasiInverse u
hw : w.IsLeftQuasiInverse (v ∘ₗ u)
⊢ ((u ∘ₗ w) ∘ₗ v) ∘ₗ id ≈ ((u ∘ₗ w) ∘ₗ v) ∘ₗ u ∘ₗ u'

Tactic:
hu.equiv

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v : V₂ →ₗ[K] V₃
u' : V₂ →ₗ[K] V
w : V₃ →ₗ[K] V
hu : u'.IsRightQuasiInverse u
hw : w.IsLeftQuasiInverse (v ∘ₗ u)
⊢ ((u ∘ₗ w) ∘ₗ v) ∘ₗ id ≈ ((u ∘ₗ w) ∘ₗ v) ∘ₗ id
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Field K
inst✝³ : IsDedekindDomain A
I : Ideal R
J : Ideal A
B : Type u_4
inst✝² : CommRing B
inst✝¹ : IsDedekindDomain B
L : Ideal B
inst✝ : IsDedekindDomain R
f : R ⧸ I ≃+* A ⧸ J
f_surj : Function.Surjective ⇑↑f
fsym_surj : Function.Surjective ⇑↑f.symm
⊢ (idealFactorsFunOfQuotHom fsym_surj).comp (idealFactorsFunOfQuotHom f_surj) = OrderHom.id

Tactic:
simpa using! idealFactorsFunOfQuotHom_comp f_surj fsym_surj

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ Associates.mk J ^ (Associates.mk J).count (Associates.mk I).factors ≤ Associates.mk I

Tactic:
rw [Associates.prime_pow_dvd_iff_le hI hJ']

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬Associates.mk J ^ ((Associates.mk J).count (Associates.mk I).factors + 1) ≤ Associates.mk I

Tactic:
rw [Associates.prime_pow_dvd_iff_le hI hJ']

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬(Associates.mk J).count (Associates.mk I).factors + 1 ≤ (Associates.mk J).count (Associates.mk I).factors
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
y : ↥S := commonDenomOfFinset S f s
hx₁ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
apply congrArg (Submodule.span R) at hx₁

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : Submodule.span R (y • ↑s) = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case hsucc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ ¬a ^ (multiplicity a b + 1) ∣ b

Tactic:
apply h.not_pow_dvd_of_multiplicity_lt
      apply lt_add_one

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
x : M
s : Finset M'
hx : f x ∈ Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
let y : S := IsLocalizedModule.commonDenomOfFinset S f s
  have hx₁ : y • (s : Set M') = f '' _ :=
    (IsLocalizedModule.finsetIntegerMultiple_image S f s).symm
  apply congrArg (Submodule.span R) at hx₁
  rw [Submodule.span_smul] at hx₁
  replace hx : _ ∈ y • Submodule.span R (s : Set M') := Set.smul_mem_smul_set hx
  rw [hx₁, ← f.map_smul, ← Submodule.map_span f] at hx
  obtain ⟨x', hx', hx''⟩ := hx
  obtain ⟨a, ha⟩ := (IsLocalizedModule.eq_iff_exists S f).mp hx''
  use a * y
  convert!
    (Submodule.span R (IsLocalizedModule.finsetIntegerMultiple S f s : Set M)).smul_mem a hx'
      using 1
  convert! ha.symm using 1
  simp only [Submonoid.smul_def, ← smul_smul]

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
n : ℕ
⊢ p ^ n • x = 0 ↔ Associates.mk (generator (torsionOf R M x)) ∣ Associates.mk p ^ n

Tactic:
rw [← Associates.mk_pow, Associates.mk_dvd_mk, ← mem_iff_generator_dvd]

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x : M
n : ℕ
⊢ p ^ n • x = 0 ↔ p ^ n ∈ torsionOf R M x
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case pos.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
this : f.symm ⟨p ^ k • x, h⟩ ∈ R ∙ (Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (p ^ k)
⊢ ∃ a, p ^ k • x = p ^ k • a • y

Tactic:
Submodule.mem_span_singleton

Goal state after:
case pos.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
this : ∃ a, a • (Ideal.Quotient.mk (R ∙ p ^ (pOrder hM y - k) * p ^ k)) (p ^ k) = f.symm ⟨p ^ k • x, h⟩
⊢ ∃ a, p ^ k • x = p ^ k • a • y
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ (pderiv i) (X j) = 0

Tactic:
by
  classical simp [h]

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

Goal state before:
pp: case zero
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ x • 1 ∈ ⊤ ⊓ annihilator R (Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)

Tactic:
annihilator_dfinsupp,

Goal state after:
case zero
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ x • 1 ∈ ⊤ ⊓ ⨅ i, annihilator R (R ⧸ R ∙ p i ^ n i)
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
⊢ e.symm x ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))

Tactic:
RingHom.mem_ker,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) (e.symm x) = 0
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
⊢ RingHom.ker (Q.aux P) = Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))

Tactic:
rw [aux_eq_comp, ← AlgHom.comap_ker, MvPolynomial.ker_mapAlgHom]
  change Ideal.comap _ (Ideal.map (IsScalarTower.toAlgHom R (MvPolynomial ι R) _) _) = _
  rw [← sumAlgEquiv_comp_rename_inr, ← Ideal.map_mapₐ, Ideal.comap_map_of_bijective]
  simpa using AlgEquiv.bijective (sumAlgEquiv R ι' ι)

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ x ∈ RingHom.ker (aeval (Q.comp P).val)

Tactic:
RingHom.mem_ker,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
x : (Q.comp P).Ring
hx : (Q.ofComp P).toAlgHom x = 0
⊢ (aeval (Q.comp P).val) x = 0