awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R_1 : Type u
S : Type v
a b : R_1
n m : ℕ
inst : Semiring R_1
p_1 q r : R_1[X]
R : Type u_1
A : Type u_2
M : Type u_3
inst_1 : Semiring R
inst_2 : Semiring A
inst_3 : AddCommMonoid M
inst_4 : Module R A
inst_5 : Module R M
f : ℕ → A →ₗ[R] M
c : R
p : A[X]
⊢ ((c • p).sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) c : R)
      (p.sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2)
have rw : ∑ n ∈ p.support, (f n : (a : A) → M) ((c • p).coeff n) =
  HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) c : R)
    (p.sum fun (x1 : ℕ) (x2 : A) ↦ (f x1 : (a : A) → M) x2)
Tactic: rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
⊢ (List.map f l).sum.coeff n = List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l)
have simp_rw : Eq (α := R) (List.sum (List.map (⇑(lcoeff R n) : (a : R[X]) → R) (List.map f l)))
  (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
Tactic: simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
simp_rw :
  Eq (α := R) (List.sum (List.map (⇑(lcoeff R n) : (a : R[X]) → R) (List.map f l)))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
⊢ (List.map f l).sum.coeff n = List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l)
have simp_rw₁ : Eq (α := R) (List.sum (List.map ((⇑(lcoeff R n) : (a : R[X]) → R) ∘ f) l))
  (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
Tactic: simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
l : List ι
f : ι → R[X]
n : ℕ
simp_rw :
  Eq (α := R) (List.sum (List.map (⇑(lcoeff R n) : (a : R[X]) → R) (List.map f l)))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
simp_rw₁ :
  Eq (α := R) (List.sum (List.map ((⇑(lcoeff R n) : (a : R[X]) → R) ∘ f) l))
    (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
⊢ (List.map f l).sum.coeff n = List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l)
have simp_rw₂ : Eq.{u + 1} (α := R) (List.sum (List.map (fun (x : ι) ↦ (lcoeff R n : (a : R[X]) → R) (f x)) l))
  (List.sum (List.map (fun (a : ι) ↦ (f a).coeff n) l))
Tactic: simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
⊢ (p * q).coeff n = ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2
have rcases : ∀ (p : R[ℕ]),
  ({ toFinsupp := p : R[X] } * q).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, { toFinsupp := p : R[X] }.coeff x.1 * q.coeff x.2
Tactic: rcases p with ⟨p⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
q : R[X]
n : ℕ
p : R[ℕ]
⊢ ({ toFinsupp := p : R[X] } * q).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, { toFinsupp := p : R[X] }.coeff x.1 * q.coeff x.2
have rcases : ∀ (q : R[ℕ]),
  ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      { toFinsupp := p : R[X] }.coeff x.1 * { toFinsupp := q : R[X] }.coeff x.2
Tactic: rcases q with ⟨q⟩
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[ℕ]
⊢ ({ toFinsupp := p : R[X] } * { toFinsupp := q : R[X] }).coeff n =
    ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      { toFinsupp := p : R[X] }.coeff x.1 * { toFinsupp := q : R[X] }.coeff x.2
have simp_rw : Eq (α := R) ((p * q : (a : ℕ) → R) n : R)
  (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := R) (β := R) ((p : (a : ℕ) → R) x.1 : R) ((q : (a : ℕ) → R) x.2 : R) :
    R)
Tactic: simp_rw [← ofFinsupp_mul, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).coeff 1 = p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
have rw : ∑ x ∈ map { toFun := fun (i : ℕ) ↦ (i, 1 - i), inj' := sorry } (range (HAdd.hAdd (α := ℕ) 1 1)), p.coeff x.1 * q.coeff x.2 =
  p.coeff 0 * q.coeff 1 + p.coeff 1 * q.coeff 0
Tactic: rw [coeff_mul, Nat.antidiagonal_eq_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
x : R
k n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n = if n = k then x else 0
have rw : (if k = n then x else 0) = if n = k then x else 0
Tactic: rw [C_mul_X_pow_eq_monomial, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) x : R[X]) X).coeff n = if n = 1 then x else 0
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)).coeff n =
  if n = 1 then x else 0
Tactic: rw [← pow_one X, coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
x : R
n : ℕ
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 1)).coeff n =
    if n = 1 then x else 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) x : R[X]) X).coeff n = if n = 1 then x else 0
have rw₁ : (if n = 1 then x else 0) = if n = 1 then x else 0
Tactic: rw [← pow_one X, coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff n = a * p.coeff n
have rcases : ∀ (p : R[ℕ]),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) { toFinsupp := p : R[X] }).coeff n =
    a * { toFinsupp := p : R[X] }.coeff n
Tactic: rcases p with ⟨p⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
p : R[ℕ]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) { toFinsupp := p : R[X] }).coeff n =
    a * { toFinsupp := p : R[X] }.coeff n
have simp_rw : (AddMonoidAlgebra.single 0 a * p : (a : ℕ) → R) n = HMul.hMul (β := R) a ((p : (a : ℕ) → R) n : R)
Tactic: simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f = a • f
have a₁ : ∀ (n : ℕ), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n
have a₁ : a * f.coeff n = (a • f).coeff n
Tactic: rw [coeff_C_mul, coeff_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
n : ℕ
a₁ : a * f.coeff n = (a • f).coeff n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n
have a₂ : a * f.coeff n = a • f.coeff n
Tactic: rw [coeff_C_mul, coeff_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
a : R
f : R[X]
n : ℕ
a₁ : a * f.coeff n = (a • f).coeff n
a₂ : a * f.coeff n = a • f.coeff n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) f).coeff n = (a • f).coeff n
have a₃ : a * f.coeff n = a * f.coeff n
Tactic: rw [coeff_C_mul, coeff_smul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff n = p.coeff n * a
have rcases : ∀ (p : R[ℕ]),
  (HMul.hMul (β := R[X]) { toFinsupp := p : R[X] } ((C : (a : R) → R[X]) a : R[X])).coeff n =
    { toFinsupp := p : R[X] }.coeff n * a
Tactic: rcases p with ⟨p⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (HMul.hMul (β := R[X]) { toFinsupp := p : R[X] } ((C : (a : R) → R[X]) a : R[X])).coeff n =
    { toFinsupp := p : R[X] }.coeff n * a
have simp_rw : (p * AddMonoidAlgebra.single 0 a : (a : ℕ) → R) n = HMul.hMul (α := R) ((p : (a : ℕ) → R) n : R) a
Tactic: simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support =
    {k, m}
have apply : {k, m} ⊆
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
Tactic: apply subset_antisymm (support_binomial' k m x y)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw : k ∈
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
  {m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₁ : k ∈
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
  m ∈
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₂ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
      k ≠
    0 ∧
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
      m ≠
    0
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₃ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
    0 ∧
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
    0
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
simp_rw₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
      0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₄ : x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧
  x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m ≠ 0
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
simp_rw₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
      0
simp_rw₄ :
  x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m ≠ 0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₅ : x * 1 + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y * 1 ≠ 0
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
simp_rw :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    {m} ⊆
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₁ :
  k ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support ∧
    m ∈
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
simp_rw₂ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff
        m ≠
      0
simp_rw₃ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff k +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff k ≠
      0 ∧
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff m +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff m ≠
      0
simp_rw₄ :
  x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m ≠ 0
simp_rw₅ : x * 1 + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y * 1 ≠ 0
⊢ {k, m} ⊆
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).support
have simp_rw₆ : x + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y ≠ 0
Tactic: simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
    coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add,
    add_zero, Ne, hx, hy, not_false_eq_true, and_true]