mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Concrete

Goal state before:
pp: case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : ¬orderOf (p.cycleOf x) ∣ n.succ
hm' : ¬orderOf (p.cycleOf x) ∣ m.succ
⊢ n + 1 = m + 1

Tactic:
rw [← hc.support_pow_eq_iff] at hn' hm'

Goal state after:
case neg.succ.succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
hx : x ∈ (p.cycleOf x).support
hc : (p.cycleOf x).IsCycle
n : ℕ
hn✝ : n + 1 < (p.toList x).length
hn : n + 1 < orderOf (p.cycleOf x)
m : ℕ
hm✝ : m + 1 < (p.toList x).length
hm : m + 1 < orderOf (p.cycleOf x)
h : (p.cycleOf x ^ (n + 1)) x = (p.cycleOf x ^ (m + 1)) x
hn' : (p.cycleOf x ^ n.succ).support = (p.cycleOf x).support
hm' : (p.cycleOf x ^ m.succ).support = (p.cycleOf x).support
⊢ n + 1 = m + 1
Module: Mathlib.Algebra.Lie.Loop

Goal state before:
pp: case pos
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ b • (Φ ⁅x, z⁆) y = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x

Tactic:
hΦ,

Goal state after:
case pos
R : Type u_1
A : Type u_2
L : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : LieRing L
inst✝³ : LieAlgebra R L
inst✝² : CommRing A
inst✝¹ : IsAddTorsionFree R
inst✝ : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
h0 : a + b + c = 0
⊢ b • -(Φ z) ⁅x, y⁆ = c • (Φ ⁅x, y⁆) z + a • (Φ ⁅y, z⁆) x
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
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ α' ∈ S (p + 1) i, ∑ t, bminor A i (α' t) (t.removeNth α') * A (α' t) j

Tactic:
← Finset.sum_product'

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n) (Fin n) R
p : ℕ
i j : Fin n
⊢ ∑ x ∈ S p i ×ˢ Finset.Ioi i, bminor A i x.2 x.1 * A x.2 j =
    ∑ x ∈ S (p + 1) i ×ˢ Finset.univ, bminor A i (x.1 x.2) (x.2.removeNth x.1) * A (x.1 x.2) j
Module: Mathlib.Algebra.Lie.LieTheorem

Goal state before:
pp: case h
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
imL : LieSubalgebra k (Module.End k V) := ⋯
toEndo : L →ₗ[k] ↥imL := ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
⊢ Nontrivial ↥(weightSpace V ⇑(χ ∘ₗ toEndo))

Tactic:
obtain ⟨⟨v, hv⟩, hv0⟩ := exists_ne (0 : weightSpace V χ)

Goal state after:
case h
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
imL : LieSubalgebra k (Module.End k V) := (toEnd k L V).range
toEndo : L →ₗ[k] ↥imL := LinearMap.codRestrict imL.toSubmodule ↑(toEnd k L V) ⋯
χ : Module.Dual k ↥imL
h : Nontrivial ↥(weightSpace V ⇑χ)
v : V
hv : v ∈ weightSpace V ⇑χ
hv0 : ⟨v, hv⟩ ≠ 0
⊢ Nontrivial ↥(weightSpace V ⇑(χ ∘ₗ toEndo))
Module: Mathlib.Algebra.LieRinehartAlgebra.Defs

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst✝²⁰ : CommRing R
inst✝¹⁹ : CommRing A₁
inst✝¹⁸ : LieRing L₁
inst✝¹⁷ : Module A₁ L₁
inst✝¹⁶ : LieRingModule L₁ A₁
inst✝¹⁵ : CommRing A₂
inst✝¹⁴ : LieRing L₂
inst✝¹³ : Module A₂ L₂
inst✝¹² : LieRingModule L₂ A₂
inst✝¹¹ : CommRing A₃
inst✝¹⁰ : LieRing L₃
inst✝⁹ : Module A₃ L₃
inst✝⁸ : LieRingModule L₃ A₃
inst✝⁷ : Algebra R A₁
inst✝⁶ : LieAlgebra R L₁
inst✝⁵ : Algebra R A₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : Algebra R A₃
inst✝² : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst✝¹ : LieRinehartRing A₁ L₁
inst✝ : LieRinehartAlgebra R A₁ L₁
x✝¹ x✝ : L₁
⊢ Derivation.mk' ((LieModule.toEnd R L₁ A₁) ⁅x✝¹, x✝⁆) ⋯ =
    ⁅Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝¹) ⋯, Derivation.mk' ((LieModule.toEnd R L₁ A₁) x✝) ⋯⁆

Tactic:
by ext; simp [Derivation.commutator_apply]

Goal state after:
Module: Mathlib.RingTheory.ChainOfDivisors

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

Tactic:
rw [← Finset.card_fin (i + 1)]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : UniqueFactorizationMonoid M
q r : Associates M
n : ℕ
hn : n ≠ 0
c : Fin (n + 1) → Associates M
h₁ : StrictMono c
h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i
hr : r ∣ q
hq : q ≠ 0
i : ℕ := (normalizedFactors r).card
hi : normalizedFactors r = Multiset.replicate i (c 1)
H : r = c 1 ^ i
| Finset.univ.card
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 J : FractionalIdeal S P
⊢ I * J = ⟨↑I * ↑J, ⋯⟩

