Theorem: LO.Gentzen.refutable_iff_inconsistent (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
p : F
⊢ 𝓣 ⊢! ~p → System.Inconsistent (cons p 𝓣)
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ System.Inconsistent (cons p 𝓣)

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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ System.Inconsistent (cons p 𝓣)
Tactic:
simp [inconsistent_iff_nonempty]
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ Nonempty (cons p 𝓣 ⊢' [])

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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ Nonempty (cons p 𝓣 ⊢' [])
Tactic:
exact ⟨⟨p :: Δ, by simp; intro q hq; right; exact h q hq, ofNegRight d⟩⟩
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ p_1 ∈ p :: Δ, p_1 ∈ cons p 𝓣
Tactic:
simp
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ 𝓣

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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
⊢ ∀ a ∈ Δ, a = p ∨ a ∈ 𝓣
Tactic:
intro q hq
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q = p ∨ q ∈ 𝓣

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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q = p ∨ q ∈ 𝓣
Tactic:
right
State after:
case h
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣

State before:
case h
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
p : F
Δ : List F
h : ∀ p ∈ Δ, p ∈ 𝓣
d : Δ ⊢² [~p]
q : F
hq : q ∈ Δ
⊢ q ∈ 𝓣
Tactic:
exact h q hq
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
p : F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p
Tactic:
letI := Classical.typeDecidableEq F
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
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p

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
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ System.Inconsistent (cons p 𝓣) → 𝓣 ⊢! ~p
Tactic:
simp [inconsistent_iff_nonempty]
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
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons p 𝓣 ⊢' [] → 𝓣 ⊢! ~p

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
p : F
this : DecidableEq F := Classical.typeDecidableEq F
⊢ cons p 𝓣 ⊢' [] → 𝓣 ⊢! ~p
Tactic:
exact fun b ↦ ⟨b.deduction⟩
State after:
no goals