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
M N : 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)
H : M ≤ IsUnit.submonoid R
y : S
x : R
s : ↥M
eq : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
u : Rˣ
hu : (↑u : R) = (↑s : R)
⊢ (algebraMap R S : (a : R) → S) (x * (↑u⁻¹ : R)) = y
have h : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) ((↑u : R) * (↑u⁻¹ : R)) : S) = y
Tactic: rw [map_mul, ← eq, ← hu, mul_assoc, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
⊢ IsLocalization M P
have toIsLocalizationMap : Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
⊢ Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)
have toIsLocalizationMap : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
toIsLocalizationMap : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
⊢ Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)
have toIsLocalizationMap₁ : ∀ (z : P),
  ∃ (x : R × ↥M),
    HMul.hMul (β := P) z ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
toIsLocalizationMap : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
toIsLocalizationMap₁ :
  ∀ (z : P),
    ∃ (x : R × ↥M),
      HMul.hMul (β := P) z ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
⊢ Submonoid.IsLocalizationMap.{u_1, u_3} (M := R) (N := P) M (⇑(algebraMap R P) : (a : R) → P)
have toIsLocalizationMap₂ : ∀ {x y : R},
  Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) x : P) ((algebraMap R P : (a : R) → P) y : P) →
    ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : ↥M
⊢ IsUnit.{u_3} (M := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
have h₁ : Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) (↑y : R) : P)
  (((↑(↑h : S →ₐ[R] P).toRingHom : S →* P) : (a : S) → P) ((algebraMap R S : (a : R) → S) (↑y : R) : S) : P)
Tactic: convert! (IsLocalization.map_units S y).map h.toAlgHom.toRingHom.toMonoidHom
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
have toIsLocalizationMap : ∀ (x : R) (s : ↥M)
  (e :
    HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
      (algebraMap R S : (a : R) → S) (x, s).1),
  ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
Tactic: obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M (h.symm y)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
    (algebraMap R S : (a : R) → S) (x, s).1
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
have e₁ : Eq.{u_3 + 1} (α := P)
  ((have this : S → P := (⇑h : (a : S) → P);
    this)
    (HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S)))
  ((have this : S → P := (⇑h : (a : S) → P);
    this)
    ((algebraMap R S : (a : R) → S) (x, s).1))
Tactic: apply_fun (show S → P from h) at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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
P : Type u_3
inst_3 : CommSemiring P
inst_4 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
y : P
x : R
s : ↥M
e :
  Eq.{u_3 + 1} (α := P)
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      (HMul.hMul (α := S) (β := S) ((h.symm : (a : P) → S) y : S) ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S)))
    ((have this : S → P := (⇑h : (a : S) → P);
      this)
      ((algebraMap R S : (a : R) → S) (x, s).1))
⊢ ∃ (x : R × ↥M),
    HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑x.2 : R) : P) = (algebraMap R P : (a : R) → P) x.1
have e₁ : HMul.hMul (β := P) y ((algebraMap R P : (a : R) → P) (↑s : R) : P) = (algebraMap R P : (a : R) → P) x
Tactic: simp only [map_mul, h.apply_symm_apply, h.commutes] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Basic (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 : Algebra R P
inst_5 : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ Eq.{u_3 + 1} (α := P) ((algebraMap R P : (a : R) → P) x : P) ((algebraMap R P : (a : R) → P) y : P) →
    ∃ (c : ↥M), (↑c : R) * x = (↑c : R) * y
have toIsLocalizationMap : Eq.{u_2 + 1} (α := S) ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
    ((h.symm.toEquiv : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S) →
  Eq.{u_2 + 1} (α := S) ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) x : P) : S)
    ((h.symm : (a : P) → S) ((algebraMap R P : (a : R) → P) y : P) : S)
Tactic: rw [← h.symm.toEquiv.injective.eq_iff, ← IsLocalization.eq_iff_exists M S, ← h.symm.commutes, ←
      h.symm.commutes]
-- 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 : R
ha : a ∈ (↑M₂ : Set R)
⊢ IsUnit.{u_6} (M := T)
    ((algebraMap S₁ T : (a : S₁) → T)
        ((↑(Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                ((algebraMap R S₁ : (a : R) → S₁) a) ⋯) :
            S₁) :
          S₁) :
      T)
