Theorem: LO.FirstOrder.provable_iff_of_consistent_of_complete (Logic/FirstOrder/Incompleteness/FirstIncompleteness.lean)

State before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
⊢ T ⊢! σ → ¬T ⊢! ~σ
Tactic:
rintro ⟨b₁⟩ ⟨b₂⟩
State after:
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False

State before:
case intro.intro
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
b₁ : T ⊢ σ
b₂ : T ⊢ ~σ
⊢ False
Tactic:
exact (Gentzen.inconsistent_of_provable_and_refutable b₁ b₂).not_con consis
State after:
no goals

State before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
⊢ ¬T ⊢! ~σ → T ⊢! σ
Tactic:
intro h
State after:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
h : ¬T ⊢! ~σ
⊢ T ⊢! σ

State before:
L : Language
σ : Sentence L
T : Theory L
consis : System.Consistent T
comp : System.Complete T
h : ¬T ⊢! ~σ
⊢ T ⊢! σ
Tactic:
exact or_iff_not_imp_right.mp (comp σ) h
State after:
no goals