awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
hα : IsAlgebraic F α
⊢ ∀ (x : E), Membership.mem (γ := Set E) {α} x → IsAlgebraic F x

Tactic:
simpa
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
α : E
hα : IsIntegral F α
⊢ ∀ (x : E), Membership.mem (γ := Set E) {α} x → IsAlgebraic F x

Tactic:
simpa [isAlgebraic_iff_isIntegral]

Premises used: isAlgebraic_iff_isIntegral
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
S : Set E
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (Algebra.adjoin F S)

Tactic:
adjoin_toSubalgebra_of_isAlgebraic fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x

Premises used: Algebra.IsAlgebraic.isAlgebraic, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
hS : ∀ x ∈ S, IsAlgebraic F x
rw : Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
rw₁ :
  Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) (toSubalgebra ⊤) ↔
    Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
rw₂ rw₃ :
  Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤ ↔ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F S)) ⊤
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤

Tactic:
rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic hS,
      ← IntermediateField.toSubalgebra_inj,
      IntermediateField.top_toSubalgebra]

Premises used: IntermediateField.top_toSubalgebra, IntermediateField.toSubalgebra_inj, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : IsAlgebraic F x
⊢ ∀ (x_1 : E), Membership.mem (γ := Set E) {x} x_1 → IsAlgebraic F x_1

Tactic:
simp [hx]
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Algebra.IsAlgebraic F E
S : Set E
⊢ Eq (α := IntermediateField F E) (adjoin F S) ⊤ ↔ Eq (α := Subalgebra F E) (Algebra.adjoin F S) ⊤

Tactic:
adjoin_eq_top_iff_of_isAlgebraic (fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x)

Premises used: IntermediateField.adjoin_eq_top_iff_of_isAlgebraic, Algebra.IsAlgebraic.isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
obtain : ∀ (s : Finset E) (hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤), Module.Finite F E
⊢ Module.Finite F E

Tactic:
obtain ⟨s, hs⟩ := fg_top F E

Premises used: IntermediateField.fg_top
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
h : Eq (α := Subalgebra F E) (Algebra.adjoin F (↑s : Set E)) ⊤
⊢ FiniteType F E

Tactic:
use s
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
h : Eq (α := Subalgebra F E) (toSubalgebra (adjoin F (↑s : Set E))) ⊤
⊢ Eq (α := Subalgebra F E) (Algebra.adjoin F (↑s : Set E)) ⊤

Tactic:
rw [← adjoin_toSubalgebra_of_isAlgebraic fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x]

Premises used: Algebra.IsAlgebraic.isAlgebraic, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ Eq (α := Subalgebra F E) (toSubalgebra (adjoin F (↑s : Set E))) ⊤

Tactic:
simpa [← toSubalgebra_inj] using hs

Premises used: IntermediateField.toSubalgebra_inj
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
⊢ FiniteType F E

Tactic:
have : Algebra.FiniteType F E := by
    use s
    rw [← adjoin_toSubalgebra_of_isAlgebraic fun x hx ↦ Algebra.IsAlgebraic.isAlgebraic x]
    simpa [← toSubalgebra_inj] using hs
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : FiniteType F E
⊢ Module.Finite F E

Tactic:
Algebra.IsIntegral.finite

Premises used: Algebra.IsIntegral.finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : EssFiniteType F E
inst_4 : Algebra.IsAlgebraic F E
s : Finset E
hs : Eq (α := IntermediateField F E) (adjoin F (↑s : Set E)) ⊤
this : FiniteType F E
⊢ Module.Finite F E

Tactic:
exact Algebra.IsIntegral.finite

Premises used: Algebra.IsIntegral.finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
A : Type u_3
B : Type u_4
C : Type u_5
inst_3 : Field A
inst_4 : CommSemiring B
inst_5 : Field C
inst_6 : Algebra A B
inst_7 : Algebra B C
inst_8 : Algebra A C
inst_9 : IsScalarTower A B C
b : B
⊢ IsScalarTower.{u_4, u_5, u_5} (↥A[b]) (↥A⟮((algebraMap B C : (a : B) → C) b : C)⟯) C

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: Set.Mem, IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
⊢ E1.toSubalgebra ⊔ E2.toSubalgebra ≤ (E1 ⊔ E2).toSubalgebra

Tactic:
sup_le (show E1 ≤ E1 ⊔ E2 from le_sup_left) (show E2 ≤ E1 ⊔ E2 from le_sup_right)

Premises used: le_sup_left, le_sup_right, sup_le
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
⊢ Eq (α := Subalgebra (↥E1) L) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))) (Algebra.adjoin ↥E1 (↑E2 : Set L))

Tactic:
have : (adjoin E1 (E2 : Set L)).toSubalgebra = _ := adjoin_toSubalgebra_of_isAlgebraic fun x h ↦
    IsAlgebraic.tower_top _ (isAlgebraic_iff.mp (Algebra.IsAlgebraic.isAlgebraic (⟨x, h⟩ : E2)))
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this : Eq (α := Subalgebra (↥E1) L) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))) (Algebra.adjoin ↥E1 (↑E2 : Set L))
⊢ Eq (α := Subalgebra K L) (Subalgebra.restrictScalars K (S := ↥E1) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))

Tactic:
apply_fun Subalgebra.restrictScalars K at this

Premises used: Subalgebra.restrictScalars
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (Subalgebra.restrictScalars K (S := ↥E1) (toSubalgebra (adjoin ↥E1 (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))
⊢ Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1) (Algebra.adjoin ↥E1 (↑E2 : Set L)))

Tactic:
rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin] at this

Premises used: IntermediateField.restrictScalars_toSubalgebra, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Subalgebra.restrictScalars K (S := ↥E1.toSubalgebra) (Algebra.adjoin ↥E1.toSubalgebra (↑E2 : Set L)))
⊢ Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Algebra.adjoin K ((↑E1.toSubalgebra : Set L) ∪ (↑E2 : Set L)))

Tactic:
rw [Algebra.restrictScalars_adjoin] at this

Premises used: Algebra.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Algebra.adjoin K ((↑E1.toSubalgebra : Set L) ∪ (↑E2 : Set L)))
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
this
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Eq (α := Subalgebra K L) (toSubalgebra (adjoin K ((↑E1 : Set L) ∪ (↑E2 : Set L))))
    (Algebra.adjoin K ((↑E1.toSubalgebra : Set L) ∪ (↑E2 : Set L)))
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
exact this
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1
⊢ (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra

Tactic:
have := sup_toSubalgebra_of_isAlgebraic_right E2 E1
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1
this : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
rwa : (E2 ⊔ E1).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
rwa₁ rwa₂ rwa₃ rwa₄ : (E2 ⊔ E1).toSubalgebra = E2.toSubalgebra ⊔ E1.toSubalgebra
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
rwa [sup_comm (a := E1), sup_comm (a := E1.toSubalgebra)]

Premises used: sup_comm, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
halg.elim (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_left E1 E2)
    (fun _ ↦ sup_toSubalgebra_of_isAlgebraic_right E1 E2)

Premises used: IntermediateField.sup_toSubalgebra_of_isAlgebraic_left, Or.elim, IntermediateField.sup_toSubalgebra_of_isAlgebraic_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : FiniteDimensional.{u_3, u_4} K ↥E1
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
sup_toSubalgebra_of_isAlgebraic_left E1 E2

Premises used: IntermediateField.sup_toSubalgebra_of_isAlgebraic_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_3 : FiniteDimensional.{u_3, u_4} K ↥E2
⊢ (E1 ⊔ E2).toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra

Tactic:
sup_toSubalgebra_of_isAlgebraic_right E1 E2

Premises used: IntermediateField.sup_toSubalgebra_of_isAlgebraic_right
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
h :
  ∀ (x : E),
    Eq (α := K) ((algebraMap E K : (a : E) → K) x : K)
      (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E') x : K)
⊢ Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))

Tactic:
ext x
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
x : E
⊢ Eq (α := K) ((algebraMap E K : (a : E) → K) x : K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E') x : K)

Tactic:
rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
⊢ Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))

Tactic:
have hi : algebraMap E K = (algebraMap E' K) ∘ i' := by ext x; rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := Subalgebra E K) (β := Subalgebra F K) (Subalgebra.restrictScalars F)

Tactic:
Subalgebra.restrictScalars_injective F

Premises used: Subalgebra.restrictScalars_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
apply_fun :
  Eq (α := Subalgebra F K) (Subalgebra.restrictScalars F (toSubalgebra (adjoin E (↑L : Set K))))
    (Subalgebra.restrictScalars F (Algebra.adjoin E (↑L : Set K)))
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L : Set K))) (Algebra.adjoin E (↑L : Set K))

Tactic:
apply_fun _ using Subalgebra.restrictScalars_injective F

