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

Goal state before:
pp: case h.refine_3
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
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (algebraMap S T) t₁ * t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t

Tactic:
]

Goal state after:
case h.refine_3
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
s : Finset S
hs : ∀ (s_1 : S), ∃ t ∈ adjoin R ↑s, IsUnit t ∧ s_1 * t ∈ adjoin R ↑s
t : Finset T
ht : ∀ (s : T), ∃ t_1 ∈ adjoin S ↑t, IsUnit t_1 ∧ s * t_1 ∈ adjoin S ↑t
x y : T
hy₁ : y ∈ adjoin S ↑t
hy₂ : IsUnit y
hy₃ : x * y ∈ adjoin S ↑t
t₁ : S
h₁ : t₁ ∈ adjoin R ↑s
h₂ : IsUnit t₁
h₃ : t₁ • y ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
t₂ : S
h₄ : t₂ ∈ adjoin R ↑s
h₅ : IsUnit t₂
h₆ : t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
⊢ (algebraMap S T) t₁ * t₂ • (x * y) ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) (adjoin R ↑s) ⊔ adjoin R ↑t
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y = mk' S 1 z • y

Tactic:
]

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
h₁ : ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
h₂ : ∃ σ, ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ
⊢ ∃ σ, ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ

Tactic:
classical
  obtain ⟨s, hs⟩ := h₁
  obtain ⟨t, ht⟩ := h₂
  use s.image (IsScalarTower.toAlgHom R S T) ∪ t
  simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
  obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
  obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
  refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
  · rw [Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
  · rw [Algebra.smul_def, Algebra.smul_def]
    exact (h₅.map _).mul ((h₂.map _).mul hy₂)
  · rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆

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
h : ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∃ σ, ∀ (s : T ⊗[R] S), ∃ t ∈ adjoin T ↑σ, IsUnit t ∧ s * t ∈ adjoin T ↑σ

Tactic:
]

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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∃ σ, ∀ (s : T ⊗[R] S), ∃ t ∈ adjoin T ↑σ, IsUnit t ∧ s * t ∈ adjoin T ↑σ
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z' • y' = mk' S 1 z' • y'

Tactic:
]

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 ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
this : TensorProduct.includeRight x ∈ Subalgebra.map TensorProduct.includeRight (adjoin R ↑σ)
⊢ 1 ⊗ₜ[R] x ∈ adjoin T ↑(adjoin R ↑(Finset.image (⇑TensorProduct.includeRight) σ))

Tactic:
]

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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x✝ : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
x : S
hx : x ∈ adjoin R ↑σ
this : TensorProduct.includeRight x ∈ Subalgebra.map TensorProduct.includeRight (adjoin R ↑σ)
⊢ 1 ⊗ₜ[R] x ∈ adjoin T ↑(adjoin R ↑(Finset.image (⇑TensorProduct.includeRight) σ))
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:
]

Goal state after:
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
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: case mp.refine_4
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : R
z' : ↥M
⊢ mk' S (y' * 1) (z' * z) • y = mk' S (y' * 1) (z' * z) • y

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.tmul
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 ↑σ
x : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
H : ∀ x ∈ adjoin R ↑σ, 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x • 1 ⊗ₜ[R] (y * t) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
]

Goal state after:
case h.tmul
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 ↑σ
x : T
y t : S
h₁ : t ∈ adjoin R ↑σ
h₂ : IsUnit t
h₃ : y * t ∈ adjoin R ↑σ
H : ∀ x ∈ adjoin R ↑σ, 1 ⊗ₜ[R] x ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x • 1 ⊗ₜ[R] (y * t) ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) ((a₁ * a₂) ⊗ₜ[R] (Ideal.Quotient.mk I) (b₁ * b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] (Ideal.Quotient.mk I) b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] (Ideal.Quotient.mk I) b₂)

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) ((a₁ * a₂) ⊗ₜ[R] (Ideal.Quotient.mk I) (b₁ * b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] (Ideal.Quotient.mk I) b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] (Ideal.Quotient.mk I) b₂)
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: 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 : S
a : Set R
⊢ (∃ y ∈ coeSubmodule S (Ideal.span a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z

Tactic:
]

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 : S
a : Set R
⊢ (∃ y ∈ coeSubmodule S (Ideal.span a), ∃ z, x = mk' S 1 z • y) → ∃ y ∈ Ideal.span a, ∃ z, x = mk' S y z
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case h
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ 0 = 0

pp: case h
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0

Tactic:
]

Goal state after:
case h
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: 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 : S
a : Set R
y : R
hy : y ∈ ↑(Ideal.span a)
z : ↥M
hz : x = mk' S 1 z • (Algebra.linearMap R S) y
⊢ mk' S y z = mk' S y z

Tactic:
]

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

