Theorem: LO.Modal.Standard.Theory.not_mem_falsum_of_Lconsistent (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
⊢ ⊥ ∉ T
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
⊢ False
Tactic:
have : L ⊬! ⊥ ⟶ ⊥ := consisT (Γ := [⊥]) (by simpa)
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this : L ⊬! ⊥ ⟶ ⊥
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this : L ⊬! ⊥ ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! ⊥ ⟶ ⊥ := efq!
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this✝ : L ⊬! ⊥ ⟶ ⊥
this : L ⊢! ⊥ ⟶ ⊥
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
this✝ : L ⊬! ⊥ ⟶ ⊥
this : L ⊢! ⊥ ⟶ ⊥
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
hC : ⊥ ∈ T
⊢ ∀ p ∈ [⊥], p ∈ T
Tactic:
simpa
State after:
no goals