awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
key :
  Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))
refine : Normal F (p * q).SplittingField
⊢ IsSolvable.{u_1}
    (Gal
      (minpoly F (B := (p * q).SplittingField)
        ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
            (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
          (p * q).SplittingField)))

Tactic:
refine gal_isSolvable_of_splits ⟨Normal.splits ?_ (f ⟨z, hz'⟩)⟩ (gal_mul_isSolvable hx' hy')

Premises used: Normal.splits, Subtype.mk, Fact.mk, gal_mul_isSolvable, gal_isSolvable_of_splits, DFunLike.coe
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hx' : IsSolvable.{u_1} (Gal (minpoly F x))
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ z
p : F[X] := minpoly F x
q : F[X] := minpoly F y
hpq :
  Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F x)) ∧
    Splits (R := (p * q).SplittingField) (Polynomial.map (algebraMap F (p * q).SplittingField) (minpoly F y))
f : AlgHom.{u_1, u_2, u_1} F (↥F⟮x, y⟯) (p * q).SplittingField
key :
  Eq (α := F[X]) (minpoly F z)
    (minpoly F (B := (p * q).SplittingField)
      ((f : (a : ↥F⟮x, y⟯) → (p * q).SplittingField)
          (Subtype.mk (p := fun (x_1 : E) ↦ Membership.mem (γ := IntermediateField F E) F⟮x, y⟯ x_1) z hz') :
        (p * q).SplittingField))
⊢ Normal F (p * q).SplittingField

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
y : F
mem : IsSolvable.{u_1} (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).Gal
⊢ IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))

Tactic:
rw [minpoly.eq_X_sub_C E]

Premises used: minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
y : F
⊢ IsSolvable.{u_1} (HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) y : F[X])).Gal

Tactic:
infer_instance
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
apply₁ : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z
⊢ IsSolvable.{u_1} (Gal (minpoly F (y + z)))

Tactic:
apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..)

Premises used: _private.0.induction_step, AddMemClass.add_mem
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
a : Membership.mem (γ := Set E) {y, z} y
⊢ Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y

Tactic:
apply subset_adjoin

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
a : Membership.mem (γ := Set E) {y, z} z
⊢ Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z

Tactic:
apply subset_adjoin

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ Membership.mem (γ := Set E) {y, z} y

Tactic:
simp
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
⊢ Membership.mem (γ := Set E) {y, z} z

Tactic:
simp
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x y z : E
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y
hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z
hy' : IsSolvable.{u_1} (Gal (minpoly F y))
hz' : IsSolvable.{u_1} (Gal (minpoly F z))
apply : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ y
apply₁ : Membership.mem (γ := IntermediateField F E) F⟮y, z⟯ z
⊢ IsSolvable.{u_1} (Gal (minpoly F (y * z)))

Tactic:
apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..)

Premises used: _private.0.induction_step, MulMemClass.mul_mem
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
y : E
hn : n ≠ 0
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (y ^ n)
hy' : IsSolvable.{u_1} (Gal (minpoly F (y ^ n)))
⊢ IsSolvable.{u_1} (Gal (minpoly F y))

Tactic:
induction_rad (solvableByRad.rad_mem hn hy) hn hy'

Premises used: solvableByRad.rad_mem, _private.0.induction_rad
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
n : ℕ
y : E
hn : n ≠ 0
hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (y ^ n)
hy' : IsSolvable.{u_1} (Gal (minpoly F (y ^ n)))
⊢ IsSolvable.{u_1} (Gal (minpoly F y))

Tactic:
exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'

Premises used: solvableByRad.rad_mem, _private.0.induction_rad
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
mem : ∀ (y : F), IsSolvable.{u_1} (Gal (minpoly.{u_1, u_2} F (B := E) ((algebraMap F E : (a : F) → E) y : E)))
add :
  ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
    (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z)
    (hy' : IsSolvable.{u_1} (Gal (minpoly F y))) (hz' : IsSolvable.{u_1} (Gal (minpoly F z))),
    IsSolvable.{u_1} (Gal (minpoly F (y + z)))
