-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem PolyCnstr.denote_combine {ctx : Context} {c₁ c₂ : PolyCnstr} (h₁ : c₁.denote ctx) (h₂ : c₂.denote ctx) : (c₁.combine c₂).denote ctx

Proof state:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Tactic:
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-

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

Proof state:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Tactic:
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-

Result:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote ctx lhs₁ ≤ Poly.denote ctx rhs₁
h₂ : Poly.denote ctx lhs₂ = Poly.denote ctx rhs₂
⊢ Poly.denote ctx lhs₁ + Poly.denote ctx lhs₂ ≤ Poly.denote ctx rhs₁ + Poly.denote ctx rhs₂

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

Tactic:
apply Nat.add_le_add h₁ h₂

Result:
no goals

Proof state:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Tactic:
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-

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

Proof state:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx
    (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Tactic:
rw [Poly.denote_le_cancel_eq]

Result:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Proof state:
case mk.mk
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
h₁ : denote ctx { eq := eq₁, lhs := lhs₁, rhs := rhs₁ }
eq₂ : Bool
lhs₂ rhs₂ : Poly
h₂ : denote ctx { eq := eq₂, lhs := lhs₂, rhs := rhs₂ }
⊢ denote ctx ({ eq := eq₁, lhs := lhs₁, rhs := rhs₁ }.combine { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })

Tactic:
simp [denote] at h₁ h₂

Result:
case mk.mk
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
h₁ : bif eq₁ then Poly.denote_eq ctx (lhs₁, rhs₁) else Poly.denote_le ctx (lhs₁, rhs₁)
eq₂ : Bool
lhs₂ rhs₂ : Poly
h₂ : bif eq₂ then Poly.denote_eq ctx (lhs₂, rhs₂) else Poly.denote_le ctx (lhs₂, rhs₂)
⊢ denote ctx ({ eq := eq₁, lhs := lhs₁, rhs := rhs₁ }.combine { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })

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

Tactic:
rw [h₁]

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

Proof state:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx
    (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Tactic:
rw [Poly.denote_le_cancel_eq]

Result:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_le ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Proof state:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx
    (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Tactic:
rw [Poly.denote_le_cancel_eq]

Result:
case neg
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : eq₁ = true
he₂ : ¬eq₂ = true
h₁ : Poly.denote_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_le ctx (lhs₂, rhs₂)
⊢ Poly.denote_le ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Proof state:
case mk
ctx : Context
c₂ : PolyCnstr
h₂ : denote ctx c₂
eq✝ : Bool
lhs✝ rhs✝ : Poly
h₁ : denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }
⊢ denote ctx ({ eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.combine c₂)

Tactic:
cases c₂

Result:
case mk.mk
ctx : Context
eq✝¹ : Bool
lhs✝¹ rhs✝¹ : Poly
h₁ : denote ctx { eq := eq✝¹, lhs := lhs✝¹, rhs := rhs✝¹ }
eq✝ : Bool
lhs✝ rhs✝ : Poly
h₂ : denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }
⊢ denote ctx ({ eq := eq✝¹, lhs := lhs✝¹, rhs := rhs✝¹ }.combine { eq := eq✝, lhs := lhs✝, rhs := rhs✝ })

Proof state:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote ctx lhs₁ ≤ Poly.denote ctx rhs₁
h₂ : Poly.denote ctx lhs₂ = Poly.denote ctx rhs₂
⊢ Poly.denote ctx lhs₁ + Poly.denote ctx lhs₂ ≤ Poly.denote ctx rhs₁ + Poly.denote ctx rhs₂

Tactic:
rw [h₂]

Result:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote ctx lhs₁ ≤ Poly.denote ctx rhs₁
h₂ : Poly.denote ctx lhs₂ = Poly.denote ctx rhs₂
⊢ Poly.denote ctx lhs₁ + Poly.denote ctx rhs₂ ≤ Poly.denote ctx rhs₁ + Poly.denote ctx rhs₂

Proof state:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : ¬eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote ctx lhs₁ ≤ Poly.denote ctx rhs₁
h₂ : Poly.denote ctx lhs₂ = Poly.denote ctx rhs₂
⊢ Poly.denote ctx lhs₁ + Poly.denote ctx rhs₂ ≤ Poly.denote ctx rhs₁ + Poly.denote ctx rhs₂

Tactic:
apply Nat.add_le_add_right h₁

Result:
no goals

Proof state:
case pos
ctx : Context
eq₁ : Bool
lhs₁ rhs₁ : Poly
eq₂ : Bool
lhs₂ rhs₂ : Poly
he₁ : eq₁ = true
he₂ : eq₂ = true
h₁ : Poly.denote ctx lhs₁ = Poly.denote ctx rhs₁
h₂ : Poly.denote ctx lhs₂ = Poly.denote ctx rhs₂
⊢ Poly.denote ctx lhs₁ + Poly.denote ctx lhs₂ = Poly.denote ctx rhs₁ + Poly.denote ctx rhs₂

Tactic:
simp [h₁, h₂]

Result:
no goals