Theorem: S_de_morgan_inv (SInfinity/Lemmas.lean)

State before:
⊢ ∀ {α β : Sinf} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ (α ∨ₛ β) → (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
intros α β Δ d
State after:
α β : Sinf
Δ : Ctx Sinf
d : Δ ⋁ ¬ₛ (α ∨ₛ β)
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)

State before:
α β : Sinf
Δ : Ctx Sinf
d : Δ ⋁ ¬ₛ (α ∨ₛ β)
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
cases d
State after:
case S_weakening
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)

case S_de_morgan
α β : Sinf
Δ : Ctx Sinf
a✝¹ : Δ ⋁ ¬ₛ α
a✝ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)

State before:
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)
Tactic:
case S_weakening ne => exact And.intro (S_weakening (¬ₛ α) ne) (S_weakening (¬ₛ β) ne)
State after:
no goals

State before:
α β : Sinf
Δ : Ctx Sinf
nα : Δ ⋁ ¬ₛ α
nβ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
case S_de_morgan nα nβ => exact And.intro nα nβ
State after:
no goals

State before:
α β δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ (δ✝ :: Δ✝ ⋁ ¬ₛ α) ∧ (δ✝ :: Δ✝ ⋁ ¬ₛ β)
Tactic:
exact And.intro (S_weakening (¬ₛ α) ne) (S_weakening (¬ₛ β) ne)
State after:
no goals

State before:
α β : Sinf
Δ : Ctx Sinf
nα : Δ ⋁ ¬ₛ α
nβ : Δ ⋁ ¬ₛ β
⊢ (Δ ⋁ ¬ₛ α) ∧ (Δ ⋁ ¬ₛ β)
Tactic:
exact And.intro nα nβ
State after:
no goals