Theorem: Smt.Reconstruct.Prop.orAssocDir (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ {P Q R : Prop}, P ∨ Q ∨ R → (P ∨ Q) ∨ R
Tactic:
intros P Q R h
State after:
P Q R : Prop
h : P ∨ Q ∨ R
⊢ (P ∨ Q) ∨ R

State before:
P Q R : Prop
h : P ∨ Q ∨ R
⊢ (P ∨ Q) ∨ R
Tactic:
cases h with
| inl h₁ => exact Or.inl (Or.inl h₁)
| inr h₂ => cases h₂ with
            | inl h₃ => exact Or.inl (Or.inr h₃)
            | inr h₄ => exact Or.inr h₄
State after:
no goals

State before:
case inl
P Q R : Prop
h₁ : P
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inl (Or.inl h₁)
State after:
no goals

State before:
case inr
P Q R : Prop
h₂ : Q ∨ R
⊢ (P ∨ Q) ∨ R
Tactic:
cases h₂ with
| inl h₃ => exact Or.inl (Or.inr h₃)
| inr h₄ => exact Or.inr h₄
State after:
no goals

State before:
case inr.inl
P Q R : Prop
h₃ : Q
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inl (Or.inr h₃)
State after:
no goals

State before:
case inr.inr
P Q R : Prop
h₄ : R
⊢ (P ∨ Q) ∨ R
Tactic:
exact Or.inr h₄
State after:
no goals