awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ (range fun (x : ι) ↦ g (f x)) = g '' range f

Tactic:
range_comp g f

Premises used: Set.range_comp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
s : Set α
⊢ range f ⊆ s ↔ ∀ (y : ι), f y ∈ s

Tactic:
forall_mem_range

Premises used: Set.forall_mem_range, Set.Subset
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
⊢ range f ⊆ range g ↔ ∃ (h : α → β), f = g ∘ h

Tactic:
simp only [range_subset_iff, mem_range, Classical.skolem, funext_iff, (· ∘ ·), eq_comm]

Premises used: Classical.skolem, Set.mem_range, funext_iff, Function.comp, eq_comm, Set.range_subset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ range f = s ↔ (∀ (a : α), f a ∈ s) ∧ ∀ (b : β), b ∈ s → ∃ (a : α), f a = b

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ range (g ∘ f) ⊆ range g

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
⊢ (range f).Nonempty ↔ Nonempty ι

Tactic:
⟨fun ⟨_, x, _⟩ => ⟨x⟩, fun ⟨x⟩ => ⟨f x, mem_range_self x⟩⟩

Premises used: Set.mem_range_self, Nonempty.intro, Set.Nonempty, Iff.intro, Exists.intro, Nonempty, _private.0.Set.range_nonempty_iff_nonempty.match_1, Set.range, _private.0.Set.range_nonempty_iff_nonempty.match_2
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
h : Nonempty ι
f : ι → α
⊢ (range f).Nonempty

Tactic:
range_nonempty_iff_nonempty.2 h

Premises used: Iff.mpr, Set.range_nonempty_iff_nonempty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
rw : range f = ∅ ↔ ¬Nonempty ι
rw₁ : range f = ∅ ↔ ¬(range f).Nonempty
rw₂ : Type u_1
rw₃ : ι → α
rw₄ : range f = ∅ ↔ range f = ∅
rw₅ : Type u_1
rw₆ : ι → α
rw₇ : range f = ∅ ↔ range f = ∅
rw₈ : Type u_1
rw₉ : ι → α
⊢ range f = ∅ ↔ IsEmpty ι

Tactic:
rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]

Premises used: Set.range_nonempty_iff_nonempty, Set.not_nonempty_iff_eq_empty, not_nonempty_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
inst : IsEmpty ι
f : ι → α
⊢ range f = ∅

Tactic:
range_eq_empty_iff.2 ‹_›

Premises used: Iff.mpr, Set.range_eq_empty_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
simp_rw : (∀ (x : α), (∃ (y : ι), f y = x) ↔ x = y) ↔ ∀ (x : ι), f x = y
⊢ range f = {y} ↔ ∀ (x : ι), f x = y

Tactic:
simp_rw [Set.ext_iff, Set.mem_range, Set.mem_singleton_iff]

Premises used: Set.mem_range, Set.mem_singleton_iff, Set.ext_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
h : ∀ (x : α), (∃ (y : ι), f y = x) ↔ x = y
x : ι
simp_rw : ∃ (y : ι), f y = f x
⊢ f x = y

Tactic:
simp_rw [← h, exists_apply_eq_apply]

Premises used: exists_apply_eq_apply
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x : α
simp_rw : (∃ (y_1 : ι), y = x) ↔ x = y
simp_rw₁ : y = x ↔ x = y
⊢ (∃ (y : ι), f y = x) ↔ x = y

Tactic:
simp_rw [h, exists_const, eq_comm]

Premises used: eq_comm, exists_const
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
⊢ (∀ (x : α), (∃ (y : ι), f y = x) ↔ x = y) ↔ ∀ (x : ι), f x = y

Tactic:
exact ⟨fun h _ => by simp_rw [← h, exists_apply_eq_apply],
      fun h _ => by simp_rw [h, exists_const, eq_comm]⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
hy : ∀ (x : ι), f x = y
⊢ range f = {y}

Tactic:
range_eq_singleton_iff.mpr hy

Premises used: Iff.mpr, Set.range_eq_singleton_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
f_1 : ι → α
s t : Set α
inst : Nonempty ι
f : ι → α
⊢ Nonempty.{u_1 + 1} (↑(range f) : Type u_1)

Tactic:
(range_nonempty f).to_subtype

Premises used: Set.Nonempty.to_subtype, Set.range_nonempty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ f '' s ∪ f '' sᶜ = range f

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : α
⊢ insert (f x) (f '' {x}ᶜ) = range f

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

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

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

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

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ s ⊆ range f ↔ ∃ (t : Set α), f '' t = s

Tactic:
⟨fun h => ⟨_, image_preimage_eq_iff.2 h⟩, fun ⟨_, ht⟩ => ht ▸ image_subset_range _ _⟩

Premises used: Iff.mpr, _private.0.Set.subset_range_iff_exists_image_eq.match_1, Eq.rec, Set.image_subset_range, HasSubset.Subset, Set.preimage, Iff.intro, Exists.intro, Set.range, Set.image_preimage_eq_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ range (image f) = 𝒫 range f

Tactic:
ext fun _ => subset_range_iff_exists_image_eq.symm

Premises used: Set.ext, Set.subset_range_iff_exists_image_eq, Iff.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
rw : (∃ (s : Set β), s ⊆ range f ∧ p s) ↔ ∃ (a : Set β), a ∈ 𝒫 range f ∧ p a
⊢ (∃ (s : Set β), s ⊆ range f ∧ p s) ↔ ∃ (s : Set α), p (f '' s)

Tactic:
rw [← exists_range_iff, range_image]

Premises used: Set.exists_range_iff, Set.range_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ (s : Set β), s ⊆ range f ∧ p s) ↔ ∃ (a : Set β), a ∈ 𝒫 range f ∧ p a

Tactic:
rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
rw : (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (s : Set α), p (f '' s)

Tactic:
rw [← forall_mem_range, range_image]

Premises used: Set.forall_mem_range, Set.range_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a

Tactic:
simp only [mem_powerset_iff]

Premises used: Set.mem_powerset_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
mp : f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t
mpr : s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
mp : ∀ (y : β) (hx : f y ∈ s), f y ∈ t
⊢ x ∈ t

Tactic:
rcases hs hx with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t

Tactic:
h hx

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t

Tactic:
exact h hx
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t

Tactic:
apply h
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
mp : f ⁻¹' s = f ⁻¹' t → s = t
mpr : s = t → f ⁻¹' s = f ⁻¹' t
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : s ⊆ t
mp₁ : t ⊆ s
⊢ s = t

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : f ⁻¹' s ⊆ f ⁻¹' t
mp₁ mp₂ : f ⁻¹' t ⊆ f ⁻¹' t
⊢ s ⊆ t

Tactic:
rw [← preimage_subset_preimage_iff hs, h]

Premises used: Set.preimage_subset_preimage_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : f ⁻¹' t ⊆ f ⁻¹' s
mp₁ mp₂ : f ⁻¹' t ⊆ f ⁻¹' t
⊢ t ⊆ s

Tactic:
rw [← preimage_subset_preimage_iff ht, h]

Premises used: Set.preimage_subset_preimage_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s

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

Tactic:
Set.ext fun x => and_iff_left ⟨x, rfl⟩

Premises used: Set.ext, and_iff_left, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f ⁻¹' (s ∩ range f) = f ⁻¹' s
rw₁ rw₂ : f ⁻¹' s = f ⁻¹' s
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s

Tactic:
rw [inter_comm, preimage_inter_range]

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

Tactic:
rw [image_preimage_eq_range_inter, preimage_range_inter]

Premises used: Set.image_preimage_eq_range_inter, Set.preimage_range_inter
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (range id) univ

Tactic:
range_eq_univ.2 surjective_id

Premises used: Iff.mpr, Set.range_eq_univ, Function.surjective_id
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Set α) (range fun (x : α) ↦ x) univ

Tactic:
range_id

Premises used: Set.range_id
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
⊢ Eq.{u_1 + 1} (α := Set α) (range (ι := α × β) Prod.fst) univ

Tactic:
Prod.fst_surjective.range_eq

Premises used: Prod.fst_surjective, Function.Surjective.range_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
⊢ Eq.{u_2 + 1} (α := Set β) (range (ι := α × β) Prod.snd) univ

Tactic:
Prod.snd_surjective.range_eq

Premises used: Function.Surjective.range_eq, Prod.snd_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
ι : Sort u_4
α : ι → Type u_5
inst : ∀ (i : ι), Nonempty.{u_5 + 1} (α i)
i : ι
⊢ Eq.{u_5 + 1} (α := Set (α i)) (range (eval (β := α) i)) univ

Tactic:
(surjective_eval i).range_eq

Premises used: Function.surjective_eval, Function.Surjective.range_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (val : α),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inl val)
h₁ :
  ∀ (val : β),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inr val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inr val)
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl) {x : α ⊕ β | x.isLeft = true}

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
val : α
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
val : β
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inr val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (val : α),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inl val)
h₁ :
  ∀ (val : β),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inr val)
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr) {x : α ⊕ β | x.isRight = true}

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
val : α
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inl val)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
val : β
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inr val)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Membership.mem (γ := Set (α ⊕ β)) ⊥ (Sum.inl x₁)

Tactic:
Sum.noConfusion rfl rfl (heq_of_eq h)

Premises used: heq_of_eq, Sum.noConfusion, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Membership.mem (γ := Set (α ⊕ β)) ⊥ (Sum.inl x₁)

Tactic:
exact Sum.noConfusion rfl rfl (heq_of_eq h)

Premises used: heq_of_eq, Sum.noConfusion, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x : α
inl : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl x)
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl ⊔ range Sum.inr) (Sum.inl x)

Tactic:
left
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
y : β
inr : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr y)
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl ⊔ range Sum.inr) (Sum.inr y)

Tactic:
right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x : α
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl x)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
x : α
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl x)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
y : β
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr y)

Tactic:
mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
y : β
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr y)

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl ∪ range Sum.inr) univ

Tactic:
isCompl_range_inl_range_inr.sup_eq_top

Premises used: IsCompl.sup_eq_top, Set.isCompl_range_inl_range_inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl ∩ range Sum.inr) ∅

Tactic:
isCompl_range_inl_range_inr.inf_eq_bot

Premises used: IsCompl.inf_eq_bot, Set.isCompl_range_inl_range_inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr ∪ range Sum.inl) univ

Tactic:
isCompl_range_inl_range_inr.symm.sup_eq_top

Premises used: IsCompl.sup_eq_top, Set.isCompl_range_inl_range_inr, IsCompl.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr ∩ range Sum.inl) ∅

Tactic:
isCompl_range_inl_range_inr.symm.inf_eq_bot

Premises used: IsCompl.inf_eq_bot, Set.isCompl_range_inl_range_inr, IsCompl.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set β
h : ∀ (x : α), Membership.mem (γ := Set α) (Sum.inl ⁻¹' Sum.inr '' s) x ↔ Membership.mem (γ := Set α) ∅ x
⊢ Eq.{u_1 + 1} (α := Set α) (Sum.inl ⁻¹' Sum.inr '' s) ∅

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set β
x : α
⊢ Membership.mem (γ := Set α) (Sum.inl ⁻¹' Sum.inr '' s) x ↔ Membership.mem (γ := Set α) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
h : ∀ (x : β), Membership.mem (γ := Set β) (Sum.inr ⁻¹' Sum.inl '' s) x ↔ Membership.mem (γ := Set β) ∅ x
⊢ Eq.{u_2 + 1} (α := Set β) (Sum.inr ⁻¹' Sum.inl '' s) ∅

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
x : β
⊢ Membership.mem (γ := Set β) (Sum.inr ⁻¹' Sum.inl '' s) x ↔ Membership.mem (γ := Set β) ∅ x

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
rw : Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (Sum.inr '' univ)) ∅
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (range Sum.inr)) ∅

Tactic:
rw [← image_univ, preimage_inl_image_inr]

Premises used: Set.image_univ, Set.preimage_inl_image_inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
rw : Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (Sum.inl '' univ)) ∅
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (range Sum.inl)) ∅

Tactic:
rw [← image_univ, preimage_inr_image_inl]

Premises used: Set.image_univ, Set.preimage_inr_image_inl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl)ᶜ (range Sum.inr)

Tactic:
IsCompl.compl_eq isCompl_range_inl_range_inr

Premises used: IsCompl.compl_eq, Set.isCompl_range_inl_range_inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr)ᶜ (range Sum.inl)

Tactic:
IsCompl.compl_eq isCompl_range_inl_range_inr.symm

Premises used: IsCompl.compl_eq, Set.isCompl_range_inl_range_inr, IsCompl.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
h : ∀ (val : α), Sum.inl val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
h₁ : ∀ (val : β), Sum.inr val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val : α
⊢ Sum.inl val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
val : β
⊢ Sum.inr val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
rw : Sum.elim Sum.inl Sum.inr ⁻¹' s = s
rw₁ : id ⁻¹' s = s
rw₂ rw₃ : s = s
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s

Tactic:
rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]

Premises used: Set.preimage_sumElim, Set.preimage_id, Sum.elim_inl_inr
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (α ⊕ β)
f : α → γ
g : β → γ
⊢ Sum.elim f g '' s = f '' Sum.inl ⁻¹' s ∪ g '' Sum.inr ⁻¹' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
r : α → α → Prop
⊢ range (Quot.mk r) = univ

Tactic:
Quot.mk_surjective.range_eq

Premises used: Function.Surjective.range_eq, Quot.mk_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
r : ι → ι → Prop
hf : ∀ (x y : ι), r x y → f x = f y
⊢ range (Quot.lift (r := r) f hf) = range f

Tactic:
ext fun _ => Quot.mk_surjective.exists

