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

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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ L ⊬! Δ.conj' ⟶ ⊥
Tactic:
have := @h Δ₁ Δ₂ (by intro _ h; simpa using List.of_mem_filter h;) (by intro _ h; simpa using List.of_mem_filter h;)
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊬! Δ.conj' ⟶ ⊥

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊬! Δ.conj' ⟶ ⊥
Tactic:
exact unprovable_imp_trans! (by
  apply FiniteContext.deduct'!;
  apply iff_provable_list_conj.mpr;
  intro q hq;
  cases (hΔ q hq);
  . exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
  . exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
) this
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ ∀ p ∈ Δ₁, p ∈ T₁
Tactic:
intro _ h
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₁
⊢ p✝ ∈ T₁

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₁
⊢ p✝ ∈ T₁
Tactic:
simpa using List.of_mem_filter h
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
⊢ ∀ p ∈ Δ₂, p ∈ T₂
Tactic:
intro _ h
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₂
⊢ p✝ ∈ T₂

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h✝ : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
p✝ : Formula α
h : p✝ ∈ Δ₂
⊢ p✝ ∈ T₂
Tactic:
simpa using List.of_mem_filter h
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ L ⊢! Δ₁.conj' ⋏ Δ₂.conj' ⟶ Δ.conj'
Tactic:
apply FiniteContext.deduct'!
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ [Δ₁.conj' ⋏ Δ₂.conj'] ⊢[L]! Δ.conj'

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ [Δ₁.conj' ⋏ Δ₂.conj'] ⊢[L]! Δ.conj'
Tactic:
apply iff_provable_list_conj.mpr
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ ∀ p ∈ Δ, { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! p

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
⊢ ∀ p ∈ Δ, { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! p
Tactic:
intro q hq
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
cases (hΔ q hq)
State after:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

State before:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
. exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
State after:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q

State before:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
. exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa);
State after:
no goals

State before:
case h.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
exact iff_provable_list_conj.mp (conj₁'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa)
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₁
⊢ decide (q ∈ T₁) = true
Tactic:
simpa
State after:
no goals

State before:
case h.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ { ctx := [Δ₁.conj' ⋏ Δ₂.conj'] } ⊢! q
Tactic:
exact iff_provable_list_conj.mp (conj₂'! FiniteContext.id!) q $ List.mem_filter_of_mem hq (by simpa)
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
T₁ T₂ : Theory α
h : ∀ {Γ₁ Γ₂ : List (Formula α)}, (∀ p ∈ Γ₁, p ∈ T₁) → (∀ p ∈ Γ₂, p ∈ T₂) → L ⊬! Γ₁.conj' ⋏ Γ₂.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ T₁ ∨ p ∈ T₂
Δ₁ : List (Formula α) := List.filter (fun x => decide (x ∈ T₁)) Δ
Δ₂ : List (Formula α) := List.filter (fun x => decide (x ∈ T₂)) Δ
this : L ⊬! Δ₁.conj' ⋏ Δ₂.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Δ
h✝ : q ∈ T₂
⊢ decide (q ∈ T₂) = true
Tactic:
simpa
State after:
no goals