awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
hy₁ : x ∈ s₂
⊢ f x = f x

Tactic:
obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy

Premises used: Or.inl, Or.inr, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
hy : x ∈ s₂
hxy : f x = f x
⊢ False

Tactic:
h.le_bot ⟨hx, hy⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
hy : x ∈ s₂
hxy : f x = f x
⊢ False

Tactic:
exact h.le_bot ⟨hx, hy⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

Tactic:
h₁ hx hy hxy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

Tactic:
(h₁₂ _ hx _ hy hxy).elim

Premises used: False.elim
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

Tactic:
(h₁₂ _ hy _ hx hxy.symm).elim

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₂
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

Tactic:
h₂ hx hy hxy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
h₁ : InjOn f s₁
h₂ : InjOn f s₂
h₁₂ : ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₁
hxy : f x = f y
⊢ x = y

Tactic:
exacts [h₁ hx hy hxy, (h₁₂ _ hx _ hy hxy).elim, (h₁₂ _ hy _ hx hxy.symm).elim, h₂ hx hy hxy]

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
rw :
  (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), Membership.mem (γ := Set α) {a} y → f x ≠ f y) ↔
    InjOn f s ∧ ¬f a ∈ f '' s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]

Premises used: Iff.mpr, Set.disjoint_singleton_right, Set.injOn_union, Set.union_singleton
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), Membership.mem (γ := Set α) {a} y → f x ≠ f y) ↔
    InjOn f s ∧ ¬f a ∈ f '' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ InjOn f univ ↔ Injective f

Tactic:
simp [InjOn, Injective]

Premises used: Function.Injective, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
h : Injective f
s : Set α
⊢ InjOn f s

Tactic:
fun _ _ _ _ hxy => h hxy

