awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.degree < (HSub.hSub (α := A[X]) (β := A[X]) X ((C : (a : A) → A[X]) a : A[X])).degree
h0 : ¬q = 0
⊢ Ne.{u_2 + 1} (α := B) (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B)
    (0 : B)
have hl₁ : q.natDegree = 0
Tactic: rw [← natDegree_lt_natDegree_iff h0, natDegree_X_sub_C, Nat.lt_one_iff] at hl
Cleared hypotheses: hl, h0
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬q = 0
⊢ Ne.{u_2 + 1} (α := B) (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B) q : B)
    (0 : B)
have refine_2 : ∀ (h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])),
  Ne.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
      B)
    (0 : B)
Tactic: rw [eq_C_of_natDegree_eq_zero hl] at h0 ⊢
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
⊢ Ne.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
      B)
    (0 : B)
have refine_2 : Ne.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) (q.coeff 0) : B) (0 : B)
Tactic: rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
refine_2 : Ne.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) (q.coeff 0) : B) (0 : B)
⊢ Ne.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
      B)
    (0 : B)
have refine_2₁ : q.coeff 0 ≠ 0
Tactic: rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
a : A
hf : Injective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
h : Nontrivial A
q : A[X]
hl : q.natDegree = 0
h0 : ¬Eq (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
refine_2 : Ne.{u_2 + 1} (α := B) ((algebraMap A B : (a : A) → B) (q.coeff 0) : B) (0 : B)
refine_2₁ : q.coeff 0 ≠ 0
⊢ Ne.{u_2 + 1} (α := B)
    (((Polynomial.aeval ((algebraMap A B : (a : A) → B) a) : A[X] →ₐ[A] B) : (a : A[X]) → B)
        ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) :
      B)
    (0 : B)
have refine_2₂ : Ne (α := A[X]) ((C : (a : A) → A[X]) (q.coeff 0) : A[X]) (0 : A[X])
Tactic: rwa [aeval_C, map_ne_zero_iff _ hf, ← C_ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
⊢ Ne.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
have refine : ∀ (ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)),
  a.natDegree < natDegree (minpoly A x)
Tactic: refine fun ha => (min A x hamonic ha).not_gt (degree_lt_degree ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
hdvd : DvdNotUnit a (minpoly A x)
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
⊢ a.natDegree < natDegree (minpoly A x)
have obtain : a ≠ 0 → ∀ (c : A[X]) (hu : ¬IsUnit c) (he : minpoly A x = a * c), a.natDegree < natDegree (minpoly A x)
Tactic: obtain ⟨_, c, hu, he⟩ := hdvd
Cleared hypotheses: hdvd
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
⊢ a.natDegree < natDegree (minpoly A x)
have hcm : c.Monic
Tactic: have hcm := hamonic.of_mul_monic_left (he.subst <| monic hx)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < natDegree (minpoly A x)
have rw : a.natDegree < a.natDegree + c.natDegree
Tactic: rw [he, hamonic.natDegree_mul hcm]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ a.natDegree < a.natDegree + c.natDegree
have h : 0 < c.natDegree
Tactic: apply lt_add_of_pos_right
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
⊢ 0 < c.natDegree
have h : ∀ (h : c.natDegree ≤ 0), IsUnit c
Tactic: refine (lt_of_not_ge fun h => hu ?_)
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
a : A[X]
hx : IsIntegral A x
hamonic : a.Monic
ha : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) a : B) (0 : B)
left : a ≠ 0
c : A[X]
hu : ¬IsUnit c
he : minpoly A x = a * c
hcm : c.Monic
h : c.natDegree ≤ 0
⊢ IsUnit c
have h₁ : IsUnit.{u_1} (M := A[X]) 1
Tactic: rw [eq_C_of_natDegree_le_zero h, ← Nat.eq_zero_of_le_zero h, ← leadingCoeff, hcm.leadingCoeff,
    C_1]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
⊢ Irreducible (M := A[X]) (minpoly A x)
have refine : ∀ (f g : A[X]) (hf : f.Monic) (hg : g.Monic) (he : f * g = minpoly A x), f = 1 ∨ g = 1
Tactic: refine (irreducible_of_monic (monic hx) <| ne_one A x).2 fun f g hf hg he => ?_
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ f = 1 ∨ g = 1
have rw : IsUnit f ∨ IsUnit g
Tactic: rw [← hf.isUnit_iff, ← hg.isUnit_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
⊢ IsUnit f ∨ IsUnit g
have by_contra! : ∀ (h : ¬IsUnit f ∧ ¬IsUnit g), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
⊢ False
have heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (f * g) : B)
  ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
Tactic: have heval := congr_arg (Polynomial.aeval x) he
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) (f * g) : B)
    ((Polynomial.aeval x : (a : A[X]) → B) (minpoly A x) : B)
