Theorem: ClassicalPropositionalLogic.weakening (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
Tactic:
induction h generalizing Δ
State after:
case ax
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case impI
v : Variable → Prop
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
v : Variable → Prop
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
v : Variable → Prop
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
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case andE2
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case orI1
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orI2
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orE
v : Variable → Prop
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 botC
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
a_ih✝ : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

State before:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
case botC ih => apply botC; solve_by_elim [insert_subset_insert]
State after:
no goals

State before:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply ax
State after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ

State before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ A✝ ∈ Δ
Tactic:
solve_by_elim
State after:
no goals

State before:
v : Variable → Prop
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
v : Variable → Prop
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
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
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
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

State before:
case a
v : Variable → Prop
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:
v : Variable → Prop
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
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
ih : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

State before:
case a
v : Variable → Prop
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:
v : Variable → Prop
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:
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝
Tactic:
apply botC
State after:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert (~A✝) Δ ⊢ ⊥

State before:
case a
v : Variable → Prop
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : insert (~A✝) Γ✝ ⊢ ⊥
ih : ∀ {Δ : Set Formula}, insert (~A✝) Γ✝ ⊆ Δ → Δ ⊢ ⊥
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ insert (~A✝) Δ ⊢ ⊥
Tactic:
solve_by_elim [insert_subset_insert]
State after:
no goals