awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
i : ι → E
x : E
simp_rw :
  (∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) s ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (Set.range i)) x ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
have simp_rw₁ : (∃ (r : E),
    Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) r ∧
      ∃ (s : E), Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) s ∧ x = r / s) ↔
  ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
    x =
      HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
        ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
Tactic: simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
ι : Type u_3
i : ι → E
x : E
simp_rw :
  (∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (Algebra.adjoin F (Set.range i)) s ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
simp_rw₁ :
  (∃ (r : E),
      Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) r ∧
        ∃ (s : E), Membership.mem (γ := Subalgebra F E) (AlgHom.range (MvPolynomial.aeval i)) s ∧ x = r / s) ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
⊢ Membership.mem (γ := IntermediateField F E) (adjoin F (Set.range i)) x ↔
    ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
      x =
        HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
          ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
have simp_rw₂ : (∃ (r : E),
    (∃ (x : MvPolynomial ι F), (MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) x = r) ∧
      ∃ (s : E), (∃ (x : MvPolynomial ι F), (MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) x = s) ∧ x = r / s) ↔
  ∃ (r : MvPolynomial ι F) (s : MvPolynomial ι F),
    x =
      HDiv.hDiv (α := E) (β := E) ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) r : E)
        ((MvPolynomial.aeval i : (a : MvPolynomial ι F) → E) s : E)
Tactic: simp_rw [mem_adjoin_iff_div, Algebra.adjoin_range_eq_range_aeval,
    AlgHom.mem_range, exists_exists_eq_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
⊢ FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)
have h : FiniteDimensional.{u_3, u_4} K
  ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) g.range : Submodule K L)
Tactic: have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
this : g.range = (E1 ⊔ E2).toSubalgebra
h :
  FiniteDimensional.{u_3, u_4} K
    ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) g.range : Submodule K L)
⊢ FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)
have rwa : ∀
  (h :
    FiniteDimensional.{u_3, u_4} K
      ↥((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (E1 ⊔ E2).toSubalgebra : Submodule K L)),
  FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)
Tactic: rwa [this] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
⊢ FiniteDimensional.{u_3, u_4} K ↥(E1 ⊔ E2)
have suffices : g.range = (E1 ⊔ E2).toSubalgebra
Tactic: suffices g.range = (E1 ⊔ E2).toSubalgebra by
    have h : FiniteDimensional K (Subalgebra.toSubmodule g.range) :=
      g.toLinearMap.finiteDimensional_range
    rwa [this] at h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
⊢ g.range = (E1 ⊔ E2).toSubalgebra
have rw : E1.val.range ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
Tactic: rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
rw : E1.val.range ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
⊢ g.range = (E1 ⊔ E2).toSubalgebra
have rw₁ : E1.toSubalgebra ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
Tactic: rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
rw : E1.val.range ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
rw₁ : E1.toSubalgebra ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
⊢ g.range = (E1 ⊔ E2).toSubalgebra
have rw₂ : E1.toSubalgebra ⊔ E2.toSubalgebra = (E1 ⊔ E2).toSubalgebra
Tactic: rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
inst_6 : FiniteDimensional.{u_3, u_4} K ↥E1
inst_7 : FiniteDimensional.{u_3, u_4} K ↥E2
g : TensorProduct K ↥E1 ↥E2 →ₐ[K] L := Algebra.TensorProduct.productMap E1.val E2.val
rw : E1.val.range ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
rw₁ : E1.toSubalgebra ⊔ E2.val.range = (E1 ⊔ E2).toSubalgebra
rw₂ : E1.toSubalgebra ⊔ E2.toSubalgebra = (E1 ⊔ E2).toSubalgebra
⊢ g.range = (E1 ⊔ E2).toSubalgebra
have rw₃ : E1.toSubalgebra ⊔ E2.toSubalgebra = E1.toSubalgebra ⊔ E2.toSubalgebra
Tactic: rw [Algebra.TensorProduct.productMap_range, E1.range_val, E2.range_val, sup_toSubalgebra_of_left]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2
have this : Module.rank K ↥(E1.toSubalgebra ⊔ E2.toSubalgebra) ≤ Module.rank K ↥E1.toSubalgebra * Module.rank K ↥E2.toSubalgebra
Tactic: have := E1.toSubalgebra.rank_sup_le_of_free E2.toSubalgebra
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ Module.rank K ↥(E1 ⊔ E2) ≤ Module.rank K ↥E1 * Module.rank K ↥E2
have 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
Tactic: rwa [← sup_toSubalgebra_of_isAlgebraic E1 E2 halg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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
Tactic: by_cases h : FiniteDimensional K E1
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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
Tactic: by_cases h : FiniteDimensional K E1
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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
Tactic: have := E1.toSubalgebra.finrank_sup_le_of_free E2.toSubalgebra
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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
Tactic: change _ ≤ finrank K E1 * finrank K E2 at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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
Tactic: rwa [← sup_toSubalgebra_of_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have h₁ : Cardinal.aleph0 ≤ Module.rank K ↥E1
Tactic: rw [FiniteDimensional, ← rank_lt_aleph0_iff, not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have 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)
Tactic: have := LinearMap.rank_le_of_injective _ <| Submodule.inclusion_injective <|
    show Subalgebra.toSubmodule E1.toSubalgebra ≤ Subalgebra.toSubmodule (E1 ⊔ E2).toSubalgebra by
      simp
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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)
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have neg : finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ 0 * 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have neg₁ : 0 ≤ 0 * 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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ finrank.{u_3, u_4} K ↥(E1 ⊔ E2) ≤ finrank.{u_3, u_4} K ↥E1 * finrank.{u_3, u_4} K ↥E2
have neg₂ : LE.le (α := ℕ) 0 0
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]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
have inl : IsEmpty ι → (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
have inr : Nonempty ι → (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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 ι
⊢ (iSup t).toSubalgebra = ⨆ (i : ι), (t i).toSubalgebra
have inl : Eq.{u_4 + 1} (α := Subalgebra K L) (toSubalgebra ⊥) ⊥
Tactic: simp_rw [iSup_of_empty, bot_toSubalgebra]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ (i : ι), t i)
have rw : FiniteDimensional.{u_3, u_4} K ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), t x)
Tactic: rw [← iSup_univ]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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 ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), t x)
have empty : FiniteDimensional.{u_3, u_4} K ↥⊥
Tactic: rw [iSup_emptyset]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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 ↥(⨆ x ∈ insert a s_1, t x)
have insert : FiniteDimensional.{u_3, u_4} K ↥(t a ⊔ ⨆ x ∈ s_1, t x)
Tactic: rw [iSup_insert]
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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)
⊢ FiniteDimensional.{u_3, u_4} K ↥(⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), t x)
have induction : ∀ (x : Set ι), x.Finite → FiniteDimensional.{u_3, u_4} K ↥(⨆ x_2 ∈ x, t x_2)
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 _ _
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (hypothesis)
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
⊢ IsSplittingField.{u_3, u_4} K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
have hF : ∀ 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)
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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
⊢ IsSplittingField.{u_3, u_4} K (↥(⨆ i ∈ s, t i)) (∏ i ∈ s, p i)
have 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))
Tactic: simp only [isSplittingField_iff, Polynomial.map_prod] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IntermediateField.Adjoin.Basic (goal)
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)
⊢ 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))
have refine : 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, ?_⟩