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
⊢ Eq.{u_2 + 1} (α := Subfield E) (toSubfield.{u_1, u_2} (K := F) ⊤) ⊤

Tactic:
rfl

Premises used: 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 : IntermediateField F E
⊢ (↑(S ⊓ T) : Set E) = (↑S : Set E) ∩ (↑T : Set E)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, 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 : IntermediateField F E
x : E
⊢ x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- 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 : IntermediateField F E
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
rfl

Premises used: Subalgebra.copy, 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 : IntermediateField F E
⊢ (S ⊓ T).toSubfield = S.toSubfield ⊓ T.toSubfield

Tactic:
rfl

Premises used: 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 : IntermediateField F E
rw : (S ⊔ T).toSubfield = Subfield.closure ((↑S.toSubfield : Set E) ∪ (↑T.toSubfield : Set E))
⊢ (S ⊔ T).toSubfield = S.toSubfield ⊔ T.toSubfield

Tactic:
rw [← S.toSubfield.closure_eq, ← T.toSubfield.closure_eq, ← Subfield.closure_union]

Premises used: Subfield.closure_eq, Subfield.closure_union, 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
S T : IntermediateField F E
simp_rw :
  Eq (α := Subfield E)
    (Subfield.closure
      (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E))))
    (Subfield.closure ((↑S : Set E) ∪ (↑T : Set E)))
⊢ (S ⊔ T).toSubfield = Subfield.closure ((↑S.toSubfield : Set E) ∪ (↑T.toSubfield : Set E))

Tactic:
simp_rw [sup_def, adjoin_toSubfield, coe_toSubfield]

Premises used: IntermediateField.coe_toSubfield, IntermediateField.sup_def, IntermediateField.adjoin_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
S T : IntermediateField F E
e_s :
  Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E)) =
    (↑S : Set E) ∪ (↑T : Set E)
⊢ Eq (α := Subfield E)
    (Subfield.closure
      (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E))))
    (Subfield.closure ((↑S : Set E) ∪ (↑T : Set E)))

Tactic:
congr 1
-- 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 : IntermediateField F E
e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑S : Set E) ∪ (↑T : Set E)
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ((↑S : Set E) ∪ (↑T : Set E)) =
    (↑S : Set E) ∪ (↑T : Set E)

Tactic:
rw [Set.union_eq_right]

Premises used: Set.union_eq_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 : IntermediateField F E
x : F
⊢ Membership.mem (α := E) ((↑S : Set E) ∪ (↑T : Set E)) ((algebraMap F E : (a : F) → E) x : E)

Tactic:
Set.mem_union_left _ (algebraMap_mem S x)

Premises used: IntermediateField.algebraMap_mem, Set.mem_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 : IntermediateField F E
x : F
⊢ Membership.mem (α := E) ((↑S : Set E) ∪ (↑T : Set E)) ((algebraMap F E : (a : F) → E) x : E)

Tactic:
exact Set.mem_union_left _ (algebraMap_mem S x)

Premises used: IntermediateField.algebraMap_mem, Set.mem_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 : Set (IntermediateField F E)
⊢ Eq (α := Set E) (sInf ((fun (x : IntermediateField F E) ↦ (↑x : Set E)) '' S)) (⋂ s ∈ S, (↑s : Set E))

Tactic:
simp
-- 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 (IntermediateField F E)
x : E
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simpa only [Set.mem_iInter] using Set.ext_iff.1 (coe_sInf S) x

Premises used: Set.mem_iInter, Iff.mp, Set.ext_iff, IntermediateField.coe_sInf
-- 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 (IntermediateField F E)
⊢ (↑(sInf S).toSubalgebra : Set E) = (↑(sInf (toSubalgebra '' S)) : Set E)

Tactic:
simp
-- 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 (IntermediateField F E)
⊢ (↑(sInf S).toSubfield : Set E) = (↑(sInf (toSubfield '' S)) : Set E)

Tactic:
simp
-- 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 (IntermediateField F E)
hS : S.Nonempty
rw : toSubfield '' S = (fun (x : IntermediateField F E) ↦ Subfield.closure (↑x : Set E)) '' S
⊢ toSubfield '' S = Subfield.closure '' SetLike.coe '' S

Tactic:
rw [Set.image_image]

Premises used: Set.image_image
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : ∀ x ∈ S, x.toSubfield = Subfield.closure (↑x : Set E)
⊢ toSubfield '' S = (fun (x : IntermediateField F E) ↦ Subfield.closure (↑x : Set E)) '' S

