awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : (∃ (y : α), f y = x) ∧ x ∈ s
⊢ x ∈ s'

Tactic:
aesop
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ image f = preimage g

Tactic:
funext fun s =>
    Subset.antisymm (image_subset_preimage_of_inverse h₁ s) (preimage_subset_image_of_inverse h₂ s)

Premises used: Set.image_subset_preimage_of_inverse, Set.Subset.antisymm, funext, Set.preimage_subset_image_of_inverse
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
hf : Involutive f
⊢ image f = preimage f

Tactic:
image_eq_preimage_of_inverse hf.leftInverse hf.rightInverse

Premises used: Function.Involutive.rightInverse, Set.image_eq_preimage_of_inverse, Function.Involutive.leftInverse
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
rw : b ∈ g ⁻¹' s ↔ g b ∈ s
rw₁ rw₂ : g b ∈ s ↔ g b ∈ s
⊢ b ∈ f '' s ↔ g b ∈ s

Tactic:
rw [image_eq_preimage_of_inverse h₁ h₂, mem_preimage]

Premises used: Set.image_eq_preimage_of_inverse, Set.mem_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Injective f
⊢ Disjoint (f '' s) (f '' sᶜ)

Tactic:
simp [disjoint_iff_inf_le, ← image_inter H]

Premises used: Set.image_inter, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
rw : f '' (s ∪ sᶜ) = univ
⊢ f '' s ∪ f '' sᶜ = univ

Tactic:
rw [← image_union]

Premises used: Set.image_union
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ

Tactic:
simp [image_univ_of_surjective H]

Premises used: Set.image_univ_of_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Bijective f
⊢ f '' sᶜ = (f '' s)ᶜ

Tactic:
Subset.antisymm (image_compl_subset H.1) (subset_image_compl H.2)

Premises used: Set.Subset.antisymm, Set.subset_image_compl, Set.image_compl_subset, And.right, And.left
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
rw : f '' s ⊆ f '' (t ∪ s)
⊢ f '' s \ f '' t ⊆ f '' (s \ t)

Tactic:
rw [diff_subset_iff, ← image_union, union_diff_self]

Premises used: Set.diff_subset_iff, Set.union_diff_self, Set.image_union
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)

Tactic:
image_mono subset_union_right

Premises used: Set.image_mono, Set.subset_union_right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)

Tactic:
exact image_mono subset_union_right

Premises used: Set.image_mono, Set.subset_union_right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t

Tactic:
(union_subset_union (subset_image_diff _ _ _) <| subset_image_diff _ _ _).trans
    (superset_of_eq (image_union _ _ _))

Premises used: Set.subset_image_diff, Set.union_subset_union, HasSubset.Subset.trans, superset_of_eq, symmDiff, Set.image_union
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' (s \ t) = f '' s \ f '' t

Tactic:
Subset.antisymm
    (Subset.trans (image_diff_subset f s t) <| inter_subset_inter_right _ <| image_compl_subset hf)
    (subset_image_diff f s t)

Premises used: Set.Subset.antisymm, Set.image_diff_subset, Set.inter_subset_inter_right, Set.subset_image_diff, Set.Subset.trans, Set.image_compl_subset
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
simp_rw : f '' (s \ t ∪ t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
simp_rw₁ : f '' (s \ t) ∪ f '' (t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)

Tactic:
simp_rw [Set.symmDiff_def, image_union, image_diff hf]

Premises used: Set.symmDiff_def, Set.image_diff, Set.image_union
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s).Nonempty ↔ s.Nonempty

Tactic:
⟨Nonempty.of_image, fun h => h.image f⟩

Premises used: Set.Nonempty.image, Iff.intro, Set.Nonempty.of_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : Surjective f
y : β
hy : y ∈ s
x : α
hx : f x = y
⊢ x ∈ f ⁻¹' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f_1 : α → β
s_1 t : Set α
f : α → β
s : Set α
inst : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Nonempty.{u_2 + 1} (↑(f '' s) : Type u_2)

Tactic:
(Set.Nonempty.image f .of_subtype).to_subtype

Premises used: Set.Nonempty.of_subtype, Set.Nonempty.to_subtype, Set.Nonempty.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s ⊆ t ↔ s ⊆ f ⁻¹' t

Tactic:
forall_mem_image

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.forall_mem_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' f ⁻¹' s ⊆ s

Tactic:
image_subset_iff.2 Subset.rfl

Premises used: Iff.mpr, Set.Subset.rfl, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ s ⊆ f ⁻¹' f '' s

Tactic:
fun _ =>
  mem_image_of_mem f

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.mem_image_of_mem, Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ f ⁻¹' f '' univ = univ

Tactic:
Subset.antisymm (fun _ _ => trivial) (subset_preimage_image f univ)

Premises used: Set.Subset.antisymm, trivial, Set.univ, Set.subset_preimage_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Injective f
⊢ f ⁻¹' f '' s = s

Tactic:
Subset.antisymm (fun _ ⟨_, hy, e⟩ => h e ▸ hy) (subset_preimage_image f s)

Premises used: Set.Subset.antisymm, _private.0.Set.preimage_image_eq.match_1, Membership.mem, Eq.rec, Set.subset_preimage_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Surjective f
x : β
hx : x ∈ s
y : α
e : f y = x
⊢ y ∈ f ⁻¹' s ∧ f y = x

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
rw : (fun (x : α) ↦ a) '' s ⊆ t ↔ a ∈ t
rw₁ : {a} ⊆ t ↔ a ∈ t
rw₂ rw₃ : a ∈ t ↔ a ∈ t
⊢ s ⊆ (fun (x : α) ↦ a) ⁻¹' t ↔ a ∈ t

