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✝ }
ctx : Context
k : Nat
c : PolyCnstr
⊢ denote ctx (mul (k + 1) c) = denote ctx c
cases c
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 }
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✝ }
rename_i eq lhs rhs
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 }
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 }
have : k ≠ 0 → k + 1 ≠ 1 := by intro h; match k with | 0 => contradiction | k+1 => simp; apply Nat.succ_ne_zero
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 }
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 }
have : ¬ (k == 0) → (k + 1 == 1) = false := fun h => beq_false_of_ne (this (ne_of_beq_false (Bool.of_not_eq_true h)))
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 }
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 }
have : ¬ ((k + 1 == 0) = true)  := fun h => absurd (eq_of_beq h) (Nat.succ_ne_zero k)
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
this : (1 == 0) = false
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }
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 }
have : (1 == (0 : Nat)) = false := rfl
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
this✝ : (1 == 0) = false
this : (1 == 1) = true
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }
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
this : (1 == 0) = false
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }
have : (1 == (1 : Nat)) = true  := rfl
case mk.inl.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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 mk.inl.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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 mk.inr.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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 mk.inr.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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 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
this✝ : (1 == 0) = false
this : (1 == 1) = true
⊢ denote ctx (mul (k + 1) { eq := eq, lhs := lhs, rhs := rhs }) = denote ctx { eq := eq, lhs := lhs, rhs := rhs }
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 propext <;> apply Iff.intro <;> intro h
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : k ≠ 0
⊢ k + 1 ≠ 1
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
⊢ k ≠ 0 → k + 1 ≠ 1
intro h
no goals
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : k ≠ 0
⊢ k + 1 ≠ 1
match k with | 0 => contradiction | k+1 => simp; apply Nat.succ_ne_zero
no goals
ctx : Context
k : Nat
eq : Bool
lhs rhs : Poly
h : 0 ≠ 0
⊢ 0 + 1 ≠ 1
contradiction
ctx : Context
k✝ : Nat
eq : Bool
lhs rhs : Poly
k : Nat
h : k + 1 ≠ 0
⊢ ¬k + 1 = 0
ctx : Context
k✝ : Nat
eq : Bool
lhs rhs : Poly
k : Nat
h : k + 1 ≠ 0
⊢ k + 1 + 1 ≠ 1
simp
no goals
ctx : Context
k✝ : Nat
eq : Bool
lhs rhs : Poly
k : Nat
h : k + 1 ≠ 0
⊢ ¬k + 1 = 0
apply Nat.succ_ne_zero
case mk.inr.inr
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
this✝ : (1 == 0) = false
this : (1 == 1) = 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)
case mk.inr.inr
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
this✝ : (1 == 0) = false
this : (1 == 1) = 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)
try simp [eq_of_beq hk]
case mk.inr.inr
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
this✝ : (1 == 0) = false
this : (1 == 1) = 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)
case mk.inr.inr
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
this✝ : (1 == 0) = false
this : (1 == 1) = 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)
simp [eq_of_beq hk]
no goals
case mk.inl.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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
exact Nat.eq_of_mul_eq_mul_left (Nat.zero_lt_succ _) h
no goals
case mk.inl.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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
rw [h]
no goals
case mk.inr.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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
exact Nat.le_of_mul_le_mul_left h (Nat.zero_lt_succ _)
no goals
case mk.inr.inr.a.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
this✝ : (1 == 0) = false
this : (1 == 1) = 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
apply Nat.mul_le_mul_left _ h