awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Subsingleton β
inst_1 : Nonempty β
intro : ∀ (val : Unique β), SurjOn f s univ ↔ s.Nonempty
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
cases nonempty_unique β

Premises used: nonempty_unique
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Subsingleton β
inst_1 : Nonempty β
val : Unique β
⊢ SurjOn f s univ ↔ s.Nonempty

Tactic:
simp [univ_unique, Subsingleton.elim (f _) default, Set.Nonempty]

Premises used: Inhabited.default, Set.Nonempty, Subsingleton.elim, Set.univ_unique
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ SurjOn f s (f '' s)

Tactic:
Subset.rfl

Premises used: Set.SurjOn, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
ht : t.Nonempty
⊢ s.Nonempty

Tactic:
(ht.mono h).of_image

Premises used: Set.Nonempty.mono, Set.Nonempty.of_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
by_contra! : ∀ (this : s = ∅ ∧ t.Nonempty), False
⊢ s.Nonempty ∨ t = ∅

Tactic:
by_contra!
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
this : s = ∅ ∧ t.Nonempty
⊢ False

Tactic:
(h.comap_nonempty this.2).ne_empty this.1

Premises used: Set.Nonempty.ne_empty, And.right, And.left, Set.SurjOn.comap_nonempty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
this : s = ∅ ∧ t.Nonempty
⊢ False

Tactic:
exact (h.comap_nonempty this.2).ne_empty this.1

Premises used: Set.Nonempty.ne_empty, And.right, And.left, Set.SurjOn.comap_nonempty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
rwa : t ⊆ f₂ '' s
rwa₁ rwa₂ rwa₃ rwa₄ : t ⊆ f₁ '' s
⊢ SurjOn f₂ s t

Tactic:
rwa [SurjOn, ← H.image_eq]

Premises used: Set.SurjOn, Set.EqOn.image_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : EqOn f₁ f₂ s
⊢ SurjOn f₁ s t ↔ SurjOn f₂ s t

Tactic:
⟨fun H => H.congr h, fun H => H.congr h.symm⟩

Premises used: Set.SurjOn.congr, Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
hf : SurjOn f s₁ t₂
⊢ SurjOn f s₂ t₁

Tactic:
Subset.trans ht <| Subset.trans hf <| image_mono hs

Premises used: Set.Subset.trans, Set.image_mono, Set.SurjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s t₁
h₂ : SurjOn f s t₂
⊢ SurjOn f s (t₁ ∪ t₂)

Tactic:
fun _ hx =>
  hx.elim (fun hx => h₁ hx) fun hx => h₂ hx

Premises used: Set.SurjOn, Set.Subset, Or.elim
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
⊢ SurjOn f (s₁ ∪ s₂) (t₁ ∪ t₂)

Tactic:
(h₁.mono subset_union_left (Subset.refl _)).union
    (h₂.mono subset_union_right (Subset.refl _))

Premises used: Set.Subset.refl, Set.SurjOn.mono, Set.subset_union_right, Set.subset_union_left, Set.SurjOn.union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
rcases : ∀ (x₁ : α) (hx₁ : x₁ ∈ s₁) (hy : f x₁ ∈ t₁ ∩ t₂), f x₁ ∈ f '' (s₁ ∩ s₂)
⊢ y ∈ f '' (s₁ ∩ s₂)

Tactic:
rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩

Premises used: And.left, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
rcases : ∀ (x₂ : α) (hx₂ : x₂ ∈ s₂) (heq : f x₂ = f x₁), f x₁ ∈ f '' (s₁ ∩ s₂)
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩

Premises used: And.right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ x₁ = x₂

Tactic:
h (Or.inl hx₁) (Or.inr hx₂) heq.symm

Premises used: Or.inl, Eq.symm, Or.inr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ x₁ ∈ s₂

Tactic:
obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm

Premises used: Or.inl, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
hx₃ : x₁ ∈ s₂
⊢ f x₁ = f x₁

Tactic:
obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm

Premises used: Or.inl, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
mem_image_of_mem f ⟨hx₁, hx₂⟩

