awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
pos : ∀ (hx : x = 0), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
have neg : ∀ (hx : ¬x = 0), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : x = 0
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
have pos : Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : ¬x = 0
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
have neg : ∀ (n : ℤ) (hn : α ^ n = Units.mk0 x hx), Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
Tactic: obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = (↑α : E) ^ n
have norm_cast : x = (↑(α ^ n) : E)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = (↑(α ^ n) : E)
have rw : x = (↑(Units.mk0 x hx : Eˣ) : E)
Tactic: rw [hn, Units.val_mk0]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
rw : x = (↑(Units.mk0 x hx : Eˣ) : E)
⊢ x = (↑(α ^ n) : E)
have rw₁ : x = x
Tactic: rw [hn, Units.val_mk0]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
E : Type u_2
inst_1 : Field E
inst_2 : Algebra F E
inst_3 : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), Membership.mem (γ := Subgroup Eˣ) (Subgroup.zpowers α) x
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ x
have neg : Membership.mem (γ := IntermediateField F E) F⟮(↑α : E)⟯ ((↑α : E) ^ n)
Tactic: rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have obtain : ∀ (c : F) (hc : c ∉ s'),
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
Tactic: obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : c ∉ s'
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have hc₁ : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c
Tactic: simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg)
s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯
c : F
hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have hc₁ : ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c
Tactic: push Not at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
let let₁ let₂ let₃ :
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have let₄ : let s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg);
let s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) sorry;
∀ (c : F) (hc : c ∉ s'),
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
Tactic: classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
let let₁ let₂ let₃ :
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₄ :
  let s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg);
  let s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯;
  ∀ (c : F) (hc : c ∉ s'),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have let₅ : ∀ (c : F) (hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c),
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
Tactic: classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
let let₁ let₂ let₃ :
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₄ :
  let s : Finset E := Multiset.toFinset (sf.bind fun (α' : E) ↦ Multiset.map (fun (β' : E) ↦ -(α' - α) / (β' - β)) sg);
  let s' : Finset F := s.preimage (⇑ϕ : (a : F) → E) ⋯;
  ∀ (c : F) (hc : c ∉ s'),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
let₅ :
  ∀ (c : F) (hc : ¬∃ a ∈ sf, ∃ a_1 ∈ sg, -(a - α) / (a_1 - β) = (ϕ : (a : F) → E) c),
    ∃ (c : F),
      ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
⊢ ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
have let₆ : ∀ (c : F) (hc : ∀ (a : E) (_ : a ∈ sf) (a_1 : E) (_ : a_1 ∈ sg), -(a - α) / (a_1 - β) ≠ (ϕ : (a : F) → E) c),
  ∃ (c : F),
    ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ (ϕ : (a : F) → E) c
Tactic: classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push Not at hc
  exact ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have hα : IsIntegral F α
Tactic: have hα := Algebra.IsSeparable.isIntegral F α
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have hβ : IsIntegral F β
Tactic: have hβ := Algebra.IsSeparable.isIntegral F β
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have obtain : ∀ (c : F)
  (hc :
    ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
      ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
        -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
                ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
            HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
          (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c),
  ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
Tactic: obtain ⟨c, hc⟩ := primitive_element_inf_aux_exists_c (ιEE'.comp ιFE) (ιEE' α) (ιEE' β) f g
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ ∃ (γ : E), Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have h : Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
Tactic: use γ
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have h : LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
h : LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
⊢ Eq (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have h₁ : LE.le (α := IntermediateField F E) F⟮γ⟯ F⟮α, β⟯
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ LE.le (α := IntermediateField F E) F⟮α, β⟯ F⟮γ⟯
have h : {α, β} ⊆ (↑F⟮γ⟯ : Set E)
Tactic: rw [adjoin_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮γ⟯ α
have rw : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ (α + c • β - c • β)
Tactic: rw [← add_sub_cancel_right α (c • β)]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ {α, β} ⊆ (↑F⟮γ⟯ : Set E)
have α_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ α
Tactic: have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (goal)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ LE.le (α := IntermediateField F E) F⟮γ⟯ F⟮α, β⟯
have h : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ γ
Tactic: rw [adjoin_simple_le_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ γ
have α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
Tactic: have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
-- Lean 4 proof step from Mathlib.FieldTheory.PrimitiveElement (hypothesis)
Goal:
F : Type u_1
inst : Field F
inst_1 : Infinite F
E : Type u_2
inst_2 : Field E
α β : E
inst_3 : Algebra F E
inst_4 : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots,
      -HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) α'
              ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) α : (Polynomial.map ιFE g).SplittingField) /
          HSub.hSub (β := (Polynomial.map ιFE g).SplittingField) β'
            ((ιEE' : (a : E) → (Polynomial.map ιFE g).SplittingField) β : (Polynomial.map ιFE g).SplittingField) ≠
        (ιEE'.comp ιFE : (a : F) → (Polynomial.map ιFE g).SplittingField) c
γ : E := α + c • β
β_in_Fγ : Membership.mem (γ := IntermediateField F E) F⟮γ⟯ β
α_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ α
⊢ Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ γ
have β_in_Fαβ : Membership.mem (γ := IntermediateField F E) F⟮α, β⟯ β
Tactic: have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)