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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂ → ¬(L)-Consistent (T₁ ∪ T₂)
Tactic:
contrapose
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬¬(L)-Consistent (T₁ ∪ T₂) → ¬(¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬¬(L)-Consistent (T₁ ∪ T₂) → ¬(¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂)
Tactic:
push_neg
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂
Tactic:
exact union_ParametricConsistent
State after:
no goals