Theorem: equivOfLiftRelToEquivRight_rel_right (Controlbits/Extras/isLeft_invariant.lean)

State before:
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
he : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
b : β₁
⊢ rb ((equivOfLiftRelToEquivRight he) b) b
Tactic:
simp only [equivOfLiftRelToEquivRight_apply, ← liftRel_inr_inr (r := ra) (s := rb),
  inr_getRight, he]
State after:
no goals