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 : 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))
rw₆ 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)))
⊢ 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))

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]

Premises used: Set.range_comp, IsFractionRing.closure_range_algebraMap, RingHom.fieldRange_eq_map, RingHom.coe_comp, RingHom.map_field_closure, RingHom.coe_range
-- 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
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)
rw : Eq (α := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) (Subfield.closure s)
⊢ Eq (α := Subfield L) (RingHom.fieldRange.{u_5, u_8} (K := K) f) (Subfield.closure s)

Tactic:
rw [ringHom_fieldRange_eq_of_comp_eq h, hs]

Premises used: IsFractionRing.ringHom_fieldRange_eq_of_comp_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
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)
h₁ :
  ∀ (x : L),
    Membership.mem (γ := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) x ↔
      Membership.mem (γ := Subfield L) (Subfield.closure s) x
⊢ Eq (α := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) (Subfield.closure s)

Tactic:
ext
-- 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
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
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
⊢ Membership.mem (γ := Subfield L) (Subfield.closure (↑(Subring.closure s) : Set L)) x ↔
    Membership.mem (γ := Subfield L) (Subfield.closure s) x

Tactic:
simp_rw [Subfield.mem_closure_iff, Subring.closure_eq]

Premises used: Subfield.mem_closure_iff, Subring.closure_eq
-- 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
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
f : K →+* L
hf1 :
  ∀ (x : A),
    Eq.{u_7 + 1} (α := L) ((f : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L) ((g : (a : A) → L) x : L)
⊢ lift hg = f

Tactic:
IsLocalization.lift_unique _ hf1

Premises used: IsLocalization.lift_unique, IsFractionRing.lift
-- 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
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)
a : ∀ (z : K), Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) z : L) ((f2 : (a : K) → L) z : L)
⊢ f1 = f2

Tactic:
ext z
-- 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
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
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)
⊢ Eq.{u_7 + 1} (α := L) ((f1 : (a : K) → L) z : L) ((f2 : (a : K) → L) z : L)

Tactic:
obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.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
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)
a₃ 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)
⊢ 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:
rw [map_div₀, map_div₀, hf, hf]

Premises used: map_div₀
-- 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
⊢ Injective (β := A →+* L) fun (f : K →+* L) ↦ f.comp (algebraMap A K)

Tactic:
fun _ _ h => ringHom_ext (fun x => RingHom.congr_fun h x)

Premises used: RingHom.congr_fun, IsFractionRing.ringHom_ext, Function.Injective
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
K : Type u_5
inst_2 : Field K
L : Type u_7
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : Algebra R A
inst_7 : Algebra R K
inst_8 : IsScalarTower R A K
inst_9 : Algebra R L
g : A →ₐ[R] L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
⊢ Eq (α := K →+* L) (AlgHom.toRingHom (liftAlgHom hg)) (lift hg)

Tactic:
rfl

Premises used: IsLocalization.lift, IsFractionRing.lift, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
K : Type u_5
inst_2 : Field K
L : Type u_7
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : Algebra R A
inst_7 : Algebra R K
inst_8 : IsScalarTower R A K
inst_9 : Algebra R L
g : A →ₐ[R] L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
⊢ Eq (α := (a : K) → L) (⇑(liftAlgHom hg) : (a : K) → L) (⇑(lift hg) : (a : K) → L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
A : Type u_4
inst_1 : CommRing A
K : Type u_5
inst_2 : Field K
L : Type u_7
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : IsFractionRing A K
inst_6 : Algebra R A
inst_7 : Algebra R K
inst_8 : IsScalarTower R A K
inst_9 : Algebra R L
g : A →ₐ[R] L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
x : K
⊢ Eq.{u_7 + 1} (α := L) ((liftAlgHom hg : (a : K) → L) x : L) ((lift hg : (a : K) → L) x : L)

Tactic:
rfl

Premises used: 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
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
x : A
⊢ Eq.{u_7 + 1} (α := L) ((lift hg : (a : K) → L) ((algebraMap A K : (a : A) → K) x : K) : L) ((g : (a : A) → L) x : L)

Tactic:
lift_eq _ _

Premises used: IsLocalization.lift_eq
-- 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
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
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)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) = g

Tactic:
ext
-- 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
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
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:
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
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)
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)
⊢ @RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (lift hg) (algebraMap A K) = g

