awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
p : Set γ
f : α → β
g : β → γ
hf : InjOn f s
⊢ BijOn (g ∘ f) s p ↔ BijOn g (f '' s) p

Tactic:
simp only [BijOn, InjOn.comp_iff, surjOn_comp_iff, mapsTo_image_iff, hf]

Premises used: Set.surjOn_comp_iff, Set.mapsTo_image_iff, Set.BijOn, Set.InjOn.comp_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
⊢ MapsTo f s t

Tactic:
obtain ⟨h1, h2, h3⟩ := hbij
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
⊢ InjOn f s

Tactic:
obtain ⟨h1, h2, h3⟩ := hbij
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
⊢ SurjOn f s t

Tactic:
obtain ⟨h1, h2, h3⟩ := hbij
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
⊢ BijOn g (p₁ '' s) (p₂ '' t)

Tactic:
⟨?_, hinj, ?_⟩

Premises used: And.intro, Set.BijOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
refine_1 : MapsTo g (p₁ '' s) (p₂ '' t)
refine_2 : SurjOn g (p₁ '' s) (p₂ '' t)
⊢ BijOn g (p₁ '' s) (p₂ '' t)

Tactic:
refine ⟨?_, hinj, ?_⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
rw rw₁ : g (p₁ a) = g (p₁ a)
⊢ p₂ (f a) = g (p₁ a)

Tactic:
rw [comm a]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
⊢ g (p₁ a) ∈ p₂ '' t

Tactic:
exact ⟨f a, h1 ha, by rw [comm a]⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
b : β
hb : b ∈ t
refine_2 : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), p₂ (f a) ∈ g '' p₁ '' s
⊢ p₂ b ∈ g '' p₁ '' s

Tactic:
obtain ⟨a, ha, rfl⟩ := h3 hb

Premises used: rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ p₂ (f a) ∈ g '' p₁ '' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Subsingleton α
inst_1 : Subsingleton β
f : α → β
h : s.Nonempty ↔ t.Nonempty
⊢ BijOn f s t

Tactic:
⟨mapsTo_of_subsingleton' _ h.1, injOn_of_subsingleton _ _, surjOn_of_subsingleton' _ h.2⟩

Premises used: Iff.mpr, Set.mapsTo_of_subsingleton', Set.surjOn_of_subsingleton', And.intro, Set.BijOn, Iff.mp, Set.injOn_of_subsingleton
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
inst : Subsingleton α
f : α → α
s : Set α
⊢ BijOn f s s

Tactic:
bijOn_of_subsingleton' _ Iff.rfl

Premises used: Iff.rfl, Set.bijOn_of_subsingleton'
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : BijOn f s t
⊢ Bijective (MapsTo.restrict f s t ⋯)

Tactic:
⟨fun x y h' => Subtype.ext <| h.injOn x.2 y.2 <| Subtype.ext_iff.1 h', fun ⟨_, hy⟩ =>
    let ⟨x, hx, hxy⟩ := h.surjOn hy
    ⟨⟨x, hx⟩, Subtype.ext hxy⟩⟩

Premises used: Exists, Set.BijOn.injOn, Subtype.ext_iff, Subtype.mk, Set.BijOn.surjOn, _private.0.Set.SurjOn.forall.match_1, And.intro, Exists.intro, Iff.mp, Set.BijOn.mapsTo, Function.Bijective, _private.0.Set.BijOn.bijective.match_1, Set.MapsTo.restrict, Eq, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ BijOn f univ univ ↔ Bijective f

Tactic:
simp [Bijective, BijOn]

Premises used: Set.BijOn, Function.Bijective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : Injective f
⊢ BijOn f s (f '' s)

Tactic:
hf.injOn.bijOn_image

