Theorem: S_assoc (SInfinity/Lemmas.lean)

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

State before:
α β γ : Sinf
Δ : Ctx Sinf
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ ↔ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
constructor <;> intros h
State after:
case mp
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)

case mpr
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ

State before:
case mp
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
apply S_out
State after:
case mp.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ α :: Δ ⋁ β ∨ₛ γ

State before:
case mp.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ α :: Δ ⋁ β ∨ₛ γ
Tactic:
apply S_out
State after:
case mp.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ β :: α :: Δ ⋁ γ

State before:
case mp.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ β :: α :: Δ ⋁ γ
Tactic:
apply S_split
State after:
case mp.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ (α ∨ₛ β) :: Δ ⋁ γ

State before:
case mp.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Tactic:
apply S_in
State after:
case mp.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ

State before:
case mp.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ β ∨ₛ γ
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Tactic:
assumption
State after:
no goals

State before:
case mpr
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ β ∨ₛ γ
Tactic:
apply S_out
State after:
case mpr.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ (α ∨ₛ β) :: Δ ⋁ γ

State before:
case mpr.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ (α ∨ₛ β) :: Δ ⋁ γ
Tactic:
apply S_join
State after:
case mpr.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ β :: α :: Δ ⋁ γ

State before:
case mpr.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ β :: α :: Δ ⋁ γ
Tactic:
apply S_in
State after:
case mpr.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ α :: Δ ⋁ β ∨ₛ γ

State before:
case mpr.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ α :: Δ ⋁ β ∨ₛ γ
Tactic:
apply S_in
State after:
case mpr.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)

State before:
case mpr.a.a.a.a
α β γ : Sinf
Δ : Ctx Sinf
h : Δ ⋁ α ∨ₛ (β ∨ₛ γ)
⊢ Δ ⋁ α ∨ₛ (β ∨ₛ γ)
Tactic:
assumption
State after:
no goals