Theorem: Sum.liftRel_equiv_left_iff_symm_right (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 : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ LiftRel ra rb cd (e.symm cd)
Tactic:
convert (H (e.symm cd))
State after:
case h.e'_7
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ cd = e (e.symm cd)

State before:
case h.e'_7
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (ab : α₁ ⊕ β₁), LiftRel ra rb (e ab) ab
cd : α₂ ⊕ β₂
⊢ cd = e (e.symm cd)
Tactic:
exact (e.apply_symm_apply _).symm
State after:
no goals

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

State before:
case h.e'_8
α : Type u
β : Type v
α₁ : Type u_1
β₁ : Type u_2
α₂ : Type u_3
β₂ : Type u_4
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
H : ∀ (cd : α₂ ⊕ β₂), LiftRel ra rb cd (e.symm cd)
ab : α₁ ⊕ β₁
⊢ ab = e.symm (e ab)
Tactic:
exact (e.symm_apply_apply _).symm
State after:
no goals