awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ f ⁻¹' ∅ = ∅

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h e_f : ∀ (x : α), f x = g x
⊢ f ⁻¹' s = g ⁻¹' s

Tactic:
congr with x
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
x : α
⊢ f x = g x

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ⊆ t
⊢ f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
fun _ hx => h hx

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

Tactic:
rfl

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

Tactic:
subset_univ _

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

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
⊢ f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' sᶜ = (f ⁻¹' s)ᶜ

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Not, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
⊢ f ⁻¹' (s \ t) = f ⁻¹' s \ f ⁻¹' t

Tactic:
rfl

Premises used: Set.Mem, Set.diff, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
⊢ f ⁻¹' s ∆ t = (f ⁻¹' s) ∆ (f ⁻¹' t)

Tactic:
rfl

Premises used: Set.union, Set.Mem, Set.diff, setOf, Set.preimage, symmDiff, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t₁ t₂ : Set β
⊢ f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)

Tactic:
rfl

Premises used: Set.union, Set.ite, Set.Mem, Set.diff, setOf, Set.inter, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
f : β → α
⊢ f ⁻¹' {a : α | p a} = {a : β | p (f a)}

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (s : Set α) → Set α) (preimage id) id

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ id ⁻¹' s = s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ (fun (x : α) ↦ x) ⁻¹' s = s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
b : β
s : Set β
h : b ∈ s
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ b) ⁻¹' s) univ

Tactic:
eq_univ_of_forall fun _ => h

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
b : β
s : Set β
h : ¬b ∈ s
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ b) ⁻¹' s) ∅

Tactic:
eq_empty_of_subset_empty fun _ hx => h hx

Premises used: Set.eq_empty_of_subset_empty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
b : β
s : Set β
inst : Decidable (b ∈ s)
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (x : α) ↦ b) ⁻¹' s) (if b ∈ s then univ else ∅)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
inl : ∀ (b : β) (hb : f ⁻¹' {b} = univ), ∃ (b : β), f = const α b
inr : ∀ (hf' : ¬∃ (b : β), f ⁻¹' {b} = univ), ∃ (b : β), f = const α b
⊢ ∃ (b : β), f = const α b

Tactic:
rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'

Premises used: Set.univ, Exists, em, Set.preimage, Singleton.singleton, Eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ (b : β), f = const α b

Tactic:
⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩

Premises used: Set.eq_univ_iff_forall, funext, Exists.intro, Iff.mp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
b : β
hb : f ⁻¹' {b} = univ
⊢ ∃ (b : β), f = const α b

Tactic:
exact ⟨b, funext fun x ↦ eq_univ_iff_forall.1 hb x⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ (b : β), f ⁻¹' {b} = univ
⊢ ∀ (x : α) (b : β), f x ≠ b

Tactic:
have : ∀ x b, f x ≠ b := fun x b ↦
      eq_empty_iff_forall_notMem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ (b : β), f ⁻¹' {b} = univ
this : ∀ (x : α) (b : β), f x ≠ b
⊢ ∃ (b : β), f = const α b

Tactic:
⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩

Premises used: funext, absurd, Exists.intro, Classical.arbitrary, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ (b : β), f ⁻¹' {b} = univ
this : ∀ (x : α) (b : β), f x ≠ b
⊢ ∃ (b : β), f = const α b

Tactic:
exact ⟨Classical.arbitrary β, funext fun x ↦ absurd rfl (this x _)⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set γ
⊢ g ∘ f ⁻¹' s = f ⁻¹' g ⁻¹' s

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ preimage (g ∘ f) = preimage f ∘ preimage g

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
⊢ preimage f^[0] = (preimage f)^[0]

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
succ : preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
succ₁ : preimage (f^[n] ∘ f) = preimage f ∘ (preimage f)^[n]
succ₂ : preimage f ∘ preimage f^[n] = preimage f ∘ (preimage f)^[n]
succ₃ succ₄ : preimage f ∘ (preimage f)^[n] = preimage f ∘ (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]

Tactic:
rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

Premises used: Function.iterate_succ, Function.iterate_succ', Set.preimage_comp_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
n : ℕ
zero : preimage f^[0] = (preimage f)^[0]
succ : ∀ (n : ℕ) (ih : preimage f^[n] = (preimage f)^[n]), preimage f^[n + 1] = (preimage f)^[n + 1]
⊢ preimage f^[n] = (preimage f)^[n]

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]