Premises used: Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
hx₂ : x₁ ∈ s₂
heq : f x₁ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)

Tactic:
exact mem_image_of_mem f ⟨hx₁, hx₂⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
f : α → β
h₁ : SurjOn f s₁ t
h₂ : SurjOn f s₂ t
h : InjOn f (s₁ ∪ s₂)
⊢ SurjOn f (s₁ ∩ s₂) t

Tactic:
inter_self t ▸ h₁.inter_inter h₂ h

Premises used: Set.inter_self, Eq.rec, Set.SurjOn.inter_inter
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ SurjOn id s s

Tactic:
simp [SurjOn]

Premises used: Set.SurjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
hg : SurjOn g t p
hf : SurjOn f s t
⊢ SurjOn (g ∘ f) s p

Tactic:
Subset.trans hg <| Subset.trans (image_mono hf) <| image_comp g f s ▸ Subset.refl _

Premises used: Set.Subset.refl, Set.Subset.trans, Set.image_mono, Set.SurjOn, Eq.rec, Set.image_comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
z : γ
hz : z ∈ p
obtain : ∀ (x : α) (hx : x ∈ s) (hz : (g ∘ f) x ∈ p), (g ∘ f) x ∈ g '' t
⊢ z ∈ g '' t

Tactic:
obtain ⟨x, hx, rfl⟩ := h hz

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
x : α
hx : x ∈ s
hz : (g ∘ f) x ∈ p
⊢ (g ∘ f) x ∈ g '' t

Tactic:
⟨f x, hr hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
x : α
hx : x ∈ s
hz : (g ∘ f) x ∈ p
⊢ (g ∘ f) x ∈ g '' t

Tactic:
exact ⟨f x, hr hx, rfl⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
p : Set γ
f : α → β
g : β → γ
⊢ SurjOn (g ∘ f) s p ↔ SurjOn g (f '' s) p

Tactic:
⟨fun h ↦ h.of_comp <| mapsTo_image f s, fun h ↦ h.comp <| surjOn_image _ _⟩

Premises used: Set.surjOn_image, Set.mapsTo_image, Set.SurjOn.of_comp, Set.SurjOn.comp, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
rw : g '' t ⊆ g '' f '' s
⊢ SurjOn (g ∘ f) s (g '' t)

Tactic:
rw [SurjOn, image_comp g f]

Premises used: Set.SurjOn, Set.image_comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s

Tactic:
image_mono hf

Premises used: Set.image_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ g '' t ⊆ g '' f '' s

Tactic:
exact image_mono hf

Premises used: Set.image_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
rwa : t ⊆ g ∘ f '' f ⁻¹' s
rwa₁ : t ⊆ g '' f '' f ⁻¹' s
rwa₂ rwa₃ rwa₄ rwa₅ : t ⊆ g '' s
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t

Tactic:
rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]

Premises used: Set.SurjOn, Set.image_preimage_eq, Set.image_comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Subsingleton β
f : α → β
h : t.Nonempty → s.Nonempty
⊢ SurjOn f s t

Tactic:
fun _ ha ↦ Subsingleton.mem_iff_nonempty.2 <| (h ⟨_, ha⟩).image _

Premises used: Iff.mpr, Subsingleton.mem_iff_nonempty, Set.SurjOn, Set.Subset, Set.Nonempty.image, Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
inst : Subsingleton α
f : α → α
s : Set α
⊢ SurjOn f s s

Tactic:
surjOn_of_subsingleton' _ id

Premises used: id, Set.surjOn_of_subsingleton'
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ SurjOn f univ univ ↔ Surjective f

Tactic:
simp [Surjective, SurjOn, subset_def]

Premises used: Set.subset_def, Set.SurjOn, Function.Surjective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Surjective f
⊢ SurjOn f univ t

Tactic:
(surjOn_univ.2 hf).mono .rfl (subset_univ _)

Premises used: Iff.mpr, Set.SurjOn.mono, Set.subset_univ, Set.surjOn_univ, Set.Subset.rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : SurjOn f s univ
⊢ Surjective f

Tactic:
surjOn_univ.1 <| hf.mono s.subset_univ .rfl

Premises used: Set.SurjOn.mono, Set.subset_univ, Set.surjOn_univ, Set.Subset.rfl, Iff.mp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h₁ : SurjOn f s t
h₂ : MapsTo f s t
⊢ f '' s = t

Tactic:
eq_of_subset_of_subset h₂.image_subset h₁

Premises used: Set.MapsTo.image_subset, Set.eq_of_subset_of_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩

Premises used: And.right, And.left, Iff.intro, Set.SurjOn.image_eq_of_mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
refine : f '' s = t → SurjOn f s t ∧ MapsTo f s t
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t

Tactic:
refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)

Tactic:
⟨s.surjOn_image f, s.mapsTo_image f⟩

Premises used: Set.surjOn_image, Set.mapsTo_image, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s (f '' s) ∧ MapsTo f s (f '' s)

Tactic:
exact ⟨s.surjOn_image f, s.mapsTo_image f⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t t₁ : Set β
f : α → β
h : SurjOn f s t
ht : t₁ ⊆ t
⊢ f '' f ⁻¹' t₁ = t₁

Tactic:
image_preimage_eq_iff.2 fun _ hx ↦ mem_range_of_mem_image f s <| h <| ht hx

Premises used: Iff.mpr, Set.mem_range_of_mem_image, Set.image_preimage_eq_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
h' : Injective f
⊢ MapsTo f sᶜ tᶜ

Tactic:
fun _ hs ht =>
  let ⟨_, hx', HEq⟩ := h ht
  hs <| h' HEq ▸ hx'

Premises used: _private.0.Set.InjOn.mem_of_mem_image.match_1, False, Set.Mem, setOf, Eq.rec, Set.MapsTo, Not
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective f
⊢ SurjOn f sᶜ tᶜ

Tactic:
h'.forall.2 fun _ ht => (mem_image_of_mem _) fun hs => ht (h hs)

Premises used: Iff.mpr, Function.Surjective.forall, Set.SurjOn, Set.Subset, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), g₁ (f a) = g₂ (f a)
⊢ g₁ b = g₂ b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf' hb

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)

Tactic:
hf ha
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ g₁ (f a) = g₂ (f a)

Tactic:
exact hf ha
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : SurjOn f s t
hf' : MapsTo f s t
⊢ EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ EqOn g₁ g₂ t

Tactic:
⟨fun h => h.cancel_right hf, fun h => h.comp_right hf'⟩

Premises used: Set.EqOn.comp_right, Iff.intro, Set.EqOn.cancel_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g₁ g₂ : β → γ
⊢ EqOn (g₁ ∘ f) (g₂ ∘ f) s ↔ EqOn g₁ g₂ (f '' s)

Tactic:
(s.surjOn_image f).cancel_right <| s.mapsTo_image f

Premises used: Set.surjOn_image, Set.mapsTo_image, Set.SurjOn.cancel_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : SurjOn f s t
hf' : MapsTo f s t
⊢ (∀ (y : β), y ∈ t → p y) ↔ ∀ (x : α), x ∈ s → p (f x)

