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
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
s : Set L
hs : Eq (α := Subring L) (RingHom.range.{u_4, u_8} (R := A) g) (Subring.closure s)
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f) (Subfield.closure s)
have rw : Eq (α := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) (Subfield.closure s)
Tactic: rw [ringHom_fieldRange_eq_of_comp_eq h, hs]
-- 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
s : Set L
hs : Eq (α := Subring L) (RingHom.range.{u_4, u_8} (R := A) g) (Subring.closure s)
⊢ Eq (α := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) (Subfield.closure s)
have h₁ : ∀ (x : L),
  Membership.mem (γ := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) x ↔
    Membership.mem (γ := Subfield L) (Subfield.closure s) x
Tactic: ext
-- 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
s : Set L
hs : Eq (α := Subring L) (RingHom.range.{u_4, u_8} (R := A) g) (Subring.closure s)
x : L
⊢ Membership.mem (γ := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) x ↔
    Membership.mem (γ := Subfield L) (Subfield.closure s) x
have h₁ : (∃ (y : L),
    Membership.mem (γ := Subring L) (Subring.closure (↑(Subring.closure s) : Set L)) y ∧
      ∃ (z : L), Membership.mem (γ := Subring L) (Subring.closure (↑(Subring.closure s) : Set L)) z ∧ y / z = x) ↔
  ∃ (y : L),
    Membership.mem (γ := Subring L) (Subring.closure s) y ∧
      ∃ (z : L), Membership.mem (γ := Subring L) (Subring.closure s) z ∧ y / z = x
