awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Defs
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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j.toMonoidHom M = T
x : R
y : ↥M
⊢ (ringEquivOfRingEquiv S Q j H : (a : S) → Q) (mk' S x y) =
    mk'.{u_3, u_4} (R := P) (M := T) Q ((j : (a : R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((j : (a : R) → P) (↑y : R)) ⋯ : ↥T)

Tactic:
simp [map_mk']

Premises used: IsLocalization.map_mk'
-- Module: Mathlib.RingTheory.Localization.Defs
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
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j M = T
rw : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) (Submonoid.map j M) = M
rw₁ : Submonoid.comap (F := R ≃* P) (↑j : R ≃* P) (Submonoid.map j M) = M
rw₂ : Submonoid.comap (F := R ≃* P) (↑j : R ≃* P) (Submonoid.map (F := R ≃* P) (↑j : R ≃* P) M) = M
rw₃ rw₄ : M = M
⊢ Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) T = M

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

Premises used: Submonoid.map_coe_toMulEquiv, Submonoid.comap_map_eq_of_injective, Submonoid.comap_equiv_eq_map_symm, MulEquivClass.toMulEquiv, MulEquiv.injective
-- Module: Mathlib.RingTheory.Localization.Defs
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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j M = T
⊢ Eq (α := Q ≃+* S) (RingEquiv.symm (ringEquivOfRingEquiv S Q j H))
    (ringEquivOfRingEquiv (M := T) Q (T := M) S j.symm ⋯)

Tactic:
rfl

Premises used: IsLocalization.ringEquivOfRingEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
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
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
h : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑g : (a : R) → P)
inst_7 : IsLocalization (Submonoid.map g M) Q
⊢ Injective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map Q g ⋯) : (a : S) → Q)

Tactic:
(toLocalizationMap M S).map_injective_of_injective h (toLocalizationMap (M.map g) Q)

Premises used: Submonoid.LocalizationMap.map_injective_of_injective, Submonoid.map, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
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
g : R →+* P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
h : Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑g : (a : R) → P)
inst_7 : IsLocalization (Submonoid.map g M) Q
⊢ Surjective.{u_2 + 1, u_4 + 1} (α := S) (β := Q) (⇑(map Q g ⋯) : (a : S) → Q)

Tactic:
(toLocalizationMap M S).map_surjective_of_surjective h (toLocalizationMap (M.map g) Q)

Premises used: Submonoid.LocalizationMap.map_surjective_of_surjective, Submonoid.map, IsLocalization.toLocalizationMap
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
toIsLocalizationMap :
  Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)
⊢ IsLocalization (Submonoid.map h M) S

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
toIsLocalizationMap : ∀ (y : ↥(Submonoid.map h M)), IsUnit.{u_2} (M := S) ((algebraMap P S : (a : P) → S) (↑y : P) : S)
toIsLocalizationMap₁ :
  ∀ (z : S),
    ∃ (x : P × ↥(Submonoid.map h M)),
      HMul.hMul (β := S) z ((algebraMap P S : (a : P) → S) (↑x.2 : P) : S) = (algebraMap P S : (a : P) → S) x.1
toIsLocalizationMap₂ :
  ∀ {x y : P},
    Eq.{u_2 + 1} (α := S) ((algebraMap P S : (a : P) → S) x : S) ((algebraMap P S : (a : P) → S) y : S) →
      ∃ (c : ↥(Submonoid.map h M)), (↑c : P) * x = (↑c : P) * y
⊢ Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : R
hy : y ∈ (↑M : Set R)
⊢ IsUnit.{u_2} (M := S) ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) : S)

Tactic:
IsLocalization.map_units S ⟨y, hy⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : R
hy : y ∈ (↑M : Set R)
h₁ :
  Eq.{u_2 + 1} (α := S)
    ((algebraMap P S : (a : P) → S)
        ((↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
                ((h : (a : R) → P) y) ⋯) :
            P) :
          P) :
      S)
    ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) : S)
⊢ IsUnit.{u_2} (M := S)
    ((algebraMap P S : (a : P) → S)
        ((↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
                ((h : (a : R) → P) y) ⋯) :
            P) :
          P) :
      S)

