awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
⊢ HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap R T : (a : R) → T) z : T)
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
have h : HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
  HMul.hMul (β := T)
    (HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
      ((algebraMap S₂ T : (a : S₂) → T)
          ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
        T))
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
Tactic: rw [IsScalarTower.algebraMap_apply R S₂ T, ← hz, map_mul, ← hy]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
⊢ HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T)
        (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
        ((algebraMap S₂ T : (a : S₂) → T)
            ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
          T))
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
have h : HMul.hMul (β := T)
    (HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
      ((algebraMap S₂ T : (a : S₂) → T)
          ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
        T))
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T) =
  HMul.hMul (β := T)
    (HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T))
    ((algebraMap S₁ T : (a : S₁) → T)
        (HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) (↑hunit.unit⁻¹ : S₁)) :
      T)
Tactic: convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
h :
  HMul.hMul (β := T)
      (HMul.hMul (β := T)
        (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
        ((algebraMap S₂ T : (a : S₂) → T)
            ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
          T))
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T))
      ((algebraMap S₁ T : (a : S₁) → T)
          (HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) (↑hunit.unit⁻¹ : S₁)) :
        T)
⊢ HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T)
        (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
        ((algebraMap S₂ T : (a : S₂) → T)
            ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
          T))
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
have h₁ : HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) =
  HMul.hMul (β := T)
    (HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T))
    ((algebraMap S₁ T : (a : S₁) → T)
        (HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) (↑hunit.unit⁻¹ : S₁)) :
      T)
Tactic: convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T) =
    (algebraMap S₂ T : (a : S₂) → T)
      ((y,
            Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) m) ⋯) :
          S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
z n : R
hn : n ∈ M₂
hz :
  HMul.hMul (β := S₂) y
      ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) =
    (algebraMap R S₂ : (a : R) → S₂) (z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).1
hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
⊢ HMul.hMul (β := T)
      (HMul.hMul (β := T)
        (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
        ((algebraMap S₂ T : (a : S₂) → T)
            ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
          T))
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T) =
    HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T))
      ((algebraMap S₁ T : (a : S₁) → T)
          (HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) (↑hunit.unit⁻¹ : S₁)) :
        T)
have h : HMul.hMul (β := T)
    (HMul.hMul (β := T)
      (HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T))
      ((algebraMap S₂ T : (a : S₂) → T)
          ((algebraMap R S₂ : (a : R) → S₂) (↑(z, Subtype.mk (p := fun (x : R) ↦ x ∈ M₂) n hn).2 : R) : S₂) :
        T))
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T) =
  HMul.hMul (β := T) a ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) n : S₂) : T) *
    HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) m : S₁) : T)
      ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
Tactic: rw [map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
hxy : Eq.{u_6 + 1} (α := T) ((algebraMap S₁ T : (a : S₁) → T) x : T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have obtain : ∀ (r s : R) (d : ↥M₁)
  (hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r)
  (hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s),
  ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
Tactic: obtain ⟨r, s, d, hr, hs⟩ := IsLocalization.surj₂ M₁ S₁ x y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
hxy : Eq.{u_6 + 1} (α := T) ((algebraMap S₁ T : (a : S₁) → T) x : T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have hxy₁ : HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) x : T)
    ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T) =
  HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
    ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T)
Tactic: apply_fun (· * algebraMap S₁ T (algebraMap R S₁ d)) at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) x : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T) =
    HMul.hMul (α := T) (β := T) ((algebraMap S₁ T : (a : S₁) → T) y : T)
      ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) : T)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have hxy₁ : Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
  ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
