awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
h :
  ∀ (x : S),
    Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯)) x ↔
      Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) x
⊢ Eq (α := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯))
    (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : S
h :
  ∀ (x : R) (s : ↥M),
    Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯)) (mk' S x s) ↔
      Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) (mk' S x s)
⊢ Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯)) x ↔
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq M x

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
x : R
s : ↥M
⊢ Membership.mem (γ := Ideal S) (RingHom.ker (F := S →+* Q) (map (M := M) (T := T) Q g ⋯)) (mk' S x s) ↔
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) (RingHom.ker g)) (mk' S x s)

Tactic:
simp [RingHom.mem_ker, IsLocalization.map_mk', IsLocalization.mk'_eq_zero_iff,
    IsLocalization.mk'_mem_map_algebraMap_iff, ← hT]

Premises used: IsLocalization.map_mk', RingHom.mem_ker, IsLocalization.mk'_mem_map_algebraMap_iff, IsLocalization.mk'_eq_zero_iff
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
x : ↥(ker g)
⊢ Membership.mem (α := S) (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy))
    ((algebraMap R S : (a : R) → S) (↑x : R) : S)

Tactic:
simp [RingHom.mem_ker, RingHom.mem_ker.mp x.property]

Premises used: RingHom.mem_ker, Iff.mp, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
x y : ↥(ker g)
⊢ Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy)) x)
      ((algebraMap R S : (a : R) → S) (↑(x + y) : R)) ⋯ =
    HAdd.hAdd (α := ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy))) (β :=
      ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy)))
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy)) x)
          ((algebraMap R S : (a : R) → S) (↑x : R)) ⋯ :
        ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy)))
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy)) x)
          ((algebraMap R S : (a : R) → S) (↑y : R)) ⋯ :
        ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy)))

Tactic:
simp only [Submodule.coe_add, map_add, AddMemClass.mk_add_mk]

Premises used: Submodule.coe_add, map_add, AddMemClass.mk_add_mk
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
a : R
x : ↥(ker g)
⊢ Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy)) x)
      ((algebraMap R S : (a : R) → S) (↑(a • x) : R)) ⋯ =
    HSMul.hSMul (α := R) (β := ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy))) ((id R : (a : R) → R) a : R)
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Ideal S) (ker (F := S →+* Q) (IsLocalization.map Q g hy)) x)
          ((algebraMap R S : (a : R) → S) (↑x : R)) ⋯ :
        ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy)))

Tactic:
simp only [SetLike.val_smul, smul_eq_mul, map_mul, id_apply, SetLike.mk_smul_of_tower_mk,
      Algebra.smul_def]

Premises used: RingHom.id_apply, map_mul, SetLike.val_smul, SetLike.mk_smul_of_tower_mk, Algebra.smul_def, smul_eq_mul
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hy : M ≤ Submonoid.comap g T
r : ↥(ker g)
⊢ Eq.{u_2 + 1} (α := S)
    ((↑(((toKerIsLocalization S Q g hy :
                LinearMap.{u_1, u_1, u_1, u_2} (id R) ↥(ker g) ↥(ker (F := S →+* Q) (IsLocalization.map Q g hy))) :
              (a : ↥(ker g)) → ↥(ker (IsLocalization.map Q g hy)))
            r) :
        S) :
      S)
    ((algebraMap R S : (a : R) → S) (↑r : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (F := R →+* S) (algebraMap R S) (ker g)) ≃ₛₗ[id S]
  ↥(ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (F := R →+* S) (algebraMap R S) (ker g))
    (ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) ⋯
convert_to :
  IsLocalizedModule M
    ((↑(LinearEquiv.restrictScalars R e) :
        ↥(Ideal.map (algebraMap R S) (ker g)) →ₛₗ[id R] ↥(ker (IsLocalization.map Q g ⋯))) ∘ₗ
      Algebra.idealMap S (ker g))
⊢ IsLocalizedModule (M' := ↥(ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯))) M
    (toKerIsLocalization S Q g ⋯)

Tactic:
convert_to IsLocalizedModule M ((e.restrictScalars R).toLinearMap ∘ₗ
    Algebra.idealMap S (RingHom.ker g))

Premises used: LinearEquiv.restrictScalars, IsLocalizedModule, Algebra.idealMap, LinearMap.comp, LinearEquiv.toLinearMap, RingHom.ker
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M : Submonoid R
T : Submonoid P
inst_4 : Algebra R S
inst_5 : Algebra P Q
inst_6 : IsLocalization M S
inst_7 : IsLocalization T Q
g : R →+* P
hT : Submonoid.map g M = T
e : ↥(Ideal.map (F := R →+* S) (algebraMap R S) (ker g)) ≃ₛₗ[id S]
  ↥(ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) :=
  LinearEquiv.ofEq (Ideal.map (F := R →+* S) (algebraMap R S) (ker g))
    (ker (F := S →+* Q) (IsLocalization.map (M := M) (T := T) Q g ⋯)) ⋯
⊢ IsLocalizedModule M
    ((↑(LinearEquiv.restrictScalars R e) :
        ↥(Ideal.map (algebraMap R S) (ker g)) →ₛₗ[id R] ↥(ker (IsLocalization.map Q g ⋯))) ∘ₗ
      Algebra.idealMap S (ker g))

Tactic:
apply IsLocalizedModule.of_linearEquiv

Premises used: IsLocalizedModule.of_linearEquiv
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R_1 : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M_1 : Submonoid R_1
T : Submonoid P
inst_4 : Algebra R_1 S
inst_5 : Algebra P Q
inst_6 : IsLocalization M_1 S
inst_7 : IsLocalization T Q
g : R_1 →+* P
R : Type u_5
inst_8 : CommSemiring R
M : Submonoid R
A : Type u_6
inst_9 : CommSemiring A
inst_10 : Algebra R A
B : Type u_7
inst_11 : CommSemiring B
inst_12 : Algebra R B
Rₚ : Type u_8
inst_13 : CommSemiring Rₚ
inst_14 : Algebra R Rₚ
inst_15 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_16 : CommSemiring Aₚ
inst_17 : Algebra R Aₚ
inst_18 : Algebra A Aₚ
inst_19 : IsScalarTower R A Aₚ
inst_20 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_21 : CommSemiring Bₚ
inst_22 : Algebra R Bₚ
inst_23 : Algebra B Bₚ
inst_24 : IsScalarTower R B Bₚ
inst_25 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_26 : Algebra Rₚ Aₚ
inst_27 : Algebra Rₚ Bₚ
inst_28 : IsScalarTower R Rₚ Aₚ
inst_29 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
rw : IsLocalization (algebraMapSubmonoid B M) Bₚ
⊢ IsLocalization (Submonoid.map f.toRingHom (algebraMapSubmonoid A M)) Bₚ

Tactic:
rw [AlgHom.toRingHom_eq_coe, ← Submonoid.map_coe_toMonoidHom, AlgHom.toRingHom_toMonoidHom,
    Submonoid.map_coe_toMonoidHom, algebraMapSubmonoid_map_eq M f]

Premises used: Algebra.algebraMapSubmonoid_map_eq, AlgHom.toRingHom_eq_coe, AlgHom.toRingHom_toMonoidHom, Submonoid.map_coe_toMonoidHom
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R_1 : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M_1 : Submonoid R_1
T : Submonoid P
inst_4 : Algebra R_1 S
inst_5 : Algebra P Q
inst_6 : IsLocalization M_1 S
inst_7 : IsLocalization T Q
g : R_1 →+* P
R : Type u_5
inst_8 : CommSemiring R
M : Submonoid R
A : Type u_6
inst_9 : CommSemiring A
inst_10 : Algebra R A
B : Type u_7
inst_11 : CommSemiring B
inst_12 : Algebra R B
Rₚ : Type u_8
inst_13 : CommSemiring Rₚ
inst_14 : Algebra R Rₚ
inst_15 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_16 : CommSemiring Aₚ
inst_17 : Algebra R Aₚ
inst_18 : Algebra A Aₚ
inst_19 : IsScalarTower R A Aₚ
inst_20 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_21 : CommSemiring Bₚ
inst_22 : Algebra R Bₚ
inst_23 : Algebra B Bₚ
inst_24 : IsScalarTower R B Bₚ
inst_25 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_26 : Algebra Rₚ Aₚ
inst_27 : Algebra Rₚ Bₚ
inst_28 : IsScalarTower R Rₚ Aₚ
inst_29 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ IsLocalization (algebraMapSubmonoid B M) Bₚ

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R_1 : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M_1 : Submonoid R_1
T : Submonoid P
inst_4 : Algebra R_1 S
inst_5 : Algebra P Q
inst_6 : IsLocalization M_1 S
inst_7 : IsLocalization T Q
g : R_1 →+* P
R : Type u_5
inst_8 : CommSemiring R
M : Submonoid R
A : Type u_6
inst_9 : CommSemiring A
inst_10 : Algebra R A
B : Type u_7
inst_11 : CommSemiring B
inst_12 : Algebra R B
Rₚ : Type u_8
inst_13 : CommSemiring Rₚ
inst_14 : Algebra R Rₚ
inst_15 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_16 : CommSemiring Aₚ
inst_17 : Algebra R Aₚ
inst_18 : Algebra A Aₚ
inst_19 : IsScalarTower R A Aₚ
inst_20 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_21 : CommSemiring Bₚ
inst_22 : Algebra R Bₚ
inst_23 : Algebra B Bₚ
inst_24 : IsScalarTower R B Bₚ
inst_25 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_26 : Algebra Rₚ Aₚ
inst_27 : Algebra Rₚ Bₚ
inst_28 : IsScalarTower R Rₚ Aₚ
inst_29 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
r : Rₚ
obtain :
  ∀ (a : R) (m : ↥M),
    OneHom.toFun.{u_9, u_10} (M := Aₚ) ((↑(↑(map Bₚ f.toRingHom ⋯) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) : OneHom Aₚ Bₚ)
        ((algebraMap Rₚ Aₚ : (a : Rₚ) → Aₚ) (mk' Rₚ a m) : Aₚ) =
      (algebraMap Rₚ Bₚ : (a : Rₚ) → Bₚ) (mk' Rₚ a m)
⊢ OneHom.toFun.{u_9, u_10} (M := Aₚ) ((↑(↑(map Bₚ f.toRingHom ⋯) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) : OneHom Aₚ Bₚ)
      ((algebraMap Rₚ Aₚ : (a : Rₚ) → Aₚ) r : Aₚ) =
    (algebraMap Rₚ Bₚ : (a : Rₚ) → Bₚ) r

Tactic:
obtain ⟨a, m, rfl⟩ := IsLocalization.exists_mk'_eq M r

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R_1 : Type u_1
S : Type u_2
P : Type u_3
Q : Type u_4
inst : CommSemiring R_1
inst_1 : CommSemiring S
inst_2 : CommSemiring P
inst_3 : CommSemiring Q
M_1 : Submonoid R_1
T : Submonoid P
inst_4 : Algebra R_1 S
inst_5 : Algebra P Q
inst_6 : IsLocalization M_1 S
inst_7 : IsLocalization T Q
g : R_1 →+* P
R : Type u_5
inst_8 : CommSemiring R
M : Submonoid R
A : Type u_6
inst_9 : CommSemiring A
inst_10 : Algebra R A
B : Type u_7
inst_11 : CommSemiring B
inst_12 : Algebra R B
Rₚ : Type u_8
inst_13 : CommSemiring Rₚ
inst_14 : Algebra R Rₚ
inst_15 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_16 : CommSemiring Aₚ
inst_17 : Algebra R Aₚ
inst_18 : Algebra A Aₚ
inst_19 : IsScalarTower R A Aₚ
inst_20 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_21 : CommSemiring Bₚ
inst_22 : Algebra R Bₚ
inst_23 : Algebra B Bₚ
inst_24 : IsScalarTower R B Bₚ
inst_25 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_26 : Algebra Rₚ Aₚ
inst_27 : Algebra Rₚ Bₚ
inst_28 : IsScalarTower R Rₚ Aₚ
inst_29 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
a : R
m : ↥M
⊢ OneHom.toFun.{u_9, u_10} (M := Aₚ) ((↑(↑(map Bₚ f.toRingHom ⋯) : Aₚ →* Bₚ) : OneHom Aₚ Bₚ) : OneHom Aₚ Bₚ)
      ((algebraMap Rₚ Aₚ : (a : Rₚ) → Aₚ) (mk' Rₚ a m) : Aₚ) =
    (algebraMap Rₚ Bₚ : (a : Rₚ) → Bₚ) (mk' Rₚ a m)

Tactic:
simp [algebraMap_mk' (S := A), algebraMap_mk' (S := B), map_mk']

Premises used: IsLocalization.map_mk', IsLocalization.algebraMap_mk'
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ Eq (α := (a : Aₚ) → Bₚ) (⇑(mapₐ M Rₚ Aₚ Bₚ f) : (a : Aₚ) → Bₚ) (⇑(map Bₚ f.toRingHom ⋯) : (a : Aₚ) → Bₚ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
hf : Function.Injective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Injective.{u_9 + 1, u_10 + 1} (α := Aₚ) (β := Bₚ) (⇑(mapₐ M Rₚ Aₚ Bₚ f) : (a : Aₚ) → Bₚ)

Tactic:
IsLocalization.map_injective_of_injective _ _ _ hf

Premises used: IsLocalization.map_injective_of_injective
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
hf : Function.Surjective.{u_6 + 1, u_7 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Function.Surjective.{u_9 + 1, u_10 + 1} (α := Aₚ) (β := Bₚ) (⇑(mapₐ M Rₚ Aₚ Bₚ f) : (a : Aₚ) → Bₚ)

Tactic:
IsLocalization.map_surjective_of_surjective _ _ _ hf

Premises used: IsLocalization.map_surjective_of_surjective
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ Eq (α := Aₚ →ₗ[Rₚ] Bₚ)
    (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap :
      Aₚ →ₗ[Rₚ] Bₚ)
    (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f) : Aₚ →ₗ[Rₚ] Bₚ)

Tactic:
LinearMap.restrictScalars_injective R ?_

Premises used: LinearMap.restrictScalars_injective
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
refine :
  Eq (α := Aₚ →ₗ[R] Bₚ)
    ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := Rₚ)
      (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap))
    ((↑R :
        {S : Type u_8} →
          {M : Type u_9} →
            {M₂ : Type u_10} →
              [inst : Semiring R] →
                [inst_22 : Semiring S] →
                  [inst_23 : AddCommMonoid M] →
                    [inst_24 : AddCommMonoid M₂] →
                      [inst_25 : Module R M] →
                        [inst_26 : Module R M₂] →
                          [inst_27 : Module S M] →
                            [inst_28 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)))
⊢ Eq (α := Aₚ →ₗ[Rₚ] Bₚ)
    (((IsLocalizedModule.mapExtendScalars M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
              (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) Rₚ :
            (A →ₗ[R] B) →ₗ[R] Aₚ →ₗ[Rₚ] Bₚ) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[Rₚ] Bₚ)
        f.toLinearMap :
      Aₚ →ₗ[Rₚ] Bₚ)
    (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f) : Aₚ →ₗ[Rₚ] Bₚ)

Tactic:
refine LinearMap.restrictScalars_injective R ?_

Premises used: LinearMap.restrictScalars_injective
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
x : A
⊢ Eq.{u_10 + 1} (α := Bₚ)
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ) : (a : B) → Bₚ) ((f.toLinearMap : (a : A) → B) x : B) : Bₚ)
    (((↑R :
                {S : Type u_8} →
                  {M : Type u_9} →
                    {M₂ : Type u_10} →
                      [inst : Semiring R] →
                        [inst_22 : Semiring S] →
                          [inst_23 : AddCommMonoid M] →
                            [inst_24 : AddCommMonoid M₂] →
                              [inst_25 : Module R M] →
                                [inst_26 : Module R M₂] →
                                  [inst_27 : Module S M] →
                                    [inst_28 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)) ∘ₗ
            AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ) :
          (a : A) → Bₚ)
        x :
      Bₚ)

Tactic:
simp