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 : ↥p
⊢ Function.Bijective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

Tactic:
constructor

Goal state after:
case left
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 : ↥p
⊢ Function.Injective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)

case right
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 : ↥p
⊢ Function.Surjective ⇑((algebraMap R (Module.End R ↥(localized₀ p f M'))) ↑x)
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:
ext

Goal state after:
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)
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
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I ↔ (algebraMap R S) x ∈ I

Tactic:
constructor

Goal state after:
case mp
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
x : R
y : ↥M
I : Ideal S
⊢ mk' S x y ∈ I → (algebraMap R S) x ∈ I

case mpr
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
x : R
y : ↥M
I : Ideal S
⊢ (algebraMap R S) x ∈ I → mk' S x y ∈ I
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
z : S
⊢ (∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z) ↔
    ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

Tactic:
constructor

Goal state after:
case mp
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
z : S
⊢ (∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z) →
    ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1

case mpr
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
z : S
⊢ (∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) ↑x.1) →
    ∃ m ∈ I, ∃ s, IsLocalizedModule.mk' (Algebra.linearMap R S) m s = z
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
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ((IsLocalizedModule.map p f f') g).ker = Submodule.restrictScalars R (localized' S p f g.ker)

Tactic:
ext

Goal state after:
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
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x✝ : N
⊢ x✝ ∈ ((IsLocalizedModule.map p f f') g).ker ↔ x✝ ∈ Submodule.restrictScalars R (localized' S p f g.ker)
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
⊢ ((IsLocalizedModule.map p f f') g).range = localized₀ p f' g.range

Tactic:
ext

Goal state after:
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
x✝ : Q
⊢ x✝ ∈ ((IsLocalizedModule.map p f f') g).range ↔ x✝ ∈ localized₀ p f' g.range
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
J₁ J₂ : Ideal S
⊢ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂ ↔ J₁ ≤ J₂

Tactic:
constructor

Goal state after:
case mp
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
J₁ J₂ : Ideal S
⊢ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂ → J₁ ≤ J₂

case mpr
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
J₁ J₂ : Ideal S
⊢ J₁ ≤ J₂ → { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₁ ≤ { toFun := fun J ↦ Ideal.under R J, inj' := ⋯ } J₂
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
J : Ideal S
⊢ J.IsPrime ↔ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

Tactic:
constructor

Goal state after:
case mp
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
J : Ideal S
⊢ J.IsPrime → (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J)

case mpr
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
J : Ideal S
⊢ (Ideal.under R J).IsPrime ∧ Disjoint ↑M ↑(Ideal.under R J) → J.IsPrime
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 : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ x = y

Tactic:
suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : 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)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
⊢ eqIdeal R x y = ⊤
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
J : Ideal S
⊢ J = ⊤ ↔ ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)

Tactic:
constructor

Goal state after:
case mp
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
J : Ideal S
⊢ J = ⊤ → ∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)

case mpr
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
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤
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 I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' ↔
    I ≤ I'

Tactic:
constructor

Goal state after:
case mp
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 I' : { p // p.IsPrime }
⊢ { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I' →
    I ≤ I'

case mpr
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 I' : { p // p.IsPrime }
⊢ I ≤ I' →
    { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I ≤
      { toFun := fun p ↦ ⟨Ideal.under R ↑p, ⋯⟩, invFun := fun p ↦ ⟨Ideal.map (algebraMap R S) ↑p, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        I'
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
x✝¹ : R[X]
x✝ : A[X]
⊢ (mapRingHom (algebraMap R A)) x✝¹ * x✝ = x✝ * (mapRingHom (algebraMap R A)) x✝¹

Tactic:
ext

Goal state after:
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
x✝¹ : R[X]
x✝ : A[X]
n✝ : ℕ
⊢ ((mapRingHom (algebraMap R A)) x✝¹ * x✝).coeff n✝ = (x✝ * (mapRingHom (algebraMap R A)) x✝¹).coeff n✝
Module: Mathlib.RingTheory.Localization.Algebra

Goal state before:
pp: R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (toKerIsLocalization S Q g ⋯)

Tactic:
convert_to! IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
    Algebra.idealMap S (RingHom.ker g))

Goal state after:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : CommSemiring P
inst✝⁴ : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst✝³ : Algebra R S
inst✝² : Algebra P Q
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯
⊢ IsLocalizedModule M (↑(LinearEquiv.restrictScalars R e) ∘ₗ Algebra.idealMap S (ker g))
Module: Mathlib.RingTheory.Flat.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
⊢ lTensor S N.subtype = (Submodule.localized₀ p ((TensorProduct.mk R S P) 1) N.subtype.range).subtype ∘ₗ ↑e

Tactic:
ext

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝³ : AddCommMonoid P
x✝² : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) N.subtype.range)
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) N.subtype.range) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
x✝¹ : S
x✝ : ↥N
⊢ ((AlgebraTensorModule.curry (lTensor S N.subtype)) x✝¹) x✝ =
    ((AlgebraTensorModule.curry ((Submodule.localized₀ p ((TensorProduct.mk R S P) 1) N.subtype.range).subtype ∘ₗ ↑e))
        x✝¹)
      x✝
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

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
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) ↔
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x) →
    ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z

case mpr
R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
N : Submonoid S
x : R
⊢ (∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z) →
    ∃ y ∈ N, ∃ z ∈ Submonoid.map (algebraMap R S) M, y * z = (algebraMap R S) x
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) ∘ₗ
      Algebra.linearMap R Rₚ =
    ↑R (Algebra.linearMap Rₚ Sₚ) ∘ₗ Algebra.linearMap R Rₚ

Tactic:
ext

Goal state after:
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) ∘ₗ
        Algebra.linearMap R Rₚ)
      1 =
    (↑R (Algebra.linearMap Rₚ Sₚ) ∘ₗ Algebra.linearMap R Rₚ) 1
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:
constructor

