awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
⊢ IsDomain K

Tactic:
isDomain_of_le_nonZeroDivisors _ (le_refl (nonZeroDivisors A))

Premises used: le_refl, IsLocalization.isDomain_of_le_nonZeroDivisors, nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
rw :
  x *
      HMul.hMul (β := K)
        (mk' K (↑(sec A⁰ x).2 : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯))
        ((algebraMap A K : (a : A) → K)
            (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) :
              A) :
          K) =
    (algebraMap A K : (a : A) → K)
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)
⊢ x * IsFractionRing.inv A x = 1

Tactic:
rw [IsFractionRing.inv, dif_neg hx, ←
    IsUnit.mul_left_inj
      (map_units K
        ⟨(sec _ x).1,
          mem_nonZeroDivisors_iff_ne_zero.2 fun h0 =>
            hx <| eq_zero_of_fst_eq_zero (sec_spec (nonZeroDivisors A) x) h0⟩),
    one_mul, mul_assoc]

Premises used: Iff.mpr, IsLocalization.sec, mul_assoc, nonZeroDivisors, dif_neg, Prod.fst, Subtype.mk, IsLocalization.eq_zero_of_fst_eq_zero, IsLocalization.sec_spec, IsFractionRing.inv, IsLocalization.map_units, mem_nonZeroDivisors_iff_ne_zero, IsUnit.mul_left_inj, one_mul
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
rw :
  x =
    mk'.{u_4, u_5} (R := A) (M := A⁰) K
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)
      (sec A⁰ x).2
⊢ x *
      HMul.hMul (β := K)
        (mk' K (↑(sec A⁰ x).2 : A)
          (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯))
        ((algebraMap A K : (a : A) → K)
            (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) :
              A) :
          K) =
    (algebraMap A K : (a : A) → K)
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)

Tactic:
rw [mk'_spec, ← eq_mk'_iff_mul_eq]

Premises used: IsLocalization.eq_mk'_iff_mul_eq, IsLocalization.mk'_spec
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
⊢ x =
    mk'.{u_4, u_5} (R := A) (M := A⁰) K
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)
      (sec A⁰ x).2

Tactic:
(mk'_sec _ x).symm

Premises used: IsLocalization.mk'_sec, Eq.symm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : CommRing K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
inst_4 : IsDomain A
x : K
hx : x ≠ 0
⊢ x =
    mk'.{u_4, u_5} (R := A) (M := A⁰) K
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) (sec A⁰ x).1 ⋯) : A)
      (sec A⁰ x).2

Tactic:
exact (mk'_sec _ x).symm

Premises used: IsLocalization.mk'_sec, Eq.symm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : IsDomain A
rw :
  Eq.{u_5 + 1} (α := K)
    (if h : Eq.{u_5 + 1} (α := K) 0 0 then 0
    else
      mk' K (↑(sec.{u_4, u_5} A⁰ (S := K) 0).2 : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x)
          (sec.{u_4, u_5} A⁰ (S := K) 0).1 ⋯))
    0
⊢ Eq.{u_5 + 1} (α := K) (IsFractionRing.inv A 0) 0

Tactic:
rw [IsFractionRing.inv]

Premises used: IsFractionRing.inv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : IsDomain A
⊢ Eq.{u_5 + 1} (α := K)
    (if h : Eq.{u_5 + 1} (α := K) 0 0 then 0
    else
      mk' K (↑(sec.{u_4, u_5} A⁰ (S := K) 0).2 : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x)
          (sec.{u_4, u_5} A⁰ (S := K) 0).1 ⋯))
    0

Tactic:
dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
inst_5 : CommRing K
inst_6 : Algebra R K
inst_7 : IsFractionRing R K
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : IsDomain A
⊢ Eq.{u_5 + 1} (α := K)
    (if h : Eq.{u_5 + 1} (α := K) 0 0 then 0
    else
      mk' K (↑(sec.{u_4, u_5} A⁰ (S := K) 0).2 : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x)
          (sec.{u_4, u_5} A⁰ (S := K) 0).1 ⋯))
    0

Tactic:
exact dif_pos rfl

Premises used: dif_pos, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
r s : A
hs : Membership.mem (γ := Submonoid A) A⁰ s
⊢ mk' K r (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) s hs) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) r : K) ((algebraMap A K : (a : A) → K) s : K)

Tactic:
haveI := (algebraMap A K).domain_nontrivial
  mk'_eq_iff_eq_mul.2 <|
    (div_mul_cancel₀ (algebraMap A K r)
        (IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hs)).symm

Premises used: Iff.mpr, div_mul_cancel₀, Algebra.algebraMap, IsLocalization.mk'_eq_iff_eq_mul, IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors, Eq.symm, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
r : A
s : ↥A⁰
⊢ mk' K r s =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) r : K) ((algebraMap A K : (a : A) → K) (↑s : A) : K)

Tactic:
mk'_mk_eq_div s.2

Premises used: Set.Mem, IsFractionRing.mk'_mk_eq_div, Subtype.property
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
z : K
x y : A
hy : Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) y
h : mk' K x (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) y hy) = z
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K)
          ((algebraMap A K : (a : A) → K)
              (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (A⁰ : Submonoid A) x) y hy) : A) :
            K) =
        z),
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K) = z
⊢ HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K) = z

Tactic:
rwa [mk'_eq_div] at h

Premises used: IsFractionRing.mk'_eq_div
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
L : Type u_7
inst_1 : Field L
g : A →+* L
hg : Function.Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
y : ↥A⁰
⊢ IsUnit.{u_7} (M := L) ((g : (a : A) → L) (↑y : A) : L)

Tactic:
haveI := g.domain_nontrivial
  IsUnit.mk0 (g y) <|
    show g.toMonoidWithZeroHom y ≠ 0 from map_ne_zero_of_mem_nonZeroDivisors g hg y.2

Premises used: map_ne_zero_of_mem_nonZeroDivisors, IsUnit.mk0, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : R
y : ↥R⁰
⊢ Nontrivial R

Tactic:
haveI := (algebraMap R K).domain_nontrivial
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
K : Type u_5
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsFractionRing R K
x : R
y : ↥R⁰
this : Nontrivial R
⊢ mk' K x y = 0 ↔ x = 0

Tactic:
simp [nonZeroDivisors.ne_zero]

Premises used: nonZeroDivisors.ne_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
⊢ Nontrivial A

Tactic:
haveI := (algebraMap A K).domain_nontrivial
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : x = (↑y : A)
rw : mk' K (↑y : A) y = 1
rw₁ rw₂ : Eq.{u_5 + 1} (α := K) 1 1
⊢ mk' K x y = 1

Tactic:
rw [hxy, mk'_self']

Premises used: IsLocalization.mk'_self'
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
refine : mk' K x y = 1 → x = (↑y : A)
⊢ mk' K x y = 1 ↔ x = (↑y : A)

Tactic:
refine ⟨?_, fun hxy => by rw [hxy, mk'_self']⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : mk' K x y = 1
⊢ Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)

Tactic:
have hy : (algebraMap A K) ↑y ≠ (0 : K) :=
    IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors y.property
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : mk' K x y = 1
hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) (↑y : A) : K)

Tactic:
rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy

Premises used: IsFractionRing.mk'_eq_div, div_eq_one_iff_eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : mk' K x y = 1
hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
hxy₁ : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) (↑y : A) : K)
⊢ Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)

Tactic:
rw [IsFractionRing.mk'_eq_div, div_eq_one_iff_eq hy] at hxy

Premises used: IsFractionRing.mk'_eq_div, div_eq_one_iff_eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) (↑y : A) : K)
hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
⊢ x = (↑y : A)

Tactic:
IsFractionRing.injective A K hxy

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
x : A
y : ↥A⁰
this : Nontrivial A
hxy : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) (↑y : A) : K)
hy : Ne.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (↑y : A) : K) (0 : K)
⊢ x = (↑y : A)

Tactic:
exact IsFractionRing.injective A K hxy

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
⊢ IsFractionRing A L

Tactic:
IsFractionRing.of_algEquiv <| .symm <| .ofBijective f ⟨f.injective, fun x ↦ ?_⟩

Premises used: AlgEquiv.symm, AlgEquiv.ofBijective, IsFractionRing.of_algEquiv, RingHom.injective, AlgHom.toRingHom, And.intro
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
refine : ∀ (x : K), ∃ (a : L), (f : (a : L) → K) a = x
⊢ IsFractionRing A L

Tactic:
refine IsFractionRing.of_algEquiv <| .symm <| .ofBijective f ⟨f.injective, fun x ↦ ?_⟩

Premises used: IsFractionRing.of_algEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
x : K
obtain :
  ∀ (x y : A) (hy : Membership.mem (γ := Submonoid A) A⁰ y),
    ∃ (a : L),
      (f : (a : L) → K) a =
        HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)
⊢ ∃ (a : L), (f : (a : L) → K) a = x

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
⊢ (f : (a : L) → K)
      (HDiv.hDiv (α := L) (β := L) ((algebraMap A L : (a : A) → L) x : L) ((algebraMap A L : (a : A) → L) y : L)) =
    HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
inst_5 : Algebra A L
f : L →ₐ[A] K
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
⊢ ∃ (a : L),
    (f : (a : L) → K) a =
      HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)

