mv_polynomial puzzles

Stream: maths

[Kevin Buzzard]

I keep coming up with these. Do we have this one? What is it called, if so?

import data.mv_polynomial

open mv_polynomial

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} :
finset.sum p.support (λ s, monomial s (p.coeff s)) = p := sorry

[Kevin Buzzard]

I am such a hacker:

example {R : Type*} [comm_semiring R] {σ : Type*} {p : mv_polynomial σ R} :
finset.sum p.support (λ s, monomial s (p.coeff s)) = p :=
begin
  apply mv_polynomial.ext,
  intro s,
  rw coeff_sum,
  simp only [coeff_monomial],
  by_cases hs : s ∈ p.support,
  { rw ←finset.sum_subset (show {s} ⊆ p.support, begin
      intros i hi,
      convert hs,
      cases hi, assumption, cases hi
    end),
    swap,
    { intros t ht hts,
      rw if_neg,
      intro hts2,
      apply hts,
      rw hts2,
      apply set.mem_singleton,
    },
    convert finset.sum_singleton,
    rw if_pos,
    refl
  },
  { rw ←finset.sum_subset (finset.empty_subset p.support),
    swap,
    { intros t ht1 ht2,
      rw if_neg,
      intro hts,
      apply hs,
      rwa hts at ht1,
    },
    rw finset.sum_empty,
    rw finsupp.mem_support_iff at hs,
    symmetry,
    apply classical.not_not.1 hs
  }
end

I sometimes feel like I write Lean the way a child would.