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

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
K : Type u_5
inst✝⁴ : Field K
L : Type u_7
inst✝³ : Field L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : Algebra A L
f : L →ₐ[A] K
x y : A
hy : y ∈ A⁰
⊢ f ((algebraMap A L) x / (algebraMap A L) y) = (algebraMap A K) x / (algebraMap A K) y

Tactic:
by

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

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
K : Type u_5
inst✝⁴ : Field K
L : Type u_7
inst✝³ : Field L
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : Algebra A L
f : L →ₐ[A] K
⊢ IsFractionRing A L

Tactic:
by

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
h : R ≃+* P
⊢ IsLocalization (Submonoid.map h M) S

Tactic:
by

Goal state after:
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₂
x : K₁
⊢ (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Tactic:
by

Goal state after:
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₂
x : K₁
⊢ (algebraMap K₂ L₂) (e x) = f ((algebraMap K₁ L₁) x)

Tactic:
by

Goal state after:
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
z : K
x✝ : z ∈ ⊤
⊢ z ∈ Subfield.closure (Set.range ⇑(algebraMap A K))

Tactic:
by

Goal state after:
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
⊢ f.fieldRange = Subfield.closure ↑g.range

Tactic:
by

Goal state after:
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
⊢ f.fieldRange = Subfield.closure s

Tactic:
by

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f1 f2 : K →+* L
hf : ∀ (x : A), f1 ((algebraMap A K) x) = f2 ((algebraMap A K) x)
⊢ f1 = f2

Tactic:
by

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
x : B
hx : x ∈ adjoin R s
hr : (algebraMap A B) r ∈ B'
⊢ ∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ B'

Tactic:
by

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
s : Set L
hs : g.range = Subring.closure s
⊢ (lift hg).comp (algebraMap A K) = g

Tactic:
by

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

Goal state before:
pp: A : Type u_4
inst✝⁴ : CommRing A
K : Type u_5
inst✝³ : Field K
L : Type u_7
inst✝² : Field L
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
g : A →+* L
hg : Injective ⇑g
x : A
y : ↥A⁰
⊢ (lift hg) (mk' K x y) = g x / g ↑y

Tactic:
by

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

Goal state before:
pp: A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
h : A ≃+* B
a : A
⊢ (ringEquivOfRingEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

Tactic:
by

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

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ringEquivOfRingEquiv (RingEquiv.refl A) = RingEquiv.refl K

Tactic:
by

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

Goal state before:
pp: A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsFractionRing B L
C : Type u_12
M : Type u_13
inst✝³ : CommRing C
inst✝² : CommRing M
inst✝¹ : Algebra C M
inst✝ : IsFractionRing C M
f : A ≃+* B
g : B ≃+* C
⊢ ringEquivOfRingEquiv (f.trans g) = (ringEquivOfRingEquiv f).trans (ringEquivOfRingEquiv g)

Tactic:
by

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

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ Subalgebra.toSubmodule (adjoin R ↑s) = R ∙ 1 ⊔ s.toSubmodule

Tactic:
by

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

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : CommSemiring F
inst✝¹ : Algebra F K
inst✝ : IsScalarTower F E K
L : Subalgebra F K
ι : Type u_4
bL : Basis ι F ↥L
⊢ toSubmodule L = span F (Set.range fun i ↦ ↑(bL i))

Tactic:
by

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

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Injective ⇑(ringEquivOfRingEquivHom A K)

Tactic:
by

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

Goal state before:
pp: F : Type u_4
inst✝² : CommSemiring F
E : Type u_5
inst✝¹ : CommSemiring E
inst✝ : Algebra F E
K : Subalgebra F E
S : Set E
⊢ Subalgebra.restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
by

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

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
K K' : Subalgebra F E
h : K.toSubsemiring = K'.toSubsemiring
⊢ K = K'

Tactic:
by

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
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
K : Type u_10
L : Type u_11
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
f : A ≃+* B
r : A
x : K
⊢ (ringEquivOfRingEquiv f).toFun (r • x) = ↑f r • (ringEquivOfRingEquiv f).toFun x

Tactic:
by

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

Goal state before:
pp: A : Type u_8
B : Type u_9
K : Type u_10
L : Type u_11
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : CommRing K
inst✝⁴ : CommRing L
inst✝³ : Algebra A K
inst✝² : IsFractionRing A K
inst✝¹ : Algebra B L
inst✝ : IsFractionRing B L
f : A ≃+* B
a : A
⊢ (semilinearEquivOfRingEquiv K L f) ((algebraMap A K) a) = (algebraMap B L) (f a)

Tactic:
by

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

Goal state before:
pp: A : Type u_8
B : Type u_9
K : Type u_10
L : Type u_11
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsFractionRing B L
f : A ≃+* B
C : Type u_12
M : Type u_13
inst✝³ : CommRing C
inst✝² : CommRing M
inst✝¹ : Algebra C M
inst✝ : IsFractionRing C M
g : B ≃+* C
⊢ let this := ⋯;
  let this_1 := ⋯;
  semilinearEquivOfRingEquiv K M (f.trans g) =
    (semilinearEquivOfRingEquiv K L f).trans (semilinearEquivOfRingEquiv L M g)

Tactic:
by

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

Goal state before:
pp: F : Type u_4
E : Type u_5
L : Type u_6
L' : Type u_7
inst✝¹⁰ : CommSemiring F
inst✝⁹ : CommSemiring L
inst✝⁸ : CommSemiring L'
inst✝⁷ : Semiring E
inst✝⁶ : Algebra F L
inst✝⁵ : Algebra L E
inst✝⁴ : Algebra F L'
inst✝³ : Algebra L' E
inst✝² : Algebra F E
inst✝¹ : IsScalarTower F L E
inst✝ : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i
S : Set E
⊢ Subalgebra.restrictScalars F (adjoin L S) = Subalgebra.restrictScalars F (adjoin L' S)

Tactic:
by

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

Goal state before:
pp: R : Type u_8
A : Type u_9
K : Type u_10
B : Type u_11
L : Type u_12
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : CommRing K
inst✝¹⁰ : CommRing L
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R K
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsScalarTower R A K
inst✝⁴ : Algebra R B
inst✝³ : Algebra R L
inst✝² : Algebra B L
inst✝¹ : IsFractionRing B L
inst✝ : IsScalarTower R B L
h : A ≃ₐ[R] B
a : A
⊢ (algEquivOfAlgEquiv h) ((algebraMap A K) a) = (algebraMap B L) (h a)

Tactic:
by

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
h : R ≃+* P
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ ∀ (r : S), (algebraMap S K) r = (algebraMap S K) r

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Type u_4
inst✝⁴ : CommSemiring S
K : Type u_5
inst✝³ : CommSemiring K
inst✝² : Algebra R K
e : R ≃+* S
inst✝¹ : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h : ∀ (x : R), (algebraMap R K) x = (algebraMap S K) (e x)
inst✝ : IsLocalization M₁ K
⊢ IsLocalization M₂ K

Tactic:
by

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
a : T
⊢ ∃ x, a * (algebraMap S₁ T) ↑x.2 = (algebraMap S₁ T) x.1

Tactic:
by

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✝ : Subsingleton R
a : Localization M
x✝ : R × ↥M
⊢ mk x✝.1 x✝.2 = mk 1 1

Tactic:
by

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✝ : Subsingleton R
a : Localization M
⊢ a = default

Tactic:
by

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✝ : Subsingleton R
a : Localization M
⊢ a = default

Tactic:
by
    with_unfolding_all change a = mk 1 1
    exact Localization.induction_on a fun _ => by
      congr <;> apply Subsingleton.elim

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
d : ↥M
⊢ mk a b + mk c d = mk (↑b * c + ↑d * a) (b * d)

Tactic:
by

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
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 : FA
⊢ (ringEquivOfRingEquiv f.toRingEquiv).toFun ((algebraMap FA FB) x) = (algebraMap FA FC) x

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
a : R
b : ↥M
c : R
⊢ mk a b + mk c b = mk (a + c) b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
M : Submonoid R
x : R
y : ↥M
⊢ mk x y = mk' (Localization M) x y

Tactic:
by

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

Goal state before:
pp: A : Type u_8
B : Type u_9
C : Type u_10
inst✝²¹ : CommRing A
inst✝²⁰ : CommRing B
inst✝¹⁹ : CommRing C
inst✝¹⁸ : Algebra A B
inst✝¹⁷ : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst✝¹⁶ : Field FA
inst✝¹⁵ : Field FB
inst✝¹⁴ : Field FC
inst✝¹³ : Algebra A FA
inst✝¹² : Algebra B FB
inst✝¹¹ : Algebra C FC
inst✝¹⁰ : IsFractionRing A FA
inst✝⁹ : IsFractionRing B FB
inst✝⁸ : IsFractionRing C FC
inst✝⁷ : Algebra A FB
inst✝⁶ : IsScalarTower A B FB
inst✝⁵ : Algebra A FC
inst✝⁴ : IsScalarTower A C FC
inst✝³ : Algebra FA FB
inst✝² : IsScalarTower A FA FB
inst✝¹ : Algebra FA FC
inst✝ : IsScalarTower A FA FC
f : B ≃ₐ[A] C
⊢ AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) = algEquivOfAlgEquiv f

Tactic:
by

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

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

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
FA : Type u_12
FB : Type u_13
inst✝⁹ : Field FA
inst✝⁸ : Field FB
inst✝⁷ : Algebra A FA
inst✝⁶ : Algebra B FB
inst✝⁵ : IsFractionRing A FA
inst✝⁴ : IsFractionRing B FB
inst✝³ : Algebra A FB
inst✝² : IsScalarTower A B FB
inst✝¹ : Algebra FA FB
inst✝ : IsScalarTower A FA FB
⊢ fieldEquivOfAlgEquiv FA FB FB AlgEquiv.refl = AlgEquiv.refl

Tactic:
by

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
hM : M ≤ nonZeroDivisors R
⊢ (algebraMap R S) x = 0 ↔ x = 0

Tactic:
by

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

Goal state before:
pp: 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
g : C ≃ₐ[A] D
⊢ fieldEquivOfAlgEquiv FA FB FD (f.trans g) = (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g)

Tactic:
by

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
inst✝ : Nontrivial R
hM : M ≤ nonZeroDivisors R
x : R
hx : x ∈ nonZeroDivisors R
⊢ (algebraMap R S) x ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
M : Submonoid R
a c : R
b d : ↥M
⊢ mk a b - mk c d = mk (↑d * a - ↑b * c) (b * d)

Tactic:
by

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

Goal state before:
pp: A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
K : Type u_10
L : Type u_11
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsFractionRing A K
inst✝⁴ : IsFractionRing B L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A B L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower A K L
⊢ Injective ⇑(fieldEquivOfAlgEquivHom K L)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
P : Type u_3
inst✝ : CommRing P
h : R ≃+* P
⊢ IsFractionRing R S ↔ IsFractionRing P S

Tactic:
by

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

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
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ mk' S (-x) y = -mk' S x y

Tactic:
by

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

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
h : IsFractionRing R S
⊢ Nontrivial R ↔ Nontrivial S

Tactic:
by

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

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
inst✝ : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ mk' S (x₁ * ↑y₂ - x₂ * ↑y₁) (y₁ * y₂) = mk' S x₁ y₁ - mk' S x₂ y₂

Tactic:
by

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
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✝
R : Type u_8
S : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Algebra R S
h : IsFractionRing R S
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁴ : Group G
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A L
inst✝³ : IsFractionRing A K
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
this : MulSemiringAction G L := mulSemiringAction G B L
g : G
b : B
x : L
⊢ g • b • x = (g • b) • g • x

Tactic:
by

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

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
inst✝¹ : IsLocalization M S
T : Type u_4
inst✝ : CommRing T
f : S →+* T
h : ∀ (x : R), f ((algebraMap R S) x) = 0 → (algebraMap R S) x = 0
⊢ Injective ⇑f

Tactic:
by

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

Goal state before:
pp: G : Type u_10
B : Type u_12
L : Type u_14
inst✝⁸ : Group G
inst✝⁷ : CommRing B
inst✝⁶ : MulSemiringAction G B
inst✝⁵ : Field L
inst✝⁴ : Algebra B L
inst✝³ : IsFractionRing B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : FaithfulSMul G B
m₁✝ m₂✝ : G
h : ∀ (a : L), m₁✝ • a = m₂✝ • a
x : ?m.65 h
⊢ m₁✝ • x = m₂✝ • x

Tactic:
by

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

Goal state before:
pp: G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst✝¹⁷ : Group G
inst✝¹⁶ : CommRing A
inst✝¹⁵ : CommRing B
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra A B
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : Algebra A K
inst✝⁸ : Algebra B L
inst✝⁷ : Algebra A L
inst✝⁶ : IsFractionRing A K
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : MulSemiringAction G L
inst✝¹ : SMulDistribClass G B L
inst✝ : SMulCommClass G A B
g : G
x : K
y : L
⊢ g • x • y = x • g • y

Tactic:
by

Goal state after: