awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⁰
⊢ IsFractionRing (↥(AlgHom.range (mapToFractionRing K S B hS))) K

Tactic:
IsFractionRing.isFractionRing_of_isLocalization S _ _ hS

Premises used: Set.Mem, IsFractionRing.isFractionRing_of_isLocalization, Subsemiring.copy, RingHom.rangeS
-- 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
hS : S ≤ A⁰
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 ⋯)}
        x ↔
      x ∈ (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : 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 ⋯)} =
    (↑(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS)) : Set K)

Tactic:
ext
-- 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
hS : S ≤ A⁰
x : K
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 ⋯)}
      x
⊢ 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)

Tactic:
symm
-- 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
hS : S ≤ A⁰
x : K
⊢ 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 ⋯)}
      x

Tactic:
apply mem_range_mapToFractionRing_iff

Premises used: Localization.mem_range_mapToFractionRing_iff
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
rw :
  IsLocalization.{u_1, u_2} S
    ↥(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))
⊢ 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 ⋯)}
        ⋯)

Tactic:
rw [Subalgebra.copy_eq]

Premises used: Subalgebra.copy_eq
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
    ↥(AlgHom.range (A := Localization (M := A) S) (mapToFractionRing K S (Localization (M := A) S) hS))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
⊢ IsFractionRing (↥(subalgebra K S hS)) K

Tactic:
IsFractionRing.isFractionRing_of_isLocalization S _ _ hS

Premises used: Set.Mem, IsFractionRing.isFractionRing_of_isLocalization
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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 ⋯)) ↔
    ∃ (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)
⊢ 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)

Tactic:
rw [mem_range_mapToFractionRing_iff]

Premises used: Localization.mem_range_mapToFractionRing_iff
-- Module: Mathlib.RingTheory.Localization.AsSubring
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) (hs : s ∈ S),
      x =
        IsLocalization.mk' K a
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s ⋯)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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 ⋯)
⊢ (∃ (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)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Localization.AsSubring
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_1 : x_2 ∈ S
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⁰)
                  ⋯ :
                (a : ↥A⁰) → Kˣ)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 ⋯))⁻¹ :
        K) :
      K)
⊢ 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 ⋯)

Tactic:
congr
-- Module: Mathlib.RingTheory.Localization.AsSubring
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_1 : x_2 ∈ S
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⁰)
                  ⋯ :
                (a : ↥A⁰) → Kˣ)
              (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) x_2 ⋯)) :
          K)⁻¹ :
      K)
⊢ 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)

Tactic:
rw [Units.val_inv_eq_inv_val]

Premises used: Units.val_inv_eq_inv_val
-- Module: Mathlib.RingTheory.Localization.AsSubring
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)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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)
⊢ {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)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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
⊢ 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:
symm
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
⊢ 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:
apply mem_range_mapToFractionRing_iff_ofField

Premises used: Localization.subalgebra.mem_range_mapToFractionRing_iff_ofField
-- Module: Mathlib.RingTheory.Localization.AsSubring
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)
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.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 ⋯)}
      ⋯)
⊢ Eq (α := Subalgebra A K) (ofField K S hS) (subalgebra K S hS)

Tactic:
simp_rw [ofField, subalgebra, Subalgebra.copy_eq]

Premises used: Subalgebra.copy_eq, Localization.subalgebra.ofField, Localization.subalgebra
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
rw : IsLocalization.{u_1, u_2} S ↥(subalgebra K S hS)
⊢ IsLocalization.{u_1, u_2} S ↥(ofField K S hS)

Tactic:
rw [ofField_eq]

Premises used: Localization.subalgebra.ofField_eq
-- Module: Mathlib.RingTheory.Localization.AsSubring
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 ↥(subalgebra K S hS)

Tactic:
isLocalization_subalgebra K S hS

Premises used: Localization.subalgebra.isLocalization_subalgebra, Set.Mem
-- Module: Mathlib.RingTheory.Localization.AsSubring
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 ↥(subalgebra K S hS)

Tactic:
exact isLocalization_subalgebra K S hS

Premises used: Localization.subalgebra.isLocalization_subalgebra
-- Module: Mathlib.RingTheory.Localization.AsSubring
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

Tactic:
IsFractionRing.of_field S K fun z ↦ ?_

Premises used: Set.Mem, Membership.mem, IsFractionRing.of_field, Subtype
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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)
⊢ IsFractionRing (↥S) K

Tactic:
refine IsFractionRing.of_field S K fun z ↦ ?_

Premises used: Membership.mem, IsFractionRing.of_field, Subtype
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
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)
⊢ ∃ (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⟩

Premises used: IsFractionRing.div_surjective
-- Module: Mathlib.RingTheory.Localization.AsSubring
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 y : A
left : 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:
⟨algebraMap A S x, algebraMap A S y, eq.symm⟩

Premises used: Algebra.algebraMap, Membership.mem, Subtype, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.AsSubring
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 y : A
left : 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:
exact ⟨algebraMap A S x, algebraMap A S y, eq.symm⟩
-- Module: Mathlib.RingTheory.Localization.AsSubring
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
⊢ IsFractionRing (↥(ofField K S hS)) K

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ 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

Premises used: Algebra.algebraMap, RingHom.map_one, RingHom.map_zero
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
obtain : ∀ (t : ↥P.primeCompl) (ht : (↑t : R) * 0 = (↑t : R) * 1), False
⊢ False

Tactic:
obtain ⟨t, ht⟩ := (eq_iff_exists P.primeCompl S).1 hze

Premises used: Iff.mp, Ideal.primeCompl, IsLocalization.eq_iff_exists
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ (↑t : R) = 0

Tactic:
simpa using ht.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ (↑t : R) = 0

Tactic:
have htz : (t : R) = 0 := by simpa using ht.symm
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
htz : (↑t : R) = 0
⊢ False

Tactic:
t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

Premises used: Eq.rec, Ideal.zero_mem, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
htz : (↑t : R) = 0
⊢ False

Tactic:
exact t.2 (htz.symm ▸ P.zero_mem : ↑t ∈ P)

Premises used: Eq.rec, Ideal.zero_mem, Eq.symm, Subtype.property
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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)
obtain : ∀ (z : S) (hxyz : (x + y) * z = 1), False
⊢ False

Tactic:
obtain ⟨z, hxyz⟩ := isUnit_iff_exists_inv.1 hu

Premises used: isUnit_iff_exists_inv, Iff.mp
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
⊢ ∀ {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⟩
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
rcases : ∀ (rx : R) (sx : ↥P.primeCompl) (hrx : mk' S rx sx = x), False
⊢ False

Tactic:
rcases exists_mk'_eq P.primeCompl x with ⟨rx, sx, hrx⟩

Premises used: Ideal.primeCompl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Localization.AtPrime.Basic
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
rcases : ∀ (ry : R) (sy : ↥P.primeCompl) (hry : mk' S ry sy = y), False
⊢ False

Tactic:
rcases exists_mk'_eq P.primeCompl y with ⟨ry, sy, hry⟩

Premises used: Ideal.primeCompl, IsLocalization.exists_mk'_eq