awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
⊢ ∃ m ∈ M, x ∣ m
have have : ∀ (s : S) (hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s), ∃ m ∈ M, x ∣ m
Tactic: have ⟨s, hxs⟩ := isUnit_iff_dvd_one.mp h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
⊢ ∃ m ∈ M, x ∣ m
have have : ∀ (r : R) (m : ↥M)
  (hrm :
    HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (r, m).1),
  ∃ m ∈ M, x ∣ m
Tactic: have ⟨⟨r, m⟩, hrm⟩ := surj M s
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S) = (algebraMap R S : (a : R) → S) (r, m).1
⊢ ∃ m ∈ M, x ∣ m
have hrm₁ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
    (HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) (r, m).1 : S)
Tactic: apply_fun (algebraMap R S x * ·) at hrm
Cleared hypotheses: hrm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S)
      (HMul.hMul (β := S) s ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) (r, m).1 : S)
⊢ ∃ m ∈ M, x ∣ m
have hrm₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
  ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)
Tactic: rw [← mul_assoc, ← hxs, one_mul, ← map_mul] at hrm
Cleared hypotheses: hrm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
h : IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) x : S)
s : S
hxs : 1 = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) s
r : R
m : ↥M
hrm :
  Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑(r, m).2 : R) : S)
    ((algebraMap R S : (a : R) → S) (x * (r, m).1) : S)
⊢ ∃ m ∈ M, x ∣ m
have have : ∀ (m' : ↥M) (eq : (↑m' : R) * (↑(r, m).2 : R) = (↑m' : R) * (x * (r, m).1)), ∃ m ∈ M, x ∣ m
Tactic: have ⟨m', eq⟩ := (eq_iff_exists M S).mp hrm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
⊢ (algebraMap R S : (a : R) → S) (sec M z).1 =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S) z
have rw : (algebraMap R S : (a : R) → S) (sec M z).1 =
  HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S)
Tactic: rw [mul_comm, sec_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
rw :
  (algebraMap R S : (a : R) → S) (sec M z).1 =
    HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S)
⊢ (algebraMap R S : (a : R) → S) (sec M z).1 =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑(sec M z).2 : R) : S) z
have rw₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (sec M z).1 : S) ((algebraMap R S : (a : R) → S) (sec M z).1 : S)
Tactic: rw [mul_comm, sec_spec]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
z : S
x : R
y : ↥M
h : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = (algebraMap R S : (a : R) → S) x
hx : x = 0
⊢ z = 0
have h₁ : HMul.hMul (β := S) z ((algebraMap R S : (a : R) → S) (↑y : R) : S) = 0
Tactic: rw [hx, (algebraMap R S).map_zero] at h
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z : R
h : z * (↑y : R) = x
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    (algebraMap R S : (a : R) → S) x
have rw : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
  (algebraMap R S : (a : R) → S) (z * (↑y : R))
Tactic: rw [← h, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z : R
h : z * (↑y : R) = x
rw :
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    (algebraMap R S : (a : R) → S) (z * (↑y : R))
⊢ HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    (algebraMap R S : (a : R) → S) x
have rw₁ : HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
  HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) z : S) ((algebraMap R S : (a : R) → S) (↑y : R) : S)
Tactic: rw [← h, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔
    HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) x : S)
        (HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S)) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have rw : mk' S x y + z₁ = z₂ ↔
  HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
      HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
Tactic: rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
rw :
  mk' S x y + z₁ = z₂ ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
⊢ mk' S x y + z₁ = z₂ ↔
    HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) x : S)
        (HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S)) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have rw₁ : HMul.hMul (β := S) (mk' S x y + z₁) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S) ↔
  HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
      HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
Tactic: rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
rw :
  mk' S x y + z₁ = z₂ ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
rw₁ :
  HMul.hMul (β := S) (mk' S x y + z₁) ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S) ↔
    HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
        HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
⊢ mk' S x y + z₁ = z₂ ↔
    HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) x : S)
        (HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S)) =
      HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
have rw₂ : HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
      HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S) ↔
  HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) +
      HMul.hMul (β := S) z₁ ((algebraMap R S : (a : R) → S) (↑y : R) : S) =
    HMul.hMul (β := S) z₂ ((algebraMap R S : (a : R) → S) (↑y : R) : S)
Tactic: rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
y : ↥M
n : ℕ
⊢ mk' S (x ^ n) (y ^ n) = mk' S x y ^ n
have simp_rw : HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) x : S) n =
  HMul.hMul (β := S) (mk' S x y) ((algebraMap R S : (a : R) → S) (↑y : R) : S) ^ n
Tactic: simp_rw [IsLocalization.mk'_eq_iff_eq_mul, SubmonoidClass.coe_pow, map_pow, ← mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
⊢ IsRegular (mk' S r m) ↔ IsRegular r
have this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
Tactic: have (n : M) (x y : R) : n * x = n * y ↔ x = y := (hM _ n.2).1.eq_iff
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
⊢ IsRegular (mk' S r m) ↔ IsRegular r
have simp : (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : 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: simp +contextual only [← isLeftRegular_iff_isRegular, IsLeftRegular, Function.Injective,
    (mk'_surjective M).forall, ← mk'_mul, Prod.forall, Subtype.forall, IsLocalization.eq,
    Submonoid.coe_mul, this, exists_const, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
hM : ∀ m ∈ M, IsRegular m
r : R
m : ↥M
this : ∀ (n : ↥M) (x y : R), (↑n : R) * x = (↑n : R) * y ↔ x = y
⊢ (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : 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₂
have simp_rw : (∀ (a a_1 : R) (b : a_1 ∈ M) (a_2 a_3 : R) (b : a_3 ∈ M), r * (a_3 * a) = r * (a_1 * a_2) → a_3 * a = a_1 * a_2) ↔
  ∀ ⦃a₁ a₂ : R⦄, r * a₁ = r * a₂ → a₁ = a₂
Tactic: simp_rw [← mul_left_comm r]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
⊢ x = 0
have rw : mk' S (sec M x).1 (sec M x).2 = 0
Tactic: rw [← mk'_sec (M := M) S x, h, mk'_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
rw : mk' S (sec M x).1 (sec M x).2 = 0
⊢ x = 0
have rw₁ : mk' S 0 (sec M x).2 = 0
Tactic: rw [← mk'_sec (M := M) S x, h, mk'_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : S
hx : x ≠ 0
h : (sec M x).1 = 0
rw : mk' S (sec M x).1 (sec M x).2 = 0
rw₁ : mk' S 0 (sec M x).2 = 0
⊢ x = 0
have rw₂ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [← mk'_sec (M := M) S x, h, mk'_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : ↥M
⊢ mk' S (↑x : R) y * mk' S (↑y : R) x = 1
have rw : mk' S ((↑y : R) * (↑x : R)) (y * x) = 1
Tactic: rw [← mk'_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) m
have nth_rw : x • mk' S y m = mk' S (x * y) (1 * m)
Tactic: nth_rw 2 [← one_mul m]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
have rw : x • mk' S y m = mk' (M := M) S x 1 * mk' S y m
Tactic: rw [mk'_mul, mk'_one, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
rw : x • mk' S y m = mk' (M := M) S x 1 * mk' S y m
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
have rw₁ : x • mk' S y m = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m)
Tactic: rw [mk'_mul, mk'_one, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x y : R
m : ↥M
rw : x • mk' S y m = mk' (M := M) S x 1 * mk' S y m
rw₁ : x • mk' S y m = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m)
⊢ x • mk' S y m = mk' S (x * y) (1 * m)
have rw₂ : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m) =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) x : S) (mk' S y m)
Tactic: rw [mk'_mul, mk'_one, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
m : ↥M
⊢ x • mk' S 1 m = mk' S x m
have rw : mk' S (x * 1) m = mk' S x m
Tactic: rw [smul_mk', mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x : R
m : ↥M
rw : mk' S (x * 1) m = mk' S x m
⊢ x • mk' S 1 m = mk' S x m
have rw₁ : mk' S x m = mk' S x m
Tactic: rw [smul_mk', mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
r : R
⊢ (↑m : R) • mk' S r m = (algebraMap R S : (a : R) → S) r
have rw : mk' S ((↑m : R) * r) m = (algebraMap R S : (a : R) → S) r
Tactic: rw [smul_mk', mk'_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
m : ↥M
r : R
rw : mk' S ((↑m : R) * r) m = (algebraMap R S : (a : R) → S) r
⊢ (↑m : R) • mk' S r m = (algebraMap R S : (a : R) → S) r
have rw₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [smul_mk', mk'_mul_cancel_left]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ HMul.hMul (β := S) (mk' S x₁ y₁ + mk' S x₂ y₂) ((algebraMap R S : (a : R) → S) (↑(y₁ * y₂) : R) : S) =
    (algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R))
have rw : HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) ((↑y₁ : R) * (↑(y₁ * y₂) : R) * x₂) : S)
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((↑(y₁ * y₂) : R) * x₁) : S)
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)) =
  HMul.hMul (β := S)
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R)) : S)
      ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
    ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)
Tactic: rw [mul_comm (_ + _), mul_add, mul_mk'_eq_mk'_of_mul, mk'_add_eq_iff_add_mul_eq_mul,
          mul_comm (_ * _), ← mul_assoc, add_comm, ← map_mul, mul_mk'_eq_mk'_of_mul,
          mk'_add_eq_iff_add_mul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
x₁ x₂ : R
y₁ y₂ : ↥M
⊢ HAdd.hAdd (α := S) ((algebraMap R S : (a : R) → S) ((↑y₁ : R) * (↑(y₁ * y₂) : R) * x₂) : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) ((↑(y₁ * y₂) : R) * x₁) : S)
        ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)) =
    HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (x₁ * (↑y₂ : R) + x₂ * (↑y₁ : R)) : S)
        ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)
have simp : HMul.hMul (β := S)
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
          ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)))
      ((algebraMap R S : (a : R) → S) x₂ : S) +
    HMul.hMul (β := S)
      (HMul.hMul (β := S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S)
          ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S))
        ((algebraMap R S : (a : R) → S) x₁ : S))
      ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) =
  HMul.hMul (β := S)
    (HMul.hMul (β := S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₁ : S)
          ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S) +
        HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x₂ : S)
          ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
      ((algebraMap R S : (a : R) → S) (↑y₁ : R) : S))
    ((algebraMap R S : (a : R) → S) (↑y₂ : R) : S)
