awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  ∀ (x : Aₚ),
    Eq.{u_10 + 1} (α := Bₚ)
      ((((IsLocalizedModule.map M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
                    (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) :
                  (a : A →ₗ[R] B) → Aₚ →ₗ[R] Bₚ)
                f.toLinearMap :
              Aₚ →ₗ[R] Bₚ) :
            (a : Aₚ) → Bₚ)
          x :
        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)) :
            (a : Aₚ) → Bₚ)
          x :
        Bₚ)
⊢ Eq (α := Aₚ →ₗ[R] Bₚ)
    ((IsLocalizedModule.map M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
            (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) :
          (a : A →ₗ[R] B) → Aₚ →ₗ[R] Bₚ)
        f.toLinearMap :
      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₂)
        (AlgHom.toLinearMap (mapₐ M Rₚ Aₚ Bₚ f)) :
      Aₚ →ₗ[R] Bₚ)

Tactic:
ext x
-- 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ₚ)
    ((((IsLocalizedModule.map M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
                  (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) :
                (a : A →ₗ[R] B) → Aₚ →ₗ[R] Bₚ)
              f.toLinearMap :
            Aₚ →ₗ[R] Bₚ) :
          (a : Aₚ) → Bₚ)
        x :
      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)) :
          (a : Aₚ) → Bₚ)
        x :
      Bₚ)

Tactic:
DFunLike.congr_fun (mapExtendScalars_eq_toLinearMap_mapₐ M Rₚ Aₚ Bₚ f) x

Premises used: DFunLike.congr_fun, LocalizedModule.liftOn, IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ, LocalizedModule.lift'
-- 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ₚ)
    ((((IsLocalizedModule.map M (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ))
                  (AlgHom.toLinearMap (IsScalarTower.toAlgHom R B Bₚ)) :
                (a : A →ₗ[R] B) → Aₚ →ₗ[R] Bₚ)
              f.toLinearMap :
            Aₚ →ₗ[R] Bₚ) :
          (a : Aₚ) → Bₚ)
        x :
      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)) :
          (a : Aₚ) → Bₚ)
        x :
      Bₚ)

Tactic:
exact DFunLike.congr_fun (mapExtendScalars_eq_toLinearMap_mapₐ M Rₚ Aₚ Bₚ f) x

