awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
halg : Algebra.IsAlgebraic.{u_3, u_4} K ↥E1 ∨ Algebra.IsAlgebraic.{u_3, u_4} K ↥E2
this :
  Module.rank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Module.rank K ↥(E1 ⊔ E2).toSubalgebra ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra),
    Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2

Tactic:
rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this

Premises used: IntermediateField.sup_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
pos :
  ∀ (h : FiniteDimensional.{u_3, u_4} K ↥E1),
    finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
neg :
  ∀ (h : ¬FiniteDimensional.{u_3, u_4} K ↥E1),
    finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2

Tactic:
by_cases h : FiniteDimensional K E1

Premises used: Membership.mem, Subtype, FiniteDimensional
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional.{u_3, u_4} K ↥E1
⊢ finrank.{u_3, u_4} K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤
    finrank.{u_3, u_4} K ↥E1.toSubalgebra * finrank.{u_3, u_4} K ↥E2.toSubalgebra

Tactic:
have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional.{u_3, u_4} K ↥E1
this :
  finrank.{u_3, u_4} K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤
    finrank.{u_3, u_4} K ↥E1.toSubalgebra * finrank.{u_3, u_4} K ↥E2.toSubalgebra
⊢ finrank.{u_3, u_4} K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2

Tactic:
change _ ≤ finrank K E1 * finrank K E2 at this

Premises used: Membership.mem, Subtype, Module.finrank
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : FiniteDimensional.{u_3, u_4} K ↥E1
this : finrank.{u_3, u_4} K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
pos pos₁ pos₂ pos₃ :
  ∀ (this : finrank.{u_3, u_4} K ↥(E1 ⊔ E2).toSubalgebra ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2),
    finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2

Tactic:
rwa [← sup_toSubalgebra_of_left] at this

Premises used: IntermediateField.sup_toSubalgebra_of_left
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : ¬FiniteDimensional.{u_3, u_4} K ↥E1
⊢ Cardinal.aleph0 ≤ Module.rank K ↥E1

Tactic:
rw [FiniteDimensional, ← rank_lt_aleph0_iff, not_lt] at h

Premises used: Module.rank_lt_aleph0_iff, FiniteDimensional, not_lt
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
⊢ LE.le (α := Submodule K L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) E1.toSubalgebra : Submodule K L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (E1 ⊔ E2).toSubalgebra : Submodule K L)

Tactic:
simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
⊢ Module.rank K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) E1.toSubalgebra : Submodule K L) ≤
    Module.rank K
      ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (E1 ⊔ E2).toSubalgebra : Submodule K L)

Tactic:
have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show Subalgebra.toSubmodule E1.toSubalgebra ≤ Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra by
      simp
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
E1 E2 : IntermediateField K L
h : Cardinal.aleph0 ≤ Module.rank K ↥E1
this :
  Module.rank K ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) E1.toSubalgebra : Submodule K L) ≤
    Module.rank K
      ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (E1 ⊔ E2).toSubalgebra : Submodule K L)
neg : finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ 0 * finrank.{u_3, u_4} K ↥E2
neg₁ : 0 ≤ 0 * finrank.{u_3, u_4} K ↥E2
neg₂ neg₃ : LE.le (α := ℕ) 0 0
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2

Tactic:
rw [show finrank K E1 = 0 from Cardinal.toNat_apply_of_aleph0_le h,
    show finrank K ↥(E1 ⊔ E2) = 0 from Cardinal.toNat_apply_of_aleph0_le (h.trans this), zero_mul]

Premises used: Cardinal.toNat_apply_of_aleph0_le, MulZeroClass.zero_mul, LE.le.trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
inst_3 : Nonempty ι
dir : Directed (fun (x1 x2 : IntermediateField K L) ↦ x1 ≤ x2) t
⊢ (↑(iSup t) : Set L) = ⋃ (i : ι), (↑(t i) : Set L)

Tactic:
let M : IntermediateField K L :=
    { __ := Subalgebra.copy _ _ (Subalgebra.coe_iSup_of_directed dir).symm
      inv_mem' := fun _ hx ↦ have ⟨i, hi⟩ := Set.mem_iUnion.mp hx
        Set.mem_iUnion.mpr ⟨i, (t i).inv_mem hi⟩ }
  have : iSup t = M := le_antisymm
    (iSup_le fun i ↦ le_iSup (fun i ↦ (t i : Set L)) i) (Set.iUnion_subset fun _ ↦ le_iSup t _)
  this.symm ▸ rfl

