internlm/Lean-Github huggingface dataset:
Theorem: FreeCMonoid.valAdd_comm
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
a b : valType
⊢ valAdd a b = valAdd b a
Tactic:
cases a
Proof state after:
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
b : valType
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝, property := property✝ } b = valAdd b { val := val✝, property := property✝ }
Theorem: FreeCMonoid.valAdd_comm
Proof state before:
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
b : valType
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝, property := property✝ } b = valAdd b { val := val✝, property := property✝ }
Tactic:
cases b
Proof state after:
case mk.mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ } =
    valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }
Theorem: FreeCMonoid.valAdd_comm
Proof state before:
case mk.mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ } =
    valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }
Tactic:
apply Subtype.eq
Proof state after:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ (valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }).val =
    (valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }).val
Theorem: FreeCMonoid.valAdd_comm
Proof state before:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ (valAdd { val := val✝¹, property := property✝¹ } { val := val✝, property := property✝ }).val =
    (valAdd { val := val✝, property := property✝ } { val := val✝¹, property := property✝¹ }).val
Tactic:
dsimp [valAdd]
Proof state after:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ val✝¹ + val✝ = val✝ + val✝¹
Theorem: FreeCMonoid.valAdd_comm
Proof state before:
case mk.mk.a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
val✝¹ : Nat
property✝¹ : Nat.lt 0 val✝¹
val✝ : Nat
property✝ : Nat.lt 0 val✝
⊢ val✝¹ + val✝ = val✝ + val✝¹
Tactic:
rw [Nat.add_comm]
Proof state after:
no goals
Theorem: FreeCMonoid.mul_comm
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ x * y = y * x
Tactic:
dsimp [HMul.hMul, Mul.mul]
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars } =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }
Theorem: FreeCMonoid.mul_comm
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars } =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }
Tactic:
apply FreeCMonoid.eq
Proof state after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars }.vars =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }.vars
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars }.vars =
    { vars := KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars }.vars
Tactic:
dsimp
Proof state after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun x a b => some (valAdd a b)) x.vars y.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
rw [KVChain.mergeWith_flip]
Proof state after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a => flip fun a b => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a => flip fun a b => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
dsimp [flip]
Proof state after:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a b a => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ KVChain.mergeWith (fun a b a => some (valAdd a b)) y.vars x.vars =
    KVChain.mergeWith (fun x a b => some (valAdd a b)) y.vars x.vars
Tactic:
apply KVChain.mergeWith_congrFun
Proof state after:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ α → ∀ (b₁ b₂ : valType), some (valAdd b₂ b₁) = some (valAdd b₁ b₂)
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
⊢ α → ∀ (b₁ b₂ : valType), some (valAdd b₂ b₁) = some (valAdd b₁ b₂)
Tactic:
intros
Proof state after:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
a✝ : α
b₁✝ b₂✝ : valType
⊢ some (valAdd b₂✝ b₁✝) = some (valAdd b₁✝ b₂✝)
Theorem: FreeCMonoid.mul_comm
Proof state before:
case a.hfg
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
x y : FreeCMonoid α
a✝ : α
b₁✝ b₂✝ : valType
⊢ some (valAdd b₂✝ b₁✝) = some (valAdd b₁✝ b₂✝)
Tactic:
rw [valAdd_comm]
Proof state after:
no goals
Theorem: FreeCMonoid.degree_cons
Proof 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]
Proof 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
Theorem: FreeCMonoid.degree_cons
Proof 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]
Proof 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
Theorem: FreeCMonoid.degree_cons
Proof 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]
Proof 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
Theorem: FreeCMonoid.degree_cons
Proof 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
Proof 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)
Theorem: FreeCMonoid.degree_cons
Proof 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
Proof 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)
Theorem: FreeCMonoid.degree_cons
Proof 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]
Proof state after:
no goals
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
xs : FreeCMonoid α
hxs : degree deg xs = 0
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
⊢ xs = 1
Tactic:
revert hxs
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
xs : FreeCMonoid α
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
⊢ degree deg xs = 0 → xs = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
xs : FreeCMonoid α
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
⊢ degree deg xs = 0 → xs = 1
Tactic:
cases xs with | mk xvars =>
apply xvars.recOnList (motive:=λ xvars => degree deg ⟨xvars⟩ = 0 → FreeCMonoid.mk xvars = 1)
case mk.nil => intros; rfl
case mk.cons =>
  intro a b xvars _ _ heq0
  rw [degree_cons] at heq0
  have : deg a * b.1 > 0 := Nat.mul_pos (hdeg_pos a) b.2
  have : deg a * b.val + degree deg ⟨xvars⟩ > 0 :=
    calc
      0 < deg a * b.val := Nat.mul_pos (hdeg_pos a) b.2
      _ ≤ deg a * b.val + degree deg ⟨xvars⟩ := Nat.le_add_right _ _
  rw [heq0] at this
  cases this
Proof state after:
no goals
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
case mk
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := xvars } = 0 → { vars := xvars } = 1
Tactic:
apply xvars.recOnList (motive:=λ xvars => degree deg ⟨xvars⟩ = 0 → FreeCMonoid.mk xvars = 1)
Proof state after:
case mk.nil
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.nil } = 0 → { vars := KVChain.nil } = 1

case mk.cons
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ ∀ (a : α) (b : valType) (xs : KVChain LT.lt fun x => valType) (haxs : KVChain.boundLeft a xs),
    (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) xs →
      (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) (KVChain.cons a b xs haxs)
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.nil } = 0 → { vars := KVChain.nil } = 1
Tactic:
case mk.nil => intros; rfl
Proof state after:
no goals
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ ∀ (a : α) (b : valType) (xs : KVChain LT.lt fun x => valType) (haxs : KVChain.boundLeft a xs),
    (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) xs →
      (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) (KVChain.cons a b xs haxs)
Tactic:
case mk.cons =>
  intro a b xvars _ _ heq0
  rw [degree_cons] at heq0
  have : deg a * b.1 > 0 := Nat.mul_pos (hdeg_pos a) b.2
  have : deg a * b.val + degree deg ⟨xvars⟩ > 0 :=
    calc
      0 < deg a * b.val := Nat.mul_pos (hdeg_pos a) b.2
      _ ≤ deg a * b.val + degree deg ⟨xvars⟩ := Nat.le_add_right _ _
  rw [heq0] at this
  cases this
Proof state after:
no goals
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ degree deg { vars := KVChain.nil } = 0 → { vars := KVChain.nil } = 1
Tactic:
intros
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
a✝ : degree deg { vars := KVChain.nil } = 0
⊢ { vars := KVChain.nil } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
a✝ : degree deg { vars := KVChain.nil } = 0
⊢ { vars := KVChain.nil } = 1
Tactic:
rfl
Proof state after:
no goals
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars : KVChain LT.lt fun x => valType
⊢ ∀ (a : α) (b : valType) (xs : KVChain LT.lt fun x => valType) (haxs : KVChain.boundLeft a xs),
    (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) xs →
      (fun xvars => degree deg { vars := xvars } = 0 → { vars := xvars } = 1) (KVChain.cons a b xs haxs)
Tactic:
intro a b xvars _ _ heq0
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : degree deg { vars := KVChain.cons a b xvars haxs✝ } = 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : degree deg { vars := KVChain.cons a b xvars haxs✝ } = 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Tactic:
rw [degree_cons] at heq0
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Tactic:
have : deg a * b.1 > 0 := Nat.mul_pos (hdeg_pos a) b.2
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this : deg a * b.val > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this : deg a * b.val > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Tactic:
have : deg a * b.val + degree deg ⟨xvars⟩ > 0 :=
  calc
    0 < deg a * b.val := Nat.mul_pos (hdeg_pos a) b.2
    _ ≤ deg a * b.val + degree deg ⟨xvars⟩ := Nat.le_add_right _ _
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this✝ : deg a * b.val > 0
this : deg a * b.val + degree deg { vars := xvars } > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this✝ : deg a * b.val > 0
this : deg a * b.val + degree deg { vars := xvars } > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Tactic:
rw [heq0] at this
Proof state after:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this✝ : deg a * b.val > 0
this : 0 > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Theorem: FreeCMonoid.eq_one_of_degree_zero
Proof state before:
α : Type u
inst✝¹ : LinearLT α
inst✝ : DecidableRel LT.lt
deg : α → Nat
hdeg_pos : autoParam (∀ (a : α), deg a > 0) _auto✝
xvars✝ : KVChain LT.lt fun x => valType
a : α
b : valType
xvars : KVChain LT.lt fun x => valType
haxs✝ : KVChain.boundLeft a xvars
a✝ : degree deg { vars := xvars } = 0 → { vars := xvars } = 1
heq0 : deg a * b.val + degree deg { vars := xvars } = 0
this✝ : deg a * b.val > 0
this : 0 > 0
⊢ { vars := KVChain.cons a b xvars haxs✝ } = 1
Tactic:
cases this
Proof state after:
no goals
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 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]
Proof 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✝ }
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 x✝ : KVChain LT.lt fun x => valType
⊢ degree deg { vars := x✝ } = 0 + degree deg { vars := x✝ }
Tactic:
exact (Nat.zero_add _).symm
Proof state after:
no goals
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
⊢ 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]
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 := 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
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
⊢ 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
Proof state after:
no goals