Goal state after:
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
⊢ ⊤.FG
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:
constructor

Goal state after:
case mp
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 ↑σ

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ : Finset S
⊢ (∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ) →
    IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr
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 ↑σ
⊢ IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
constructor

Goal state after:
case mpr
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 ↑σ
⊢ (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)).IsLocalizationMap
    ⇑(algebraMap (↥(adjoin R ↑σ)) S)
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case mpr
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 ↑σ
⊢ (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)).IsLocalizationMap
    ⇑(algebraMap (↥(adjoin R ↑σ)) S)

Tactic:
constructor

Goal state after:
case mpr.map_units
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 ↑σ
⊢ ∀ (y : ↥(Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S))),
    IsUnit ((algebraMap (↥(adjoin R ↑σ)) S) ↑y)

case surj
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 ↑σ
⊢ ∀ (z : S), ∃ x, z * (algebraMap (↥(adjoin R ↑σ)) S) ↑x.2 = (algebraMap (↥(adjoin R ↑σ)) S) x.1

case mpr.exists_of_eq
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 ↑σ)}, (algebraMap (↥(adjoin R ↑σ)) S) x = (algebraMap (↥(adjoin R ↑σ)) S) y → ∃ c, ↑c * x = ↑c * y
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 ↔ ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ EssFiniteType R S → ∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S

case mpr
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∃ σ, IsLocalization (Submonoid.comap (algebraMap (↥(adjoin R ↑σ)) S) (IsUnit.submonoid S)) S) → EssFiniteType R S
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
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
⊢ {p | p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p} = {p | p.IsPrime ∧ p ≤ I}

Tactic:
ext

Goal state after:
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
A : Type u_4
inst✝² : CommRing A
inst✝¹ : IsDomain A
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x✝ : Ideal R
⊢ x✝ ∈ {p | p.IsPrime ∧ Disjoint ↑I.primeCompl ↑p} ↔ x✝ ∈ {p | p.IsPrime ∧ p ≤ I}
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:
ext

Goal state after:
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✝