awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
rw : f (f' (f x)) = f x
rw₁ rw₂ : f x = f x
⊢ f (f' y) = y

Tactic:
rw [← heq, hf' hx]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
h : ∀ (x : β), x ∈ f '' s ↔ x ∈ g ⁻¹' s
⊢ f '' s = g ⁻¹' s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
h : x ∈ f '' s → x ∈ g ⁻¹' s
h₁ : x ∈ g ⁻¹' s → x ∈ f '' s
⊢ x ∈ f '' s ↔ x ∈ g ⁻¹' s

Tactic:
constructor
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy h : y ∈ s
⊢ f y ∈ g ⁻¹' s

Tactic:
rw [mem_preimage, hgf hy]

Premises used: Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s

Tactic:
hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
y : α
hy : y ∈ s
⊢ y ∈ s

Tactic:
exact hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
⊢ x ∈ f '' s

Tactic:
⟨g x, hx, Set.InjOn.rightInvOn_of_leftInvOn ginj hgf (Set.mapsTo_preimage g s) ?_ hx⟩

Premises used: Set.Mem, setOf, Set.InjOn.rightInvOn_of_leftInvOn, Set.mapsTo_preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
h : MapsTo f s (g ⁻¹' s)
⊢ x ∈ f '' s

Tactic:
refine ⟨g x, hx, Set.InjOn.rightInvOn_of_leftInvOn ginj hgf (Set.mapsTo_preimage g s) ?_ hx⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
y : α
hy : y ∈ s
⊢ f y ∈ g ⁻¹' s

Tactic:
simpa [hgf hy] using hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ InvOn id id s s

Tactic:
⟨s.leftInvOn_id, s.rightInvOn_id⟩

Premises used: Set.leftInvOn_id, Set.InvOn, Set.rightInvOn_id, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
f' : β → α
g' : γ → β
hf : InvOn f' f s t
hg : InvOn g' g t p
fst : MapsTo f s t
g'pt : MapsTo g' p t
⊢ InvOn (f' ∘ g') (g ∘ f) s p

Tactic:
⟨hf.1.comp hg.1 fst, hf.2.comp hg.2 g'pt⟩

Premises used: Set.InvOn, Set.RightInvOn.comp, And.right, And.left, And.intro, Set.LeftInvOn.comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : InvOn f' f s t
⊢ InvOn f f' t s

Tactic:
⟨h.right, h.left⟩

Premises used: Set.InvOn, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
f : α → β
f' : β → α
h : InvOn f' f s t
hs : s₁ ⊆ s
ht : t₁ ⊆ t
⊢ InvOn f' f s₁ t₁

Tactic:
⟨h.1.mono hs, h.2.mono ht⟩

Premises used: Set.InvOn, Set.LeftInvOn.mono, Set.RightInvOn.mono, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : InvOn f' f s t
hf : MapsTo f s t
hf' : MapsTo f' t s
⊢ BijOn f s t

Tactic:
⟨hf, h.left.injOn, h.right.surjOn hf'⟩

Premises used: Set.RightInvOn.surjOn, And.right, And.left, And.intro, Set.BijOn, Set.LeftInvOn.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
rw :
  Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h ∈ s ∧
    f (Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h) = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b

Tactic:
rw [invFunOn, dif_pos h]

Premises used: Function.invFunOn, dif_pos
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
⊢ Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h ∈ s ∧
    f (Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h) = b

Tactic:
Classical.choose_spec h

Premises used: Classical.choose_spec
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
⊢ Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h ∈ s ∧
    f (Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h) = b

Tactic:
exact Classical.choose_spec h

Premises used: Classical.choose_spec
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s

Tactic:
(invFunOn_pos h).left

Premises used: Function.invFunOn_pos, And.left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
⊢ f (invFunOn f s b) = b

Tactic:
(invFunOn_pos h).right

Premises used: Function.invFunOn_pos, And.right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ¬∃ (a : α), a ∈ s ∧ f a = b
rw :
  (if h : ∃ (a : α), a ∈ s ∧ f a = b then Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h
    else Classical.choice inst) =
    Classical.choice inst
rw₁ rw₂ : Classical.choice inst = Classical.choice inst
⊢ invFunOn f s b = Classical.choice inst

Tactic:
rw [invFunOn, dif_neg h]

Premises used: Function.invFunOn, dif_neg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
a : α
inst : Nonempty α
h : a ∈ s
⊢ invFunOn f s (f a) ∈ s

Tactic:
invFunOn_mem ⟨a, h, rfl⟩

Premises used: Function.invFunOn_mem, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
a : α
inst : Nonempty α
h : a ∈ s
⊢ f (invFunOn f s (f a)) = f a

Tactic:
invFunOn_eq ⟨a, h, rfl⟩

Premises used: Function.invFunOn_eq, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
h : InjOn f s
⊢ LeftInvOn (invFunOn f s) f s

Tactic:
fun _a ha => h (invFunOn_apply_mem ha) ha (invFunOn_apply_eq ha)

Premises used: Set.LeftInvOn, Function.invFunOn_apply_mem, Function.invFunOn_apply_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
inst : Nonempty α
h : InjOn f s₂
ht : s₁ ⊆ s₂
⊢ invFunOn f s₂ '' f '' s₁ = s₁

Tactic:
h.leftInvOn_invFunOn.image_image' ht

Premises used: Set.LeftInvOn.image_image', Set.InjOn.leftInvOn_invFunOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx : x ∈ s
obtain :
  ∀ (x : α) (hx' : x ∈ s) (hx : invFunOn f s (f x) ∈ s), invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
⊢ invFunOn f s (f x) = x

Tactic:
obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
rw rw₁ : invFunOn f s (f x) = invFunOn f s (f x)
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)

Tactic:
rw [invFunOn_apply_eq (f := f) hx']

Premises used: Function.invFunOn_apply_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
⊢ InjOn f s ↔ invFunOn f s '' f '' s = s

Tactic:
⟨fun h ↦ h.invFunOn_image Subset.rfl, fun h ↦
    (Function.leftInvOn_invFunOn_of_subset_image_image h.symm.subset).injOn⟩

Premises used: Set.InjOn.invFunOn_image, Eq.subset, Set.Subset.rfl, Function.leftInvOn_invFunOn_of_subset_image_image, Iff.intro, Eq.symm, Set.LeftInvOn.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
rw : f (invFunOn f s (f x)) = f x'
rw₁ : f (invFunOn f s (f x')) = f x'
rw₂ rw₃ : f x' = f x'
⊢ f x = f x'

Tactic:
rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']

Premises used: Function.invFunOn_apply_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s

Tactic:
invFunOn_apply_mem hx

Premises used: Function.invFunOn_apply_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) ∈ s

Tactic:
exact invFunOn_apply_mem hx

Premises used: Function.invFunOn_apply_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ RightInvOn (invFunOn f s) f t

Tactic:
fun _y hy => invFunOn_eq <| h hy

Premises used: Set.LeftInvOn, Function.invFunOn_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : BijOn f s t
⊢ InvOn (invFunOn f s) f s t

Tactic:
⟨h.injOn.leftInvOn_invFunOn, h.surjOn.rightInvOn_invFunOn⟩

Premises used: Set.InvOn, Set.BijOn.injOn, Set.SurjOn.rightInvOn_invFunOn, Set.BijOn.surjOn, And.intro, Set.InjOn.leftInvOn_invFunOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
⟨?_, h.rightInvOn_invFunOn⟩

Premises used: Set.InvOn, Set.SurjOn.rightInvOn_invFunOn, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
refine : LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t

Tactic:
refine ⟨?_, h.rightInvOn_invFunOn⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
rw rw₁ : invFunOn f s y = invFunOn f s y
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y

Tactic:
rw [h.rightInvOn_invFunOn hy]

Premises used: Set.SurjOn.rightInvOn_invFunOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ MapsTo (invFunOn f s) t s

Tactic:
fun _y hy => mem_preimage.2 <| invFunOn_mem <| h hy

Premises used: Iff.mpr, Set.Mem, Function.invFunOn_mem, setOf, Set.preimage, Set.MapsTo, Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
r : Set β
hf : SurjOn f s t
hrt : r ⊆ t
⊢ f '' invFunOn f s '' r = r

Tactic:
hf.rightInvOn_invFunOn.image_image' hrt

Premises used: Set.LeftInvOn.image_image', Set.SurjOn.rightInvOn_invFunOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
hf : SurjOn f s t
⊢ f '' invFunOn f s '' t = t

Tactic:
hf.rightInvOn_invFunOn.image_image

Premises used: Set.SurjOn.rightInvOn_invFunOn, Set.LeftInvOn.image_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)

Premises used: Set.SurjOn.invOn_invFunOn, Set.mapsTo_image, Set.InvOn.bijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
refine : MapsTo f (invFunOn f s '' t) t
⊢ BijOn f (invFunOn f s '' t) t

Tactic:
refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)

Premises used: Set.SurjOn.invOn_invFunOn, Set.mapsTo_image, Set.InvOn.bijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
y : β
hy rwa rwa₁ rwa₂ rwa₃ : y ∈ t
⊢ f (invFunOn f s y) ∈ t

Tactic:
rwa [h.rightInvOn_invFunOn hy]

Premises used: Set.SurjOn.rightInvOn_invFunOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
mp : SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
mpr : (∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t
⊢ SurjOn f s t ↔ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t

Tactic:
constructor
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
mp : SurjOn f s ∅ → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' ∅
mp₁ : ∀ (ht : t.Nonempty), SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
⊢ SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t

Tactic:
rcases eq_empty_or_nonempty t with (rfl | ht)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' ∅

Tactic:
fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩

Premises used: Set.bijOn_empty, And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' ∅

Tactic:
exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ Nonempty α

Tactic:
haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t

Tactic:
⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

Premises used: Set.SurjOn.mapsTo_invFunOn, And.intro, Exists.intro, Set.MapsTo.image_subset, Set.SurjOn.bijOn_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t

Tactic:
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t

Tactic:
hfs'.surjOn.mono hs' (Subset.refl _)

Premises used: Set.Subset.refl, Set.SurjOn.mono, Set.BijOn.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t

Tactic:
exact hfs'.surjOn.mono hs' (Subset.refl _)

Premises used: Set.Subset.refl, Set.SurjOn.mono, Set.BijOn.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' (f '' s)

Tactic:
surjOn_iff_exists_bijOn_subset.mp (surjOn_image f s)

Premises used: Set.surjOn_image, Set.surjOn_iff_exists_bijOn_subset, Iff.mp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ ∃ (u : Set α), f '' u = f '' s ∧ InjOn f u

Tactic:
let ⟨u, _, hfu⟩ := exists_subset_bijOn s f
  ⟨u, hfu.image_eq, hfu.injOn⟩

Premises used: Exists, Set.BijOn.image_eq, Set.BijOn.injOn, And, _private.0.Set.exists_image_eq_and_injOn.match_1, And.intro, Exists.intro, Set.exists_subset_bijOn, Set.image, Set.InjOn, Eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
ht : t ⊆ range f
⊢ ∃ (s : Set α), f '' s = t ∧ InjOn f s

Tactic:
image_preimage_eq_of_subset ht ▸ exists_image_eq_and_injOn _ _

Premises used: Set.exists_image_eq_and_injOn, Eq.rec, Set.image_preimage_eq_of_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
obtain :
  ∀ (r : Set α) (hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) (hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))),
    ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f

Premises used: Inter.inter, SDiff.sdiff, Set.preimage, Set.exists_subset_bijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ BijOn f r ((f '' s₁ ∩ t') \ t)

Tactic:
rw [image_diff_preimage, image_inter_preimage] at hbij

Premises used: Set.image_inter_preimage, Set.image_diff_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩

Premises used: Set.subset_union_left, And.intro, Exists.intro, Union.union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_1 : s ∪ r ⊆ s₁
refine_2 : MapsTo f (s ∪ r) t'
refine_3 : InjOn f (s ∪ r)
refine_4 : ∀ (y : β) (hyt' : y ∈ t'), y ∈ f '' (s ∪ r)
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

Tactic:
union_subset hss₁ <| hrss.trans <| diff_subset.trans inter_subset_left

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ s ∪ r ⊆ s₁

Tactic:
exact union_subset hss₁ <| hrss.trans <| diff_subset.trans inter_subset_left

Premises used: Set.diff_subset, HasSubset.Subset.trans, Set.inter_subset_left, Set.union_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_2 : t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
⊢ MapsTo f (s ∪ r) t'

Tactic:
rw [mapsTo_iff_image_subset, image_union, hbij.image_eq, h.image_eq, union_subset_iff]

Premises used: Set.union_subset_iff, Set.mapsTo_iff_image_subset, Set.BijOn.image_eq, Set.image_union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
⟨htt', diff_subset.trans inter_subset_right⟩

Premises used: Set.diff_subset, HasSubset.Subset.trans, And.intro, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'

Tactic:
exact ⟨htt', diff_subset.trans inter_subset_right⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_3 : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y
refine_3₁ : Disjoint s r
⊢ InjOn f (s ∪ r)

Tactic:
rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]

Premises used: and_iff_right, Set.BijOn.injOn, Set.injOn_union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

Tactic:
fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_

Premises used: And.right, Not
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_3 : ∀ (x : α) (hxs : x ∈ s) (y : α) (hyr : y ∈ r) (hxy : f x = f y), y ∈ f ⁻¹' t
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y

Tactic:
refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_

Premises used: And.right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
refine_3 : y ∈ f ⁻¹' f '' s
⊢ y ∈ f ⁻¹' t

Tactic:
rw [← h.image_eq]

Premises used: Set.BijOn.image_eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s

Tactic:
⟨x, hxs, hxy⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' f '' s

Tactic:
exact ⟨x, hxs, hxy⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r

Tactic:
(subset_diff.1 hrss).2.symm.mono_left h.mapsTo

Premises used: Set.subset_diff, Disjoint.mono_left, Disjoint.symm, And.right, Iff.mp, Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ Disjoint s r

Tactic:
exact (subset_diff.1 hrss).2.symm.mono_left h.mapsTo

Premises used: Set.subset_diff, Disjoint.mono_left, Disjoint.symm, And.right, Iff.mp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
refine_4 : y ∈ t ∪ f '' s₁ ∩ t'
⊢ y ∈ f '' (s ∪ r)

Tactic:
rw [image_union, h.image_eq, hbij.image_eq, union_diff_self]

Premises used: Set.BijOn.image_eq, Set.union_diff_self, Set.image_union