⊢ False
have heval₁ : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B) ∨
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
Tactic: rw [aeval A x, aeval_mul, mul_eq_zero] at heval
Cleared hypotheses: heval
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
⊢ False
have inl : ∀ (heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)), False
Tactic: rcases heval with heval | heval
Cleared hypotheses: heval
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval :
  Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B) ∨
    Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
inl : ∀ (heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) f : B) (0 : B)), False
⊢ False
have inr : ∀ (heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)), False
Tactic: rcases heval with heval | heval
Cleared hypotheses: heval
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
⊢ False
have inr : minpoly A x = g * f
Tactic: refine aeval_ne_zero_of_dvdNotUnit_minpoly hx hg ⟨hg.ne_zero, f, h.1, ?_⟩ heval
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
⊢ minpoly A x = g * f
have inr : minpoly A x = f * g
Tactic: rw [mul_comm, he]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : Ring B
inst_2 : Algebra A B
x : B
inst_3 : IsDomain A
inst_4 : IsDomain B
hx : IsIntegral A x
f g : A[X]
hf : f.Monic
hg : g.Monic
he : f * g = minpoly A x
h : ¬IsUnit f ∧ ¬IsUnit g
heval : Eq.{u_2 + 1} (α := B) ((Polynomial.aeval x : (a : A[X]) → B) g : B) (0 : B)
inr : minpoly A x = f * g
⊢ minpoly A x = g * f
have inr₁ : Eq (α := A[X]) (minpoly A x) (minpoly A x)
Tactic: rw [mul_comm, he]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ Eq (α := ConjRootClass K L) (mk K x) 0 ↔ x = 0
have rw : Eq (α := ConjRootClass K L) 0 (mk K x) ↔ x = 0
Tactic: rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
rw : Eq (α := ConjRootClass K L) 0 (mk K x) ↔ x = 0
⊢ Eq (α := ConjRootClass K L) (mk K x) 0 ↔ x = 0
have rw₁ : Eq (α := ConjRootClass K L) (mk K 0) (mk K x) ↔ x = 0
Tactic: rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
rw : Eq (α := ConjRootClass K L) 0 (mk K x) ↔ x = 0
rw₁ : Eq (α := ConjRootClass K L) (mk K 0) (mk K x) ↔ x = 0
⊢ Eq (α := ConjRootClass K L) (mk K x) 0 ↔ x = 0
have rw₂ : IsConjRoot K 0 x ↔ x = 0
Tactic: rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
rw : Eq (α := ConjRootClass K L) 0 (mk K x) ↔ x = 0
rw₁ : Eq (α := ConjRootClass K L) (mk K 0) (mk K x) ↔ x = 0
rw₂ : IsConjRoot K 0 x ↔ x = 0
⊢ Eq (α := ConjRootClass K L) (mk K x) 0 ↔ x = 0
have rw₃ : x = 0 ↔ x = 0
Tactic: rw [eq_comm (b := 0), ← mk_zero, mk_eq_mk, isConjRoot_zero_iff_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
⊢ Eq (α := Set L) (carrier.{u_1, u_2} (K := K) 0) {0}
have h : ∀ (x : L), Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
⊢ Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x
have h : Eq (α := ConjRootClass K L) (mk K x) 0 ↔ Membership.mem (γ := Set L) {0} x
Tactic: rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : Eq (α := ConjRootClass K L) (mk K x) 0 ↔ Membership.mem (γ := Set L) {0} x
⊢ Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x
have h₁ : x = 0 ↔ Membership.mem (γ := Set L) {0} x
Tactic: rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x : L
h : Eq (α := ConjRootClass K L) (mk K x) 0 ↔ Membership.mem (γ := Set L) {0} x
h₁ : x = 0 ↔ Membership.mem (γ := Set L) {0} x
⊢ Membership.mem (γ := Set L) (carrier.{u_1, u_2} (K := K) 0) x ↔ Membership.mem (γ := Set L) {0} x
have h₂ : x = 0 ↔ x = 0
Tactic: rw [mem_carrier, mk_eq_zero_iff, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : ConjRootClass K L
H : x.carrier = y.carrier
⊢ x = y
have h : ∀ (x : L) (H : carrier (mk K x) = y.carrier), mk K x = y
Tactic: induction x with | h x => ?_
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : ConjRootClass K L
x : L
H : carrier (mk K x) = y.carrier
⊢ mk K x = y
have h : ∀ (y : L) (H : carrier (mk K x) = carrier (mk K y)), Eq (α := ConjRootClass K L) (mk K x) (mk K y)
Tactic: induction y with | h y => ?_
Cleared hypotheses: y, H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
H : carrier (mk K x) = carrier (mk K y)
⊢ Eq (α := ConjRootClass K L) (mk K x) (mk K y)
have H₁ : ∀ (x_1 : L), Eq (α := ConjRootClass K L) (mk K x_1) (mk K x) ↔ Eq (α := ConjRootClass K L) (mk K x_1) (mk K y)
Tactic: simp_rw [Set.ext_iff, mem_carrier] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : L
H : ∀ (x_1 : L), Eq (α := ConjRootClass K L) (mk K x_1) (mk K x) ↔ Eq (α := ConjRootClass K L) (mk K x_1) (mk K y)
⊢ Eq (α := ConjRootClass K L) (mk K x) (mk K y)
have h : Eq (α := ConjRootClass K L) (mk K x) (mk K x)
Tactic: rw [← H]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
c : ConjRootClass K L
⊢ - -c = c
have h : ∀ (x : L), Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
x : L
⊢ Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)
have h : Eq (α := ConjRootClass K L) (-mk K (-x)) (mk K x)
Tactic: rw [mk_neg, mk_neg, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
x : L
h : Eq (α := ConjRootClass K L) (-mk K (-x)) (mk K x)
⊢ Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)
have h₁ : Eq (α := ConjRootClass K L) (mk K (- -x)) (mk K x)
Tactic: rw [mk_neg, mk_neg, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
S : Type u_3
inst : Field K
inst_1 : Field L
inst_2 : Field S
inst_3 : Algebra K L
inst_4 : Algebra K S
inst_5 : Algebra L S
inst_6 : IsScalarTower K L S
x : L
h : Eq (α := ConjRootClass K L) (-mk K (-x)) (mk K x)
h₁ : Eq (α := ConjRootClass K L) (mk K (- -x)) (mk K x)
⊢ Eq (α := ConjRootClass K L) (- -mk K x) (mk K x)
have h₂ : Eq (α := ConjRootClass K L) (mk K x) (mk K x)
Tactic: rw [mk_neg, mk_neg, neg_neg]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
c : ConjRootClass K L
⊢ (-c).carrier = -c.carrier
have h : ∀ (x : L), x ∈ (-c).carrier ↔ x ∈ -c.carrier
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : ConjRootClass K L
⊢ (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) ↔ x = -y
have mp : (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) → x = -y
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
x y : ConjRootClass K L
mp : (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) → x = -y
⊢ (∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0) ↔ x = -y
have mpr : x = -y → ∃ (a : L), mk K a = x ∧ ∃ (b : L), mk K b = y ∧ a + b = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a b : L
h : a + b = 0
⊢ Eq (α := ConjRootClass K L) (mk K a) (-mk K b)
have mp : Eq (α := ConjRootClass K L) (mk K a) (mk K (-b))
Tactic: rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a b : L
h : a + b = 0
mp : Eq (α := ConjRootClass K L) (mk K a) (mk K (-b))
⊢ Eq (α := ConjRootClass K L) (mk K a) (-mk K b)
have mp₁ : IsConjRoot K a (-b)
Tactic: rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
a b : L
h : a + b = 0
mp : Eq (α := ConjRootClass K L) (mk K a) (mk K (-b))
mp₁ : IsConjRoot K a (-b)
⊢ Eq (α := ConjRootClass K L) (mk K a) (-mk K b)
have mp₂ : IsConjRoot K (-b) (-b)
Tactic: rw [mk_neg, mk_eq_mk, add_eq_zero_iff_eq_neg.mp h]
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
y : ConjRootClass K L
⊢ ∃ (a : L), mk K a = -y ∧ ∃ (b : L), mk K b = y ∧ a + b = 0
have mpr : ∀ (y : L),
  ∃ (a : L),
    Eq (α := ConjRootClass K L) (mk K a) (-mk K y) ∧
      ∃ (b : L), Eq (α := ConjRootClass K L) (mk K b) (mk K y) ∧ a + b = 0
Tactic: induction y with
    | h y => exact ⟨-y, mk_neg y, y, rfl, neg_add_cancel _⟩
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
c d : ConjRootClass K L
⊢ c.minpoly = d.minpoly ↔ c = d
have h : ∀ (x : L), ConjRootClass.minpoly (mk K x) = d.minpoly ↔ mk K x = d
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
d : ConjRootClass K L
x : L
⊢ ConjRootClass.minpoly (mk K x) = d.minpoly ↔ mk K x = d
have h : ∀ (x_1 : L),
  Eq (α := K[X]) (ConjRootClass.minpoly (mk K x)) (ConjRootClass.minpoly (mk K x_1)) ↔
    Eq (α := ConjRootClass K L) (mk K x) (mk K x_1)
Tactic: induction d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n : Normal K L
c : ConjRootClass K L
⊢ Splits (map (algebraMap K L) c.minpoly)
have h : ∀ (x : L), Splits (map (algebraMap K L) (ConjRootClass.minpoly (mk K x)))
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ c.minpoly.Monic
have h : ∀ (x : L), Monic (ConjRootClass.minpoly (mk K x))
Tactic: induction c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.FieldTheory.Minpoly.ConjRootClass (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
c : ConjRootClass K L
⊢ Irreducible c.minpoly
have h : ∀ (x : L), Irreducible (M := K[X]) (ConjRootClass.minpoly (mk K x))
Tactic: induction c
Cleared hypotheses: c