awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Algebra (goal)
Goal:
R : Type u_5
inst : CommSemiring R
M : Submonoid R
A : Type u_6
inst_1 : CommSemiring A
inst_2 : Algebra R A
B : Type u_7
inst_3 : CommSemiring B
inst_4 : Algebra R B
Rₚ : Type u_8
inst_5 : CommSemiring Rₚ
inst_6 : Algebra R Rₚ
inst_7 : IsLocalization M Rₚ
Aₚ : Type u_9
inst_8 : CommSemiring Aₚ
inst_9 : Algebra R Aₚ
inst_10 : Algebra A Aₚ
inst_11 : IsScalarTower R A Aₚ
inst_12 : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst_13 : CommSemiring Bₚ
inst_14 : Algebra R Bₚ
inst_15 : Algebra B Bₚ
inst_16 : IsScalarTower R B Bₚ
inst_17 : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst_18 : Algebra Rₚ Aₚ
inst_19 : Algebra Rₚ Bₚ
inst_20 : IsScalarTower R Rₚ Aₚ
inst_21 : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ Eq (α := Aₚ →ₗ[R] Bₚ)
    ((IsLocalizedModule.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ₚ)
have 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ₚ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
⊢ ∃ (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 ⋯)
have 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 sorry)
Tactic: obtain ⟨a, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
⊢ ∃ (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 ⋯)
have 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) sorry)
Tactic: use a, s, s.2
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
⊢ 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 ⋯))
have 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 sorry)
Tactic: use IsLocalization.mk' _ a ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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)
have 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
Tactic: refine ⟨fun a b h => ?_, Set.rangeFactorization_surjective⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
have 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)
Tactic: refine (IsLocalization.lift_injective_iff _).2 (fun a b => ?_) (Subtype.ext_iff.1 h)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
hS : S ≤ A⁰
⊢ {x : K |
      ∃ (a : A) (s : A) (hs : s ∈ S),
        x =
          IsLocalization.mk' K a
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)} =
    (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
have h : ∀ (x : K),
  Membership.mem (γ := Set K)
      {x : K |
        ∃ (a : A) (s : A) (hs : s ∈ S),
          x =
            IsLocalization.mk' K a
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s sorry)}
      x ↔
    x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
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
hS : S ≤ A⁰
x : K
⊢ Membership.mem (γ := Set K)
      {x : K |
        ∃ (a : A) (s : A) (hs : s ∈ S),
          x =
            IsLocalization.mk' K a
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)}
      x ↔
    x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
have h : x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K) ↔
  Membership.mem (γ := Set K)
    {x : K |
      ∃ (a : A) (s : A) (hs : s ∈ S),
        x =
          IsLocalization.mk' K a
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s sorry)}
    x
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ IsLocalization.{u_1, u_2} S
    ↥(Subalgebra.copy (AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
        {x : K |
          ∃ (a : A) (s : A) (hs : s ∈ S),
            x =
              IsLocalization.mk' K a
                (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)}
        ⋯)
have rw : IsLocalization.{u_1, u_2} S
  ↥(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
Tactic: rw [Subalgebra.copy_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field 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
x : K
⊢ Membership.mem (γ := Subalgebra A K) (AlgHom.range (mapToFractionRing K S B hS)) x ↔
    ∃ (a : A) (s : A) (_ : s ∈ S),
      x = HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)
have rw : (∃ (a : A) (s : A) (hs : s ∈ S),
    x =
      IsLocalization.mk' K a
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s sorry)) ↔
  ∃ (a : A) (s : A) (_ : s ∈ S),
    x = HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)
Tactic: rw [mem_range_mapToFractionRing_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field 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
x : K
⊢ (∃ (a : A) (s : A) (hs : s ∈ S),
      x =
        IsLocalization.mk' K a
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)) ↔
    ∃ (a : A) (s : A) (_ : s ∈ S),
      x = HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)
