awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact y.property

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

Tactic:
image_univ.trans range_coe

Premises used: Set.image_univ, Subtype.range_coe, Eq.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
⊢ image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ t

Tactic:
image_preimage_eq_range_inter.trans <| congr_arg (· ∩ t) range_coe

Premises used: Set.image_preimage_eq_range_inter, Subtype.range_coe, Inter.inter, congr_arg, Eq.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
⊢ image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ t

Tactic:
image_preimage_coe s t

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ u
rw₁ :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
      image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
rw₂ rw₃ :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t = s ∩ u

Tactic:
rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]

Premises used: Subtype.image_preimage_coe, Function.Injective.eq_iff, Subtype.coe_injective, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
rw : s ∩ (s ∩ t) = s ∩ t
rw₁ : s ∩ s ∩ t = s ∩ t
rw₂ rw₃ : s ∩ t = s ∩ t
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)

Tactic:
rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]

Premises used: Set.inter_self, Subtype.preimage_coe_eq_preimage_coe_iff, Set.inter_assoc
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
rw₁ rw₂ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (t ∩ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)

Tactic:
rw [inter_comm, preimage_coe_self_inter]

Premises used: Subtype.preimage_coe_self_inter, Set.inter_comm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t = s ∩ u

Tactic:
preimage_coe_eq_preimage_coe_iff

Premises used: Subtype.preimage_coe_eq_preimage_coe_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
mp :
  Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    s ∩ t ⊆ s ∩ u
mpr :
  s ∩ t ⊆ s ∩ u →
    Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t ⊆ s ∩ u

Tactic:
constructor
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
mp :
  Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ⊆
      image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    s ∩ t ⊆ s ∩ u

Tactic:
rw [← image_preimage_coe, ← image_preimage_coe]

Premises used: Subtype.image_preimage_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ⊆
      image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
image_mono

Premises used: Set.image_mono
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ⊆
      image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
exact image_mono

Premises used: Set.image_mono
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : (↑s : Type u_1)
a : Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) x
⊢ Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) x

Tactic:
(h ⟨x.2, a⟩).2

Premises used: Set.Mem, setOf, And.right, Set.preimage, And.intro, Subtype.property
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t u : Set α
h : s ∩ t ⊆ s ∩ u
x : (↑s : Type u_1)
a : Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) x
⊢ Membership.mem (γ := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) x

Tactic:
exact (h ⟨x.2, a⟩).2

Premises used: And.right, And.intro, Subtype.property
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
rw :
  (∃ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) ∧ p s) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
