mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : M
hx : x ∈ M'
s : ↥p
⊢ ↑((⟨x, hx⟩, s).2 • ⟨IsLocalizedModule.mk' f x s, ⋯⟩) = ↑((toLocalized₀ p f M') (⟨x, hx⟩, s).1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
P Q : Submodule R M
x : ↥p
h : x • P ≤ Q
a : M
ha : a ∈ P
r : ↥p
⊢ IsLocalizedModule.mk' f (x • a) (x * r) = IsLocalizedModule.mk' f a r

Tactic:
simp

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

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ M'
⊢ IsLocalizedModule.mk' f x 1 = f x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
x : R
s✝ : ↥M
x✝ : ∃ s ∈ M, s * x ∈ I
s : R
hs : s ∈ M
h : s * x ∈ I
⊢ ↑(1 * (⟨s * x, h⟩, ⟨s, hs⟩).2) * x = ↑1 * ↑(⟨s * x, h⟩, ⟨s, hs⟩).1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsUnit ((mk (map (mk (I ^ n)) I)) ((mk (I ^ n)) x)) ↔ IsUnit ((mk I) x)

pp: case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)

Tactic:
· rw [← isUnit_map_iff (DoubleQuot.quotQuotEquivQuotOfLE (Ideal.pow_le_self hn))]
    rfl

Goal state after:
case hI
S : Type u_1
inst✝ : CommRing S
I : Ideal S
x : S
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (map (mk (I ^ n)) I)
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝⁵ : IsLocalizedModule p f
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
a : M
b c : ↥p
hc : c • g a = 0
⊢ mk' f (c • a) (c * b) = Function.uncurry (mk' f) (a, b)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
N₁ N₂ : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], localized₀ P.primeCompl (f P) N₁ ≤ localized₀ P.primeCompl (f P) N₂
m : M
hm : m ∈ N₁
P : Ideal R
hP : P.IsMaximal
⊢ IsLocalizedModule.mk' (f P) m 1 = (f P) m

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
N P : Submodule R M
h : ∀ (r : ↑s), localized₀ (Submonoid.powers ↑r) (f r) N ≤ localized₀ (Submonoid.powers ↑r) (f r) P
m : M
hm : m ∈ N
r : ↑s
⊢ mk' (f r) m 1 = (f r) m

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 1) = (monomial n) a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2.hf
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (monomial n) (a * (algebraMap R A) 0) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A✝ : Type u_3
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A✝
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R S
inst✝³ : Algebra S A✝
inst✝² : IsScalarTower R S A✝
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
a : A
⊢ (polyEquivTensor R A).toFun ((algebraMap A A[X]) a) = (algebraMap A (A ⊗[R] R[X])) a

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
x : A
⊢ (IsScalarTower.toAlgHom R B Bₚ).toLinearMap (f.toLinearMap x) =
    (↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap ∘ₗ (IsScalarTower.toAlgHom R A Aₚ).toLinearMap) x

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_5
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_6
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x✝ : R[X]
⊢ ↑(polyEquivTensor' R A).symm (1 ⊗ₜ[R] x✝) = (IsScalarTower.toAlgHom R R[X] A[X]).toLinearMap x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
⊢ RingHom.ker (Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) ≤
    Ideal.map (algebraMap R S) (RingHom.ker (Ideal.Quotient.mk I))

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₁ * ↑s₂)) = ↑a * (y₁ * ↑s₂)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case e'_3
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
x₁ x₂ : S
y₁ : R
s₁ : ↥M
e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁
y₂ : R
s₂ : ↥M
e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂
a : ↥N
e : ↑a * (y₁ * ↑s₂) = ↑a * (y₂ * ↑s₁)
⊢ ↑1 * (↑a * (y₂ * ↑s₁)) = ↑a * (y₂ * ↑s₁)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
⊢ ∃ m, m * ↑⟨x, ⋯⟩ ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)

Tactic:
obtain ⟨⟨y, s⟩, e⟩ := IsLocalization.surj M x

