Theorem: equivOfLiftRelToEquivLeft_rel_left (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
a : α₁
⊢ ra ((equivOfLiftRelToEquivLeft he) a) a
Tactic:
simp only [equivOfLiftRelToEquivLeft_apply, ← liftRel_inl_inl (r := ra) (s := rb),
  inl_getLeft, he]
State after:
no goals