Goal state before:
pp: case h
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ ↑s ∉ p

Tactic:
]

Goal state after:
case h
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
s' : R
hs : (Ideal.Quotient.mk p) s' = ((Ideal.Quotient.mk p) ↑s)⁻¹
this : (algebraMap R Rₚ) ↑s ∉ maximalIdeal Rₚ
⊢ ↑s ∉ p
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ (LinearMap.rTensor M (Submodule.mkQ I)).ker = (LinearMap.rTensor M (Submodule.subtype I)).range

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
⊢ (LinearMap.rTensor M (Submodule.mkQ I)).ker = (LinearMap.rTensor M (Submodule.subtype I)).range
Module: Mathlib.RingTheory.Localization.Submodule

Goal state before:
pp: 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 : S
a : Set R
y : R
hy : y ∈ Ideal.span a
z : ↥M
hz : x = mk' S y z
⊢ mk' S y z = mk' S y z

Tactic:
]

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

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0

Tactic:
]

Goal state after:
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
⊢ (Ideal.Quotient.mk p) ↑s ≠ 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
x : R
s : ↥p.primeCompl
h₁ : (Ideal.Quotient.mk p) ↑s ≠ 0
h₂ : (equivQuotMaximalIdeal p Rₚ) ((Ideal.Quotient.mk p) ↑s) ≠ 0
⊢ (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x = (algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) x

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
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 ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * tx * ty + y * ty * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
]

Goal state after:
case h.add
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 ↑σ
x y tx : T ⊗[R] S
hx₁ : tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hx₂ : IsUnit tx
hx₃ : x * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
ty : T ⊗[R] S
hy₁ : ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy₂ : IsUnit ty
hy₃ : y * ty ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ x * tx * ty + y * ty * tx ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
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
h : ∃ σ, ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∃ σ, ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ

Tactic:
]

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✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h : ∃ σ, ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
⊢ ∃ σ, ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
x y : α
h' : k * x = k * y
⊢ k * y = k * y

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), x * k = 0 → x = 0
x y : α
h' : x * k = y * k
⊢ y * k = y * k

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
⊢ IsDedekindFiniteMonoid α ↔ ∀ (x y z : α), x * y = 1 → x * z = 1 → y = z

Tactic:
refine (isDedekindFiniteMonoid_iff _).trans ⟨fun h x y z hxy hxz ↦ ?_, fun h x y eq ↦ ?_⟩
  · simpa [← mul_assoc, h hxz] using congr_arg (z * ·) hxy
  have := h _ _ (1 - y * x + y) eq <| by
    rw [mul_add, mul_sub, ← mul_assoc, eq, mul_one, one_mul, sub_self, zero_add]
  rwa [right_eq_add, sub_eq_zero, eq_comm] at this

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.Regular

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : Ring α
h : ∀ (x y z : α), x * z = 1 → y * z = 1 → x = y
x y : α
eq : x * y = 1
this : y * x = 1
⊢ y * x = 1
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: case refine_1
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✝
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ₚ✝
Sₚ : Type u_5
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra S✝ Sₚ
inst✝⁷ : IsLocalization (algebraMapSubmonoid S✝ p✝.primeCompl) Sₚ
inst✝⁶ : Algebra Rₚ✝ Sₚ
P : Ideal S✝
S : Type u_6
R : Type u_7
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsMaximal
Rₚ : Type u_8
inst✝³ : CommRing Rₚ
inst✝² : Algebra R Rₚ
inst✝¹ : IsLocalization.AtPrime Rₚ p
inst✝ : IsLocalRing Rₚ
n : ℕ
⊢ p ^ n ≤ p ^ n

Tactic:
]

Goal state after: