-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Certificate.of_combineHyps (ctx : Context) (c : PolyCnstr) (cs : Certificate) (h : (combineHyps c cs).denote ctx → False) : c.denote ctx → cs.denote ctx

Proof state:
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)

Tactic:
intro h₁ h₂

Result:
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

Proof state:
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) c'.toNormPoly) →
    PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs

Tactic:
simp at this

Result:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs

Proof state:
ctx : Context
c : PolyCnstr
cs : Certificate
h : ¬PolyCnstr.denote ctx c
⊢ ¬PolyCnstr.denote ctx c

Tactic:
exact h

Result:
no goals

Proof state:
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

Tactic:
have := PolyCnstr.denote_combine (ctx := ctx) (c₂ := PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c')) h₁

Result:
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) c'.toNormPoly) →
    PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs

Proof state:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
this : PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
ih :
  (PolyCnstr.denote ctx (combineHyps (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly)) cs) → False) →
    PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly)) → denote ctx cs
⊢ denote ctx cs

Tactic:
exact ih h this

Result:
no goals

Proof state:
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx (combineHyps c cs) → False
⊢ PolyCnstr.denote ctx c → denote ctx cs

Tactic:
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

Result:
no goals

Proof state:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
this : PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs

Tactic:
have ih := of_combineHyps ctx (PolyCnstr.combine c (PolyCnstr.mul (k + 1) (ExprCnstr.toNormPoly c'))) cs

Result:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
this : PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
ih :
  (PolyCnstr.denote ctx (combineHyps (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly)) cs) → False) →
    PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly)) → denote ctx cs
⊢ denote ctx cs

Proof state:
ctx : Context
c : PolyCnstr
cs : Certificate
h : PolyCnstr.denote ctx (combineHyps c []) → False
⊢ PolyCnstr.denote ctx c → denote ctx []

Tactic:
simp [combineHyps, denote] at *

Result:
ctx : Context
c : PolyCnstr
cs : Certificate
h : ¬PolyCnstr.denote ctx c
⊢ ¬PolyCnstr.denote ctx c

Proof state:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs

Tactic:
have := this h₂

Result:
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 (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
this : PolyCnstr.denote ctx (c.combine (PolyCnstr.mul (k + 1) c'.toNormPoly))
⊢ denote ctx cs