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

State before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft) ↔ ∀ (ab : α₁ ⊕ β₁), LiftRel ⊤ ⊤ (e ab) ab
Tactic:
simp_rw  [Sum.forall, isLeft_inl, isLeft_inr, isLeft_eq_false, isLeft_iff, isRight_iff]
State after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), ∃ y, e (inl a) = inl y) ∧ ∀ (b : β₁), ∃ y, e (inr b) = inr y) ↔
    (∀ (a : α₁), LiftRel ⊤ ⊤ (e (inl a)) (inl a)) ∧ ∀ (b : β₁), LiftRel ⊤ ⊤ (e (inr b)) (inr b)

State before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), ∃ y, e (inl a) = inl y) ∧ ∀ (b : β₁), ∃ y, e (inr b) = inr y) ↔
    (∀ (a : α₁), LiftRel ⊤ ⊤ (e (inl a)) (inl a)) ∧ ∀ (b : β₁), LiftRel ⊤ ⊤ (e (inr b)) (inr b)
Tactic:
exact ⟨fun ⟨hA, hB⟩ => ⟨fun a => (hA a).elim (fun _ h => h ▸ LiftRel.inl (trivial)),
                        fun b => (hB b).elim (fun _ h => h ▸ LiftRel.inr (trivial))⟩,
        fun ⟨hA, hB⟩ => ⟨fun a => isLeft_iff.mp (isLeft_eq_of_liftRel (hA a)),
                        fun b => isRight_iff.mp (isRight_eq_of_liftRel (hB b))⟩⟩
State after:
no goals