Tactic:
rw [← image_subset_iff, hs.image_const, singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Set.Nonempty.image_const, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective ((Membership.mem ∘ preimage f) ∘ setOf) ↔ Surjective f

Tactic:
injective_comp_right_iff_surjective

Premises used: Set.Mem, setOf, Function.injective_comp_right_iff_surjective, Set.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective ((Membership.mem ∘ preimage f) ∘ setOf) ↔ Surjective f

Tactic:
exact injective_comp_right_iff_surjective

Premises used: Function.injective_comp_right_iff_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (Membership.mem ∘ preimage f ∘ setOf) ↔ Injective f

Tactic:
surjective_comp_right_iff_injective

Premises used: Set.Mem, setOf, Function.surjective_comp_right_iff_injective, Set.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Surjective (Membership.mem ∘ preimage f ∘ setOf) ↔ Injective f

Tactic:
exact surjective_comp_right_iff_injective

Premises used: Function.surjective_comp_right_iff_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hf : Surjective f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t

Tactic:
(preimage_injective.mpr hf).eq_iff

Premises used: Iff.mpr, Function.Injective.eq_iff, Set.preimage_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ f ⁻¹' t) = f '' s ∩ t

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (f ⁻¹' t ∩ s) = t ∩ f '' s

Tactic:
simp only [inter_comm, image_inter_preimage]

Premises used: Set.image_inter_preimage, Set.inter_comm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∩ f ⁻¹' t)).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
rw₁ rw₂ : (s ∩ f ⁻¹' t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty

Tactic:
rw [← image_inter_preimage, image_nonempty]

Premises used: Set.image_nonempty, Set.image_inter_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
simp_rw : f '' s ∩ t = ∅ ↔ s ∩ f ⁻¹' t = ∅
simp_rw₁ : ¬(f '' s ∩ t).Nonempty ↔ ¬(s ∩ f ⁻¹' t).Nonempty
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)

Tactic:
simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]

Premises used: Set.not_nonempty_iff_eq_empty, Set.disjoint_iff_inter_eq_empty, Set.image_inter_nonempty_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : Disjoint (f '' s) t ↔ Disjoint (f ⁻¹' t) s
rw₁ : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
rw₂ rw₃ : Disjoint s (f ⁻¹' t) ↔ Disjoint s (f ⁻¹' t)
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s

Tactic:
rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]

Premises used: Set.disjoint_image_left, disjoint_comm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
simp_rw : f '' (s ∩ (f ⁻¹' t)ᶜ) = f '' s ∩ tᶜ
simp_rw₁ : f '' (s ∩ f ⁻¹' tᶜ) = f '' s ∩ tᶜ
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t

Tactic:
simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]

Premises used: Set.image_inter_preimage, Set.diff_eq, Set.preimage_compl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (s : Set (Set α)) → Set (Set α)) (image compl) (preimage compl)

Tactic:
image_eq_preimage_of_inverse compl_compl compl_compl

Premises used: compl_compl, Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : Set α → Prop
⊢ Eq.{u_1 + 1} (α := Set (Set α)) (compl '' {s : Set α | p s}) {s : Set α | p sᶜ}

Tactic:
congr_fun compl_image {x | p x}

Premises used: Set.compl_image, Set.Mem, setOf, Set.preimage, congr_fun
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ s ∩ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∩ t)

Tactic:
fun _ h => ⟨mem_image_of_mem _ h.left, h.right⟩

Premises used: Set.Mem, setOf, Set.inter, Set.Subset, And.right, Set.preimage, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ s ∪ f ⁻¹' t ⊆ f ⁻¹' (f '' s ∪ t)

Tactic:
fun _ h =>
  Or.elim h (fun l => Or.inl <| mem_image_of_mem _ l) fun r => Or.inr r

Premises used: Set.Subset, Set.mem_image_of_mem, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∪ f ⁻¹' t) ⊆ f '' s ∪ t

Tactic:
image_subset_iff.2 (union_preimage_subset _ _ _)

Premises used: Iff.mpr, Set.image_subset_iff, Set.union_preimage_subset
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
A : Set α
B : Set β
f : α → β
⊢ f ⁻¹' B ⊆ A ↔ ∀ (a : α), f a ∈ B → a ∈ A

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
rw : f ⁻¹' f '' s = t
rw₁ : f ⁻¹' f '' s = f ⁻¹' f '' t
rw₂ rw₃ : f ⁻¹' f '' t = f ⁻¹' f '' t
⊢ s = t

Tactic:
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ (u : Set α), u ⊆ s ∧ f '' u = t

Tactic:
⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩

Premises used: Set.image_mono, Eq.rec, HasSubset.Subset, Inter.inter, Set.preimage, _private.0.Set.subset_image_iff.match_1, And.intro, Iff.intro, Exists.intro, Set.image, Eq.symm, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
refine : ∀ (h : t ⊆ f '' s), f '' (f ⁻¹' t ∩ s) = t
⊢ t ⊆ f '' s ↔ ∃ (u : Set α), u ⊆ s ∧ f '' u = t

Tactic:
refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
rwa : t ∩ f '' s = t
rwa₁ rwa₂ rwa₃ rwa₄ : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) = t

Tactic:
rwa [image_preimage_inter, inter_eq_left]

Premises used: Set.inter_eq_left, Set.image_preimage_inter
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∃ (t : Set β), t ⊆ f '' s ∧ p t) ↔ ∃ (t : Set α), t ⊆ s ∧ p (f '' t)

Tactic:
simp [subset_image_iff]

Premises used: Set.subset_image_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : Set β → Prop
⊢ (∀ (t : Set β), t ⊆ f '' s → p t) ↔ ∀ (t : Set α), t ⊆ s → p (f '' t)

Tactic:
simp [subset_image_iff]

Premises used: Set.subset_image_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
⊢ f '' s ⊆ f '' t ↔ s ⊆ t

Tactic:
grind [Set.image_subset_iff, Set.preimage_image_eq]

Premises used: Set.preimage_image_eq, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Setoid α
g : Quotient s → β
h : α → β
Hh : h = g ∘ Quotient.mk''
r : Set (β × β)
⊢ Eq.{u_1 + 1} (α := Set (Quotient s × Quotient s)) {x : Quotient s × Quotient s | (g x.1, g x.2) ∈ r}
    ((fun (a : α × α) ↦ (⟦a.1⟧, ⟦a.2⟧)) '' (fun (a : α × α) ↦ (h a.1, h a.2)) ⁻¹' r)

Tactic:
Hh.symm ▸
    Set.ext fun ⟨a₁, a₂⟩ =>
      ⟨Quot.induction_on₂ a₁ a₂ fun a₁ a₂ h => ⟨(a₁, a₂), h, rfl⟩, fun ⟨⟨b₁, b₂⟩, h₁, h₂⟩ =>
        show (g a₁, g a₂) ∈ r from
          have h₃ : ⟦b₁⟧ = a₁ ∧ ⟦b₂⟧ = a₂ := Prod.ext_iff.1 h₂
          h₃.1 ▸ h₃.2 ▸ h₁⟩

Premises used: Set.ext, _private.0.Set.prod_quotient_preimage_eq_image.match_2, setOf, Quotient.mk'', Function.comp, Membership.mem, Eq.rec, Prod.ext_iff, Prod.mk, Prod.fst, Quotient.mk, Quot.induction_on₂, Iff, And.right, Set.preimage, And.left, And.intro, _private.0.Set.prod_quotient_preimage_eq_image.match_1, Iff.intro, Exists.intro, Iff.mp, Set.image, Eq.symm, Prod.snd, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : Set α
P : β → Prop
⊢ (∃ (a : (↑(f '' x) : Type u_2)), P (↑a : β)) ↔ ∃ (a : (↑x : Type u_1)), P (f (↑a : α))

Tactic:
⟨fun ⟨a, h⟩ => ⟨⟨_, a.prop.choose_spec.1⟩, a.prop.choose_spec.2.symm ▸ h⟩, fun ⟨a, h⟩ =>
    ⟨⟨_, _, a.prop, rfl⟩, h⟩⟩

Premises used: Exists.choose_spec, _private.0.Set.exists_image_iff.match_2, Exists, Eq.rec, _private.0.Set.exists_image_iff.match_1, Subtype.mk, And.right, And.left, Subtype.prop, And.intro, Iff.intro, Exists.intro, Exists.choose, Eq.symm, Subtype.val, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ∘ imageFactorization f s = f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
funext fun _ => rfl

Premises used: funext, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Surjective (imageFactorization f s)

Tactic:
fun ⟨_, ⟨a, ha, rfl⟩⟩ => ⟨⟨a, ha⟩, rfl⟩

Premises used: Set.imageFactorization, Exists, Subtype.mk, _private.0.Set.imageFactorization_surjective.match_1, Exists.intro, Eq, Function.Surjective, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
h : ∀ (i : α), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
⊢ (⇑σ : (a : α) → α) '' s = s

Tactic:
ext i
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
h : ∀ (hi : (σ : (a : α) → α) i = i), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
h₁ : ∀ (hi : (σ : (a : α) → α) i ≠ i), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s

Tactic:
obtain hi | hi := eq_or_ne (σ i) i

Premises used: eq_or_ne, DFunLike.coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i = i
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s

Tactic:
⟨?_, fun h => ⟨i, h, hi⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i = i
h : Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i → i ∈ s
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s

Tactic:
refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i = i
j : α
hj : j ∈ s
h : (σ : (a : α) → α) j = i
h₁ h₂ h₃ h₄ : j ∈ s
⊢ i ∈ s

Tactic:
rwa [σ.injective (hi.trans h.symm)]

Premises used: Equiv.injective, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i ≠ i
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s

Tactic:
iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)

Premises used: Equiv.apply_symm_apply, iff_of_true, And.intro, Exists.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i ≠ i
h :
  ∀ (h : Eq (α := α) ((σ : (a : α) → α) ((Equiv.symm σ : (a : α) → α) i : α) : α) ((Equiv.symm σ : (a : α) → α) i : α)),
    (σ : (a : α) → α) i = i
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s

Tactic:
refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)

