awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Image
Goal:
β : Type u_2
ι : Sort u_4
f : ι → β
a : ι
⊢ (↑(rangeFactorization f a) : β) = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
β : Type u_2
ι : Sort u_4
f : ι → β
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ range f) ∘ rangeFactorization f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : ∀ (x : β), x ∈ f '' s ↔ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
⊢ f '' s = range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x : β
h : x ∈ f '' s → Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
h₁ : Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x → x ∈ f '' s
⊢ x ∈ f '' s ↔ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x_1 : β
x : α
h1 : x ∈ s
h2 : f x = x_1
⊢ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x_1

Tactic:
⟨⟨x, h1⟩, h2⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x_1 : β
x : α
h1 : x ∈ s
h2 : f x = x_1
⊢ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x_1

Tactic:
exact ⟨⟨x, h1⟩, h2⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x_1 : β
x : α
h1 : x ∈ s
h2 : (fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h1) = x_1
⊢ x_1 ∈ f '' s

Tactic:
⟨x, h1, h2⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x_1 : β
x : α
h1 : x ∈ s
h2 : (fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h1) = x_1
⊢ x_1 ∈ f '' s

Tactic:
exact ⟨x, h1, h2⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ⊕ β → γ
⊢ range f = range (f ∘ Sum.inl) ∪ range (f ∘ Sum.inr)

Tactic:
ext fun _ => Sum.exists

Premises used: Set.ext, Sum.exists
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
⊢ range (Sum.elim f g) = range f ∪ range g

Tactic:
Sum.range_eq _

Premises used: Sum.range_eq, Sum.elim
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : Prop
inst : Decidable p
f g : α → β
⊢ range (if p then f else g) ⊆ range f ∪ range g

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f g : α → β
⊢ (range fun (x : α) ↦ if p x then f x else g x) ⊆ range f ∪ range g

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ f ⁻¹' range f = univ

Tactic:
eq_univ_of_forall mem_range_self

Premises used: Set.mem_range_self, Set.eq_univ_of_forall
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Unique ι
⊢ range f = {f default}

Tactic:
aesop (add simp [Unique.eq_default])

Premises used: Unique.eq_default
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x : α
f : (↑{x} : Type u_1) → β
⊢ range f = {f (Subtype.mk (p := fun (x_1 : α) ↦ Membership.mem (γ := Set α) {x} x_1) x ⋯)}

Tactic:
range_unique

Premises used: Set.range_unique
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x : α
s : Set α
f : (↑(insert x s) : Type u_1) → β
⊢ range f =
    insert (f (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x s) x ⋯))
      (range fun (y : (↑s : Type u_1)) ↦ f (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ insert x s) (↑y : α) ⋯))

Tactic:
aesop
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ range f \ f '' s ⊆ f '' sᶜ

Tactic:
fun _ ⟨⟨x, h₁⟩, h₂⟩ => ⟨x, fun h => h₂ ⟨x, h, h₁⟩, h₁⟩

Premises used: Compl.compl, Membership.mem, _private.0.Set.range_diff_image_subset.match_1, Set.Subset, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
h₁ :
  ∀ (x : α) (hx : x ∈ t),
    Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ range (inclusion (s := s) (t := t) h) ↔
      Membership.mem (γ := Set (↑t : Type u_1)) {x : (↑t : Type u_1) | (↑x : α) ∈ s}
        (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)
⊢ range (inclusion (s := s) (t := t) h) = {x : (↑t : Type u_1) | (↑x : α) ∈ s}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ range (inclusion (s := s) (t := t) h) ↔
    Membership.mem (γ := Set (↑t : Type u_1)) {x : (↑t : Type u_1) | (↑x : α) ∈ s}
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : (↑(range f) : Type u_2)
a : (↑(rangeFactorization f (rangeSplitting f x)) : β) = (↑x : β)
⊢ rangeFactorization f (rangeSplitting f x) = x

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : (↑(range f) : Type u_2)
a : f (rangeSplitting f x) = (↑x : β)
⊢ (↑(rangeFactorization f (rangeSplitting f x)) : β) = (↑x : β)

Tactic:
simp only [rangeFactorization_coe]

Premises used: Set.rangeFactorization_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : (↑(range f) : Type u_2)
⊢ f (rangeSplitting f x) = (↑x : β)

Tactic:
apply apply_rangeSplitting

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Injective (rangeSplitting f)

Tactic:
(leftInverse_rangeSplitting f).injective

Premises used: Function.LeftInverse.injective, Set.leftInverse_rangeSplitting
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
h : Injective f
⊢ RightInverse (rangeFactorization f) (rangeSplitting f)

Tactic:
(leftInverse_rangeSplitting f).rightInverse_of_injective fun _ _ hxy =>
    h <| Subtype.ext_iff.1 hxy

Premises used: Subtype.ext_iff, Function.LeftInverse.rightInverse_of_injective, Iff.mp, Set.leftInverse_rangeSplitting
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ LeftInverse (rangeSplitting f) (rangeFactorization f) ↔ Injective f

Tactic:
⟨(rangeFactorization_injective.mp ·.injective),
    fun h ↦ congrFun' (rightInverse_rangeSplitting h).id⟩

Premises used: Function.LeftInverse.injective, Function.RightInverse.id, Set.rightInverse_rangeSplitting, Iff.intro, Iff.mp, Set.rangeFactorization_injective, congrFun'
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ preimage (rangeSplitting f) = image (rangeFactorization f)

Tactic:
(image_eq_preimage_of_inverse (rightInverse_rangeSplitting hf)
      (leftInverse_rangeSplitting f)).symm

Premises used: Set.rightInverse_rangeSplitting, Set.image_eq_preimage_of_inverse, Set.leftInverse_rangeSplitting, Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
⊢ IsCompl (α := Set (Option α)) (range some) {none}

Tactic:
IsCompl.of_le (fun _ ⟨⟨_, ha⟩, (hn : _ = none)⟩ => Option.some_ne_none _ (ha.trans hn))
    fun x _ => Option.casesOn x (Or.inr rfl) fun _ => Or.inl <| mem_range_self _

Premises used: Option.casesOn, Membership.mem, _private.0.Set.isCompl_range_some_none.match_1, Bot.bot, Option.some_ne_none, IsCompl.of_le, Eq.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
⊢ Eq (α := Set (Option α)) (range some)ᶜ {none}

Tactic:
(isCompl_range_some_none α).compl_eq

Premises used: Set.isCompl_range_some_none, IsCompl.compl_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
⊢ Eq (α := Set (Option α)) (range some ∩ {none}) ∅

Tactic:
(isCompl_range_some_none α).inf_eq_bot

Premises used: Set.isCompl_range_some_none, IsCompl.inf_eq_bot
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
⊢ Eq (α := Set (Option α)) (range some ∪ {none}) univ

Tactic:
(isCompl_range_some_none α).sup_eq_top

Premises used: IsCompl.sup_eq_top, Set.isCompl_range_some_none
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
⊢ Eq (α := Set (Option α)) (insert none (range some)) univ

Tactic:
(isCompl_range_some_none α).symm.sup_eq_top

Premises used: IsCompl.sup_eq_top, Set.union, Set.insert, Set.isCompl_range_some_none, Set.Mem, setOf, Set.singleton, IsCompl.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
rw₈ : h '' s = h '' (s ∩ range f ∪ s ∩ range g)
rw₉ : h '' s = h '' (s ∩ (range f ∪ range g))
rw₁₀ : h '' s = h '' (s ∩ univ)
rw₁₁ rw₁₂ : h '' s = h '' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s

Tactic:
rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]

Premises used: Set.inter_univ, Set.image_preimage_eq_inter_range, Set.image_comp, Set.inter_union_distrib_left, Set.image_union
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Subsingleton
f : α → β
⊢ (f '' s).Subsingleton

