awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
⊢ y ∈ t ∪ f '' s₁ ∩ t'

Tactic:
.inr ⟨ht' hyt', hyt'⟩

Premises used: Set.union, Set.Mem, setOf, And.intro, Or.inr
-- 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'
⊢ y ∈ t ∪ f '' s₁ ∩ t'

Tactic:
exact .inr ⟨ht' hyt', hyt'⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ SurjOn f univ t'

Tactic:
simpa [SurjOn]

Premises used: Set.SurjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
htt' : t ⊆ t'
ht' : t' ⊆ range f
⊢ ∃ (s' : Set α), s ⊆ s' ∧ BijOn f s' t'

Tactic:
simpa using h.exists_extend_of_subset (subset_univ s) htt' (by simpa [SurjOn])

Premises used: Set.subset_univ, Set.BijOn.exists_extend_of_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
obtain :
  ∀ (u : Set α) (hru : r ⊆ u) (hus : u ⊆ s) (h : BijOn f u (f '' s)),
    ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
⊢ ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
    (image_mono hrs) Subset.rfl

Premises used: Set.image_mono, Set.InjOn.bijOn_image, Set.Subset.rfl, Set.BijOn.exists_extend_of_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
⟨u, hru, hus, h.image_eq, h.injOn⟩

Premises used: Set.BijOn.image_eq, Set.BijOn.injOn, And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
u : Set α
hru : r ⊆ u
hus : u ⊆ s
h : BijOn f u (f '' s)
⊢ ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u

Tactic:
exact ⟨u, hru, hus, h.image_eq, h.injOn⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
h₁ : ∀ (x : β), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ

Tactic:
ext x
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ
h₂ : ∀ (hx : ¬x ∈ range f), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Premises used: Membership.mem, em, Set.range, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ

Tactic:
simp only [mem_preimage, mem_union, mem_compl_iff, mem_range_self, not_true, or_false,
      leftInverse_invFun hf _, hf.mem_set_image]

Premises used: Set.mem_union, Set.mem_range_self, Function.leftInverse_invFun, not_true, or_false, Function.Injective.mem_set_image, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ

Tactic:
simp only [mem_preimage, invFun_neg hx, h, hx, mem_union, mem_compl_iff, not_false_iff, or_true]

Premises used: Set.mem_union, Function.invFun_neg, not_false_iff, or_true, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
h₁ : ∀ (x : β), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
⊢ invFun f ⁻¹' s = f '' s

Tactic:
ext x
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
h₂ : ∀ (hx : ¬x ∈ range f), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)

Premises used: Membership.mem, em, Set.range, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
h₁ : invFun f (f a) ∈ s ↔ f a ∈ f '' s
h₂ : a ∈ s ↔ f a ∈ f '' s
h₃ h₄ : a ∈ s ↔ a ∈ s
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s

Tactic:
rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]

Premises used: Function.leftInverse_invFun, Function.Injective.mem_set_image, Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ ¬x ∈ f '' s

Tactic:
have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
this : ¬x ∈ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s

Tactic:
simp only [mem_preimage, invFun_neg hx, h, this]

Premises used: Function.invFun_neg, Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
g : β → α
h : InvOn f g t s
hf : BijOn f s t
⊢ BijOn g t s

Tactic:
⟨h.2.mapsTo hf.surjOn, h.1.injOn, h.2.surjOn hf.mapsTo⟩

Premises used: Set.BijOn.surjOn, Set.RightInvOn.surjOn, And.right, And.left, And.intro, Set.BijOn, Set.BijOn.mapsTo, Set.RightInvOn.mapsTo, Set.LeftInvOn.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
g : β → α
h : InvOn f g t s
⊢ BijOn f s t ↔ BijOn g t s

Tactic:
⟨BijOn.symm h, BijOn.symm h.symm⟩

Premises used: Set.InvOn.symm, Set.BijOn.symm, Iff.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hfs : SurjOn f s t
choose :
  ∀ (x : ⦃a : β⦄ → a ∈ t → α) (hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s)
    (heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a), ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t
⊢ ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t

Tactic:
choose x hmem heq using hfs
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (range fun (a : (↑t : Type u_2)) ↦ x ⋯) ⊆ s

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
x_1 : α
⊢ Membership.mem (γ := Set α) (range fun (a : (↑t : Type u_2)) ↦ x ⋯) x_1 →
    ∀ ⦃x₂ : α⦄, Membership.mem (γ := Set α) (range fun (a : (↑t : Type u_2)) ↦ x ⋯) x₂ → f x_1 = f x₂ → x_1 = x₂

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ (f '' range fun (a : (↑t : Type u_2)) ↦ x ⋯) = t

Tactic:
aesop
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
x : ⦃a : β⦄ → a ∈ t → α
hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s
heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a
⊢ ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t

Tactic:
exact ⟨range (fun a : t ↦ x a.2), by grind, fun _ ↦ by grind, by aesop⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set α
hg : Injective g
hf : InjOn f s
⊢ InjOn (g ∘ f) s

