awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) p : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) q : K) (0 : K)
⊢ ¬(p = 0 ∧ q = 0)
have h₁ : Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∨
  Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
Tactic: replace h := h 0
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h :
  Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∨
    Ne.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
⊢ ¬(p = 0 ∧ q = 0)
have refine_1 : ∀ (h : p = 0 ∧ q = 0),
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
⊢ Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
have refine_1 : Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
⊢ Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
have refine_1₁ : Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K)
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K)
⊢ Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
have refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
p q : k[X]
h : p = 0 ∧ q = 0
refine_1 :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
refine_1₁ :
  Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) 0 : K) (0 : K)
refine_1₂ : Eq.{v + 1} (α := K) 0 0 ∧ Eq.{v + 1} (α := K) 0 0
⊢ Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) p : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval 0 : (a : k[X]) → K) q : K) (0 : K)
have refine_1₃ : Eq.{v + 1} (α := K) 0 0
Tactic: rw [h.left, h.right, map_zero, and_self]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
⊢ False
have refine_2 : ∀ (a : K) (ha : eval a (map (algebraMap k K) x) = 0), False
Tactic: obtain ⟨a, ha : _ = _⟩ := IsAlgClosed.exists_root (x.map <| algebraMap k K) <| by
      simpa only [degree_map] using (ne_of_lt <| degree_pos_of_ne_zero_of_nonunit h0 hu).symm
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
⊢ Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
have simp_rw : HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w : K) = 0 ∧
  HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w_1 : K) = 0
Tactic: simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
simp_rw :
  HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w : K) = 0 ∧
    HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w_1 : K) = 0
⊢ Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
have simp_rw₁ : eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w) = 0 ∧
  eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w_1) = 0
Tactic: simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
simp_rw :
  HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w : K) = 0 ∧
    HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w_1 : K) = 0
simp_rw₁ :
  eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w) = 0 ∧
    eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w_1) = 0
⊢ Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
have simp_rw₂ : 0 * eval a (map (algebraMap k K) w) = 0 ∧ 0 * eval a (map (algebraMap k K) w_1) = 0
Tactic: simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
k : Type u
inst : Field k
K : Type v
inst_1 : Field K
inst_2 : IsAlgClosed K
inst_3 : Algebra k K
x : k[X]
hu : Membership.mem (γ := Set k[X]) (nonunits k[X]) x
h0 : x ≠ 0
w w_1 : k[X]
h :
  ∀ (a : K),
    Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∨
      Ne.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
a : K
ha : eval a (map (algebraMap k K) x) = 0
simp_rw :
  HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w : K) = 0 ∧
    HMul.hMul (α := K) (β := K) ((aeval a : (a : k[X]) → K) x : K) ((aeval a : (a : k[X]) → K) w_1 : K) = 0
simp_rw₁ :
  eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w) = 0 ∧
    eval a (map (algebraMap k K) x) * eval a (map (algebraMap k K) w_1) = 0
simp_rw₂ : 0 * eval a (map (algebraMap k K) w) = 0 ∧ 0 * eval a (map (algebraMap k K) w_1) = 0
⊢ Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w) : K) (0 : K) ∧
    Eq.{v + 1} (α := K) ((aeval a : (a : k[X]) → K) (x * w_1) : K) (0 : K)
have simp_rw₃ : True ∧ True
Tactic: simp_rw [map_mul, ← eval_map_algebraMap, ha, zero_mul, true_and]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : p.natDegree ≠ 0
x : M
⊢ ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
have rw : ∀ (hp : 0 < p.degree) (x : M), ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
Tactic: rw [← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at hp
Cleared hypotheses: hp, x
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
Goal:
M : Type w
inst : Field M
inst_1 : IsAlgClosed M
p : M[X]
hp : 0 < p.degree
x : M
⊢ ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
have have : ∀ (y : M) (hy : eval y (HSub.hSub (β := M[X]) p ((C : (a : M) → M[X]) x : M[X])) = 0),
  ∃ (a : M), (fun (x : M) ↦ eval x p) a = x
Tactic: have ⟨y, hy⟩ := (IsAlgClosed.splits (p - C x)).exists_eval_eq_zero <| by
      simpa only [degree_sub_C hp] using hp.ne'
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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)
⊢ Algebra.IsAlgebraic.{u, v} (FractionRing R) (FractionRing S)
have this₁ : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
Tactic: have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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} (FractionRing R) (FractionRing S)
have this₁ : Algebra.IsAlgebraic.{u, v} R (FractionRing S)
Tactic: have := (IsFractionRing.isAlgebraic_iff' R S (FractionRing S)).1 inferInstance
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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)
⊢ S →ₐ[R] M
have this₁ : IsScalarTower R (FractionRing R) M
Tactic: have := FractionRing.isScalarTower_liftAlgebra R M
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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
⊢ S →ₐ[R] M
have this₁ : IsScalarTower.{u, u, v} R (FractionRing R) (FractionRing S)
Tactic: have := FractionRing.isScalarTower_liftAlgebra R (FractionRing S)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have have : ∀ (emb : E →ₐ[F] F'), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Tactic: have emb : E →ₐ[F] F' := lift
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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'
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have have : ∀ (e : AlgEquiv.{u_1, u_3, u_2} F E ↥emb.range), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Tactic: have e := AlgEquiv.ofInjectiveField emb
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have this : IsSimpleOrder.{u_2} (Subalgebra F F')
Tactic: have := Subalgebra.isSimpleOrder_of_finrank h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have inl : ∀ (h : emb.range = ⊥), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Tactic: obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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')
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have inr : ∀ (h : emb.range = ⊤), Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
Tactic: obtain h | h := IsSimpleOrder.eq_bot_or_eq_top emb.range
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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 = ⊥
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have 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')
Tactic: rw [h] at e
Cleared hypotheses: e, this, h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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 = ⊤
⊢ Nonempty (E ≃ₐ[F] F) ∨ Nonempty (E ≃ₐ[F] F')
have 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')
Tactic: rw [h] at e
Cleared hypotheses: e, this, h
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ PerfectField k
have inl : CharZero k → PerfectField k
Tactic: obtain _ | ⟨p, _, _⟩ := CharP.exists' k
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ PerfectField k
have inr : ∀ (p : ℕ), Fact (Nat.Prime p) → CharP k p → PerfectField k
Tactic: obtain _ | ⟨p, _, _⟩ := CharP.exists' k
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ Infinite K
have h : ∀ (a : Fintype K), False
Tactic: apply Infinite.of_not_fintype
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (hypothesis)
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
⊢ False
have hfsep : f.Separable
Tactic: have hfsep : Separable f := separable_X_pow_sub_C 1 (by simp [n]) one_ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ False
have h : (Fintype.card K).succ ≤ Fintype.card K
Tactic: apply Nat.not_succ_le_self (Fintype.card K)
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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)
have rw : n.succ = f.natDegree
Tactic: rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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 = (HPow.hPow (α := K[X]) X (n + 1) - 1).natDegree
have rw : n.succ = (HPow.hPow (α := K[X]) X (n + 1) - (C : (a : K) → K[X]) 1).natDegree
Tactic: rw [← C_1, natDegree_X_pow_sub_C]
-- Lean 4 proof step from Mathlib.FieldTheory.IsAlgClosed.Basic (goal)
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
⊢ n.succ = (HPow.hPow (α := K[X]) X (n + 1) - 1).natDegree
have rw₁ : n.succ = n + 1
Tactic: rw [← C_1, natDegree_X_pow_sub_C]