-- 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:
ctx : Context
c₁ c₂ : PolyCnstr
h₁ : denote ctx c₁
h₂ : denote ctx c₂
⊢ denote ctx (c₁.combine c₂)

Tactic:
cases c₁

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

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:
rename_i eq₁ lhs₁ rhs₁ eq₂ lhs₂ rhs₂

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 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₂ })

Tactic:
simp [PolyCnstr.combine, denote]

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₂)
⊢ bif eq₁ && eq₂ then
    Poly.denote_eq ctx
      (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)
  else
    Poly.denote_le ctx
      (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Proof state:
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₂)
⊢ bif eq₁ && eq₂ then
    Poly.denote_eq ctx
      (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)
  else
    Poly.denote_le ctx
      (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Tactic:
by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] 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_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_eq ctx
    (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

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)

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)

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)

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_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_eq ctx (lhs₁.combine lhs₂, rhs₁.combine rhs₂)

Tactic:
simp [Poly.denote_eq] 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 pos
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_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_eq ctx
    (((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).fst, ((lhs₁.combine lhs₂).cancel (rhs₁.combine rhs₂)).snd)

Tactic:
rw [Poly.denote_eq_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_eq ctx (lhs₁, rhs₁)
h₂ : Poly.denote_eq ctx (lhs₂, rhs₂)
⊢ Poly.denote_eq 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 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₂

Tactic:
apply Nat.add_le_add_left h₂

Result:
no goals