awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
K : Type u
inst : Field K
L : Type v
M : Type w
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Field M
inst_4 : Algebra K M
inst_5 : IsAlgClosed M
E : Type u_1
inst_6 : Field E
inst_7 : Algebra K E
inst_8 : Algebra L E
inst_9 : IsScalarTower K L E
inst_10 : Algebra.IsAlgebraic L E
⊢ Function.Surjective (β := L →ₐ[K] M) fun (φ : E →ₐ[K] M) ↦ AlgHom.restrictDomain L φ

Tactic:
fun f ↦ IntermediateField.exists_algHom_of_splits'
    (E := E) f fun s ↦ ⟨Algebra.IsIntegral.isIntegral s, IsAlgClosed.splits _⟩

Premises used: Algebra.IsIntegral.isIntegral, IntermediateField.exists_algHom_of_splits', minpoly, AlgHom.toRingHom, And.intro, IsAlgClosed.splits, Polynomial.map, Function.Surjective
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
⊢ IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
⊢ Algebra.IsAlgebraic.{u, v} R (FractionRing S)

Tactic:
have := (IsFractionRing.isAlgebraic_iff' R S (FractionRing S)).1 inferInstance
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this_3 : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
this : Algebra.IsAlgebraic.{u, v} R (FractionRing S)
⊢ Algebra.IsAlgebraic.{u, v} (FractionRing R) (FractionRing S)

Tactic:
⟨fun _ ↦ (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    (Algebra.IsAlgebraic.isAlgebraic _)⟩

Premises used: Algebra.IsAlgebraic.isAlgebraic, FractionRing, Algebra.IsAlgebraic.mk, Iff.mp, IsFractionRing.isAlgebraic_iff
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this_3 : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
this : Algebra.IsAlgebraic.{u, v} R (FractionRing S)
⊢ Algebra.IsAlgebraic.{u, v} (FractionRing R) (FractionRing S)

Tactic:
exact ⟨fun _ ↦ (IsFractionRing.isAlgebraic_iff R (FractionRing R) (FractionRing S)).1
    (Algebra.IsAlgebraic.isAlgebraic _)⟩
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, w} (FractionRing R) M := FractionRing.liftAlgebra R M
this : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
⊢ IsScalarTower R (FractionRing R) M

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R M
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, w} (FractionRing R) M := FractionRing.liftAlgebra R M
this_3 : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this : IsScalarTower R (FractionRing R) M
⊢ IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)

Tactic:
have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
this_1 : IsDomain R := ⋯
this_2 : Algebra.{u, w} (FractionRing R) M := FractionRing.liftAlgebra R M
this_3 : Algebra.{u, v} (FractionRing R) (FractionRing S) := FractionRing.liftAlgebra R (FractionRing S)
this_4 : IsScalarTower R (FractionRing R) M
this : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
f : AlgHom.{u, v, w} (FractionRing R) (FractionRing S) M := liftAux.{u, v, w} (FractionRing R) (FractionRing S) M
⊢ S →ₐ[R] M

Tactic:
exact (f.restrictScalars R).comp ((Algebra.ofId S (FractionRing S)).restrictScalars R)