Premises used: Subalgebra.restrictScalars_injective
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
rw :
  Eq (α := Subalgebra F K) (toSubalgebra (adjoin F ((↑E' : Set K) ∪ (↑L : Set K))))
    (Subalgebra.restrictScalars F (S := ↥E') (Algebra.adjoin ↥E' (↑L : Set K)))
⊢ Eq (α := Subalgebra F K) (Subalgebra.restrictScalars F (toSubalgebra (adjoin E (↑L : Set K))))
    (Subalgebra.restrictScalars F (Algebra.adjoin E (↑L : Set K)))

Tactic:
rw [← restrictScalars_toSubalgebra, restrictScalars_adjoin_of_algEquiv i' hi,
    Algebra.restrictScalars_adjoin_of_algEquiv i' hi, restrictScalars_adjoin]

Premises used: IntermediateField.restrictScalars_adjoin_of_algEquiv, IntermediateField.restrictScalars_toSubalgebra, Algebra.restrictScalars_adjoin_of_algEquiv, IntermediateField.restrictScalars_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
⊢ Eq (α := Subalgebra F K) (toSubalgebra (adjoin F ((↑E' : Set K) ∪ (↑L : Set K))))
    (Algebra.adjoin F ((↑E'.toSubalgebra : Set K) ∪ (↑L : Set K)))

Tactic:
E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp
    (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)

Premises used: AlgEquiv.isAlgebraic, IntermediateField.sup_toSubalgebra_of_isAlgebraic, id, Or.imp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic.{u_1, u_3} F ↥L
i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K
E' : IntermediateField F K := i.fieldRange
i' : AlgEquiv.{u_1, u_2, u_3} F E ↥E' := AlgEquiv.ofInjectiveField i
hi :
  Eq (α := (a : E) → K) (⇑(algebraMap E K) : (a : E) → K)
    (Function.comp (β := ↥E') (⇑(algebraMap (↥E') K) : (a : ↥E') → K) (⇑i' : (a : E) → ↥E'))
⊢ Eq (α := Subalgebra F K) (toSubalgebra (adjoin F ((↑E' : Set K) ∪ (↑L : Set K))))
    (Algebra.adjoin F ((↑E'.toSubalgebra : Set K) ∪ (↑L : Set K)))

Tactic:
exact E'.sup_toSubalgebra_of_isAlgebraic L (halg.imp
    (fun (_ : Algebra.IsAlgebraic F E) ↦ i'.isAlgebraic) id)

Premises used: AlgEquiv.isAlgebraic, IntermediateField.sup_toSubalgebra_of_isAlgebraic, id, Or.imp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic F E
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L : Set K))) (Algebra.adjoin E (↑L : Set K))

Tactic:
adjoin_intermediateField_toSubalgebra_of_isAlgebraic E L (Or.inl halg)

Premises used: IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic, Or.inl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
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
inst_5 : Algebra E K
inst_6 : IsScalarTower F E K
L : IntermediateField F K
halg : Algebra.IsAlgebraic.{u_1, u_3} F ↥L
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L : Set K))) (Algebra.adjoin E (↑L : Set K))

Tactic:
adjoin_intermediateField_toSubalgebra_of_isAlgebraic E L (Or.inr halg)

Premises used: IntermediateField.adjoin_intermediateField_toSubalgebra_of_isAlgebraic, Or.inr
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
h : S.FG
obtain : ∀ (t : Finset E) (ht : Algebra.adjoin F (↑t : Set E) = S.toSubalgebra), S.FG
⊢ S.FG

Tactic:
obtain ⟨t, ht⟩ := h
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F (↑t : Set E) = S.toSubalgebra
⊢ S.FG

Tactic:
⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩

Premises used: IntermediateField.FG, Exists.intro, Eq.symm, IntermediateField.eq_adjoin_of_eq_algebra_adjoin
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
t : Finset E
ht : Algebra.adjoin F (↑t : Set E) = S.toSubalgebra
⊢ S.FG

Tactic:
exact ⟨t, (eq_adjoin_of_eq_algebra_adjoin _ _ _ ht.symm).symm⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : IntermediateField F E
inst_3 : IsNoetherian F E
⊢ S.FG

Tactic:
S.fg_of_fg_toSubalgebra S.toSubalgebra.fg_of_noetherian

Premises used: Subalgebra.fg_of_noetherian, IntermediateField.fg_of_fg_toSubalgebra, IntermediateField.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : FiniteDimensional F E
P : IntermediateField F E → Prop
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (L' := ↥K) (↥K)⟮x⟯)
K : IntermediateField F E
⊢ P K

Tactic:
letI : IsNoetherian F E := IsNoetherian.iff_fg.2 inferInstance
  induction_on_adjoin_fg P base ih K K.fg_of_noetherian

Premises used: IntermediateField.induction_on_adjoin_fg, IntermediateField.fg_of_noetherian
-- 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 : f.fieldRange.toSubfield = IntermediateField.toSubfield (IntermediateField.adjoin F (↑g.range : Set L))
⊢ f.fieldRange = IntermediateField.adjoin F (↑g.range : Set L)

Tactic:
apply IntermediateField.toSubfield_injective

Premises used: IntermediateField.toSubfield_injective