awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
i : ι
S : Submonoid (R i)
T : Submonoid ((i : ι) → R i) := Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S
refine_1 :
  ∀ (x₁ x₂ : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S))
    (eq :
      Eq.{u_2 + 1} (α := Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₁ :
          Localization (M := R i) S)
        ((mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)
            x₂ :
          Localization (M := R i) S)),
    x₁ = x₂
refine_2 refine_2₁ :
  ∀ (x : Localization (M := R i) S),
    ∃ (a : Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)),
      (mapPiEvalRingHom (R := R) S : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S) a = x
⊢ Bijective (α := Localization (Submonoid.comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) S)) (β :=
    Localization (M := R i) S)
    (⇑(mapPiEvalRingHom (R := R) S) : (a : Localization (Submonoid.comap (Pi.evalRingHom R i) S)) → Localization S)

Tactic:
classical
  refine ⟨fun x₁ x₂ eq ↦ ?_, fun x ↦ ?_⟩
  · obtain ⟨r₁, s₁, rfl⟩ := exists_mk'_eq T x₁
    obtain ⟨r₂, s₂, rfl⟩ := exists_mk'_eq T x₂
    simp_rw [map_mk'] at eq
    rw [IsLocalization.eq] at eq ⊢
    obtain ⟨s, hs⟩ := eq
    refine ⟨⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩, funext fun j ↦ ?_⟩
    obtain rfl | ne := eq_or_ne j i
    · simpa using hs
    · simp [update_of_ne ne]
  · obtain ⟨r, s, rfl⟩ := exists_mk'_eq S x
    exact ⟨mk' (M := T) _ (update 0 i r) ⟨update 0 i s, by apply update_self i s.1 0 ▸ s.2⟩,
      by simp [map_mk']⟩

Premises used: IsLocalization.map_mk', Localization.r, IsLocalization.eq, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
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
inst_4 : Finite R
x : S
⊢ ∃ (a : R × ↥M), uncurry (mk' S) a = x

Tactic:
simpa using IsLocalization.exists_mk'_eq M x

Premises used: IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
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
inst_4 : Finite R
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := R × ↥M) (uncurry (mk' S))

Tactic:
have : Function.Surjective (Function.uncurry (mk' (M := M) S)) := fun x ↦ by
    simpa using IsLocalization.exists_mk'_eq M x
-- Module: Mathlib.RingTheory.Localization.Basic
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
inst_4 : Finite R
this : Surjective.{u_1 + 1, u_2 + 1} (α := R × ↥M) (uncurry (mk' S))
⊢ Finite S

Tactic:
.of_surjective _ this

Premises used: Finite.of_surjective
-- Module: Mathlib.RingTheory.Localization.Basic
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
inst_4 : Finite R
this : Surjective.{u_1 + 1, u_2 + 1} (α := R × ↥M) (uncurry (mk' S))
⊢ Finite S

Tactic:
exact .of_surjective _ this
-- Module: Mathlib.RingTheory.Localization.Basic
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
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s : S
s' : N₁
obtain :
  ∀ (r : R) (m : ↥M),
    (f : (a : N₁) → N₂) (mk' S r m • s') = HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
⊢ (f : (a : N₁) → N₂) (s • s') = HSMul.hSMul (β := N₂) s ((f : (a : N₁) → N₂) s' : N₂)

Tactic:
obtain ⟨r, m, rfl⟩ := exists_mk'_eq M s

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Basic
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
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
rw :
  HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))
⊢ (f : (a : N₁) → N₂) (mk' S r m • s') = HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)

Tactic:
rw [← (map_units S m).smul_left_cancel]

Premises used: IsUnit.smul_left_cancel, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Basic
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
N₁ : Type u_4
N₂ : Type u_5
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : Module R N₁
inst_7 : Module R N₂
inst_8 : Module S N₁
inst_9 : Module S N₂
inst_10 : IsScalarTower R S N₁
inst_11 : IsScalarTower R S N₂
f : N₁ →ₗ[R] N₂
s' : N₁
r : R
m : ↥M
simp_rw :
  HSMul.hSMul (β := N₂) (↑m : R) ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₁ :
  (f : (a : N₁) → N₂) ((↑m : R) • mk' S r m • s') =
    (↑m : R) • HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₂ :
  (f : (a : N₁) → N₂) (((↑m : R) • mk' S r m) • s') =
    HSMul.hSMul (β := N₂) ((↑m : R) • mk' S r m) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₃ :
  (f : (a : N₁) → N₂) (HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) r : S) s') =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : N₁) → N₂) s' : N₂)
simp_rw₄ : (f : (a : N₁) → N₂) (r • s') = HSMul.hSMul (β := N₂) r ((f : (a : N₁) → N₂) s' : N₂)
⊢ HSMul.hSMul.{u_2, u_5, u_5} (α := S) (β := N₂) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      ((f : (a : N₁) → N₂) (mk' S r m • s') : N₂) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((algebraMap R S : (a : R) → S) (↑m : R) : S)
      (HSMul.hSMul (β := N₂) (mk' S r m) ((f : (a : N₁) → N₂) s' : N₂))

Tactic:
simp_rw [algebraMap_smul, ← map_smul, ← smul_assoc, smul_mk'_self, algebraMap_smul, map_smul]

Premises used: smul_assoc, IsLocalization.smul_mk'_self, algebraMap_smul, map_smul
-- Module: Mathlib.RingTheory.Localization.Basic
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
N₁ : Type u_4
N₂ : Type u_5
inst_5 : AddCommMonoid N₁
inst_6 : AddCommMonoid N₂
inst_7 : Module R N₁
inst_8 : Module R N₂
inst_9 : Module.{u_1, u_4} (Localization (M := R) M) N₁
inst_10 : Module.{u_1, u_5} (Localization (M := R) M) N₂
inst_11 : IsScalarTower R (Localization (M := R) M) N₁
inst_12 : IsScalarTower R (Localization (M := R) M) N₂
⊢ LinearMap.CompatibleSMul N₁ N₂ (Localization (M := R) M) R

Tactic:
linearMap_compatibleSMul M ..

Premises used: IsLocalization.linearMap_compatibleSMul
-- Module: Mathlib.RingTheory.Localization.Basic
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
inst_5 : Algebra R P
f g : S →ₐ[R] P
rw :
  Eq (α := R →+* P) (algebraMap R P)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))
rw₁ rw₂ : Eq (α := R →+* P) (algebraMap R P) (algebraMap R P)
⊢ Eq (α := R →+* P) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : S →+* P) (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑g : S →+* P) (algebraMap R S))

Tactic:
rw [f.comp_algebraMap, g.comp_algebraMap]

Premises used: AlgHom.comp_algebraMap
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
x : R
y : ↥M
⊢ (algEquiv M S Q : (a : S) → Q) (mk' S x y) = mk' Q x y

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
x : R
y : ↥M
⊢ (AlgEquiv.symm (algEquiv M S Q) : (a : Q) → S) (mk' Q x y) = mk' S x y

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
h :
  Eq (α := R →+* Q) (f.comp (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
⊢ f = (↑(algEquiv M S Q) : S →+* Q)

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
h :
  Eq (α := R →+* Q) (algebraMap R Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))
⊢ Eq (α := R →+* Q) (f.comp (algebraMap R S))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))

Tactic:
rw [hf]
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
h :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := Q) ((algebraMap R Q : (a : R) → Q) x : Q)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S) :
            (a : R) → Q)
          x :
        Q)
⊢ Eq (α := R →+* Q) (algebraMap R Q)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S))

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.Basic
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
Q : Type u_4
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
f : S →+* Q
hf : Eq (α := R →+* Q) (f.comp (algebraMap R S)) (algebraMap R Q)
x : R
⊢ Eq.{u_4 + 1} (α := Q) ((algebraMap R Q : (a : R) → Q) x : Q)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(algEquiv M S Q) : S →+* Q) (algebraMap R S) : (a : R) → Q)
        x :
      Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