mul :
  ∀ (y z : E) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) y)
    (hz : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) z)
    (hy' : IsSolvable.{u_1} (Gal (minpoly F y))) (hz' : IsSolvable.{u_1} (Gal (minpoly F z))),
    IsSolvable.{u_1} (Gal (minpoly F (y * z)))
rad :
  ∀ (n : ℕ) (y : E) (hn : n ≠ 0) (hy : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) (y ^ n))
    (hy' : IsSolvable.{u_1} (Gal (minpoly F (y ^ n)))), IsSolvable.{u_1} (Gal (minpoly F y))
⊢ IsSolvable.{u_1} (Gal (minpoly F x))

Tactic:
induction hx using solvableByRad.induction with
  | mem y => rw [minpoly.eq_X_sub_C E]; infer_instance
  | add y z hy hz hy' hz' =>
    apply induction_step hy hz (add_mem hy hz) hy' hz' (add_mem ..) <;> apply subset_adjoin <;> simp
  | mul y z hy hz hy' hz' =>
    apply induction_step hy hz (mul_mem hy hz) hy' hz' (mul_mem ..) <;> apply subset_adjoin <;> simp
  | rad n y hn hy hy' => exact induction_rad (solvableByRad.rad_mem hn hy) hn hy'

Premises used: IntermediateField.subset_adjoin, minpoly.eq_X_sub_C
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
rw : IsSolvable.{u_1} (Gal (minpoly F x))
⊢ IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal

Tactic:
rw [minpoly.eq_of_irreducible q_irred q_aeval]

Premises used: minpoly.eq_of_irreducible
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
⊢ IsSolvable.{u_1} (Gal (minpoly F x))

Tactic:
isSolvable_gal_minpoly hx

Premises used: isSolvable_gal_minpoly
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
⊢ IsSolvable.{u_1} (Gal (minpoly F x))

Tactic:
exact isSolvable_gal_minpoly hx

Premises used: isSolvable_gal_minpoly
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
⊢ IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal

Tactic:
have : IsSolvable (q * C q.leadingCoeff⁻¹).Gal := by
    rw [minpoly.eq_of_irreducible q_irred q_aeval]
    exact isSolvable_gal_minpoly hx
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
this : IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
⊢ IsSolvable.{u_1} q.Gal

Tactic:
solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)

Premises used: Polynomial.C, solvable_of_surjective, Polynomial.leadingCoeff, Inv.inv, Exists.intro, DFunLike.coe, Polynomial.Gal.restrictDvd_surjective, rfl
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
this : IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
refine : HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X]) ≠ 0
⊢ IsSolvable.{u_1} q.Gal

Tactic:
refine solvable_of_surjective (Gal.restrictDvd_surjective ⟨C q.leadingCoeff⁻¹, rfl⟩ ?_)

Premises used: Polynomial.C, solvable_of_surjective, Polynomial.leadingCoeff, Inv.inv, Exists.intro, DFunLike.coe, Polynomial.Gal.restrictDvd_surjective, rfl
-- Module: Mathlib.FieldTheory.AbelRuffini
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
hx : Membership.mem (γ := IntermediateField F E) (solvableByRad F E) x
q : F[X]
q_irred : Irreducible q
q_aeval : Eq.{u_2 + 1} (α := E) ((aeval x : (a : F[X]) → E) q : E) (0 : E)
this : IsSolvable.{u_1} (HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X])).Gal
⊢ HMul.hMul (β := F[X]) q ((C : (a : F) → F[X]) q.leadingCoeff⁻¹ : F[X]) ≠ 0

Tactic:
aesop
-- Module: Mathlib.FieldTheory.AbsoluteGaloisGroup
Goal:
K : Type u_1
inst : Field K
⊢ Subgroup.Normal.{u_1} (G := G_K K) (Subgroup.topologicalClosure (commutator (G_K K)))

