Theorem: LO.Gentzen.inconsistent_of_provable_and_refutable! (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
bp : 𝓣 ⊢! p
br : 𝓣 ⊢! ~p
⊢ System.Inconsistent 𝓣
Tactic:
rcases bp with ⟨bp⟩
State after:
case intro
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
br : 𝓣 ⊢! ~p
bp : 𝓣 ⊢ p
⊢ System.Inconsistent 𝓣

State before:
case intro
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
br : 𝓣 ⊢! ~p
bp : 𝓣 ⊢ p
⊢ System.Inconsistent 𝓣
Tactic:
rcases br with ⟨br⟩
State after:
case intro.intro
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
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
⊢ System.Inconsistent 𝓣

State before:
case intro.intro
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
bp : 𝓣 ⊢ p
br : 𝓣 ⊢ ~p
⊢ System.Inconsistent 𝓣
Tactic:
exact inconsistent_of_provable_and_refutable bp br
State after:
no goals