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

Goal state before:
pp: case refine_2
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
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
h_yb : ∃ a_1, a_1 * a = y * b
⊢ (algebraMap A K) (y * b) * ((algebraMap A K) a)⁻¹ ∈ 1

Tactic:
rcases h_yb with ⟨c, hc⟩

Goal state after:
case refine_2
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
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) (y * b) * ((algebraMap A K) a)⁻¹ ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case neg
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
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹
y : K
hy : y ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range
⊢ y ∈ ↑(↑I)⁻¹

Tactic:
obtain ⟨p, rfl⟩ := (AlgHom.mem_range _).mp hy

Goal state after:
case neg
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
x : K
hx : x ∈ (↑I * (↑I)⁻¹)⁻¹
x_mul_mem : ∀ b ∈ (↑I)⁻¹, x * b ∈ (↑I)⁻¹
p : A[X]
hy : (Polynomial.aeval x) p ∈ Subalgebra.toSubmodule (Polynomial.aeval x).range
⊢ (Polynomial.aeval x) p ∈ ↑(↑I)⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case inr.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I * (J⁻¹ * J) ≤ I

Tactic:
mul_comm _ J,

Goal state after:
case inr.refine_2
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I✝ J✝ I J : FractionalIdeal A⁰ K
hJ : J ≠ 0
⊢ I * (J * J⁻¹) ≤ I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
⊢ IsNoetherianRing A

Tactic:
refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
this : CommGroupWithZero (FractionalIdeal A⁰ (FractionRing A)) := commGroupWithZero (FractionRing A) h
I : Ideal A
⊢ Submodule.FG I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥

Tactic:
exact coeIdeal_ne_zero.mp (right_ne_zero_of_mul hI)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ p = comap (algebraMap R A) P ↔ comap (algebraMap R A) P = p

Tactic:
eq_comm

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra R A
p : Ideal R
P : Ideal A
hP : P ≠ ⊤
inst✝ : p.IsMaximal
⊢ comap (algebraMap R A) P = p ↔ comap (algebraMap R A) P = 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
⊢ ⨅ i ∈ (factors I).toFinset, i ^ Multiset.count i P = I

Tactic:
← Finset.inf_eq_iInf,

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) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
⊢ ((factors I).toFinset.inf fun i ↦ i ^ Multiset.count i P) = I
Module: Mathlib.RingTheory.Flat.IsBaseChange

Goal state before:
pp: R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : IsBaseChange S h₂
isb₃ : IsBaseChange S h₃
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
⊢ IsBaseChange S h₁

Tactic:
simp only [IsBaseChange, IsTensorProduct] at isb₂ isb₃ ⊢

Goal state after:
R : Type u_1
inst✝²¹ : CommRing R
S : Type u_2
inst✝²⁰ : CommRing S
inst✝¹⁹ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁸ : AddCommGroup M₁
inst✝¹⁷ : AddCommGroup M₂
inst✝¹⁶ : AddCommGroup M₃
inst✝¹⁵ : AddCommGroup N₁
inst✝¹⁴ : AddCommGroup N₂
inst✝¹³ : AddCommGroup N₃
inst✝¹² : Module R M₁
inst✝¹¹ : Module R M₂
inst✝¹⁰ : Module R M₃
inst✝⁹ : Module R N₁
inst✝⁸ : Module R N₂
inst✝⁷ : Module R N₃
inst✝⁶ : Module S N₁
inst✝⁵ : Module S N₂
inst✝⁴ : Module S N₃
inst✝³ : IsScalarTower R S N₁
inst✝² : IsScalarTower R S N₂
inst✝¹ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
inst✝ : Module.Flat R S
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
isb₃ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₃ →ₗ[R] N₃))).flip h₃)))
exact₁ : Function.Exact ⇑f ⇑g
inj₁ : Function.Injective ⇑f
exact₂ : Function.Exact ⇑f' ⇑g'
inj₂ : Function.Injective ⇑f'
⊢ Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J * spanSingleton R₁⁰ (d⁻¹ * d) ≤ J

Tactic:
inv_mul_cancel₀ hd,

Goal state after:
case a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ J * spanSingleton R₁⁰ 1 ≤ J
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case a
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₁
J : FractionalIdeal R₁⁰ K
d : K
hd : ¬d = 0
h_spand : spanSingleton R₁⁰ d ≠ 0
⊢ 1 / spanSingleton R₁⁰ d * J ≤ J / spanSingleton R₁⁰ d

Tactic:
· rw [le_div_iff_mul_le h_spand, mul_assoc, mul_left_comm, one_div_spanSingleton,
      spanSingleton_mul_spanSingleton, inv_mul_cancel₀ hd, spanSingleton_one, mul_one]

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

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J
⊢ ∀ z ∈ I, x * z ∈ J