Premises used: Iff.mpr, Subalgebra.coe_iSup_of_directed, IntermediateField.mk, _private.0.IntermediateField.coe_iSup_of_directed.match_1, Set.iUnion_subset, iSup, Submonoid.toSubsemigroup, Set.mem_iUnion, Membership.mem, Eq.rec, le_iSup, Subalgebra.toSubsemiring, Subsemiring.toSubmonoid, le_antisymm, Inv.inv, SetLike.coe, Exists.intro, Subsemigroup.carrier, Iff.mp, iSup_le, IntermediateField.inv_mem, Eq.symm, Set.iUnion, IntermediateField.toSubalgebra, Subalgebra.copy, rfl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun (x1 x2 : IntermediateField K L) ↦ x1 ≤ x2) t
inl : IsEmpty ι → (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
inr : Nonempty ι → (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun (x1 x2 : IntermediateField K L) ↦ x1 ≤ x2) t
h : IsEmpty ι
inl : Eq.{u_4 + 1} (α := Subalgebra K L) (toSubalgebra ⊥) ⊥
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra

Tactic:
simp_rw [iSup_of_empty, bot_toSubalgebra]

Premises used: IntermediateField.bot_toSubalgebra, iSup_of_empty
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun (x1 x2 : IntermediateField K L) ↦ x1 ≤ x2) t
h : Nonempty ι
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra

Tactic:
SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)

Premises used: Subalgebra.coe_iSup_of_directed, IntermediateField.coe_iSup_of_directed, SetLike.ext', Eq.symm, Eq.trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
dir : Directed (fun (x1 x2 : IntermediateField K L) ↦ x1 ≤ x2) t
h : Nonempty ι
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra

Tactic:
exact SetLike.ext' ((coe_iSup_of_directed dir).trans (Subalgebra.coe_iSup_of_directed dir).symm)

Premises used: IntermediateField.coe_iSup_of_directed, SetLike.ext', Eq.trans
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
rw : FiniteDimensional.{u_3, u_4} K ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), t x)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ (i : ι), t i)

Tactic:
rw [← iSup_univ]

Premises used: iSup_univ
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
empty : FiniteDimensional.{u_3, u_4} K ↥⊥
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), t x)

Tactic:
rw [iSup_emptyset]

Premises used: iSup_emptyset
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
⊢ FiniteDimensional.{u_3, u_4} K ↥⊥

Tactic:
(botEquiv K L).symm.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional, AlgEquiv.symm, Set.Mem, AlgEquiv.toLinearEquiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
⊢ FiniteDimensional.{u_3, u_4} K ↥⊥

Tactic:
exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional

Premises used: LinearEquiv.finiteDimensional, AlgEquiv.symm, AlgEquiv.toLinearEquiv, IntermediateField.botEquiv
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
a : ι
s_1 : Set ι
s : a ∉ s_1
hs : s_1.Finite
h_1 : FiniteDimensional.{u_3, u_4} K ↥(⨆ x ∈ s_1, t x)
insert : FiniteDimensional.{u_3, u_4} K ↥(t a ⊔ ⨆ x ∈ s_1, t x)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ x ∈ Insert.insert a s_1, t x)

Tactic:
rw [iSup_insert]

Premises used: iSup_insert
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
a : ι
s_1 : Set ι
s : a ∉ s_1
hs : s_1.Finite
h_1 : FiniteDimensional.{u_3, u_4} K ↥(⨆ x ∈ s_1, t x)
⊢ FiniteDimensional.{u_3, u_4} K ↥(t a ⊔ ⨆ x ∈ s_1, t x)

Tactic:
IntermediateField.finiteDimensional_sup _ _

Premises used: Set.Mem, IntermediateField.finiteDimensional_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
x : Set ι
a : ι
s_1 : Set ι
s : a ∉ s_1
hs : s_1.Finite
h_1 : FiniteDimensional.{u_3, u_4} K ↥(⨆ x ∈ s_1, t x)
⊢ FiniteDimensional.{u_3, u_4} K ↥(t a ⊔ ⨆ x ∈ s_1, t x)

Tactic:
exact IntermediateField.finiteDimensional_sup _ _

Premises used: IntermediateField.finiteDimensional_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
h : Finite ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
induction : ∀ (x : Set ι), x.Finite → FiniteDimensional.{u_3, u_4} K ↥(⨆ x_2 ∈ x, t x_2)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), t x)

Tactic:
induction Set.univ, Set.finite_univ (α := ι) using Set.Finite.induction_on with
  | empty =>
    rw [iSup_emptyset]
    exact (botEquiv K L).symm.toLinearEquiv.finiteDimensional
  | insert s hs =>
    rw [iSup_insert]
    exact IntermediateField.finiteDimensional_sup _ _

Premises used: iSup_insert, LinearEquiv.finiteDimensional, AlgEquiv.symm, Set.univ, Insert.insert, iSup_emptyset, Set.finite_univ, AlgEquiv.toLinearEquiv, IntermediateField.botEquiv, IntermediateField.finiteDimensional_sup
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
S : Set E
K : Type u_3
L : Type u_4
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra K L
E1 E2 : IntermediateField K L
ι : Type u_5
t : ι → IntermediateField K L
s : Finset ι
inst_6 : ∀ (i : ι), FiniteDimensional.{u_3, u_4} K ↥(t i)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ i ∈ s, t i)

Tactic:
iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite

Premises used: Set.Mem, setOf, iSup_subtype'', Eq.rec, IntermediateField.finiteDimensional_iSup_of_finite
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
s : Finset ι
h : ∀ i ∈ s, FiniteDimensional.{u_3, u_4} K ↥(t i)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ i ∈ s, t i)

Tactic:
have := Subtype.forall'.mp h
  iSup_subtype'' s t ▸ IntermediateField.finiteDimensional_iSup_of_finite

Premises used: Set.Mem, setOf, iSup_subtype'', Eq.rec, SetLike.coe, IntermediateField.finiteDimensional_iSup_of_finite, Iff.mp, Subtype.forall'
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
h : ∀ i ∈ s, IsSplittingField.{u_3, u_4} K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
⊢ ∀ i ∈ s, t i ≤ F

Tactic:
have hF : ∀ i ∈ s, t i ≤ F := fun i hi ↦ le_iSup_of_le i (le_iSup (fun _ ↦ t i) hi)
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
h : ∀ i ∈ s, IsSplittingField.{u_3, u_4} K (↥(t i)) (p i)
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
simp :
  ∀
    (h :
      ∀ i ∈ s,
        Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)),
    Splits.{u_4} (R := ↥(⨆ i ∈ s, t i)) (∏ i ∈ s, Polynomial.map (algebraMap K ↥(⨆ i ∈ s, t i)) (p i)) ∧
      Eq (α := IntermediateField K L) (⨆ i ∈ s, t i) (adjoin K (rootSet.{u_3, u_4} (T := K) (∏ i ∈ s, p i) L))
⊢ IsSplittingField.{u_3, u_4} K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)

Tactic:
simp only [isSplittingField_iff, Polynomial.map_prod] at h ⊢

Premises used: Polynomial.map_prod, IntermediateField.isSplittingField_iff
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)
i : ι
hi : i ∈ s
⊢ Splits.{u_4} (R := ↥(⨆ i ∈ s, t i)) (Polynomial.map (algebraMap K ↥(⨆ i ∈ s, t i)) (p i))

Tactic:
simpa [Polynomial.map_map] using (h i hi).1.map (inclusion (hF i hi)).toRingHom

Premises used: And.left, AlgHom.toRingHom, IntermediateField.inclusion, Polynomial.Splits.map, Polynomial.map_map
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)
refine : Eq (α := IntermediateField K L) (⨆ i ∈ s, t i) (adjoin K (rootSet.{u_3, u_4} (T := K) (∏ i ∈ s, p i) L))
⊢ Splits.{u_4} (R := ↥(⨆ i ∈ s, t i)) (∏ i ∈ s, Polynomial.map (algebraMap K ↥(⨆ i ∈ s, t i)) (p i)) ∧
    Eq (α := IntermediateField K L) (⨆ i ∈ s, t i) (adjoin K (rootSet.{u_3, u_4} (T := K) (∏ i ∈ s, p i) L))

