case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ isValid { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = True
ctx : Context
c : PolyCnstr
⊢ isValid c = true → denote ctx c = True
cases c
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ isValid { eq := eq, lhs := lhs, rhs := rhs } = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ isValid { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = True
rename_i eq lhs rhs
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then Poly.isZero lhs && Poly.isZero rhs else Poly.isZero lhs) = true →
    denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ isValid { eq := eq, lhs := lhs, rhs := rhs } = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True
simp [isValid]
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ Poly.isZero lhs = true ∧ Poly.isZero rhs = true → (Poly.denote ctx lhs = Poly.denote ctx rhs) = True

case mk.inr
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ Poly.isZero lhs = true → (Poly.denote ctx lhs ≤ Poly.denote ctx rhs) = True
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then Poly.isZero lhs && Poly.isZero rhs else Poly.isZero lhs) = true →
    denote ctx { eq := eq, lhs := lhs, rhs := rhs } = True
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le]
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
h₁ : Poly.isZero lhs = true
h₂ : Poly.isZero rhs = true
⊢ (Poly.denote ctx lhs = Poly.denote ctx rhs) = True
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ Poly.isZero lhs = true ∧ Poly.isZero rhs = true → (Poly.denote ctx lhs = Poly.denote ctx rhs) = True
intro ⟨h₁, h₂⟩
no goals
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
h₁ : Poly.isZero lhs = true
h₂ : Poly.isZero rhs = true
⊢ (Poly.denote ctx lhs = Poly.denote ctx rhs) = True
simp [Poly.of_isZero, h₁, h₂]
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h : Poly.isZero lhs = true
⊢ (Poly.denote ctx lhs ≤ Poly.denote ctx rhs) = True
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ Poly.isZero lhs = true → (Poly.denote ctx lhs ≤ Poly.denote ctx rhs) = True
intro h
no goals
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h : Poly.isZero lhs = true
⊢ (Poly.denote ctx lhs ≤ Poly.denote ctx rhs) = True
simp [Poly.of_isZero, h]