Tactic: simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
⊢ f1 = f2
have a : ∀ (z : K), Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) z : L) ((f2 : (a : K) → L) z : L)
Tactic: ext z
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
z : K
⊢ Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) z : L) ((f2 : (a : K) → L) z : L)
have a : ∀ (x y : A) (hy : Membership.mem (γ := Submonoid A) A⁰ y),
  Eq.{u_7 + 1} (α := L)
    ((f1 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
    ((f2 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
Tactic: obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A z
Cleared hypotheses: z
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
⊢ Eq.{u_7 + 1} (α := L)
    ((f1 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
    ((f2 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
have a : HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
  (f2 : (a : K) → L)
    (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
Tactic: rw [map_div₀, map_div₀, hf, hf]
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
a :
  HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    (f2 : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
⊢ Eq.{u_7 + 1} (α := L)
    ((f1 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
    ((f2 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
have a₁ : HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
  HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
Tactic: rw [map_div₀, map_div₀, hf, hf]
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
a :
  HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    (f2 : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
a₁ :
  HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
⊢ Eq.{u_7 + 1} (α := L)
    ((f1 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
    ((f2 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
have a₂ : HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
  HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
Tactic: rw [map_div₀, map_div₀, hf, hf]
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
f1 f2 : K →+* L
hf :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
x y : A
hy : Membership.mem (γ := Submonoid A) A⁰ y
a :
  HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    (f2 : (a : K) → L)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K))
a₁ :
  HDiv.hDiv (α := L) (β := L) ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
a₂ :
  HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f1 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
    HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
      ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
⊢ Eq.{u_7 + 1} (α := L)
    ((f1 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
    ((f2 : (a : K) → L)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap A K : (a : A) → K) x : K) ((algebraMap A K : (a : A) → K) y : K)) :
      L)
have a₃ : HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L) =
  HDiv.hDiv (α := L) (β := L) ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L)
    ((f2 : (a : K) → L) ((algebraMap A K : (a : A) → K) y : K) : L)
Tactic: rw [map_div₀, map_div₀, hf, hf]
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) = g
have a : ∀ (x : A),
  Eq.{u_7 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) : (a : A) → L) x : L)
    ((g : (a : A) → L) x : L)
Tactic: ext
-- 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
L : Type u_7
inst_2 : Field L
inst_3 : Algebra A K
inst_4 : IsFractionRing A K
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
s : Set L
hs : Eq (α := Subring L) (RingHom.range.{u_4, u_7} (R := A) g) (Subring.closure s)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) = g
have a : ∀ (x : A),
  Eq.{u_7 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) : (a : A) → L) x : L)
    ((g : (a : A) → L) x : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
K : Type u_9
B : Type u_10
L : Type u_11
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing K
inst_3 : CommRing L
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : Algebra B L
inst_7 : IsFractionRing B L
C : Type u_12
M : Type u_13
inst_8 : CommRing C
inst_9 : CommRing M
inst_10 : Algebra C M
inst_11 : IsFractionRing C M
f : A ≃+* B
g : B ≃+* C
⊢ Eq (α := K ≃+* M) (ringEquivOfRingEquiv (f.trans g))
    (RingEquiv.trans.{u_9, u_11, u_13} (S := L) (ringEquivOfRingEquiv f) (ringEquivOfRingEquiv g))
have h : ∀ (a : K),
  Eq.{u_13 + 1} (α := M) ((ringEquivOfRingEquiv (f.trans g) : (a : K) → M) a : M)
    ((RingEquiv.trans.{u_9, u_11, u_13} (S := L) (ringEquivOfRingEquiv f) (ringEquivOfRingEquiv g) : (a : K) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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_1 : Type u_4
inst_4 : CommRing A_1
K : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K
L : Type u_7
inst_8 : Field L
inst_9 : Algebra A_1 K
inst_10 : IsFractionRing A_1 K
g : A_1 →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst_11 : CommRing A
inst_12 : CommRing B
inst_13 : CommRing C
inst_14 : CommRing D
inst_15 : Algebra A B
inst_16 : Algebra A C
inst_17 : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst_18 : Field FA
inst_19 : Field FB
inst_20 : Field FC
inst_21 : Field FD
inst_22 : Algebra A FA
inst_23 : Algebra B FB
inst_24 : Algebra C FC
inst_25 : Algebra D FD
inst_26 : IsFractionRing A FA
inst_27 : IsFractionRing B FB
inst_28 : IsFractionRing C FC
inst_29 : IsFractionRing D FD
inst_30 : Algebra A FB
inst_31 : IsScalarTower A B FB
inst_32 : Algebra A FC
inst_33 : IsScalarTower A C FC
inst_34 : Algebra A FD
inst_35 : IsScalarTower A D FD
inst_36 : Algebra FA FB
inst_37 : IsScalarTower A FA FB
inst_38 : Algebra FA FC
inst_39 : IsScalarTower A FA FC
inst_40 : Algebra FA FD
inst_41 : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x : FA
⊢ Eq.{u_14 + 1} (α := FC)
    (Equiv.toFun.{u_13 + 1, u_14 + 1} (α := FB) (RingEquiv.toEquiv (ringEquivOfRingEquiv f.toRingEquiv) : FB ≃ FC)
        ((algebraMap FA FB : (a : FA) → FB) x : FB) :
      FC)
    ((algebraMap FA FC : (a : FA) → FC) x : FC)
have obtain : ∀ (x y : A),
  Eq.{u_14 + 1} (α := FC)
    (Equiv.toFun.{u_13 + 1, u_14 + 1} (α := FB) (RingEquiv.toEquiv (ringEquivOfRingEquiv f.toRingEquiv) : FB ≃ FC)
        ((algebraMap FA FB : (a : FA) → FB)
            (HDiv.hDiv (α := FA) (β := FA) ((algebraMap A FA : (a : A) → FA) x : FA)
              ((algebraMap A FA : (a : A) → FA) y : FA)) :
          FB) :
      FC)
    ((algebraMap FA FC : (a : FA) → FC)
        (HDiv.hDiv (α := FA) (β := FA) ((algebraMap A FA : (a : A) → FA) x : FA)
          ((algebraMap A FA : (a : A) → FA) y : FA)) :
      FC)
Tactic: obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective A x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
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_1 : Type u_4
inst_4 : CommRing A_1
K : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K
L : Type u_7
inst_8 : Field L
inst_9 : Algebra A_1 K
inst_10 : IsFractionRing A_1 K
g : A_1 →+* L
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst_11 : CommRing A
inst_12 : CommRing B
inst_13 : CommRing C
inst_14 : CommRing D
inst_15 : Algebra A B
inst_16 : Algebra A C
inst_17 : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst_18 : Field FA
inst_19 : Field FB
inst_20 : Field FC
inst_21 : Field FD
inst_22 : Algebra A FA
inst_23 : Algebra B FB
inst_24 : Algebra C FC
inst_25 : Algebra D FD
inst_26 : IsFractionRing A FA
inst_27 : IsFractionRing B FB
inst_28 : IsFractionRing C FC
inst_29 : IsFractionRing D FD
inst_30 : Algebra A FB
inst_31 : IsScalarTower A B FB
inst_32 : Algebra A FC
inst_33 : IsScalarTower A C FC
inst_34 : Algebra A FD
inst_35 : IsScalarTower A D FD
inst_36 : Algebra FA FB
inst_37 : IsScalarTower A FA FB
inst_38 : Algebra FA FC
inst_39 : IsScalarTower A FA FC
inst_40 : Algebra FA FD
inst_41 : IsScalarTower A FA FD
f : B ≃ₐ[A] C
x y : A
⊢ Eq.{u_14 + 1} (α := FC)
    (Equiv.toFun.{u_13 + 1, u_14 + 1} (α := FB) (RingEquiv.toEquiv (ringEquivOfRingEquiv f.toRingEquiv) : FB ≃ FC)
        ((algebraMap FA FB : (a : FA) → FB)
            (HDiv.hDiv (α := FA) (β := FA) ((algebraMap A FA : (a : A) → FA) x : FA)
              ((algebraMap A FA : (a : A) → FA) y : FA)) :
          FB) :
      FC)
    ((algebraMap FA FC : (a : FA) → FC)
        (HDiv.hDiv (α := FA) (β := FA) ((algebraMap A FA : (a : A) → FA) x : FA)
          ((algebraMap A FA : (a : A) → FA) y : FA)) :
      FC)
have simp_rw : Equiv.toFun (RingEquiv.toEquiv (ringEquivOfRingEquiv f.toRingEquiv))
    (HDiv.hDiv (α := FB) (β := FB) ((algebraMap B FB : (a : B) → FB) ((algebraMap A B : (a : A) → B) x : B) : FB)
      ((algebraMap B FB : (a : B) → FB) ((algebraMap A B : (a : A) → B) y : B) : FB)) =
  HDiv.hDiv (α := FC) (β := FC) ((algebraMap A FC : (a : A) → FC) x : FC) ((algebraMap A FC : (a : A) → FC) y : FC)
Tactic: simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : Algebra A B
inst_4 : Algebra A C
FA : Type u_12
FB : Type u_13
FC : Type u_14
inst_5 : Field FA
inst_6 : Field FB
inst_7 : Field FC
inst_8 : Algebra A FA
inst_9 : Algebra B FB
inst_10 : Algebra C FC
inst_11 : IsFractionRing A FA
inst_12 : IsFractionRing B FB
inst_13 : IsFractionRing C FC
inst_14 : Algebra A FB
inst_15 : IsScalarTower A B FB
inst_16 : Algebra A FC
inst_17 : IsScalarTower A C FC
inst_18 : Algebra FA FB
inst_19 : IsScalarTower A FA FB
inst_20 : Algebra FA FC
inst_21 : IsScalarTower A FA FC
f : B ≃ₐ[A] C
⊢ Eq (α := FB ≃ₐ[A] FC) (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) (algEquivOfAlgEquiv f)
have h : ∀ (a : FB),
  Eq.{u_14 + 1} (α := FC) ((AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f) : (a : FB) → FC) a : FC)
    ((algEquivOfAlgEquiv f : (a : FB) → FC) a : FC)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
FA : Type u_12
FB : Type u_13
inst_3 : Field FA
inst_4 : Field FB
inst_5 : Algebra A FA
inst_6 : Algebra B FB
inst_7 : IsFractionRing A FA
inst_8 : IsFractionRing B FB
inst_9 : Algebra A FB
inst_10 : IsScalarTower A B FB
inst_11 : Algebra FA FB
inst_12 : IsScalarTower A FA FB
⊢ Eq (α := FB ≃ₐ[FA] FB)
    (fieldEquivOfAlgEquiv.{u_8, u_9, u_9, u_12, u_13, u_13} (A := A) (B := B) FA FB FB AlgEquiv.refl) AlgEquiv.refl
have h : ∀ (x : FB),
  Eq (α := FB)
    ((fieldEquivOfAlgEquiv.{u_8, u_9, u_9, u_12, u_13, u_13} (A := A) (B := B) FA FB FB AlgEquiv.refl : (a : FB) → FB)
        x :
      FB)
    ((AlgEquiv.refl : (a : FB) → FB) x : FB)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
FA : Type u_12
FB : Type u_13
inst_3 : Field FA
inst_4 : Field FB
inst_5 : Algebra A FA
inst_6 : Algebra B FB
inst_7 : IsFractionRing A FA
inst_8 : IsFractionRing B FB
inst_9 : Algebra A FB
inst_10 : IsScalarTower A B FB
inst_11 : Algebra FA FB
inst_12 : IsScalarTower A FA FB
x : FB
⊢ Eq (α := FB)
    ((fieldEquivOfAlgEquiv.{u_8, u_9, u_9, u_12, u_13, u_13} (A := A) (B := B) FA FB FB AlgEquiv.refl : (a : FB) → FB)
        x :
      FB)
    ((AlgEquiv.refl : (a : FB) → FB) x : FB)
have h : ∀ (x y : B),
  Eq (α := FB)
    ((fieldEquivOfAlgEquiv.{u_8, u_9, u_9, u_12, u_13, u_13} (A := A) (B := B) FA FB FB AlgEquiv.refl : (a : FB) → FB)
        (HDiv.hDiv (α := FB) (β := FB) ((algebraMap B FB : (a : B) → FB) x : FB)
          ((algebraMap B FB : (a : B) → FB) y : FB)) :
      FB)
    ((AlgEquiv.refl : (a : FB) → FB)
        (HDiv.hDiv (α := FB) (β := FB) ((algebraMap B FB : (a : B) → FB) x : FB)
          ((algebraMap B FB : (a : B) → FB) y : FB)) :
      FB)
Tactic: obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : CommRing D
inst_4 : Algebra A B
inst_5 : Algebra A C
inst_6 : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst_7 : Field FA
inst_8 : Field FB
inst_9 : Field FC
inst_10 : Field FD
inst_11 : Algebra A FA
inst_12 : Algebra B FB
inst_13 : Algebra C FC
inst_14 : Algebra D FD
inst_15 : IsFractionRing A FA
inst_16 : IsFractionRing B FB
inst_17 : IsFractionRing C FC
inst_18 : IsFractionRing D FD
inst_19 : Algebra A FB
inst_20 : IsScalarTower A B FB
inst_21 : Algebra A FC
inst_22 : IsScalarTower A C FC
inst_23 : Algebra A FD
inst_24 : IsScalarTower A D FD
inst_25 : Algebra FA FB
inst_26 : IsScalarTower A FA FB
inst_27 : Algebra FA FC
inst_28 : IsScalarTower A FA FC
inst_29 : Algebra FA FD
inst_30 : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
⊢ Eq (α := FB ≃ₐ[FA] FD) (fieldEquivOfAlgEquiv FA FB FD (f.trans g))
    (AlgEquiv.trans (fieldEquivOfAlgEquiv FA FB FC f) (fieldEquivOfAlgEquiv FA FC FD g))
have h : ∀ (x : FB),
  Eq.{u_15 + 1} (α := FD) ((fieldEquivOfAlgEquiv FA FB FD (f.trans g) : (a : FB) → FD) x : FD)
    ((AlgEquiv.trans (fieldEquivOfAlgEquiv FA FB FC f) (fieldEquivOfAlgEquiv FA FC FD g) : (a : FB) → FD) x : FD)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
D : Type u_11
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
inst_3 : CommRing D
inst_4 : Algebra A B
inst_5 : Algebra A C
inst_6 : Algebra A D
FA : Type u_12
FB : Type u_13
FC : Type u_14
FD : Type u_15
inst_7 : Field FA
inst_8 : Field FB
inst_9 : Field FC
inst_10 : Field FD
inst_11 : Algebra A FA
inst_12 : Algebra B FB
inst_13 : Algebra C FC
inst_14 : Algebra D FD
inst_15 : IsFractionRing A FA
inst_16 : IsFractionRing B FB
inst_17 : IsFractionRing C FC
inst_18 : IsFractionRing D FD
inst_19 : Algebra A FB
inst_20 : IsScalarTower A B FB
inst_21 : Algebra A FC
inst_22 : IsScalarTower A C FC
inst_23 : Algebra A FD
inst_24 : IsScalarTower A D FD
inst_25 : Algebra FA FB
inst_26 : IsScalarTower A FA FB
inst_27 : Algebra FA FC
inst_28 : IsScalarTower A FA FC
inst_29 : Algebra FA FD
inst_30 : IsScalarTower A FA FD
f : B ≃ₐ[A] C
g : C ≃ₐ[A] D
x : FB
⊢ Eq.{u_15 + 1} (α := FD) ((fieldEquivOfAlgEquiv FA FB FD (f.trans g) : (a : FB) → FD) x : FD)
    ((AlgEquiv.trans (fieldEquivOfAlgEquiv FA FB FC f) (fieldEquivOfAlgEquiv FA FC FD g) : (a : FB) → FD) x : FD)
have h : ∀ (x y : B),
  Eq.{u_15 + 1} (α := FD)
    ((fieldEquivOfAlgEquiv FA FB FD (f.trans g) : (a : FB) → FD)
        (HDiv.hDiv (α := FB) (β := FB) ((algebraMap B FB : (a : B) → FB) x : FB)
          ((algebraMap B FB : (a : B) → FB) y : FB)) :
      FD)
    ((AlgEquiv.trans (fieldEquivOfAlgEquiv FA FB FC f) (fieldEquivOfAlgEquiv FA FC FD g) : (a : FB) → FD)
        (HDiv.hDiv (α := FB) (β := FB) ((algebraMap B FB : (a : B) → FB) x : FB)
          ((algebraMap B FB : (a : B) → FB) y : FB)) :
      FD)
Tactic: obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Localization.FractionRing (goal)
Goal:
A : Type u_8
B : Type u_9
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
K : Type u_10
L : Type u_11
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : Algebra B L
inst_7 : IsFractionRing A K
inst_8 : IsFractionRing B L
inst_9 : Algebra A L
inst_10 : IsScalarTower A B L
inst_11 : Algebra K L
inst_12 : IsScalarTower A K L
f g : B ≃ₐ[A] B
h :
  Eq.{u_11 + 1} (α := L ≃ₐ[K] L) ((fieldEquivOfAlgEquivHom K L : (a : B ≃ₐ[A] B) → L ≃ₐ[K] L) f : L ≃ₐ[K] L)
    ((fieldEquivOfAlgEquivHom K L : (a : B ≃ₐ[A] B) → L ≃ₐ[K] L) g : L ≃ₐ[K] L)
⊢ f = g
have h₁ : ∀ (b : B), Eq (α := B) ((f : (a : B) → B) b : B) ((g : (a : B) → B) b : B)
Tactic: ext b