awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
a :
  Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L)))
⊢ f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F (↑g.range : Set L))

Tactic:
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]

Premises used: AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L)) (Subfield.closure (↑(RingHom.range (↑g : A →+* L)) : Set L))

Tactic:
ringHom_fieldRange_eq_of_comp_eq h

Premises used: IsFractionRing.ringHom_fieldRange_eq_of_comp_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
h₁ :
  Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L) =
    (↑(RingHom.range (↑g : A →+* L)) : Set L)
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L)))

Tactic:
convert! ringHom_fieldRange_eq_of_comp_eq h using 2

Premises used: IsFractionRing.ringHom_fieldRange_eq_of_comp_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
x_1 : L
h_1 : Membership.mem (γ := Set L) (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L)) x_1
x : F
hx : (algebraMap F L : (a : F) → L) x = x_1
⊢ (g.toRingHom : (a : A) → L) ((algebraMap F A : (a : F) → A) x : A) = x_1

Tactic:
simp [← hx]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
⊢ Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ (↑g.range : Set L) =
    (↑(RingHom.range (↑g : A →+* L)) : Set L)

Tactic:
exact Set.union_eq_self_of_subset_left fun _ ⟨x, hx⟩ ↦ ⟨algebraMap F A x, by simp [← hx]⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
a : f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F s)
⊢ f.fieldRange = IntermediateField.adjoin F s

Tactic:
apply IntermediateField.toSubfield_injective

Premises used: IntermediateField.toSubfield_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
a :
  Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
⊢ f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F s)

Tactic:
simp_rw [AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield]

Premises used: AlgHom.fieldRange_toSubfield, IntermediateField.adjoin_toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))

Tactic:
ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_

Premises used: IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
a :
  Eq (α := Subring L) (RingHom.range (↑g : A →+* L))
    (Subring.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))
⊢ Eq (α := Subfield L) (RingHom.fieldRange (↑f : K →+* L))
    (Subfield.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))

Tactic:
refine ringHom_fieldRange_eq_of_comp_eq_of_range_eq h ?_

Premises used: IsFractionRing.ringHom_fieldRange_eq_of_comp_eq_of_range_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
a : RingHom.range (↑g : A →+* L) = g.range.toSubring
⊢ Eq (α := Subring L) (RingHom.range (↑g : A →+* L))
    (Subring.closure (Set.range.{u_4, u_1 + 1} (ι := F) (⇑(algebraMap F L) : (a : F) → L) ∪ s))

Tactic:
rw [← Algebra.adjoin_eq_ring_closure, ← hs]

Premises used: Algebra.adjoin_eq_ring_closure
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
f : K →ₐ[F] L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f : K →+* L) (algebraMap A K)) (↑g : A →+* L)
s : Set L
hs : g.range = Algebra.adjoin F s
⊢ RingHom.range (↑g : A →+* L) = g.range.toSubring

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
a :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
          x :
        L)
      (((↑g : A →+* L) : (a : A) → L) x : L)
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K))
    (↑g : A →+* L)

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
x : A
⊢ Eq.{u_4 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
        x :
      L)
    (((↑g : A →+* L) : (a : A) → L) x : L)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
s : Set L
hs : g.range = Algebra.adjoin F s
a :
  ∀ (x : A),
    Eq.{u_4 + 1} (α := L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
          x :
        L)
      (((↑g : A →+* L) : (a : A) → L) x : L)
⊢ Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K))
    (↑g : A →+* L)

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
A : Type u_2
K : Type u_3
L : Type u_4
inst : Field F
inst_1 : CommRing A
inst_2 : Algebra F A
inst_3 : Field K
inst_4 : Algebra F K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Field L
inst_8 : Algebra F L
g : A →ₐ[F] L
inst_9 : IsScalarTower F A K
hg : Function.Injective.{u_2 + 1, u_4 + 1} (α := A) (β := L) (⇑g : (a : A) → L)
s : Set L
hs : g.range = Algebra.adjoin F s
x : A
⊢ Eq.{u_4 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(liftAlgHom hg) : K →+* L) (algebraMap A K) : (a : A) → L)
        x :
      L)
    (((↑g : A →+* L) : (a : A) → L) x : L)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E₁ E₂ : IntermediateField L E
