awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
h : S ⊆ T
⊢ LE.le (α := IntermediateField F E) (adjoin F S) (adjoin F T)

Tactic:
GaloisConnection.monotone_l gc h

Premises used: IntermediateField.gc, GaloisConnection.monotone_l
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
E : Type u_2
inst : Field E
S : Set E
F : Subfield E
⊢ (↑F : Set E) ⊆ (↑(adjoin (↥F) S) : Set E)

Tactic:
fun x hx =>
  adjoin.algebraMap_mem F S ⟨x, hx⟩

Premises used: Set.Mem, Membership.mem, Subtype, Set.Subset, Subtype.mk, IntermediateField.adjoin.algebraMap_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
E : Type u_2
inst : Field E
S : Set E
F : Subfield E
T : Set E
HT : T ⊆ (↑F : Set E)
⊢ T ⊆ (↑(adjoin (↥F) S) : Set E)

Tactic:
fun x hx => (adjoin F S).algebraMap_mem ⟨x, HT hx⟩

Premises used: IntermediateField.algebraMap_mem, Set.Mem, Membership.mem, Subtype, Set.Subset, Subtype.mk, IntermediateField.adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
H : T ⊆ S
⊢ T ⊆ (↑(adjoin F S) : Set E)

Tactic:
fun _ hx =>
  subset_adjoin F S (H hx)

Premises used: Set.Subset, IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_4 + 1} (α := IntermediateField F E) (adjoin F ∅) ⊥

Tactic:
eq_bot_iff.mpr (adjoin_le_iff.mpr (Set.empty_subset _))

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, Set.empty_subset, eq_bot_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_3
E : Type u_4
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq.{u_4 + 1} (α := IntermediateField F E) (adjoin F Set.univ) ⊤

Tactic:
eq_top_iff.mpr <| subset_adjoin _ _

Premises used: Iff.mpr, eq_top_iff, IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
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 : Subfield E
HF : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑K : Set E)
HS : S ⊆ (↑K : Set E)
⊢ toSubfield (adjoin F S) ≤ K

Tactic:
simpa using ⟨HF, HS⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
F' : Type u_3
inst_3 : Field F'
inst_4 : Algebra F' E
S S' : Set E
⊢ (↑(adjoin F S) : Set E) ⊆ (↑(adjoin F' S') : Set E) ↔
    Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin F' S') : Set E) ∧
      S ⊆ (↑(adjoin F' S') : Set E)

Tactic:
⟨fun h => ⟨(adjoin.range_algebraMap_subset _ _).trans h,
    (subset_adjoin _ _).trans h⟩, fun ⟨hF, hS⟩ =>
      (Subfield.closure_le (t := (adjoin F' S').toSubfield)).mpr (Set.union_subset hF hS)⟩

Premises used: Iff.mpr, Subfield.closure_le, HasSubset.Subset.trans, HasSubset.Subset, IntermediateField.subset_adjoin, IntermediateField.adjoin.range_algebraMap_subset, Set.union_subset, _private.0.IntermediateField.adjoin_subset_adjoin_iff.match_1, SetLike.coe, And.intro, IntermediateField.adjoin, Iff.intro
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
rw : (↑(restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T)) : Set E) = (↑(adjoin F (S ∪ T)) : Set E)
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (adjoin F (S ∪ T))

Tactic:
rw [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a : (↑(adjoin (↥(adjoin F S)) T) : Set E) ⊆ (↑(adjoin F (S ∪ T)) : Set E)
a₁ : (↑(adjoin F (S ∪ T)) : Set E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
⊢ (↑(adjoin (↥(adjoin F S)) T) : Set E) = (↑(adjoin F (S ∪ T)) : Set E)

Tactic:
apply subset_antisymm

Premises used: subset_antisymm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a :
  Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
      (↑(adjoin F (S ∪ T)) : Set E) ∧
    T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
⊢ (↑(adjoin (↥(adjoin F S)) T) : Set E) ⊆ (↑(adjoin F (S ∪ T)) : Set E)

Tactic:
rw [adjoin_subset_adjoin_iff]

Premises used: IntermediateField.adjoin_subset_adjoin_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a :
  Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E) ∧
    S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
⊢ (↑(adjoin F (S ∪ T)) : Set E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
rw [adjoin_subset_adjoin_iff]

Premises used: IntermediateField.adjoin_subset_adjoin_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a :
  Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
    (↑(adjoin F (S ∪ T)) : Set E)
a₁ : T ⊆ (↑(adjoin F (S ∪ T)) : Set E)
⊢ Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E) ⊆
      (↑(adjoin F (S ∪ T)) : Set E) ∧
    T ⊆ (↑(adjoin F (S ∪ T)) : Set E)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
a : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
a₁ : S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E) ∧
    S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