Premises used: Function.iterate_succ, Function.iterate_succ', Set.preimage_comp_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
s : Set γ
⊢ f ⁻¹' g ⁻¹' s = (fun (x : α) ↦ g (f x)) ⁻¹' s

Tactic:
preimage_comp.symm

Premises used: Set.preimage_comp, Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
s : Set (Subtype p)
t : Set α
⊢ s = Subtype.val (p := p) ⁻¹' t ↔ ∀ (x : α) (h : p x), Subtype.mk (p := p) x h ∈ s ↔ x ∈ t

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

Tactic:
let ⟨x, hx⟩ := hf
  ⟨f x, hx⟩

Premises used: Set.Nonempty, Exists.intro, _private.0.Set.nonempty_of_nonempty_preimage.match_1
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
h : ∀ (x : α), x ∈ p ⁻¹' {True} ↔ Membership.mem (γ := Set α) {a : α | p a} x
⊢ p ⁻¹' {True} = {a : α | p a}

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
x : α
⊢ x ∈ p ⁻¹' {True} ↔ Membership.mem (γ := Set α) {a : α | p a} x

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
h : ∀ (x : α), x ∈ p ⁻¹' {False} ↔ Membership.mem (γ := Set α) {a : α | ¬p a} x
⊢ p ⁻¹' {False} = {a : α | ¬p a}

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
p : α → Prop
x : α
⊢ x ∈ p ⁻¹' {False} ↔ Membership.mem (γ := Set α) {a : α | ¬p a} x

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
h :
  ∀ (x : α) (x_in_s : x ∈ s),
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) ↔
      Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
⊢ Eq (α := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ

Tactic:
ext ⟨x, x_in_s⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
h :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
h₁ :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
⊢ Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) ↔
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
x_in_v :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
⊢ False

Tactic:
eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩

Premises used: Set.eq_empty_iff_forall_notMem, And.intro, Iff.mp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
x_in_u :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
x_in_v :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
⊢ False

Tactic:
exact eq_empty_iff_forall_notMem.mp H x ⟨x_in_s, ⟨x_in_u, x_in_v⟩⟩

Premises used: Set.eq_empty_iff_forall_notMem, And.intro, Iff.mp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
obtain : ∀ (b : α) (hb : b ∈ t) (hba : f b = f a), a ∈ t
⊢ a ∈ t

Tactic:
obtain ⟨b, hb, hba⟩ := hs ha
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
rwa : b ∈ f ⁻¹' s
⊢ a ∈ t

Tactic:
rwa [hf ha _ hba.symm]

Premises used: Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ b ∈ f ⁻¹' s

Tactic:
simpa [hba]
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ f '' s = (fun (x : α) ↦ f x) '' s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
a : α
⊢ a ∈ s → f a ∈ f '' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
hf : Injective f
h : SurjOn f s t
⊢ f ⁻¹' t ⊆ s

Tactic:
fun _ hx ↦
  hf.mem_set_image.1 <| h hx

Premises used: Set.Subset, Iff.mp, Function.Injective.mem_set_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∀ (y : β), y ∈ f '' s → p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
p : β → Prop
⊢ (∃ (y : β), y ∈ f '' s ∧ p y) ↔ ∃ (x : α), x ∈ s ∧ p (f x)

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (a : α), a ∈ s → f a = g a
⊢ f '' s = g '' s

Tactic:
aesop
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
h : ∀ (x : α), f x = g x
⊢ f '' s = g '' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : s ⊆ t
⊢ f '' s ⊆ f '' t

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Monotone (image f)

Tactic:
fun _ _ => image_mono

Premises used: Set.image_mono, Monotone
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → γ
g : α → β
a : Set α
⊢ f ∘ g '' a = f '' g '' a

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

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
s : Set α
⊢ g '' f '' s = (fun (x : α) ↦ g (f x)) '' s