Tactic:
refine ⟨Splits.prod fun i hi ↦ by
    simpa [Polynomial.map_map] using (h i hi).1.map (inclusion (hF i hi)).toRingHom, ?_⟩
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)
simp : Eq.{u_4 + 1} (α := IntermediateField K L) (⨆ i ∈ s, t i) (⨆ i ∈ s, adjoin K ((p i).rootSet L))
⊢ Eq (α := IntermediateField K L) (⨆ i ∈ s, t i) (adjoin K (rootSet.{u_3, u_4} (T := K) (∏ i ∈ s, p i) L))

Tactic:
simp only [rootSet_prod p s h0, ← Set.iSup_eq_iUnion, (@gc K _ L _ _).l_iSup₂]

Premises used: Set.iSup_eq_iUnion, GaloisConnection.l_iSup₂, IntermediateField.gc, Polynomial.rootSet_prod
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (⨆ i ∈ s, t i) (⨆ i ∈ s, adjoin K ((p i).rootSet L))

Tactic:
iSup_congr fun i ↦ iSup_congr fun hi ↦ (h i hi).2

Premises used: And.right, iSup_congr
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
K : Type u_3
L : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type u_5
t : ι → IntermediateField K L
p : ι → K[X]
s : Finset ι
h0 : Ne.{u_3 + 1} (α := K[X]) (∏ i ∈ s, p i) 0
F : IntermediateField K L := ⨆ i ∈ s, t i
hF : ∀ i ∈ s, t i ≤ F
h : ∀ i ∈ s, Splits.{u_4} (R := ↥(t i)) (Polynomial.map (algebraMap K ↥(t i)) (p i)) ∧ t i = adjoin K ((p i).rootSet L)
⊢ Eq.{u_4 + 1} (α := IntermediateField K L) (⨆ i ∈ s, t i) (⨆ i ∈ s, adjoin K ((p i).rootSet L))

Tactic:
exact iSup_congr fun i ↦ iSup_congr fun hi ↦ (h i hi).2

Premises used: And.right, iSup_congr
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
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
⊢ Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L.toSubalgebra : Set K)))
    (Algebra.adjoin E (↑L.toSubalgebra : Set K))

Tactic:
have h : (adjoin E (L.toSubalgebra : Set K)).toSubalgebra =
      Algebra.adjoin E (L.toSubalgebra : Set K) :=
    L.adjoin_intermediateField_toSubalgebra_of_isAlgebraic E halg
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
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
h :
  Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L.toSubalgebra : Set K)))
    (Algebra.adjoin E (↑L.toSubalgebra : Set K))
⊢ Module.rank E ↥(Algebra.adjoin E (↑L.toSubalgebra : Set K)) ≤ Module.rank F ↥L.toSubalgebra

Tactic:
have := L.toSubalgebra.adjoin_rank_le E
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
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
h :
  Eq (α := Subalgebra E K) (toSubalgebra (adjoin E (↑L.toSubalgebra : Set K)))
    (Algebra.adjoin E (↑L.toSubalgebra : Set K))
this : Module.rank E ↥(Algebra.adjoin E (↑L.toSubalgebra : Set K)) ≤ Module.rank F ↥L.toSubalgebra
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Module.rank E ↥(toSubalgebra (adjoin E (↑L.toSubalgebra : Set K))) ≤ Module.rank F ↥L.toSubalgebra),
    Module.rank E ↥(adjoin E (↑L : Set K)) ≤ Module.rank F ↥L
⊢ Module.rank E ↥(adjoin E (↑L : Set K)) ≤ Module.rank F ↥L

Tactic:
rwa [(Subalgebra.equivOfEq _ _ h).symm.toLinearEquiv.rank_eq] at this

Premises used: AlgEquiv.symm, Subalgebra.equivOfEq, LinearEquiv.rank_eq, AlgEquiv.toLinearEquiv
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
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
⊢ Module.rank E ↥(adjoin E (↑L : Set K)) ≤ Module.rank F ↥L

Tactic:
adjoin_rank_le_of_isAlgebraic E L (Or.inl halg)

Premises used: IntermediateField.adjoin_rank_le_of_isAlgebraic, Or.inl
-- Module: Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
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
⊢ Module.rank E ↥(adjoin E (↑L : Set K)) ≤ Module.rank F ↥L

Tactic:
adjoin_rank_le_of_isAlgebraic E L (Or.inr halg)

Premises used: IntermediateField.adjoin_rank_le_of_isAlgebraic, Or.inr