Premises used: Set.ext, Function.Surjective.exists, Quot.mk_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Setoid α
⊢ range (Quotient.mk s) = univ

Tactic:
range_quot_mk _

Premises used: Set.range_quot_mk, Quotient
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
s : Setoid ι
hf : ∀ (a b : ι), a ≈ b → f a = f b
⊢ range (Quotient.lift f hf) = range f

Tactic:
range_quot_lift _

Premises used: Set.range_quot_lift, Quotient
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Setoid α
⊢ Eq.{u_1 + 1} (α := Set (Quotient s)) (range Quotient.mk') univ

Tactic:
range_quot_mk _

Premises used: Set.range_quot_mk, Quotient, Quotient.mk'
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
sa : Setoid α
⊢ Eq.{u_1 + 1} (α := Set (Quotient sa)) (range Quotient.mk'') univ

Tactic:
range_quotient_mk

Premises used: Set.range_quotient_mk
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
s : Setoid ι
hf : ∀ (a b : ι), (s : ι → ι → Prop) a b → f a = f b
⊢ (range fun (x : Quotient s) ↦ x.liftOn' f hf) = range f

Tactic:
range_quot_lift _

Premises used: Quotient.liftOn', Set.range_quot_lift, Quotient
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
c : α
⊢ Subset (α := Set α) (range fun (x : ι) ↦ c) {c}

Tactic:
range_subset_iff.2 fun _ => rfl

Premises used: Iff.mpr, Set.range_subset_iff, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
inst : Nonempty ι
c : α
⊢ Eq (α := Set α) (range fun (x : ι) ↦ c) {c}

Tactic:
range_eq_singleton (fun _ => rfl)

Premises used: Set.range_eq_singleton, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
h₁ :
  ∀ (x : β) (hx : q x),
    Subtype.mk (p := q) x hx ∈ range (Subtype.map (p := p) (q := q) f h) ↔
      Membership.mem (γ := Set (Subtype q)) (Subtype.val (p := q) ⁻¹' f '' {x : α | p x}) (Subtype.mk (p := q) x hx)
⊢ range (Subtype.map (p := p) (q := q) f h) = Subtype.val (p := q) ⁻¹' f '' {x : α | p x}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
h₁ :
  (∃ (a : α), ∃ (h_1 : p a), Subtype.mk (p := q) (f a) ⋯ = Subtype.mk (p := q) x hx) ↔
    ∃ (x_1 : α), Membership.mem (γ := Set α) {x : α | p x} x_1 ∧ f x_1 = x
⊢ Subtype.mk (p := q) x hx ∈ range (Subtype.map (p := p) (q := q) f h) ↔
    Membership.mem (γ := Set (Subtype q)) (Subtype.val (p := q) ⁻¹' f '' {x : α | p x}) (Subtype.mk (p := q) x hx)

Tactic:
simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]

Premises used: Set.mem_range, Subtype.map, Set.mem_image, Subtype.exists, Set.mem_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ (a : α), ∃ (h_1 : p a), Subtype.mk (p := q) (f a) ⋯ = Subtype.mk (p := q) x hx) ↔
    ∃ (x_1 : α), Membership.mem (γ := Set α) {x : α | p x} x_1 ∧ f x_1 = x

Tactic:
simp only [Subtype.mk.injEq, exists_prop, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, exists_prop, Subtype.mk.injEq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := (s : Set (α × β)) → Set (β × α)) (image Prod.swap) (preimage Prod.swap)

Tactic:
image_eq_preimage_of_inverse Prod.swap_leftInverse Prod.swap_rightInverse

Premises used: Prod.swap_rightInverse, Prod.swap_leftInverse, Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ (f ⁻¹' {y}).Nonempty ↔ y ∈ range f

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Nonempty, Set.preimage, Set.singleton, Set.range
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ f ⁻¹' {y} = ∅ ↔ ¬y ∈ range f

Tactic:
not_nonempty_iff_eq_empty.symm.trans preimage_singleton_nonempty.not

Premises used: Set.preimage_singleton_nonempty, Set.not_nonempty_iff_eq_empty, Iff.not, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
x : α
⊢ range f ⊆ {x} ↔ f = const ι x

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f '' (univ \ f ⁻¹' s) = range f \ s
rw₁ : f '' univ \ s = range f \ s
rw₂ rw₃ : range f \ s = range f \ s
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s

Tactic:
rw [compl_eq_univ_diff, image_diff_preimage, image_univ]

Premises used: Set.image_univ, Set.image_diff_preimage, Set.compl_eq_univ_diff
-- 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:
funext fun _ => rfl

Premises used: funext, rfl