Tactic: simp_rw [← map_mul, hr, hs, ← IsScalarTower.algebraMap_apply,
      IsScalarTower.algebraMap_apply R S₂ T] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have obtain : ∀ (c : R) (hmc : c ∈ (↑M₁ : Set R))
  (hc :
    HMul.hMul (α := S₂) (β := S₂)
        ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
                ((algebraMap R S₂ : (a : R) → S₂) c) sorry) :
            S₂) :
          S₂)
        ((algebraMap R S₂ : (a : R) → S₂) r : S₂) =
      HMul.hMul (α := S₂) (β := S₂)
        ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
                ((algebraMap R S₂ : (a : R) → S₂) c) sorry) :
            S₂) :
          S₂)
        ((algebraMap R S₂ : (a : R) → S₂) s : S₂)),
  ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
Tactic: obtain ⟨⟨-, c, hmc, rfl⟩, hc⟩ := exists_of_eq (M := Algebra.algebraMapSubmonoid S₂ M₁) hxy
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  HMul.hMul (α := S₂) (β := S₂)
      ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
          S₂) :
        S₂)
      ((algebraMap R S₂ : (a : R) → S₂) r : S₂) =
    HMul.hMul (α := S₂) (β := S₂)
      ((↑(Subtype.mk (p := fun (x : S₂) ↦ Membership.mem (γ := Submonoid S₂) (Algebra.algebraMapSubmonoid S₂ M₁) x)
              ((algebraMap R S₂ : (a : R) → S₂) c) ⋯) :
          S₂) :
        S₂)
      ((algebraMap R S₂ : (a : R) → S₂) s : S₂)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have hc₁ : Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
Tactic: simp_rw [← map_mul] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have obtain : ∀ (a : ↥M₂) (ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)),
  ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
Tactic: obtain ⟨a, ha⟩ := IsLocalization.exists_of_eq (M := M₂) hc
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
⊢ ∃ (c : ↥(Algebra.algebraMapSubmonoid S₁ M₂)), (↑c : S₁) * x = (↑c : S₁) * y
have h : HMul.hMul (α := S₁)
    ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
            ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) sorry) :
        S₁) :
      S₁)
    x =
  HMul.hMul (α := S₁)
    ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
            ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) sorry) :
        S₁) :
      S₁)
    y
Tactic: use ⟨algebraMap R S₁ a, a, a.property, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S₁ : Type u_4
S₂ : Type u_5
T : Type u_6
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : CommSemiring T
inst_4 : Algebra R S₁
inst_5 : Algebra R S₂
inst_6 : Algebra R T
inst_7 : Algebra S₁ T
inst_8 : Algebra S₂ T
inst_9 : IsScalarTower R S₁ T
inst_10 : IsScalarTower R S₂ T
M₁ M₂ : Submonoid R
inst_11 : IsLocalization M₁ S₁
inst_12 : IsLocalization M₂ S₂
inst_13 : IsLocalization (Algebra.algebraMapSubmonoid S₂ M₁) T
x y : S₁
r s : R
d : ↥M₁
hr : HMul.hMul (β := S₁) x ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) r
hs : HMul.hMul (β := S₁) y ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) = (algebraMap R S₁ : (a : R) → S₁) s
hxy :
  Eq.{u_6 + 1} (α := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) r : S₂) : T)
    ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) s : S₂) : T)
c : R
hmc : c ∈ (↑M₁ : Set R)
hc :
  Eq.{u_5 + 1} (α := S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * r) : S₂) ((algebraMap R S₂ : (a : R) → S₂) (c * s) : S₂)
a : ↥M₂
ha : (↑a : R) * (c * r) = (↑a : R) * (c * s)
⊢ HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      x =
    HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) ⋯) :
          S₁) :
        S₁)
      y
have h : HMul.hMul (β := S₁)
    (HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) sorry) :
          S₁) :
        S₁)
      x)
    ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁) =
  HMul.hMul (β := S₁)
    (HMul.hMul (α := S₁)
      ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) (↑a : R)) sorry) :
          S₁) :
        S₁)
      y)
    ((algebraMap R S₁ : (a : R) → S₁) (↑d : R) : S₁)
Tactic: apply (map_units S₁ d).mul_right_cancel