awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
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) ((algebraMap R S₂ : (a : R) → S₂) a : S₂) : T)

Tactic:
IsUnit.map _ (IsLocalization.map_units _ ⟨a, ha⟩)

Premises used: Subtype.mk, IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.Basic
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) ((algebraMap R S₂ : (a : R) → S₂) a : S₂) : T)

Tactic:
exact IsUnit.map _ (IsLocalization.map_units _ ⟨a, ha⟩)

Premises used: Subtype.mk, IsLocalization.map_units, IsUnit.map
-- Module: Mathlib.RingTheory.Localization.Basic
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
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) ⋯).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
⊢ ∃ (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

Premises used: IsLocalization.surj, Algebra.algebraMapSubmonoid, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ 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

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₁ T] at hy

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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
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
⊢ ∃ (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

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Basic
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
⊢ 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⟩
-- Module: Mathlib.RingTheory.Localization.Basic
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) 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
⊢ ∃ (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:
use ⟨algebraMap R S₁ z * hunit.unit⁻¹, ⟨algebraMap R S₁ n, n, hn, rfl⟩⟩
-- Module: Mathlib.RingTheory.Localization.Basic
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) 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)
⊢ 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

Tactic:
rw [map_mul, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply R S₂ T]

Premises used: map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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₁)
rw :
  HMul.hMul (α := T) (β := T) ((algebraMap R T : (a : R) → T) z : T)
    ((algebraMap S₁ T : (a : S₁) → T) (↑hunit.unit⁻¹ : 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 [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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) 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)
⊢ 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:
conv_rhs => rw [← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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) 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)
⊢ 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:
rw [IsScalarTower.algebraMap_apply R S₂ T, ← hz, map_mul, ← hy]

Premises used: map_mul, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
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)
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)
⊢ 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:
convert_to _ = a * (algebraMap S₂ T) ((algebraMap R S₂) n) *
        (algebraMap S₁ T) (((algebraMap R S₁) m) * hunit.unit⁻¹.val)

Premises used: Units.val, HMul.hMul, Algebra.algebraMap, Inv.inv, IsUnit.unit, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Basic
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) 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)
⊢ 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:
rw [map_mul]

Premises used: map_mul