awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
rw :
  Eq (α := AdjoinRoot f)
    (((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f)
    (0 : AdjoinRoot f)
rw₁ :
  Eq (α := AdjoinRoot f)
    ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval : (a : AdjoinRoot q) → AdjoinRoot f)
        ((mk q : (a : K[X]) → AdjoinRoot q) q) :
      AdjoinRoot f)
    (0 : AdjoinRoot f)
rw₂ :
  Eq (α := AdjoinRoot f) ((lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval : (a : AdjoinRoot q) → AdjoinRoot f) 0) 0
⊢ Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
have rw₃ : Eq.{u_5 + 1} (α := AdjoinRoot f) 0 0
Tactic: rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ f ∣ q
have this : Eq (α := AdjoinRoot f) ((mk f : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
Tactic: have : mk f q = 0 := by rw [← commutes, RingHom.comp_apply, mk_self, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have refine_2 : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have refine_2₁ : ¬f.leadingCoeff⁻¹ = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
refine_2₁ : ¬f.leadingCoeff⁻¹ = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have refine_2₂ : ¬f.leadingCoeff = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
f'_monic : (HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])).Monic
q : K[X]
q_monic : q.Monic
q_aeval : Eq (α := AdjoinRoot f) ((aeval (root f) : (a : K[X]) → AdjoinRoot f) q : AdjoinRoot f) (0 : AdjoinRoot f)
commutes : (lift (algebraMap K (AdjoinRoot f)) (root f) q_aeval).comp (mk q) = mk f
refine_2 : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
refine_2₁ : ¬f.leadingCoeff⁻¹ = 0
refine_2₂ : ¬f.leadingCoeff = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have refine_2₃ : ¬f = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ f'.natDegree = f.natDegree
have rw : Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
Tactic: rw [natDegree_mul hf, natDegree_C, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have rwa : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rwa : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have rwa₁ : ¬f.leadingCoeff⁻¹ = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rwa : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
rwa₁ : ¬f.leadingCoeff⁻¹ = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have rwa₂ : ¬f.leadingCoeff = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
rwa : ¬Eq (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
rwa₁ : ¬f.leadingCoeff⁻¹ = 0
rwa₂ : ¬f.leadingCoeff = 0
⊢ Ne (α := K[X]) ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) (0 : K[X])
have rwa₃ : ¬f = 0
Tactic: rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)
have deg_f' : f'.natDegree = f.natDegree
Tactic: have deg_f' : f'.natDegree = f.natDegree := by
    rw [natDegree_mul hf, natDegree_C, add_zero]
    · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)
have minpoly_eq : minpoly K (root f) = f'
Tactic: have minpoly_eq : minpoly K (root f) = f' := minpoly_root hf
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)
have hli : LinearIndependent K (M := AdjoinRoot f) fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)
Tactic: apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
hli : LinearIndependent K (M := AdjoinRoot f) fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)
⊢ Basis (Fin f.natDegree) K (AdjoinRoot f)
have hsp : LE.le (α := Submodule K (AdjoinRoot f)) ⊤ (Submodule.span K (Set.range fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)))
Tactic: apply Basis.mk (v := fun i : Fin f.natDegree ↦ root f ^ i.val)
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
⊢ LinearIndependent K (M := AdjoinRoot f) fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ)
have hli : LinearIndependent K (M := AdjoinRoot f) fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ)
Tactic: rw [← deg_f', ← minpoly_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ Membership.mem (γ := Submodule K (AdjoinRoot f))
    (Submodule.span K (Set.range fun (i : Fin f.natDegree) ↦ root f ^ (↑i : ℕ))) y
have hsp : Membership.mem (γ := Submodule K (AdjoinRoot f))
  (Submodule.span K (Set.range fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ))) y
Tactic: rw [← deg_f', ← minpoly_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ Membership.mem (γ := Submodule K (AdjoinRoot f))
    (Submodule.span K (Set.range fun (i : Fin (natDegree (minpoly K (root f)))) ↦ root f ^ (↑i : ℕ))) y
have hsp : ∃ (f_1 : K[X]), y = (aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1
Tactic: apply (isIntegral_root hf).mem_span_pow
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
⊢ ∃ (f_1 : K[X]), y = (aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1
have hsp : ∀ (g : K[X]),
  ∃ (f_1 : K[X]),
    Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1)
Tactic: obtain ⟨g⟩ := y
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g_1 : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ ∃ (f_1 : K[X]),
    Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
      ((aeval (root f) : (a : K[X]) → AdjoinRoot f) f_1)
have h : Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
  ((aeval (root f) : (a : K[X]) → AdjoinRoot f) g)
Tactic: use g
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
g_1 : R[X]
inst_1 : Field K
f : K[X]
hf : f ≠ 0
f' : K[X] := HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
deg_f' : f'.natDegree = f.natDegree
minpoly_eq : minpoly K (root f) = f'
y : AdjoinRoot f
g : K[X]
⊢ Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
    ((aeval (root f) : (a : K[X]) → AdjoinRoot f) g)
have h : Eq (α := AdjoinRoot f) (Quot.mk (⇑(Submodule.quotientRel (span {f})) : K[X] → K[X] → Prop) g)
  ((mk f : (a : K[X]) → AdjoinRoot f) g)
Tactic: rw [aeval_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
⊢ minpoly K (powerBasis hf).gen = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
have rw : minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
Tactic: rw [powerBasis_gen, minpoly_root hf]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f ≠ 0
rw : minpoly K (root f) = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
⊢ minpoly K (powerBasis hf).gen = HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
have rw₁ : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) =
  HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X])
