Theorem: IntuitionisticPropositionalLogic.weakening (LCTutorial/Solutions/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
induction h generalizing Δ
State after:
case ax
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case impI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝

case impE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case andI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝

case andE1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case andE2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case orI1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orI2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orE
H : Type ?u.100787
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✝² : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
a_ih✝ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝

case botE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case ax => apply ax; solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
case impI ih => apply impI; solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case impE ih₁ ih₂ => apply impE <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝
Tactic:
case andI ih₁ ih₂ => apply andI <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case andE1 ih => apply andE1 <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
case andE2 ih => apply andE2 <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI1 ih => apply orI1; solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
case orI2 ih => apply orI2; solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
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✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
ih₂ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
ih₃ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝
Tactic:
case orE ih₁ ih₂ ih₃ => apply orE <;> solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case botE ih => apply botE; solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply ax
State after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ

State before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Tactic:
solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝
Tactic:
apply impI
State after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝

State before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert A✝ Δ ⊢ B✝
Tactic:
solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
apply impE <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
ih₂ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝
Tactic:
apply andI <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply andE1 <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
apply andE2 <;> solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
apply orI1
State after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

State before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝
Tactic:
apply orI2
State after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

State before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝
Tactic:
solve_by_elim
State after:
no goals

State before:
H : Type ?u.100787
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✝
ih₁ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
ih₂ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
ih₃ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝
Tactic:
apply orE <;> solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply botE
State after:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ bot

State before:
case a
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ bot
Tactic:
solve_by_elim [insert_subset_insert]
State after:
no goals