mathlib-initiative/mathlib-tactics huggingface dataset:
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 : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * (1 / I) = 1

Tactic:
← eq_one_div_of_mul_eq_one_right I J hJ

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 : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * J = 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
⊢ (↑I * (↑I)⁻¹)⁻¹ ≤ 1

Tactic:
intro x hx

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 ∈ 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: 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 : ∀ y ∈ ↑I * (↑I)⁻¹, x * y ∈ 1
b : K
hb : b ∈ (↑I)⁻¹
⊢ ∀ y ∈ ↑I, x * (y * b) ∈ 1

Tactic:
exact fun y hy ↦ hx _ (mul_mem_mul hy hb)

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

Goal state before:
pp: case refine_2
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)
⊢ IsInteger R₁ (↑a' • 0)

Tactic:
rw [smul_zero]

Goal state after:
case refine_2
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)
⊢ IsInteger R₁ 0
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

Goal state after:
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)
c : R₁
x : K
hx✝ : x ∈ span R₁ (f '' ↑s)
hx : IsInteger R₁ (↑a' • x)
⊢ IsInteger R₁ (↑a' • c • x)
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
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
⊢ (↑M)⁻¹ * ↑P ≤ ↑P

Tactic:
intro x hx

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
P : Ideal A
P_ne : P ≠ ⊥
hP : P.IsPrime
M : Ideal A
hM : P < M
P'_ne : ↑P ≠ 0
M'_ne : ↑M ≠ 0
x : FractionRing A
hx : x ∈ (↑M)⁻¹ * ↑P
⊢ x ∈ ↑P
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case neg.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 ≤ 1 / spanSingleton R₁⁰ d * J

Tactic:
intro x hx

Goal state after:
case neg.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
x : K
hx : x ∈ J / spanSingleton R₁⁰ d
⊢ x ∈ 1 / spanSingleton R₁⁰ d * J
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ map (algebraMap R A) p ≤ P)

Tactic:
map_le_iff_le_comap

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : IsDedekindDomain A
p : Ideal R
h : p.IsMaximal
inst✝² : Algebra R A
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
hp : p ≠ ⊥
P : Ideal A
⊢ P.IsPrime → (p = comap (algebraMap R A) P ↔ p ≤ comap (algebraMap R A) P)
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
⊢ ∀ a ∈ I, IsInteger S (f r • ↑(semilinearEquivOfRingEquiv K L f) a)

Tactic:
intro x hx

Goal state after:
case h
R : Type u_5
S : Type u_6
K : Type u_7
L : Type u_8
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra R K
inst✝² : Algebra S L
inst✝¹ : IsFractionRing R K
inst✝ : IsFractionRing S L
f : R ≃+* S
I : Submodule R K
r : R
hr0 : ¬r = 0
hr : ∀ b ∈ I, IsInteger R (r • b)
x : K
hx : x ∈ I
⊢ IsInteger S (f r • ↑(semilinearEquivOfRingEquiv K L f) x)
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
⊢ (smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ιB), M i)

Tactic:
apply DirectSum.addHom_ext

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
⊢ ∀ (i : ιB) (y : M i), ((smulAddMonoidHom A M) 1) ((of M i) y) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) y)
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
V : Type u_3
inst✝⁴ : AddCommGroup V
inst✝³ : Module R V
inst✝² : Module A V
inst✝¹ : IsScalarTower R A V
M : Submodule R V
inst✝ : IsLattice A M
⊢ Module.Finite R ↥M

Tactic:
rw [Module.Finite.iff_fg]
  exact IsLattice.fg

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

Goal state before:
pp: case map_smul
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ ∀ (c : R) (x : M × M), (c • x).1 + (c • x).2 = c • (x.1 + x.2)

Tactic:
simp [smul_add]

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

Goal state before:
pp: R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
⊢ FinitePresentation R M

Tactic:
have := Module.Finite.of_surjective g hg

Goal state after:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : Type u_1
inst✝² : AddCommGroup P
inst✝¹ : Module R P
inst✝ : FinitePresentation R N
f : M →ₗ[R] N
g : N →ₗ[R] P
l : P →ₗ[R] N
hl : g ∘ₗ l = LinearMap.id
hf : Function.Injective ⇑f
H : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
this : Module.Finite R P
⊢ FinitePresentation R M
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
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : ↥(factors ⊤.annihilator).toFinset
⊢ torsionBySet R M ↑(Ideal.span {IsPrincipal.generator ↑x✝} ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))

Tactic:
Ideal.span_singleton_generator

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
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : ↥(factors ⊤.annihilator).toFinset
⊢ torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
⊢ ↑σ ⊆ ↑(σ.prod s • g₁ - σ.prod s • g₂).ker

Tactic:
intro x hx

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g₁ g₂ : M →ₗ[R] N
h : f ∘ₗ g₁ = f ∘ₗ g₂
s : M → ↥S
hs : ∀ (x : M), s x • g₁ x = s x • g₂ x
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
x : M
hx : x ∈ ↑σ
⊢ x ∈ ↑(σ.prod s • g₁ - σ.prod s • g₂).ker
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ (R ∙ s j).subtype.range = (↑f ∘ₗ (R ∙ s j).mkQ).ker

