awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : R[X]
q : PolynomialModule R M
r : R
zero :
  Eq.{u_2 + 1} (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) 0 : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) 0 : M)
add :
  ∀ (f g : PolynomialModule R M)
    (e₁ :
      Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) f : M)
        ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) f : M))
    (e₂ :
      Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) g : M)
        ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) g : M)),
    Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) (f + g) : M)
      ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) (f + g) : M)
⊢ Eq (α := M) ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M) q : M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M) q : M)
have single : ∀ (i : ℕ) (m : M),
  Eq (α := M)
    ((eval r ∘ₗ comp p : (a : PolynomialModule R M) → M)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
    ((eval (Polynomial.eval r p) : (a : PolynomialModule R M) → M)
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
      M)
Tactic: induction q using induction_linear with
  | zero => simp_rw [map_zero]
  | add _ _ e₁ e₂ => simp_rw [map_add, e₁, e₂]
  | single i m =>
    rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, eval_pow]
    module
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ (comp p : (a : PolynomialModule R M) → PolynomialModule R M) (p' • q) =
    HSMul.hSMul (β := PolynomialModule R M) (p'.comp p)
      ((comp p : (a : PolynomialModule R M) → PolynomialModule R M) q : PolynomialModule R M)
have rw : HSMul.hSMul (β := PolynomialModule R M) (eval₂ (algebraMap R R[X]) p p')
    ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
        ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
      PolynomialModule R M) =
  HSMul.hSMul (β := PolynomialModule R M) (eval₂ C p p')
    ((eval p : (a : PolynomialModule R[X] (PolynomialModule R M)) → PolynomialModule R M)
        ((map R[X] (lsingle R 0) : (a : PolynomialModule R M) → PolynomialModule R[X] (PolynomialModule R M)) q) :
      PolynomialModule R M)
Tactic: rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.FiniteDimensional (hypothesis)
Goal:
R : Type u_1
M : Type u_3
A : Type u_4
a : A
inst : CommSemiring R
inst_1 : NoZeroDivisors R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : AddCommMonoid M
inst_5 : Module A M
inst_6 : Module R M
inst_7 : IsScalarTower R A M
p : R[X]
h : Eq.{u_4 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
h' : p ≠ 0
⊢ IsTorsion.{u_1, u_3} R[X] (AEval R M a)
have hp : Membership.mem (γ := Submonoid R[X]) (nonZeroDivisors R[X]) p
Tactic: have hp : p ∈ nonZeroDivisors R[X] := mem_nonZeroDivisors_iff_right.mpr
    fun q hq ↦ Or.resolve_right (mul_eq_zero.mp hq) h'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : LinearMap (R := R[X]) (RingHom.id R[X]) (R[X] ⊗[R] M) (PolynomialModule R M) := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M :=
  (↑R :
        {S : Type u_1} →
          {M M₂ : Type (max u_1 u_2)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (eval X) ∘ₗ
    map R[X] ((TensorProduct.mk R R[X] M : (a : R[X]) → M →ₗ[R] R[X] ⊗[R] M) 1)
⊢ inv ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_3 : Semiring S] →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        e =
    LinearMap.id
have a : ∀ (n : ℕ) (x : M),
  Eq (α := R[X] ⊗[R] M)
    ((((AlgebraTensorModule.curry
                    (inv ∘ₗ
                      (↑R :
                          {S : Type u_1} →
                            {M : Type (max u_1 u_2)} →
                              {M₂ : Type u_2} →
                                [inst : Semiring R] →
                                  [inst_3 : Semiring S] →
                                    [inst_4 : AddCommMonoid M] →
                                      [inst_5 : AddCommMonoid M₂] →
                                        [inst_6 : Module R M] →
                                          [inst_7 : Module R M₂] →
                                            [inst_8 : Module S M] →
                                              [inst_9 : Module S M₂] →
                                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                        e) ∘ₗ
                  monomial n :
                R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
              (a : R) → M →ₗ[R] R[X] ⊗[R] M)
            1 :
          (a : M) → R[X] ⊗[R] M)
        x :
      R[X] ⊗[R] M)
    ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ monomial n : R →ₗ[R] M →ₗ[R] R[X] ⊗[R] M) :
              (a : R) → M →ₗ[R] R[X] ⊗[R] M)
            1 :
          (a : M) → R[X] ⊗[R] M)
        x :
      R[X] ⊗[R] M)
Tactic: ext n x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
| p
have rw : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
  ∑ x ∈ range p.natDegree, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x)
Tactic: rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ p =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
have conv_lhs : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
    ∑ x ∈ range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ i ∈ range p.natDegree, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
Tactic: conv_lhs => rw [p.as_sum_range_C_mul_X_pow, sum_range_succ_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
this : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
have rw : 1 * HPow.hPow (α := R[X]) X p.natDegree +
    ∑ x ∈ range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ i ∈ range p.natDegree, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
Tactic: rw [this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
this : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])
rw :
  1 * HPow.hPow (α := R[X]) X p.natDegree +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
have rw₁ : HPow.hPow (α := R[X]) X p.natDegree +
    ∑ x ∈ range p.natDegree,
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
  HPow.hPow (α := R[X]) X p.natDegree +
    ∑ i ∈ range p.natDegree, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
Tactic: rw [this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (HPow.hPow (α := R[X]) X p.natDegree) +
      ∑ x ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x) =
    HPow.hPow (α := R[X]) X p.natDegree +
      ∑ i ∈ range p.natDegree,
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (p.coeff i) : R[X]) (HPow.hPow (α := R[X]) X i)
have suffices : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) (1 : R[X])
Tactic: suffices C (p.coeff p.natDegree) = 1 by rw [this, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) p).leadingCoeff = 1
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
h : Nontrivial R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) p).leadingCoeff = 1
have rw : leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff = 1
Tactic: rw [leadingCoeff_mul' _]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : b * p.leadingCoeff = 1
h : Nontrivial R
rw : leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff = 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) p).leadingCoeff = 1
have rw₁ : leadingCoeff ((C : (a : R) → R[X]) b) * p.leadingCoeff ≠ 0
Tactic: rw [leadingCoeff_mul' _]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) b : R[X])).leadingCoeff = 1
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
h : Nontrivial R
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) b : R[X])).leadingCoeff = 1
have rw : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) = 1
Tactic: rw [leadingCoeff_mul' _]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
b : R
hp : p.leadingCoeff * b = 1
h : Nontrivial R
rw : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) = 1
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) b : R[X])).leadingCoeff = 1
have rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) b) ≠ 0
Tactic: rw [leadingCoeff_mul' _]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1
have rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
Tactic: rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1
have rw₁ : (if n = n then 1 else 0) + p.coeff n = 1
Tactic: rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
rw₁ : (if n = n then 1 else 0) + p.coeff n = 1
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1
have rw₂ : 1 + p.coeff n = 1
Tactic: rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
rw₁ : (if n = n then 1 else 0) + p.coeff n = 1
rw₂ : 1 + p.coeff n = 1
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1
have rw₃ : HAdd.hAdd (α := R) 1 0 = 1
Tactic: rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
H : p.degree < (↑n : WithBot ℕ)
rw : (HPow.hPow (α := R[X]) X n).coeff n + p.coeff n = 1
rw₁ : (if n = n then 1 else 0) + p.coeff n = 1
rw₂ : 1 + p.coeff n = 1
rw₃ : HAdd.hAdd (α := R) 1 0 = 1
⊢ (HPow.hPow (α := R[X]) X n + p).coeff n = 1
have rw₄ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [coeff_add, coeff_X_pow, if_pos rfl, coeff_eq_zero_of_degree_lt H, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
⊢ (p * q).Monic
have this₁ : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: have : p.leadingCoeff * q.leadingCoeff ≠ 0 := by
      simp [Monic.def.1 hp, Monic.def.1 hq, Ne.symm h0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ (p * q).Monic
have rw : (p * q).leadingCoeff = 1
Tactic: rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).leadingCoeff = 1
⊢ (p * q).Monic
have rw₁ : p.leadingCoeff * q.leadingCoeff = 1
Tactic: rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).leadingCoeff = 1
rw₁ : p.leadingCoeff * q.leadingCoeff = 1
⊢ (p * q).Monic
have rw₂ : 1 * q.leadingCoeff = 1
Tactic: rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).leadingCoeff = 1
rw₁ : p.leadingCoeff * q.leadingCoeff = 1
rw₂ : 1 * q.leadingCoeff = 1
⊢ (p * q).Monic
have rw₃ : HMul.hMul (α := R) 1 1 = 1
Tactic: rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
h0 : ¬Eq.{u + 1} (α := R) 0 1
this : p.leadingCoeff * q.leadingCoeff ≠ 0
rw : (p * q).leadingCoeff = 1
rw₁ : p.leadingCoeff * q.leadingCoeff = 1
rw₂ : 1 * q.leadingCoeff = 1
rw₃ : HMul.hMul (α := R) 1 1 = 1
⊢ (p * q).Monic
have rw₄ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [Monic.def, leadingCoeff_mul' this, Monic.def.1 hp, Monic.def.1 hq, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + q).Monic
have rwa : (p + q).leadingCoeff = 1
Tactic: rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
rwa : (p + q).leadingCoeff = 1
⊢ (p + q).Monic
have rwa₁ : (q + p).leadingCoeff = 1
Tactic: rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
rwa : (p + q).leadingCoeff = 1
rwa₁ : (q + p).leadingCoeff = 1
⊢ (p + q).Monic
have rwa₂ : p.leadingCoeff = 1
Tactic: rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p + q).Monic
have rwa : (p + q).leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_add_of_degree_lt hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : p.degree < q.degree
rwa : (p + q).leadingCoeff = 1
⊢ (p + q).Monic
have rwa₁ : q.leadingCoeff = 1
Tactic: rwa [Monic, leadingCoeff_add_of_degree_lt hpq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : (p * q).Monic
⊢ q.Monic
have contrapose : ∀ (hpq : ¬q.Monic), ¬(p * q).Monic
Tactic: contrapose hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hpq : ¬q.Monic
⊢ ¬(p * q).Monic
have hpq₁ : ¬q.leadingCoeff = 1
Tactic: rw [Monic.def] at hpq ⊢
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : (p * q).Monic
⊢ p.Monic
have contrapose : ∀ (hpq : ¬p.Monic), ¬(p * q).Monic
Tactic: contrapose hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.Monic
⊢ ¬(p * q).Monic
have hpq₁ : ¬p.leadingCoeff = 1
Tactic: rw [Monic.def] at hpq ⊢
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
⊢ (p.comp q).Monic
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
⊢ (p.comp q).Monic
have this : (p.comp q).natDegree = p.natDegree * q.natDegree
Tactic: have : (p.comp q).natDegree = p.natDegree * q.natDegree :=
    natDegree_comp_eq_of_mul_ne_zero <| by simp [hp.leadingCoeff, hq.leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).Monic
have rw : (p.comp q).leadingCoeff = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
⊢ (p.comp q).Monic
have rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
⊢ (p.comp q).Monic
have rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
⊢ (p.comp q).Monic
have rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
⊢ (p.comp q).Monic
have rw₄ : 1 * q.leadingCoeff ^ p.natDegree = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Monic (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
h_1 : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
rw : (p.comp q).leadingCoeff = 1
rw₁ : (p.comp q).coeff (p.comp q).natDegree = 1
rw₂ : (p.comp q).coeff (p.natDegree * q.natDegree) = 1
rw₃ : p.leadingCoeff * q.leadingCoeff ^ p.natDegree = 1
rw₄ : 1 * q.leadingCoeff ^ p.natDegree = 1
⊢ (p.comp q).Monic
have rw₅ : 1 * HPow.hPow (α := R) 1 p.natDegree = 1
Tactic: rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]