Premises used: FractionRing, Algebra.ofId, AlgHom.restrictScalars, AlgHom.comp
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h : finrank F F' = 2
have : ∀ (emb : E →ₐ[F] F'), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
have emb : E →ₐ[F] F' := lift
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h : finrank F F' = 2
emb : E →ₐ[F] F'
have : ∀ (e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
have e := AlgEquiv.ofInjectiveField emb
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range
⊢ IsSimpleOrder.{u_2} (Subalgebra F F')

Tactic:
have := Subalgebra.isSimpleOrder_of_finrank h
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range
this : IsSimpleOrder.{u_2} (Subalgebra F F')
inl : ∀ (h : emb.range = ⊥), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
inr : ∀ (h : emb.range = ⊤), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range

Premises used: IsSimpleOrder.eq_bot_or_eq_top, AlgHom.range
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h_1 : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range
this : IsSimpleOrder.{u_2} (Subalgebra F F')
h : emb.range = ⊥
inl :
  ∀ (e : AlgEquiv.{u_1, u_3, u_2} F E ↥⊥) (this : IsSimpleOrder.{u_2} (Subalgebra F F')) (h : emb.range = ⊥),
    Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
rw [h] at e
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h_1 : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range
this : IsSimpleOrder.{u_2} (Subalgebra F F')
h : emb.range = ⊤
inr :
  ∀ (e : AlgEquiv.{u_1, u_3, u_2} F E ↥⊤) (this : IsSimpleOrder.{u_2} (Subalgebra F F')) (h : emb.range = ⊤),
    Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
rw [h] at e
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h_1 : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥⊥
this : IsSimpleOrder.{u_2} (Subalgebra F F')
h : emb.range = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
.inl ⟨e.trans <| Algebra.botEquiv ..⟩

Premises used: Nonempty.intro, AlgEquiv.trans, Algebra.botEquiv, Or.inl
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h_1 : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥⊤
this : IsSimpleOrder.{u_2} (Subalgebra F F')
h : emb.range = ⊤
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
.inr ⟨e.trans Subalgebra.topEquiv⟩

Premises used: Nonempty.intro, AlgEquiv.trans, Subalgebra.topEquiv, Or.inr
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
F : Type u_1
F' : Type u_2
E : Type u_3
inst : Field F
inst_1 : Field F'
inst_2 : Field E
inst_3 : Algebra F F'
inst_4 : Algebra F E
inst_5 : Algebra.IsAlgebraic F E
inst_6 : IsAlgClosed F'
h_1 : finrank F F' = 2
emb : E →ₐ[F] F'
e : AlgEquiv.{u_1, u_3, u_2} F E ↥⊥
this : IsSimpleOrder.{u_2} (Subalgebra F F')
h : emb.range = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')

Tactic:
exacts [.inl ⟨e.trans <| Algebra.botEquiv ..⟩, .inr ⟨e.trans Subalgebra.topEquiv⟩]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
p : ℕ
inst_17 : Fact (Nat.Prime p)
inst_18 : CharP k p
inst_19 : IsAlgClosed k
⊢ PerfectRing k p

Tactic:
PerfectRing.ofSurjective k p fun _ => IsAlgClosed.exists_pow_nat_eq _ <| NeZero.pos p

Premises used: IsAlgClosed.exists_pow_nat_eq, PerfectRing.ofSurjective, NeZero.pos
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
inst_17 : IsAlgClosed k
inl : CharZero k → PerfectField k
inr : ∀ (p : ℕ), Fact (Nat.Prime p) → CharP k p → PerfectField k
⊢ PerfectField k

Tactic:
obtain _ | ⟨p, _, _⟩ := CharP.exists' k

Premises used: CharP.exists'
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
inst_17 : IsAlgClosed k
h : CharZero k
⊢ PerfectField k

Tactic:
.ofCharZero

Premises used: PerfectField.ofCharZero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
inst_17 : IsAlgClosed k
p : ℕ
left : Fact (Nat.Prime p)
right : CharP k p
⊢ PerfectField k

Tactic:
PerfectRing.toPerfectField k p

Premises used: PerfectRing.toPerfectField
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K : Type u
inst_1 : Field K
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
inst_17 : IsAlgClosed k
h : CharZero k
⊢ PerfectField k

Tactic:
exacts [.ofCharZero, PerfectRing.toPerfectField k p]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
h : ∀ (a : Fintype K), False
⊢ Infinite K

Tactic:
apply Infinite.of_not_fintype

Premises used: Infinite.of_not_fintype
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
⊢ Ne.{u_1 + 1} (α := K) (↑(n + 1) : K) 0

Tactic:
simp [n]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
⊢ f.Separable

Tactic:
have hfsep : Separable f := separable_X_pow_sub_C 1 (by simp [n]) one_ne_zero
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
h : (Fintype.card K).succ ≤ Fintype.card K
⊢ False

Tactic:
apply Nat.not_succ_le_self (Fintype.card K)

Premises used: Fintype.card, Nat.not_succ_le_self
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
rw : n.succ = f.natDegree
⊢ n.succ = Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1)

Tactic:
rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]

Premises used: Polynomial.card_rootSet_eq_natDegree, IsAlgClosed.splits_domain
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
unfold : n.succ = (HPow.hPow (α := K[X]) X (n + 1) - 1).natDegree
⊢ n.succ = f.natDegree

Tactic:
unfold f
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
rw : n.succ = (HPow.hPow (α := K[X]) X (n + 1) - (C : (a : K) → K[X]) 1).natDegree
rw₁ rw₂ : n.succ = n + 1
⊢ n.succ = (HPow.hPow (α := K[X]) X (n + 1) - 1).natDegree

Tactic:
rw [← C_1, natDegree_X_pow_sub_C]

Premises used: Polynomial.C_1, Polynomial.natDegree_X_pow_sub_C
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
⊢ n.succ = Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1)

Tactic:
have hroot : n.succ = Fintype.card (f.rootSet K) := by
    rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]
    unfold f
    rw [← C_1, natDegree_X_pow_sub_C]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1)
h : Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1) ≤ Fintype.card K
⊢ (Fintype.card K).succ ≤ Fintype.card K

Tactic:
rw [hroot]
-- Module: Mathlib.FieldTheory.IsAlgClosed.Basic
Goal:
k : Type u
inst : Field k
K_1 : Type u
inst_1 : Field K_1
L : Type v
M : Type w
inst_2 : Field L
inst_3 : Algebra K_1 L
inst_4 : Field M
inst_5 : Algebra K_1 M
inst_6 : IsAlgClosed M
inst_7 : Algebra.IsAlgebraic K_1 L
R : Type u
inst_8 : CommRing R
inst_9 : IsDomain R
S : Type v
inst_10 : CommRing S
inst_11 : IsDomain S
inst_12 : Algebra R S
inst_13 : Algebra R M
inst_14 : IsTorsionFree R S
inst_15 : IsTorsionFree R M
inst_16 : Algebra.IsAlgebraic R S
K : Type u_1
inst_17 : Field K
inst_18 : IsAlgClosed K
hfin : Fintype K
n : ℕ := Fintype.card K
f : K[X] := HPow.hPow (α := K[X]) X (n + 1) - 1
hfsep : f.Separable
hroot : n.succ = Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1)
⊢ Fintype.card.{u_1} (↑(f.rootSet K) : Type u_1) ≤ Fintype.card K

Tactic:
Fintype.card_le_of_injective _ Subtype.coe_injective

Premises used: Fintype.card_le_of_injective, Subtype.coe_injective