Premises used: DFunLike.congr_fun, IsLocalization.mapExtendScalars_eq_toLinearMap_mapₐ
-- 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
Rₚ : Type u_8
inst_3 : CommSemiring Rₚ
inst_4 : Algebra R Rₚ
inst_5 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_6 : CommSemiring Aₚ
inst_7 : Algebra R Aₚ
inst_8 : Algebra A Aₚ
inst_9 : IsScalarTower R A Aₚ
inst_10 : IsLocalization (algebraMapSubmonoid A M) Aₚ
inst_11 : Algebra Rₚ Aₚ
inst_12 : IsScalarTower R Rₚ Aₚ
⊢ Eq (α := Rₚ →ₗ[R] Aₚ)
    ((IsLocalizedModule.map M (Algebra.linearMap R Rₚ) (AlgHom.toLinearMap (IsScalarTower.toAlgHom R A Aₚ)) :
          (a : R →ₗ[R] A) → Rₚ →ₗ[R] Aₚ)
        (Algebra.linearMap R A) :
      Rₚ →ₗ[R] Aₚ)
    ((↑R :
          {S M : Type u_8} →
            {M₂ : Type u_9} →
              [inst : Semiring R] →
                [inst_13 : Semiring S] →
                  [inst_14 : AddCommMonoid M] →
                    [inst_15 : AddCommMonoid M₂] →
                      [inst_16 : Module R M] →
                        [inst_17 : Module R M₂] →
                          [inst_18 : Module S M] →
                            [inst_19 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (AlgHom.toLinearMap (mapₐ M Rₚ Rₚ Aₚ (ofId R A))) :
      Rₚ →ₗ[R] Aₚ)

Tactic:
map_eq_toLinearMap_mapₐ M Rₚ Rₚ Aₚ (Algebra.ofId R A)

Premises used: AlgHom.toLinearMap, Algebra.linearMap, Algebra.ofId, IsLocalization.map_eq_toLinearMap_mapₐ
-- 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 : ↥(RingHom.ker f)
⊢ Eq.{u_9 + 1} (α := ↥(RingHom.ker (F := Aₚ →ₐ[Rₚ] Bₚ) (mapₐ M Rₚ Aₚ Bₚ f)))
    (((toKerIsLocalization M Rₚ Aₚ Bₚ f :
            LinearMap.{u_6, u_6, u_6, u_9} (RingHom.id A) ↥(RingHom.ker f)
              ↥(RingHom.ker (F := Aₚ →ₐ[Rₚ] Bₚ) (mapₐ M Rₚ Aₚ Bₚ f))) :
          (a : ↥(RingHom.ker f)) → ↥(RingHom.ker (mapₐ M Rₚ Aₚ Bₚ f)))
        x :
      ↥(RingHom.ker (F := Aₚ →ₐ[Rₚ] Bₚ) (mapₐ M Rₚ Aₚ Bₚ f)))
    (((RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯ :
            LinearMap.{u_6, u_6, u_6, u_9} (RingHom.id A) ↥(RingHom.ker f.toRingHom)
              ↥(RingHom.ker (F := Aₚ →+* Bₚ) (map Bₚ f.toRingHom ⋯))) :
          (a : ↥(RingHom.ker f.toRingHom)) → ↥(RingHom.ker (map Bₚ f.toRingHom ⋯)))
        x :
      ↥(RingHom.ker (F := Aₚ →+* Bₚ) (map Bₚ f.toRingHom ⋯)))

Tactic:
rfl

Premises used: Set.Mem, 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
⊢ IsLocalizedModule (M' := ↥(RingHom.ker (F := Aₚ →ₐ[Rₚ] Bₚ) (mapₐ M Rₚ Aₚ Bₚ f))) (algebraMapSubmonoid A M)
    (toKerIsLocalization M Rₚ Aₚ Bₚ f)

Tactic:
RingHom.toKerIsLocalization_isLocalizedModule Bₚ f.toRingHom
    (algebraMapSubmonoid_map_eq M f)

Premises used: IsLocalization.mapₐ, IsLocalization.map, AlgHom.toKerIsLocalization, Set.Mem, Algebra.algebraMapSubmonoid_map_eq, IsLocalization.lift, AlgHom.toRingHom, Ideal.comap, RingHom.toKerIsLocalization_isLocalizedModule, RingHom.ker
-- Module: Mathlib.RingTheory.Localization.Algebra
Goal:
R : Type u_5
inst : CommSemiring R
S : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
inst_3 : IsLocalization S A
x : R[X]
⊢ Eq.{u_6 + 1} (α := A[X])
    (((↑(AlgEquiv.symm (polyEquivTensor' R A)) : TensorProduct R A R[X] ≃ₗ[A] A[X]) :
          (a : TensorProduct R A R[X]) → A[X])
        (1 ⊗ₜ[R] x) :
      A[X])
    ((AlgHom.toLinearMap (IsScalarTower.toAlgHom R R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
hS : S ≤ A⁰
s : ↥S
⊢ IsUnit.{u_2} (M := K) ((algebraMap A K : (a : A) → K) (↑s : A) : K)

Tactic:
apply IsLocalization.map_units K (⟨s.1, hS s.2⟩ : A⁰)

Premises used: Subtype.mk, IsLocalization.map_units, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a : A
⊢ OneHom.toFun.{u_3, u_2} (M := B)
      ((↑(↑(IsLocalization.lift (g := algebraMap A K) ⋯) : B →* K) : OneHom B K) : OneHom B K)
      ((algebraMap A B : (a : A) → B) a : B) =
    (algebraMap A K : (a : A) → K) a

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
b : B
⊢ Eq.{u_2 + 1} (α := K) ((mapToFractionRing K S B hS : (a : B) → K) b : K)
    ((IsLocalization.lift (g := algebraMap A K) ⋯ : (a : B) → K) b : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
x : B
obtain :
  ∀ (a : A) (s : ↥S),
    ∃ (a_1 : A) (s_1 : A) (hs : s_1 ∈ S),
      (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K) (IsLocalization.mk' B a s) =
        IsLocalization.mk' K a_1
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s_1 ⋯)
⊢ ∃ (a : A) (s : A) (hs : s ∈ S),
    (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K) x =
      IsLocalization.mk' K a
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)

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

Premises used: rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
h :
  (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K) (IsLocalization.mk' B a s) =
    IsLocalization.mk' K a
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (↑s : A) ⋯)
⊢ ∃ (a_1 : A) (s_1 : A) (hs : s_1 ∈ S),
    (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K) (IsLocalization.mk' B a s) =
      IsLocalization.mk' K a_1
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s_1 ⋯)

Tactic:
use a, s, s.2

Premises used: Subtype.property
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a : A
s : ↥S
⊢ (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K) (IsLocalization.mk' B a s) =
    IsLocalization.mk' K a
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (↑s : A) ⋯)

Tactic:
apply IsLocalization.lift_mk'

Premises used: IsLocalization.lift_mk'
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
h :
  (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K)
      (IsLocalization.mk' B a (Subtype.mk (p := fun (x : A) ↦ x ∈ S) s hs)) =
    IsLocalization.mk' K a (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)
⊢ Membership.mem (γ := Subalgebra A K) (AlgHom.range (mapToFractionRing K S B hS))
    (IsLocalization.mk' K a
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯))

Tactic:
use IsLocalization.mk' _ a ⟨s, hs⟩

Premises used: Subtype.mk, IsLocalization.mk'
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a s : A
hs : s ∈ S
⊢ (AlgHom.toRingHom (mapToFractionRing K S B hS) : (a : B) → K)
      (IsLocalization.mk' B a (Subtype.mk (p := fun (x : A) ↦ x ∈ S) s hs)) =
    IsLocalization.mk' K a (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)

Tactic:
apply IsLocalization.lift_mk'

Premises used: IsLocalization.lift_mk'
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := B) (β := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (⇑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) : (a : B) → ↥(mapToFractionRing K S B hS).range)

Tactic:
⟨fun a b h => ?_, Set.rangeFactorization_surjective⟩

Premises used: Set.rangeFactorization_surjective, And.intro, Function.Bijective
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
refine :
  ∀ (a b : B)
    (h :
      Eq.{u_2 + 1} (α := ↥(AlgHom.range (mapToFractionRing K S B hS)))
        (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
                AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
              (a : B) → ↥(mapToFractionRing K S B hS).range)
            a :
          ↥(AlgHom.range (mapToFractionRing K S B hS)))
        (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
                AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
              (a : B) → ↥(mapToFractionRing K S B hS).range)
            b :
          ↥(AlgHom.range (mapToFractionRing K S B hS)))),
    a = b
⊢ Function.Bijective.{u_3 + 1, u_2 + 1} (α := B) (β := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (⇑(AlgHom.rangeRestrict (mapToFractionRing K S B hS)) : (a : B) → ↥(mapToFractionRing K S B hS).range)

Tactic:
refine ⟨fun a b h => ?_, Set.rangeFactorization_surjective⟩
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a b : B
h :
  Eq.{u_2 + 1} (α := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        a :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        b :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
⊢ a = b

Tactic:
(IsLocalization.lift_injective_iff _).2 (fun a b => ?_) (Subtype.ext_iff.1 h)

Premises used: Iff.mpr, Subtype.ext_iff, Iff.mp, IsLocalization.lift_injective_iff
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a b : B
h :
  Eq.{u_2 + 1} (α := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        a :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        b :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
refine :
  ∀ (a b : A),
    Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔
      Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)
⊢ a = b

Tactic:
refine (IsLocalization.lift_injective_iff _).2 (fun a b => ?_) (Subtype.ext_iff.1 h)

Premises used: Iff.mpr, Subtype.ext_iff, Iff.mp, IsLocalization.lift_injective_iff
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a_1 b_1 : B
h :
  Eq.{u_2 + 1} (α := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        a_1 :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        b_1 :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
a b : A
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)

Tactic:
⟨fun h => congr_arg _ (IsLocalization.injective _ hS h),
        fun h => congr_arg _ (IsFractionRing.injective A K h)⟩

Premises used: Algebra.algebraMap, IsFractionRing.injective, IsLocalization.injective, congr_arg, Iff.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AsSubring
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS_1 : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
B : Type u_3
inst_4 : CommRing B
inst_5 : Algebra A B
inst_6 : IsLocalization S B
hS : S ≤ A⁰
a_1 b_1 : B
h :
  Eq.{u_2 + 1} (α := ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        a_1 :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
    (((AlgHom.rangeRestrict (mapToFractionRing K S B hS) :
            AlgHom.{u_1, u_3, u_2} A B ↥(AlgHom.range (mapToFractionRing K S B hS))) :
          (a : B) → ↥(mapToFractionRing K S B hS).range)
        b_1 :
      ↥(AlgHom.range (mapToFractionRing K S B hS)))
a b : A
⊢ Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔
    Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) a : K) ((algebraMap A K : (a : A) → K) b : K)

Tactic:
exact ⟨fun h => congr_arg _ (IsLocalization.injective _ hS h),
        fun h => congr_arg _ (IsFractionRing.injective A K h)⟩