Tactic:
(image_comp g f s).symm

Premises used: Set.image_comp, Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
β' : Type u_5
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ f '' g '' s = g' '' f' '' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
⊢ Semiconj (image f) (image ga) (image gb)

Tactic:
fun _ =>
  image_comm h

Premises used: Function.Semiconj, Set.image_comm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Function.Commute (image f) (image g)

Tactic:
Function.Semiconj.set_image h

Premises used: Function.Commute, Function.Semiconj.set_image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (s ∪ t) = f '' s ∪ f '' t

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

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

Tactic:
subset_inter (image_mono inter_subset_left) (image_mono inter_subset_right)

Premises used: Set.image_mono, Set.inter_subset_left, Set.subset_inter, Set.inter_subset_right
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' (s \ t) ⊆ f '' s ∩ f '' tᶜ

Tactic:
image_inter_subset f s tᶜ

Premises used: Set.Mem, Compl.compl, Set.diff, setOf, Set.image_inter_subset, Not
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ s → f x = f y → x = y
b : β
h_1 : b ∈ f '' s ∩ f '' t
a₁ : α
ha₁ : a₁ ∈ s
h₁ : f a₁ = b
a₂ : α
ha₂ : a₂ ∈ t
h₂ : f a₂ = b
⊢ f a₂ = f a₁

Tactic:
simp [*]
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
H : Injective f
⊢ f '' (s ∩ t) = f '' s ∩ f '' t

Tactic:
image_inter_on fun _ _ _ _ h => H h

Premises used: Set.image_inter_on
-- Module: Mathlib.Data.Set.Image
Goal:
β : Type u_2
ι : Type u_5
f : ι → β
H : Surjective f
⊢ ∀ (x : β), x ∈ f '' univ

Tactic:
simpa [image]

Premises used: Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ f '' {a} = {f a}

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
a : β
⊢ Eq (α := Set β) ((fun (x : α) ↦ a) '' s) {a}

Tactic:
ext fun _ =>
    ⟨fun ⟨_, _, h⟩ => h ▸ mem_singleton _, fun h =>
      (eq_of_mem_singleton h).symm ▸ hs.imp fun _ hy => ⟨hy, rfl⟩⟩

Premises used: Set.ext, Set.mem_singleton, Set.eq_of_mem_singleton, Membership.mem, Eq.rec, Exists.imp, And.intro, Iff.intro, Singleton.singleton, Eq.symm, rfl, _private.0.Set.Nonempty.image_const.match_1
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
simp : (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s
⊢ f '' s = ∅ ↔ s = ∅

Tactic:
simp only [eq_empty_iff_forall_notMem]

Premises used: Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s

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

Premises used: False, And.intro, Iff.intro, Exists.intro, _private.0.Set.image_eq_empty.match_1, rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s

Tactic:
exact ⟨fun H a ha => H _ ⟨_, ha, rfl⟩, fun H b ⟨_, ha, _⟩ => H _ ha⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
rw : f '' s = ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ ∅ = f '' s ↔ s = ∅

Tactic:
rw [eq_comm, image_eq_empty]

Premises used: eq_comm, Set.image_eq_empty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
⊢ compl ⁻¹' s = compl '' s

Tactic:
Set.ext fun x =>
    ⟨fun h => ⟨xᶜ, h, compl_compl x⟩, fun h =>
      Exists.elim h fun _ hy => (compl_eq_comm.mp hy.2).symm.subst hy.1⟩

Premises used: Set.ext, compl_compl, Compl.compl, Eq.subst, And.right, And.left, And.intro, Iff.intro, Exists.intro, Iff.mp, Eq.symm, compl_eq_comm, Exists.elim
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
inst : BooleanAlgebra α
t : α
s : Set α
⊢ t ∈ compl '' s ↔ tᶜ ∈ s

Tactic:
simp [← preimage_compl_eq_image_compl]

Premises used: Set.preimage_compl_eq_image_compl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
h : ∀ (x : Set α) (x_1 : α), x_1 ∈ id '' x ↔ x_1 ∈ id x
⊢ Eq.{u_1 + 1} (α := (s : Set α) → Set α) (image id) id

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
x : Set α
x_1 : α
⊢ x_1 ∈ id '' x ↔ x_1 ∈ id x

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
h : ∀ (x : α), Membership.mem (γ := Set α) ((fun (x : α) ↦ x) '' s) x ↔ x ∈ s
⊢ (fun (x : α) ↦ x) '' s = s

Tactic:
ext
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
x : α
⊢ Membership.mem (γ := Set α) ((fun (x : α) ↦ x) '' s) x ↔ x ∈ s

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ id '' s = s

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
⊢ image f^[0] = (image f)^[0]

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
succ : image (f ∘ f^[n]) = (image f)^[n + 1]
succ₁ : image (f ∘ f^[n]) = image f ∘ (image f)^[n]
succ₂ : image (f ∘ f^[n]) = image f ∘ image f^[n]
succ₃ succ₄ : image f ∘ image f^[n] = image f ∘ image f^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]