Tactic:
by simp only [← mul_eq_mul, mul_def']

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

Goal state before:
pp: K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * I⁻¹ = 1

Tactic:
by rwa [← right_inverse_eq K I J hJ]

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

Goal state before:
pp: case pos
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 ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1

Tactic:
rw [hJ0, inv_zero']

Goal state after:
case pos
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 ≠ ⊥
hJ0 : ↑I * (↑I)⁻¹ = 0
⊢ 0 ≤ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J

Tactic:
have : P.IsMaximal := by
          refine ⟨⟨mt Ideal.isUnit_iff.mpr hirr.not_isUnit, ?_⟩⟩
          intro J hJ
          obtain ⟨_J_ne, H, hunit, P_eq⟩ := Ideal.dvdNotUnit_iff_lt.mpr hJ
          exact Ideal.isUnit_iff.mp ((hirr.isUnit_or_isUnit P_eq).resolve_right hunit)

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
P : Ideal A
hirr : Irreducible P
I J : Ideal A
this : P.IsMaximal
⊢ P ∣ I * J → P ∣ I ∨ P ∣ J
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors I))

Tactic:
apply torsionBySet_isInternal (p := fun p => p ^ P.count p) _

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := ⋯
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ Module.IsTorsionBySet R M ↑(⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P)

R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := ⋯
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ (↑(factors I).toFinset).Pairwise fun i j ↦ i ^ Multiset.count i P ⊔ j ^ Multiset.count j P = ⊤
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ ¬(Multiset.count q P ≠ 0 ∧ p = normalize q)

Tactic:
exact fun H => pq <| H.2.trans <| normalize_eq q

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

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ⊓ J ∣ lcm I J

Tactic:
rw [dvd_iff_le, le_inf_iff, ← dvd_iff_le, ← dvd_iff_le]
      exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩

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

Goal state before:
pp: ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
⊢ (decomposeAddEquiv 𝓜) (↑(((decompose 𝓐) x) i) • ∑ i ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓜) y) i)) =
    ↑(((decompose 𝓐) x) i) • ∑ x ∈ DFinsupp.support ((decompose 𝓜) y), (decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) x)

Tactic:
Finset.smul_sum,

Goal state after:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst✝¹⁵ : AddMonoid ιA
inst✝¹⁴ : AddAction ιA ιM
inst✝¹³ : CommSemiring R
inst✝¹² : Semiring A
inst✝¹¹ : Algebra R A
𝓐 : ιA → σ'
inst✝¹⁰ : SetLike σ' A
𝓜 : ιM → σ
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module A M
inst✝⁷ : SetLike σ M
inst✝⁶ : AddSubmonoidClass σ' A
inst✝⁵ : AddSubmonoidClass σ M
inst✝⁴ : SetLike.GradedSMul 𝓐 𝓜
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιM
inst✝¹ : GradedRing 𝓐
inst✝ : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi : i ∈ DFinsupp.support ((decompose 𝓐) x)
⊢ (decomposeAddEquiv 𝓜)
      (∑ x_1 ∈ DFinsupp.support ((decompose 𝓜) y), ↑(((decompose 𝓐) x) i) • ↑(((decompose 𝓜) y) x_1)) =
    ↑(((decompose 𝓐) x) i) • ∑ x ∈ DFinsupp.support ((decompose 𝓜) y), (decomposeAddEquiv 𝓜) ↑(((decompose 𝓜) y) x)
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f g : V →ₗ[K] V₂
hf : f.HasNoetherianRange
hg : g.HasNoetherianRange
⊢ (f + g).HasNoetherianRange

Tactic:
rw [HasNoetherianRange] at *
  exact isNoetherian_of_le (range_add_le f g)

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : Module.FinitePresentation R M
⊢ Module.Finite R M

Tactic:
obtain ⟨s, hs₁, _⟩ := h
  exact ⟨s, hs₁⟩

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
v' : V₃ →ₗ[K] V₂
hu : u'.IsLeftQuasiInverse u
hv : v'.IsLeftQuasiInverse v
⊢ u' ∘ₗ (v' ∘ₗ v) ∘ₗ u ≈ u' ∘ₗ id ∘ₗ u

