awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R_1 : Type u_1
inst : CommRing R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommRing P
A_1 : Type u_4
inst_4 : CommRing A_1
K_1 : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K_1
L_1 : Type u_7
inst_8 : Field L_1
inst_9 : Algebra A_1 K_1
inst_10 : IsFractionRing A_1 K_1
g_1 : A_1 →+* L_1
R : Type u_8
S : Type u_9
inst_11 : CommSemiring R
inst_12 : CommSemiring S
inst_13 : 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_14 : Group G
inst_15 : CommRing A
inst_16 : CommRing B
inst_17 : MulSemiringAction G B
inst_18 : Algebra A B
inst_19 : Field K
inst_20 : Field L
inst_21 : Algebra K L
inst_22 : Algebra A K
inst_23 : Algebra B L
inst_24 : Algebra A L
inst_25 : IsFractionRing A K
inst_26 : IsFractionRing B L
inst_27 : IsScalarTower A K L
inst_28 : IsScalarTower A B L
inst_29 : SMulCommClass G A B
this : MulSemiringAction G L := mulSemiringAction G A B K L
g : G
b : B
x : L
rw :
  HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) * g • x =
    HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) (g • b) : L) (g • x)
⊢ g • b • x = (g • b) • g • x

Tactic:
rw [Algebra.smul_def', Algebra.smul_def', smul_mul']

Premises used: Algebra.smul_def', smul_mul'
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R_1 : Type u_1
inst : CommRing R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommRing P
A_1 : Type u_4
inst_4 : CommRing A_1
K_1 : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K_1
L_1 : Type u_7
inst_8 : Field L_1
inst_9 : Algebra A_1 K_1
inst_10 : IsFractionRing A_1 K_1
g_1 : A_1 →+* L_1
R : Type u_8
S : Type u_9
inst_11 : CommSemiring R
inst_12 : CommSemiring S
inst_13 : 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_14 : Group G
inst_15 : CommRing A
inst_16 : CommRing B
inst_17 : MulSemiringAction G B
inst_18 : Algebra A B
inst_19 : Field K
inst_20 : Field L
inst_21 : Algebra K L
inst_22 : Algebra A K
inst_23 : Algebra B L
inst_24 : Algebra A L
inst_25 : IsFractionRing A K
inst_26 : IsFractionRing B L
inst_27 : IsScalarTower A K L
inst_28 : IsScalarTower A B L
inst_29 : SMulCommClass G A B
this : MulSemiringAction G L := mulSemiringAction G A B K L
g : G
b : B
x : L
e_a : HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b)
⊢ HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) * g • x =
    HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) (g • b) : L) (g • x)

Tactic:
congr
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R_1 : Type u_1
inst : CommRing R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
P : Type u_3
inst_3 : CommRing P
A_1 : Type u_4
inst_4 : CommRing A_1
K_1 : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K_1
L_1 : Type u_7
inst_8 : Field L_1
inst_9 : Algebra A_1 K_1
inst_10 : IsFractionRing A_1 K_1
g_1 : A_1 →+* L_1
R : Type u_8
S : Type u_9
inst_11 : CommSemiring R
inst_12 : CommSemiring S
inst_13 : 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_14 : Group G
inst_15 : CommRing A
inst_16 : CommRing B
inst_17 : MulSemiringAction G B
inst_18 : Algebra A B
inst_19 : Field K
inst_20 : Field L
inst_21 : Algebra K L
inst_22 : Algebra A K
inst_23 : Algebra B L
inst_24 : Algebra A L
inst_25 : IsFractionRing A K
inst_26 : IsFractionRing B L
inst_27 : IsScalarTower A K L
inst_28 : IsScalarTower A B L
inst_29 : SMulCommClass G A B
this : MulSemiringAction G L := mulSemiringAction G A B K L
g : G
b : B
x : L
⊢ HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b)

Tactic:
apply fieldEquivOfAlgEquiv_algebraMap

Premises used: IsFractionRing.fieldEquivOfAlgEquiv_algebraMap
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
G : Type u_10
B : Type u_12
L : Type u_14
inst : Group G
inst_1 : CommRing B
inst_2 : MulSemiringAction G B
inst_3 : Field L
inst_4 : Algebra B L
inst_5 : IsFractionRing B L
inst_6 : MulSemiringAction G L
inst_7 : SMulDistribClass G B L
inst_8 : FaithfulSMul G B
m₁ m₂ : G
h : ∀ (a : L), m₁ • a = m₂ • a
x : B
⊢ m₁ • x = m₂ • x

Tactic:
simpa [← algebraMap.coe_smul'] using h (algebraMap B L x)

Premises used: Algebra.algebraMap, algebraMap.coe_smul', DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : SMulCommClass G A B
g : G
x : K
y : L
obtain :
  ∀ (a b : A) (hb : Membership.mem (γ := Submonoid A) A⁰ b),
    g • HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) • y =
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) • g • y
⊢ g • x • y = x • g • y

Tactic:
obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective A x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : SMulCommClass G A B
g : G
y : L
a b : A
hb : Membership.mem (γ := Submonoid A) A⁰ b
obtain :
  ∀ (c d : B) (hd : Membership.mem (γ := Submonoid B) B⁰ d),
    g •
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) •
          HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) c : L) ((algebraMap B L : (a : B) → L) d : L) =
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) •
        g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) c : L) ((algebraMap B L : (a : B) → L) d : L)
⊢ g • HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) • y =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) • g • y

Tactic:
obtain ⟨c, d, hd, rfl⟩ := IsFractionRing.div_surjective B y

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
G : Type u_10
A : Type u_11
B : Type u_12
K : Type u_13
L : Type u_14
inst : Group G
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : MulSemiringAction G B
inst_4 : Algebra A B
inst_5 : Field K
inst_6 : Field L
inst_7 : Algebra K L
inst_8 : Algebra A K
inst_9 : Algebra B L
inst_10 : Algebra A L
inst_11 : IsFractionRing A K
inst_12 : IsFractionRing B L
inst_13 : IsScalarTower A K L
inst_14 : IsScalarTower A B L
inst_15 : MulSemiringAction G L
inst_16 : SMulDistribClass G B L
inst_17 : SMulCommClass G A B
g : G
a b : A
hb : Membership.mem (γ := Submonoid A) A⁰ b
c d : B
hd : Membership.mem (γ := Submonoid B) B⁰ d
⊢ g •
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) •
        HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) c : L) ((algebraMap B L : (a : B) → L) d : L) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K) •
      g • HDiv.hDiv (α := L) (β := L) ((algebraMap B L : (a : B) → L) c : L) ((algebraMap B L : (a : B) → L) d : L)

Tactic:
simp [Algebra.smul_def, map_div₀, ← IsScalarTower.algebraMap_apply A K L,
      IsScalarTower.algebraMap_apply A B L, smul_mul', smul_div₀',
      ← algebraMap.coe_smul', smul_algebraMap]

Premises used: smul_algebraMap, map_div₀, algebraMap.coe_smul', smul_div₀', Algebra.smul_def, IsScalarTower.algebraMap_apply, smul_mul'
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
Function.Injective.of_comp (f := algebraMap S L) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
refine :
  Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
    (Function.comp.{u_1 + 1, u_2 + 1, u_7 + 1} (β := S) (⇑(algebraMap S L) : (a : S) → L)
      (⇑(algebraMap R S) : (a : R) → S))
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)

Tactic:
refine Function.Injective.of_comp (f := algebraMap S L) ?_

Premises used: Function.Injective.of_comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
rw :
  Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)
⊢ Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
    (Function.comp.{u_1 + 1, u_2 + 1, u_7 + 1} (β := S) (⇑(algebraMap S L) : (a : S) → L)
      (⇑(algebraMap R S) : (a : R) → S))

Tactic:
rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]

Premises used: IsScalarTower.algebraMap_eq, RingHom.coe_comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
⊢ Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)

Tactic:
(algebraMap K L).injective.comp (IsFractionRing.injective R K)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
⊢ Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)

Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective R K)

Premises used: Algebra.algebraMap, IsFractionRing.injective, RingHom.injective, Function.Injective.comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
K : Type u_6
L : Type u_7
inst_3 : Field K
inst_4 : Semiring L
inst_5 : Nontrivial L
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra S L
inst_9 : Algebra K L
inst_10 : Algebra R L
inst_11 : IsScalarTower R S L
inst_12 : IsScalarTower R K L
⊢ FaithfulSMul R S

Tactic:
(faithfulSMul_iff_algebraMap_injective R S).mpr <|
    algebraMap_injective_of_field_isFractionRing R S K L

Premises used: Iff.mpr, faithfulSMul_iff_algebraMap_injective, algebraMap_injective_of_field_isFractionRing
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
⊢ IsFractionRing.{u_1, u_1} (FractionRing R) (FractionRing R)

Tactic:
IsFractionRing.idem R _

Premises used: IsFractionRing.idem
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : Nontrivial R
⊢ Nontrivial.{u_1} (FractionRing R)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : DecidableEq R
x y : FractionRing R
apply :
  (a c : R) →
    (b d : ↥(R⁰ : Submonoid R)) →
      Decidable (Eq (α := Localization (M := R) R⁰) (Localization.mk a b) (Localization.mk c d))
⊢ Decidable (x = y)

Tactic:
apply Localization.recOnSubsingleton₂ x y (r := fun x y ↦ Decidable (x = y))

Premises used: Localization.recOnSubsingleton₂
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : DecidableEq R
x y : FractionRing R
a c : R
b d : ↥(R⁰ : Submonoid R)
simp : Decidable (a * (↑d : R) = (↑b : R) * c)
⊢ Decidable (Eq (α := Localization (M := R) R⁰) (Localization.mk a b) (Localization.mk c d))

Tactic:
simp only [Localization.mk_eq_mk_iff, Localization.r_iff_of_le_nonZeroDivisors (le_refl _)]

Premises used: le_refl, Localization.r_iff_of_le_nonZeroDivisors, Localization.mk_eq_mk_iff
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : DecidableEq R
x y : FractionRing R
a c : R
b d : ↥(R⁰ : Submonoid R)
⊢ Decidable (a * (↑d : R) = (↑b : R) * c)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
inst_1 : IsDomain A
r : A
s : ↥(A⁰ : Submonoid A)
rw :
  IsLocalization.mk' (Localization (M := A) A⁰) r s =
    HDiv.hDiv (α := FractionRing A) (β := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) r : FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑s : A) : FractionRing A)
rw₁ rw₂ :
  HDiv.hDiv (α := Localization (M := A) A⁰) (β := Localization (M := A) A⁰)
      ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) r : Localization (M := A) A⁰)
      ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) (↑s : A) : Localization (M := A) A⁰) =
    HDiv.hDiv (α := FractionRing A) (β := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) r : FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑s : A) : FractionRing A)
⊢ Localization.mk r s =
    HDiv.hDiv (α := FractionRing A) (β := FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) r : FractionRing A)
      ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) (↑s : A) : FractionRing A)

Tactic:
rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]

Premises used: Localization.mk_eq_mk', IsFractionRing.mk'_eq_div
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : IsDomain A
inst_6 : Field K
inst_7 : Algebra R K
inst_8 : FaithfulSMul R K
⊢ IsScalarTower R (FractionRing R) K

Tactic:
have := IsDomain.of_faithfulSMul R K
  .of_algebraMap_eq fun x ↦
    (IsFractionRing.lift_algebraMap (FaithfulSMul.algebraMap_injective R K) x).symm

Premises used: FaithfulSMul.algebraMap_injective, IsScalarTower.of_algebraMap_eq, IsDomain.of_faithfulSMul, Eq.symm, IsFractionRing.lift_algebraMap
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : FaithfulSMul R K
⊢ have this : IsDomain R := ⋯;
  Eq (α := RingHom.{u_1, u_5} (FractionRing R) K) (algebraMap (FractionRing R) K)
    (IsFractionRing.lift (g := algebraMap R K) ⋯)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : IsDomain A
inst_6 : Field K
inst_7 : Algebra R K
inst_8 : FaithfulSMul R K
R₀ : Type u_6
inst_9 : SMul R₀ R
inst_10 : IsScalarTower R₀ R R
inst_11 : SMul R₀ K
inst_12 : IsScalarTower R₀ R K
⊢ IsScalarTower.{u_6, u_1, u_5} R₀ (FractionRing R) K