Tactic:
congr! with 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
S : Set (IntermediateField F E)
hS : S.Nonempty
x : IntermediateField F E
h : x ∈ S
⊢ x.toSubfield = Subfield.closure (↑x : Set E)

Tactic:
x.toSubfield.closure_eq.symm

Premises used: Subfield.closure_eq, IntermediateField.toSubfield, Eq.symm
-- 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 (IntermediateField F E)
hS : S.Nonempty
x : IntermediateField F E
h : x ∈ S
⊢ x.toSubfield = Subfield.closure (↑x : Set E)

Tactic:
exact x.toSubfield.closure_eq.symm

Premises used: Subfield.closure_eq, IntermediateField.toSubfield, Eq.symm
-- 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 (IntermediateField F E)
hS : S.Nonempty
⊢ toSubfield '' S = Subfield.closure '' SetLike.coe '' S

Tactic:
have h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S := by
    rw [Set.image_image]
    congr! with x
    exact x.toSubfield.closure_eq.symm
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
rw :
  Eq (α := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S)))
    (Subfield.closure (⋃₀ (SetLike.coe '' S)))
⊢ (sSup S).toSubfield = sSup (toSubfield '' S)

Tactic:
rw [h, sSup_image, ← Subfield.closure_sUnion, sSup_def, adjoin_toSubfield]

Premises used: IntermediateField.sSup_def, Subfield.closure_sUnion, sSup_image, IntermediateField.adjoin_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
S : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
e_s :
  Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)
⊢ Eq (α := Subfield E)
    (Subfield.closure (Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S)))
    (Subfield.closure (⋃₀ (SetLike.coe '' S)))

Tactic:
congr 1
-- 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 (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
e_s : Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ ⋃₀ (SetLike.coe '' S)
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
rw [Set.union_eq_right]

Premises used: Set.union_eq_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 : Set (IntermediateField F E)
hS : S.Nonempty
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
e_s :
  ∀ (y : IntermediateField F E) (hy : y ∈ S),
    Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)
⊢ Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)

Tactic:
obtain ⟨y, hy⟩ := 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
S : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
y : IntermediateField F E
hy : y ∈ S
e_s : ∃ a ∈ S, Membership.mem (α := E) a ((algebraMap F E : (a : F) → E) x : E)
⊢ Membership.mem (α := E) (⋃₀ (SetLike.coe '' S)) ((algebraMap F E : (a : F) → E) x : E)

Tactic:
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]

Premises used: Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe, Set.mem_sUnion
-- 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 (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ ∃ a ∈ S, Membership.mem (α := E) a ((algebraMap F E : (a : F) → E) x : E)

Tactic:
⟨y, hy, algebraMap_mem y x⟩

Premises used: IntermediateField.algebraMap_mem, And.intro, Exists.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 : Set (IntermediateField F E)
h : toSubfield '' S = Subfield.closure '' SetLike.coe '' S
x : F
y : IntermediateField F E
hy : y ∈ S
⊢ ∃ a ∈ S, Membership.mem (α := E) a ((algebraMap F E : (a : F) → E) x : E)

Tactic:
exact ⟨y, hy, algebraMap_mem y 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
ι : Sort u_3
S : ι → IntermediateField F E
⊢ (↑(iInf S) : Set E) = ⋂ (i : ι), (↑(S i) : Set E)

Tactic:
simp [iInf]

Premises used: iInf
-- 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
S : ι → IntermediateField F E
⊢ (↑(iInf S).toSubalgebra : Set E) = (↑(⨅ (i : ι), (S i).toSubalgebra) : Set E)

Tactic:
simp [iInf]

Premises used: iInf
-- 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
S : ι → IntermediateField F E
⊢ (↑(iInf S).toSubfield : Set E) = (↑(⨅ (i : ι), (S i).toSubfield) : Set E)

Tactic:
simp [iInf]

Premises used: iInf
-- 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
inst_3 : Nonempty ι
S : ι → IntermediateField F E
⊢ (iSup S).toSubfield = ⨆ (i : ι), (S i).toSubfield

Tactic:
simp only [iSup, Set.range_nonempty, sSup_toSubfield, ← Set.range_comp, Function.comp_def]

Premises used: IntermediateField.sSup_toSubfield, Set.range_comp, iSup, Function.comp_def, Set.range_nonempty
-- 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
x : F
⊢ (botEquiv F E : (a : ↥⊥) → F) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) x : ↥⊥) = x

Tactic:
simp
-- 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
x : F
⊢ Eq.{u_2 + 1} (α := ↥⊥) (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) x : ↥⊥)
    ((algebraMap F ↥⊥ : (a : F) → ↥⊥) x : ↥⊥)

Tactic:
rfl

Premises used: 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
⊢ Eq (α := (a : ↥⊥) → F) (⇑(algebraMap (↥⊥) F) : (a : ↥⊥) → F) (⇑(botEquiv F E) : (a : ↥⊥) → F)

Tactic:
rfl

Premises used: 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
x : ↥⊥
obtain :
  ∀ (y : F),
    Eq (α := E)
      ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
          (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
        E)
      ((algebraMap F E : (a : F) → E)
          ((algebraMap (↥⊥) F : (a : ↥⊥) → F)
              (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
            F) :
        E)
⊢ Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) x : E)
    ((algebraMap F E : (a : F) → E) ((algebraMap (↥⊥) F : (a : ↥⊥) → F) x : F) : E)

Tactic:
obtain ⟨y, rfl⟩ := (botEquiv F E).symm.surjective x

Premises used: AlgEquiv.symm, IntermediateField.botEquiv, AlgEquiv.surjective, 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
y : F
rw :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((botEquiv F E : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)
rw₁ :
  Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E) y : E)
rw₂ :
  Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
    ((algebraMap F E : (a : F) → E) y : E)
rw₃ rw₄ :
  Eq (α := E) ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E) ((algebraMap F ↥⊥ : (a : F) → ↥⊥) y : ↥⊥) : E)
⊢ Eq (α := E)
    ((algebraMap (↥⊥) E : (a : ↥⊥) → E)
        (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
      E)
    ((algebraMap F E : (a : F) → E)
        ((algebraMap (↥⊥) F : (a : ↥⊥) → F)
            (((AlgEquiv.symm (botEquiv F E) : AlgEquiv.{u_1, u_1, u_2} F F ↥⊥) : (a : F) → ↥⊥) y : ↥⊥) :
          F) :
      E)

Tactic:
rw [coe_algebraMap_over_bot, (botEquiv F E).apply_symm_apply, botEquiv_symm,
        IsScalarTower.algebraMap_apply F (⊥ : IntermediateField F E) E]

Premises used: IntermediateField.coe_algebraMap_over_bot, IntermediateField.botEquiv_symm, Membership.mem, Subtype, AlgEquiv.apply_symm_apply, Bot.bot, IntermediateField.botEquiv, IsScalarTower.algebraMap_apply
-- 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
⊢ restrictScalars F (L' := ↥K) ⊥ = K

Tactic:
SetLike.coe_injective Subtype.range_coe

Premises used: SetLike.coe_injective, Subtype.range_coe
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra K E
inst_5 : Algebra K F
inst_6 : IsScalarTower K F E
⊢ Eq.{u_2 + 1} (α := IntermediateField K E) (restrictScalars.{u_3, u_2, u_1} K (L' := F) ⊤) ⊤

Tactic:
rfl

Premises used: IntermediateField.copy, IntermediateField.restrictScalars, Subalgebra.copy, 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra K E
inst_5 : Algebra K F
inst_6 : IsScalarTower K F E
L : IntermediateField F E
⊢ Eq (α := IntermediateField K E) (restrictScalars K L) ⊤ ↔ L = ⊤

Tactic:
simp [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
K : Type u_3
inst_3 : Field K
inst_4 : Algebra K E
inst_5 : Algebra K F
inst_6 : IsScalarTower K F E
L L' : IntermediateField F E
⊢ toSubfield (restrictScalars K L ⊔ restrictScalars K L') = toSubfield (restrictScalars K (L ⊔ L'))

Tactic:
simp
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra K E
inst_5 : Algebra K F
inst_6 : IsScalarTower K F E
L L' : IntermediateField F E
⊢ Eq (α := IntermediateField K E) (restrictScalars K L ⊓ restrictScalars K L') (restrictScalars K (L ⊓ L'))

Tactic:
rfl

Premises used: IntermediateField.copy, IntermediateField.restrictScalars, Subalgebra.copy, 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
f : E →ₐ[F] K
⊢ map f ⊥ = ⊥

Tactic:
toSubalgebra_injective <| Algebra.map_bot _

Premises used: Algebra.map_bot, IntermediateField.toSubalgebra_injective
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
s t : IntermediateField F E
f : E →ₐ[F] K
⊢ map f (s ⊔ t) = map f s ⊔ map f t

Tactic:
(gc_map_comap f).l_sup

Premises used: IntermediateField.gc_map_comap, 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
ι : Sort u_4
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ map f (iSup s) = ⨆ (i : ι), map f (s i)

Tactic:
(gc_map_comap f).l_iSup

Premises used: GaloisConnection.l_iSup, IntermediateField.gc_map_comap
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
s t : IntermediateField F E
f : E →ₐ[F] K
⊢ map f (s ⊓ t) = map f s ⊓ map f t

Tactic:
SetLike.coe_injective (Set.image_inter f.injective)

Premises used: Set.image_inter, SetLike.coe_injective, RingHom.injective, AlgHom.toRingHom
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
ι : Sort u_4
inst_5 : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
a : (↑(map f (iInf s)) : Set K) = (↑(⨅ (i : ι), map f (s i)) : Set K)
⊢ map f (iInf s) = ⨅ (i : ι), map f (s i)

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_injective
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
ι : Sort u_4
inst_5 : Nonempty ι
f : E →ₐ[F] K
s : ι → IntermediateField F E
⊢ (↑(map f (iInf s)) : Set K) = (↑(⨅ (i : ι), map f (s i)) : Set K)

Tactic:
simpa using (Set.injOn_of_injective f.injective).image_iInter_eq (s := SetLike.coe ∘ s)

Premises used: Set.InjOn.image_iInter_eq, RingHom.injective, AlgHom.toRingHom, Set.injOn_of_injective
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
f : E →ₐ[F] K
⊢ f.fieldRange = map f ⊤

Tactic:
SetLike.ext' Set.image_univ.symm

Premises used: Set.image_univ, SetLike.ext', Eq.symm
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
L : Type u_4
inst_5 : Field L
inst_6 : Algebra F L
f : E →ₐ[F] K
g : K →ₐ[F] L
⊢ map g f.fieldRange = (g.comp f).fieldRange

Tactic:
SetLike.ext' (Set.range_comp g f).symm

Premises used: Set.range_comp, SetLike.ext', Eq.symm, DFunLike.coe
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
f : E →ₐ[F] K
⊢ f.fieldRange = ⊤ ↔ Function.Surjective.{u_2 + 1, u_3 + 1} (α := E) (β := K) (⇑f : (a : E) → K)

Tactic:
SetLike.ext'_iff.trans Set.range_eq_univ

Premises used: Set.range_eq_univ, SetLike.ext'_iff, Iff.trans
-- 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 : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
f : E ≃ₐ[F] K
⊢ (↑f : E →ₐ[F] K).fieldRange = ⊤

Tactic:
AlgHom.fieldRange_eq_top.mpr f.surjective

Premises used: Iff.mpr, AlgHom.fieldRange_eq_top, AlgEquiv.surjective
-- 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
⊢ (↑(adjoin F S) : Set E) = Set.range (ι := ↥(adjoin F S)) (⇑(algebraMap (↥(adjoin F S)) E) : (a : ↥(adjoin F S)) → E)

Tactic:
Subtype.range_coe.symm

Premises used: Subtype.range_coe, Eq.symm
-- 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 : F
⊢ Membership.mem (α := E) (γ := IntermediateField F E) (adjoin F S) ((algebraMap F E : (a : F) → E) x : E)

Tactic:
IntermediateField.algebraMap_mem (adjoin F S) x

Premises used: IntermediateField.algebraMap_mem, 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 : Set E
⊢ Set.range.{u_2, u_1 + 1} (ι := F) (⇑(algebraMap F E) : (a : F) → E) ⊆ (↑(adjoin F S) : Set E)

Tactic:
set_range_subset (adjoin F S)

Premises used: IntermediateField.adjoin, IntermediateField.set_range_subset
-- 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
⊢ S ⊆ (↑(adjoin F S) : Set E)

Tactic:
fun _ hx => Subfield.subset_closure (Or.inr hx)

Premises used: Set.Mem, Set.Subset, Subfield.subset_closure, Or.inr
-- 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
s : E
hs : s ∈ S
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F S) s

Tactic:
subset_adjoin F S hs

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 : Set E
s : E
hs : s ∉ adjoin F S
⊢ s ∉ S

Tactic:
fun h =>
  hs <| mem_adjoin_of_mem F h

Premises used: IntermediateField.mem_adjoin_of_mem, Not