P : Type u_7
inst_12 : CommSemiring P
inst_13 : Algebra A P
inst_14 : IsLocalization M S
f : R →ₐ[A] P
hf : ∀ (y : ↥M), IsUnit.{u_7} (M := P) ((f : (a : R) → P) (↑y : R) : P)
x : S
r : A
⊢ Eq.{u_7 + 1} (α := P) ((lift hf : (a : S) → P) ((algebraMap A S : (a : A) → S) r : S) : P)
    ((algebraMap A P : (a : A) → P) r : P)

Tactic:
simp [IsScalarTower.algebraMap_apply A R S]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
P : Type u_7
inst_7 : CommSemiring P
inst_8 : Algebra A P
inst_9 : IsLocalization M S
f : R →ₐ[A] P
hf : ∀ (y : ↥M), IsUnit.{u_7} (M := P) ((f : (a : R) → P) (↑y : R) : P)
⊢ Eq (α := S →+* P) (AlgHom.toRingHom (liftAlgHom hf)) (lift hf)

Tactic:
rfl

Premises used: IsLocalization.lift, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
P : Type u_7
inst_7 : CommSemiring P
inst_8 : Algebra A P
inst_9 : IsLocalization M S
f : R →ₐ[A] P
hf : ∀ (y : ↥M), IsUnit.{u_7} (M := P) ((f : (a : R) → P) (↑y : R) : P)
⊢ Eq (α := (a : S) → P) (⇑(liftAlgHom hf) : (a : S) → P) (⇑(lift hf) : (a : S) → P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
P : Type u_7
inst_7 : CommSemiring P
inst_8 : Algebra A P
inst_9 : IsLocalization M S
f : R →ₐ[A] P
hf : ∀ (y : ↥M), IsUnit.{u_7} (M := P) ((f : (a : R) → P) (↑y : R) : P)
x : S
⊢ Eq.{u_7 + 1} (α := P) ((liftAlgHom hf : (a : S) → P) x : P) ((lift hf : (a : S) → P) x : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
dsimp :
  Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
⊢ (RingEquiv.toEquiv (ringEquivOfRingEquiv S Q h.toRingEquiv H)).toFun ((algebraMap A S : (a : A) → S) x) =
    (algebraMap A Q : (a : A) → Q) x

Tactic:
dsimp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : A
rw :
  Eq.{u_8 + 1} (α := Q)
    ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q)
        ((algebraMap R S : (a : R) → S) ((algebraMap A R : (a : A) → R) x : R) : S) :
      Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₁ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) (((↑h : R →+* P) : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₂ :
  Eq.{u_8 + 1} (α := Q)
    ((algebraMap P Q : (a : P) → Q) ((h : (a : R) → P) ((algebraMap A R : (a : A) → R) x : R) : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₃ :
  Eq.{u_8 + 1} (α := Q) ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)
rw₄ rw₅ :
  Eq.{u_8 + 1} (α := Q) ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
    ((algebraMap P Q : (a : P) → Q) ((algebraMap A P : (a : A) → P) x : P) : Q)
⊢ Eq.{u_8 + 1} (α := Q) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((algebraMap A S : (a : A) → S) x : S) : Q)
    ((algebraMap A Q : (a : A) → Q) x : Q)

Tactic:
rw [IsScalarTower.algebraMap_apply A R S, map_eq,
    RingHom.coe_coe, AlgEquiv.commutes, IsScalarTower.algebraMap_apply A P Q]

Premises used: RingHom.coe_coe, AlgEquiv.commutes, IsLocalization.map_eq, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
inst_7 : IsLocalization M S
P : Type u_7
inst_8 : CommSemiring P
inst_9 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_10 : CommSemiring Q
inst_11 : Algebra A Q
inst_12 : Algebra P Q
inst_13 : IsScalarTower A P Q
inst_14 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ Eq (α := S →+* Q) (↑(algEquivOfAlgEquiv S Q h H) : S →+* Q) (map Q (↑h : R →+* P) ⋯)

Tactic:
rfl

Premises used: IsLocalization.map, MonoidHomClass.toMonoidHom, IsLocalization.lift, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
inst_7 : IsLocalization M S
P : Type u_7
inst_8 : CommSemiring P
inst_9 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_10 : CommSemiring Q
inst_11 : Algebra A Q
inst_12 : Algebra P Q
inst_13 : IsScalarTower A P Q
inst_14 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : R
⊢ Eq.{u_8 + 1} (α := Q) ((algEquivOfAlgEquiv S Q h H : (a : S) → Q) ((algebraMap R S : (a : R) → S) x : S) : Q)
    ((algebraMap P Q : (a : P) → Q) ((h : (a : R) → P) x : P) : Q)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
inst_7 : IsLocalization M S
P : Type u_7
inst_8 : CommSemiring P
inst_9 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_10 : CommSemiring Q
inst_11 : Algebra A Q
inst_12 : Algebra P Q
inst_13 : IsScalarTower A P Q
inst_14 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
x : R
y : ↥M
⊢ (algEquivOfAlgEquiv S Q h H : (a : S) → Q) (mk' S x y) =
    mk'.{u_7, u_8} (R := P) (M := T) Q ((h : (a : R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((h : (a : R) → P) (↑y : R)) ⋯ : ↥T)

Tactic:
simp [map_mk']

Premises used: IsLocalization.map_mk'
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M_1 N : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
P_1 : Type u_3
inst_3 : CommSemiring P_1
inst_4 : IsLocalization M_1 S_1
g : R_1 →+* P_1
hg : ∀ (y : ↥M_1), IsUnit.{u_3} (M := P_1) ((g : (a : R_1) → P_1) (↑y : R_1) : P_1)
A : Type u_4
inst_5 : CommSemiring A
R : Type u_5
inst_6 : CommSemiring R
inst_7 : Algebra A R
M : Submonoid R
S : Type u_6
inst_8 : CommSemiring S
inst_9 : Algebra A S
inst_10 : Algebra R S
inst_11 : IsScalarTower A R S
inst_12 : IsLocalization M S
P : Type u_7
inst_13 : CommSemiring P
inst_14 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_15 : CommSemiring Q
inst_16 : Algebra A Q
inst_17 : Algebra P Q
inst_18 : IsScalarTower A P Q
inst_19 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
rw : Submonoid.map h.symm (Submonoid.map h M) = M
rw₁ : Submonoid.map (F := P ≃* R) (↑h.symm : P ≃* R) (Submonoid.map h M) = M
rw₂ : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑h : R ≃* P)) (Submonoid.map h M) = M
rw₃ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map h M) = M
rw₄ : Submonoid.comap (F := R ≃* P) (↑h : R ≃* P) (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) = M
rw₅ rw₆ : M = M
⊢ Submonoid.map h.symm T = M

Tactic:
rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv,
        ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
        Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]

Premises used: Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv, Submonoid.comap_map_eq_of_injective, Submonoid.comap_equiv_eq_map_symm, MulEquivClass.toMulEquiv, MulEquiv.injective
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
A : Type u_4
inst : CommSemiring A
R : Type u_5
inst_1 : CommSemiring R
inst_2 : Algebra A R
M : Submonoid R
S : Type u_6
inst_3 : CommSemiring S
inst_4 : Algebra A S
inst_5 : Algebra R S
inst_6 : IsScalarTower A R S
inst_7 : IsLocalization M S
P : Type u_7
inst_8 : CommSemiring P
inst_9 : Algebra A P
T : Submonoid P
Q : Type u_8
inst_10 : CommSemiring Q
inst_11 : Algebra A Q
inst_12 : Algebra P Q
inst_13 : IsScalarTower A P Q
inst_14 : IsLocalization T Q
h : R ≃ₐ[A] P
H : Submonoid.map h M = T
⊢ Eq (α := Q ≃ₐ[A] S) (AlgEquiv.symm (algEquivOfAlgEquiv S Q h H)) (algEquivOfAlgEquiv (M := T) Q (T := M) S h.symm ⋯)

Tactic:
rfl

Premises used: AlgEquiv.symm, IsLocalization.algEquivOfAlgEquiv, Equiv.symm, rfl
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
⊢ s • x ∈ N' ↔ x ∈ N'