Tactic:
IsScalarTower.to₁₃₄ _ R _ _

Premises used: IsScalarTower.to₁₃₄
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : IsDomain A
inst_6 : Algebra R A
inst_7 : FaithfulSMul R A
rw :
  Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := FractionRing A)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (FractionRing A)) (algebraMap R A)) :
      (a : R) → FractionRing A)
⊢ FaithfulSMul.{u_1, u_4} R (FractionRing A)

Tactic:
rw [faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq R A]

Premises used: faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : IsDomain A
inst_6 : Algebra R A
inst_7 : FaithfulSMul R A
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := FractionRing A)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (FractionRing A)) (algebraMap R A)) :
      (a : R) → FractionRing A)

Tactic:
(FaithfulSMul.algebraMap_injective A (FractionRing A)).comp
    (FaithfulSMul.algebraMap_injective R A)

Premises used: FractionRing, Function.Injective.comp, Quotient.mk', FaithfulSMul.algebraMap_injective, OreLocalization.oreDiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : IsDomain A
inst_6 : Algebra R A
inst_7 : FaithfulSMul R A
⊢ Function.Injective.{u_1 + 1, u_4 + 1} (α := R) (β := FractionRing A)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A (FractionRing A)) (algebraMap R A)) :
      (a : R) → FractionRing A)

Tactic:
exact (FaithfulSMul.algebraMap_injective A (FractionRing A)).comp
    (FaithfulSMul.algebraMap_injective R A)

Premises used: FractionRing, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K_1 : Type u_5
inst_5 : IsDomain A
k : Type u_6
K : Type u_7
inst_6 : Field k
inst_7 : Field K
inst_8 : Algebra A k
inst_9 : Algebra A K
inst_10 : Algebra k K
inst_11 : FaithfulSMul A k
inst_12 : FaithfulSMul A K
inst_13 : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x : A × ↥(A⁰ : Submonoid A)
a₁ : A
a₂ : ↥(A⁰ : Submonoid A)
rw :
  (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)
⊢ HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)

Tactic:
rw [← smul_right_inj (nonZeroDivisors.coe_ne_zero a₂)]

Premises used: nonZeroDivisors.coe_ne_zero, smul_right_inj
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K_1 : Type u_5
inst_5 : IsDomain A
k : Type u_6
K : Type u_7
inst_6 : Field k
inst_7 : Field K
inst_8 : Algebra A k
inst_9 : Algebra A K
inst_10 : Algebra k K
inst_11 : FaithfulSMul A k
inst_12 : FaithfulSMul A K
inst_13 : IsScalarTower A k K
a : FractionRing A
b : k
c : K
x : A × ↥(A⁰ : Submonoid A)
a₁ : A
a₂ : ↥(A⁰ : Submonoid A)
simp_rw simp_rw₁ :
  (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk a₁ a₂) (b • c)
simp_rw₂ :
  (HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b) • c =
    HSMul.hSMul (β := FractionRing A) (↑a₂ : A) (Localization.mk a₁ a₂) • b • c
simp_rw₃ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) • a₁) a₂) (b • c)
simp_rw₄ :
  HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (Localization.mk ((↑a₂ : A) * a₁) a₂) (b • c)
simp_rw₅ :
  HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) b • c =
    HSMul.hSMul (α := FractionRing A) (IsLocalization.mk' (Localization (M := A) A⁰) ((↑a₂ : A) * a₁) a₂) (b • c)
simp_rw₆ :
  HSMul.hSMul (α := FractionRing A)
        ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) b •
      c =
    HSMul.hSMul (α := FractionRing A)
      ((algebraMap A (Localization (M := A) A⁰) : (a : A) → Localization A⁰) a₁ : Localization (M := A) A⁰) (b • c)
simp_rw₇ : (a₁ • b) • c = a₁ • b • c
⊢ (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) b • c =
    (↑a₂ : A) • HSMul.hSMul (α := FractionRing A) (Localization.mk (a₁, a₂).1 (a₁, a₂).2) (b • c)

Tactic:
simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]

Premises used: Localization.mk_eq_mk', smul_assoc, IsLocalization.mk'_mul_cancel_left, algebraMap_smul, Localization.smul_mk, smul_eq_mul