⊢ LE.le (α := IntermediateField K E) (restrictScalars K E₁) (restrictScalars K E₂) ↔ E₁ ≤ E₂

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
H : FG (restrictScalars K E')
obtain : ∀ (s : Finset E) (hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')), E'.FG
⊢ E'.FG

Tactic:
obtain ⟨s, hs⟩ := H
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ E'.FG

Tactic:
⟨s, le_antisymm ?_ ?_⟩

Premises used: IntermediateField.FG, le_antisymm, Exists.intro
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
refine_1 : adjoin L (↑s : Set E) ≤ E'
refine_2 : E' ≤ adjoin L (↑s : Set E)
⊢ E'.FG

Tactic:
refine ⟨s, le_antisymm ?_ ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
refine_1 : (↑s : Set E) ⊆ (↑E' : Set E)
⊢ adjoin L (↑s : Set E) ≤ E'

Tactic:
rw [adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ (↑s : Set E) ⊆ (↑E' : Set E)

Tactic:
(subset_adjoin K _).trans_eq congr(($hs : Set E))

Premises used: LE.le.trans_eq, congrArg, id, IntermediateField.subset_adjoin, SetLike.coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ (↑s : Set E) ⊆ (↑E' : Set E)

Tactic:
exact (subset_adjoin K _).trans_eq congr(($hs : Set E))

Premises used: LE.le.trans_eq, congrArg, id, IntermediateField.subset_adjoin, SetLike.coe
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
refine_2 : (↑s : Set E) ⊆ (↑(restrictScalars K (adjoin L (↑s : Set E))) : Set E)
⊢ E' ≤ adjoin L (↑s : Set E)

Tactic:
rw [← restrictScalars_le_iff K, ← hs, adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff, IntermediateField.restrictScalars_le_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ (↑s : Set E) ⊆ (↑(restrictScalars K (adjoin L (↑s : Set E))) : Set E)

Tactic:
subset_adjoin L _

Premises used: iInf, Set.iInter, IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_1
L : Type u_2
E : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Algebra L E
inst_6 : IsScalarTower K L E
E' : IntermediateField L E
s : Finset E
hs : Eq (α := IntermediateField K E) (adjoin K (↑s : Set E)) (restrictScalars K E')
⊢ (↑s : Set E) ⊆ (↑(restrictScalars K (adjoin L (↑s : Set E))) : Set E)

Tactic:
exact subset_adjoin L _

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
i : ι → E
x : E
simp_rw :
  (∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) s ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
simp_rw₁ :
  (∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) s ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
simp_rw₂ :
  (∃ (r : E),
      (∃ (x : MvPolynomial ι F), (MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) x = r) ∧
        ∃ (s : E), (∃ (x : MvPolynomial ι F), (MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) x = s) ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (Set.range i)) x ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)

Tactic:
simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

Premises used: AlgHom.mem_range, IntermediateField.mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval, exists_exists_eq_and
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α x : E
⊢ Membership.mem (γ := IntermediateField F E) F⟮α⟯ x ↔
    ∃ (r : F[X]) (s : F[X]),
      x = HDiv.hDiv (α := E) (β := E) ((aeval α : (a : F[X]) → E) r : E) ((aeval α : (a : F[X]) → E) s : E)

Tactic:
simp only [mem_adjoin_iff_div, Algebra.adjoin_singleton_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]

Premises used: Algebra.adjoin_singleton_eq_range_aeval, AlgHom.mem_range, IntermediateField.mem_adjoin_iff_div, exists_exists_eq_and
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
M : Type u_3
inst_3 : Monoid M
inst_4 : MulSemiringAction M E
inst_5 : SMulCommClass M F E
m : M
⊢ (∀ (x : E), Membership.mem (γ := IntermediateField F E) (adjoin F S) x → m • x = x) ↔ ∀ x ∈ S, m • x = x

Tactic:
simpa [-adjoin_le_iff, Set.subset_def, SetLike.le_def, FixedBy.intermediateField_mem_iff] using
    adjoin_le_iff (T := FixedBy.intermediateField F E m)

Premises used: Set.subset_def, IntermediateField.adjoin_le_iff, SetLike.le_def, FixedBy.intermediateField_mem_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
⊢ FiniteDimensional.{u_3, u_4} K
    ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) g.range : Submodule K L)

Tactic:
have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
h :
  FiniteDimensional.{u_3, u_4} K
    ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) g.range : Submodule K L)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      FiniteDimensional.{u_3, u_4} K
        ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (E1 ⊔ E2).toSubalgebra : Submodule K L)),
    FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)
⊢ FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)

Tactic:
rwa [this] at h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
suffices : g.range = (E1 ⊔ E2).toSubalgebra
⊢ FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)

Tactic:
suffices g.range = (E1 ⊔ E2).toSubalgebra by
    have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
    rwa [this] at h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
rw : E1.val.range ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
rw₁ : E1.toSubalgebra ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
rw₂ : E1.toSubalgebra ⊔ E2.toSubalgebra = (E1 ⊔ E2).toSubalgebra
rw₃ rw₄ : E1.toSubalgebra ⊔ E2.toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
⊢ g.range = (E1 ⊔ E2).toSubalgebra

Tactic:
rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]

Premises used: IntermediateField.range_val, Algebra.TensorProduct.productMap_range, IntermediateField.sup_toSubalgebra_of_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1 ∨ Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
⊢ Module.rank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra

Tactic:
have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra