Theorem: LO.Gentzen.consistent_iff_isEmpty (Logic/Logic/Calculus.lean)

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ System.Consistent 𝓣 → IsEmpty (𝓣 ⊢' [])
Tactic:
contrapose
State after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬IsEmpty (𝓣 ⊢' []) → ¬System.Consistent 𝓣

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬IsEmpty (𝓣 ⊢' []) → ¬System.Consistent 𝓣
Tactic:
simp [System.Consistent, System.not_consistent_iff_inconsistent, System.inconsistent_iff_provable_bot]
State after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢' [] → 𝓣 ⊢! ⊥

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢' [] → 𝓣 ⊢! ⊥
Tactic:
intro b
State after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ 𝓣 ⊢! ⊥

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ 𝓣 ⊢! ⊥
Tactic:
exact ⟨b.wk (by simp)⟩
State after:
no goals

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
b : 𝓣 ⊢' []
⊢ [] ⊆ [⊥]
Tactic:
simp
State after:
no goals

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ IsEmpty (𝓣 ⊢' []) → System.Consistent 𝓣
Tactic:
contrapose
State after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬System.Consistent 𝓣 → ¬IsEmpty (𝓣 ⊢' [])

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ ¬System.Consistent 𝓣 → ¬IsEmpty (𝓣 ⊢' [])
Tactic:
simp [System.Consistent, System.not_consistent_iff_inconsistent, System.inconsistent_iff_provable_bot]
State after:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢! ⊥ → Nonempty (𝓣 ⊢' [])

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
⊢ 𝓣 ⊢! ⊥ → Nonempty (𝓣 ⊢' [])
Tactic:
rintro ⟨Δ, h, d⟩
State after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
⊢ Nonempty (𝓣 ⊢' [])

State before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
⊢ Nonempty (𝓣 ⊢' [])
Tactic:
have : Δ ⊢² [] := Cut.cut d (falsum _ _)
State after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
this : Δ ⊢² []
⊢ Nonempty (𝓣 ⊢' [])

State before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [⊥]
this : Δ ⊢² []
⊢ Nonempty (𝓣 ⊢' [])
Tactic:
exact ⟨toDisjconseq this h⟩
State after:
no goals