Tactic:
hg.injOn.comp hf (mapsTo_univ _ _)

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

Tactic:
fun x _ => h x

Premises used: Set.LeftInvOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : RightInverse f g
s : Set α
⊢ RightInvOn f g s

Tactic:
fun x _ => h x

Premises used: Set.LeftInvOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse f g
⊢ RightInvOn f g (range g)

Tactic:
forall_mem_range.2 fun i => congr_arg g (h i)

Premises used: Iff.mpr, Set.LeftInvOn, Set.forall_mem_range, congr_arg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : MapsTo fa s t
⊢ MapsTo fb (f '' s) (f '' t)

Tactic:
fun _y ⟨x, hx, hy⟩ => hy ▸ ⟨fa x, ha hx, h x⟩

Premises used: Membership.mem, Eq.rec, Set.MapsTo, And.intro, _private.0.Function.Semiconj.mapsTo_image.match_1, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
t : Set β
h : Semiconj f fa fb
hst : MapsTo f s t
⊢ MapsTo f (fa '' s) (fb '' t)

Tactic:
mapsTo_image_iff.2 fun x hx ↦ ⟨f x, hst hx, (h x).symm⟩

Premises used: Iff.mpr, Set.mapsTo_image_iff, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
⊢ MapsTo fb (range f) (range f)

Tactic:
fun _y ⟨x, hy⟩ =>
  hy ▸ ⟨fa x, h x⟩

Premises used: Membership.mem, Eq.rec, Set.MapsTo, _private.0.Function.Semiconj.mapsTo_range.match_1, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
rcases : ∀ (x : α) (hxs : x ∈ s) (hxt : fa x ∈ t), f (fa x) ∈ fb '' f '' s
⊢ f x ∈ fb '' f '' s

Tactic:
rcases ha hxt with ⟨x, hxs, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
rw : fb (f x) ∈ fb '' f '' s
⊢ f (fa x) ∈ fb '' f '' s

Tactic:
rw [h x]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s

Tactic:
mem_image_of_mem _ (mem_image_of_mem _ hxs)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ fb (f x) ∈ fb '' f '' s

Tactic:
exact mem_image_of_mem _ (mem_image_of_mem _ hxs)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
rw : SurjOn fb (f '' univ) (f '' univ)
⊢ SurjOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)

Tactic:
h.surjOn_image ha.surjOn

Premises used: Function.Semiconj.surjOn_image, Function.Surjective.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (f '' univ) (f '' univ)

Tactic:
exact h.surjOn_image ha.surjOn

Premises used: Function.Semiconj.surjOn_image, Function.Surjective.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f (fa x) = f (fa y)

Tactic:
simp only [← h.eq] at H

Premises used: Function.Semiconj.eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y

Tactic:
congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)

Premises used: congr_arg, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : f (fa x) = f (fa y)
⊢ f x = f y

Tactic:
exact congr_arg f (ha hx hy <| hf (mem_image_of_mem fa hx) (mem_image_of_mem fa hy) H)

Premises used: congr_arg, Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
rw : ∀ (hf : InjOn f (fa '' univ)), InjOn fb (f '' univ)
⊢ InjOn fb (range f)

Tactic:
rw [← image_univ] at *

Premises used: Set.image_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)

Tactic:
h.injOn_image ha.injOn hf

Premises used: Function.Injective.injOn, Function.Semiconj.injOn_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (fa '' univ)
⊢ InjOn fb (f '' univ)

Tactic:
exact h.injOn_image ha.injOn hf

Premises used: Function.Injective.injOn, Function.Semiconj.injOn_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : BijOn fa s t
hf : InjOn f t
⊢ BijOn fb (f '' s) (f '' t)

Tactic:
⟨h.mapsTo_image ha.mapsTo, h.injOn_image ha.injOn (ha.image_eq.symm ▸ hf),
    h.surjOn_image ha.surjOn⟩

Premises used: Function.Semiconj.mapsTo_image, Function.Semiconj.surjOn_image, Eq.rec, Set.BijOn.image_eq, Set.BijOn.injOn, Set.BijOn.surjOn, Function.Semiconj.injOn_image, And.intro, Set.BijOn, Set.BijOn.mapsTo, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
rw : BijOn fb (f '' univ) (f '' univ)
⊢ BijOn fb (range f) (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)

Tactic:
h.bijOn_image ha.bijOn_univ hf.injOn

Premises used: Function.Injective.injOn, Function.Semiconj.bijOn_image, Function.Bijective.bijOn_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (f '' univ) (f '' univ)

Tactic:
exact h.bijOn_image ha.bijOn_univ hf.injOn

Premises used: Function.Injective.injOn, Function.Semiconj.bijOn_image, Function.Bijective.bijOn_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s t : Set β
hb : MapsTo fb s t
x : α
hx : x ∈ f ⁻¹' s
⊢ fa x ∈ f ⁻¹' t

Tactic:
simp only [mem_preimage, h x, hb hx]

Premises used: Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ f (fa x) = f (fa y)

Tactic:
have := congr_arg f H
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ fb (f x) = fb (f y)

