Theorem: LO.System.Context.provable_iff (Logic/Logic/HilbertStyle/Context.lean)

State before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ Γ *⊢[𝓢]! p → ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
Tactic:
rintro ⟨⟨Δ, h, b⟩⟩
State after:
case intro.mk
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ { ctx := Γ }
b : Δ ⊢[𝓢] p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p

State before:
case intro.mk
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ { ctx := Γ }
b : Δ ⊢[𝓢] p
⊢ ∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p
Tactic:
exact ⟨Δ, h, ⟨b⟩⟩
State after:
no goals

State before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
⊢ (∃ Δ, (∀ q ∈ Δ, q ∈ Γ) ∧ Δ ⊢[𝓢]! p) → Γ *⊢[𝓢]! p
Tactic:
rintro ⟨Δ, h, ⟨d⟩⟩
State after:
case intro.intro.intro
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ Γ
d : { ctx := Δ } ⊢ p
⊢ Γ *⊢[𝓢]! p

State before:
case intro.intro.intro
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
Γ : Set F
p : F
Δ : List F
h : ∀ q ∈ Δ, q ∈ Γ
d : { ctx := Δ } ⊢ p
⊢ Γ *⊢[𝓢]! p
Tactic:
exact ⟨⟨Δ, h, d⟩⟩
State after:
no goals