Theorem: LO.FirstOrder.Derivation.iff_cut (Logic/FirstOrder/Hauptsatz.lean)

State before:
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
⊢ Nonempty { d // CutFree d } → ⊢¹! Δ
Tactic:
rintro ⟨d⟩
State after:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d : { d // CutFree d }
⊢  ⊢¹! Δ

State before:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d : { d // CutFree d }
⊢  ⊢¹! Δ
Tactic:
exact ⟨d⟩
State after:
no goals

State before:
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
⊢  ⊢¹! Δ → Nonempty { d // CutFree d }
Tactic:
rintro ⟨d⟩
State after:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d :  ⊢¹ Δ
⊢ Nonempty { d // CutFree d }

State before:
case intro
L✝ : Language
inst✝¹ : (k : ℕ) → DecidableEq (L✝.Func k)
inst✝ : (k : ℕ) → DecidableEq (L✝.Rel k)
C : Set (SyntacticFormula L✝)
hC : ∀ (f : ℕ → Semiterm L✝ ℕ 0), ∀ p ∈ C, (Rew.rewrite f).hom p ∈ C
Δ✝ Δ₁ Δ₂ Γ : Sequent L✝
L : Language
Δ : Sequent L
this : (α : Sort ?u.2461882) → DecidableEq α
d :  ⊢¹ Δ
⊢ Nonempty { d // CutFree d }
Tactic:
exact ⟨hauptsatz d⟩
State after:
no goals