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

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

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
State after:
no goals

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)
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)

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
State after:
no goals

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
State after:
no goals

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

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
State after:
no goals

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

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

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

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 _ _
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

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

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
State after:
no goals