Theorem: LO.Modal.Standard.Theory.union_ParametricConsistent (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₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂
Tactic:
simp only [ParametricConsistent]
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥) →
    (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
      ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥) →
    (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
      ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro h
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
    ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
    ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥

State before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
. intro Γ hΓ; exact h (by intro p hp; simp; left; exact hΓ p hp);
State after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥

State before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
. intro Γ hΓ; exact h (by intro p hp; simp; right; exact hΓ p hp);
State after:
no goals

State before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ hΓ
State after:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ L ⊬! Γ.conj' ⟶ ⊥

State before:
case left
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
exact h (by intro p hp; simp; left; exact hΓ p hp)
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
⊢ ∀ p ∈ Γ, p ∈ T₁ ∪ T₂
Tactic:
intro p hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Tactic:
simp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Tactic:
left
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₁
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁
Tactic:
exact hΓ p hp
State after:
no goals

State before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ hΓ
State after:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ L ⊬! Γ.conj' ⟶ ⊥

State before:
case right
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ L ⊬! Γ.conj' ⟶ ⊥
Tactic:
exact h (by intro p hp; simp; right; exact hΓ p hp)
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
⊢ ∀ p ∈ Γ, p ∈ T₁ ∪ T₂
Tactic:
intro p hp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∪ T₂
Tactic:
simp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₁ ∨ p ∈ T₂
Tactic:
right
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₂

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T₂
p : Formula α
hp : p ∈ Γ
⊢ p ∈ T₂
Tactic:
exact hΓ p hp
State after:
no goals