Premises used: Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
p : α → Prop
s : Set { x : α // p x }
⊢ InjOn (Subtype.val (p := fun (x : α) ↦ p x)) s

Tactic:
Subtype.coe_injective.injOn

Premises used: Function.Injective.injOn, Subtype.coe_injective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ InjOn id s

Tactic:
injective_id.injOn

Premises used: Function.Injective.injOn, Function.injective_id
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g : β → γ
hg : InjOn g t
hf : InjOn f s
h : MapsTo f s t
⊢ InjOn (g ∘ f) s

Tactic:
fun _ hx _ hy heq => hf hx hy <| hg (h hx) (h hy) heq

Premises used: Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
h : InjOn (g ∘ f) s
x : α
hx : x ∈ s
x_1 : α
hy : x_1 ∈ s
heq : f x = f x_1
⊢ (g ∘ f) x = (g ∘ f) x_1

Tactic:
simp [heq]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
h : InjOn (g ∘ f) s
⊢ InjOn g (f '' s)

Tactic:
forall_mem_image.2 fun _x hx ↦ forall_mem_image.2 fun _y hy heq ↦ congr_arg f <| h hx hy heq

Premises used: Iff.mpr, congr_arg, Set.InjOn, Set.forall_mem_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f : α → β
g : β → γ
hf : InjOn f s
⊢ InjOn (g ∘ f) s ↔ InjOn g (f '' s)

Tactic:
⟨image_of_comp, fun h ↦ InjOn.comp h hf <| mapsTo_image f s⟩

Premises used: Set.InjOn.image_of_comp, Set.InjOn.comp, Set.mapsTo_image, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Subsingleton α
f : α → β
s : Set α
⊢ InjOn f s

Tactic:
(injective_of_subsingleton _).injOn

Premises used: Function.Injective.injOn, Function.injective_of_subsingleton
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y

Tactic:
congr_arg f (h H)

Premises used: congr_arg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
h : Injective (g ∘ f)
x y : α
H : g (f x) = g (f y)
⊢ f x = f y

Tactic:
exact congr_arg f (h H)

Premises used: congr_arg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
h_1 : InjOn g s
hs : range f ⊆ s
h : Injective f
x : α
⊢ ∀ ⦃a₂ : α⦄, (g ∘ f) x = (g ∘ f) a₂ → x = a₂

Tactic:
aesop
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Nonempty β
h : ∃ (f : (↑s : Type u_1) → β), Injective f
f : (↑s : Type u_1) → β
hf : Injective f
⊢ True

Tactic:
trivial

Premises used: trivial
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Nonempty β
h : ∃ (f : (↑s : Type u_1) → β), Injective f
f : (↑s : Type u_1) → β
hf : Injective f
lift :
  ∀ (f : α → β) (hf : Injective.{u_1 + 1, u_2 + 1} (β := β) fun (i : (↑s : Type u_1)) ↦ f (↑i : α)),
    ∃ (f : α → β), InjOn f s
⊢ ∃ (f : α → β), InjOn f s

Tactic:
lift f to α → β using trivial

Premises used: trivial
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Nonempty β
h : ∃ (f : (↑s : Type u_1) → β), Injective f
f : α → β
hf : Injective.{u_1 + 1, u_2 + 1} (β := β) fun (i : (↑s : Type u_1)) ↦ f (↑i : α)
⊢ ∃ (f : α → β), InjOn f s

Tactic:
⟨f, injOn_iff_injective.2 hf⟩

Premises used: Iff.mpr, Set.injOn_iff_injective, Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Nonempty β
h : ∃ (f : (↑s : Type u_1) → β), Injective f
f : α → β
hf : Injective.{u_1 + 1, u_2 + 1} (β := β) fun (i : (↑s : Type u_1)) ↦ f (↑i : α)
⊢ ∃ (f : α → β), InjOn f s

Tactic:
exact ⟨f, injOn_iff_injective.2 hf⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
B : Set (Set β)
hB : B ⊆ 𝒫 range f
⊢ InjOn (preimage f) B

Tactic:
fun _ hs _ ht hst => (preimage_eq_preimage' (hB hs) (hB ht)).1 hst

Premises used: Set.preimage_eq_preimage', Iff.mp, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
x : α
hf : InjOn f s
hs : s₁ ⊆ s
h : x ∈ s
h₁ : f x ∈ f '' s₁
⊢ x ∈ s₁

Tactic:
let ⟨_, h', Eq⟩ := h₁
  hf (hs h') h Eq ▸ h'

Premises used: _private.0.Set.InjOn.mem_of_mem_image.match_1, Membership.mem, Eq.rec
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
x : α
hf : InjOn f s
hs : s₁ ⊆ s
hx : x ∈ s
⊢ f x ∈ f '' s₁ ↔ x ∈ s₁

Tactic:
⟨hf.mem_of_mem_image hs hx, mem_image_of_mem f⟩

Premises used: Set.InjOn.mem_of_mem_image, Set.mem_image_of_mem, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
hf : InjOn f s
hs : s₁ ⊆ s
⊢ f ⁻¹' f '' s₁ ∩ s = s₁

Tactic:
ext fun _ => ⟨fun ⟨h₁, h₂⟩ => hf.mem_of_mem_image hs h₂ h₁, fun h => ⟨mem_image_of_mem _ h, hs h⟩⟩

Premises used: Set.ext, Membership.mem, Set.InjOn.mem_of_mem_image, Set.mem_image_of_mem, And.intro, Iff.intro, _private.0.Set.InjOn.preimage_image_inter.match_1
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f₁ f₂ : α → β
g : β → γ
h : EqOn (g ∘ f₁) (g ∘ f₂) s
hg : InjOn g t
hf₁ : MapsTo f₁ s t
hf₂ : MapsTo f₂ s t
⊢ EqOn f₁ f₂ s

Tactic:
fun _ ha => hg (hf₁ ha) (hf₂ ha) (h ha)

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f₁ f₂ : α → β
g : β → γ
hg : InjOn g t
hf₁ : MapsTo f₁ s t
hf₂ : MapsTo f₂ s t
⊢ EqOn (g ∘ f₁) (g ∘ f₂) s ↔ EqOn f₁ f₂ s

Tactic:
⟨fun h => h.cancel_left hg hf₁ hf₂, EqOn.comp_left⟩

Premises used: Set.EqOn.cancel_left, Set.EqOn.comp_left, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
apply : f '' s ∩ f '' t ⊆ f '' (s ∩ t)
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
apply Subset.antisymm (image_inter_subset _ _ _)

Premises used: Set.Subset.antisymm, Set.image_inter_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
this : ∀ (y : α) (ys : y ∈ s) (hy : f y = x) (z : α) (zt : z ∈ t) (hz : f z = x), x ∈ f '' (s ∩ t)
⊢ x ∈ f '' s ∩ f '' t → x ∈ f '' (s ∩ t)

Tactic:
⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
apply : f y = f z
⊢ y = z

Tactic:
apply hf (hs ys) (ht zt)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hy : f y = f z) (zt : z ∈ t) (hz : f z = x), f y = f z
⊢ f y = f z

Tactic:
rwa [← hz] at hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z

Tactic:
have : y = z := by
    apply hf (hs ys) (ht zt)
    rwa [← hz] at hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ y ∈ t

Tactic:
rw [← this] at zt
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
zt₁ : y ∈ t
⊢ f z = x

Tactic:
rw [← this] at zt
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
zt₁ : y ∈ t
hz₁ : f z = x
⊢ y = z

Tactic:
rw [← this] at zt
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
⟨y, ⟨ys, zt⟩, hy⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
exact ⟨y, ⟨ys, zt⟩, hy⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
rw : f ⁻¹' f '' s₁ ∩ s = s₂
rw₁ : f ⁻¹' f '' s₂ ∩ s = s₂
rw₂ rw₃ : s₂ = s₂
⊢ s₁ = s₂

Tactic:
rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

Premises used: Set.InjOn.preimage_image_inter
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ = f '' s₂ ↔ s₁ = s₂

Tactic:
h.image.eq_iff h₁ h₂

Premises used: Set.InjOn.eq_iff, Set.InjOn.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Tactic:
⟨fun h' ↦ ?_, image_mono⟩

Premises used: Set.image_mono, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
refine : ∀ (h' : f '' s₁ ⊆ f '' s₂), s₁ ⊆ s₂
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂

Tactic:
refine ⟨fun h' ↦ ?_, image_mono⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
rw : f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s
⊢ s₁ ⊆ s₂

Tactic:
rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]

Premises used: Set.InjOn.preimage_image_inter
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s

Tactic:
inter_subset_inter_left _ (preimage_mono h')

Premises used: Set.inter_subset_inter_left, Set.preimage_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s

Tactic:
exact inter_subset_inter_left _ (preimage_mono h')

Premises used: Set.inter_subset_inter_left, Set.preimage_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
simp_rw : f '' s₁ ⊆ f '' s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
simp_rw₁ : s₁ ⊆ s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]

Premises used: Set.ssubset_def, Set.InjOn.image_subset_image_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
rw : ∀ (h : s ∩ t = ∅) (hf : InjOn f u) (hs : s ⊆ u) (ht : t ⊆ u), f '' s ∩ f '' t = ∅
⊢ Disjoint (f '' s) (f '' t)

Tactic:
rw [disjoint_iff_inter_eq_empty] at h ⊢

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
rw : f '' (s ∩ t) = ∅
rw₁ : f '' ∅ = ∅
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ f '' s ∩ f '' t = ∅

Tactic:
rw [← hf.image_inter hs ht, h, image_empty]

Premises used: Set.InjOn.image_inter, Set.image_empty
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
rw : f '' s ⊆ f '' (s ∩ t ∪ s \ t)
rw₁ rw₂ : f '' s ⊆ f '' s
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)

Tactic:
rw [← image_union, inter_union_diff]

Premises used: Set.inter_union_diff, Set.image_union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
refine : Disjoint (f '' (s \ t)) (f '' (s ∩ t))
⊢ f '' (s \ t) = f '' s \ f '' (s ∩ t)

Tactic:
refine subset_antisymm (subset_diff.2 ⟨image_mono diff_subset, ?_⟩)
    (diff_subset_iff.2 (by rw [← image_union, inter_union_diff]))

Premises used: Iff.mpr, Set.diff_subset, Set.diff_subset_iff, Set.image_mono, Set.subset_diff, subset_antisymm, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))

Tactic:
Disjoint.image disjoint_sdiff_inter h diff_subset inter_subset_left

Premises used: Set.diff_subset, Set.disjoint_sdiff_inter, Set.inter_subset_left, Disjoint.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ Disjoint (f '' (s \ t)) (f '' (s ∩ t))

Tactic:
exact Disjoint.image disjoint_sdiff_inter h diff_subset inter_subset_left

Premises used: Set.diff_subset, Set.disjoint_sdiff_inter, Set.inter_subset_left, Disjoint.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
rw : f '' s \ f '' (s ∩ t) = f '' s \ f '' t
rw₁ rw₂ : f '' s \ f '' t = f '' s \ f '' t
⊢ f '' (s \ t) = f '' s \ f '' t

Tactic:
rw [h.image_diff, inter_eq_self_of_subset_right hst]

Premises used: Set.InjOn.image_diff, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x_1 x_2 : (↑s : Type u_1)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' :
  imageFactorization f s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) =
    imageFactorization f s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx = Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy

Tactic:
simpa [imageFactorization, h.eq_iff hx hy] using h'

Premises used: Set.InjOn.eq_iff, Set.imageFactorization
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h_1 : f x = f y
⊢ imageFactorization f s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) =
    imageFactorization f s (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
simpa [imageFactorization]

Premises used: Set.imageFactorization
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : Injective (imageFactorization f s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h_1 : f x = f y
⊢ x = y

Tactic:
simpa using @h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa [imageFactorization])
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f g : α → β
⊢ graphOn f univ = graphOn g univ ↔ f = g

Tactic:
simp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
⊢ Injective (β := Set (α × β)) fun (f : α → β) ↦ graphOn f univ

Tactic:
fun _f _g ↦ graphOn_univ_inj.1

Premises used: Iff.mp, Set.graphOn_univ_inj, Function.Injective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
⊢ (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s

Tactic:
⟨?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
refine_1 : (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s
refine_2 : ∀ (h : InjOn Prod.fst s), ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
⊢ (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s

Tactic:
refine ⟨?_, fun h ↦ ?_⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
refine_1 : InjOn Prod.fst (graphOn f (Prod.fst '' s))
⊢ InjOn Prod.fst s

Tactic:
rw [hf]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))

Tactic:
InjOn.image_of_comp <| injOn_id _

Premises used: Set.injOn_id, Set.InjOn.image_of_comp, Set.graphOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst (graphOn f (Prod.fst '' s))

Tactic:
exact InjOn.image_of_comp <| injOn_id _

Premises used: Set.injOn_id, Set.InjOn.image_of_comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∀ (x : α), x ∈ Prod.fst '' s → ∃ (y : β), (x, y) ∈ s

Tactic:
have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
this : ∀ (x : α), x ∈ Prod.fst '' s → ∃ (y : β), (x, y) ∈ s
refine_2 :
  ∀ (f : (x : α) → β) (hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s), ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)

Tactic:
choose! f hf using this
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s
⊢ ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s

Tactic:
rw [forall_mem_image] at hf

Premises used: Set.forall_mem_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
h₁ : s = graphOn f (Prod.fst '' s)
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)