Tactic:
⟨fun H x hx ↦ H (f x) (hf' hx), fun H _y hy ↦ let ⟨x, hx, hxy⟩ := hf hy; hxy ▸ H x hx⟩

Premises used: Eq.rec, _private.0.Set.SurjOn.forall.match_1, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β : Type u_8
f : α → β
p : Set β
h : ∀ (a : α), f a ∈ p
hf : SurjOn f univ p
⊢ Surjective (Subtype.coind f (p := Membership.mem p) h)

Tactic:
fun ⟨_, hb⟩ ↦
  let ⟨a, _, ha⟩ := hf hb
  ⟨a, Subtype.coe_injective ha⟩

Premises used: Exists, Subtype.coe_injective, Subtype.mk, Subtype.coind, Exists.intro, _private.0.Subtype.coind_surjective.match_1, _private.0.Subtype.coind_surjective.match_2, Eq, Function.Surjective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β : Type u_8
f : α → β
p : Set β
h : ∀ (a : α), f a ∈ p
hf_inj : Injective f
hf_surj : SurjOn f univ p
⊢ Bijective (Subtype.coind f (p := Membership.mem p) h)

Tactic:
⟨Subtype.coind_injective h hf_inj, Subtype.coind_surjective h hf_surj⟩

Premises used: Subtype.coind_injective, And.intro, Subtype.coind_surjective, Function.Bijective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ MapsTo f s t

Tactic:
h.left

Premises used: And.left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ InjOn f s

Tactic:
h.right.left

Premises used: And.right, And.left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ SurjOn f s t

Tactic:
h.right.right

Premises used: And.right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h₁ : MapsTo f s t
h₂ : InjOn f s
h₃ : SurjOn f s t
⊢ BijOn f s t

Tactic:
⟨h₁, h₂, h₃⟩

Premises used: And.intro, Set.BijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
⟨mapsTo_empty f ∅, injOn_empty f, surjOn_empty f ∅⟩

Premises used: Set.surjOn_empty, Set.mapsTo_empty, And.intro, Set.BijOn, EmptyCollection.emptyCollection, Set.injOn_empty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : BijOn f s ∅
⊢ s = ∅

Tactic:
simpa using h.mapsTo

Premises used: Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
bijOn_empty f

Premises used: Set.bijOn_empty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f ∅ ∅

Tactic:
exact bijOn_empty f

Premises used: Set.bijOn_empty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
h : BijOn f ∅ t
⊢ t = ∅

Tactic:
simpa using h.surjOn

Premises used: Set.BijOn.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b

Tactic:
simp [BijOn, eq_comm]

Premises used: eq_comm, Set.BijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : BijOn f s₁ t₁
h₂ : MapsTo f s₂ t₂
h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂
⊢ BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
⟨h₁.mapsTo.inter_inter h₂, h₁.injOn.mono inter_subset_left, fun _ hy =>
    let ⟨x, hx, hxy⟩ := h₁.surjOn hy.1
    ⟨x, ⟨hx, h₃ ⟨hx, hxy.symm.subst hy.2⟩⟩, hxy⟩⟩

Premises used: Set.MapsTo.inter_inter, Eq.subst, Membership.mem, Set.inter_subset_left, Set.BijOn.injOn, Inter.inter, Set.BijOn.surjOn, _private.0.Set.SurjOn.forall.match_1, And.right, And.left, And.intro, Set.BijOn, Exists.intro, Set.BijOn.mapsTo, Set.InjOn.mono, Set.image, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : MapsTo f s₁ t₁
h₂ : BijOn f s₂ t₂
h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁
⊢ BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
inter_comm s₂ s₁ ▸ inter_comm t₂ t₁ ▸ h₂.inter_mapsTo h₁ h₃

Premises used: Eq.rec, Set.inter_comm, Set.BijOn.inter_mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : BijOn f s₁ t₁
h₂ : BijOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ BijOn f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
⟨h₁.mapsTo.inter_inter h₂.mapsTo, h₁.injOn.mono inter_subset_left,
    h₁.surjOn.inter_inter h₂.surjOn h⟩

Premises used: Set.MapsTo.inter_inter, Set.SurjOn.inter_inter, Set.inter_subset_left, Set.BijOn.injOn, Set.BijOn.surjOn, And.intro, Set.BijOn, Set.BijOn.mapsTo, Set.InjOn.mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : BijOn f s₁ t₁
h₂ : BijOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
⊢ BijOn f (s₁ ∪ s₂) (t₁ ∪ t₂)

Tactic:
⟨h₁.mapsTo.union_union h₂.mapsTo, h, h₁.surjOn.union_union h₂.surjOn⟩

Premises used: Set.SurjOn.union_union, Set.BijOn.surjOn, And.intro, Set.MapsTo.union_union, Set.BijOn, Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ t ⊆ range f

Tactic:
h.surjOn.subset_range

Premises used: Set.BijOn.surjOn, Set.SurjOn.subset_range
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
⊢ BijOn f s (f '' s)

Tactic:
BijOn.mk (mapsTo_image f s) h (Subset.refl _)

Premises used: Set.Subset.refl, Set.mapsTo_image, Set.BijOn.mk
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
rw : u ∈ t ∩ range f
⊢ u ∈ f '' f ⁻¹' t

Tactic:
rw [image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ t ∩ range f

Tactic:
⟨hu, mem_range.mpr (subset_range h hu)⟩

Premises used: Iff.mpr, Set.mem_range, Set.Mem, setOf, Set.inter, And.intro, Set.SurjOn.subset_range
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ t ∩ range f

Tactic:
exact ⟨hu, mem_range.mpr (subset_range h hu)⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h₁ : BijOn f₁ s t
h : EqOn f₁ f₂ s
⊢ BijOn f₂ s t

Tactic:
BijOn.mk (h₁.mapsTo.congr h) (h₁.injOn.congr h) (h₁.surjOn.congr h)

Premises used: Set.BijOn.injOn, Set.BijOn.surjOn, Set.SurjOn.congr, Set.InjOn.congr, Set.BijOn.mapsTo, Set.BijOn.mk, Set.MapsTo.congr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
H : EqOn f₁ f₂ s
⊢ BijOn f₁ s t ↔ BijOn f₂ s t

Tactic:
⟨fun h => h.congr H, fun h => h.congr H.symm⟩

Premises used: Iff.intro, Set.EqOn.symm, Set.BijOn.congr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ f '' s = t

Tactic:
h.surjOn.image_eq_of_mapsTo h.mapsTo

Premises used: Set.BijOn.surjOn, Set.BijOn.mapsTo, Set.SurjOn.image_eq_of_mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
b : β
hb : b ∈ t
obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), p (f a)
⊢ p b

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Premises used: Set.BijOn.surjOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Tactic:
h _ ha
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p (f a)

Tactic:
exact h _ ha
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t) (h : p (f a)), ∃ (a : α), a ∈ s ∧ p (f a)
⊢ ∃ (a : α), a ∈ s ∧ p (f a)