Tactic:
exact ⟨algebraMap A L x / algebraMap A L y, by simp⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
B : Type u_6
inst_1 : CommRing B
inst_2 : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Algebra A K₁
inst_6 : Algebra A K₂
inst_7 : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst_8 : Field L₁
inst_9 : Field L₂
inst_10 : Algebra B L₁
inst_11 : Algebra B L₂
inst_12 : Algebra K₁ L₁
inst_13 : Algebra K₂ L₂
inst_14 : Algebra A L₁
inst_15 : Algebra A L₂
inst_16 : IsScalarTower A K₁ L₁
inst_17 : IsScalarTower A K₂ L₂
inst_18 : IsScalarTower A B L₁
inst_19 : IsScalarTower A B L₂
e : K₁ →ₐ[A] K₂
f : L₁ →ₐ[B] L₂
x : K₁
obtain :
  ∀ (r s : A) (hs : Membership.mem (γ := Submonoid A) A⁰ s),
    Eq.{u_11 + 1} (α := L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂)
          ((e : (a : K₁) → K₂)
              (HDiv.hDiv (α := K₁) (β := K₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁)
                ((algebraMap A K₁ : (a : A) → K₁) s : K₁)) :
            K₂) :
        L₂)
      ((f : (a : L₁) → L₂)
          ((algebraMap K₁ L₁ : (a : K₁) → L₁)
              (HDiv.hDiv (α := K₁) (β := K₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁)
                ((algebraMap A K₁ : (a : A) → K₁) s : K₁)) :
            L₁) :
        L₂)
⊢ Eq.{u_11 + 1} (α := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) x : K₂) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) x : L₁) : L₂)

Tactic:
obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective A x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
B : Type u_6
inst_1 : CommRing B
inst_2 : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Algebra A K₁
inst_6 : Algebra A K₂
inst_7 : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst_8 : Field L₁
inst_9 : Field L₂
inst_10 : Algebra B L₁
inst_11 : Algebra B L₂
inst_12 : Algebra K₁ L₁
inst_13 : Algebra K₂ L₂
inst_14 : Algebra A L₁
inst_15 : Algebra A L₂
inst_16 : IsScalarTower A K₁ L₁
inst_17 : IsScalarTower A K₂ L₂
inst_18 : IsScalarTower A B L₁
inst_19 : IsScalarTower A B L₂
e : K₁ ≃ₐ[A] K₂
f : L₁ ≃ₐ[B] L₂
x : K₁
⊢ Eq.{u_11 + 1} (α := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) x : K₂) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) x : L₁) : L₂)

Tactic:
algHom_commutes e.toAlgHom f.toAlgHom _

Premises used: AlgEquiv.toAlgHom, IsFractionRing.algHom_commutes
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
B : Type u_6
inst_1 : CommRing B
inst_2 : Algebra A B
K₁ : Type u_8
K₂ : Type u_9
inst_3 : Field K₁
inst_4 : Field K₂
inst_5 : Algebra A K₁
inst_6 : Algebra A K₂
inst_7 : IsFractionRing A K₁
L₁ : Type u_10
L₂ : Type u_11
inst_8 : Field L₁
inst_9 : Field L₂
inst_10 : Algebra B L₁
inst_11 : Algebra B L₂
inst_12 : Algebra K₁ L₁
inst_13 : Algebra K₂ L₂
inst_14 : Algebra A L₁
inst_15 : Algebra A L₂
inst_16 : IsScalarTower A K₁ L₁
inst_17 : IsScalarTower A K₂ L₂
inst_18 : IsScalarTower A B L₁
inst_19 : IsScalarTower A B L₂
e : K₁ ≃ₐ[A] K₂
f : L₁ ≃ₐ[B] L₂
x : K₁
⊢ Eq.{u_11 + 1} (α := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) x : K₂) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) x : L₁) : L₂)

Tactic:
exact algHom_commutes e.toAlgHom f.toAlgHom _

Premises used: AlgEquiv.toAlgHom, IsFractionRing.algHom_commutes
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
z : K
h : Membership.mem (γ := Subfield K) ⊤ z
obtain :
  ∀ (w w_1 : A),
    Membership.mem (γ := Subfield K) ⊤
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K)) →
      Membership.mem (γ := Subfield K)
        (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
⊢ Membership.mem (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))) z

Tactic:
obtain ⟨_, _, -, rfl⟩ := div_surjective A z

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
w w_1 : A
h :
  Membership.mem (γ := Subfield K) ⊤
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
hx :
  Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w : K)
hy :
  Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w_1 : K)
⊢ Membership.mem (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))

Tactic:
apply div_mem

Premises used: div_mem
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
w w_1 : A
h :
  Membership.mem (γ := Subfield K) ⊤
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
⊢ Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w : K)

Tactic:
Subfield.subset_closure ⟨_, rfl⟩

Premises used: Exists.intro, Subfield.subset_closure, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
w w_1 : A
h :
  Membership.mem (γ := Subfield K) ⊤
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
⊢ Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w : K)

Tactic:
exact Subfield.subset_closure ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
w w_1 : A
h :
  Membership.mem (γ := Subfield K) ⊤
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
⊢ Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w_1 : K)

Tactic:
Subfield.subset_closure ⟨_, rfl⟩

Premises used: Exists.intro, Subfield.subset_closure, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_4
inst : CommRing A
K : Type u_5
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsFractionRing A K
w w_1 : A
h :
  Membership.mem (γ := Subfield K) ⊤
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) w : K) ((algebraMap A K : (a : A) → K) w_1 : K))
⊢ Membership.mem.{u_5, u_5} (α := K) (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K)))
    ((algebraMap A K : (a : A) → K) w_1 : K)

Tactic:
exact Subfield.subset_closure ⟨_, rfl⟩