Theorem: equivIsRightInvariant_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).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), LiftRel ⊤ ⊤ (e ab) ab
Tactic:
rw [← equivIsLeftInvariant_iff_liftRel_top_top]
State after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ (∀ (ab : α₁ ⊕ β₁), (e ab).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft

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).isRight = ab.isRight) ↔ ∀ (ab : α₁ ⊕ β₁), (e ab).isLeft = ab.isLeft
Tactic:
simp_rw [Sum.forall]
State after:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), (e (inl a)).isRight = (inl a).isRight) ∧ ∀ (b : β₁), (e (inr b)).isRight = (inr b).isRight) ↔
    (∀ (a : α₁), (e (inl a)).isLeft = (inl a).isLeft) ∧ ∀ (b : β₁), (e (inr b)).isLeft = (inr b).isLeft

State before:
α₁ : Type u_2
β₁ : Type u_1
α₂ : Type u_4
β₂ : Type u_3
e✝ : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
ra : α₂ → α₁ → Prop
rb : β₂ → β₁ → Prop
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
e : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
⊢ ((∀ (a : α₁), (e (inl a)).isRight = (inl a).isRight) ∧ ∀ (b : β₁), (e (inr b)).isRight = (inr b).isRight) ↔
    (∀ (a : α₁), (e (inl a)).isLeft = (inl a).isLeft) ∧ ∀ (b : β₁), (e (inr b)).isLeft = (inr b).isLeft
Tactic:
simp_rw  [isRight_inl, isRight_eq_false, isRight_inr, isLeft_inl, isLeft_inr, isLeft_eq_false]
State after:
no goals