awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
h : R ≃+* P
⊢ IsLocalization.{u_1, u_2} (R := R) R⁰ S ↔ IsLocalization.{u_3, u_2} (R := P) P⁰ S
have h₁ : Eq (α := Submonoid P) (P⁰ : Submonoid P) (Submonoid.map h (R⁰ : Submonoid R))
Tactic: convert! isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
⊢ Nontrivial R ↔ Nontrivial S
have inl : Nontrivial R → Subsingleton S → False
Tactic: by_contra! ⟨_, _⟩ | ⟨_, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
inl : Nontrivial R → Subsingleton S → False
⊢ Nontrivial R ↔ Nontrivial S
have inr : Subsingleton R → Nontrivial S → False
Tactic: by_contra! ⟨_, _⟩ | ⟨_, _⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Nontrivial R
right : Subsingleton S
⊢ False
have inl : ∀ (c : ↥(R⁰ : Submonoid R)) (hc : (↑c : R) * 1 = (↑c : R) * 0), False
Tactic: obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Subsingleton R
right : Nontrivial S
⊢ False
have inr : Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑1 : R) : S) (0 : S)
Tactic: apply (h.map_units S 1).ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Subsingleton R
right : Nontrivial S
⊢ Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑1 : R) : S) (0 : S)
have inr : Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
Tactic: rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Subsingleton R
right : Nontrivial S
inr : Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
⊢ Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑1 : R) : S) (0 : S)
have inr₁ : Eq.{u_9 + 1} (α := S) 0 0
Tactic: rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ g • b • x = (g • b) • g • x
have 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)
Tactic: rw [Algebra.smul_def', Algebra.smul_def', smul_mul']
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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) * g • x =
    HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) (g • b) : L) (g • x)
have e_a : HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ g • x • y = x • g • y
have 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
Tactic: obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective A x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ 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
have 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)
Tactic: obtain ⟨c, d, hd, rfl⟩ := IsFractionRing.div_surjective B y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
have 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))
Tactic: refine Function.Injective.of_comp (f := algebraMap S L) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
    (Function.comp.{u_1 + 1, u_2 + 1, u_7 + 1} (β := S) (⇑(algebraMap S L) : (a : S) → L)
      (⇑(algebraMap R S) : (a : R) → S))
have rw : Function.Injective.{u_1 + 1, u_7 + 1} (α := R) (β := L)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)
Tactic: rw [← RingHom.coe_comp, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq R K L]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ Decidable (x = y)
have apply : (a c : R) →
  (b d : ↥(R⁰ : Submonoid R)) →
    Decidable (Eq (α := Localization (M := R) R⁰) (Localization.mk a b) (Localization.mk c d))
Tactic: apply Localization.recOnSubsingleton₂ x y (r := fun x y ↦ Decidable (x = y))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 (Eq (α := Localization (M := R) R⁰) (Localization.mk a b) (Localization.mk c d))
have simp : Decidable (a * (↑d : R) = (↑b : R) * c)
Tactic: simp only [Localization.mk_eq_mk_iff, Localization.r_iff_of_le_nonZeroDivisors (le_refl _)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_4
inst : CommRing A
inst_1 : IsDomain A
r : A
s : ↥(A⁰ : Submonoid 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)
have 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)
Tactic: rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Localization.mk_eq_mk', IsFractionRing.mk'_eq_div]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ FaithfulSMul.{u_1, u_4} R (FractionRing A)
have 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)
Tactic: rw [faithfulSMul_iff_algebraMap_injective, IsScalarTower.algebraMap_eq R A]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← smul_right_inj (nonZeroDivisors.coe_ne_zero a₂)]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ (↑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)
have 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)
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ (↑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)
have 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
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ (↑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)
have 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)
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ (↑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)
have 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)
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ (↑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)
have 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)
Tactic: simp_rw [← smul_assoc, Localization.smul_mk, smul_eq_mul, Localization.mk_eq_mk',
      IsLocalization.mk'_mul_cancel_left, algebraMap_smul, smul_assoc]