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

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

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

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

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