have h : ∀ (x x_1 : A) (x_2 : x_1 ∈ S),
  HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) (((algebraMap A K : (a : A) → K) x_1)⁻¹ : K) =
    IsLocalization.mk' K x
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_1 sorry)
Tactic: convert! Iff.rfl
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field 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
x : K
x_1 x_2 : A
h : x_2 ∈ S
⊢ HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) x_1 : K) (((algebraMap A K : (a : A) → K) x_2)⁻¹ : K) =
    IsLocalization.mk' K x_1
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 ⋯)
have h : Eq.{u_2 + 1} (α := K) (((algebraMap A K : (a : A) → K) x_2)⁻¹ : K)
  ((↑((IsUnit.liftRight
                (MonoidHom.restrict
                  (Submonoid.LocalizationMap.toMonoidHom (S := A⁰) (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
                sorry :
              (a : ↥A⁰) → Kˣ)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 sorry))⁻¹ :
      K) :
    K)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field 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
x : K
x_1 x_2 : A
h : x_2 ∈ S
⊢ Eq.{u_2 + 1} (α := K) (((algebraMap A K : (a : A) → K) x_2)⁻¹ : K)
    ((↑((IsUnit.liftRight
                  (MonoidHom.restrict
                    (Submonoid.LocalizationMap.toMonoidHom (S := A⁰) (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
                  ⋯ :
                (a : ↥A⁰) → Kˣ)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 ⋯))⁻¹ :
        K) :
      K)
have h : Eq.{u_2 + 1} (α := K) (((algebraMap A K : (a : A) → K) x_2)⁻¹ : K)
  ((↑((IsUnit.liftRight
                (MonoidHom.restrict
                  (Submonoid.LocalizationMap.toMonoidHom (S := A⁰) (IsLocalization.toLocalizationMap A⁰ K)) A⁰)
                sorry :
              (a : ↥A⁰) → Kˣ)
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 sorry)) :
        K)⁻¹ :
    K)
Tactic: rw [Units.val_inv_eq_inv_val]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ {x : K |
      ∃ (a : A) (s : A) (_ : s ∈ S),
        x =
          HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K)
            (((algebraMap A K : (a : A) → K) s)⁻¹ : K)} =
    (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
have h : ∀ (x : K),
  Membership.mem (γ := Set K)
      {x : K |
        ∃ (a : A) (s : A) (_ : s ∈ S),
          x =
            HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K)
              (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
      x ↔
    x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : K
⊢ Membership.mem (γ := Set K)
      {x : K |
        ∃ (a : A) (s : A) (_ : s ∈ S),
          x =
            HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K)
              (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
      x ↔
    x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)
have h : x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K) ↔
  Membership.mem (γ := Set K)
    {x : K |
      ∃ (a : A) (s : A) (_ : s ∈ S),
        x =
          HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
    x
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ Eq (α := Subalgebra A K) (ofField K S hS) (subalgebra K S hS)
have simp_rw : Eq (α := Subalgebra A K)
  (Subalgebra.copy (AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
    {x : K |
      ∃ (a : A) (s : A) (_ : s ∈ S),
        x =
          HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
    sorry)
  (subalgebra K S hS)
Tactic: simp_rw [ofField, subalgebra, Subalgebra.copy_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
simp_rw :
  Eq (α := Subalgebra A K)
    (Subalgebra.copy (AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
      {x : K |
        ∃ (a : A) (s : A) (_ : s ∈ S),
          x =
            HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K)
              (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
      ⋯)
    (subalgebra K S hS)
⊢ Eq (α := Subalgebra A K) (ofField K S hS) (subalgebra K S hS)
have simp_rw₁ : Eq (α := Subalgebra A K)
  (Subalgebra.copy (AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
    {x : K |
      ∃ (a : A) (s : A) (_ : s ∈ S),
        x =
          HMul.hMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) a : K) (((algebraMap A K : (a : A) → K) s)⁻¹ : K)}
    sorry)
  (Subalgebra.copy (AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
    {x : K |
      ∃ (a : A) (s : A) (hs : s ∈ S),
        x =
          IsLocalization.mk' K a
            (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s sorry)}
    sorry)
Tactic: simp_rw [ofField, subalgebra, Subalgebra.copy_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
⊢ IsLocalization.{u_1, u_2} S ↥(ofField K S hS)
have rw : IsLocalization.{u_1, u_2} S ↥(subalgebra K S hS)
Tactic: rw [ofField_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S_1 : Submonoid A
hS : S_1 ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
S : Subalgebra A K
⊢ IsFractionRing (↥S) K
have refine : ∀ (z : K),
  ∃ (x : ↥S) (y : ↥S),
    z =
      HDiv.hDiv (α := K) (β := K) ((algebraMap (↥S) K : (a : ↥S) → K) x : K) ((algebraMap (↥S) K : (a : ↥S) → K) y : K)
Tactic: refine IsFractionRing.of_field S K fun z ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AsSubring (goal)
Goal:
A : Type u_1
K : Type u_2
inst : CommRing A
S_1 : Submonoid A
hS : S_1 ≤ A⁰
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
S : Subalgebra A K
z : K
⊢ ∃ (x : ↥S) (y : ↥S),
    z =
      HDiv.hDiv (α := K) (β := K) ((algebraMap (↥S) K : (a : ↥S) → K) x : K) ((algebraMap (↥S) K : (a : ↥S) → K) y : K)
have rcases : ∀ (x y : A),
  Membership.mem (γ := Submonoid A) A⁰ y →
    ∀
      (eq :
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K) = z),
      ∃ (x : ↥S) (y : ↥S),
        z =
          HDiv.hDiv (α := K) (β := K) ((algebraMap (↥S) K : (a : ↥S) → K) x : K)
            ((algebraMap (↥S) K : (a : ↥S) → K) y : K)
Tactic: rcases IsFractionRing.div_surjective A z with ⟨x, y, _, eq⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
hze : Eq.{u_2 + 1} (α := S) 0 1
⊢ False
have hze₁ : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) 1 : S)
Tactic: rw [← (algebraMap R S).map_one, ← (algebraMap R S).map_zero] at hze
Cleared hypotheses: hze
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
hze : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) 1 : S)
⊢ False
have obtain : ∀ (t : ↥P.primeCompl) (ht : (↑t : R) * 0 = (↑t : R) * 1), False
Tactic: obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
hze : Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) ((algebraMap R S : (a : R) → S) 1 : S)
t : ↥P.primeCompl
ht : (↑t : R) * 0 = (↑t : R) * 1
⊢ False
have htz : (↑t : R) = 0
Tactic: have htz : (t : R) = 0 := by simpa using ht.symm
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
⊢ False
have obtain : ∀ (z : S) (hxyz : (x + y) * z = 1), False
Tactic: obtain ⟨z, hxyz⟩ := isUnit_iff_exists_inv.1 hu
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
⊢ False
have this₁ : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
Tactic: have : ∀ {r : R} {s : P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P := fun {r s} =>
        not_imp_comm.1 fun nr => isUnit_iff_exists_inv.2 ⟨mk' S ↑s (⟨r, nr⟩ : P.primeCompl),
          mk'_mul_mk'_eq_one' _ _ <| show r ∈ P.primeCompl from nr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
⊢ False
have rcases : ∀ (rx : R) (sx : ↥P.primeCompl) (hrx : mk' S rx sx = x), False
Tactic: rcases exists_mk'_eq P.primeCompl x with ⟨rx, sx, hrx⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.AtPrime.Basic (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
P : Ideal R
hp : P.IsPrime
inst_3 : IsLocalization.AtPrime S P
this_1 : Nontrivial S := ⋯
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
this : ∀ {r : R} {s : ↥P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P
rx : R
sx : ↥P.primeCompl
hrx : mk' S rx sx = x
⊢ False
have rcases : ∀ (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y), False
Tactic: rcases exists_mk'_eq P.primeCompl y with ⟨ry, sy, hry⟩