rw₁ rw₂ : (∃ (s : Set α), s ⊆ t ∧ p s) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
⊢ (∃ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∃ (s : Set α), s ⊆ t ∧ p s

Tactic:
rw [← exists_subset_range_and_iff, range_coe]

Premises used: Set.exists_subset_range_and_iff, Subtype.range_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
rw :
  (∀ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
rw₁ rw₂ : (∀ (s : Set α), s ⊆ t → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
⊢ (∀ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s

Tactic:
rw [← forall_subset_range_iff, range_coe]

Premises used: Set.forall_subset_range_iff, Subtype.range_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
rw :
  Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔
    (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)).Nonempty
rw₁ rw₂ :
  Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔
    Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
⊢ Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔ (s ∩ t).Nonempty

Tactic:
rw [← image_preimage_coe, image_nonempty]

Premises used: Set.image_nonempty, Subtype.image_preimage_coe
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s t : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ∅ ↔ s ∩ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, preimage_coe_nonempty]

Premises used: Subtype.preimage_coe_nonempty, Set.not_nonempty_iff_eq_empty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' sᶜ) ∅

Tactic:
preimage_coe_eq_empty.2 (inter_compl_self s)

Premises used: Iff.mpr, Set.inter_compl_self, Subtype.preimage_coe_eq_empty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
s : Set α
⊢ Eq (α := Set (↑sᶜ : Type u_1)) ((fun (x : (↑sᶜ : Type u_1)) ↦ (↑x : α)) ⁻¹' s) ∅

Tactic:
preimage_coe_eq_empty.2 (compl_inter_self s)

Premises used: Iff.mpr, Subtype.preimage_coe_eq_empty, Set.compl_inter_self
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
simp : Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)

Tactic:
simp only [mem_range, not_exists, (· ∘ ·)]

Premises used: Set.mem_range, Function.comp, not_exists
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none

Tactic:
⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩

Premises used: Function.Injective.ne, Function.Injective.comp, And.intro, Iff.intro, Option.some_injective, Option.some_ne_none
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
hf : (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none

Tactic:
refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ Eq.{u_1 + 1} (α := Option α) none none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
b : α
hab : f none = f (some b)
⊢ none = some b

Tactic:
(h_none _ hab.symm).elim

Premises used: False.elim, Eq.symm
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a : α
hab : f (some a) = f none
⊢ some a = none

Tactic:
(h_none _ hab).elim

Premises used: False.elim
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
a b : α
hab : f (some a) = f (some b)
⊢ some a = some b

Tactic:
congr_arg some (h_some hab)

Premises used: Option.some, congr_arg
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
h_some : Injective (f ∘ some)
h_none : ∀ (x : α), ¬f (some x) = f none
hab : f none = f none
⊢ Eq.{u_1 + 1} (α := Option α) none none

Tactic:
exacts [rfl, (h_none _ hab.symm).elim, (h_none _ hab).elim, congr_arg some (h_some hab)]

Premises used: rfl
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ range f = insert (f none) (range (f ∘ some))

Tactic:
Set.ext fun _ => Option.exists.trans <| eq_comm.or Iff.rfl

Premises used: Set.ext, Iff.rfl, eq_comm, Iff.or, Option.exists, Iff.trans
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
rw :
  insert (Option.elim none b f) (range.{u_2, u_1 + 1} (ι := α) ((fun (o : Option α) ↦ o.elim b f) ∘ some)) =
    insert b (range f)
⊢ (range fun (o : Option α) ↦ o.elim b f) = insert b (range f)

Tactic:
rw [range_eq]

Premises used: Option.range_eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ insert (Option.elim none b f) (range.{u_2, u_1 + 1} (ι := α) ((fun (o : Option α) ↦ o.elim b f) ∘ some)) =
    insert b (range f)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
rw : (range fun (x : α) ↦ (some x).elim b f) = range f
⊢ (fun (o : Option α) ↦ o.elim b f) '' range some = range f

Tactic:
rw [← range_comp']

Premises used: Set.range_comp'
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (range fun (x : α) ↦ (some x).elim b f) = range f

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f

Tactic:
⟨fun h y => ?_, Surjective.image_surjective⟩

Premises used: Iff.intro, Function.Surjective.image_surjective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
refine : ∀ (h : Surjective (image f)) (y : β), ∃ (a : α), f a = y
⊢ Surjective (image f) ↔ Surjective f

Tactic:
refine ⟨fun h y => ?_, Surjective.image_surjective⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
rcases : ∀ (s : Set α) (hs : f '' s = {y}), ∃ (a : α), f a = y
⊢ ∃ (a : α), f a = y

Tactic:
rcases h {y} with ⟨s, hs⟩

Premises used: Singleton.singleton
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ Membership.mem (γ := Set β) {y} y

Tactic:
have := mem_singleton y
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : Membership.mem (γ := Set β) {y} y
⊢ y ∈ f '' s

Tactic:
rw [← hs] at this
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
rcases : ∀ (x : α), x ∈ s → ∀ (hx : f x = y), ∃ (a : α), f a = y
⊢ ∃ (a : α), f a = y

Tactic:
rcases this with ⟨x, _, hx⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left : x ∈ s
hx : f x = y
⊢ ∃ (a : α), f a = y

Tactic:
⟨x, hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
x : α
left : x ∈ s
hx : f x = y
⊢ ∃ (a : α), f a = y

Tactic:
exact ⟨x, hx⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f

Tactic:
⟨fun h x x' hx => ?_, Injective.image_injective⟩

Premises used: Iff.intro, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
refine : ∀ (h : Injective (image f)) (x x' : α) (hx : f x = f x'), x = x'
⊢ Injective (image f) ↔ Injective f

Tactic:
refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
rw : Eq (α := Set α) {x} {x'}
⊢ x = x'

Tactic:
rw [← singleton_eq_singleton_iff]

Premises used: Set.singleton_eq_singleton_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
a : f '' {x} = f '' {x'}
⊢ Eq (α := Set α) {x} {x'}

Tactic:
apply h
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
a : {f x} = f '' {x'}
a₁ : Eq (α := Set β) {f x} {f x'}
a₂ a₃ : Eq (α := Set β) {f x'} {f x'}
⊢ f '' {x} = f '' {x'}

Tactic:
rw [image_singleton, image_singleton, hx]

Premises used: Set.image_singleton
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
rw : f '' f ⁻¹' s = f '' t ↔ s = f '' t
rw₁ rw₂ : s = f '' t ↔ s = f '' t
⊢ f ⁻¹' s = t ↔ s = f '' t

Tactic:
rw [← image_eq_image hf.1, hf.2.image_preimage]

Premises used: Set.image_eq_image, And.right, And.left, Function.Surjective.image_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
rw : f '' s = f '' f ⁻¹' t ↔ f '' s = t
rw₁ rw₂ : f '' s = t ↔ f '' s = t
⊢ s = f ⁻¹' t ↔ f '' s = t

Tactic:
rw [← image_eq_image hf.1, hf.2.image_preimage]

Premises used: Set.image_eq_image, And.right, And.left, Function.Surjective.image_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Disjoint s t
⊢ Disjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
disjoint_iff_inf_le.mpr fun _ hx => h.le_bot hx

Premises used: Iff.mpr, Disjoint.le_bot, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Codisjoint s t
simp : ∀ (h : s ∪ t = ⊤), f ⁻¹' (s ∪ t) = ⊤
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)

Tactic:
simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢

Premises used: Set.sup_eq_union, codisjoint_iff_le_sup, Set.preimage_union, top_le_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
rw : f ⁻¹' ⊤ = ⊤
⊢ f ⁻¹' (s ∪ t) = ⊤

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

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

Tactic:
⟨h.1.preimage f, h.2.preimage f⟩

Premises used: Codisjoint.preimage, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint, Disjoint.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ Membership.mem (γ := Set α) ⊥ (g c)

Tactic:
h b hb c hc eq

Premises used: Set.Mem
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β → α
g : γ → α
s : Set β
t : Set γ
h : ∀ (b : β), b ∈ s → ∀ (c : γ), c ∈ t → f b ≠ g c
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
eq : f b = g c
⊢ Membership.mem (γ := Set α) ⊥ (g c)

Tactic:
exact h b hb c hc eq
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
hd : Disjoint s t
⊢ Disjoint (f '' s) (f '' t)

Tactic:
disjoint_image_image fun _ hx _ hy => hf.ne fun H => Set.disjoint_iff.1 hd ⟨hx, H.symm ▸ hy⟩

Premises used: Function.Injective.ne, Eq.rec, Set.disjoint_image_image, And.intro, Iff.mp, Eq.symm, Set.disjoint_iff
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
h : Disjoint (f '' s) (f '' t)
⊢ Disjoint s t

Tactic:
disjoint_iff_inf_le.mpr fun _ hx =>
    disjoint_left.1 h (mem_image_of_mem _ hx.1) (mem_image_of_mem _ hx.2)

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left, Set.mem_image_of_mem, Iff.mp, disjoint_iff_inf_le
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
hf : Injective f
⊢ Disjoint (f '' s) (f '' t) ↔ Disjoint s t

Tactic:
⟨Disjoint.of_image, disjoint_image_of_injective hf⟩

Premises used: Disjoint.of_image, Iff.intro, Set.disjoint_image_of_injective
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
rw : s ∩ t = ∅
rw₁ : f '' f ⁻¹' (s ∩ t) = ∅
rw₂ : f '' (f ⁻¹' s ∩ f ⁻¹' t) = ∅
rw₃ : f '' ∅ = ∅
rw₄ rw₅ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ Disjoint s t

Tactic:
rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]

Premises used: Set.preimage_inter, Set.image_preimage_eq, Set.disjoint_iff_inter_eq_empty, Inter.inter, Disjoint.inter_eq, Set.image_empty
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
⊢ Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t

Tactic:
⟨Disjoint.of_preimage hf, Disjoint.preimage _⟩

Premises used: Iff.intro, Disjoint.of_preimage, Disjoint.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : Disjoint s (range f)
⊢ f ⁻¹' s = ∅

Tactic:
simpa using h.preimage f

Premises used: Disjoint.preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f ⁻¹' s = ∅
⊢ ∀ (x : α), ¬f x ∈ s

Tactic:
simp only [eq_empty_iff_forall_notMem, mem_preimage] at h ⊢

Premises used: Set.eq_empty_iff_forall_notMem, Set.mem_preimage
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : ∀ (x : α), ¬f x ∈ s
⊢ Disjoint s (range f)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
u : Set α
v : Set β
⊢ ∀ (b : α), b ∈ u → ∀ (c : β), c ∈ v → Sum.inl b ≠ Sum.inr c

Tactic:
simp
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
v : Set β
⊢ Disjoint (α := Set (α ⊕ β)) (range Sum.inl) (Sum.inr '' v)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : Type u_2
u : Set α
⊢ Disjoint (α := Set (α ⊕ β)) (Sum.inl '' u) (range Sum.inr)

Tactic:
grind
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : α → Type u_2
i j : α
s : Set (β i)
h : i ≠ j
⊢ Sigma.mk (β := β) j ⁻¹' Sigma.mk (β := β) i '' s = ∅

Tactic:
simp [image, h]

Premises used: Set.image
-- Module: Mathlib.Data.Set.Image
Goal:
α : Type u_1
β : α → Type u_2
i : α
s : Set (β i)
⊢ Sigma.mk (β := β) i ⁻¹' Sigma.mk (β := β) i '' s = s

Tactic:
simp [image]

Premises used: Set.image
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s : Set α
x : (↑s : Type u_1)
⊢ inclusion (s := s) (t := s) ⋯ x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s : Set α
h : s ⊆ s
⊢ inclusion (s := s) (t := s) h = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ inclusion (s := s) (t := t) h = Subtype.map (p := Membership.mem s) (q := Membership.mem t) id h

Tactic:
rfl

Premises used: Subtype.map, rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
a : α
ha : a ∈ s
⊢ inclusion (s := s) (t := t) h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : α) ↦ x ∈ t) a ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
x : (↑t : Type u_1)
m : (↑x : α) ∈ s
⊢ inclusion (s := s) (t := t) h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) m) = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
x : (↑s : Type u_1)
⊢ inclusion (s := t) (t := u) htu (inclusion (s := s) (t := t) hst x) = inclusion (s := s) (t := u) ⋯ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_2
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
⊢ inclusion (s := t) (t := u) htu ∘ inclusion (s := s) (t := t) hst = inclusion (s := s) (t := u) ⋯

Tactic:
funext (inclusion_inclusion hst htu)

Premises used: funext, Set.inclusion_inclusion
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
x : (↑s : Type u_1)
⊢ (↑(inclusion (s := s) (t := t) h x) : α) = (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ t) ∘ inclusion (s := s) (t := t) h = Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ Injective (inclusion (s := s) (t := t) h)

Tactic:
Subtype.map_injective h injective_id

Premises used: Subtype.map, Function.injective_id, Subtype.map_injective
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
x y : (↑s : Type u_1)
⊢ inclusion (s := s) (t := t) h x = inclusion (s := s) (t := t) h y ↔ x = y

Tactic:
(inclusion_injective h).eq_iff

Premises used: Function.Injective.eq_iff, Set.inclusion_injective
-- Module: Mathlib.Data.Set.Inclusion
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
h_surj : Surjective (inclusion (s := s) (t := t) h)
x : α
hx : x ∈ t
⊢ x ∈ s

Tactic:
grind [h_surj ⟨x, hx⟩]

Premises used: Subtype.mk