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
g : R →+* P
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
x y : R × ↥M
⊢ Eq.{u_3 + 1} (α := P) ((lift hg : (a : S) → P) (mk' S x.1 x.2) : P) ((lift hg : (a : S) → P) (mk' S y.1 y.2) : P) ↔
    Eq.{u_3 + 1} (α := P) ((g : (a : R) → P) (x.1 * (↑y.2 : R)) : P) ((g : (a : R) → P) (y.1 * (↑x.2 : R)) : P)

Tactic:
(toLocalizationMap M S).lift_eq_iff _

Premises used: Submonoid.LocalizationMap.lift_eq_iff, IsLocalization.mk', 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
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap R S) = g

Tactic:
RingHom.ext <| (DFunLike.ext_iff (F := MonoidHom _ _)).1 <| (toLocalizationMap M S).lift_comp _

Premises used: DFunLike.ext_iff, RingHom.ext, Submonoid.LocalizationMap.lift_comp, IsLocalization.toLocalizationMap, Iff.mp
-- 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
j : S →+* P
⊢ lift (g := j.comp (algebraMap R S)) ⋯ = j

Tactic:
RingHom.ext <| (DFunLike.ext_iff (F := MonoidHom _ _)).1 <|
    (toLocalizationMap M S).lift_of_comp j.toMonoidHom

Premises used: Submonoid.LocalizationMap.lift_of_comp, DFunLike.ext_iff, RingHom.ext, IsLocalization.toLocalizationMap, Iff.mp, RingHom.toMonoidHom
-- 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
inst_3 : IsLocalization M S
P : Type u_4
inst_4 : Monoid P
j k : S →* P
h : Eq (α := R →* P) (j.comp (↑(algebraMap R S) : R →* S)) (k.comp (↑(algebraMap R S) : R →* S))
⊢ j = k

Tactic:
(toLocalizationMap M S).epic_of_localizationMap h

Premises used: Submonoid.LocalizationMap.epic_of_localizationMap, 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
inst_3 : IsLocalization M S
P : Type u_4
inst_4 : Semiring P
j k : S →+* P
h : Eq (α := R →+* P) (j.comp (algebraMap R S)) (k.comp (algebraMap R S))
⊢ j = k

Tactic:
RingHom.coe_monoidHom_injective <| monoidHom_ext M <| MonoidHom.ext <| RingHom.congr_fun h

Premises used: RingHom.congr_fun, MonoidHom.ext, IsLocalization.monoidHom_ext, RingHom.coe_monoidHom_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
inst_3 : IsLocalization M S
P : Type u_4
inst_4 : Monoid P
j k : S → P
hj1 : j 1 = 1
hk1 : k 1 = 1
hjm : ∀ (a b : S), j (a * b) = j a * j b
hkm : ∀ (a b : S), k (a * b) = k a * k b
h : ∀ (a : R), j ((algebraMap R S : (a : R) → S) a) = k ((algebraMap R S : (a : R) → S) a)
j' : S →* P := { toFun := j, map_one' := hj1, map_mul' := hjm }
k' : S →* P := { toFun := k, map_one' := hk1, map_mul' := hkm }
this : j' = k'
rw rw₁ : (↑k' : OneHom S P).toFun = (↑k' : OneHom S P).toFun
⊢ (↑j' : OneHom S P).toFun = (↑k' : OneHom S P).toFun

Tactic:
rw [this]
-- 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)
j : S →+* P
hj :
  ∀ (x : R),
    Eq.{u_3 + 1} (α := P) ((j : (a : S) → P) ((algebraMap R S : (a : R) → S) x : S) : P) ((g : (a : R) → P) x : P)
⊢ lift hg = j

Tactic:
RingHom.ext <|
    (DFunLike.ext_iff (F := MonoidHom _ _)).1 <|
      Submonoid.LocalizationMap.lift_unique (toLocalizationMap M S) (g := g.toMonoidHom) hg
        (j := j.toMonoidHom) hj

Premises used: Submonoid.LocalizationMap.lift_unique, DFunLike.ext_iff, RingHom.ext, IsLocalization.toLocalizationMap, Iff.mp
-- 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
inst_3 : IsLocalization M S
x : S
⊢ (lift.{u_1, u_2, u_2} (R := R) (M := M) (g := algebraMap R S) ⋯ : (a : S) → S) x = x

Tactic:
(toLocalizationMap M S).lift_id _

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.lift_id
-- 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)
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := S) (β := P) (⇑(lift hg) : (a : S) → P) ↔
    ∀ (v : P), ∃ (x : R × ↥M), HMul.hMul (β := P) v ((g : (a : R) → P) (↑x.2 : R) : P) = (g : (a : R) → P) x.1

Tactic:
(toLocalizationMap M S).lift_surjective_iff hg

Premises used: Set.Mem, Submonoid.LocalizationMap.lift_surjective_iff, 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
hg : ∀ (y : ↥M), IsUnit.{u_3} (M := P) ((g : (a : R) → P) (↑y : R) : P)
⊢ Injective.{u_2 + 1, u_3 + 1} (α := S) (β := P) (⇑(lift hg) : (a : S) → P) ↔
    ∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_3 + 1} (α := P) ((g : (a : R) → P) x : P) ((g : (a : R) → P) y : P)

Tactic:
(toLocalizationMap M S).lift_injective_iff hg

Premises used: IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.lift_injective_iff
-- 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
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommSemiring T
f : S →+* T
rw :
  (∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T) ((f.comp (algebraMap R S) : (a : R) → T) x : T)
          ((f.comp (algebraMap R S) : (a : R) → T) y : T)) ↔
    ∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T)
          ((lift (g := f.comp (algebraMap R S)) ⋯ : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
          ((lift (g := f.comp (algebraMap R S)) ⋯ : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)
⊢ Injective.{u_2 + 1, u_4 + 1} (α := S) (β := T) (⇑f : (a : S) → T) ↔
    ∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T) ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
          ((f : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)

Tactic:
rw [← IsLocalization.lift_of_comp (M := M) f, IsLocalization.lift_injective_iff]

Premises used: IsLocalization.lift_of_comp, IsLocalization.lift_injective_iff
-- 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
inst_3 : IsLocalization M S
T : Type u_4
inst_4 : CommSemiring T
f : S →+* T
⊢ (∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T) ((f.comp (algebraMap R S) : (a : R) → T) x : T)
          ((f.comp (algebraMap R S) : (a : R) → T) y : T)) ↔
    ∀ (x y : R),
      Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x : S) ((algebraMap R S : (a : R) → S) y : S) ↔
        Eq.{u_4 + 1} (α := T)
          ((lift (g := f.comp (algebraMap R S)) ⋯ : (a : S) → T) ((algebraMap R S : (a : R) → S) x : S) : T)
          ((lift (g := f.comp (algebraMap R S)) ⋯ : (a : S) → T) ((algebraMap R S : (a : R) → S) y : S) : T)

Tactic:
simp
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : R
⊢ Eq.{u_4 + 1} (α := Q) ((map Q g hy : (a : S) → Q) ((algebraMap R S : (a : R) → S) x : S) : Q)
    ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) x : P) : Q)

Tactic:
lift_eq (fun y => map_units _ ⟨g y, hy y.2⟩) x

Premises used: IsLocalization.lift_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
inst_4 : IsLocalization M S
g : R →+* P
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
⊢ Eq (α := R →+* Q) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map Q g hy) (algebraMap R S))
    (RingHom.comp (algebraMap P Q) g)

Tactic:
lift_comp fun y => map_units _ ⟨g y, hy y.2⟩

Premises used: IsLocalization.map, IsLocalization.lift_comp
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : R
y : ↥M
⊢ (map Q g hy : (a : S) → Q) (mk' S x y) =
    mk'.{u_3, u_4} (R := P) (M := T) Q ((g : (a : R) → P) x : P)
      (Subtype.mk (p := fun (x : P) ↦ x ∈ T) ((g : (a : R) → P) (↑y : R)) ⋯ : ↥T)

Tactic:
Submonoid.LocalizationMap.map_mk' (toLocalizationMap M S) (g := g.toMonoidHom)
    (fun y => hy y.2) (k := toLocalizationMap T Q) ..

Premises used: Set.Mem, Submonoid.LocalizationMap.map_mk', IsLocalization.mk', IsLocalization.toLocalizationMap, Subtype.property
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
j : S →+* Q
hj :
  ∀ (x : R),
    Eq.{u_4 + 1} (α := Q) ((j : (a : S) → Q) ((algebraMap R S : (a : R) → S) x : S) : Q)
      ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) x : P) : Q)
⊢ map Q g hy = j

Tactic:
lift_unique (fun y => map_units _ ⟨g y, hy y.2⟩) hj

Premises used: IsLocalization.map, IsLocalization.lift_unique
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst_8 : CommSemiring A
U : Submonoid A
W : Type u_6
inst_9 : CommSemiring W
inst_10 : Algebra A W
inst_11 : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
⊢ Eq (α := S →+* W) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map W l hl) (map Q g hy))
    (map (M := M) (T := U) W (l.comp g) ⋯)

Tactic:
RingHom.ext fun x =>
    Submonoid.LocalizationMap.map_map (P := P) (toLocalizationMap M S) (fun y => hy y.2)
      (toLocalizationMap U W) (fun w => hl w.2) x

Premises used: RingHom.ext, IsLocalization.toLocalizationMap, Submonoid.LocalizationMap.map_map, Subtype.property
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst_8 : CommSemiring A
U : Submonoid A
W : Type u_6
inst_9 : CommSemiring W
inst_10 : Algebra A W
inst_11 : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
rw :
  Eq.{u_6 + 1} (α := W) ((map W l hl : (a : Q) → W) ((map Q g hy : (a : S) → Q) x : Q) : W)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map W l hl) (map Q g hy) : (a : S) → W) x : W)
⊢ Eq.{u_6 + 1} (α := W) ((map W l hl : (a : Q) → W) ((map Q g hy : (a : S) → Q) x : Q) : W)
    ((map (M := M) (T := U) W (l.comp g) ⋯ : (a : S) → W) x : W)

Tactic:
rw [← map_comp_map (Q := Q) hy hl]

Premises used: IsLocalization.map_comp_map
-- 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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
A : Type u_5
inst_8 : CommSemiring A
U : Submonoid A
W : Type u_6
inst_9 : CommSemiring W
inst_10 : Algebra A W
inst_11 : IsLocalization U W
l : P →+* A
hl : T ≤ Submonoid.comap l U
x : S
⊢ Eq.{u_6 + 1} (α := W) ((map W l hl : (a : Q) → W) ((map Q g hy : (a : S) → Q) x : Q) : W)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (map W l hl) (map Q g hy) : (a : S) → W) x : W)

Tactic:
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
T : Submonoid P
Q : Type u_4
inst_5 : CommSemiring Q
inst_6 : Algebra P Q
inst_7 : IsLocalization T Q
hy : M ≤ Submonoid.comap g T
x : S
z : R
rw :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)
rw₁ :
  (map Q g hy : (a : S) → Q) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) z : S) x) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
rw₂ :
  HMul.hMul (α := Q) (β := Q) ((map Q g hy : (a : S) → Q) ((algebraMap R S : (a : R) → S) z : S) : Q)
      ((map Q g hy : (a : S) → Q) x : Q) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
rw₃ rw₄ :
  HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q) =
    HMul.hMul (α := Q) (β := Q) ((algebraMap P Q : (a : P) → Q) ((g : (a : R) → P) z : P) : Q)
      ((map Q g hy : (a : S) → Q) x : Q)
⊢ (map Q g hy : (a : S) → Q) (z • x) =
    HSMul.hSMul.{u_3, u_4, u_4} (α := P) (β := Q) ((g : (a : R) → P) z : P) ((map Q g hy : (a : S) → Q) x : Q)

Tactic:
rw [Algebra.smul_def, Algebra.smul_def, map_mul, map_eq]

Premises used: IsLocalization.map_eq, map_mul, Algebra.smul_def
-- 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
inst_3 : IsLocalization M S
Q : Type u_5
inst_4 : CommSemiring Q
inst_5 : Algebra R Q
inst_6 : IsLocalization M Q
x : R
y : ↥M
⊢ (map (M := M) (T := M) Q (RingHom.id R) ⋯ : (a : S) → Q) (mk' S x y) = mk' Q x y

Tactic:
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
inst_3 : IsLocalization M S
z : S
h : M ≤ Submonoid.comap (F := R →+* R) (RingHom.id R) M
⊢ (map S (RingHom.id R) h : (a : S) → S) z = z

Tactic:
lift_id _

Premises used: IsLocalization.lift_id
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
rw :
  Eq (α := Submonoid R) (Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M)
    (Submonoid.map (F := R →* R) (MonoidHom.id R) M)
⊢ Submonoid.map h.symm.toMonoidHom T = M

Tactic:
rw [← M.map_id, ← H, Submonoid.map_map]

Premises used: Submonoid.map_map, Submonoid.map_id
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
e_f : h.symm.toMonoidHom.comp h.toMonoidHom = MonoidHom.id R
⊢ Eq (α := Submonoid R) (Submonoid.map (h.symm.toMonoidHom.comp h.toMonoidHom) M)
    (Submonoid.map (F := R →* R) (MonoidHom.id R) M)

Tactic:
congr
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
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)
⊢ h.symm.toMonoidHom.comp h.toMonoidHom = MonoidHom.id R

Tactic:
ext
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
x : R
⊢ Eq (α := R) ((h.symm.toMonoidHom.comp h.toMonoidHom : (a : R) → R) x : R) ((MonoidHom.id R : (a : R) → R) x : R)

Tactic:
apply 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
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
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)
⊢ (map S (↑h.symm : P →+* R) ⋯ : (a : Q) → S) ((map Q (↑h : R →+* P) ⋯ : (a : S) → Q) x : Q) = x

Tactic:
rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]

Premises used: RingHom.id_apply, IsLocalization.map_map, IsLocalization.map_unique, RingHom.id
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : S
⊢ ∀ (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:
simp
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : Q
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)
⊢ (map Q (↑h : R →+* P) ⋯ : (a : S) → Q) ((map S (↑h.symm : P →+* R) ⋯ : (a : Q) → S) x : S) = x

Tactic:
rw [map_map, map_unique _ (RingHom.id _), RingHom.id_apply]

Premises used: RingHom.id_apply, IsLocalization.map_map, IsLocalization.map_unique, RingHom.id
-- 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
h : R ≃+* P
H : Submonoid.map h.toMonoidHom M = T
H' : Submonoid.map h.symm.toMonoidHom T = M
x : Q
⊢ ∀ (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:
simp
-- 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
⊢ Eq (α := S →+* Q) (↑(ringEquivOfRingEquiv S Q j H) : S →+* Q) (map Q (↑j : R →+* P) ⋯)

Tactic:
rfl

Premises used: IsLocalization.map, MonoidHomClass.toMonoidHom, IsLocalization.lift, RingHomClass.toRingHom, 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
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
⊢ Eq.{u_4 + 1} (α := Q) ((ringEquivOfRingEquiv S Q j H : (a : S) → Q) ((algebraMap R S : (a : R) → S) x : S) : Q)
    ((algebraMap P Q : (a : P) → Q) ((j : (a : R) → P) x : P) : Q)

Tactic:
simp