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

State before:
α₁ : Type u_2
β₁ : Type u_4
α₂ : Type u_1
β₂ : Type u_3
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
hea : ∀ (a : α₁), ra (ea a) a
heb : ∀ (b : β₁), rb (eb b) b
ab : α₁ ⊕ β₁
⊢ LiftRel ra rb ((ea.sumCongr eb) ab) ab
Tactic:
cases ab <;> simp [hea, heb]
State after:
no goals