mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
s : Set R
spn : 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ₚ : ↑s → Type u_6
inst✝² : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝¹ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
F : M →ₗ[R] N
H : ∀ (r : ↑s), Function.Injective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
x y : M
eq : F x = F y
P : ↑s
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑P) (f P) (g P)) F) ((f P) x) =
    ((IsLocalizedModule.map (Submonoid.powers ↑P) (f P) (g P)) F) ((f P) y)

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsFractionRing S T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
this✝ : Nontrivial T
this : Nontrivial S
x : R
hx : x ∈ M
hx' : x = 0
⊢ ↑⟨x, hx⟩ * 1 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
M : Submonoid R
inst✝⁸ : IsDomain 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
⊢ IsFractionRing S T

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
L : Type u_4
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid L
inst✝⁹ : Module R L
s : Set R
spn : 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ₚ : ↑s → Type u_6
inst✝⁵ : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝⁴ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)
Lₚ : ↑s → Type u_7
inst✝² : (r : ↑s) → AddCommMonoid (Lₚ r)
inst✝¹ : (r : ↑s) → Module R (Lₚ r)
h : (r : ↑s) → L →ₗ[R] Lₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)
F : M →ₗ[R] N
G : N →ₗ[R] L
H :
  ∀ (r : ↑s),
    Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
      ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)
⊢ Function.Exact ⇑F ⇑G

Tactic:
by

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ₚ)
⊢ (map p.primeCompl (Algebra.linearMap R Rₚ) ↑(IsScalarTower.toAlgHom R S Sₚ)) (Algebra.linearMap R S) =
    ↑R (Algebra.linearMap Rₚ Sₚ)

Tactic:
by

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))
⊢ Function.Injective ⇑(algebraMap R S)

Tactic:
by

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))
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
by

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
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝² : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
this✝ : ∀ (r : ↑s), IsLocalization.Away ((algebraMap R S) ↑r) (Sᵣ r)
this : (r : ↑s) → Algebra (Rᵣ r) (Sᵣ r) := fun r ↦ localizationAlgebra (Submonoid.powers ↑r) S
r : ↑s
⊢ ∀ (x : R), (algebraMap R (Sᵣ r)) x = (algebraMap (Rᵣ r) (Sᵣ r)) ((algebraMap R (Rᵣ r)) x)

Tactic:
by

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
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Injective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Injective ⇑f

Tactic:
by

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
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝² : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this✝¹ : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
this✝ : ∀ (r : ↑s), IsLocalization.Away ((algebraMap R S) ↑r) (Sᵣ r)
this : (r : ↑s) → Algebra (Rᵣ r) (Sᵣ r) := fun r ↦ localizationAlgebra (Submonoid.powers ↑r) S
r : ↑s
⊢ ∀ (x : R), (algebraMap R (Sᵣ r)) x = (algebraMap (Rᵣ r) (Sᵣ r)) ((algebraMap R (Rᵣ r)) x)

Tactic:
by

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
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
⊢ Function.Surjective ⇑f

Tactic:
by

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✝ : EssFiniteType R S
⊢ FiniteType R ↥(EssFiniteType.subalgebra R S)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : ↥(adjoin R ↑σ)
e : (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y
⊢ ↑1 * x = ↑1 * y

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔
    ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
by

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✝ : FiniteType R S
s : Finset S
hs : adjoin R ↑s = ⊤
x✝ : S
⊢ ∃ t ∈ adjoin R ↑s, IsUnit t ∧ x✝ * t ∈ adjoin R ↑s

Tactic:
by

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✝ : FiniteType R S
⊢ EssFiniteType R S

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ EssFiniteType R S

Tactic:
by

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 : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : (algebraMap R S) 0 = (algebraMap R S) 1
t : ↥P.primeCompl
ht : ↑t * 0 = ↑t * 1
⊢ ↑t = 0

Tactic:
by

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 : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
hze : 0 = 1
⊢ False

Tactic:
by

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 : N
hx : x ∈ n
⊢ x ∈ ((mk R M N).flip.compr₂ ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range).mkQ).ker

Tactic:
by

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

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 : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
⊢ ∀ (a b : S), a ∈ nonunits S → b ∈ nonunits S → a + b ∈ nonunits S

