awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : R[X]
rw : Membership.mem (γ := Ideal R[X]) (RingHom.ker h.map) (h.repr ((h.map : (a : R[X]) → S) g) - g)
rw₁ :
  Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) (h.repr ((h.map : (a : R[X]) → S) g)) : S)
    ((h.map : (a : R[X]) → S) g : S)
⊢ f ∣ h.repr ((h.map : (a : R[X]) → S) g) - g
have rw₂ : Eq.{v + 1} (α := S) ((h.map : (a : R[X]) → S) g : S) ((h.map : (a : R[X]) → S) g : S)
Tactic: rw [← h.mem_ker_map, RingHom.sub_mem_ker_iff, map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
| h.repr (x + y) %ₘ f
have rw : h.repr x %ₘ f + h.repr y %ₘ f
Tactic: rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
⊢ h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
have conv_lhs : h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
Tactic: conv_lhs =>
      rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x y : S
conv_lhs : h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
⊢ h.repr (x + y) %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
have conv_lhs₁ : h.repr x %ₘ f + h.repr y %ₘ f = h.repr x %ₘ f + h.repr y %ₘ f
Tactic: conv_lhs =>
      rw [← h.map_repr x, ← h.map_repr y, ← map_add, h.modByMonic_repr_map, add_modByMonic]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₁ : h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
  c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₂ : h.repr (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S) ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
    f =
  c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₃ : h.repr
      (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
        ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
    f =
  c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₄ : h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
  c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₄ :
  h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₅ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x) %ₘ f =
  c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₄ :
  h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₆ : c • h.repr x %ₘ f = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₄ :
  h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₆ : c • h.repr x %ₘ f = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₇ : c • (h.repr x %ₘ f) = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
c : R
x : S
rw : h.repr (c • x) %ₘ f = c • (h.repr x %ₘ f)
rw₁ :
  h.repr (HSMul.hSMul (β := S) c ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₂ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) c : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₃ :
  h.repr
        (HMul.hMul (α := S) (β := S) ((h.map : (a : R[X]) → S) ((C : (a : R) → R[X]) c : R[X]) : S)
          ((h.map : (a : R[X]) → S) (h.repr x) : S)) %ₘ
      f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₄ :
  h.repr ((h.map : (a : R[X]) → S) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x))) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₅ :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (h.repr x) %ₘ f =
    c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₆ : c • h.repr x %ₘ f = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
rw₇ : c • (h.repr x %ₘ f) = c • (h.repr ((h.map : (a : R[X]) → S) (h.repr x)) %ₘ f)
⊢ h.repr (c • x) %ₘ f = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) (h.repr x %ₘ f)
have rw₈ : c • (h.repr x %ₘ f) = c • (h.repr x %ₘ f)
Tactic: rw [RingHom.id_apply, ← h.map_repr x, Algebra.smul_def, h.algebraMap_apply, ← map_mul,
        h.modByMonic_repr_map, ← smul_eq_C_mul, smul_modByMonic, h.map_repr]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
⊢ (h.modByMonicHom : (a : S) → R[X]) (h.root ^ n) = HPow.hPow (α := R[X]) X n
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
h_1 : Nontrivial R
⊢ (h.modByMonicHom : (a : S) → R[X]) (h.root ^ n) = HPow.hPow (α := R[X]) X n
have rw : (↑n : WithBot ℕ) < f.degree
Tactic: rw [← h.map_X, ← map_pow, modByMonicHom_map, modByMonic_eq_self_iff h.monic, degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
n : ℕ
hdeg : n < f.natDegree
h_1 : Nontrivial R
⊢ (↑n : WithBot ℕ) < f.degree
have contrapose! : ∀ (hdeg : f.degree ≤ (↑n : WithBot ℕ)), f.natDegree ≤ n
Tactic: contrapose! hdeg
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
⊢ (fun (g : Fin f.natDegree →₀ R) ↦
        ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
      ((fun (x : S) ↦
          (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
            Fin f.natDegree →₀ R))
        x) =
    x
have a : Nontrivial R
Tactic: nontriviality R using Algebra.subsingleton R S
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
⊢ (fun (g : Fin f.natDegree →₀ R) ↦
        ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
      ((fun (x : S) ↦
          (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
            Fin f.natDegree →₀ R))
        x) =
    x
have simp : (h.map : (a : R[X]) → S)
    {
      toFinsupp :=
        Finsupp.mapDomain (α := Fin f.natDegree) Fin.val
          (Finsupp.comapDomain Fin.val (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)) sorry) } =
  x
Tactic: simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
⊢ (h.map : (a : R[X]) → S)
      {
        toFinsupp :=
          Finsupp.mapDomain (α := Fin f.natDegree) Fin.val
            (Finsupp.comapDomain Fin.val (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)) ⋯) } =
    x
have hf : Function.Injective (α := Fin f.natDegree) Fin.val
Tactic: rw [Finsupp.mapDomain_comapDomain, Polynomial.eta, h.map_modByMonicHom x]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
hf : Function.Injective (α := Fin f.natDegree) Fin.val
⊢ (h.map : (a : R[X]) → S)
      {
        toFinsupp :=
          Finsupp.mapDomain (α := Fin f.natDegree) Fin.val
            (Finsupp.comapDomain Fin.val (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)) ⋯) } =
    x
have hl : (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ) ⊆
  Set.range (ι := Fin f.natDegree) Fin.val
Tactic: rw [Finsupp.mapDomain_comapDomain, Polynomial.eta, h.map_modByMonicHom x]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
i : ℕ
hi : i ∈ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
⊢ i ∈ Set.range (ι := Fin f.natDegree) Fin.val
have hl : i < f.natDegree
Tactic: refine Set.mem_range.mpr ⟨⟨i, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
i : ℕ
hi : i ∈ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
⊢ i < f.natDegree
have hl : ∀ (hi : f.natDegree ≤ i),
  i ∉ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
⊢ i ∉ (↑(Finsupp.support.{0, u} (M := R) (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) : Set ℕ)
have hl : Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := sorry } : (a : S) → R[X]) x) i) 0
Tactic: simp only [Polynomial.toFinsupp_apply, Classical.not_not, Finsupp.mem_support_iff, Ne,
      modByMonicHom, LinearMap.coe_mk, Finset.mem_coe]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
have hl : ∀ (h : IsAdjoinRootMonic.{u, v} (R := R) S 1) (hi : natDegree.{u} (R := R) 1 ≤ i),
  Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ 1, map_add' := sorry } : (a : S) → R[X]) x) i) 0
Tactic: obtain rfl | hf := eq_or_ne f 1
Cleared hypotheses: f, h, hi
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
x : S
h_1 : Nontrivial R
i : ℕ
hi : f.natDegree ≤ i
hl :
  ∀ (h : IsAdjoinRootMonic.{u, v} (R := R) S 1) (hi : natDegree.{u} (R := R) 1 ≤ i),
    Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ 1, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
⊢ Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := ⋯ } : (a : S) → R[X]) x) i) 0
have hl₁ : ∀ (hf : f ≠ 1),
  Eq.{u + 1} (α := R) (coeff (({ toFun := fun (x : S) ↦ h.repr x %ₘ f, map_add' := sorry } : (a : S) → R[X]) x) i) 0
Tactic: obtain rfl | hf := eq_or_ne f 1
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
⊢ (fun (x : S) ↦
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
          Fin f.natDegree →₀ R))
      ((fun (g : Fin f.natDegree →₀ R) ↦
          ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
        g) =
    g
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
⊢ (fun (x : S) ↦
        (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x))) ⋯ :
          Fin f.natDegree →₀ R))
      ((fun (g : Fin f.natDegree →₀ R) ↦
          ((h.map : (a : R[X]) → S) { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } : S))
        g) =
    g
have h₁ : ∀ (i : Fin f.natDegree),
  Eq (α := R)
    (((fun (x : S) ↦
              (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)))
                  sorry :
                Fin f.natDegree →₀ R))
            ((fun (g : Fin f.natDegree →₀ R) ↦
                ((h.map : (a : R[X]) → S)
                    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } :
                  S))
              g) :
          (a : Fin f.natDegree) → R)
        i :
      R)
    ((g : (a : Fin f.natDegree) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
⊢ Eq (α := R)
    (((fun (x : S) ↦
              (Finsupp.comapDomain Fin.val (AddMonoidAlgebra.coeff (toFinsupp ((h.modByMonicHom : (a : S) → R[X]) x)))
                  ⋯ :
                Fin f.natDegree →₀ R))
            ((fun (g : Fin f.natDegree →₀ R) ↦
                ((h.map : (a : R[X]) → S)
                    { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) : R[X] } :
                  S))
              g) :
          (a : Fin f.natDegree) → R)
        i :
      R)
    ((g : (a : Fin f.natDegree) → R) i : R)
have h₁ : ({ toFinsupp := Finsupp.mapDomain Fin.val g : R[X] } %ₘ f).coeff (↑i : ℕ) = (g : (a : Fin f.natDegree) → R) i
Tactic: simp only [AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff, h.modByMonicHom_map,
      Finsupp.comapDomain_apply, Polynomial.toFinsupp_apply]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
⊢ ({ toFinsupp := Finsupp.mapDomain Fin.val g : R[X] } %ₘ f).coeff (↑i : ℕ) = (g : (a : Fin f.natDegree) → R) i
have h₁ : Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) (↑i : ℕ) : R) ((g : (a : Fin f.natDegree) → R) i : R)
Tactic: rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
h₁ : Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) (↑i : ℕ) : R) ((g : (a : Fin f.natDegree) → R) i : R)
⊢ ({ toFinsupp := Finsupp.mapDomain Fin.val g : R[X] } %ₘ f).coeff (↑i : ℕ) = (g : (a : Fin f.natDegree) → R) i
have h₂ : { toFinsupp := Finsupp.mapDomain Fin.val g : R[X] }.degree < f.degree
Tactic: rw [(Polynomial.modByMonic_eq_self_iff h.monic).mpr, Polynomial.coeff]
-- Lean 4 proof step from Mathlib.RingTheory.IsAdjoinRoot (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
f : R[X]
inst_2 : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
h_1 : Nontrivial R
i : Fin f.natDegree
⊢ Eq (α := R) ((Finsupp.mapDomain Fin.val g : (a : ℕ) → R) (↑i : ℕ) : R) ((g : (a : Fin f.natDegree) → R) i : R)
have h₁ : Eq (α := R) ((g : (a : Fin f.natDegree) → R) i : R) ((g : (a : Fin f.natDegree) → R) i : R)
Tactic: rw [Finsupp.mapDomain_apply Fin.val_injective]