Tactic:
rw [h.eq, h.eq] at this

Premises used: Function.Semiconj.eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y

Tactic:
hf hx hy (hb hx hy this)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y

Tactic:
exact hf hx hy (hb hx hy this)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Sort u_7
β : Type u_8
γ : β → Sort u_9
inst : DecidableEq β
g : (b : β) → γ b
f : α → β
i : β
a : γ i
h : ¬i ∈ range f
⊢ Eq (α := (j : α) → γ (f j)) (fun (j : α) ↦ update (β := γ) g i a (f j)) fun (j : α) ↦ g (f j)

Tactic:
(update_comp_eq_of_forall_ne' _ _) fun x hx => h ⟨x, hx⟩

Premises used: Function.update_comp_eq_of_forall_ne', Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Sort u_7
β : Type u_8
γ : Sort u_9
inst : DecidableEq β
g : β → γ
f : α → β
i : β
a : γ
h : ¬i ∈ range f
⊢ update (β := fun (a : β) ↦ γ) g i a ∘ f = g ∘ f

Tactic:
update_comp_eq_of_notMem_range' g a h

Premises used: Function.update, Function.update_comp_eq_of_notMem_range', dite
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ InjOn (β := Set α) (fun (a : α) ↦ insert a s) sᶜ

Tactic:
fun _a ha _ _ =>
  (insert_inj ha).1

Premises used: Iff.mp, Set.InjOn, Set.insert_inj
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
h : range f = {b}
a : α
⊢ f a = b

Tactic:
simpa only [h, mem_singleton_iff] using mem_range_self (f := f) a

Premises used: Set.mem_range_self, Set.mem_singleton_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : MapsTo (⇑g : (a : α) → α) s t
a : α
ha : a ∈ s
simp_rw :
  Eq (α := β) ((↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) : β)
    ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
⊢ Eq (α := β)
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
        ((g : (a : α) → α) a : α) :
      β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
      β)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image]

Premises used: Equiv.Perm.extendDomain_apply_image, Function.comp_apply
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : MapsTo (⇑g : (a : α) → α) s t
a : α
ha : a ∈ s
⊢ Membership.mem (α := β) (γ := Set β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' t)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
      β)

Tactic:
exact ⟨_, h ha, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : SurjOn (⇑g : (a : α) → α) s t
a : α
ha : a ∈ t
obtain :
  ∀ (b : α) (hb : b ∈ s) (ha : Membership.mem (α := α) t ((g : (a : α) → α) b : α)),
    Membership.mem (γ := Set β)
      (image (α := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s))
      (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
        ((g : (a : α) → α) b : α))
⊢ Membership.mem (γ := Set β)
    (image (α := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
      (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s))
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a)

Tactic:
obtain ⟨b, hb, rfl⟩ := h ha

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : SurjOn (⇑g : (a : α) → α) s t
b : α
hb : b ∈ s
ha : Membership.mem (α := α) t ((g : (a : α) → α) b : α)
simp_rw :
  Eq (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) b) : β) : β)
    ((↑((f : (a : α) → Subtype p) ((g : (a : α) → α) b)) : β) : β)
⊢ Eq (α := β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) b) :
      β)
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
        ((g : (a : α) → α) b : α) :
      β)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image]

Premises used: Equiv.Perm.extendDomain_apply_image, Function.comp_apply
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : SurjOn (⇑g : (a : α) → α) s t
b : α
hb : b ∈ s
ha : Membership.mem (α := α) t ((g : (a : α) → α) b : α)
⊢ Membership.mem (γ := Set β)
    (image (α := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
      (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s))
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
      ((g : (a : α) → α) b : α))

Tactic:
exact ⟨_, ⟨_, hb, rfl⟩, by simp_rw [Function.comp_apply, extendDomain_apply_image]⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : BijOn (⇑g : (a : α) → α) s t
⊢ BijOn (α := β) (β := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' t)

Tactic:
⟨h.mapsTo.extendDomain, (g.extendDomain f).injective.injOn, h.surjOn.extendDomain⟩

Premises used: Equiv.Perm.extendDomain, Function.Injective.injOn, Set.SurjOn.extendDomain, Set.BijOn.surjOn, And.intro, Set.BijOn, Set.MapsTo.extendDomain, Set.BijOn.mapsTo, Equiv.injective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (β := α) (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) s
a : α
ha : a ∈ s
simp_rw :
  Eq (α := β)
    ((g₁.extendDomain (p := p) f : (a : β) → β)
        ((g₂.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β) :
      β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
simp_rw₁ :
  Eq.{u_2 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g₁ : (a : α) → α) ((g₂ : (a : α) → α) a : α))) : β)
    (↑((f : (a : α) → Subtype p) a) : β)
⊢ Eq (α := β)
    ((g₁.extendDomain (p := p) f : (a : β) → β)
        ((g₂.extendDomain (p := p) f : (a : β) → β)
            (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
          β) :
      β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a : β)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

Premises used: Equiv.Perm.extendDomain_apply_image, Function.comp_apply