Tactic:
fun _ ⟨_, hx, Hx⟩ _ ⟨_, hy, Hy⟩ => Hx ▸ Hy ▸ congr_arg f (hs hx hy)

Premises used: Eq.rec, congr_arg, Set.Subsingleton, _private.0.Set.Subsingleton.image.match_1, Eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Subsingleton
hf : Injective f
⊢ (f ⁻¹' s).Subsingleton

Tactic:
fun _ ha _ hb => hf <| hs ha hb

Premises used: Set.Subsingleton
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
hs : (f '' s).Subsingleton
⊢ s.Subsingleton

Tactic:
(hs.preimage hf).anti <| subset_preimage_image _ _

Premises used: Set.Subsingleton.anti, Set.subset_preimage_image, Set.Subsingleton.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
rcases : ∀ (x : α) (hx : f x ∈ s) (y : α) (hy : f y ∈ s), f x = f y
⊢ fx = fy

Tactic:
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y

Tactic:
congr_arg f (hs hx hy)

Premises used: congr_arg
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y

Tactic:
exact congr_arg f (hs hx hy)

Premises used: congr_arg
-- Module: Mathlib.Data.Set.Image
Goal:
β : Type u_2
α : Sort u_5
inst : Subsingleton α
f : α → β
⊢ (range f).Subsingleton

Tactic:
forall_mem_range.2 fun x => forall_mem_range.2 fun y => congr_arg f (Subsingleton.elim x y)

Premises used: Iff.mpr, Set.forall_mem_range, congr_arg, Set.Subsingleton, Subsingleton.elim
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
rcases : ∀ (fx : β) (hx : fx ∈ s) (fy : β) (hy : fy ∈ s) (hxy : fx ≠ fy), (f ⁻¹' s).Nontrivial
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hs with ⟨fx, hx, fy, hy, hxy⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
rcases : ∀ (x : α) (hx : f x ∈ s) (y : α) (hy : f y ∈ s) (hxy : f x ≠ f y), (f ⁻¹' s).Nontrivial
⊢ (f ⁻¹' s).Nontrivial

Tactic:
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ (f ⁻¹' s).Nontrivial

Tactic:
⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

Premises used: mt, congr_arg, And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ (f ⁻¹' s).Nontrivial

Tactic:
exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : Injective f
⊢ (f '' s).Nontrivial

Tactic:
let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨f x, mem_image_of_mem f hx, f y, mem_image_of_mem f hy, hf.ne hxy⟩

Premises used: _private.0.Set.Nontrivial.image.match_1, Function.Injective.ne, Set.mem_image_of_mem, And.intro, Exists.intro, Set.image, Set.Nontrivial
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
obtain : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), (f '' s).Nontrivial
⊢ (f '' s).Nontrivial

Tactic:
obtain ⟨x, hx, y, hy, hxy⟩ := hs
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (f '' s).Nontrivial

Tactic:
⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ (f '' s).Nontrivial

Tactic:
exact ⟨f x, mem_image_of_mem _ hx, f y, mem_image_of_mem _ hy, (hxy <| hf hx hy ·)⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
hs : (f '' s).Nontrivial
⊢ s.Nontrivial

Tactic:
let ⟨_, ⟨x, hx, rfl⟩, _, ⟨y, hy, rfl⟩, hxy⟩ := hs
  ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩

Premises used: mt, _private.0.Set.nontrivial_of_image.match_1, congr_arg, And.intro, Exists.intro, Set.Nontrivial
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : Injective f
⊢ (f '' s).Nontrivial ↔ s.Nontrivial

Tactic:
⟨nontrivial_of_image f s, fun h ↦ h.image hf⟩

Premises used: Set.Nontrivial.image, Set.nontrivial_of_image, Iff.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hf : InjOn f s
⊢ (f '' s).Nontrivial ↔ s.Nontrivial

Tactic:
⟨nontrivial_of_image f s, fun h ↦ h.image_of_injOn hf⟩

Premises used: Set.nontrivial_of_image, Set.Nontrivial.image_of_injOn, Iff.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set β
hs : (f ⁻¹' s).Nontrivial
⊢ s.Nontrivial

Tactic:
(hs.image hf).mono <| image_preimage_subset _ _

Premises used: Set.Nontrivial.image, Set.image_preimage_subset, Set.Nontrivial.mono
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Injective (preimage f)

Tactic:
fun _ _ =>
  (preimage_eq_preimage hf).1

Premises used: Set.preimage_eq_preimage, Iff.mp, Function.Injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f ⁻¹' f '' s = s

Tactic:
preimage_image_eq s hf

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Surjective (preimage f)

Tactic:
Set.preimage_surjective.mpr hf

Premises used: Iff.mpr, Set.preimage_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s).Subsingleton ↔ s.Subsingleton

Tactic:
⟨subsingleton_of_image hf s, fun h => h.image f⟩

Premises used: Set.Subsingleton.image, Set.subsingleton_of_image, Iff.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' f ⁻¹' s = s

Tactic:
image_preimage_eq s hf

Premises used: Set.image_preimage_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
h : f '' f ⁻¹' s = s
⊢ ∃ (a : Set α), f '' a = s

Tactic:
use f ⁻¹' s
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
h h₁ : s = s
⊢ f '' f ⁻¹' s = s

Tactic:
rw [hf.image_preimage]

Premises used: Function.Surjective.image_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
rw : (f '' f ⁻¹' s).Nonempty ↔ s.Nonempty
rw₁ : Type u_2
rw₂ : α → β
rw₃ rw₄ : s.Nonempty ↔ s.Nonempty
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty

Tactic:
rw [← image_nonempty, hf.image_preimage]

Premises used: Set.image_nonempty, Function.Surjective.image_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : 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, h]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
inj : Injective f
⊢ StrictMono (image f)

Tactic:
monotone_image.strictMono_of_injective inj.image_injective

Premises used: Monotone.strictMono_of_injective, Set.monotone_image, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
apply Set.preimage_subset_preimage_iff

Premises used: Set.preimage_subset_preimage_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
hs : s ⊆ univ
⊢ s ⊆ range f

Tactic:
rw [hf.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ univ

Tactic:
apply subset_univ

Premises used: Set.subset_univ
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_3
ι' : Sort u_4
f : ι → ι'
hf : Surjective f
g : ι' → α
⊢ range (g ∘ f) = range g

Tactic:
ext fun y => (@Surjective.exists _ _ _ hf fun x => g x = y).symm

Premises used: Set.ext, Function.Surjective.exists, Iff.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
b : β
⊢ b ∈ range f ↔ ∃! a : α, f a = b

Tactic:
⟨fun ⟨a, h⟩ => ⟨a, h, fun _ ha => hf (ha.trans h.symm)⟩, ExistsUnique.exists⟩

Premises used: ExistsUnique.exists, _private.0.Set.Nonempty.preimage'.match_1, ExistsUnique, And.intro, Iff.intro, Exists.intro, Eq.symm, Eq, Eq.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ (f '' s)ᶜ = f '' sᶜ ∪ (range f)ᶜ

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f '' s = s
rw₁ : id '' s = s
rw₂ rw₃ : s = s
⊢ g '' f '' s = s

Tactic:
rw [← image_comp, h.comp_eq_id, image_id]

Premises used: Function.LeftInverse.comp_eq_id, Set.image_comp, Set.image_id
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f ⁻¹' s = s
rw₁ : id ⁻¹' s = s
rw₂ rw₃ : s = s
⊢ f ⁻¹' g ⁻¹' s = s

Tactic:
rw [← preimage_comp, h.comp_eq_id, preimage_id]

Premises used: Set.preimage_id, Set.preimage_comp, Function.LeftInverse.comp_eq_id
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
hf : Involutive f
⊢ Involutive (preimage f)

Tactic:
hf.rightInverse.preimage_preimage

Premises used: Function.Involutive.rightInverse, Function.LeftInverse.preimage_preimage, Function.Involutive
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
rw : f '' s = f '' f ⁻¹' g ⁻¹' s
rw₁ rw₂ : f '' s = f '' s
⊢ f '' s = range f ∩ g ⁻¹' s

Tactic:
rw [← image_preimage_eq_range_inter, hfg.preimage_preimage]

Premises used: Function.LeftInverse.preimage_preimage, Set.image_preimage_eq_range_inter
-- Module: Mathlib.Data.Set.Image
Goal:
ι : Sort u_1
ι' : Sort u_2
E : Type u_3
inst : EquivLike E ι ι'
α : Type u_4
f : ι' → α
e : E
⊢ range.{u_4, u_1} (ι := ι) (f ∘ (⇑e : (a : ι) → ι')) = range f

Tactic:
(EquivLike.surjective _).range_comp _

Premises used: Function.Surjective.range_comp, EquivLike.surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
⊢ val (p := p) '' s = {x : α | ∃ (h : p x), mk (p := p) x h ∈ s}

Tactic:
Set.ext fun a =>
    ⟨fun ⟨⟨_, ha'⟩, in_s, h_eq⟩ => h_eq ▸ ⟨ha', in_s⟩, fun ⟨ha, in_s⟩ => ⟨⟨a, ha⟩, in_s, rfl⟩⟩

Premises used: Set.ext, setOf, Membership.mem, Exists, Eq.rec, _private.0.Subtype.coe_image.match_1, Subtype.mk, _private.0.Subtype.coe_image.match_2, And.intro, Iff.intro, Exists.intro, Set.image, Subtype.val, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
h : t ⊆ s
h₁ :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (image (α := (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s)) {x : (↑s : Type u_1) | (↑x : α) ∈ t}) x ↔
      x ∈ t
⊢ image (α := (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s)) {x : (↑s : Type u_1) | (↑x : α) ∈ t} = t

Tactic:
ext x
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ (x_1 : (↑s : Type u_1)),
      Membership.mem (γ := Set (↑s : Type u_1)) {x : (↑s : Type u_1) | (↑x : α) ∈ t} x_1 ∧ (↑x_1 : α) = x) ↔
    x ∈ t

Tactic:
⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

Premises used: Membership.mem, Eq.rec, Subtype.mk, And.intro, Iff.intro, Exists.intro, _private.0.Subtype.coe_image_of_subset.match_1, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ (x_1 : (↑s : Type u_1)),
      Membership.mem (γ := Set (↑s : Type u_1)) {x : (↑s : Type u_1) | (↑x : α) ∈ t} x_1 ∧ (↑x_1 : α) = x) ↔
    x ∈ t

Tactic:
exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
rw : image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ = s
⊢ range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) = s

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ = s

Tactic:
simp [-image_univ, coe_image]

Premises used: Subtype.coe_image, Set.image_univ
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) = s

Tactic:
range_coe

Premises used: Subtype.range_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
⊢ Eq.{u_1 + 1} (α := Set α) (range (ι := Subtype p) (val (p := p))) {x : α | p x}

Tactic:
range_coe

Premises used: Set.Mem, setOf, Subtype.range_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
    (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
rw₁ : { x : α // x ∈ s } → α
rw₂ : Type u_1
rw₃ rw₄ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) univ

Tactic:
rw [← preimage_range, range_coe]

Premises used: Set.preimage_range, Subtype.range_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
t : Set (↑s : Type u_1)
x : α
h : x ∈ val (p := fun (x : α) ↦ x ∈ s) '' t
y : { x : α // x ∈ s }
left : y ∈ t
yvaleq : (↑y : α) = x
rw : (↑y : α) ∈ s
⊢ x ∈ s

Tactic:
rw [← yvaleq]
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
t : Set (↑s : Type u_1)
x : α
h : x ∈ val (p := fun (x : α) ↦ x ∈ s) '' t
y : { x : α // x ∈ s }
left : y ∈ t
yvaleq : (↑y : α) = x
⊢ (↑y : α) ∈ s

Tactic:
y.property

Premises used: Subtype.property