Tactic:
by

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
a : ↥m ⊗[R] N
b : M ⊗[R] ↥n
f : ↥m ⊗[R] N →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map m.subtype LinearMap.id
g : M ⊗[R] ↥n →ₗ[R] (M ⧸ m) ⊗[R] (N ⧸ n) := map m.mkQ n.mkQ ∘ₗ map LinearMap.id n.subtype
⊢ f.coprod g = 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
x✝ : ↥P.primeCompl
val✝ : R
h : val✝ ∈ P.primeCompl
⊢ ↑⟨val✝, h⟩ ≠ 0

Tactic:
by

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

Goal state before:
pp: S : Type u_2
inst✝⁴ : CommSemiring S
R : Type u_4
inst✝³ : CommRing R
inst✝² : NoZeroDivisors R
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
⊢ FaithfulSMul R S

Tactic:
by

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 ⊗[R] N
hx : x ∈ (map m.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range
⊢ x ∈ (map m.mkQ n.mkQ).ker

Tactic:
by

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
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
h : IsLocalRing S
⊢ (algebraMap R S) x ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
by

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
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
h : IsLocalRing S
x : R
⊢ x ∈ Ideal.under R (IsLocalRing.maximalIdeal S) ↔ x ∈ I

Tactic:
by

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
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
h : IsLocalRing S
⊢ mk' S x y ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)

Tactic:
by

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
⊢ 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) ⋯ =
    LinearMap.id

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
J : Ideal (Localization.AtPrime I)
h : Ideal.under R J = I
⊢ IsLocalRing.maximalIdeal (Localization.AtPrime I) ≤ J

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∈ Ideal.comap f J
⊢ x ∈ I

Tactic:
contrapose hx

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∉ I
⊢ x ∉ Ideal.comap f J
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
h : I.primeCompl ≤ Submonoid.comap f J.primeCompl
x : R
hx : x ∈ Ideal.comap f J
⊢ x ∈ I

Tactic:
by

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
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ f ↑y ∈ J.primeCompl

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : R
y : ↥I.primeCompl
⊢ (localRingHom I J f hIJ) (mk x y) = mk (f x) ⟨f ↑y, ⋯⟩

Tactic:
by

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
⊢ ((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
          ⋯) =
    LinearMap.id

Tactic:
by

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
⊢ Submodule.map (↑(LinearEquiv.refl R (M ⊗[R] N)))
      ((map m.subtype LinearMap.id).range ⊔ (map LinearMap.id ⊥.subtype).range) =
    (map m.subtype LinearMap.id).range

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
P : Type u_3
inst✝ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
hJ : J.IsPrime
f : R →+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
hx : IsUnit ((localRingHom I J f hIJ) x)
⊢ IsUnit x

Tactic:
by

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
n : Submodule R N
⊢ Submodule.map (↑(LinearEquiv.refl R (M ⊗[R] N)))
      ((map ⊥.subtype LinearMap.id).range ⊔ (map LinearMap.id n.subtype).range) =
    (map LinearMap.id n.subtype).range

Tactic:
by

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
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
⊢ I = Ideal.comap (g.comp f) K

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
S : Type u_4
inst✝ : CommSemiring S
J : Ideal S
hJ : J.IsPrime
K : Ideal P
hK : K.IsPrime
f : R →+* S
hIJ : I = Ideal.comap f J
g : S →+* P
hJK : J = Ideal.comap g K
r : R
⊢ ((localRingHom J K g hJK).comp (localRingHom I J f hIJ)) ((algebraMap R (Localization.AtPrime I)) r) =
    (algebraMap P (Localization.AtPrime K)) ((g.comp f) r)

Tactic:
by

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:
by

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
⊢ Submodule.map (↑(TensorProduct.lid R M)) (map (Submodule.subtype I) LinearMap.id).range = I • ⊤

Tactic:
by

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
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) I

Tactic:
by

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
⊢ (quotTensorEquivQuotSMul M I) (1 ⊗ₜ[R] x) = Submodule.Quotient.mk x

Tactic:
by

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
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
x : Localization.AtPrime I
⊢ (localRingHom J I ↑f.symm ⋯) ((↑↑(localRingHom I J (↑f) hIJ)).toFun x) = x

Tactic:
by

Goal state after: