awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ Eq (α := Submonoid R) (Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M)
    (Submonoid.map (F := R →* R) (MonoidHom.id R) M)
have e_f : h.symm.toMonoidHom.comp h.toMonoidHom = MonoidHom.id R
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
⊢ h.symm.toMonoidHom.comp h.toMonoidHom = MonoidHom.id R
have e_f : ∀ (x : R),
  Eq (α := R) ((h.symm.toMonoidHom.comp h.toMonoidHom : (a : R) → R) x : R) ((MonoidHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ (map S (↑h.symm : P →+* R) ⋯ : (a : Q) → S) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) x : Q) = x
have rw : ∀ (x : R),
  Eq (α := S) ((RingHom.id S : (a : S) → S) ((algebraMap R S : (a : R) → S) x : S) : S)
    ((algebraMap R S : (a : R) → S)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑h.symm : P →+* R) (↑h : R →+* P) : (a : R) → R) x : R) :
      S)
Tactic: rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : Q
⊢ (map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((map S (↑h.symm : P →+* R) ⋯ : (a : Q) → S) x : S) = x
have rw : ∀ (x : P),
  Eq (α := Q) ((RingHom.id Q : (a : Q) → Q) ((algebraMap P Q : (a : P) → Q) x : Q) : Q)
    ((algebraMap P Q : (a : P) → Q)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑h : R →+* P) (↑h.symm : P →+* R) : (a : P) → P) x : P) :
      Q)
Tactic: rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) T = M
have rw : Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) (Submonoid.map j M) = M
Tactic: rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) T = M
have rw₁ : Submonoid.comap (F := R ≃* P) (↑j : R ≃* P) (Submonoid.map j M) = M
Tactic: rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) T = M
have rw₂ : Submonoid.comap (F := R ≃* P) (↑j : R ≃* P) (Submonoid.map (F := R ≃* P) (↑j : R ≃* P) M) = M
Tactic: rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ Submonoid.map (F := P ≃* R) (MulEquiv.symm (↑j : R ≃* P)) T = M
have rw₃ : M = M
Tactic: rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
          Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
⊢ IsLocalization (Submonoid.map h M) S
have toIsLocalizationMap : Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
⊢ Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)
have toIsLocalizationMap : ∀ (y : ↥(Submonoid.map h M)), IsUnit.{u_2} (M := S) ((algebraMap P S : (a : P) → S) (↑y : P) : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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)
⊢ Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ Submonoid.IsLocalizationMap.{u_3, u_2} (N := S) (Submonoid.map h M) (⇑(algebraMap P S) : (a : P) → S)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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 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)
have 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)
              sorry) :
          P) :
        P) :
    S)
  ((algebraMap R S : (a : R) → S) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y hy) : R) : S)
Tactic: convert! IsLocalization.map_units S ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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 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)
have 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)
Tactic: dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
y : S
⊢ ∃ (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
have 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
Tactic: obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
have 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)) sorry).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)) sorry).1 :
      P)
Tactic: refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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
⊢ 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)
have 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)
Tactic: dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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) ((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)
have h₁ : (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) (↑s : R) : P) = (↑s : R)
Tactic: convert! e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : 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)
⊢ 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)
have h₂ : (h.symm.toRingHom : (a : P) → R) ((h : (a : R) → P) x : P) = x
Tactic: convert! e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
inst_4 : IsLocalization M S
h : R ≃+* P
this : Algebra P S := RingHom.toAlgebra (RingHom.comp (algebraMap R S) h.symm.toRingHom)
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
have 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
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply,
      IsLocalization.eq_iff_exists M S]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
have refine : IsLocalization (Submonoid.map h M) S → IsLocalization M S
Tactic: refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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 M S
have h₁ : M = Submonoid.map h.symm (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M)
Tactic: convert! isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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)
⊢ IsLocalization M S
have h₂ : inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap P S) h.symm.symm.toRingHom)
Tactic: convert! isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
⊢ M = Submonoid.map h.symm (Submonoid.map (F := R ≃* P) (↑h : R ≃* P) M)
have h₁ : Injective.{u_1 + 1, u_3 + 1} (α := R) (β := P) (⇑(↑h : R ≃* P) : (a : R) → P)
Tactic: rw [← Submonoid.map_coe_toMulEquiv, RingEquiv.coe_toMulEquiv_symm, ←
      Submonoid.comap_equiv_eq_map_symm, Submonoid.comap_map_eq_of_injective]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
⊢ inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap P S) h.symm.symm.toRingHom)
have h₁ : inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap R S) (h.symm.toRingHom.comp h.symm.symm.toRingHom))
Tactic: rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
⊢ inst_2 = RingHom.toAlgebra (RingHom.comp (algebraMap R S) (h.symm.toRingHom.comp h.symm.symm.toRingHom))
have h₁ : inst_2 = RingHom.toAlgebra (algebraMap R S)
Tactic: simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
⊢ inst_2 = RingHom.toAlgebra (algebraMap R S)
have h₁ : ∀ (r : R), Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: apply Algebra.algebra_ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommSemiring P
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
r : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
have h₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) r : S) ((algebraMap R S : (a : R) → S) r : S)
Tactic: rw [RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
⊢ IsLocalization M₂ K
have rw : IsLocalization M₁ K
Tactic: rw [IsLocalization.isLocalization_iff_of_base_ringEquiv _ _ e, hM]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Defs (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_4
inst_1 : CommSemiring S
K : Type u_5
inst_2 : CommSemiring K
inst_3 : Algebra R K
e : R ≃+* S
inst_4 : Algebra S K
M₁ : Submonoid S
M₂ : Submonoid R
hM : Submonoid.map e M₂ = M₁
h :
  ∀ (x : R),
    Eq.{u_5 + 1} (α := K) ((algebraMap R K : (a : R) → K) x : K)
      ((algebraMap S K : (a : S) → K) ((e : (a : R) → S) x : S) : K)
inst_5 : IsLocalization M₁ K
⊢ IsLocalization M₁ K
have h₁ : RingHom.toAlgebra (RingHom.comp (algebraMap R K) e.symm.toRingHom) = inst_4
Tactic: convert! (inferInstance : IsLocalization M₁ K)