Premises used: iff_of_true
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i ≠ i
h : Eq (α := α) ((σ : (a : α) → α) ((Equiv.symm σ : (a : α) → α) i : α) : α) ((Equiv.symm σ : (a : α) → α) i : α)
⊢ (σ : (a : α) → α) i = i

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
h : ∀ (t : Set α), t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
ext t
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s
h₁ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
pos : ∀ (hs : a ∈ t), t ∈ 𝒫 s ∪ insert a '' 𝒫 s
neg : ∀ (hs : ¬a ∈ t), t ∈ 𝒫 s ∪ insert a '' 𝒫 s
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
by_cases hs : a ∈ t
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
pos : t ∈ insert a '' 𝒫 s
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t \ {a} ∈ 𝒫 s ∧ insert a (t \ {a}) = t

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ insert a '' 𝒫 s

Tactic:
refine ⟨t \ {a}, by grind⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : ¬a ∈ t
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
⊢ Disjoint (𝒫 s) (insert a '' 𝒫 s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
a : α
h : ¬a ∈ s
u : Set α
u_mem : u ∈ 𝒫 s
v : Set α
v_mem : v ∈ 𝒫 s
eq : insert a u = insert a v
⊢ u = v

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∀ (a : α), a ∈ range f → p a) ↔ ∀ (i : ι), p (f i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
p : (↑(range f) : Type u_1) → Prop
⊢ (∀ (a : (↑(range f) : Type u_1)), p a) ↔ ∀ (i : ι), p (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f i) ⋯)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
p : α → Prop
⊢ (∃ (a : α), a ∈ range f ∧ p a) ↔ ∃ (i : ι), p (f i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
p : (↑(range f) : Type u_1) → Prop
⊢ (∃ (a : (↑(range f) : Type u_1)), p a) ↔ ∃ (i : ι), p (Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f i) ⋯)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = univ ↔ Surjective f