Tactic:
obtain ⟨a, ha, rfl⟩ := hf.surjOn hb

Premises used: Set.BijOn.surjOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ (a : α), a ∈ s ∧ p (f a)

Tactic:
⟨a, ha, h⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ (a : α), a ∈ s ∧ p (f a)

Tactic:
exact ⟨a, ha, h⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ (b : β), b ∈ t ∧ p b

Tactic:
⟨f a, hf.mapsTo ha, h⟩

Premises used: And.intro, Exists.intro, Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
h : p (f a)
⊢ ∃ (b : β), b ∈ t ∧ p b

Tactic:
exact ⟨f a, hf.mapsTo ha, h⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
e : α ≃ β
⊢ (⇑e : (a : α) → β) '' s = t ↔ BijOn (⇑e : (a : α) → β) s t

Tactic:
⟨fun h ↦ ⟨(mapsTo_image e s).mono_right h.subset, e.injective.injOn, h ▸ surjOn_image e s⟩,
  BijOn.image_eq⟩

Premises used: Set.surjOn_image, Set.MapsTo.mono_right, Function.Injective.injOn, Set.mapsTo_image, Eq.rec, Set.BijOn.image_eq, Eq.subset, And.intro, Iff.intro, Equiv.injective, DFunLike.coe
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ BijOn id s s

Tactic:
⟨s.mapsTo_id, s.injOn_id, s.surjOn_id⟩

Premises used: Set.mapsTo_id, Set.injOn_id, Set.surjOn_id, And.intro, Set.BijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
hg : BijOn g t p
hf : BijOn f s t
⊢ BijOn (g ∘ f) s p

Tactic:
BijOn.mk (hg.mapsTo.comp hf.mapsTo) (hg.injOn.comp hf.injOn hf.mapsTo) (hg.surjOn.comp hf.surjOn)

Premises used: Set.InjOn.comp, Set.BijOn.injOn, Set.BijOn.surjOn, Set.MapsTo.comp, Set.SurjOn.comp, Set.BijOn.mapsTo, Set.BijOn.mk