Theorem: Sum.isLeft_eq_of_liftRel_inl_right (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 : α✝ ⊕ β✝
c : γ✝
h : LiftRel ra rb ab (inl c)
⊢ ab.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
c : γ✝
a✝¹ : α✝
a✝ : ra a✝¹ c
⊢ (inl a✝¹).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
c : γ✝
a✝¹ : α✝
a✝ : ra a✝¹ c
⊢ (inl a✝¹).isLeft = true
Tactic:
simp
State after:
no goals