mathlib-initiative/mathlib-tactics huggingface dataset:
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 :
  (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) =
    (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂)
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂

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 :
  (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁) =
    (mapPiEvalRingHom S) (mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂)
⊢ mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₁ s₁ =
    mk' (Localization (Submonoid.comap (Pi.evalRingHom R i) S)) r₂ s₂
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
n : ℕ
⊢ mk' S (x ^ n) (y ^ n) = mk' S x y ^ n

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 : R
y : ↥M
n : ℕ
⊢ mk' S (x ^ n) (y ^ n) = mk' S x y ^ 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
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), ↑n * x = ↑n * y ↔ x = y
⊢ (∀ (a a_1 : R), a_1 ∈ M → ∀ (a_2 a_3 : R), a_3 ∈ M → a_3 * (r * a) = a_1 * (r * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂

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
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), ↑n * x = ↑n * y ↔ x = y
⊢ (∀ (a a_1 : R), a_1 ∈ M → ∀ (a_2 a_3 : R), a_3 ∈ M → a_3 * (r * a) = a_1 * (r * a_2) → a_3 * a = a_1 * a_2) ↔
    ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂
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.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.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 ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      g ((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 ↑((toLocalizationMap M S).sec (x + y)).2 +
      g ↑((toLocalizationMap M S).sec y).2 * g ((toLocalizationMap M S).sec x).1 *
        g ↑((toLocalizationMap M S).sec (x + y)).2 =
    g ↑((toLocalizationMap M S).sec y).2 * g ↑((toLocalizationMap M S).sec x).2 *
      g ((toLocalizationMap M S).sec (x + y)).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
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'
⊢ (↑j').toFun = (↑k').toFun

Tactic:
this

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
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
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) (e ((algebraMap A K₁) r / (algebraMap A K₁) s)) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r / (algebraMap A K₁) s))