Tactic:
zI

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
h : ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J
zI : P
⊢ zI ∈ I → x * zI ∈ J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ J ^ count J (normalizedFactors I) = J ^ multiplicity J I

Tactic:
congr
    rw [← Nat.cast_inj (R := ℕ∞), ← FiniteMultiplicity.emultiplicity_eq_multiplicity,
      emultiplicity_eq_count_normalizedFactors hJ hI, normalize_eq J]
    rw [← emultiplicity_lt_top]
    apply hn.trans_lt
    simp

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

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
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ X ≤ comap (Ideal.Quotient.mk I) (map (Ideal.Quotient.mk I) Y)

Tactic:
comap_map_of_surjective (Ideal.Quotient.mk I)
      Ideal.Quotient.mk_surjective,

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
I : Ideal R
J : Ideal A
f : R ⧸ I →+* A ⧸ J
hf : Function.Surjective ⇑f
X : Ideal R
hX : X ∣ I
Y : Ideal R
hY : Y ∣ I
h : X ≤ Y
⊢ X ≤ Y ⊔ comap (Ideal.Quotient.mk I) ⊥
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ↑(sec i).2 * ∏ i ∈ s.erase i, ↑(sec i).2 = ∏ i ∈ s, ↑(sec i).2

Tactic:
← Finset.prod_insert (f := fun i ↦ ((sec i).snd).val) (s.notMem_erase i),

Goal state after:
case refine_2.e_a
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ ∏ x ∈ insert i (s.erase i), ↑(sec x).2 = ∏ i ∈ s, ↑(sec i).2
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
⊢ Function.Injective fun d ↦ ⟨span {↑d}, ⋯⟩

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩ h

Goal state after:
case refine_2.refine_1
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
a : R
ha : a ∈ {d | d ∈ normalizedFactors r}
b : R
hb : b ∈ {d | d ∈ normalizedFactors r}
h : (fun d ↦ ⟨span {↑d}, ⋯⟩) ⟨a, ha⟩ = (fun d ↦ ⟨span {↑d}, ⋯⟩) ⟨b, hb⟩
⊢ ⟨a, ha⟩ = ⟨b, hb⟩
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) + (monomial s) 1 • f i =
    (monomial s) 1 • f i +
      (monomial (Finsupp.single i 1)) 1 • s.sum fun i k ↦ (monomial (s - Finsupp.single i 1)) ↑k • f i

Tactic:
add_comm,

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((monomial s) 1 • f i + s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (monomial s) 1 • f i +
      (monomial (Finsupp.single i 1)) 1 • s.sum fun i k ↦ (monomial (s - Finsupp.single i 1)) ↑k • f i
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial (single i 1 + (m - single i 1))) (↑(m i) * r) = (monomial m) (↑(m i) * r)

Tactic:
add_comm,

Goal state after:
case neg
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
h : ¬m i = 0
⊢ (monomial (m - single i 1 + single i 1)) (↑(m i) * r) = (monomial m) (↑(m i) * r)
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ (auxInv S r).comp (auxHom S r).toRingHom = RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1})

Tactic:
rw [← RingHom.cancel_right (Ideal.Quotient.mk_surjective)]
  ext x
  · simp [auxInv]
  · simp only [auxInv, AlgHom.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
      Function.comp_apply, auxHom_mk, aeval_X, RingHomCompTriple.comp_eq, invSelf, Away.lift,
      lift_mk'_spec]
    simp only [map_one]
    rw [← map_one (Ideal.Quotient.mk _), ← map_mul, Ideal.Quotient.mk_eq_mk_iff_sub_mem,
      ← Ideal.neg_mem_iff, neg_sub]
    exact Ideal.mem_span_singleton_self (C r * X x - 1)

Goal state after:
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 ι σ
⊢ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i)) =
    RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val)

Tactic:
apply le_antisymm
  · rw [Ideal.span_le]
    intro x ⟨y, hy⟩
    have Z := aeval_val_relation P y
    apply_fun TensorProduct.includeRight (R := R) (A := T) at Z
    rw [map_zero] at Z
    simp only [SetLike.mem_coe, RingHom.mem_ker, ← Z, ← hy,
      TensorProduct.includeRight_apply]
    rw [aeval_map_algebraMap T (P.baseChange T).val (P.relation y)]
    change _ = TensorProduct.includeRight.toRingHom _
    rw [map_aeval, AlgHom.toRingHom_eq_coe, RingHom.coe_coe,
      TensorProduct.includeRight.comp_algebraMap]
    rfl
  · intro x hx
    rw [RingHom.mem_ker] at hx
    have H := Algebra.TensorProduct.lTensor_ker (A := T) (IsScalarTower.toAlgHom R P.Ring S)
      P.algebraMap_surjective
    let e := MvPolynomial.algebraTensorAlgEquiv (R := R) (σ := ι) (A := T)
    have H' : e.symm x ∈ RingHom.ker (TensorProduct.map (AlgHom.id R T)
        (IsScalarTower.toAlgHom R P.Ring S)) := by
      rw [RingHom.mem_ker, ← hx]
      clear hx
      induction x using MvPolynomial.induction_on with
      | C a =>
        simp only [algHom_C, TensorProduct.algebraMap_apply,
          algebraMap_self, RingHom.id_apply, e]
        rw [← MvPolynomial.algebraMap_eq, AlgEquiv.commutes]
        simp only [TensorProduct.algebraMap_apply, algebraMap_self, RingHom.id_apply,
          TensorProduct.map_tmul, AlgHom.coe_id, id_eq, map_one]
      | add p q hp hq => simp only [map_add, hp, hq]
      | mul_X p i hp => simp [hp, e]
    rw [H] at H'
    replace H' : e.symm x ∈ Ideal.map TensorProduct.includeRight P.ker := H'
    rw [← P.span_range_relation_eq_ker, ← Ideal.mem_comap, ← Ideal.comap_coe,
      ← AlgEquiv.toRingEquiv_toRingHom, Ideal.comap_coe, AlgEquiv.symm_toRingEquiv,
      Ideal.comap_symm, ← Ideal.map_coe, ← Ideal.map_coe _ (Ideal.span _), Ideal.map_map,
      Ideal.map_span, ← Set.range_comp, AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp,
      RingHom.coe_coe] at H'
    convert! H'
    simp [e]

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
P : Generators R S ι
r : R
inst✝ : IsLocalization.Away r S
s : S
⊢ (algebraMap R S) (IsLocalization.Away.sec r s).1 *
      (aeval fun x ↦ IsLocalization.Away.invSelf r) (X () ^ (IsLocalization.Away.sec r s).2) =
    s

Tactic:
map_pow,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Generators R S ι
r : R
inst✝ : IsLocalization.Away r S
s : S
⊢ (algebraMap R S) (IsLocalization.Away.sec r s).1 *
      (aeval fun x ↦ IsLocalization.Away.invSelf r) (X ()) ^ (IsLocalization.Away.sec r s).2 =
    s
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
t : (i : ι) → (relations i).Solution N
x✝ : (directSum relations).R
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun x ↦
        match x with
        | ⟨i, g⟩ => (t i).var g)
      ((directSum relations).relation ⟨i, r⟩) =
    0

Tactic:
by
        rw [← (t i).linearCombination_var_relation r]
        apply Finsupp.linearCombination_embDomain

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
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Generators R' S' ι'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ f.toAlgHom ((monomial v) r) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2

Tactic:
toAlgHom,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Generators R' S' ι'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : ι →₀ ℕ
r : R
⊢ (aeval f.val) ((monomial v) r) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2
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
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ RingHom.ker (aeval fun x ↦ ↑e (P.val x)) = P.ker

Tactic:
← MvPolynomial.comp_aeval,

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Generators R S ι
T : Type u_8
inst✝¹ : CommRing T
inst✝ : Algebra R T
e : S ≃ₐ[R] T
⊢ RingHom.ker ((↑e).comp (aeval P.val)) = P.ker
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ if v.1 = i then
    (∑ x ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with x.1 = i,
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      (aeval P.val) ((monomial v.2) a)
  else
    (∑ x ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with x.1 = i,
        if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
      0

Tactic:
← apply_ite,

Goal state after:
case a.convert_4.monomial
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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
a : R
v : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ (∑ x ∈ Finset.map (↑e).toEmbedding ((monomial (e.symm v)) a).support with x.1 = i,
      if v = x then (aeval P.val) ((monomial x.2) a) else 0) =
    if v.1 = i then (aeval P.val) ((monomial v.2) a) else 0
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst✝ : Fintype κ
e : κ ≃ ι
⊢ IsTrivialRelation (f ∘ ⇑e) (x ∘ ⇑e) ↔ IsTrivialRelation f x

Tactic:
isTrivialRelation_iff_vanishesTrivially,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
f : ι → R
x : ι → M
κ : Type u_4
inst✝ : Fintype κ
e : κ ≃ ι
⊢ VanishesTrivially R (f ∘ ⇑e) (x ∘ ⇑e) ↔ VanishesTrivially R f x
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ support R M ⊆ support R N

Tactic:
Set.subset_def,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ ∀ x ∈ support R M, x ∈ support R N