Premises used: Function.Injective.injOn, Set.InjOn.bijOn_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Surjective f
⊢ SurjOn f (f ⁻¹' t) t

Tactic:
hf.surjOn.preimage

Premises used: Set.SurjOn.preimage, Function.Surjective.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Bijective f
⊢ BijOn f (f ⁻¹' t) t

Tactic:
⟨fun _ ↦ id, hf.injective.injOn, hf.surjective.surjOn_preimage⟩

Premises used: Function.Injective.injOn, id, Function.Bijective.injective, Function.Bijective.surjective, And.intro, Set.BijOn, Function.Surjective.surjOn_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hst : BijOn f s t
hf : Bijective f
⊢ BijOn f sᶜ tᶜ

Tactic:
⟨hst.surjOn.mapsTo_compl hf.1, hf.1.injOn, hst.mapsTo.surjOn_compl hf.2⟩

Premises used: Set.SurjOn.mapsTo_compl, Function.Injective.injOn, Set.BijOn.surjOn, And.right, And.left, And.intro, Set.BijOn, Set.BijOn.mapsTo, Set.MapsTo.surjOn_compl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩

Premises used: Set.inter_subset_left, Set.BijOn.injOn, And.intro, Set.BijOn, Set.InjOn.mono, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
refine : ∀ (x : β) (hx : x ∈ r), x ∈ f '' (s ∩ f ⁻¹' r)
⊢ BijOn f (s ∩ f ⁻¹' r) r

Tactic:
refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
x : β
hx : x ∈ r
obtain : ∀ (y : α) (hy : y ∈ s) (hx : f y ∈ r), f y ∈ f '' (s ∩ f ⁻¹' r)
⊢ x ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)

Premises used: Set.BijOn.surjOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
⟨y, ⟨hy, 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
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
y : α
hy : y ∈ s
hx : f y ∈ r
⊢ f y ∈ f '' (s ∩ f ⁻¹' r)

Tactic:
exact ⟨y, ⟨hy, hx⟩, rfl⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set α
hf : BijOn f s t
hrs : r ⊆ s
⊢ BijOn f r (f '' r)

Tactic:
(hf.injOn.mono hrs).bijOn_image

Premises used: Set.InjOn.bijOn_image, Set.BijOn.injOn, Set.InjOn.mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
⊢ Eq.{u_2 + 1} (α := Set β) ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) (f '' s)))
    ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) t))

Tactic:
have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this :
  Eq.{u_2 + 1} (α := Set β) ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) (f '' s)))
    ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) t))
⊢ f '' s \ {f a} = t \ {f a}

Tactic:
simp only [mem_singleton_iff, insert_diff_of_mem] at this

Premises used: Set.insert_diff_of_mem, Set.mem_singleton_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
rw : ∀ (this : f '' s = t), BijOn f s t
rw₁ : ∀ (this : f '' s \ {f a} = t), ¬f a ∈ f '' s
⊢ BijOn f s t

Tactic:
rw [diff_singleton_eq_self hfa, diff_singleton_eq_self] at this

Premises used: Set.diff_singleton_eq_self
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ MapsTo f s t

Tactic:
simp [← this, mapsTo_iff_image_subset]

Premises used: Set.mapsTo_iff_image_subset
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ SurjOn f s t

Tactic:
simp [← this, surjOn_image]

Premises used: Set.surjOn_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s = t
⊢ BijOn f s t

Tactic:
exact ⟨by simp [← this, mapsTo_iff_image_subset], h.injOn.mono (subset_insert ..),
        by simp [← this, surjOn_image]⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
simp : ∀ (x : α), x ∈ s → ¬f x = f a
⊢ ¬f a ∈ f '' s

Tactic:
simp only [mem_image, not_exists, not_and]

Premises used: Set.mem_image, not_exists, not_and
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ a ∈ insert a s

Tactic:
simp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
rw : ¬x = a
⊢ ¬f x = f a

Tactic:
rw [h.injOn.eq_iff (by simp [hx]) (by simp)]

Premises used: Set.InjOn.eq_iff, Set.BijOn.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬x = a

Tactic:
ha ∘ (· ▸ hx)

Premises used: Function.comp, Eq.rec, Not
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬x = a

Tactic:
exact ha ∘ (· ▸ hx)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
(bijOn_singleton.mpr rfl).union h ?_

Premises used: Iff.mpr, Set.bijOn_singleton, Set.BijOn.union, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
refine : InjOn f ({a} ∪ s)
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
refine (bijOn_singleton.mpr rfl).union h ?_

Premises used: Iff.mpr, Set.bijOn_singleton, Set.BijOn.union, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
simp : ∀ (x : α), x ∈ s → ¬f x = f a
⊢ InjOn f ({a} ∪ s)

Tactic:
simp only [singleton_union, injOn_insert fun x ↦ (hfa (h.mapsTo x)), h.injOn, mem_image,
      not_exists, not_and, true_and]

Premises used: Set.mem_image, Set.singleton_union, not_exists, Set.BijOn.injOn, Set.injOn_insert, Set.BijOn.mapsTo, not_and, true_and
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ ∀ (x : α), x ∈ s → ¬f x = f a

Tactic:
fun _ hx h₂ ↦ hfa (h₂ ▸ h.mapsTo hx)

