Theorem: Sum.isRight_eq_of_liftRel_inr_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 : α✝ ⊕ β✝
d : δ✝
h : LiftRel ra rb ab (inr d)
⊢ ab.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
d : δ✝
b✝ : β✝
a✝ : rb b✝ d
⊢ (inr b✝).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
d : δ✝
b✝ : β✝
a✝ : rb b✝ d
⊢ (inr b✝).isRight = true
Tactic:
simp
State after:
no goals