Tactic:
hv.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
v' : V₃ →ₗ[K] V₂
hu : u'.IsLeftQuasiInverse u
hv : v'.IsLeftQuasiInverse v
⊢ u' ∘ₗ id ∘ₗ u ≈ u' ∘ₗ id ∘ₗ u
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₃
v' : V₃ →ₗ[K] V₂
w : V₃ →ₗ[K] V
hv : v'.IsLeftQuasiInverse v
hw : w.IsRightQuasiInverse (v ∘ₗ u)
⊢ id ∘ₗ u ∘ₗ w ∘ₗ v ≈ (v' ∘ₗ v) ∘ₗ u ∘ₗ w ∘ₗ v

Tactic:
hv.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₃
v' : V₃ →ₗ[K] V₂
w : V₃ →ₗ[K] V
hv : v'.IsLeftQuasiInverse v
hw : w.IsRightQuasiInverse (v ∘ₗ u)
⊢ id ∘ₗ u ∘ₗ w ∘ₗ v ≈ id ∘ₗ u ∘ₗ w ∘ₗ v
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
⊢ span {a} ∈ normalizedFactors (span {b})

Tactic:
· suffices Prime (span ({a} : Set R)) by
      obtain ⟨c, hc, hc'⟩ := exists_mem_normalizedFactors_of_dvd ?_ this.irreducible
          (dvd_iff_le.mpr (span_singleton_le_span_singleton.mpr (dvd_of_mem_normalizedFactors ha)))
      rwa [associated_iff_eq.mp hc']
    · by_contra h
      exact hb (span_singleton_eq_bot.mp h)
    rw [prime_iff_isPrime]
    · exact (span_singleton_prime (prime_of_normalized_factor a ha).ne_zero).mpr
        (prime_of_normalized_factor a ha)
    · by_contra h
      exact (prime_of_normalized_factor a ha).ne_zero (span_singleton_eq_bot.mp h)

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

Goal state before:
pp: case refine_2
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
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)

Tactic:
have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)

Goal state after:
case refine_2
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
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
hP : Prime p
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

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

Tactic:
by classical simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case inl
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f p : MvPolynomial σ R
j : σ
eq : (pderiv j) ((map φ) p) = (map φ) ((pderiv j) p)
⊢ (pderiv j) ((map φ) (p * X j)) = (map φ) ((pderiv j) (p * X j))

pp: case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Tactic:
· simp [eq]

Goal state after:
case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = (mvPolynomialQuotientEquiv S r) ((Ideal.Quotient.mk (Ideal.span {C r * X () - 1})) (X x))

Tactic:
IsLocalization.Away.mvPolynomialQuotientEquiv_apply,

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : Unit
⊢ invSelf r = (aeval fun x ↦ invSelf r) (X x)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R' R''
inst✝³ : Algebra R R''
inst✝² : Algebra S S'
inst✝¹ : Algebra S' S''
inst✝ : Algebra S S''
f : P.Hom P'
alg : Algebra P.Ring P'.Ring
halg : algebraMap P.Ring P'.Ring = f.toRingHom
⊢ ∀ (m : P.Ring) (x : ↥P.ker), ⟨f.toRingHom ↑(m • x), ⋯⟩ = (RingHom.id P.Ring) m • ⟨f.toRingHom ↑x, ⋯⟩

Tactic:
simp [Algebra.smul_def, ← halg]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case C
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 ι σ
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
a : T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) ((algebraTensorAlgEquiv R T).symm (C a)) =
    a ⊗ₜ[R] 1

Tactic:
← MvPolynomial.algebraMap_eq,

Goal state after:
case C
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 ι σ
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
a : T
⊢ (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S))
      ((algebraTensorAlgEquiv R T).symm ((algebraMap T (MvPolynomial ι T)) a)) =
    a ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
r : P.Ring
x : P.Cotangent
⊢ (P.σ ((algebraMap P.Ring S) r) - r) • x.val = 0

Tactic:
exact Cotangent.smul_eq_zero_of_mem _ (by simp) _

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

Goal state before:
pp: case h
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 ι
a : S
⊢ (aeval fun x ↦ C (P.val x)) (P.σ a) = C a

Tactic:
← MvPolynomial.algebraMap_eq,

Goal state after:
case h
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 ι
a : S
⊢ (aeval fun x ↦ (algebraMap S (MvPolynomial ι' S)) (P.val x)) (P.σ a) = (algebraMap S (MvPolynomial ι' S)) a
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ (((Q.ofComp P).toAlgHom.comp (aeval (X ∘ Sum.inr))) (P.σ ((↑x).coeff j)) *
      j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)

Tactic:
comp_aeval

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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ ((aeval fun i ↦ (Q.ofComp P).toAlgHom ((X ∘ Sum.inr) i)) (P.σ ((↑x).coeff j)) *
      j.prod fun a b ↦ (Q.ofComp P).val (Sum.inl a) ^ b) =
    (monomial j) (coeff j ↑x)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e_a
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ eval₂ ((algebraMap S Q.Ring).comp (algebraMap R S)) (fun i ↦ C (P.val i)) (P.σ ((↑x).coeff j)) = C (coeff j ↑x)

Tactic:
← MvPolynomial.algebraMap_eq,

Goal state after:
case e_a
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.ker
j : ι' →₀ ℕ
x✝ : j ∈ support ↑x
⊢ eval₂ ((algebraMap S Q.Ring).comp (algebraMap R S)) (fun i ↦ (algebraMap S (MvPolynomial ι' S)) (P.val i))
      (P.σ ((↑x).coeff j)) =
    (algebraMap S (MvPolynomial ι' S)) (coeff j ↑x)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
⊢ Nontrivial Mₚ''

Tactic:
rw [Submodule.Quotient.nontrivial_iff, ne_comm]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
⊢ ⊤ ≠ Ideal.map (algebraMap R Rₚ) I • ⊤