Theorem: FreeCMonoid.degree_cons (Algdata/Algebra/Monoid/FreeCMonoid.lean)

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ degree deg { vars := KVChain.cons a n xs haxs } = deg a * n.val + degree deg { vars := xs }
Tactic:
dsimp [degree]
State after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ KVChain.foldl (fun d a n => d + deg a * n.val) 0 (KVChain.cons a n xs haxs) =
    deg a * n.val + KVChain.foldl (fun d a n => d + deg a * n.val) 0 xs

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ KVChain.foldl (fun d a n => d + deg a * n.val) 0 (KVChain.cons a n xs haxs) =
    deg a * n.val + KVChain.foldl (fun d a n => d + deg a * n.val) 0 xs
Tactic:
dsimp [KVChain.foldl, List.foldl]
State after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (0 + deg a * n.val) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (0 + deg a * n.val) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList
Tactic:
rw [Nat.add_comm 0]
State after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (deg a * n.val + 0) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList

State before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ List.foldl (fun c x => c + deg x.fst * x.snd.val) (deg a * n.val + 0) xs.toList =
    deg a * n.val + List.foldl (fun c x => c + deg x.fst * x.snd.val) 0 xs.toList
Tactic:
apply List.foldl_hom
State after:
case H
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ ∀ (x : Nat) (y : (_ : α) × valType),
    deg a * n.val + x + deg y.fst * y.snd.val = deg a * n.val + (x + deg y.fst * y.snd.val)

State before:
case H
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
⊢ ∀ (x : Nat) (y : (_ : α) × valType),
    deg a * n.val + x + deg y.fst * y.snd.val = deg a * n.val + (x + deg y.fst * y.snd.val)
Tactic:
intros
State after:
case H
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
x✝ : Nat
y✝ : (_ : α) × valType
⊢ deg a * n.val + x✝ + deg y✝.fst * y✝.snd.val = deg a * n.val + (x✝ + deg y✝.fst * y✝.snd.val)

State before:
case H
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
a : α
n : valType
xs : KVChain LT.lt fun x => valType
haxs : KVChain.boundLeft a xs
x✝ : Nat
y✝ : (_ : α) × valType
⊢ deg a * n.val + x✝ + deg y✝.fst * y✝.snd.val = deg a * n.val + (x✝ + deg y✝.fst * y✝.snd.val)
Tactic:
rw [Nat.add_assoc]
State after:
no goals