constructor
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
⊢ Membership.mem (α := E) (↑(adjoin F (S ∪ T)) : Set E)
    ((algebraMap (↥(adjoin F S)) E : (a : ↥(adjoin F S)) → E)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) :
      E)

Tactic:
adjoin.mono _ _ _ Set.subset_union_left hx

Premises used: IntermediateField.adjoin.mono, Set.subset_union_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
x : E
hx : Membership.mem (γ := IntermediateField F E) (adjoin F S) x
⊢ Membership.mem (α := E) (↑(adjoin F (S ∪ T)) : Set E)
    ((algebraMap (↥(adjoin F S)) E : (a : ↥(adjoin F S)) → E)
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := IntermediateField F E) (adjoin F S) x) x hx) :
      E)

Tactic:
exact adjoin.mono _ _ _ Set.subset_union_left hx

Premises used: IntermediateField.adjoin.mono, Set.subset_union_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ T ⊆ (↑(adjoin F (S ∪ T)) : Set E)

Tactic:
subset_adjoin_of_subset_right _ _ Set.subset_union_right

Premises used: Set.subset_union_right, IntermediateField.subset_adjoin_of_subset_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ T ⊆ (↑(adjoin F (S ∪ T)) : Set E)

Tactic:
exact subset_adjoin_of_subset_right _ _ Set.subset_union_right

Premises used: Set.subset_union_right, IntermediateField.subset_adjoin_of_subset_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
Set.range_subset_iff.mpr fun f ↦ Subfield.subset_closure (.inl ⟨f, rfl⟩)

Premises used: Iff.mpr, Algebra.algebraMap, Subtype.mk, IntermediateField.adjoin.algebraMap_mem, Exists.intro, Or.inl, Subfield.subset_closure, Set.range_subset_iff, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
exact Set.range_subset_iff.mpr fun f ↦ Subfield.subset_closure (.inl ⟨f, rfl⟩)

Premises used: Iff.mpr, Subfield.subset_closure, Set.range_subset_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
Set.union_subset
      (fun x hx ↦ Subfield.subset_closure <| .inl ⟨⟨x, Subfield.subset_closure (.inr hx)⟩, rfl⟩)
      (fun x hx ↦ Subfield.subset_closure <| .inr hx)

Premises used: Subtype.mk, Set.union_subset, Exists.intro, Or.inl, Subfield.subset_closure, Or.inr, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ S ∪ T ⊆ (↑(adjoin (↥(adjoin F S)) T) : Set E)

Tactic:
exact Set.union_subset
      (fun x hx ↦ Subfield.subset_closure <| .inl ⟨⟨x, Subfield.subset_closure (.inr hx)⟩, rfl⟩)
      (fun x hx ↦ Subfield.subset_closure <| .inr hx)

Premises used: Set.union_subset, Subfield.subset_closure
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
x : E
grw grw₁ : LE.le (α := IntermediateField F E) (adjoin F (insert x S)) (adjoin F (insert x S))
⊢ LE.le (α := IntermediateField F E) (adjoin F (insert x S)) (adjoin F (insert x (↑(adjoin F S) : Set E)))

Tactic:
grw [← subset_adjoin]

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
rw :
  Eq (α := IntermediateField F E) (adjoin F (S ∪ T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))
rw₁ : Eq (α := IntermediateField F E) (adjoin F (S ∪ T)) (adjoin F (T ∪ S))
rw₂ rw₃ : Eq (α := IntermediateField F E) (adjoin F (T ∪ S)) (adjoin F (T ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥(adjoin F S)) (adjoin (↥(adjoin F S)) T))
    (restrictScalars F (L' := ↥(adjoin F T)) (adjoin (↥(adjoin F T)) S))

Tactic:
rw [adjoin_adjoin_left, adjoin_adjoin_left, Set.union_comm]

Premises used: Set.union_comm, IntermediateField.adjoin_adjoin_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
E' : Type u_3
inst_3 : Field E'
inst_4 : Algebra F E'
f : E →ₐ[F] E'
⊢ map f (adjoin F S) = adjoin F ((⇑f : (a : E) → E') '' S)

Tactic:
le_antisymm
    (map_le_iff_le_comap.mpr <| adjoin_le_iff.mpr fun x hx ↦ subset_adjoin _ _ ⟨x, hx, rfl⟩)
    (adjoin_le_iff.mpr <| Set.monotone_image <| subset_adjoin _ _)

Premises used: Iff.mpr, IntermediateField.map_le_iff_le_comap, IntermediateField.adjoin_le_iff, IntermediateField.subset_adjoin, le_antisymm, And.intro, Exists.intro, Set.image, Set.monotone_image, DFunLike.coe, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set ↥K
⊢ lift (adjoin F S) = adjoin F (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' S)

Tactic:
adjoin_map _ _ _

Premises used: IntermediateField.lift, IntermediateField.adjoin_map
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
α : ↥K
⊢ Eq (α := IntermediateField F E) (lift (F := K) (adjoin F {α})) (adjoin F {(↑α : E)})

Tactic:
simp only [lift_adjoin, Set.image_singleton]

Premises used: Set.image_singleton, IntermediateField.lift_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (lift (F := K) ⊥) ⊥

Tactic:
map_bot _

Premises used: IntermediateField.lift, IntermediateField.map_bot
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
rw : map K.val ⊤ = K
rw₁ : K.val.fieldRange = K
rw₂ rw₃ : K = K
⊢ lift (F := K) ⊤ = K

Tactic:
rw [lift, ← AlgHom.fieldRange_eq_map, fieldRange_val]

Premises used: IntermediateField.lift, AlgHom.fieldRange_eq_map, IntermediateField.fieldRange_val
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
L L' : IntermediateField F ↥K
⊢ lift (L ⊔ L') = lift L ⊔ lift L'

Tactic:
simp [lift, map_sup]

Premises used: IntermediateField.lift, IntermediateField.map_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
L L' : IntermediateField F ↥K
⊢ lift (L ⊓ L') = lift L ⊓ lift L'

Tactic:
simp [lift, map_inf]

Premises used: IntermediateField.lift, IntermediateField.map_inf
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
⊢ adjoin F (↑K : Set E) = K

Tactic:
le_antisymm (adjoin_le_iff.2 fun _ ↦ id) (subset_adjoin F _)

Premises used: Iff.mpr, IntermediateField.adjoin_le_iff, id, IntermediateField.subset_adjoin, le_antisymm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw :
  Eq (α := IntermediateField F E)
    (restrictScalars F (L' := ↥(adjoin F (↑K : Set E))) (adjoin (↥(adjoin F (↑K : Set E))) S))
    (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
rw₁ : Eq (α := IntermediateField F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑(adjoin F (↑K : Set E)) : Set E) ∪ S))
rw₂ rw₃ : Eq (α := IntermediateField F E) (adjoin F ((↑K : Set E) ∪ S)) (adjoin F ((↑K : Set E) ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (L' := ↥K) (adjoin (↥K) S)) (adjoin F ((↑K : Set E) ∪ S))

Tactic:
rw [← adjoin_self _ K, adjoin_adjoin_left, adjoin_self _ K]

Premises used: IntermediateField.adjoin_adjoin_left, IntermediateField.adjoin_self
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
rw : Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((↑K : Set E) ∪ S))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (extendScalars h)) (restrictScalars F (L' := ↥K) (adjoin (↥K) S))

Tactic:
rw [extendScalars_restrictScalars, restrictScalars_adjoin]

Premises used: IntermediateField.extendScalars_restrictScalars, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((↑K : Set E) ∪ S))

Tactic:
le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

Premises used: Iff.mpr, IntermediateField.adjoin.mono, IntermediateField.adjoin_le_iff, Set.subset_union_right, IntermediateField.subset_adjoin, Set.union_subset, le_antisymm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
h : K ≤ adjoin F S
⊢ Eq (α := IntermediateField F E) (adjoin F S) (adjoin F ((↑K : Set E) ∪ S))

Tactic:
exact le_antisymm (adjoin.mono F S _ Set.subset_union_right) <| adjoin_le_iff.2 <|
    Set.union_subset h (subset_adjoin F S)

Premises used: Iff.mpr, IntermediateField.adjoin.mono, IntermediateField.adjoin_le_iff, Set.subset_union_right, IntermediateField.subset_adjoin, Set.union_subset, le_antisymm
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S T : Set E
⊢ Eq (α := IntermediateField F E) (adjoin F (S ∪ T)) (adjoin F S ⊔ adjoin F T)

Tactic:
gc.l_sup

Premises used: IntermediateField.gc, GaloisConnection.l_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
K : IntermediateField F E
S : Set E
rw : adjoin F ((↑K : Set E) ∪ S) = K ⊔ adjoin F S
rw₁ : adjoin F (↑K : Set E) ⊔ adjoin F S = K ⊔ adjoin F S
rw₂ rw₃ : K ⊔ adjoin F S = K ⊔ adjoin F S
⊢ restrictScalars F (L' := ↥K) (adjoin (↥K) S) = K ⊔ adjoin F S

Tactic:
rw [restrictScalars_adjoin, adjoin_union, adjoin_self]

Premises used: IntermediateField.adjoin_union, IntermediateField.adjoin_self, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
f : ι → Set E
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (adjoin F (⋃ (i : ι), f i)) (⨆ (i : ι), adjoin F (f i))

Tactic:
gc.l_iSup

Premises used: GaloisConnection.l_iSup, IntermediateField.gc, Set.iUnion
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Sort u_3
f : ι → IntermediateField F E
simp_rw : Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (i : ι), f i) (⨆ (i : ι), adjoin F (↑(f i) : Set E))
⊢ Eq.{u_2 + 1} (α := IntermediateField F E) (⨆ (i : ι), f i) (adjoin F (⋃ (i : ι), (↑(f i) : Set E)))

Tactic:
simp_rw [adjoin_iUnion, adjoin_self]

Premises used: IntermediateField.adjoin_iUnion, IntermediateField.adjoin_self
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
h₁ : ∀ (x : E), x ∈ K ↔ x ∈ K'
⊢ K = K'

Tactic:
ext x
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
x : E
h₁ : x ∈ K.toSubfield ↔ x ∈ K'.toSubfield
⊢ x ∈ K ↔ x ∈ K'

Tactic:
change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield

Premises used: IntermediateField.toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
K K' : IntermediateField F E
h : K.toSubfield = K'.toSubfield
x : E
h₁ h₂ : x ∈ K'.toSubfield ↔ x ∈ K'.toSubfield
⊢ x ∈ K.toSubfield ↔ x ∈ K'.toSubfield

Tactic:
rw [h]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
apply_fun :
  Eq (α := Subfield E) (toSubfield (restrictScalars F (adjoin L S))) (toSubfield (restrictScalars F (adjoin L' S)))
⊢ Eq (α := IntermediateField F E) (restrictScalars F (adjoin L S)) (restrictScalars F (adjoin L' S))

Tactic:
apply_fun toSubfield using (fun K K' h ↦ by
    ext x; change x ∈ K.toSubfield ↔ x ∈ K'.toSubfield; rw [h])

Premises used: IntermediateField.toSubfield
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
L : Type u_3
L' : Type u_4
inst_3 : Field L
inst_4 : Field L'
inst_5 : Algebra F L
inst_6 : Algebra L E
inst_7 : Algebra F L'
inst_8 : Algebra L' E
inst_9 : IsScalarTower F L E
inst_10 : IsScalarTower F L' E
i : L ≃ₐ[F] L'
hi :
  Eq (α := (a : L) → E) (⇑(algebraMap L E) : (a : L) → E)
    (Function.comp.{u_3 + 1, u_4 + 1, u_2 + 1} (β := L') (⇑(algebraMap L' E) : (a : L') → E) (⇑i : (a : L) → L'))
S : Set E
⊢ Eq (α := Subfield E) (toSubfield (restrictScalars F (adjoin L S))) (toSubfield (restrictScalars F (adjoin L' S)))

Tactic:
simp [hi]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
s : Set E
p : (x : E) → Membership.mem (γ := IntermediateField F E) (adjoin F s) x → Prop
mem : ∀ (x : E) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (x : F), p ((Algebra.algebraMap F E : (a : F) → E) x) ⋯
add :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x + y) ⋯
inv : ∀ (x : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x), p x hx → p x⁻¹ ⋯
mul :
  ∀ (x y : E) (hx : Membership.mem (γ := IntermediateField F E) (adjoin F s) x)
    (hy : Membership.mem (γ := IntermediateField F E) (adjoin F s) y), p x hx → p y hy → p (x * y) ⋯
x : E
h : Membership.mem (γ := IntermediateField F E) (adjoin F s) x
simp_rw : p ((Algebra.algebraMap F E : (a : F) → E) 1) ⋯
⊢ p 1 ⋯

Tactic:
simp_rw [← (Algebra.algebraMap F E).map_one]

Premises used: Algebra.algebraMap, RingHom.map_one