Tactic:
convert! IsLocalization.map_units S ⟨y, hy⟩

Premises used: Subtype.mk, IsLocalization.map_units
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : R
hy : y ∈ (↑M : Set R)
h₁ :
  Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) y : P) : R) : S)
    ((algebraMap R S : (a : R) → S) y : S)
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap P S : (a : P) → S)
        ((↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
                ((h : (a : R) → P) y) ⋯) :
            P) :
          P) :
      S)
    ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) : S)

Tactic:
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]

Premises used: RingHom.comp_apply, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : R
hy : y ∈ (↑M : Set R)
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) y : P) : R) : S)
    ((algebraMap R S : (a : R) → S) y : S)

Tactic:
congr_arg _ (h.symm_apply_apply _)

Premises used: RingEquiv.symm_apply_apply, congr_arg
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : R
hy : y ∈ (↑M : Set R)
⊢ Eq.{u_2 + 1} (α := S)
    ((algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) y : P) : R) : S)
    ((algebraMap R S : (a : R) → S) y : S)

Tactic:
exact congr_arg _ (h.symm_apply_apply _)

Premises used: RingEquiv.symm_apply_apply, congr_arg
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
toIsLocalizationMap :
  ∀ (x : R) (s : ↥M)
    (e :
      HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) =
        (algebraMap R S : (a : R) → S) (x, s).1),
    ∃ (x : P × ↥(Submonoid.map h M)),
      HMul.hMul (β := S) y ((algebraMap P S : (a : P) → S) (↑x.2 : P) : S) = (algebraMap P S : (a : P) → S) x.1
⊢ ∃ (x : P × ↥(Submonoid.map h M)),
    HMul.hMul (β := S) y ((algebraMap P S : (a : P) → S) (↑x.2 : P) : S) = (algebraMap P S : (a : P) → S) x.1

Tactic:
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y

Premises used: IsLocalization.surj
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
⊢ ∃ (x : P × ↥(Submonoid.map h M)),
    HMul.hMul (β := S) y ((algebraMap P S : (a : P) → S) (↑x.2 : P) : S) = (algebraMap P S : (a : P) → S) x.1

Tactic:
⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩

Premises used: Prod.mk, Subtype.mk, Subtype.prop, And.intro, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
toIsLocalizationMap :
  HMul.hMul (β := S) y
      ((algebraMap P S : (a : P) → S)
          ((↑((h : (a : R) → P) x,
                    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
                      ((h : (a : R) → P) (↑s : R)) ⋯).2 :
              P) :
            P) :
        S) =
    (algebraMap P S : (a : P) → S)
      (((h : (a : R) → P) x,
            Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
              ((h : (a : R) → P) (↑s : R)) ⋯).1 :
        P)
⊢ ∃ (x : P × ↥(Submonoid.map h M)),
    HMul.hMul (β := S) y ((algebraMap P S : (a : P) → S) (↑x.2 : P) : S) = (algebraMap P S : (a : P) → S) x.1

Tactic:
refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑(x, s).2 : R) : S) = (algebraMap R S : (a : R) → S) (x, s).1
toIsLocalizationMap :
  HMul.hMul (β := S) y
      ((algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) : R) : S) =
    (algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) : R)
⊢ HMul.hMul (β := S) y
      ((algebraMap P S : (a : P) → S)
          ((↑((h : (a : R) → P) x,
                    Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
                      ((h : (a : R) → P) (↑s : R)) ⋯).2 :
              P) :
            P) :
        S) =
    (algebraMap P S : (a : P) → S)
      (((h : (a : R) → P) x,
            Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := Submonoid P) (Submonoid.map h M) x)
              ((h : (a : R) → P) (↑s : R)) ⋯).1 :
        P)

Tactic:
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢

Premises used: RingHom.comp_apply, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
⊢ HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x

Tactic:
e
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
h₁ : (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) = (↑s : R)
h₂ : (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) = x
⊢ HMul.hMul (β := S) y
      ((algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) : R) : S) =
    (algebraMap R S : (a : R) → S) ((h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) : R)

Tactic:
convert! e
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
⊢ (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) = (↑s : R)

Tactic:
h.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
⊢ (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) = (↑s : R)

Tactic:
exact h.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
⊢ (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) = x

Tactic:
h.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
x : R
s : ↥M
e : HMul.hMul (β := S) y ((algebraMap R S : (a : R) → S) (↑s : R) : S) = (algebraMap R S : (a : R) → S) x
⊢ (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) = x

Tactic:
exact h.symm_apply_apply _

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
x y : P
toIsLocalizationMap :
  (∃ (c : ↥M),
      HMul.hMul (β := R) (↑c : R) ((h.symm.toRingHom : (a : P) → R) x : R) =
        HMul.hMul (β := R) (↑c : R) ((h.symm.toRingHom : (a : P) → R) y : R)) →
    ∃ (c : ↥(Submonoid.map h M)), (↑c : P) * x = (↑c : P) * y
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap P S : (a : P) → S) x : S) ((algebraMap P S : (a : P) → S) y : S) →
    ∃ (c : ↥(Submonoid.map h M)), (↑c : P) * x = (↑c : P) * y

Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply,
      IsLocalization.eq_iff_exists M S]

Premises used: RingHom.comp_apply, RingHom.algebraMap_toAlgebra, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
x y : P
⊢ (∃ (c : ↥M),
      HMul.hMul (β := R) (↑c : R) ((h.symm.toRingHom : (a : P) → R) x : R) =
        HMul.hMul (β := R) (↑c : R) ((h.symm.toRingHom : (a : P) → R) y : R)) →
    ∃ (c : ↥(Submonoid.map h M)), (↑c : P) * x = (↑c : P) * y

Tactic:
simp [← h.toEquiv.apply_eq_iff_eq]

Premises used: RingEquiv.toEquiv, Equiv.apply_eq_iff_eq
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S

Tactic:
⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩

Premises used: IsLocalization.isLocalization_of_base_ringEquiv, Iff.intro
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
refine : IsLocalization (Submonoid.map h M) S → IsLocalization M S
⊢ IsLocalization M S ↔ IsLocalization (Submonoid.map h M) S

Tactic:
refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
⊢ IsLocalization (Submonoid.map h.symm (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M)) S

Tactic:
isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm

Premises used: Submonoid.map, IsLocalization.isLocalization_of_base_ringEquiv, MulEquivClass.toMulEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
h₁ : M = Submonoid.map h.symm (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M)
h₂ : inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap P S) h.symm.symm.toRingHom)
⊢ IsLocalization M S

Tactic:
convert! isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm

Premises used: Submonoid.map, IsLocalization.isLocalization_of_base_ringEquiv, MulEquivClass.toMulEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
h₁ : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑(↑h : R ≃* P) : (a : R) → P)
⊢ M = Submonoid.map h.symm (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M)

Tactic:
rw [← Submonoid.map_coe_toMulEquiv, RingEquiv.coe_toMulEquiv_symm, ←
      Submonoid.comap_equiv_eq_map_symm, Submonoid.comap_map_eq_of_injective]

Premises used: Submonoid.map_coe_toMulEquiv, Submonoid.comap_map_eq_of_injective, Submonoid.comap_equiv_eq_map_symm, RingEquiv.coe_toMulEquiv_symm
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
⊢ Injective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑(↑h : R ≃* P) : (a : R) → P)

Tactic:
h.toEquiv.injective

Premises used: RingEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
⊢ Injective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑(↑h : R ≃* P) : (a : R) → P)

Tactic:
exact h.toEquiv.injective

Premises used: RingEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.RingTheory.Localization.Defs
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
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
H : IsLocalization (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M) S
h₁ : inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap R S) (h.symm.toRingHom.comp h.symm.symm.toRingHom))
⊢ inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap P S) h.symm.symm.toRingHom)

Tactic:
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]

Premises used: RingHom.comp_assoc, RingHom.algebraMap_toAlgebra