Premises used: Eq.rec, Set.BijOn.mapsTo, Not
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ ∀ (x : α), x ∈ s → ¬f x = f a

Tactic:
exact fun _ hx h₂ ↦ hfa (h₂ ▸ h.mapsTo hx)
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : ¬f a ∈ t
⊢ BijOn f (Insert.insert a s) (Insert.insert (f a) t)

Tactic:
(insert_iff (h₂ <| h₁.mapsTo ·) h₂).mpr h₁

Premises used: Iff.mpr, Set.BijOn.insert_iff, Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (f '' (s \ {a}))

Tactic:
h₁.subset_left diff_subset

Premises used: Set.diff_subset, Set.BijOn.subset_left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
h : t \ {f a} = f '' (s \ {a})
⊢ BijOn f (s \ {a}) (t \ {f a})

Tactic:
convert! h₁.subset_left diff_subset

Premises used: Set.diff_subset, Set.BijOn.subset_left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ t \ {f a} = f '' (s \ {a})

Tactic:
simp [h₁.injOn.image_diff, h₁.image_eq, h₂, inter_eq_self_of_subset_right]

Premises used: Set.InjOn.image_diff, Set.BijOn.image_eq, Set.BijOn.injOn, Set.inter_eq_self_of_subset_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
h : LeftInvOn f' f s
⊢ EqOn (f' ∘ f) id s

Tactic:
h

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
h : LeftInvOn f' f s
x : α
hx : x ∈ s
⊢ f' (f x) = x

Tactic:
h hx
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f₁' f₂' : β → α
h₁ : LeftInvOn f₁' f s
t : Set β
h₁' : MapsTo f s t
heq : EqOn f₁' f₂' t
⊢ LeftInvOn f₂' f s

Tactic:
fun _ hx => heq (h₁' hx) ▸ h₁ hx

Premises used: Set.LeftInvOn, Eq.rec
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
f₁' : β → α
h₁ : LeftInvOn f₁' f₁ s
heq : EqOn f₁ f₂ s
⊢ LeftInvOn f₁' f₂ s

Tactic:
fun _ hx => heq hx ▸ h₁ hx

Premises used: Set.LeftInvOn, Eq.rec
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f₁' : β → α
h : LeftInvOn f₁' f s
⊢ InjOn f s

Tactic:
fun x₁ h₁ x₂ h₂ heq =>
  calc
    x₁ = f₁' (f x₁) := Eq.symm <| h h₁
    _ = f₁' (f x₂) := congr_arg f₁' heq
    _ = x₂ := h h₂

Premises used: Trans.trans, congr_arg, Set.InjOn, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : MapsTo f s t
⊢ SurjOn f' t s

Tactic:
fun x hx =>
  ⟨f x, hf hx, h hx⟩

Premises used: Set.Mem, setOf, Set.SurjOn, Set.Subset, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
let : ∀ (x : α) (hs : x ∈ s) (hx : f x = y), f' y ∈ s
⊢ f' y ∈ s

Tactic:
let ⟨x, hs, hx⟩ := hf hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
rwa : f' (f x) ∈ s
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ s
⊢ f' y ∈ s

Tactic:
rwa [← hx, h hs]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ LeftInvOn id id s

Tactic:
fun _ _ ↦ rfl

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

Tactic:
fun x h =>
  calc
    (f' ∘ g') ((g ∘ f) x) = f' (f x) := congr_arg f' (hg' (hf h))
    _ = x := hf' h

Premises used: Set.LeftInvOn, Trans.trans, congr_arg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
ht : s₁ ⊆ s
⊢ LeftInvOn f' f s₁

Tactic:
fun _ hx =>
  hf (ht hx)

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

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
rwa : f' (f x) ∈ s₁
rwa₁ rwa₂ rwa₃ rwa₄ : x ∈ s₁
⊢ f x ∈ f' ⁻¹' s₁

Tactic:
rwa [mem_preimage, hf h]

Premises used: Set.mem_preimage
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁ ∩ f '' s

Tactic:
exact ⟨by rwa [mem_preimage, hf h], mem_image_of_mem _ h⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
rwa rwa₁ rwa₂ rwa₃ : f' (f x) ∈ s₁
⊢ x ∈ s₁

Tactic:
rwa [← hf h]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f '' (s₁ ∩ s)

Tactic:
exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
rw : f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
rw [hf.image_inter']

Premises used: Set.LeftInvOn.image_inter'
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))

Premises used: Set.Subset.antisymm, Set.inter_subset_left, Set.inter_subset_inter_left, Set.preimage_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
refine : f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))