Tactic:
rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

Premises used: Function.iterate_succ', Set.image_comp_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
f : α → α
n : ℕ
zero : image f^[0] = (image f)^[0]
succ : ∀ (n : ℕ) (ih : image f^[n] = (image f)^[n]), image f^[n + 1] = (image f)^[n + 1]
⊢ image f^[n] = (image f)^[n]

Tactic:
induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]

Premises used: Function.iterate_succ', Set.image_comp_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
rw : compl ∘ compl '' s = s
rw₁ : id '' s = s
rw₂ rw₃ : s = s
⊢ compl '' compl '' s = s

Tactic:
rw [← image_comp, compl_comp_compl, image_id]

Premises used: compl_comp_compl, Set.image_comp, Set.image_id
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ f '' {a, b} = {f a, f b}

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
rw : g (f x) ∈ s ↔ x ∈ s
rw₁ rw₂ : x ∈ s ↔ x ∈ s
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s

Tactic:
rw [Set.mem_preimage, hfg x]

Premises used: Set.mem_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
I : LeftInverse g f
s : Set α
⊢ f '' s ⊆ g ⁻¹' s

Tactic:
fun _ ⟨_, h, e⟩ => e ▸ I.mem_preimage_iff.mpr h

Premises used: Iff.mpr, Membership.mem, Eq.rec, Set.Subset, Set.preimage, Function.LeftInverse.mem_preimage_iff, _private.0.Set.image_eq_empty.match_1
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
I : LeftInverse g f
s : Set β
⊢ f ⁻¹' s ⊆ g '' s

Tactic:
fun b h => ⟨f b, h, I b⟩

Premises used: Set.Mem, setOf, Set.Subset, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
simp :
  (range f ∩ s ⊆ range f ∩ s' ∧ ∃ (x : β), x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
    f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ (x : α), x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s
⊢ range f ∩ s ⊂ range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' s'

Tactic:
simp only [Set.ssubset_iff_exists]

Premises used: Set.ssubset_iff_exists
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (∃ (x : β), x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔ ∃ (x : α), x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
aesop
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
apply : range f ∩ s ⊆ range f ∩ s' ↔ f ⁻¹' s ⊆ f ⁻¹' s'
⊢ (range f ∩ s ⊆ range f ∩ s' ∧ ∃ (x : β), x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
    f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ (x : α), x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s

Tactic:
apply and_congr ?_ (by aesop)

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

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

Tactic:
simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]

Premises used: Set.mem_range, Set.subset_inter_iff, Set.mem_inter_iff, Set.inter_subset_left, Set.mem_preimage, true_and
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
x : α
r : range f ∩ s ⊆ s'
hx : f x ∈ s
⊢ f x ∈ s'

Tactic:
aesop
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : x ∈ range f ∩ s
mpr : ∀ (hx : (∃ (y : α), f y = x) ∧ x ∈ s), x ∈ s'
⊢ x ∈ range f ∩ s'

Tactic:
simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]

Premises used: Set.mem_range, Set.subset_inter_iff, Set.mem_inter_iff, Set.inter_subset_left, Set.mem_preimage, true_and