internlm/Lean-Github huggingface dataset:
Theorem: FreeCMonoid.degree_mul
Proof 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 *
Proof 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 }
Theorem: FreeCMonoid.degree_mul
Proof 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₁⟩
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₁
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 }
Theorem: FreeCMonoid.degree_mul
Proof 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
Proof 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 }
Theorem: FreeCMonoid.degree_mul
Proof 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]
Proof 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 }
Theorem: FreeCMonoid.degree_mul
Proof 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]
Proof 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 })
Theorem: FreeCMonoid.degree_mul
Proof 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
Proof 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 })
Theorem: FreeCMonoid.degree_mul
Proof 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]
Proof 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 })
Theorem: FreeCMonoid.degree_mul
Proof 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
  ]
Proof state after:
no goals
Theorem: FreeCMonoid.degree_mul
Proof 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₁]
Proof 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 }
Theorem: FreeCMonoid.degree_mul
Proof 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₂]
Proof 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 }
Theorem: FreeCMonoid.degree_mul
Proof 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]
Proof state after:
no goals