Tactic:
eq_univ_iff_forall

Premises used: Set.Mem, Set.eq_univ_iff_forall, setOf, Set.range, Function.Surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
h : Surjective f
s : Set β
⊢ s ⊆ range f

Tactic:
Surjective.range_eq h ▸ subset_univ s

Premises used: Set.subset_univ, Eq.rec, Function.Surjective.range_eq, Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ f '' univ = range f

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
rw : f '' sᶜ = f '' univ \ f '' s
rw₁ : f '' sᶜ = f '' (univ \ s)
rw₂ rw₃ : f '' (univ \ s) = f '' (univ \ s)
⊢ f '' sᶜ = range f \ f '' s

Tactic:
rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]

Premises used: Set.image_univ, Set.image_diff, Set.compl_eq_univ_diff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
rw rw₁ : range f \ f '' s = range f \ f '' s
⊢ range f \ f '' s = f '' sᶜ

Tactic:
rw [image_compl_eq_range_diff_image hf]

Premises used: Set.image_compl_eq_range_diff_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : univ ⊆ f ⁻¹' s ↔ range f ⊆ s
rw₁ : f '' univ ⊆ s ↔ range f ⊆ s
rw₂ rw₃ : range f ⊆ s ↔ range f ⊆ s
⊢ f ⁻¹' s = univ ↔ range f ⊆ s

Tactic:
rw [← univ_subset_iff, ← image_subset_iff, image_univ]

Premises used: Set.univ_subset_iff, Set.image_univ, Set.image_subset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
rw : f '' s ⊆ f '' univ
⊢ f '' s ⊆ range f

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Tactic:
image_mono (subset_univ _)

Premises used: Set.subset_univ, Set.image_mono
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ

Tactic:
exact image_mono (subset_univ _)

Premises used: Set.subset_univ, Set.image_mono
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x : β
h : x ∈ f '' s
⊢ x ∈ range f

Tactic:
image_subset_range f s h

Premises used: Set.image_subset_range
-- Module: Mathlib.Data.Set.Image
Goal:
i : ℕ
⊢ i ∈ range Nat.succ → 0 < i

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set β
hs : s.Nonempty
f : α → β
hf : s ⊆ range f
w : β
hy : w ∈ s
x : α
hx : f x = w
⊢ x ∈ f ⁻¹' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ range (g ∘ f) = g '' range f

Tactic:
aesop