Theorem: Set.bijOn_empty_iff_right (Matroid/ForMathlib/Function.lean)

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
h : BijOn f ∅ t
⊢ t = ∅
Tactic:
simpa using h.surjOn
State after:
no goals

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t✝ t' t₁ t₂ : Set β
f✝ f : α → β
t : Set β
⊢ t = ∅ → BijOn f ∅ t
Tactic:
rintro rfl
State after:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅

State before:
α : Type u_1
β : Type u_2
r s s₁ s₂ : Set α
t t' t₁ t₂ : Set β
f✝ f : α → β
⊢ BijOn f ∅ ∅
Tactic:
exact bijOn_empty f
State after:
no goals