-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem PolyCnstr.denote_mul (ctx : Context) (k : Nat) (c : PolyCnstr) : (c.mul (k+1)).denote ctx = c.denote ctx

Proof state:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]

Result:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this : k ≠ 0 → k + 1 ≠ 1
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
ctx : Context
k : Nat
c : PolyCnstr
⊢ denote ctx (mul (k + 1) c) = denote ctx c

Tactic:
cases c

Result:
case mk
ctx : Context
k : Nat
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ denote ctx (mul (k + 1) { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }) = denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }

Proof state:
ctx : Context
k✝ : Nat
eq : Bool
lhs rhs : Poly
k : Nat
h : k + 1 ≠ 0
⊢ k + 1 + 1 ≠ 1

Tactic:
simp [Nat.succ.injEq]

Result:
no goals

Proof state:
case pos
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : (k == 0) = true
⊢ Poly.denote ctx (bif k + 1 == 0 then [] else bif k + 1 == 1 then lhs else Poly.mul.go (k + 1) lhs) ≤
      Poly.denote ctx (bif k + 1 == 0 then [] else bif k + 1 == 1 then rhs else Poly.mul.go (k + 1) rhs) ↔
    Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Tactic:
simp [eq_of_beq hk]

Result:
no goals

Proof state:
case mk
ctx : Context
k : Nat
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ denote ctx (mul (k + 1) { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }) = denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }

Tactic:
rename_i eq lhs rhs

Result:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
by_cases he : eq = true <;> simp [he, PolyCnstr.mul, PolyCnstr.denote, Poly.denote_le, Poly.denote_eq]
   <;> by_cases hk : k == 0 <;> (try simp [eq_of_beq hk]) <;> simp [*] <;> apply Iff.intro <;> intro h

Result:
case neg.mp
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : eq = true
hk : ¬(k == 0) = true
h : (k + 1) * Poly.denote ctx lhs = (k + 1) * Poly.denote ctx rhs
⊢ Poly.denote ctx lhs = Poly.denote ctx rhs

case neg.mpr
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : eq = true
hk : ¬(k == 0) = true
h : Poly.denote ctx lhs = Poly.denote ctx rhs
⊢ (k + 1) * Poly.denote ctx lhs = (k + 1) * Poly.denote ctx rhs

case neg.mp
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : ¬(k == 0) = true
h : (k + 1) * Poly.denote ctx lhs ≤ (k + 1) * Poly.denote ctx rhs
⊢ Poly.denote ctx lhs ≤ Poly.denote ctx rhs

case neg.mpr
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : ¬(k == 0) = true
h : Poly.denote ctx lhs ≤ Poly.denote ctx rhs
⊢ (k + 1) * Poly.denote ctx lhs ≤ (k + 1) * Poly.denote ctx rhs

Proof state:
case neg.mp
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : ¬(k == 0) = true
h : (k + 1) * Poly.denote ctx lhs ≤ (k + 1) * Poly.denote ctx rhs
⊢ Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Tactic:
exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)

Result:
no goals

Proof state:
case neg.mpr
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : eq = true
hk : ¬(k == 0) = true
h : Poly.denote ctx lhs = Poly.denote ctx rhs
⊢ (k + 1) * Poly.denote ctx lhs = (k + 1) * Poly.denote ctx rhs

Tactic:
rw [h]

Result:
no goals

Proof state:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝ : k ≠ 0 → k + 1 ≠ 1
this : ¬(k == 0) = true → (k + 1 == 1) = false
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)

Result:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : 0 ≠ 0
⊢ 0 + 1 ≠ 1

Tactic:
contradiction

Result:
no goals

Proof state:
case neg.mp
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : eq = true
hk : ¬(k == 0) = true
h : (k + 1) * Poly.denote ctx lhs = (k + 1) * Poly.denote ctx rhs
⊢ Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h

Result:
no goals

Proof state:
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : k ≠ 0
⊢ k + 1 ≠ 1

Tactic:
match k with | 0 => contradiction | k+1 => simp [Nat.succ.injEq]

Result:
no goals

Proof state:
case neg.mpr
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : ¬(k == 0) = true
h : Poly.denote ctx lhs ≤ Poly.denote ctx rhs
⊢ (k + 1) * Poly.denote ctx lhs ≤ (k + 1) * Poly.denote ctx rhs

Tactic:
apply Nat.mul_le_mul_left _ h

Result:
no goals

Proof state:
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
⊢ k ≠ 0 → k + 1 ≠ 1

Tactic:
intro h

Result:
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : k ≠ 0
⊢ k + 1 ≠ 1

Proof state:
case pos
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝¹ : k ≠ 0 → k + 1 ≠ 1
this✝ : ¬(k == 0) = true → (k + 1 == 1) = false
this : ¬(k + 1 == 0) = true
he : ¬eq = true
hk : (k == 0) = true
⊢ Poly.denote ctx (bif k + 1 == 0 then [] else bif k + 1 == 1 then lhs else Poly.mul.go (k + 1) lhs) ≤
      Poly.denote ctx (bif k + 1 == 0 then [] else bif k + 1 == 1 then rhs else Poly.mul.go (k + 1) rhs) ↔
    Poly.denote ctx lhs ≤ Poly.denote ctx rhs

Tactic:
try simp [eq_of_beq hk]

Result:
no goals

Proof state:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this : k ≠ 0 → k + 1 ≠ 1
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))

Result:
case mk
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
this✝ : k ≠ 0 → k + 1 ≠ 1
this : ¬(k == 0) = true → (k + 1 == 1) = false
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }