case orE Γ A B C _h1 _h2 _h3 ih₁ ih₂ ih₃ =>
  specialize ih₁ hv
  have h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D := by
    simp; intros D hD; exact inf_le_of_left_le (hv D hD) have h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D := by
    simp; intros D hD; exact inf_le_of_left_le (hv D hD) simp at ih₁
  rw [← inf_eq_left.mpr ih₁, inf_sup_left]
  rw [← sup_idem (a := eval v C)]
  exact sup_le_sup (ih₂ h2v) (ih₃ h3v)
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₁ : Γ ⊨ A || B
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
⊢ c ≤ eval v C
no goals