Tactic:
Subgroup.is_normal_topologicalClosure (commutator (G_K K))

Premises used: Field.absoluteGaloisGroup, commutator, Subgroup.is_normal_topologicalClosure
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
⊢ Eq (α := Subalgebra F E) (toSubalgebra (algebraicClosure F E)) (integralClosure F E)

Tactic:
rfl

Premises used: integralClosure, rfl
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x ↔ IsIntegral F x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, RingHom.IsIntegralElem, IsIntegral
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
x : E
⊢ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x ↔ IsAlgebraic F x

Tactic:
isAlgebraic_iff_isIntegral.symm

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, isAlgebraic_iff_isIntegral, Iff.symm
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
simp_rw : IsIntegral.{u_1, u_3} F (A := K) ((i : (a : E) → K) x : K) ↔ IsIntegral F x
simp_rw₁ : Ne (α := F[X]) (minpoly.{u_1, u_3} F (B := K) ((i : (a : E) → K) x : K)) 0 ↔ Ne (α := F[X]) (minpoly F x) 0
⊢ Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((i : (a : E) → K) x : K) ↔
    Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x

Tactic:
simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]

Premises used: minpoly.ne_zero_iff, minpoly.algHom_eq, RingHom.injective, AlgHom.toRingHom, mem_algebraicClosure_iff'
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
h : ∀ (x : E), x ∈ comap i (algebraicClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x
⊢ comap i (algebraicClosure F K) = algebraicClosure F E

Tactic:
ext x
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (algebraicClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x

Tactic:
map_mem_algebraicClosure_iff i

Premises used: Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, Set.preimage, map_mem_algebraicClosure_iff
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (algebraicClosure F K) ↔ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x

Tactic:
exact map_mem_algebraicClosure_iff i

Premises used: map_mem_algebraicClosure_iff
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E →ₐ[F] K
⊢ IntermediateField.map i (algebraicClosure F E) ≤ algebraicClosure F K

Tactic:
map_le_iff_le_comap.2 (comap_eq_of_algHom i).ge

Premises used: Iff.mpr, IntermediateField.map_le_iff_le_comap, Eq.ge, algebraicClosure.comap_eq_of_algHom
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E))
    (algebraicClosure F K)

Tactic:
le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Premises used: algebraicClosure.map_le_of_algHom, le_antisymm
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
refine :
  ∀ (x : K) (hx : Membership.mem (γ := IntermediateField F K) (algebraicClosure F K) x),
    Membership.mem (γ := IntermediateField F K)
      (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) x
⊢ Eq (α := IntermediateField F K) (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E))
    (algebraicClosure F K)

Tactic:
refine le_antisymm (map_le_of_algHom _) (fun x hx ↦ ?_)

Premises used: algebraicClosure.map_le_of_algHom, le_antisymm
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
x : K
hx : Membership.mem (γ := IntermediateField F K) (algebraicClosure F K) x
obtain :
  ∀ (y : E)
    (hx :
      Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K)
        ((algebraMap E K : (a : E) → K) y : K)),
    Membership.mem (α := K) (γ := IntermediateField F K)
      (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E))
      ((algebraMap E K : (a : E) → K) y : K)
⊢ Membership.mem (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) x

