awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
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)
⊢ 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)

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

Premises used: IsFractionRing.div_surjective, 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_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
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)
⊢ 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:
simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]

Premises used: map_div₀, IsScalarTower.algebraMap_apply
-- 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_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
⊢ 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 [← IsScalarTower.algebraMap_apply A C FC]

Premises used: IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ Eq (α := FB ≃ₐ[A] FC) (AlgEquiv.restrictScalars A (fieldEquivOfAlgEquiv FA FB FC f)) (algEquivOfAlgEquiv f)

Tactic:
ext
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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:
rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
b : B
⊢ Eq.{u_14 + 1} (α := FC)
    ((fieldEquivOfAlgEquiv FA FB FC f : (a : FB) → FC) ((algebraMap B FB : (a : B) → FB) b : FB) : FC)
    ((algebraMap C FC : (a : C) → FC) ((f : (a : B) → C) b : C) : FC)

Tactic:
ringEquivOfRingEquiv_algebraMap f.toRingEquiv b

Premises used: IsFractionRing.ringEquivOfRingEquiv_algebraMap, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ 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

Tactic:
ext x
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ 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:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
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 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:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ Eq (α := FB ≃ₐ[FA] FD) (fieldEquivOfAlgEquiv FA FB FD (f.trans g))
    (AlgEquiv.trans (fieldEquivOfAlgEquiv FA FB FC f) (fieldEquivOfAlgEquiv FA FC FD g))

Tactic:
ext x
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ 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:
obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x

Premises used: IsFractionRing.div_surjective, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
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 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:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
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 : B ≃ₐ[A] B
⊢ Eq.{u_11 + 1} (α := L ≃ₐ[K] L) ((fieldEquivOfAlgEquivHom K L : (a : B ≃ₐ[A] B) → L ≃ₐ[K] L) f : L ≃ₐ[K] L)
    (fieldEquivOfAlgEquiv K L L f : L ≃ₐ[K] L)

Tactic:
rfl

Premises used: IsFractionRing.fieldEquivOfAlgEquiv, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
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)
h₁ : ∀ (b : B), Eq (α := B) ((f : (a : B) → B) b : B) ((g : (a : B) → B) b : B)
⊢ f = g

Tactic:
ext b
-- Module: Mathlib.RingTheory.Localization.FractionRing
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)
b : B
⊢ Eq (α := B) ((f : (a : B) → B) b : B) ((g : (a : B) → B) b : B)

Tactic:
simpa using AlgEquiv.ext_iff.mp h (algebraMap B L b)

Premises used: Algebra.algebraMap, AlgEquiv.ext_iff, Iff.mp, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
h : R ≃+* P
⊢ IsLocalization.{u_1, u_2} (R := R) R⁰ S ↔ IsLocalization (Submonoid.map h (R⁰ : Submonoid R)) S

Tactic:
isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h

Premises used: IsLocalization.isLocalization_iff_of_base_ringEquiv, nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
h : R ≃+* P
h₁ : Eq (α := Submonoid P) (P⁰ : Submonoid P) (Submonoid.map h (R⁰ : Submonoid R))
⊢ IsLocalization.{u_1, u_2} (R := R) R⁰ S ↔ IsLocalization.{u_3, u_2} (R := P) P⁰ S

Tactic:
convert! isLocalization_iff_of_base_ringEquiv (nonZeroDivisors R) S h

Premises used: IsLocalization.isLocalization_iff_of_base_ringEquiv, nonZeroDivisors
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
h : R ≃+* P
⊢ Eq (α := Submonoid P) (P⁰ : Submonoid P) (Submonoid.map h (R⁰ : Submonoid R))

Tactic:
(MulEquivClass.map_nonZeroDivisors h).symm

Premises used: MulEquivClass.map_nonZeroDivisors, Eq.symm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
h : R ≃+* P
⊢ Eq (α := Submonoid P) (P⁰ : Submonoid P) (Submonoid.map h (R⁰ : Submonoid R))

Tactic:
exact (MulEquivClass.map_nonZeroDivisors h).symm

Premises used: MulEquivClass.map_nonZeroDivisors, Eq.symm
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
inl : Nontrivial R → Subsingleton S → False
inr : Subsingleton R → Nontrivial S → False
⊢ Nontrivial R ↔ Nontrivial S

Tactic:
by_contra! ⟨_, _⟩ | ⟨_, _⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Nontrivial R
right : Subsingleton S
inl : ∀ (c : ↥(R⁰ : Submonoid R)) (hc : (↑c : R) * 1 = (↑c : R) * 0), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := h.exists_of_eq (x := 1) (y := 0) (Subsingleton.elim _ _)

Premises used: Subsingleton.elim, IsLocalization.exists_of_eq
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Nontrivial R
right : Subsingleton S
c : ↥(R⁰ : Submonoid R)
hc : (↑c : R) * 1 = (↑c : R) * 0
⊢ False

Tactic:
simp at hc
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Subsingleton R
right : Nontrivial S
inr : Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑1 : R) : S) (0 : S)
⊢ False

Tactic:
apply (h.map_units S 1).ne_zero

Premises used: IsLocalization.map_units, IsUnit.ne_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
left : Subsingleton R
right : Nontrivial S
inr : Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) 0 : S) (0 : S)
inr₁ inr₂ : Eq.{u_9 + 1} (α := S) 0 0
⊢ Eq.{u_9 + 1} (α := S) ((algebraMap R S : (a : R) → S) (↑1 : R) : S) (0 : S)

Tactic:
rw [Subsingleton.eq_zero ((1 : nonZeroDivisors R) : R), map_zero]

Premises used: map_zero, Subsingleton.eq_zero, OfNat.ofNat, Subtype.val
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
S : Type u_9
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : IsFractionRing R S
hR : Nontrivial R
⊢ Nontrivial S

Tactic:
h.nontrivial_iff_nontrivial.mp hR

Premises used: IsFractionRing.nontrivial_iff_nontrivial, Iff.mp