no goals
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx (combineHyps c cs) → False
⊢ PolyCnstr.denote ctx c → denote ctx cs
match cs with
| [] => simp [combineHyps, denote] at *; exact h
| (k, c')::cs =>
  intro h₁ h₂
  have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) h₁
  simp at this
  have := this h₂
  have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs
  exact ih h this
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx c → False
⊢ PolyCnstr.denote ctx c → False
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx (combineHyps c []) → False
⊢ PolyCnstr.denote ctx c → denote ctx []
simp [combineHyps, denote] at *
no goals
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx c → False
⊢ PolyCnstr.denote ctx c → False
exact h
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
⊢ denote ctx cs
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
⊢ PolyCnstr.denote ctx c → denote ctx ((k, c') :: cs)
intro h₁ h₂
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this :
  PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) →
    PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
⊢ denote ctx cs
have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) h₁
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this :
  PolyCnstr.denote ctx (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) →
    PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
simp at this
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this✝ :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
this : PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
have := this h₂
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this✝ :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
this : PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
ih :
  (PolyCnstr.denote ctx (combineHyps (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs) →
      False) →
    PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) → denote ctx cs
⊢ denote ctx cs
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this✝ :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
this : PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
⊢ denote ctx cs
have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs
no goals
ctx : Context
c : PolyCnstr
cs✝ : Certificate
k : Nat
c' : ExprCnstr
cs : List (Nat × ExprCnstr)
h : PolyCnstr.denote ctx (combineHyps c ((k, c') :: cs)) → False
h₁ : PolyCnstr.denote ctx c
h₂ : ExprCnstr.denote ctx c'
this✝ :
  ExprCnstr.denote ctx c' → PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
this : PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')))
ih :
  (PolyCnstr.denote ctx (combineHyps (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs) →
      False) →
    PolyCnstr.denote ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) → denote ctx cs
⊢ denote ctx cs
exact ih h this