Theorem: IntuitionisticPropositionalLogic.soundness_theorem (GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type ?u.36751
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
⊢ Γ ⊨ A
Tactic:
induction h <;> intros H hH v c hv
State after:
case ax
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case impI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)

case impE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case andI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)

case andE1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case andE2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case orI1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orI2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v C✝

case botE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

State before:
case ax
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case impI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)

case impE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case andI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)

case andE1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case andE2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case orI1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orI2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v C✝

case botE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
solve_by_elim
State after:
case impI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)

case impE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : Γ✝ ⊨ A✝ ⇒ B✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case andI
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : Γ✝ ⊨ A✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)

case andE1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

case andE2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝

case orI1
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orI2
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)

case orE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : Γ✝ ⊨ A✝ || B✝
a_ih✝¹ : insert A✝ Γ✝ ⊨ C✝
a_ih✝ : insert B✝ Γ✝ ⊨ C✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v C✝

case botE
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)
Tactic:
case impI ih =>
  simp
  apply ih
  simp
  intros B hB
  exact inf_le_of_left_le (hv B hB)
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
case impE ih₁ ih₂ =>
  specialize ih₁ hv
  simp at ih₁
  rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)
Tactic:
case andI ih₁ ih₂ => simp [ih₁ hv, ih₂ hv]
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
case andE1 ih =>
  specialize ih hv
  simp at ih
  exact ih.1
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
case andE2 ih =>
  specialize ih hv
  simp at ih
  exact ih.2
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
case orI1 ih =>
  simp
  exact le_trans (ih hv) le_sup_left
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
case orI2 ih =>
  simp
  exact le_trans (ih hv) le_sup_right
State after:
no goals

State before:
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
Tactic:
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)
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
case botE ih =>
  specialize ih hv
  simp at ih
  simp [ih]
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)
Tactic:
simp
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ⊓ eval v A✝ ≤ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ⊓ eval v A✝ ≤ eval v B✝
Tactic:
apply ih
State after:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ B ∈ insert A✝ Γ✝, c ⊓ eval v A✝ ≤ eval v B

State before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ B ∈ insert A✝ Γ✝, c ⊓ eval v A✝ ≤ eval v B
Tactic:
simp
State after:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a

State before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ ∀ a ∈ Γ✝, c ⊓ eval v A✝ ≤ eval v a
Tactic:
intros B hB
State after:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B

State before:
case a
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B✝¹ : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
B : Formula
hB : B ∈ Γ✝
⊢ c ⊓ eval v A✝ ≤ eval v B
Tactic:
exact inf_le_of_left_le (hv B hB)
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih₁ hv
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ≤ eval v (A✝ ⇒ B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih₁
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih₁ : c ⊓ eval v A✝ ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : Γ✝ ⊨ A✝
ih₂ : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ && B✝)
Tactic:
simp [ih₁ hv, ih₂ hv]
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
specialize ih hv
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v A✝
Tactic:
simp at ih
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v A✝
Tactic:
exact ih.1
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : Γ✝ ⊨ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
Tactic:
specialize ih hv
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v (A✝ && B✝)
⊢ c ≤ eval v B✝
Tactic:
simp at ih
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v A✝ ∧ c ≤ eval v B✝
⊢ c ≤ eval v B✝
Tactic:
exact ih.2
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_left
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
Tactic:
simp
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝ ⊔ eval v B✝
Tactic:
exact le_trans (ih hv) le_sup_right
State after:
no goals

State before:
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
Tactic:
specialize ih₁ hv
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ c ≤ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ c ≤ eval v C
Tactic:
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)
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ c ≤ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ c ≤ eval v C
Tactic:
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)
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Tactic:
simp at ih₁
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ≤ eval v C
Tactic:
rw [← inf_eq_left.mpr ih₁, inf_sup_left]
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C
Tactic:
rw [← sup_idem (a := eval v C)]
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C ⊔ eval v C

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v A ⊔ eval v B
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
h3v : ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
⊢ c ⊓ eval v A ⊔ c ⊓ eval v B ≤ eval v C ⊔ eval v C
Tactic:
exact sup_le_sup (ih₂ h2v) (ih₃ h3v)
State after:
no goals

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
Tactic:
simp
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ a ∈ Γ, c ⊓ eval v A ≤ eval v a

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
⊢ ∀ a ∈ Γ, c ⊓ eval v A ≤ eval v a
Tactic:
intros D hD
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v A ≤ eval v D

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v A ≤ eval v D
Tactic:
exact inf_le_of_left_le (hv D hD)
State after:
no goals

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
Tactic:
simp
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ a ∈ Γ, c ⊓ eval v B ≤ eval v a

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ a ∈ Γ, c ⊓ eval v B ≤ eval v a
Tactic:
intros D hD
State after:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v B ≤ eval v D

State before:
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₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
D : Formula
hD : D ∈ Γ
⊢ c ⊓ eval v B ≤ eval v D
Tactic:
exact inf_le_of_left_le (hv D hD)
State after:
no goals

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : Γ✝ ⊨ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v A✝
Tactic:
specialize ih hv
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v bot
⊢ c ≤ eval v A✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c ≤ eval v bot
⊢ c ≤ eval v A✝
Tactic:
simp at ih
State after:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c = ⊥
⊢ c ≤ eval v A✝

State before:
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
ih : c = ⊥
⊢ c ≤ eval v A✝
Tactic:
simp [ih]
State after:
no goals