Tactic:
[

Goal state after:
A : Type u_4
inst✝¹⁹ : CommRing A
B : Type u_6
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst✝¹⁶ : Field K₁
inst✝¹⁵ : Field K₂
inst✝¹⁴ : Algebra A K₁
inst✝¹³ : Algebra A K₂
inst✝¹² : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst✝¹¹ : Field L₁
inst✝¹⁰ : Field L₂
inst✝⁹ : Algebra B L₁
inst✝⁸ : Algebra B L₂
inst✝⁷ : Algebra K₁ L₁
inst✝⁶ : Algebra K₂ L₂
inst✝⁵ : Algebra A L₁
inst✝⁴ : Algebra A L₂
inst✝³ : IsScalarTower A K₁ L₁
inst✝² : IsScalarTower A K₂ L₂
inst✝¹ : IsScalarTower A B L₁
inst✝ : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
r s : A
hs : s ∈ A⁰
⊢ (algebraMap K₂ L₂) (e ((algebraMap A K₁) r / (algebraMap A K₁) s)) =
    f ((algebraMap K₁ L₁) ((algebraMap A K₁) r / (algebraMap A K₁) s))
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Subfield.map f ⊤ = Subfield.closure ↑g.range

Tactic:
← closure_range_algebraMap A K,

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Subfield.map f (Subfield.closure (Set.range ⇑(algebraMap A K))) = Subfield.closure ↑g.range
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s

Tactic:
[

Goal state after:
A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
L : Type u_8
inst✝ : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
s : Set L
hs : g.range = Subring.closure s
x✝ : L
⊢ x✝ ∈ Subfield.closure ↑(Subring.closure s) ↔ x✝ ∈ Subfield.closure s
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
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap FA FB) ((algebraMap A FA) x / (algebraMap A FA) y)) =
    (algebraMap FA FC) ((algebraMap A FA) x / (algebraMap A FA) 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
B✝ : Type u_6
inst✝³⁶ : CommRing B✝
inst✝³⁵ : IsDomain B✝
inst✝³⁴ : Field K
L : Type u_7
inst✝³³ : Field L
inst✝³² : Algebra A✝ K
inst✝³¹ : IsFractionRing A✝ K
g : A✝ →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst✝³⁰ : CommRing A
inst✝²⁹ : CommRing B
inst✝²⁸ : CommRing C
inst✝²⁷ : CommRing D
inst✝²⁶ : Algebra A B
inst✝²⁵ : Algebra A C
inst✝²⁴ : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst✝²³ : Field FA
inst✝²² : Field FB
inst✝²¹ : Field FC
inst✝²⁰ : Field FD
inst✝¹⁹ : Algebra A FA
inst✝¹⁸ : Algebra B FB
inst✝¹⁷ : Algebra C FC
inst✝¹⁶ : Algebra D FD
inst✝¹⁵ : IsFractionRing A FA
inst✝¹⁴ : IsFractionRing B FB
inst✝¹³ : IsFractionRing C FC
inst✝¹² : IsFractionRing D FD
inst✝¹¹ : Algebra A FB
inst✝¹⁰ : IsScalarTower A B FB
inst✝⁹ : Algebra A FC
inst✝⁸ : IsScalarTower A C FC
inst✝⁷ : Algebra A FD
inst✝⁶ : IsScalarTower A D FD
inst✝⁵ : Algebra FA FB
inst✝⁴ : IsScalarTower A FA FB
inst✝³ : Algebra FA FC
inst✝² : IsScalarTower A FA FC
inst✝¹ : Algebra FA FD
inst✝ : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap FA FB) ((algebraMap A FA) x / (algebraMap A FA) y)) =
    (algebraMap FA FC) ((algebraMap A FA) x / (algebraMap A FA) y)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy :
  (algebraMap S₁ T) x * (algebraMap S₁ T) ((algebraMap R S₁) ↑d) =
    (algebraMap S₁ T) y * (algebraMap S₁ T) ((algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy :
  (algebraMap S₁ T) x * (algebraMap S₁ T) ((algebraMap R S₁) ↑d) =
    (algebraMap S₁ T) y * (algebraMap S₁ T) ((algebraMap R S₁) ↑d)
⊢ ∃ c, ↑c * x = ↑c * y
Module: Mathlib.RingTheory.Localization.Defs

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Submonoid R
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra A R
m : A
⊢ mk ((algebraMap A R) m) 1 = (algebraMap A (Localization M)) m

Tactic:
by
  rw [mk_eq_mk', mk'_eq_iff_eq_mul, Submonoid.coe_one, map_one, mul_one]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) c * (algebraMap R S₂) r = (algebraMap R S₂) c * (algebraMap R S₂) s
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹³ : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst✝¹² : CommSemiring S₁
inst✝¹¹ : CommSemiring S₂
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R S₁
inst✝⁸ : Algebra R S₂
inst✝⁷ : Algebra R T
inst✝⁶ : Algebra S₁ T
inst✝⁵ : Algebra S₂ T
inst✝⁴ : IsScalarTower R S₁ T
inst✝³ : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst✝² : IsLocalization M₁ S₁
inst✝¹ : IsLocalization M₂ S₂
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : x * (algebraMap R S₁) ↑d = (algebraMap R S₁) r
hs : y * (algebraMap R S₁) ↑d = (algebraMap R S₁) s
hxy : (algebraMap S₂ T) ((algebraMap R S₂) r) = (algebraMap S₂ T) ((algebraMap R S₂) s)
c : R
hmc : c ∈ ↑M₁
hc : (algebraMap R S₂) c * (algebraMap R S₂) r = (algebraMap R S₂) c * (algebraMap R S₂) s
⊢ ∃ c, ↑c * x = ↑c * 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
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ ↑a₂ • (Localization.mk a₁ a₂ • b) • c = ↑a₂ • Localization.mk a₁ a₂ • b • c

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
inst✝⁸ : IsDomain A
k : Type u_6
K : Type u_7
inst✝⁷ : Field k
inst✝⁶ : Field K
inst✝⁵ : Algebra A k
inst✝⁴ : Algebra A K
inst✝³ : Algebra k K
inst✝² : FaithfulSMul A k
inst✝¹ : FaithfulSMul A K
inst✝ : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x✝ : A × ↥A⁰
a₁ : A
a₂ : ↥A⁰
⊢ ↑a₂ • (Localization.mk a₁ a₂ • b) • c = ↑a₂ • Localization.mk a₁ a₂ • b • c
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
⊢ (r M) (a, b) (c, d) ↔ a * ↑d = ↑b * c

Tactic:
simp only [Localization.r_eq_r', Localization.r', Subtype.exists, exists_prop, Con.rel_mk]

Goal state after:
R : Type u_1
inst✝ : CommRing R
M : Submonoid R
hM : M ≤ nonZeroDivisors R
a c : R
b d : ↥M
⊢ (∃ a_1 ∈ M, a_1 * (↑d * a) = a_1 * (↑b * c)) ↔ a * ↑d = ↑b * c
Module: Mathlib.RingTheory.TensorProduct.Finite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
N : Submodule R M
hN : N ≠ ⊤
hx : ⊤ = R ∙ 0
f : (R ⧸ (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker) ≃ₗ[R] M ⧸ N :=
  (LinearMap.toSpanSingleton R (M ⧸ N) 0).quotKerEquivOfSurjective ⋯
e : (LinearMap.toSpanSingleton R (M ⧸ N) 0).ker = ⊤
this : Nontrivial (M ⧸ N)
⊢ False

Tactic:
simp at hx

Goal state after:
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆
Module: Mathlib.Algebra.Star.Pointwise

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆

Tactic:
[

Goal state after:
α : Type u_1
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p

Tactic:
[

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p = p * q ∧ p = p * q ↔ p = p * q

Tactic:
[

Goal state after:
R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p = p * q ∧ p = p * q ↔ p = p * q
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
⊢ star s.centralizer = (star s).centralizer
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ (s ∪ star s).centralizer
Module: Mathlib.Algebra.Star.Center

Goal state before:
pp: R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ s.centralizer ∩ (star s).centralizer

Tactic:
← star_centralizer,

Goal state after:
R : Type u_1
inst✝¹ : Mul R
inst✝ : StarMul R
s : Set R
hcomm : ∀ x ∈ s, ∀ y ∈ s, y * x = x * y
hcomm_star : ∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y
⊢ s ∪ star s ⊆ s.centralizer ∩ star s.centralizer
Module: Mathlib.Algebra.Algebra.Spectrum.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ

Tactic:
[

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : Subsingleton A
a : A
⊢ resolventSet R a = univ
Module: Mathlib.RingTheory.TensorProduct.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Module R M
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Module A M
inst✝⁵ : Module B M
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A M
inst✝¹ : IsScalarTower R B M
inst✝ : SMulCommClass A B M
x : A ⊗[R] B
⊢ x • 0 = 0

Tactic:
simp only [(· • ·), map_zero]

Goal state after: