Theorem: LO.Gentzen.provable_iff (Logic/Logic/Calculus.lean)

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ 𝓣 ⊢! p → ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
rintro ⟨b⟩
State after:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]

State before:
case intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
rcases proofEquivDerivation b with ⟨Δ, d⟩
State after:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
Δ : { Δ // ∀ π ∈ Δ, π ∈ 𝓣 }
d : ↑Δ ⊢² [p]
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]

State before:
case intro.mk
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
b : 𝓣 ⊢ p
Δ : { Δ // ∀ π ∈ Δ, π ∈ 𝓣 }
d : ↑Δ ⊢² [p]
⊢ ∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]
Tactic:
exact ⟨Δ, Δ.prop, ⟨d⟩⟩
State after:
no goals

State before:
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
⊢ (∃ Δ, (∀ π ∈ Δ, π ∈ 𝓣) ∧ Δ ⊢²! [p]) → 𝓣 ⊢! p
Tactic:
rintro ⟨Δ, h, ⟨d⟩⟩
State after:
case intro.intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ π ∈ Δ, π ∈ 𝓣
d : Δ ⊢² [p]
⊢ 𝓣 ⊢! p

State before:
case intro.intro.intro
F : Type u_1
inst✝³ : LogicalConnective F
inst✝² : Gentzen F
inst✝¹ : Cut F
Γ Δ✝ E : List F
S : Type u_2
inst✝ : Collection F S
𝓣 : S
p : F
Δ : List F
h : ∀ π ∈ Δ, π ∈ 𝓣
d : Δ ⊢² [p]
⊢ 𝓣 ⊢! p
Tactic:
exact ⟨proofEquivDerivation.symm ⟨⟨Δ, h⟩, d⟩⟩
State after:
no goals