Tactic:
use f
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
h₁ : EqOn (fun (x : α × β) ↦ (x.1, f x.1)) id s
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
rw [graphOn, image_image, EqOn.image_eq_self]

Premises used: Set.image_image, Set.graphOn, Set.EqOn.image_eq_self
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ EqOn (fun (x : α × β) ↦ (x.1, f x.1)) id s

Tactic:
fun x hx ↦ h (hf hx) hx rfl

Premises used: Set.EqOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ EqOn (fun (x : α × β) ↦ (x.1, f x.1)) id s

Tactic:
exact fun x hx ↦ h (hf hx) hx rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : ∃ (f : α → β), ∃ (t : Set α), s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
rw : graphOn f t = graphOn f (Prod.fst '' graphOn f t)
rw₁ rw₂ : graphOn f t = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)

Tactic:
rw [hs, image_fst_graphOn]

Premises used: Set.image_fst_graphOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ t ⊆ range f

Tactic:
Subset.trans h <| image_subset_range f s

Premises used: Set.Subset.trans, Set.image_subset_range
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h :
  ∃ (t' : Set β),
    ∃ (g : (↑s : Type u_1) → (↑t' : Type u_2)),
      t ⊆ t' ∧ Surjective g ∧ ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
y : β
hy : y ∈ t
t' : Set β
g : (↑s : Type u_1) → (↑t' : Type u_2)
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : (↑s : Type u_1)
hx : g x = Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯
rw : (↑(g x) : β) = y
rw₁ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯) : β) = y
rw₂ rw₃ : y = y
⊢ f (↑x : α) = y

Tactic:
rw [hfg, hx, Subtype.coe_mk]

Premises used: Subtype.coe_mk
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ SurjOn f s ∅

Tactic:
empty_subset _

Premises used: Set.SurjOn, Set.empty_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ SurjOn f ∅ t ↔ t = ∅

Tactic:
simp [SurjOn, subset_empty_iff]

Premises used: Set.SurjOn, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
⊢ SurjOn f s {b} ↔ b ∈ f '' s

Tactic:
singleton_subset_iff

Premises used: Set.singleton_subset_iff, Set.SurjOn