have rw : IsUnit.{u_6} (M := T) ((algebraMap S₂ T : (a : S₂) → T) ((algebraMap R S₂ : (a : R) → S₂) a : S₂) : T)
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]
-- 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
⊢ ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
have obtain : ∀ (y : S₂) (m : R) (hm : m ∈ (↑M₁ : Set R))
  (hy :
    HMul.hMul (β := T) a
        ((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) sorry).2 :
                S₂) :
              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) sorry) :
            S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1),
  ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
Tactic: obtain ⟨⟨y, -, m, hm, rfl⟩, hy⟩ := surj (M := Algebra.algebraMapSubmonoid S₂ M₁) a
-- 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
a : T
y : S₂
m : R
hm : m ∈ (↑M₁ : Set R)
hy :
  HMul.hMul (β := T) a
      ((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) ⋯).2 :
              S₂) :
            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
⊢ ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
have 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) sorry) :
        S₂ × ↥(Algebra.algebraMapSubmonoid S₂ M₁)).1
Tactic: rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₁ T] at hy
Cleared hypotheses: 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
⊢ ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
have obtain : ∀ (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),
  ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
Tactic: obtain ⟨⟨z, n, hn⟩, hz⟩ := IsLocalization.surj (M := M₂) 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
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
⊢ ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
have hunit : IsUnit.{u_4} (M := S₁) ((algebraMap R S₁ : (a : R) → S₁) m : S₁)
Tactic: have hunit : IsUnit (algebraMap R S₁ m) := map_units _ ⟨m, hm⟩
-- 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₁)
⊢ ∃ (x : S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)),
    HMul.hMul (β := T) a ((algebraMap S₁ T : (a : S₁) → T) (↑x.2 : S₁) : T) = (algebraMap S₁ T : (a : S₁) → T) x.1
have h : HMul.hMul (β := T) a
    ((algebraMap S₁ T : (a : S₁) → T)
        ((↑(HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) z : S₁) (↑hunit.unit⁻¹ : S₁),
                  Subtype.mk (p := fun (x : S₁) ↦
                    Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                    ((algebraMap R S₁ : (a : R) → S₁) n) sorry).2 :
            S₁) :
          S₁) :
      T) =
  (algebraMap S₁ T : (a : S₁) → T)
    ((HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) z : S₁) (↑hunit.unit⁻¹ : S₁),
          Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
            ((algebraMap R S₁ : (a : R) → S₁) n) sorry) :
        S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)).1
Tactic: use ⟨algebraMap R S₁ z * hunit.unit⁻¹, ⟨algebraMap R S₁ n, n, hn, 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
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)
          ((↑(HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) z : S₁) (↑hunit.unit⁻¹ : S₁),
                    Subtype.mk (p := fun (x : S₁) ↦
                      Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
                      ((algebraMap R S₁ : (a : R) → S₁) n) ⋯).2 :
              S₁) :
            S₁) :
        T) =
    (algebraMap S₁ T : (a : S₁) → T)
      ((HMul.hMul (α := S₁) ((algebraMap R S₁ : (a : R) → S₁) z : S₁) (↑hunit.unit⁻¹ : S₁),
            Subtype.mk (p := fun (x : S₁) ↦ Membership.mem (γ := Submonoid S₁) (Algebra.algebraMapSubmonoid S₁ M₂) x)
              ((algebraMap R S₁ : (a : R) → S₁) n) ⋯) :
          S₁ × ↥(Algebra.algebraMapSubmonoid S₁ M₂)).1
have h : 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₁) z : S₁) : T)
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
Tactic: rw [map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]
-- 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) (β := T) ((algebraMap S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) z : S₁) : T)
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
have rw : HMul.hMul (α := T) (β := T) ((algebraMap R T : (a : R) → T) z : T)
  ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
Tactic: rw [← IsScalarTower.algebraMap_apply]
-- 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 S₁ T : (a : S₁) → T) ((algebraMap R S₁ : (a : R) → S₁) z : 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) (β := T) ((algebraMap R T : (a : R) → T) z : T)
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : S₁) : T)
Tactic: conv_rhs => rw [← IsScalarTower.algebraMap_apply]