-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem PolyCnstr.eq_false_of_isUnsat (ctx : Context) {c : PolyCnstr} : c.isUnsat → c.denote ctx = False

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
this : Poly.denote ctx lhs ≠ 0
⊢ ¬Poly.denote ctx lhs = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ lhs.isNonZero = true ∧ rhs.isZero = true → Poly.denote ctx rhs < Poly.denote ctx lhs

Tactic:
intro ⟨h₁, h₂⟩

Result:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ Poly.denote ctx rhs < Poly.denote ctx lhs

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isZero = true
h₂ : rhs.isNonZero = true
⊢ ¬0 = Poly.denote ctx rhs

Tactic:
have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂)

Result:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isZero = true
h₂ : rhs.isNonZero = true
this : Poly.denote ctx rhs ≠ 0
⊢ ¬0 = Poly.denote ctx rhs

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isZero = true
h₂ : rhs.isNonZero = true
this : Poly.denote ctx rhs ≠ 0
⊢ ¬0 = Poly.denote ctx rhs

Tactic:
simp [this.symm]

Result:
no goals

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ ¬Poly.denote ctx lhs = 0

Tactic:
have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁)

Result:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
this : Poly.denote ctx lhs ≠ 0
⊢ ¬Poly.denote ctx lhs = 0

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ { eq := eq, lhs := lhs, rhs := rhs }.isUnsat = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = False

Tactic:
simp [isUnsat]

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then lhs.isZero && rhs.isNonZero || lhs.isNonZero && rhs.isZero else lhs.isNonZero && rhs.isZero) = true →
    ¬denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ Poly.denote ctx rhs < Poly.denote ctx lhs

Tactic:
simp [Poly.of_isZero, h₂]

Result:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ 0 < Poly.denote ctx lhs

Proof state:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.isUnsat = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = False

Tactic:
rename_i eq lhs rhs

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ { eq := eq, lhs := lhs, rhs := rhs }.isUnsat = true → denote ctx { eq := eq, lhs := lhs, rhs := rhs } = False

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ ¬Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
simp [Poly.of_isZero, h₂]

Result:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ ¬Poly.denote ctx lhs = 0

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
h₁ : lhs.isNonZero = true
h₂ : rhs.isZero = true
⊢ 0 < Poly.denote ctx lhs

Tactic:
exact Poly.of_isNonZero ctx h₁

Result:
no goals

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true →
    ¬Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
intro
  | Or.inl ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₁]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₂); simp [this.symm]
  | Or.inr ⟨h₁, h₂⟩ => simp [Poly.of_isZero, h₂]; have := Nat.not_eq_zero_of_lt (Poly.of_isNonZero ctx h₁); simp [this]

Result:
no goals

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Poly
⊢ (bif eq then lhs.isZero && rhs.isNonZero || lhs.isNonZero && rhs.isZero else lhs.isNonZero && rhs.isZero) = true →
    ¬denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
by_cases he : eq = true <;> simp [he, denote, Poly.denote_eq, Poly.denote_le, -and_imp]

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
⊢ lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true →
    ¬Poly.denote ctx lhs = Poly.denote ctx rhs

case neg
ctx : Context
eq : Bool
lhs rhs : Poly
he : ¬eq = true
⊢ lhs.isNonZero = true ∧ rhs.isZero = true → Poly.denote ctx rhs < Poly.denote ctx lhs

Proof state:
ctx : Context
c : PolyCnstr
⊢ c.isUnsat = true → denote ctx c = False

Tactic:
cases c

Result:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Poly
⊢ { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.isUnsat = true → denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } = False

Proof state:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isZero = true
h₂ : rhs.isNonZero = true
⊢ ¬Poly.denote ctx lhs = Poly.denote ctx rhs

Tactic:
simp [Poly.of_isZero, h₁]

Result:
ctx : Context
eq : Bool
lhs rhs : Poly
he : eq = true
x✝ : lhs.isZero = true ∧ rhs.isNonZero = true ∨ lhs.isNonZero = true ∧ rhs.isZero = true
h₁ : lhs.isZero = true
h₂ : rhs.isNonZero = true
⊢ ¬0 = Poly.denote ctx rhs