Theorem: LO.System.inconsistent_compact (Logic/Logic/System.lean)

State before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕
Tactic:
rcases Compact.finite_provable (H ⊥) with ⟨𝓕, h𝓕, fin, h⟩
State after:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
fin : Collection.Finite 𝓕
h : 𝓕 ⊢! ⊥
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕

State before:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
H : Inconsistent 𝓢
𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
fin : Collection.Finite 𝓕
h : 𝓕 ⊢! ⊥
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕
Tactic:
exact ⟨𝓕, h𝓕, fin, inconsistent_of_provable h⟩
State after:
no goals

State before:
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 : S
⊢ (∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ Inconsistent 𝓕) → Inconsistent 𝓢
Tactic:
rintro ⟨𝓕, h𝓕, _, H⟩
State after:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
left✝ : Collection.Finite 𝓕
H : Inconsistent 𝓕
⊢ Inconsistent 𝓢

State before:
case intro.intro.intro
S : Type u_1
F : Type u_2
inst✝⁵ : LogicalConnective F
inst✝⁴ : System F S
inst✝³ : DeductiveExplosion S
inst✝² : Collection F S
inst✝¹ : Axiomatized S
inst✝ : Compact S
𝓢 𝓕 : S
h𝓕 : 𝓕 ⊆ 𝓢
left✝ : Collection.Finite 𝓕
H : Inconsistent 𝓕
⊢ Inconsistent 𝓢
Tactic:
exact H.of_supset h𝓕
State after:
no goals