Goal state after:
case refine_2
R : Type u_1
inst✝⁸ : CommRing R
M : Submonoid R
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsFractionRing R T
hM : M ≤ nonZeroDivisors R
this : IsLocalization (Submonoid.map (algebraMap R S) (nonZeroDivisors R)) T
x : S
left✝ : x ∈ ↑(nonZeroDivisorsLeft S)
hx : x ∈ ↑(nonZeroDivisorsRight S)
y : R
s : ↥M
e : x * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1
⊢ ∃ m, m * ↑⟨x, ⋯⟩ ∈ Submonoid.map (algebraMap R S) (nonZeroDivisors R)
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ 1 = (Algebra.linearMap R Rₚ) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring S
inst✝¹¹ : Algebra R S
Rₚ : Type u_5
Sₚ : Type u_6
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : CommSemiring Sₚ
inst✝⁷ : Algebra S Sₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : IsScalarTower R S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R Rₚ Sₚ
p : Ideal R
inst✝² : p.IsPrime
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S Sₚ)
⊢ ↑(IsScalarTower.toAlgHom R S Sₚ) ((Algebra.linearMap R S) 1) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Injective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S)) =
    ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
rw [DFunLike.coe_fn_eq]
    apply IsLocalizedModule.map_linearMap_of_isLocalization

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
Rₚ : (p : Ideal R) → [p.IsMaximal] → Type u_3
inst✝⁹ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Rₚ p)
inst✝⁸ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Rₚ p)
Sₚ : (p : Ideal R) → [p.IsMaximal] → Type u_4
inst✝⁷ : (p : Ideal R) → [inst : p.IsMaximal] → CommSemiring (Sₚ p)
inst✝⁶ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra S (Sₚ p)
inst✝⁵ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra (Rₚ p) (Sₚ p)
inst✝⁴ : (p : Ideal R) → [inst : p.IsMaximal] → Algebra R (Sₚ p)
inst✝³ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R (Rₚ p) (Sₚ p)
inst✝² : ∀ (p : Ideal R) [inst : p.IsMaximal], IsScalarTower R S (Sₚ p)
inst✝¹ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalization.AtPrime (Rₚ p) p
inst✝ : ∀ (p : Ideal R) [inst : p.IsMaximal], IsLocalizedModule.AtPrime p ↑(IsScalarTower.toAlgHom R S (Sₚ p))
H : ∀ (p : Ideal R) [inst : p.IsMaximal], Function.Surjective ⇑(algebraMap (Rₚ p) (Sₚ p))
p : Ideal R
hp : p.IsMaximal
⊢ ⇑((IsLocalizedModule.map p.primeCompl (Algebra.linearMap R (Rₚ p)) ↑(IsScalarTower.toAlgHom R S (Sₚ p)))
        (Algebra.linearMap R S)) =
    ⇑(↑R (Algebra.linearMap (Rₚ p) (Sₚ p)))

Tactic:
rw [DFunLike.coe_fn_eq]
    apply IsLocalizedModule.map_linearMap_of_isLocalization

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x : M
hx : x ∈ m
⊢ x ∈
    (n.liftQ ((mk R M N).flip.compr₂ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ)
          ⋯).flip.ker

Tactic:
by
      ext y
      simp only [LinearMap.coe_comp, Function.comp_apply, Submodule.mkQ_apply, LinearMap.flip_apply,
        Submodule.liftQ_apply, LinearMap.compr₂_apply, mk_apply, LinearMap.zero_comp,
        LinearMap.zero_apply, Submodule.Quotient.mk_eq_zero]
      exact Submodule.mem_sup_left ⟨⟨x, hx⟩ ⊗ₜ y, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
          ((lift
                (m.liftQ
                  (n.liftQ
                      ((mk R M N).flip.compr₂
                        ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ)
                      ⋯).flip
                  ⋯) ∘ₗ
              ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).liftQ (map m.mkQ n.mkQ) ⋯) ∘ₗ
            ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ))
        x✝¹)
      x✝ =
    ((AlgebraTensorModule.curry
          (LinearMap.id ∘ₗ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ))
        x✝¹)
      x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
m : Submodule R M
n : Submodule R N
x✝¹ : M
x✝ : N
⊢ ((AlgebraTensorModule.curry
              (((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).liftQ (map m.mkQ n.mkQ) ⋯ ∘ₗ
                lift
                  (m.liftQ
                    (n.liftQ
                        ((mk R M N).flip.compr₂
                          ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ)
                        ⋯).flip
                    ⋯)) ∘ₗ
            m.mkQ)
          x✝¹ ∘ₗ
        n.mkQ)
      x✝ =
    ((AlgebraTensorModule.curry LinearMap.id ∘ₗ m.mkQ) x✝¹ ∘ₗ n.mkQ) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
I : Ideal R
x✝¹ : ↥I
x✝ : ↥⊤
⊢ ((↑(TensorProduct.lid R M) ∘ₗ map (Submodule.subtype I) LinearMap.id) ∘ₗ
        ↑(LinearEquiv.lTensor (↥I) Submodule.topEquiv))
      (x✝¹ ⊗ₜ[R] x✝) =
    (lift (LinearMap.lsmul R M) ∘ₗ mapIncl I ⊤) (x✝¹ ⊗ₜ[R] x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
x : M
⊢ Submodule.Quotient.mk (1 • x) = Submodule.Quotient.mk x

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
S : Type u_4
inst✝¹ : CommRing S
inst✝ : Algebra R S
I : Ideal R
⊢ I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P✝ : Type u_3
inst✝¹ : CommSemiring P✝
I : Ideal R
hI : I.IsPrime
P : Ideal S
inst✝ : P.IsPrime
s : Subalgebra R S
⊢ P.primeCompl ⊓ s.toSubmonoid ≤ s.toSubmonoid

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • 0) =
    (RingHom.id A) m • (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) 0

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case tmul
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M
y : N ⧸ n
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • x ⊗ₜ[R] y) =
    (RingHom.id A) m • (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (x ⊗ₜ[R] y)

Tactic:
obtain ⟨y, rfl⟩ := Submodule.Quotient.mk_surjective _ y

Goal state after:
case tmul
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x : M
y : N
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • x ⊗ₜ[R] Submodule.Quotient.mk y) =
    (RingHom.id A) m •
      (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (x ⊗ₜ[R] Submodule.Quotient.mk y)
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ : A
x✝ : M
⊢ { toFun := fun n ↦ S.mkQ ((x✝¹ • x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    (RingHom.id A) x✝¹ • { toFun := fun n ↦ S.mkQ (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }

Tactic:
simp

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
x✝¹ : A
x✝ : M
⊢ { toFun := fun n ↦ Submodule.Quotient.mk ((x✝¹ • x✝) ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ } =
    x✝¹ • { toFun := fun n ↦ Submodule.Quotient.mk (x✝ ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_4
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : IsLocalization M S
inst✝ : (under R ⊤).IsMaximal
⊢ under R ⊤ = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
p : Ideal R
inst✝⁵ : p.IsPrime
Rₚ : Type u_4
inst✝⁴ : CommSemiring Rₚ
inst✝³ : Algebra R Rₚ
inst✝² : IsLocalization.AtPrime Rₚ p
inst✝¹ : IsLocalRing Rₚ
inst✝ : p.IsMaximal
n : ℕ
x✝ : R
h : x✝ ∈ p ^ n
⊢ 1 ∈ p.primeCompl

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ 0 * 1 ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
u v : B
⊢ (u * v) ⊗ₜ[A] 1 = u ⊗ₜ[A] 1 * v ⊗ₜ[A] 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x : A
⊢ (TensorProduct.comm A B (A ⧸ I)) (1 ⊗ₜ[A] (algebraMap A (A ⧸ I)) x) = (algebraMap A ((A ⧸ I) ⊗[A] B)) x

Tactic:
simp

Goal state after: