Theorem: Sum.isLeft_eq_of_liftRel_inl_left (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
a : α✝¹
cd : α✝ ⊕ β✝
h : LiftRel ra rb (inl a) cd
⊢ cd.isLeft = true
Tactic:
cases h
State after:
case inl
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
a : α✝¹
c✝ : α✝
a✝ : ra a c✝
⊢ (inl c✝).isLeft = true

State before:
case inl
α : Type u
β : Type v
α✝¹ : Type u_1
α✝ : Type u_2
ra : α✝¹ → α✝ → Prop
β✝¹ : Type u_3
β✝ : Type u_4
rb : β✝¹ → β✝ → Prop
a : α✝¹
c✝ : α✝
a✝ : ra a c✝
⊢ (inl c✝).isLeft = true
Tactic:
simp
State after:
no goals