-- Module: Mathlib.Algebra.Polynomial.Coeff
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
simp_rw₆ : x + y * (HPow.hPow (α := R[X]) X m).coeff k ≠ 0 ∧ x * (HPow.hPow (α := R[X]) X k).coeff m + y ≠ 0
simp_rw₇ : (x + y * if k = m then 1 else 0) ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₈ : x + y * 0 ≠ 0 ∧ (x * if m = k then 1 else 0) + y ≠ 0
simp_rw₉ : x + y * 0 ≠ 0 ∧ x * 0 + y ≠ 0
simp_rw₁₀ : x + 0 ≠ 0 ∧ 0 + y ≠ 0
simp_rw₁₁ : x + 0 ≠ 0 ∧ y ≠ 0
simp_rw₁₂ : x ≠ 0 ∧ y ≠ 0
simp_rw₁₃ : ¬x = 0 ∧ ¬y = 0
simp_rw₁₄ : ¬False ∧ ¬y = 0
simp_rw₁₅ : ¬False ∧ ¬False
simp_rw₁₆ : True ∧ True
⊢ {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:
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]

Premises used: and_true, Finset.insert_subset_iff, Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Finset.singleton_subset_iff, Polynomial.mem_support_iff, Ne, Ne.symm, Polynomial.coeff_add, zero_add, MulZeroClass.mul_zero, Polynomial.coeff_X_pow_self, mul_one, add_zero, not_false_eq_true, if_neg