Theorem: LO.System.Compact.finite_provable (Logic/Logic/System.lean)

State before:
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
h : 𝓢 ⊢! f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f
Tactic:
rcases h with ⟨b⟩
State after:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
b : 𝓢 ⊢ f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f

State before:
case intro
F : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
inst✝⁶ : System F S
inst✝⁵ : System F T
inst✝⁴ : System F U
inst✝³ : Collection F S
inst✝² : Collection F T
inst✝¹ : Axiomatized S
inst✝ : Compact S
f : F
𝓢 : S
b : 𝓢 ⊢ f
⊢ ∃ 𝓕 ⊆ 𝓢, Collection.Finite 𝓕 ∧ 𝓕 ⊢! f
Tactic:
exact ⟨φ b, φ_subset b, φ_finite b, ⟨φPrf b⟩⟩
State after:
no goals