Tactic:
obtain ⟨y, rfl⟩ := mem_bot.1 <| h ▸ mem_algebraicClosure_iff'.2
    (IsIntegral.tower_top <| mem_algebraicClosure_iff'.1 hx)

Premises used: Iff.mp, IntermediateField.mem_bot, rfl
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
y : E
hx : Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((algebraMap E K : (a : E) → K) y : K)
⊢ Membership.mem (α := K) (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) ((algebraMap E K : (a : E) → K) y : K)

Tactic:
⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩

Premises used: Set.Mem, setOf, IsScalarTower.toAlgHom, And.intro, map_mem_algebraicClosure_iff, Exists.intro, Iff.mp, Set.image, rfl
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
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
h : Eq (α := IntermediateField E K) (algebraicClosure E K) ⊥
y : E
hx : Membership.mem (α := K) (γ := IntermediateField F K) (algebraicClosure F K) ((algebraMap E K : (a : E) → K) y : K)
⊢ Membership.mem (α := K) (γ := IntermediateField F K)
    (IntermediateField.map (IsScalarTower.toAlgHom F E K) (algebraicClosure F E)) ((algebraMap E K : (a : E) → K) y : K)

Tactic:
exact ⟨y, (map_mem_algebraicClosure_iff <| IsScalarTower.toAlgHom F E K).mp hx, rfl⟩
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
i : E ≃ₐ[F] K
x : K
h : Membership.mem (γ := IntermediateField F K) (algebraicClosure F K) x
⊢ ((↑(↑i : E →ₐ[F] K) : E →+* K) : (a : E) → K) (((↑i.symm : K →ₐ[F] E) : (a : K) → E) x : E) = x

Tactic:
simp
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
⊢ Algebra.IsAlgebraic.{u_1, u_2} F ↥(algebraicClosure F E)

Tactic:
⟨fun x ↦ isAlgebraic_iff.mpr x.2.isAlgebraic⟩

Premises used: Iff.mpr, IntermediateField.isAlgebraic_iff, IsIntegral.isAlgebraic, Algebra.IsAlgebraic.mk, Subtype.property
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
K : Type u_3
inst_3 : Field K
inst_4 : Algebra F K
⊢ IsIntegralClosure (↥(algebraicClosure F E)) F E

Tactic:
inferInstanceAs (IsIntegralClosure (integralClosure F E) F E)

Premises used: _private.0.algebraicClosure.isIntegralClosure._proof_1
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
a : E
ha : Transcendental F a
⊢ Transcendental (↥(algebraicClosure F E)) a

Tactic:
ha.extendScalars _

Premises used: Transcendental.extendScalars
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
hs : ∀ (x : ↥L), IsAlgebraic F x
x : E
h : x ∈ L
⊢ Membership.mem (γ := IntermediateField F E) (algebraicClosure F E) x

Tactic:
simpa only [mem_algebraicClosure_iff, IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
    Algebra.algebraMap_self, RingHom.id_apply, IntermediateField.algebraMap_apply] using hs ⟨x, h⟩

Premises used: Polynomial.aeval_algebraMap_eq_zero_iff, RingHom.id_apply, IsAlgebraic, Algebra.algebraMap_self, mem_algebraicClosure_iff, ne_eq, IntermediateField.algebraMap_apply, Subtype.mk
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
inst_3 : Algebra.IsAlgebraic.{u_1, u_2} F ↥L
⊢ L ≤ algebraicClosure F E

Tactic:
le_algebraicClosure' F E (Algebra.IsAlgebraic.isAlgebraic)

Premises used: Algebra.IsAlgebraic.isAlgebraic, le_algebraicClosure'
-- Module: Mathlib.FieldTheory.AlgebraicClosure
Goal:
F : Type u_1
E : Type u_2
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : IntermediateField F E
h : L ≤ algebraicClosure F E
x : ↥L
⊢ IsAlgebraic F x

Tactic:
simpa only [IsAlgebraic, ne_eq, ← aeval_algebraMap_eq_zero_iff E,
    IntermediateField.algebraMap_apply,
    Algebra.algebraMap_self, RingHomCompTriple.comp_apply, mem_algebraicClosure_iff] using h x.2

Premises used: Polynomial.aeval_algebraMap_eq_zero_iff, IsAlgebraic, Algebra.algebraMap_self, mem_algebraicClosure_iff, ne_eq, IntermediateField.algebraMap_apply, RingHomCompTriple.comp_apply, Subtype.property