Theorem: Sinf.contradiction_yields_anything (SInfinity/Lemmas.lean)

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

State before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
have iβ := S_inr β contr
State after:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β

State before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
have s_return := S_in iβ
State after:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β

State before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
⊢ Δ ⋁ β
Tactic:
cases S_de_morgan_inv s_return
State after:
case intro
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
left✝ : β :: Δ ⋁ ¬ₛ α
right✝ : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β

State before:
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β
Tactic:
apply S_contraction
State after:
case a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ β

State before:
case a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ β
Tactic:
apply S_section (¬ₛ α)
State after:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ ¬ₛ α

case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ ¬ₛ ¬ₛ α ∨ₛ β

State before:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ β ∨ₛ ¬ₛ α
Tactic:
apply S_out
State after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ α

State before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ α
Tactic:
assumption
State after:
no goals

State before:
case a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ ¬ₛ ¬ₛ α ∨ₛ β
Tactic:
apply S_out
State after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ (¬ₛ ¬ₛ α) :: Δ ⋁ β

State before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ (¬ₛ ¬ₛ α) :: Δ ⋁ β
Tactic:
apply S_exchange_ctx
State after:
case a.a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ ¬ₛ α

State before:
case a.a.a.a
α β : Sinf
Δ : Ctx Sinf
contr : Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
iβ : Δ ⋁ β ∨ₛ ¬ₛ (α ∨ₛ ¬ₛ α)
s_return : β :: Δ ⋁ ¬ₛ (α ∨ₛ ¬ₛ α)
n : β :: Δ ⋁ ¬ₛ α
nn : β :: Δ ⋁ ¬ₛ ¬ₛ α
⊢ β :: Δ ⋁ ¬ₛ ¬ₛ α
Tactic:
assumption
State after:
no goals