Tactic:
⟨fun h ↦ ?_, fun h ↦ Submodule.smul_of_tower_mem N' s h⟩

Premises used: Iff.intro, Submodule.smul_of_tower_mem
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
refine : ∀ (h : s • x ∈ N'), x ∈ N'
⊢ s • x ∈ N' ↔ x ∈ N'

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Submodule.smul_of_tower_mem N' s h⟩
-- Module: Mathlib.RingTheory.Localization.Basic
Goal:
R : Type u_4
inst : CommSemiring R
S : Submonoid R
R' : Type u_5
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
inst_3 : IsLocalization S R'
M' : Type u_6
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : IsScalarTower R R' M'
N' : Submodule R' M'
x : M'
s : ↥S
h : s • x ∈ N'
rwa : HSMul.hSMul.{u_5, u_6, u_6} (α := R') ((algebraMap R R' : (a : R) → R') (↑s : R) : R') x ∈ N'
rwa₁ rwa₂ rwa₃ rwa₄ : (↑s : R) • x ∈ N'
⊢ x ∈ N'

Tactic:
rwa [← Submodule.smul_mem_iff_of_isUnit (r := algebraMap R R' s) N' (map_units R' s),
    algebraMap_smul]

Premises used: algebraMap_smul, Submodule.smul_mem_iff_of_isUnit, IsLocalization.map_units