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

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
⊢ ((∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y) ↔
    (∀ (y : ↥M), IsUnit ((algebraMap R S) ↑y)) ∧
      (∀ (z : S), ∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1) ∧
        ∀ {x y : R}, (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
]

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

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
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y

Tactic:
]

Goal state after:
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 : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

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
z : S
⊢ (algebraMap R S) (sec M z).1 = (algebraMap R S) (sec M z).1

Tactic:
]

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

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
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0

Tactic:
]

Goal state after:
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
z : S
x : R
y : ↥M
h : z * (algebraMap R S) ↑y = 0
hx : x = 0
⊢ z = 0
Module: Mathlib.RingTheory.Localization.Defs

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
z : R
h : z * ↑y = x
⊢ (algebraMap R S) z * (algebraMap R S) ↑y = (algebraMap R S) z * (algebraMap R S) ↑y

Tactic:
]

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

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  ∃ c,
    ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
      ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)

Tactic:
]

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (Pi.evalRingHom R i) S
r₁ : (i : ι) → R i
s₁ : ↥T
r₂ : (i : ι) → R i
s₂ : ↥T
eq :
  ∃ c,
    ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₂, ⋯⟩ * (Pi.evalRingHom R i) r₁) =
      ↑c * (↑⟨(Pi.evalRingHom R i) ↑s₁, ⋯⟩ * (Pi.evalRingHom R i) r₂)
⊢ ∃ c, ↑c * (↑s₂ * r₁) = ↑c * (↑s₁ * r₂)
Module: Mathlib.RingTheory.Localization.Defs

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
z₁ z₂ : S
⊢ mk' S x y * (algebraMap R S) ↑y + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y ↔
    mk' S x y * (algebraMap R S) ↑y + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

Tactic:
]

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

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 : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ 0 = 0

Tactic:
]

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

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 y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1

Tactic:
]

Goal state after:
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 y : ↥M
⊢ mk' S (↑y * ↑x) (y * x) = 1
Module: Mathlib.RingTheory.Localization.Defs

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 y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)

Tactic:
]

Goal state after:
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 y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
Module: Mathlib.RingTheory.Localization.Defs

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 y : R
m : ↥M
⊢ (algebraMap R S) x * mk' S y m = (algebraMap R S) x * mk' S y m

Tactic:
]

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

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
m : ↥M
⊢ mk' S x m = mk' S x m

Tactic:
]

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

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
m : ↥M
r : R
⊢ (algebraMap R S) r = (algebraMap R S) r

Tactic:
]

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

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
N₁ : Type u_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'

Tactic:
]

Goal state after:
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_4
N₂ : Type u_5
inst✝⁷ : AddCommMonoid N₁
inst✝⁶ : AddCommMonoid N₂
inst✝⁵ : Module R N₁
inst✝⁴ : Module R N₂
inst✝³ : Module S N₁
inst✝² : Module S N₂
inst✝¹ : IsScalarTower R S N₁
inst✝ : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
⊢ (algebraMap R S) ↑m • f (mk' S r m • s') = (algebraMap R S) ↑m • mk' S r m • f s'
Module: Mathlib.RingTheory.Localization.Basic

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
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
inst✝ : Algebra R P
f g : S →ₐ[R] P
⊢ algebraMap R P = algebraMap R P

Tactic:
]

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

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₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂

Tactic:
]

Goal state after:
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₁ x₂ : R
y₁ y₂ : ↥M
⊢ (algebraMap R S) (↑y₁ * ↑(y₁ * y₂) * x₂) + (algebraMap R S) (↑(y₁ * y₂) * x₁) * (algebraMap R S) ↑y₂ =
    (algebraMap R S) (x₁ * ↑y₂ + x₂ * ↑y₁) * (algebraMap R S) ↑y₁ * (algebraMap R S) ↑y₂
Module: Mathlib.RingTheory.Localization.Basic

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
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)

Tactic:
]

Goal state after:
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
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
f : S →+* Q
hf : f.comp (algebraMap R S) = algebraMap R Q
⊢ algebraMap R Q = (↑(algEquiv M S Q)).comp (algebraMap R S)
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).domRestrict M) y * z₁ = ((↑g).domRestrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
M : Submonoid R
P : Type u_3
inst✝ : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit (g ↑y)
y : ↥M
w z₁ z₂ : P
⊢ w + ((↑g).domRestrict M) y * z₁ = ((↑g).domRestrict M) y * z₂ ↔ w + g ↑y * z₁ = g ↑y * z₂
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x✝ : A
⊢ (algebraMap P Q) ((algebraMap A P) x✝) = (algebraMap P Q) ((algebraMap A P) x✝)

Tactic:
]

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

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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
z : S
w w' v : P
⊢ ↑g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v ↔
    g ((toLocalizationMap M S).sec z).1 * w + g ↑((toLocalizationMap M S).sec z).2 * w' =
      g ↑((toLocalizationMap M S).sec z).2 * v
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 *
        (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) +
      g ↑((toLocalizationMap M S).sec y).2 *
        (g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) =
    g ↑((toLocalizationMap M S).sec y).2 *
      (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
x y : S
⊢ g ((toLocalizationMap M S).sec y).1 *
        (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) +
      g ↑((toLocalizationMap M S).sec y).2 *
        (g ((toLocalizationMap M S).sec x).1 * ↑g.toMonoidWithZeroHom ↑((toLocalizationMap M S).sec (x + y)).2) =
    g ↑((toLocalizationMap M S).sec y).2 *
      (g ↑((toLocalizationMap M S).sec x).2 * ↑g.toMonoidWithZeroHom ((toLocalizationMap M S).sec (x + y)).1)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R✝ : Type u_1
inst✝¹⁹ : CommSemiring R✝
M✝ N : Submonoid R✝
S✝ : Type u_2
inst✝¹⁸ : CommSemiring S✝
inst✝¹⁷ : Algebra R✝ S✝
P✝ : Type u_3
inst✝¹⁶ : CommSemiring P✝
inst✝¹⁵ : IsLocalization M✝ S✝
g : R✝ →+* P✝
hg : ∀ (y : ↥M✝), IsUnit (g ↑y)
A : Type u_4
inst✝¹⁴ : CommSemiring A
R : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : Algebra A R
M : Submonoid R
S : Type u_6
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra A S
inst✝⁹ : Algebra R S
inst✝⁸ : IsScalarTower A R S
inst✝⁷ : IsLocalization M S
P : Type u_7
inst✝⁶ : CommSemiring P
inst✝⁵ : Algebra A P
T : Submonoid P
Q : Type u_8
inst✝⁴ : CommSemiring Q
inst✝³ : Algebra A Q
inst✝² : Algebra P Q
inst✝¹ : IsScalarTower A P Q
inst✝ : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ M = M

Tactic:
]

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

Goal state before:
pp: R : Type u_4
inst✝⁷ : CommSemiring R
S : Submonoid R
R' : Type u_5
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
inst✝⁴ : IsLocalization S R'
M' : Type u_6
inst✝³ : AddCommMonoid M'
inst✝² : Module R' M'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
⊢ ↑s • x ∈ N'

Tactic:
]

Goal state after:
R : Type u_4
inst✝⁷ : CommSemiring R
S : Submonoid R
R' : Type u_5
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
inst✝⁴ : IsLocalization S R'
M' : Type u_6
inst✝³ : AddCommMonoid M'
inst✝² : Module R' M'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
⊢ ↑s • x ∈ N'
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_4
inst✝ : Monoid P
j k : S → P
hj1 : j 1 = 1
hk1 : k 1 = 1
hjm : ∀ (a b : S), j (a * b) = j a * j b
hkm : ∀ (a b : S), k (a * b) = k a * k b
h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)
j' : S →* P := { toFun := j, map_one' := hj1, map_mul' := hjm }
k' : S →* P := { toFun := k, map_one' := hk1, map_mul' := hkm }
this : j' = k'
⊢ (↑k').toFun = (↑k').toFun

Tactic:
]

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

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
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x : ℤ
hx✝ : x ∈ ℤ⁰
hx : x ≠ 0
⊢ IsUnit ((algebraMap ℤ ℚ) ↑⟨x, hx✝⟩)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x : ℤ
hx✝ : x ∈ ℤ⁰
hx : x ≠ 0
⊢ IsUnit ((algebraMap ℤ ℚ) ↑⟨x, hx✝⟩)
Module: Mathlib.RingTheory.Localization.Defs

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
T : Type u_4
inst✝ : CommSemiring T
f : S →+* T
⊢ (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (f.comp (algebraMap R S)) x = (f.comp (algebraMap R S)) y) ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (lift ⋯) ((algebraMap R S) x) = (lift ⋯) ((algebraMap R S) y)

Tactic:
]

Goal state after:
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
T : Type u_4
inst✝ : CommSemiring T
f : S →+* T
⊢ (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (f.comp (algebraMap R S)) x = (f.comp (algebraMap R S)) y) ↔
    ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ (lift ⋯) ((algebraMap R S) x) = (lift ⋯) ((algebraMap R S) y)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : (Algebra.ofId R S) x = (Algebra.ofId R S) y
c : ↥M
u : Rˣ
eq : x = y
hu : ↑u = ↑c
⊢ x = y

Tactic:
]

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
x y : R
hxy : (Algebra.ofId R S) x = (Algebra.ofId R S) y
c : ↥M
u : Rˣ
eq : x = y
hu : ↑u = ↑c
⊢ x = y
Module: Mathlib.RingTheory.Localization.FractionRing

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
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ 0 < d

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ 0 < d
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹¹ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
P : Type u_3
inst✝⁸ : CommSemiring P
inst✝⁷ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝⁶ : CommSemiring Q
inst✝⁵ : Algebra P Q
inst✝⁴ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst✝³ : CommSemiring A
U : Submonoid A
W : Type u_6
inst✝² : CommSemiring W
inst✝¹ : Algebra A W
inst✝ : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ (map W l hl) ((map Q g hy) x) = ((map W l hl).comp (map Q g hy)) x
Module: Mathlib.RingTheory.Localization.FractionRing

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
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℤ
⊢ x = y → ∃ c, ↑c * x = ↑c * y

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommRing P
A : Type u_4
inst✝ : CommRing A
K : Type u_5
x y : ℤ
⊢ x = y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
⊢ (algebraMap P Q) (g z) * (map Q g hy) x = (algebraMap P Q) (g z) * (map Q g hy) x

Tactic:
]

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ y * (algebraMap R S) (↑u * ↑u⁻¹) = y

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M N : Submonoid R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
inst✝ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : y * (algebraMap R S) ↑(x, s).2 = (algebraMap R S) (x, s).1
u : Rˣ
hu : ↑u = ↑s
⊢ y * (algebraMap R S) (↑u * ↑u⁻¹) = y
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M = Submonoid.map (MonoidHom.id R) M

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M = Submonoid.map (MonoidHom.id R) M
Module: Mathlib.RingTheory.Localization.Defs

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
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ x = x

pp: R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ ∀ (x : R), (RingHom.id S) ((algebraMap R S) x) = (algebraMap R S) (((↑h.symm).comp ↑h) x)

Tactic:
]

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ ∀ (x : R), (RingHom.id S) ((algebraMap R S) x) = (algebraMap R S) (((↑h.symm).comp ↑h) x)