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 (combine { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } c₂)
ctx : Context
c₁ c₂ : PolyCnstr
h₁ : denote ctx c₁
h₂ : denote ctx c₂
⊢ denote ctx (combine c₁ c₂)
cases c₁
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 (combine { eq := eq✝¹, lhs := lhs✝¹, rhs := rhs✝¹ } { eq := eq✝, lhs := lhs✝, rhs := rhs✝ })
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 (combine { eq := eq✝, lhs := lhs✝, rhs := rhs✝ } c₂)
cases c₂
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 (combine { eq := eq₁, lhs := lhs₁, rhs := rhs₁ } { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })
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 (combine { eq := eq✝¹, lhs := lhs✝¹, rhs := rhs✝¹ } { eq := eq✝, lhs := lhs✝, rhs := rhs✝ })
rename_i eq₁ lhs₁ rhs₁ eq₂ lhs₂ rhs₂
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 (combine { eq := eq₁, lhs := lhs₁, rhs := rhs₁ } { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })
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 (combine { eq := eq₁, lhs := lhs₁, rhs := rhs₁ } { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })
simp [denote] at h₁ h₂
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
      ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
        (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
  else
    Poly.denote_le ctx
      ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
        (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
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 (combine { eq := eq₁, lhs := lhs₁, rhs := rhs₁ } { eq := eq₂, lhs := lhs₂, rhs := rhs₂ })
simp [PolyCnstr.combine, denote]
case mk.mk.inl.inl
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)

case mk.mk.inl.inr
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)

case mk.mk.inr.inl
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)

case mk.mk.inr.inr
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
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
      ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
        (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
  else
    Poly.denote_le ctx
      ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
        (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
by_cases he₁ : eq₁ = true <;> by_cases he₂ : eq₂ = true <;> simp [he₁, he₂] at h₁ h₂ |-
case mk.mk.inl.inl
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
case mk.mk.inl.inl
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
rw [Poly.denote_eq_cancel_eq]
case mk.mk.inl.inl
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₂
case mk.mk.inl.inl
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
simp [Poly.denote_eq] at h₁ h₂ |-
no goals
case mk.mk.inl.inl
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₂
simp [h₁, h₂]
case mk.mk.inl.inr
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
case mk.mk.inl.inr
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
rw [Poly.denote_le_cancel_eq]
case mk.mk.inl.inr
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₂
case mk.mk.inl.inr
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-
case mk.mk.inl.inr
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₂
case mk.mk.inl.inr
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₂
rw [h₁]
no goals
case mk.mk.inl.inr
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₂
apply Nat.add_le_add_left h₂
case mk.mk.inr.inl
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
case mk.mk.inr.inl
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
rw [Poly.denote_le_cancel_eq]
case mk.mk.inr.inl
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₂
case mk.mk.inr.inl
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-
case mk.mk.inr.inl
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₂
case mk.mk.inr.inl
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₂
rw [h₂]
no goals
case mk.mk.inr.inl
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₂
apply Nat.add_le_add_right h₁
case mk.mk.inr.inr
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
case mk.mk.inr.inr
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
    ((Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).fst,
      (Poly.cancel (Poly.combine lhs₁ lhs₂) (Poly.combine rhs₁ rhs₂)).snd)
rw [Poly.denote_le_cancel_eq]
case mk.mk.inr.inr
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₂
case mk.mk.inr.inr
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 (Poly.combine lhs₁ lhs₂, Poly.combine rhs₁ rhs₂)
simp [Poly.denote_eq, Poly.denote_le] at h₁ h₂ |-
no goals
case mk.mk.inr.inr
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₂
apply Nat.add_le_add h₁ h₂