Theorem: FreeCMonoid.degree_mul
Proof state before:
case e.t
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }

case e.e
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : ¬y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }
Tactic:
. rw [KVChain.cons_mergeWith_cons_flip hy₁x₁]
  rw [degree_cons y₁ y₂, degree_cons y₁ y₂]
  rw [h_ind_ys]
  conv =>
    lhs; rw [←Nat.add_assoc, Nat.add_comm (deg y₁ * y₂.val), Nat.add_assoc]
Proof state after:
case e.e
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars✝ : KVChain LT.lt fun x => valType
x₁ : α
x₂ : valType
xs : KVChain LT.lt fun x => valType
hxs : KVChain.boundLeft x₁ xs
h_ind_xs :
  ∀ (x : KVChain LT.lt fun x => valType),
    degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs x } =
      degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
y₁ : α
y₂ : valType
ys : KVChain LT.lt fun x => valType
hys : KVChain.boundLeft y₁ ys
h_ind_ys :
  degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
hx₁y₁ : ¬x₁ < y₁
hy₁x₁ : ¬y₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons y₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }