awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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₂)
have 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₂)
Tactic: obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective A x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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₂
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₂)
have simp_rw : HDiv.hDiv (α := L₂) (β := L₂)
    ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : K₂) : L₂)
    ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : K₂) : L₂) =
  HDiv.hDiv (α := L₂) (β := L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
Tactic: simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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₂
r s : A
hs : Membership.mem (γ := Submonoid A) A⁰ s
simp_rw :
  HDiv.hDiv (α := L₂) (β := L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((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₂)
            (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₂)
have simp_rw₁ : HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) r : K₂) : L₂)
    ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) s : K₂) : L₂) =
  HDiv.hDiv (α := L₂) (β := L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
Tactic: simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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₂
r s : A
hs : Membership.mem (γ := Submonoid A) A⁰ s
simp_rw :
  HDiv.hDiv (α := L₂) (β := L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
simp_rw₁ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) r : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) s : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((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₂)
            (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₂)
have simp_rw₂ : HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
  HDiv.hDiv (α := L₂) (β := L₂) ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) r : L₁) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) s : L₁) : L₂)
Tactic: simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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₂
r s : A
hs : Membership.mem (γ := Submonoid A) A⁰ s
simp_rw :
  HDiv.hDiv (α := L₂) (β := L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((e : (a : K₁) → K₂) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
simp_rw₁ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) r : K₂) : L₂)
      ((algebraMap K₂ L₂ : (a : K₂) → L₂) ((algebraMap A K₂ : (a : A) → K₂) s : K₂) : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) r : K₁) : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap K₁ L₁ : (a : K₁) → L₁) ((algebraMap A K₁ : (a : A) → K₁) s : K₁) : L₁) : L₂)
simp_rw₂ :
  HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
    HDiv.hDiv (α := L₂) (β := L₂) ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) r : L₁) : L₂)
      ((f : (a : L₁) → L₂) ((algebraMap A L₁ : (a : A) → L₁) s : L₁) : L₂)
⊢ 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₂)
have simp_rw₃ : HDiv.hDiv (α := L₂) (β := L₂) ((algebraMap A L₂ : (a : A) → L₂) r : L₂) ((algebraMap A L₂ : (a : A) → L₂) s : L₂) =
  HDiv.hDiv (α := L₂) (β := L₂)
    ((f : (a : L₁) → L₂) ((algebraMap B L₁ : (a : B) → L₁) ((algebraMap A B : (a : A) → B) r : B) : L₁) : L₂)
    ((f : (a : L₁) → L₂) ((algebraMap B L₁ : (a : B) → L₁) ((algebraMap A B : (a : A) → B) s : B) : L₁) : L₂)
Tactic: simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
    IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
⊢ Membership.mem (γ := Subfield K)
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))) z
have 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))
Tactic: obtain ⟨_, _, -, rfl⟩ := div_surjective A z
Cleared hypotheses: z, h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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 (γ := 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))
have 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)
Tactic: apply div_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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)
⊢ 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))
have 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)
Tactic: apply div_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw : Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₁ : Eq (α := Subfield L)
  (Subfield.map.{u_5, u_8} (K := K) f
    (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₁ :
  Eq (α := Subfield L)
    (Subfield.map.{u_5, u_8} (K := K) f
      (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₂ : Eq (α := Subfield L)
  (Subfield.closure
    (Set.image.{u_5, u_8} (α := K) (⇑f : (a : K) → L)
      (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₁ :
  Eq (α := Subfield L)
    (Subfield.map.{u_5, u_8} (K := K) f
      (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₂ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.image.{u_5, u_8} (α := K) (⇑f : (a : K) → L)
        (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₃ : Eq (α := Subfield L)
  (Subfield.closure
    (Set.range.{u_8, u_4 + 1} (ι := A)
      (Function.comp.{u_4 + 1, u_5 + 1, u_8 + 1} (β := K) (⇑f : (a : K) → L) (⇑(algebraMap A K) : (a : A) → K))))
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₁ :
  Eq (α := Subfield L)
    (Subfield.map.{u_5, u_8} (K := K) f
      (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₂ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.image.{u_5, u_8} (α := K) (⇑f : (a : K) → L)
        (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₃ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.range.{u_8, u_4 + 1} (ι := A)
        (Function.comp.{u_4 + 1, u_5 + 1, u_8 + 1} (β := K) (⇑f : (a : K) → L) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₄ : Eq (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑(f.comp (algebraMap A K)) : (a : A) → L)))
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₁ :
  Eq (α := Subfield L)
    (Subfield.map.{u_5, u_8} (K := K) f
      (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₂ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.image.{u_5, u_8} (α := K) (⇑f : (a : K) → L)
        (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₃ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.range.{u_8, u_4 + 1} (ι := A)
        (Function.comp.{u_4 + 1, u_5 + 1, u_8 + 1} (β := K) (⇑f : (a : K) → L) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₄ :
  Eq (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑(f.comp (algebraMap A K)) : (a : A) → L)))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₅ : Eq (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑g : (a : A) → L)))
  (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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
L : Type u_8
inst_4 : Field L
g : A →+* L
f : K →+* L
h : f.comp (algebraMap A K) = g
rw :
  Eq (α := Subfield L) (Subfield.map.{u_5, u_8} (K := K) f ⊤)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₁ :
  Eq (α := Subfield L)
    (Subfield.map.{u_5, u_8} (K := K) f
      (Subfield.closure (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₂ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.image.{u_5, u_8} (α := K) (⇑f : (a : K) → L)
        (Set.range.{u_5, u_4 + 1} (ι := A) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₃ :
  Eq (α := Subfield L)
    (Subfield.closure
      (Set.range.{u_8, u_4 + 1} (ι := A)
        (Function.comp.{u_4 + 1, u_5 + 1, u_8 + 1} (β := K) (⇑f : (a : K) → L) (⇑(algebraMap A K) : (a : A) → K))))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₄ :
  Eq (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑(f.comp (algebraMap A K)) : (a : A) → L)))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
rw₅ :
  Eq (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑g : (a : A) → L)))
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f)
    (Subfield.closure (↑(RingHom.range.{u_4, u_8} (R := A) g) : Set L))
have rw₆ : Eq.{u_8 + 1} (α := Subfield L) (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑g : (a : A) → L)))
  (Subfield.closure (Set.range.{u_8, u_4 + 1} (ι := A) (⇑g : (a : A) → L)))
Tactic: rw [f.fieldRange_eq_map, ← closure_range_algebraMap A K,
    f.map_field_closure, ← Set.range_comp, ← f.coe_comp, h, g.coe_range]