Tactic:
ext
-- 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
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)
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:
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
g : A →+* L
hg : Injective.{u_4 + 1, u_7 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
x : A
y : ↥A⁰
⊢ (lift hg : (a : K) → L) (mk' K x y) =
    HDiv.hDiv (α := L) (β := L) ((g : (a : A) → L) x : L) ((g : (a : A) → L) (↑y : A) : L)

Tactic:
simp only [mk'_eq_div, map_div₀, lift_algebraMap]

Premises used: IsFractionRing.mk'_eq_div, map_div₀, IsFractionRing.lift_algebraMap
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
h : A ≃+* B
a : A
⊢ Eq.{u_11 + 1} (α := L) ((ringEquivOfRingEquiv h : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) ((h : (a : A) → B) a : B) : L)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
h : A ≃+* B
⊢ Eq (α := L ≃+* K) (RingEquiv.symm (ringEquivOfRingEquiv h)) (ringEquivOfRingEquiv h.symm)

Tactic:
rfl

Premises used: IsFractionRing.ringEquivOfRingEquiv, IsLocalization.ringEquivOfRingEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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)
⊢ Eq (α := K ≃+* M) (ringEquivOfRingEquiv (f.trans g))
    (RingEquiv.trans.{u_9, u_11, u_13} (S := L) (ringEquivOfRingEquiv f) (ringEquivOfRingEquiv g))

Tactic:
ext a
-- Module: Mathlib.RingTheory.Localization.FractionRing
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
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:
simp [IsLocalization.map_map]

Premises used: IsLocalization.map_map
-- 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_1 : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K_1
L_1 : Type u_7
inst_8 : Field L_1
inst_9 : Algebra A_1 K_1
inst_10 : IsFractionRing A_1 K_1
g : A_1 →+* L_1
A : Type u_8
B : Type u_9
K : Type u_10
L : Type u_11
inst_11 : CommRing A
inst_12 : CommRing B
inst_13 : CommRing K
inst_14 : CommRing L
inst_15 : Algebra A K
inst_16 : IsFractionRing A K
inst_17 : Algebra B L
inst_18 : IsFractionRing B L
f : A ≃+* B
⊢ RingHomInvPair (↑f : A →+* B) (↑f.symm : B →+* A)

Tactic:
RingHomInvPair.of_ringEquiv f

Premises used: RingHomInvPair.of_ringEquiv
-- 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_1 : Type u_5
B_1 : Type u_6
inst_5 : CommRing B_1
inst_6 : IsDomain B_1
inst_7 : Field K_1
L_1 : Type u_7
inst_8 : Field L_1
inst_9 : Algebra A_1 K_1
inst_10 : IsFractionRing A_1 K_1
g : A_1 →+* L_1
A : Type u_8
B : Type u_9
K : Type u_10
L : Type u_11
inst_11 : CommRing A
inst_12 : CommRing B
inst_13 : CommRing K
inst_14 : CommRing L
inst_15 : Algebra A K
inst_16 : IsFractionRing A K
inst_17 : Algebra B L
inst_18 : IsFractionRing B L
f : A ≃+* B
r : A
x : K
⊢ Equiv.toFun (RingEquiv.toEquiv (ringEquivOfRingEquiv f)) (r • x) =
    HSMul.hSMul.{u_9, u_11, u_11} (α := B) (β := L) (((↑f : A →+* B) : (a : A) → B) r : B)
      (Equiv.toFun (RingEquiv.toEquiv (ringEquivOfRingEquiv f)) x)

Tactic:
simp [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_8
B : Type u_9
K : 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
f : A ≃+* B
x : K
⊢ Eq.{u_11 + 1} (α := L) ((semilinearEquivOfRingEquiv K L f : (a : K) → L) x : L)
    ((ringEquivOfRingEquiv f : (a : K) → L) x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_8
B : Type u_9
K : 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
f : A ≃+* B
a : A
⊢ Eq.{u_11 + 1} (α := L) ((semilinearEquivOfRingEquiv K L f : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) ((f : (a : A) → B) a : B) : L)

Tactic:
simp [semilinearEquivOfRingEquiv, ringEquivOfRingEquiv]

Premises used: IsFractionRing.ringEquivOfRingEquiv, IsFractionRing.semilinearEquivOfRingEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_8
B : Type u_9
K : 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
f : A ≃+* B
x : L
⊢ Eq.{u_10 + 1} (α := K) ((LinearEquiv.symm (semilinearEquivOfRingEquiv K L f) : (a : L) → K) x : K)
    ((RingEquiv.symm (ringEquivOfRingEquiv f) : (a : L) → K) x : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
A : Type u_8
B : Type u_9
K : 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
f : A ≃+* B
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
g : B ≃+* C
a : K
⊢ Eq.{u_13 + 1} (α := M) ((semilinearEquivOfRingEquiv K M (f.trans g) : (a : K) → M) a : M)
    ((LinearEquiv.trans (module_M₂ := Algebra.toModule) (semilinearEquivOfRingEquiv K L f)
            (semilinearEquivOfRingEquiv L M g) :
          (a : K) → M)
        a :
      M)

Tactic:
simp [-RingEquiv.coe_ringHom_trans, semilinearEquivOfRingEquiv_apply,
    semilinearEquivOfRingEquiv_apply K M, ringEquivOfRingEquiv_comp K L M]

Premises used: RingEquiv.coe_ringHom_trans, IsFractionRing.semilinearEquivOfRingEquiv_apply, IsFractionRing.ringEquivOfRingEquiv_comp
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
A : Type u_9
K : Type u_10
B : Type u_11
L : Type u_12
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing K
inst_4 : CommRing L
inst_5 : Algebra R A
inst_6 : Algebra R K
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsScalarTower R A K
inst_10 : Algebra R B
inst_11 : Algebra R L
inst_12 : Algebra B L
inst_13 : IsFractionRing B L
inst_14 : IsScalarTower R B L
h : A ≃ₐ[R] B
a : A
⊢ Eq.{u_12 + 1} (α := L) ((algEquivOfAlgEquiv h : (a : K) → L) ((algebraMap A K : (a : A) → K) a : K) : L)
    ((algebraMap B L : (a : B) → L) ((h : (a : A) → B) a : B) : L)

Tactic:
simp [algEquivOfAlgEquiv]

Premises used: IsFractionRing.algEquivOfAlgEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_8
A : Type u_9
K : Type u_10
B : Type u_11
L : Type u_12
inst : CommSemiring R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing K
inst_4 : CommRing L
inst_5 : Algebra R A
inst_6 : Algebra R K
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsScalarTower R A K
inst_10 : Algebra R B
inst_11 : Algebra R L
inst_12 : Algebra B L
inst_13 : IsFractionRing B L
inst_14 : IsScalarTower R B L
h : A ≃ₐ[R] B
⊢ Eq (α := L ≃ₐ[R] K) (AlgEquiv.symm (algEquivOfAlgEquiv h)) (algEquivOfAlgEquiv h.symm)

Tactic:
rfl

Premises used: IsFractionRing.algEquivOfAlgEquiv, AlgEquiv.symm, IsLocalization.algEquivOfAlgEquiv, Equiv.symm, rfl