Premises used: Set.Subset.antisymm, Set.inter_subset_left, Set.inter_subset_inter_left, Set.preimage_mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ f' (f x) ∈ s

Tactic:
rwa [hf hx]
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
hx : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ f x ∈ f' ⁻¹' (s₁ ∩ s) ∩ f '' s

Tactic:
exact ⟨⟨h₁, by rwa [hf hx]⟩, mem_image_of_mem _ hx⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
rw : (fun (x : α) ↦ f' (f x)) '' s = s
rw₁ : (fun (a : α) ↦ a) '' s = s
rw₂ rw₃ : s = s
⊢ f' '' f '' s = s

Tactic:
rw [Set.image_image, image_congr hf, image_id']

Premises used: Set.image_image, Set.image_id', Set.image_congr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
hs : s₁ ⊆ s
⊢ f' '' f '' s₁ = s₁

Tactic:
(hf.mono hs).image_image

Premises used: Set.LeftInvOn.mono, Set.LeftInvOn.image_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
f' : β → α
h : RightInvOn f' f t
⊢ EqOn (f ∘ f') id t

Tactic:
h

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
f' : β → α
h : RightInvOn f' f t
y : β
hy : y ∈ t
⊢ f (f' y) = y

Tactic:
h hy
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
h : LeftInvOn f' f s
⊢ RightInvOn f' f (f '' s)

Tactic:
fun _y ⟨_x, hx, heq⟩ => heq ▸ (congr_arg f <| h.eq hx)

Premises used: Set.LeftInvOn, Set.LeftInvOn.eq, Eq.rec, congr_arg, _private.0.Set.SurjOn.forall.match_1, Eq
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
f₁' f₂' : β → α
h₁ : RightInvOn f₁' f t
heq : EqOn f₁' f₂' t
⊢ RightInvOn f₂' f t

Tactic:
h₁.congr_right heq

Premises used: Set.LeftInvOn.congr_right
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
f' : β → α
h₁ : RightInvOn f' f₁ t
hg : MapsTo f' t s
heq : EqOn f₁ f₂ s
⊢ RightInvOn f' f₂ t

Tactic:
LeftInvOn.congr_left h₁ hg heq

Premises used: Set.LeftInvOn.congr_left
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : RightInvOn f' f t
hf' : MapsTo f' t s
⊢ SurjOn f s t

Tactic:
LeftInvOn.surjOn hf hf'

Premises used: Set.LeftInvOn.surjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : RightInvOn f' f t
hf : SurjOn f' t s
⊢ MapsTo f s t

Tactic:
LeftInvOn.mapsTo h hf

Premises used: Set.LeftInvOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ RightInvOn id id s

Tactic:
fun _ _ ↦ rfl

Premises used: Set.LeftInvOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Set β
p : Set γ
f : α → β
g : β → γ
f' : β → α
g' : γ → β
hf : RightInvOn f' f t
hg : RightInvOn g' g p
g'pt : MapsTo g' p t
⊢ RightInvOn (f' ∘ g') (g ∘ f) p

Tactic:
LeftInvOn.comp hg hf g'pt

Premises used: Set.LeftInvOn.comp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t t₁ : Set β
f : α → β
f' : β → α
hf : RightInvOn f' f t
ht : t₁ ⊆ t
⊢ RightInvOn f' f t₁

Tactic:
LeftInvOn.mono hf ht

Premises used: Set.LeftInvOn.mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : InjOn f s
hf' : LeftInvOn f f' t
h₁ : MapsTo f s t
h₂ : MapsTo f' t s
⊢ RightInvOn f f' s

Tactic:
fun _ h =>
  hf (h₂ <| h₁ h) h (hf' (h₁ h))

Premises used: Set.LeftInvOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f₁' f₂' : β → α
h₁ : LeftInvOn f₁' f s
h₂ : RightInvOn f₂' f t
h : MapsTo f₂' t s
⊢ EqOn f₁' f₂' t

Tactic:
fun y hy =>
  calc
    f₁' y = (f₁' ∘ f ∘ f₂') y := congr_arg f₁' (h₂ hy).symm
    _ = f₂' y := h₁ (h hy)

Premises used: Trans.trans, Set.EqOn, congr_arg, Eq.symm
-- 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
let : ∀ (x : α) (hx : x ∈ s) (heq : f x = y), f (f' y) = y
⊢ f (f' y) = y

Tactic:
let ⟨x, hx, heq⟩ := hf hy