Theorem: Smt.Reconstruct.Prop.orAssocConv (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₁ => cases h₁ with
            | inl h₃ => exact Or.inl h₃
            | inr h₄ => exact (Or.inr (Or.inl h₄))
| inr h₂ => exact Or.inr (Or.inr h₂)
State after:
no goals

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

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

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

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