Theorem: Sum.isLeft_eq_of_liftRel (Controlbits/Extras/isLeft_invariant.lean)

State before:
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
ab : α✝¹ ⊕ β✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb ab cd
⊢ ab.isLeft = cd.isLeft
Tactic:
cases h <;> simp
State after:
no goals