Tactic:
range_subtype,

Goal state after:
case h.succ.refine_3.refine_2.refine_1
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
⊢ R ∙ s j = (↑f ∘ₗ (R ∙ s j).mkQ).ker
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
x : M
⊢ ((map S f g) l' ∘ₗ f) x = (((s • LinearMap.id) ∘ₗ ↑l) ∘ₗ f) x

Tactic:
simp only [LinearMap.coe_comp, Function.comp_apply, IsLocalizedModule.map_apply]

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
x : M
⊢ g (l' x) = (s • LinearMap.id) (↑l (f x))
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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R M) ≃ₗ[R] ⨁ (i : I), R ⧸ R ∙ p i ^ e i
n : ℕ
g : (M ⧸ torsion R M) ≃ₗ[R] Fin n →₀ R
f : M ⧸ torsion R M →ₗ[R] M
hf : (torsion R M).mkQ ∘ₗ f = LinearMap.id
⊢ (torsion R M).subtype.range = (torsion R M).mkQ.ker

Tactic:
range_subtype,

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
h' : Module.Finite R M
I : Type u
fI : Fintype I
p : I → R
hp : ∀ (i : I), Irreducible (p i)
e : I → ℕ
h : ↥(torsion R M) ≃ₗ[R] ⨁ (i : I), R ⧸ R ∙ p i ^ e i
n : ℕ
g : (M ⧸ torsion R M) ≃ₗ[R] Fin n →₀ R
f : M ⧸ torsion R M →ₗ[R] M
hf : (torsion R M).mkQ ∘ₗ f = LinearMap.id
⊢ torsion R M = (torsion R M).mkQ.ker
Module: Mathlib.RingTheory.Extension.Presentation.Basic

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

Tactic:
intro x hx

Goal state after:
case a
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 : x ∈ RingHom.ker (aeval (Generators.baseChange T P.toGenerators).val)
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
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
H' : x ∈ Ideal.map (↑e.toRingEquiv) (Ideal.map TensorProduct.includeRight (Ideal.span (Set.range P.relation)))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
← Ideal.map_coe _ (Ideal.span _),

Goal state after:
case a
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
H' : x ∈ Ideal.map (↑e.toRingEquiv) (Ideal.map (↑TensorProduct.includeRight) (Ideal.span (Set.range P.relation)))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ LieSubmodule.restr J H = LieSubmodule.restr I H

Tactic:
rw [J.restr_eq_iSup_sl2SubmoduleOfRoot, I.restr_eq_iSup_sl2SubmoduleOfRoot]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
⊢ ⨆ α ∈ J.rootSet, sl2SubmoduleOfRoot ⋯ = ⨆ α ∈ I.rootSet, sl2SubmoduleOfRoot ⋯
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]

Goal state after:
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 ι σ
⊢ Ideal.comap (↑(sumAlgEquiv R ι' ι)) (Ideal.map C (RingHom.ker (aeval P.val))) =
    Ideal.map (rename Sum.inr) (RingHom.ker (aeval P.val))
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
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf : Function.Bijective ⇑(rename ⇑e.symm)
⊢ Ideal.comap (rename ⇑e.symm) (Ideal.map (rename ⇑e.symm) (Ideal.span (Set.range P.relation))) =
    Ideal.comap (rename ⇑e.symm) (Ideal.comap (rename ⇑e) (Ideal.span (Set.range P.relation)))

Tactic:
Ideal.comap_comapₐ,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P✝ P : Presentation R S ι σ
ι' : Type u_1
σ' : Type u_2
e : ι' ≃ ι
f : σ' ≃ σ
hf : Function.Bijective ⇑(rename ⇑e.symm)
⊢ Ideal.comap (rename ⇑e.symm) (Ideal.map (rename ⇑e.symm) (Ideal.span (Set.range P.relation))) =
    Ideal.comap ((rename ⇑e).comp (rename ⇑e.symm)) (Ideal.span (Set.range P.relation))
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 ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
x : MvPolynomial σ R ⧸ I
⊢ (aeval fun i ↦ (Ideal.Quotient.mk I) (X i)) (s x) = x

Tactic:
conv_rhs => rw [← hs x, ← Ideal.Quotient.mkₐ_eq_mk R, aeval_unique (Ideal.Quotient.mkₐ _ I)]
    simp [Function.comp_def]

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
⊢ (aeval f.val) ((monomial v) r) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2

Tactic:
aeval_monomial,

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
⊢ ((algebraMap R P'.Ring) r * v.prod fun i k ↦ f.val i ^ k) = r • v.prod fun x1 x2 ↦ f.val x1 ^ x2
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case 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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
this : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
simp only [Ideal.mem_comap,
      RingHom.mem_ker, ← AlgHom.comp_apply, this, IsScalarTower.toAlgHom_apply]

Goal state after:
case 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 ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
this : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R P.Ring Q.Ring
⊢ (algebraMap P.Ring Q.Ring) x = 0