Tactic: simp only [map_add, Submonoid.coe_mul, map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
P : Type u_3
inst_1 : CommSemiring P
g : R →+* P
h : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
y : ↥M
w z₁ z₂ : P
⊢ w * (↑((IsUnit.liftRight ((↑g : R →* P).restrict M) h : (a : ↥M) → Pˣ) y)⁻¹ : P) + z₁ = z₂ ↔
    w + HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₁ = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₂
have rw : w + HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₁ =
    HMul.hMul (α := P) ((((↑g : R →* P).restrict M : MonoidHom.{u_1, u_3} (↥M) P) : (a : ↥M) → P) y : P) z₂ ↔
  w + HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₁ = HMul.hMul (α := P) ((g : (a : R) → P) (↑y : R) : P) z₂
Tactic: rw [mul_comm, ← one_mul z₁, ← Units.inv_mul (IsUnit.liftRight (g.toMonoidHom.restrict M) h y),
    mul_assoc, ← mul_add, Units.inv_mul_eq_iff_eq_mul, Units.inv_mul_cancel_left,
    IsUnit.coe_liftRight]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
z : S
w w' v : P
⊢ HMul.hMul (α := P) ((Submonoid.LocalizationMap.lift (toLocalizationMap M S) hg : (a : S) → P) z : P) w + w' = v ↔
    HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
        HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P)
          w' =
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v
have rw : HMul.hMul (α := P) (((↑g : R →* P) : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) w' =
    HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v ↔
  HMul.hMul (α := P) ((g : (a : R) → P) (Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).1 : P) w +
      HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) w' =
    HMul.hMul (α := P) ((g : (a : R) → P) (↑(Submonoid.LocalizationMap.sec (toLocalizationMap M S) z).2 : R) : P) v
Tactic: rw [mul_comm, Submonoid.LocalizationMap.lift_apply, ← mul_assoc, mul_add_inv_left hg,
    mul_comm]