awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L ≤ finrank (↥E) L
l : L
hl : l ∈ E
rwa : l ∈ extendScalars ⋯
rwa₁ : l ∈ extendScalars h_le
rwa₂ rwa₃ rwa₄ rwa₅ : l ∈ E
⊢ l ∈ F

Tactic:
rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]

Premises used: Iff.mpr, le_refl, _private.0.IntermediateField.eq_of_le_of_finrank_le'', IntermediateField.mem_extendScalars, IntermediateField.extendScalars_le_extendScalars_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h_le : F ≤ E
h_finrank : finrank (↥F) L = finrank (↥E) L
⊢ F = E

Tactic:
eq_of_le_of_finrank_le' h_le h_finrank.le

Premises used: Eq.le, IntermediateField.eq_of_le_of_finrank_le'
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
⊢ IsScalarTower (↥F) (↥E) L

Tactic:
have : IsScalarTower F E L := .of_algebraMap_eq' rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L < finrank (↥F) L

Tactic:
lt_of_le_of_ne ?_ ?_

Premises used: lt_of_le_of_ne
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
refine_1 : finrank (↥E) L ≤ finrank (↥F) L
refine_2 : finrank (↥E) L ≠ finrank (↥F) L
⊢ finrank (↥E) L < finrank (↥F) L

Tactic:
refine lt_of_le_of_ne ?_ ?_

Premises used: lt_of_le_of_ne
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L

Tactic:
Module.finrank_top_le_finrank_of_isScalarTower _ _ _

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≤ finrank (↥F) L

Tactic:
exact Module.finrank_top_le_finrank_of_isScalarTower _ _ _

Premises used: Module.finrank_top_le_finrank_of_isScalarTower
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L

Tactic:
.symm (mt (eq_of_le_of_finrank_eq' H.le) H.ne)

Premises used: mt, LT.lt.le, Ne.symm, IntermediateField.eq_of_le_of_finrank_eq', LT.lt.ne
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
H : F < E
this_1 : Algebra ↥F ↥E := (inclusion ⋯).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ≠ finrank (↥F) L

Tactic:
exact .symm (mt (eq_of_le_of_finrank_eq' H.le) H.ne)
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
⊢ IsScalarTower (↥F) (↥E) L

Tactic:
have : IsScalarTower F E L := IsScalarTower.of_algebraMap_eq fun x ↦ rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ∣ finrank (↥F) L

Tactic:
Dvd.intro_left (finrank F E) (finrank_mul_finrank F E L)

Premises used: Membership.mem, Subtype, Dvd.intro_left, Module.finrank_mul_finrank, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
this : IsScalarTower (↥F) (↥E) L
⊢ finrank (↥E) L ∣ finrank (↥F) L

Tactic:
exact Dvd.intro_left (finrank F E) (finrank_mul_finrank F E L)

Premises used: Membership.mem, Subtype, Dvd.intro_left, Module.finrank_mul_finrank, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
⊢ finrank.{u_1, u_2} K ↥F ∣ finrank.{u_1, u_2} K ↥E

Tactic:
Dvd.intro (finrank F E) (finrank_mul_finrank K F E)

Premises used: Dvd.intro, Membership.mem, Subtype, Module.finrank_mul_finrank, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
h : F ≤ E
x : Algebra ↥F ↥E := (inclusion h).toAlgebra
⊢ finrank.{u_1, u_2} K ↥F ∣ finrank.{u_1, u_2} K ↥E

Tactic:
exact Dvd.intro (finrank F E) (finrank_mul_finrank K F E)

Premises used: Dvd.intro, Membership.mem, Subtype, Module.finrank_mul_finrank, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional (↥F) L
h : F ≤ E
⊢ finrank (↥E) L ≤ finrank (↥F) L

Tactic:
Nat.le_of_dvd Module.finrank_pos (finrank_dvd_of_le_left h)

Premises used: Nat.le_of_dvd, IntermediateField.finrank_dvd_of_le_left, Module.finrank_pos
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
F E : IntermediateField K L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
h : F ≤ E
⊢ finrank.{u_1, u_2} K ↥F ≤ finrank.{u_1, u_2} K ↥E

Tactic:
Nat.le_of_dvd Module.finrank_pos (finrank_dvd_of_le_right h)

Premises used: Nat.le_of_dvd, IntermediateField.finrank_dvd_of_le_right, Module.finrank_pos
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S F E : IntermediateField K L
f : L →ₐ[K] L
inst_3 : FiniteDimensional.{u_1, u_2} K ↥E
⊢ FiniteDimensional.{u_1, u_2} K ↥(map f E)

Tactic:
LinearEquiv.finiteDimensional (IntermediateField.equivMap E f).toLinearEquiv

Premises used: LinearEquiv.finiteDimensional, AlgEquiv.toLinearEquiv, IntermediateField.equivMap
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ IsAlgebraic K x ↔ IsAlgebraic K (↑x : L)

Tactic:
(isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, isAlgebraic_algebraMap_iff, Iff.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ IsIntegral K x ↔ IsIntegral K (↑x : L)

Tactic:
(isIntegral_algHom_iff S.val S.val.injective).symm

Premises used: isIntegral_algHom_iff, RingHom.injective, AlgHom.toRingHom, IntermediateField.val, Iff.symm
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ Eq (α := Polynomial K) (minpoly K x) (minpoly K (↑x : L))

Tactic:
(minpoly.algebraMap_eq (algebraMap S L).injective x).symm

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, Eq.symm, minpoly.algebraMap_eq
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
S : Subalgebra K L
x : L
⊢ Membership.mem (γ := IntermediateField K L)
      ((subalgebraEquivIntermediateField : (a : Subalgebra K L) → IntermediateField K L) S : IntermediateField K L) x ↔
    x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Algebraic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
S : IntermediateField K L
x : L
⊢ Membership.mem (γ := Subalgebra K L)
      ((OrderIso.symm subalgebraEquivIntermediateField : (a : IntermediateField K L) → Subalgebra K L) S :
        Subalgebra K L)
      x ↔
    x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S : IntermediateField K L
toSubsemiring : Subsemiring L
algebraMap_mem' : ∀ (r : K), Membership.mem (α := L) toSubsemiring.carrier ((algebraMap K L : (a : K) → L) r : L)
inv_mem' :
  ∀ x ∈ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra K L }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' : Subalgebra K L }.carrier
toSubsemiring_1 : Subsemiring L
algebraMap_mem'_1 : ∀ (r : K), Membership.mem (α := L) toSubsemiring_1.carrier ((algebraMap K L : (a : K) → L) r : L)
inv_mem'_1 :
  ∀ x ∈ { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 : Subalgebra K L }.carrier,
    x⁻¹ ∈ { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1 : Subalgebra K L }.carrier
⊢ Eq.{u_2 + 1} (α := Set L)
      ((fun (S : IntermediateField K L) ↦ S.carrier)
        { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem', inv_mem' := inv_mem' })
      ((fun (S : IntermediateField K L) ↦ S.carrier)
        { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1, inv_mem' := inv_mem'_1 }) →
    { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem', inv_mem' := inv_mem' :
        IntermediateField K L } =
      { toSubsemiring := toSubsemiring_1, algebraMap_mem' := algebraMap_mem'_1, inv_mem' := inv_mem'_1 }

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
⊢ -x ∈ S.toSubalgebra

Tactic:
simpa
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : IntermediateField K L
x : L
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S T : IntermediateField K L
h : ∀ (x : L), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ (↑S.toSubalgebra : Set L) = (↑S : Set L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ (↑S.toSubfield : Set L) = (↑S : Set L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ ↥S.toSubalgebra = ↥S

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ ↥S.toSubfield = ↥S

Tactic:
rfl

Premises used: Set.Mem, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : Subsemiring L
hK : ∀ (x : K), Membership.mem (α := L) s ((algebraMap K L : (a : K) → L) x : L)
hi :
  ∀ x ∈ { toSubsemiring := s, algebraMap_mem' := hK : Subalgebra K L }.carrier,
    x⁻¹ ∈ { toSubsemiring := s, algebraMap_mem' := hK : Subalgebra K L }.carrier
x : L
⊢ x ∈ { toSubsemiring := s, algebraMap_mem' := hK, inv_mem' := hi : IntermediateField K L } ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : IntermediateField K L
x : L
⊢ x ∈ s.toSubalgebra ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
s : IntermediateField K L
x : L
⊢ x ∈ s.toSubfield ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ StrictMono.{u_2, u_2} (α := IntermediateField K L) toSubalgebra

Tactic:
fun _ _ h ↦ h

Premises used: StrictMono
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
s : Set L
hs : s = (↑S : Set L)
⊢ (↑(S.copy s hs) : Set L) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
s : Set L
hs : s = (↑S : Set L)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : K
⊢ Membership.mem (α := L) S ((algebraMap K L : (a : K) → L) x : L)

Tactic:
S.algebraMap_mem' x

Premises used: Set.Mem, Subalgebra.algebraMap_mem', IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
y : L
⊢ y ∈ S → ∀ {x : K}, x • y ∈ S

Tactic:
S.toSubalgebra.smul_mem

Premises used: Set.Mem, Subalgebra.smul_mem, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ 1 ∈ S

Tactic:
one_mem S

Premises used: Set.Mem, OneMemClass.one_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ 0 ∈ S

Tactic:
zero_mem S

Premises used: Set.Mem, ZeroMemClass.zero_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : L
⊢ x ∈ S → y ∈ S → x * y ∈ S

Tactic:
mul_mem

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : L
⊢ x ∈ S → y ∈ S → x + y ∈ S

Tactic:
add_mem

Premises used: AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : L
⊢ x ∈ S → y ∈ S → x - y ∈ S

Tactic:
sub_mem

Premises used: sub_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
⊢ x ∈ S → x⁻¹ ∈ S

Tactic:
inv_mem

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : L
⊢ x ∈ S → y ∈ S → x / y ∈ S

Tactic:
div_mem

Premises used: div_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
l : List L
⊢ (∀ x ∈ l, x ∈ S) → l.prod ∈ S

Tactic:
list_prod_mem

Premises used: list_prod_mem, Set.Mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
l : List L
⊢ (∀ x ∈ l, x ∈ S) → l.sum ∈ S

Tactic:
list_sum_mem

Premises used: Set.Mem, list_sum_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
m : Multiset L
⊢ (∀ a ∈ m, a ∈ S) → m.prod ∈ S

Tactic:
multiset_prod_mem m

Premises used: multiset_prod_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
m : Multiset L
⊢ (∀ a ∈ m, a ∈ S) → m.sum ∈ S

Tactic:
multiset_sum_mem m

Premises used: multiset_sum_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
ι : Type u_4
t : Finset ι
f : ι → L
h : ∀ c ∈ t, f c ∈ S
⊢ ∏ i ∈ t, f i ∈ S

Tactic:
prod_mem h

Premises used: prod_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
ι : Type u_4
t : Finset ι
f : ι → L
h : ∀ c ∈ t, f c ∈ S
⊢ ∑ i ∈ t, f i ∈ S

Tactic:
sum_mem h

Premises used: sum_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
n : ℤ
⊢ x ^ n ∈ S

Tactic:
zpow_mem hx n

Premises used: zpow_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
hx : x ∈ S
n : ℤ
⊢ n • x ∈ S

Tactic:
zsmul_mem hx n

Premises used: zsmul_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
n : ℤ
⊢ (↑n : L) ∈ S

Tactic:
intCast_mem S n

Premises used: intCast_mem, Set.Mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : ↥S
⊢ (↑(x + y) : L) = (↑x : L) + (↑y : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ (↑(-x) : L) = -(↑x : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : ↥S
⊢ (↑(x * y) : L) = (↑x : L) * (↑y : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
⊢ (↑x⁻¹ : L) = (↑x : L)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x y : ↥S
⊢ (↑(x / y) : L) = (↑x : L) / (↑y : L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ Eq.{u_2 + 1} (α := L) (↑0 : L) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
⊢ Eq.{u_2 + 1} (α := L) (↑1 : L) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : ↥S
n : ℕ
⊢ (↑(x ^ n) : L) = (↑x : L) ^ n

Tactic:
SubmonoidClass.coe_pow x n

Premises used: SubmonoidClass.coe_pow
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
n : ℕ
⊢ (↑n : L) ∈ S

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
h : ∀ (x : L), x ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x ∈ S
⊢ (S.toIntermediateField inv_mem).toSubalgebra = S

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
x : L
⊢ x ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x ∈ S

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
h : ∀ (x : L), x ∈ S.toIntermediateField ⋯ ↔ x ∈ S
⊢ S.toIntermediateField ⋯ = S

Tactic:
ext
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
S : IntermediateField K L
x : L
⊢ x ∈ S.toIntermediateField ⋯ ↔ x ∈ S

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
pos : ∀ (hx0 : x = 0), x⁻¹ ∈ S
neg : ∀ (hx0 : ¬x = 0), x⁻¹ ∈ S
⊢ x⁻¹ ∈ S

Tactic:
by_cases hx0 : x = 0
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : x = 0
pos : 0 ∈ S
⊢ x⁻¹ ∈ S

Tactic:
rw [hx0, inv_zero]

Premises used: inv_zero
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ 0 ∈ S

Tactic:
S.zero_mem

Premises used: Set.Mem, Subalgebra.zero_mem
-- Module: Mathlib.FieldTheory.IntermediateField.Basic
Goal:
K : Type u_1
L : Type u_2
L' : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field L'
inst_3 : Algebra K L
inst_4 : Algebra K L'
S_1 : IntermediateField K L
S : Subalgebra K L
hS : IsField.{u_2} ↥S
x : L
hx : x ∈ S
hx0 : x = 0
⊢ 0 ∈ S

Tactic:
exact S.zero_mem

Premises used: Subalgebra.zero_mem