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

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