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

State before:
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars x✝ : KVChain LT.lt fun x => valType
⊢ degree deg ({ vars := KVChain.nil } * { vars := x✝ }) = degree deg { vars := KVChain.nil } + degree deg { vars := x✝ }
Tactic:
rw [nil_eq_one, one_mul, degree_one]
State after:
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars x✝ : KVChain LT.lt fun x => valType
⊢ degree deg { vars := x✝ } = 0 + degree deg { vars := x✝ }

State before:
α : Type u
inst✝³ : LinearLT α
inst✝² : DecidableRel LT.lt
deg : α → Nat
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
xvars yvars x✝ : KVChain LT.lt fun x => valType
⊢ degree deg { vars := x✝ } = 0 + degree deg { vars := x✝ }
Tactic:
exact (Nat.zero_add _).symm
State after:
no goals

State before:
α : 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 := xs } * { vars := x }) = degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
⊢ degree deg ({ vars := KVChain.cons x₁ x₂ xs hxs } * { vars := KVChain.nil }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.nil }
Tactic:
rw [nil_eq_one, mul_one, degree_one]
State after:
α : 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 := xs } * { vars := x }) = degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.cons x₁ x₂ xs hxs } = degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + 0

State before:
α : 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 := xs } * { vars := x }) = degree deg { vars := xs } + degree deg { vars := x }
yvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.cons x₁ x₂ xs hxs } = degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + 0
Tactic:
exact (Nat.add_zero _).symm
State after:
no goals

State before:
α : 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 := xs } * { vars := 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.cons x₁ x₂ xs hxs } * { vars := ys }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }
⊢ degree deg ({ vars := KVChain.cons x₁ x₂ xs hxs } * { vars := 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:
dsimp [HMul.hMul, Mul.mul] at *
State after:
α : 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 }
⊢ 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 }

State before:
α : 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 }
⊢ 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:
apply dite (x₁ < y₁) <;> intro hx₁y₁
State after:
case 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₁
⊢ 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
α : 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₁
⊢ 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 }

State before:
case 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₁
⊢ 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
α : 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₁
⊢ 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_rel hx₁y₁]
  rw [degree_cons x₁ x₂, degree_cons x₁ x₂]
  rw [h_ind_xs, Nat.add_assoc]
State after:
case 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₁
⊢ 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 }

State before:
case 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₁
⊢ 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:
apply dite (y₁ < x₁) <;> intro hy₁x₁
State after:
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 }

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]
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 }

State before:
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:
have : x₁ = y₁ := Trichotomous.eq_of_incomp ⟨hx₁y₁,hy₁x₁⟩
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₁
this : x₁ = y₁
⊢ 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 }

State before:
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₁
this : x₁ = y₁
⊢ 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:
cases this
State after:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons x₁ y₂ ys hys }

State before:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ degree deg
      {
        vars :=
          KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) (KVChain.cons x₁ y₂ ys hys) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons x₁ y₂ ys hys }
Tactic:
rw [KVChain.cons_mergeWith_cons_rfl]
State after:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ degree deg
      {
        vars :=
          Option.casesOn (some (valAdd x₂ y₂)) (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys) fun bf =>
            KVChain.cons x₁ bf (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys)
              (_ : KVChain.boundLeft x₁ (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys)) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons x₁ y₂ ys hys }

State before:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ degree deg
      {
        vars :=
          Option.casesOn (some (valAdd x₂ y₂)) (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys) fun bf =>
            KVChain.cons x₁ bf (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys)
              (_ : KVChain.boundLeft x₁ (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys)) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons x₁ y₂ ys hys }
Tactic:
rw [degree_cons, degree_cons, degree_cons]
State after:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (valAdd x₂ y₂).val + degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys } =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })

State before:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (valAdd x₂ y₂).val + degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys } =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })
Tactic:
dsimp
State after:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (x₂.val + y₂.val) + degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys } =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })

State before:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (x₂.val + y₂.val) + degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs ys } =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })
Tactic:
rw [h_ind_xs]
State after:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (x₂.val + y₂.val) + (degree deg { vars := xs } + degree deg { vars := ys }) =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })

State before:
case e.e.refl
α : 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₂ : valType
ys : KVChain LT.lt fun x => valType
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 }
hys : KVChain.boundLeft x₁ ys
hx₁y₁ hy₁x₁ : ¬x₁ < x₁
⊢ deg x₁ * (x₂.val + y₂.val) + (degree deg { vars := xs } + degree deg { vars := ys }) =
    deg x₁ * x₂.val + degree deg { vars := xs } + (deg x₁ * y₂.val + degree deg { vars := ys })
Tactic:
conv =>
  rhs;
  rw [
    Nat.add_assoc,
    ←Nat.add_assoc _ (deg x₁ * y₂.val),
    Nat.add_comm _ (deg x₁ * y₂.val),
    Nat.add_assoc,
    ←Nat.add_assoc,
    ←Nat.mul_add (deg x₁) x₂.val y₂.val
  ]
State after:
no goals

State before:
case 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₁
⊢ 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_rel hx₁y₁]
State after:
case 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₁
⊢ degree deg
      {
        vars :=
          KVChain.cons x₁ x₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (KVChain.cons y₁ y₂ ys hys))
            (_ :
              KVChain.boundLeft x₁
                (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (KVChain.cons y₁ y₂ ys hys))) } =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }

State before:
case 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₁
⊢ degree deg
      {
        vars :=
          KVChain.cons x₁ x₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (KVChain.cons y₁ y₂ ys hys))
            (_ :
              KVChain.boundLeft x₁
                (KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (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 [degree_cons x₁ x₂, degree_cons x₁ x₂]
State after:
case 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₁
⊢ deg x₁ * x₂.val +
      degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (KVChain.cons y₁ y₂ ys hys) } =
    deg x₁ * x₂.val + degree deg { vars := xs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }

State before:
case 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₁
⊢ deg x₁ * x₂.val +
      degree deg { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) xs (KVChain.cons y₁ y₂ ys hys) } =
    deg x₁ * x₂.val + degree deg { vars := xs } + degree deg { vars := KVChain.cons y₁ y₂ ys hys }
Tactic:
rw [h_ind_xs, Nat.add_assoc]
State after:
no goals

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 }
Tactic:
rw [KVChain.cons_mergeWith_cons_flip hy₁x₁]
State after:
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.cons y₁ y₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)
            (_ :
              KVChain.boundLeft y₁
                (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 := KVChain.cons y₁ y₂ ys hys }

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.cons y₁ y₂ (KVChain.mergeWith (fun x a b => some (valAdd a b)) (KVChain.cons x₁ x₂ xs hxs) ys)
            (_ :
              KVChain.boundLeft y₁
                (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 := KVChain.cons y₁ y₂ ys hys }
Tactic:
rw [degree_cons y₁ y₂, degree_cons y₁ y₂]
State after:
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₁
⊢ deg y₁ * y₂.val +
      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 } + (deg y₁ * y₂.val + degree deg { vars := ys })

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₁
⊢ deg y₁ * y₂.val +
      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 } + (deg y₁ * y₂.val + degree deg { vars := ys })
Tactic:
rw [h_ind_ys]
State after:
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₁
⊢ deg y₁ * y₂.val + (degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })

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₁
⊢ deg y₁ * y₂.val + (degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + degree deg { vars := ys }) =
    degree deg { vars := KVChain.cons x₁ x₂ xs hxs } + (deg y₁ * y₂.val + degree deg { vars := ys })
Tactic:
conv =>
  lhs; rw [←Nat.add_assoc, Nat.add_comm (deg y₁ * y₂.val), Nat.add_assoc]
State after:
no goals