Theorem: sumCongrEquivLiftRelLeftRight_eq_self (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
⊢ (equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he) = e
Tactic:
ext ab
State after:
case H
α₁ : 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
ab : α₁ ⊕ β₁
⊢ ((equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he)) ab = e ab

State before:
case H
α₁ : 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
ab : α₁ ⊕ β₁
⊢ ((equivOfLiftRelToEquivLeft he).sumCongr (equivOfLiftRelToEquivRight he)) ab = e ab
Tactic:
cases ab <;> simp [he]
State after:
no goals