Tactic: rw [powerBasis_gen, minpoly_root hf]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
⊢ minpoly K (powerBasis hf').gen = f
have rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
Tactic: rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
⊢ minpoly K (powerBasis hf').gen = f
have rw₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
Tactic: rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
rw₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
⊢ minpoly K (powerBasis hf').gen = f
have rw₂ : f * (C : (a : K) → K[X]) 1 = f
Tactic: rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
rw₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
rw₂ : f * (C : (a : K) → K[X]) 1 = f
⊢ minpoly K (powerBasis hf').gen = f
have rw₃ : f * 1 = f
Tactic: rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f.Monic
hf' : f ≠ 0
rw : HMul.hMul (β := K[X]) f ((C : (a : K) → K[X]) f.leadingCoeff⁻¹ : K[X]) = f
rw₁ : f * (C : (a : K) → K[X]) 1⁻¹ = f
rw₂ : f * (C : (a : K) → K[X]) 1 = f
rw₃ : f * 1 = f
⊢ minpoly K (powerBasis hf').gen = f
have rw₄ : f = f
Tactic: rw [minpoly_powerBasis_gen hf', hf.leadingCoeff, inv_one, C.map_one, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
have pos : ∀ (hf : f = 0), finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
pos : ∀ (hf : f = 0), finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
have neg : ∀ (hf : ¬f = 0), finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
Tactic: by_cases hf : f = 0
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : f = 0
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
have pos : finrank K K[X] = 0
Tactic: rw [hf, natDegree_zero,
      ((Submodule.quotEquivOfEqBot _ (by simp)).restrictScalars K).finrank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : ¬f = 0
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
have neg : (powerBasis hf).dim = f.natDegree
Tactic: rw [PowerBasis.finrank]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
K : Type u_5
inst : Field K
f : K[X]
hf : ¬f = 0
neg : (powerBasis hf).dim = f.natDegree
⊢ finrank K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f})) = f.natDegree
have neg₁ : PowerBasis K (HasQuotient.Quotient K[X] (B := Ideal K[X]) (span {f}))
Tactic: rw [PowerBasis.finrank]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ eval₂ (↑(ofId R ↥R[x]) : R →+* ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x ⋯) (minpoly R x) =
    0
have change : Eq.{u_2 + 1} (α := ↥R[x])
  ((aeval (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) x sorry) : (a : R[X]) → ↥R[x])
      (minpoly R x) :
    ↥R[x])
  (0 : ↥R[x])
Tactic: change aeval _ _ = _
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := AdjoinRoot (minpoly R x)) (β := ↥R[x])
    (⇑(toAdjoin R x) : (a : AdjoinRoot (minpoly R x)) → ↥R[x])
have rw : LE.le (α := Subalgebra R ↥R[x])
  (adjoin R (Subtype.val (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) ⁻¹' {x}))
  (AlgHom.range (toAdjoin R x))
Tactic: rw [← AlgHom.range_eq_top, _root_.eq_top_iff, ← adjoin_adjoin_coe_preimage]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x_1 : AdjoinRoot g
x : R[X]
⊢ Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g)
        ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
          ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)) :
      AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
have change : Eq.{u_1 + 1} (α := AdjoinRoot g)
  ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) x) : AdjoinRoot g)
  ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
Tactic: change pb.lift _ _ (aeval _ _) = _
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x_1 : AdjoinRoot g
x : R[X]
⊢ Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) x) : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
have rw : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
  ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
Tactic: rw [pb.lift_aeval, aeval_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x_1 : AdjoinRoot g
x : R[X]
rw :
  Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
⊢ Eq.{u_1 + 1} (α := AdjoinRoot g)
    ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) x) : AdjoinRoot g)
    ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
have rw₁ : Eq (α := AdjoinRoot g) ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
  ((mk g : (a : R[X]) → AdjoinRoot g) x : AdjoinRoot g)
Tactic: rw [pb.lift_aeval, aeval_eq]
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x : S
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
      ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) x : AdjoinRoot g) =
    x
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.RingTheory.AdjoinRoot (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
K : Type u_5
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
g : R[X]
pb : PowerBasis R S
h₁ : Eq (α := AdjoinRoot g) ((aeval (root g) : (a : R[X]) → AdjoinRoot g) (minpoly R pb.gen)) 0
h₂ : Eq.{u_2 + 1} (α := S) ((aeval pb.gen : (a : R[X]) → S) g : S) (0 : S)
x : S
h : Nontrivial S
⊢ (liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
      ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) x : AdjoinRoot g) =
    x
have obtain : ∀ (f : R[X]) (_hf : f.natDegree < pb.dim),
  Eq.{u_2 + 1} (α := S)
    ((liftAlgHom g (Algebra.ofId R S) pb.gen h₂ : (a : AdjoinRoot g) → S)
        ((pb.lift (root g) h₁ : (a : S) → AdjoinRoot g) ((aeval pb.gen : (a : R[X]) → S) f) : AdjoinRoot g) :
      S)
    ((aeval pb.gen : (a : R[X]) → S) f : S)
Tactic: obtain ⟨f, _hf, rfl⟩ := pb.exists_eq_aeval x
Cleared hypotheses: x