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

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

State before:
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ R ∨ Q
Tactic:
apply orComm
State after:
case a
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ Q ∨ R

State before:
case a
P Q R : Prop
h₁ : P → Q
h₂ : R ∨ P
⊢ Q ∨ R
Tactic:
exact congOrRight h₁ (orComm h₂)
State after:
no goals