Theorem: Sum.liftRel_equiv_right_iff_symm_left (Controlbits/Extras/isLeft_invariant.lean)

State before:
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), LiftRel ra rb ab (e ab)) ↔ ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb (e.symm cd) cd
Tactic:
convert liftRel_equiv_left_iff_symm_right.symm
State after:
case h.e'_1.h.h.e'_8.h.e'_5
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
a✝ : α₁ ⊕ β₁
⊢ e = e.symm.symm

State before:
case h.e'_1.h.h.e'_8.h.e'_5
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₁ → α₂ → Prop
rb : β₁ → β₂ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
a✝ : α₁ ⊕ β₁
⊢ e = e.symm.symm
Tactic:
exact e.symm_symm
State after:
no goals