c8892e44 mv_polynomial.total_degree_mul

sus_mv_polynomial.total_degree_mul.lean

lemma {u u_1} mv_polynomial.total_degree_mul {R : Type u} {σ : Type u_1}
    [inst_1 : comm_semiring R] (a b : mv_polynomial σ R) :
  mv_polynomial.total_degree (a * b) ≤ 
    mv_polynomial.total_degree a + mv_polynomial.total_degree b :=
finset.sup_le
  (λ (n : σ →₀ nat) (hn : n ∈ finsupp.support (a * b)),
  (λ (this :
        n ∈ 
          finset.bUnion (finsupp.support a)
            (λ (a₁ : σ →₀ nat),
            finset.bUnion (finsupp.support b)
              (λ (a₂ : σ →₀ nat),
              has_singleton.singleton (a₁ + a₂)))),
    Exists.dcases_on
      (eq.mp
        (eq.trans (propext finset.mem_bUnion)
          ((λ (p p_0 : (∀ (ᾰ : σ →₀ nat), Prop)) (e_1 : p = p_0),
            congr_arg Exists e_1)
            (λ (a_0 : σ →₀ nat),
            Exists
              (λ (H : a_0 ∈ finsupp.support a),
              n ∈ 
                finset.bUnion (finsupp.support b)
                  (λ (a₂ : σ →₀ nat),
                  has_singleton.singleton (a_0 + a₂))))
            (λ (a_0 : σ →₀ nat),
            Exists
              (λ (H : a_0 ∈ finsupp.support a),
              Exists
                (λ (a_1 : σ →₀ nat),
                Exists (λ (H_0 : a_1 ∈ finsupp.support b), n = a_0 + a_1))))
            (funext
              (λ (a_0 : σ →₀ nat),
              (λ (p p_0 : (∀ (ᾰ : a_0 ∈ finsupp.support a), Prop))
                  (e_1 : p = p_0),
                congr_arg Exists e_1)
                (λ (H : a_0 ∈ finsupp.support a),
                n ∈ 
                  finset.bUnion (finsupp.support b)
                    (λ (a₂ : σ →₀ nat),
                    has_singleton.singleton (a_0 + a₂)))
                (λ (H : a_0 ∈ finsupp.support a),
                Exists
                  (λ (a_1 : σ →₀ nat),
                  Exists (λ (H_0 : a_1 ∈ finsupp.support b), n = a_0 + a_1)))
                (funext
                  (λ (H : a_0 ∈ finsupp.support a),
                  eq.trans (propext finset.mem_bUnion)
                    ((λ (p p_0 : (∀ (ᾰ : σ →₀ nat), Prop))
                        (e_1 : p = p_0),
                      congr_arg Exists e_1)
                      (λ (a_1 : σ →₀ nat),
                      Exists
                        (λ (H_0 : a_1 ∈ finsupp.support b),
                        n ∈ has_singleton.singleton (a_0 + a_1)))
                      (λ (a_1 : σ →₀ nat),
                      Exists
                        (λ (H_0 : a_1 ∈ finsupp.support b), n = a_0 + a_1))
                      (funext
                        (λ (a_1 : σ →₀ nat),
                        (λ (p p_0 :
                              (∀ (ᾰ : a_1 ∈ finsupp.support b), Prop))
                            (e_1 : p = p_0),
                          congr_arg Exists e_1)
                          (λ (H_0 : a_1 ∈ finsupp.support b),
                          n ∈ has_singleton.singleton (a_0 + a_1))
                          (λ (H_0 : a_1 ∈ finsupp.support b), n = a_0 + a_1)
                          (funext
                            (λ (H_0 : a_1 ∈ finsupp.support b),
                            propext finset.mem_singleton))))))))))) this)
      (λ (a₁ : σ →₀ nat)
        (this_h :
          Exists
            (λ (H : a₁ ∈ finsupp.support a),
            Exists
              (λ (a_0 : σ →₀ nat),
              Exists (λ (H_0 : a_0 ∈ finsupp.support b), n = a₁ + a_0)))),
      Exists.dcases_on this_h
        (λ (h₁ : a₁ ∈ finsupp.support a)
          (this_h_h :
            Exists
              (λ (a_0 : σ →₀ nat),
              Exists (λ (H : a_0 ∈ finsupp.support b), n = a₁ + a_0))),
        Exists.dcases_on this_h_h
          (λ (a₂ : σ →₀ nat)
            (this_h_h_h :
              Exists (λ (H : a₂ ∈ finsupp.support b), n = a₁ + a₂)),
          Exists.dcases_on this_h_h_h
            (λ (h₂ : a₂ ∈ finsupp.support b)
              (this_h_h_h_h : n = a₁ + a₂),
            eq.rec (a₁ + a₂)
              (λ (hn_0 : a₁ + a₂ ∈ finsupp.support (a * b)),
              eq.mpr
                (id
                  (eq.rec
                    (finsupp.sum (a₁ + a₂) (λ (n_0 : σ) (e : nat), e))
                    (eq.refl
                      (finsupp.sum (a₁ + a₂)
                          (λ (n_0 : σ) (e : nat), e) ≤ 
                        mv_polynomial.total_degree a + 
                          mv_polynomial.total_degree b))
                    (finsupp.sum a₁ (λ (n_0 : σ) (e : nat), e) + 
                      finsupp.sum a₂ (λ (n_0 : σ) (e : nat), e))
                    (finsupp.sum_add_index
                      (λ (a_0 : σ), eq.refl has_zero.zero)
                      (λ (a_0 : σ) (b₁ b₂ : nat),
                      eq.refl (b₁ + b₂)))))
                (add_le_add (finset.le_sup h₁) (finset.le_sup h₂))) n
              (eq.symm this_h_h_h_h) hn)))))
    (add_monoid_algebra.support_mul a b hn))