-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
inst : Semiring R
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 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) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
      {n} ⊆
        (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) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support ∧
      n ∈
        (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) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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) +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
          m ≠
        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) +
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).coeff
          n ≠
        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 +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).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 +
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).coeff m ≠
        0 ∧
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)).coeff n +
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) y : R[X]) (HPow.hPow (α := R[X]) X m)).coeff n +
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n ≠
        0
simp_rw₄ :
  x * (HPow.hPow (α := R[X]) X k).coeff k + y * (HPow.hPow (α := R[X]) X m).coeff k +
        z * (HPow.hPow (α := R[X]) X n).coeff k ≠
      0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * (HPow.hPow (α := R[X]) X m).coeff m +
          z * (HPow.hPow (α := R[X]) X n).coeff m ≠
        0 ∧
      x * (HPow.hPow (α := R[X]) X k).coeff n + y * (HPow.hPow (α := R[X]) X m).coeff n +
          z * (HPow.hPow (α := R[X]) X n).coeff n ≠
        0
simp_rw₅ :
  x * 1 + y * (HPow.hPow (α := R[X]) X m).coeff k + z * (HPow.hPow (α := R[X]) X n).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y * 1 + z * (HPow.hPow (α := R[X]) X n).coeff m ≠ 0 ∧
      x * (HPow.hPow (α := R[X]) X k).coeff n + y * (HPow.hPow (α := R[X]) X m).coeff n + z * 1 ≠ 0
simp_rw₆ :
  x + y * (HPow.hPow (α := R[X]) X m).coeff k + z * (HPow.hPow (α := R[X]) X n).coeff k ≠ 0 ∧
    x * (HPow.hPow (α := R[X]) X k).coeff m + y + z * (HPow.hPow (α := R[X]) X n).coeff m ≠ 0 ∧
      x * (HPow.hPow (α := R[X]) X k).coeff n + y * (HPow.hPow (α := R[X]) X m).coeff n + z ≠ 0
simp_rw₇ :
  ((x + y * if k = m then 1 else 0) + z * if k = n then 1 else 0) ≠ 0 ∧
    ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0) ≠ 0 ∧
      ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0
simp_rw₈ :
  (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    ((x * if m = k then 1 else 0) + y + z * if m = n then 1 else 0) ≠ 0 ∧
      ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0
simp_rw₉ :
  (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    (x * 0 + y + z * if m = n then 1 else 0) ≠ 0 ∧ ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0
simp_rw₁₀ :
  (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧
    x * 0 + y + z * 0 ≠ 0 ∧ ((x * if n = k then 1 else 0) + y * if n = m then 1 else 0) + z ≠ 0
⊢ {k, m, n} ⊆
    (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) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) z : R[X]) (HPow.hPow (α := R[X]) X n)).support
have simp_rw₁₁ : (x + y * 0 + z * if k = n then 1 else 0) ≠ 0 ∧ x * 0 + y + z * 0 ≠ 0 ∧ (x * if n = k then 1 else 0) + y * 0 + z ≠ 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.ne, if_neg hkm.ne', if_neg hmn.ne,
    if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
    zero_add, Ne, hx, hy, hz, not_false_eq_true, and_true]