awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
pos : ∀ (f : ℕ → (↑s : Type u_1)) (hf : Function.Surjective f), Nonempty.{u_1 + 1} s.FiniteExhaustion
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion

Tactic:
obtain ⟨f, hf⟩ := @exists_surjective_nat s h hs

Premises used: Set.Elem, exists_surjective_nat
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion

Tactic:
⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩

Premises used: setOf, Function.comp, LE.le, Nonempty.intro, Set.image, Subtype.val, Set.FiniteExhaustion.mk
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
pos :
  ∀ (n : ℕ),
    Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)
pos₁ :
  ∀ (n : ℕ),
    Subset.{u_1} (α := Set α) ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n)
      ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) (n + 1))
pos₂ : ⋃ (n : ℕ), (fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n = s
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion

Tactic:
refine ⟨fun n ↦ (Subtype.val ∘ f) '' {i | i ≤ n}, ?_, ?_, ?_⟩
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ ∀ (n : ℕ),
    Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)

Tactic:
fun n ↦ Finite.image _ (finite_le_nat n)

Premises used: Set.Finite, Function.comp, Set.Finite.image, Subtype.val, Set.finite_le_nat
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ ∀ (n : ℕ),
    Finite.{u_1 + 1} (↑((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n) : Type u_1)

Tactic:
exact fun n ↦ Finite.image _ (finite_le_nat n)

Premises used: Set.Finite.image, Set.finite_le_nat
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ ∀ (n : ℕ),
    Subset.{u_1} (α := Set α) ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n)
      ((fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) (n + 1))

Tactic:
grind
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : Nonempty.{u_1 + 1} (↑s : Type u_1)
f : ℕ → (↑s : Type u_1)
hf : Function.Surjective f
⊢ ⋃ (n : ℕ), (fun (n : ℕ) ↦ Subtype.val (p := fun (x : α) ↦ x ∈ s) ∘ f '' {i : ℕ | i ≤ n}) n = s

Tactic:
simp [← image_image, ← image_iUnion, iUnion_le_nat, range_eq_univ.mpr hf]

Premises used: Iff.mpr, Set.range_eq_univ, Set.image_image, Set.iUnion_le_nat, Set.image_iUnion
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ ∀ (n : ℕ), Finite.{u_1 + 1} (↑((fun (x : ℕ) ↦ (∅ : Set α)) n) : Type u_1)

Tactic:
simp [Finite.to_subtype]

Premises used: Set.Finite.to_subtype
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)
n : ℕ
⊢ Subset.{u_1} (α := Set α) ((fun (x : ℕ) ↦ (∅ : Set α)) n) ((fun (x : ℕ) ↦ (∅ : Set α)) (n + 1))

Tactic:
simp
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)
neg : ⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set α)) n = s
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion

Tactic:
refine ⟨fun _ ↦ ∅, by simp [Finite.to_subtype], fun n ↦ by simp, ?_⟩
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s_1 : Set α
K : s_1.FiniteExhaustion
s : Set α
hs : s.Countable
h : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ ⋃ (n : ℕ), (fun (x : ℕ) ↦ (∅ : Set α)) n = s

Tactic:
simp [Set.not_nonempty_iff_eq_empty'.mp h]

Premises used: Set.not_nonempty_iff_eq_empty', Iff.mp
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion ↔ s.Countable

Tactic:
⟨fun ⟨K⟩ ↦ ?_, fun h ↦ ⟨h.finiteExhaustion⟩⟩

Premises used: Nonempty.intro, Iff.intro, _private.0.Set.nonempty_finiteExhaustion_iff.match_1, Set.Countable, Set.Countable.finiteExhaustion
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
refine : Nonempty.{u_1 + 1} s.FiniteExhaustion → ∀ (K : s.FiniteExhaustion), s.Countable
⊢ Nonempty.{u_1 + 1} s.FiniteExhaustion ↔ s.Countable

Tactic:
refine ⟨fun ⟨K⟩ ↦ ?_, fun h ↦ ⟨h.finiteExhaustion⟩⟩
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
h : Nonempty.{u_1 + 1} s.FiniteExhaustion
K : s.FiniteExhaustion
rw : Set.Countable.{u_1} (α := α) (⋃ (n : ℕ), (K : (a : ℕ) → Set α) n)
⊢ s.Countable

Tactic:
rw [← K.iUnion_eq]

Premises used: Set.FiniteExhaustion.iUnion_eq
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
h : Nonempty.{u_1 + 1} s.FiniteExhaustion
K : s.FiniteExhaustion
⊢ Set.Countable.{u_1} (α := α) (⋃ (n : ℕ), (K : (a : ℕ) → Set α) n)

Tactic:
countable_iUnion <| fun i ↦ (K.finite i).countable

Premises used: Set.countable_iUnion, Set.FiniteExhaustion.finite, Set.Finite.countable
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
h : Nonempty.{u_1 + 1} s.FiniteExhaustion
K : s.FiniteExhaustion
⊢ Set.Countable.{u_1} (α := α) (⋃ (n : ℕ), (K : (a : ℕ) → Set α) n)

Tactic:
exact countable_iUnion <| fun i ↦ (K.finite i).countable

Premises used: Set.countable_iUnion, Set.FiniteExhaustion.finite, Set.Finite.countable
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
rw :
  SProd.sprod (α := Set α) (β := Set β) (⋃ (x : ℕ), (K : (a : ℕ) → Set α) x) (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) =
    s ×ˢ t
rw₁ : SProd.sprod (β := Set β) s (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) = s ×ˢ t
rw₂ rw₃ : s ×ˢ t = s ×ˢ t
⊢ ⋃ (n : ℕ),
      SProd.sprod (α := Set α) (β := Set β) ((K : (a : ℕ) → Set α) n : Set α) ((K' : (a : ℕ) → Set β) n : Set β) =
    s ×ˢ t

Tactic:
rw [Set.iUnion_prod_of_monotone (OrderHomClass.mono K) (OrderHomClass.mono K'),
          K.iUnion_eq, K'.iUnion_eq]

Premises used: Set.iUnion_prod_of_monotone, OrderHomClass.mono, Set.FiniteExhaustion.iUnion_eq
-- Module: Mathlib.Data.Set.FiniteExhaustion
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
n : ℕ
⊢ (K.prod (s := s) (t := t) K' : (a : ℕ) → Set (α × β)) n =
    SProd.sprod (α := Set α) (β := Set β) ((K : (a : ℕ) → Set α) n : Set α) ((K' : (a : ℕ) → Set β) n : Set β)

Tactic:
rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
a : α
h : EqOn f₁ f₂ s
ha : a ∈ s
⊢ f₁ a = f₂ a

Tactic:
h ha
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
a : α
⊢ EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a

Tactic:
simp [Set.EqOn]

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ univ ↔ f₁ = f₂

Tactic:
simp [EqOn, funext_iff]

Premises used: funext_iff, Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
h : EqOn f₁ f₂ s
⊢ EqOn f₂ f₁ s

Tactic:
fun _ hx => (h hx).symm

Premises used: Set.EqOn, Eq.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ s ↔ EqOn f₂ f₁ s

Tactic:
⟨EqOn.symm, EqOn.symm⟩

Premises used: Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ EqOn f f s

Tactic:
fun _ _ => rfl

Premises used: Set.EqOn, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ f₃ : α → β
h₁ : EqOn f₁ f₂ s
h₂ : EqOn f₂ f₃ s
⊢ EqOn f₁ f₃ s

Tactic:
fun _ hx =>
  (h₁ hx).trans (h₂ hx)

Premises used: Set.EqOn, Eq.trans
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
⊢ f₁ '' s = f₂ '' s

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
f : α → α
h : EqOn f id s
⊢ f '' s = s

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
heq : EqOn f₁ f₂ s
t : Set β
⊢ s ∩ f₁ ⁻¹' t = s ∩ f₂ ⁻¹' t

Tactic:
grind
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f₁ f₂ : α → β
hs : s₁ ⊆ s₂
hf : EqOn f₁ f₂ s₂
⊢ EqOn f₁ f₂ s₁

Tactic:
fun _ hx => hf (hs hx)

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f₁ f₂ : α → β
⊢ EqOn f₁ f₂ (s₁ ∪ s₂) ↔ EqOn f₁ f₂ s₁ ∧ EqOn f₁ f₂ s₂

Tactic:
forall₂_or_left

Premises used: Set.union, Set.Mem, setOf, forall₂_or_left, Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f₁ f₂ : α → β
h₁ : EqOn f₁ f₂ s₁
h₂ : EqOn f₁ f₂ s₂
⊢ EqOn f₁ f₂ (s₁ ∪ s₂)

Tactic:
eqOn_union.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, Set.eqOn_union, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
f₁ f₂ : α → β
g : β → γ
h : EqOn f₁ f₂ s
⊢ EqOn (g ∘ f₁) (g ∘ f₂) s

Tactic:
fun _ ha =>
  congr_arg _ <| h ha

Premises used: Set.EqOn, congr_arg
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β : Type u_8
δ : Type u_9
γ : Type u_10
op : α → β → δ
a₁ a₂ : γ → α
b₁ b₂ : γ → β
s : Set γ
ha : EqOn a₁ a₂ s
hb : EqOn b₁ b₂ s
⊢ EqOn.{u_10, u_9} (β := δ) (fun (x : γ) ↦ op (a₁ x) (b₁ x)) (fun (x : γ) ↦ op (a₂ x) (b₂ x)) s

Tactic:
fun _ hx ↦ congr_arg₂ _ (ha hx) (hb hx)

Premises used: Set.EqOn, congr_arg₂
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_7
f : ι → α
g₁ g₂ : α → β
⊢ EqOn g₁ g₂ (range f) ↔ g₁ ∘ f = g₂ ∘ f

Tactic:
forall_mem_range.trans <| funext_iff.symm

Premises used: Set.forall_mem_range, funext_iff, Set.EqOn, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ MapsTo f s t ↔ f '' s ⊆ t

Tactic:
image_subset_iff.symm

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.MapsTo, Set.image_subset_iff, Iff.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
⊢ s ⊆ f ⁻¹' t

Tactic:
hf

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

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset, Set.preimage, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ MapsTo (Prod.map f f) (diagonal α) (diagonal β)

Tactic:
mapsTo_iff_subset_preimage.mpr <| diagonal_subset_iff.2 fun _ => rfl

Premises used: Set.mapsTo_iff_subset_preimage, Iff.mpr, Set.diagonal_subset_iff, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
x : α
⊢ MapsTo f {x} t ↔ f x ∈ t

Tactic:
mapsTo_iff_subset_preimage.trans singleton_subset_iff

Premises used: Set.mapsTo_iff_subset_preimage, Set.singleton_subset_iff, Iff.trans
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
t : Set β
⊢ MapsTo f ∅ t

Tactic:
fun _ ↦ False.elim

Premises used: Set.Mem, False.elim, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ MapsTo f s ∅ ↔ s = ∅

Tactic:
simp [mapsTo_iff_image_subset, subset_empty_iff]

Premises used: Set.mapsTo_iff_image_subset, Set.subset_empty_iff
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hs : s.Nonempty
⊢ t.Nonempty

Tactic:
(hs.image f).mono (mapsTo_iff_image_subset.mp h)

Premises used: Set.mapsTo_iff_image_subset, Set.Nonempty.mono, Set.Nonempty.image, Iff.mp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ f '' s ⊆ t

Tactic:
mapsTo_iff_image_subset.1 h

Premises used: Set.mapsTo_iff_image_subset, Iff.mp
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h₁ : MapsTo f₁ s t
h : EqOn f₁ f₂ s
⊢ MapsTo f₂ s t

Tactic:
fun _ hx =>
  h hx ▸ h₁ hx

Premises used: Eq.rec, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hg : EqOn g₁ g₂ t
hf : MapsTo f s t
⊢ EqOn (g₁ ∘ f) (g₂ ∘ f) s

Tactic:
fun _ ha => hg <| hf ha

Premises used: Set.EqOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
H : EqOn f₁ f₂ s
⊢ MapsTo f₁ s t ↔ MapsTo f₂ s t

Tactic:
⟨fun h => h.congr H, fun h => h.congr H.symm⟩

Premises used: Iff.intro, Set.EqOn.symm, Set.MapsTo.congr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h₁ : MapsTo g t p
h₂ : MapsTo f s t
⊢ MapsTo (g ∘ f) s p

Tactic:
fun _ h =>
  h₁ (h₂ h)

Premises used: Set.Mem, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
⊢ MapsTo id s s

Tactic:
fun _ => id

Premises used: Set.Mem, id, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
h₁ : ∀ (x : (↑s : Type u_1)), (↑((restrict f s s h)^[n] x) : α) = (↑(restrict f^[n] s s ⋯ x) : α)
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯

Tactic:
ext
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
x : (↑s : Type u_1)
⊢ (↑((restrict f s s h)^[n] x) : α) = (↑(restrict f^[n] s s ⋯ x) : α)

Tactic:
simpa using coe_iterate_restrict _ _ _

Premises used: Set.MapsTo.coe_iterate_restrict
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst : Subsingleton β
f : α → β
h : s.Nonempty → t.Nonempty
⊢ MapsTo f s t

Tactic:
fun a ha ↦ Subsingleton.mem_iff_nonempty.2 <| h ⟨a, ha⟩

Premises used: Iff.mpr, Subsingleton.mem_iff_nonempty, Set.MapsTo, Exists.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
inst : Subsingleton α
f : α → α
s : Set α
⊢ MapsTo f s s

Tactic:
mapsTo_of_subsingleton' _ id

Premises used: Set.mapsTo_of_subsingleton', id
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
hf : MapsTo f s₁ t₁
hs : s₂ ⊆ s₁
ht : t₁ ⊆ t₂
⊢ MapsTo f s₂ t₂

Tactic:
fun _ hx => ht (hf <| hs hx)

Premises used: Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
f : α → β
hf : MapsTo f s₁ t
hs : s₂ ⊆ s₁
⊢ MapsTo f s₂ t

Tactic:
fun _ hx =>
  hf (hs hx)

Premises used: Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
f : α → β
hf : MapsTo f s t₁
ht : t₁ ⊆ t₂
⊢ MapsTo f s t₂

Tactic:
fun _ hx =>
  ht (hf hx)

Premises used: Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : MapsTo f s₁ t₁
h₂ : MapsTo f s₂ t₂
⊢ MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)

Tactic:
fun _ hx =>
  hx.elim (fun hx => Or.inl <| h₁ hx) fun hx => Or.inr <| h₂ hx

Premises used: Set.MapsTo, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
f : α → β
h₁ : MapsTo f s₁ t
h₂ : MapsTo f s₂ t
⊢ MapsTo f (s₁ ∪ s₂) t

Tactic:
union_self t ▸ h₁.union_union h₂

Premises used: Eq.rec, Set.MapsTo.union_union, Set.union_self
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
f : α → β
⊢ MapsTo f (s₁ ∪ s₂) t ↔ MapsTo f s₁ t ∧ MapsTo f s₂ t

Tactic:
⟨fun h =>
    ⟨h.mono subset_union_left (Subset.refl t),
      h.mono subset_union_right (Subset.refl t)⟩,
    fun h => h.1.union h.2⟩

Premises used: Set.Subset.refl, Set.subset_union_right, Set.MapsTo.mono, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, Set.MapsTo.union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
f : α → β
h₁ : MapsTo f s t₁
h₂ : MapsTo f s t₂
⊢ MapsTo f s (t₁ ∩ t₂)

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

Premises used: Set.Mem, setOf, Set.inter, Set.MapsTo, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

Tactic:
simpa [← singleton_union] using h.mono_right subset_union_right

Premises used: Set.MapsTo.mono_right, Set.subset_union_right, Set.singleton_union
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : MapsTo f s₁ t₁
h₂ : MapsTo f s₂ t₂
⊢ MapsTo f (s₁ ∩ s₂) (t₁ ∩ t₂)

Tactic:
fun _ hx => ⟨h₁ hx.1, h₂ hx.2⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, Set.MapsTo, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
f : α → β
⊢ MapsTo f s (t₁ ∩ t₂) ↔ MapsTo f s t₁ ∧ MapsTo f s t₂

Tactic:
⟨fun h =>
    ⟨h.mono (Subset.refl s) inter_subset_left,
      h.mono (Subset.refl s) inter_subset_right⟩,
    fun h => h.1.inter h.2⟩

Premises used: Set.Subset.refl, Set.MapsTo.mono, Set.inter_subset_left, And.right, And.left, And.intro, Iff.intro, Set.inter_subset_right, Set.MapsTo.inter
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ MapsTo f s univ

Tactic:
fun _ _ => trivial

Premises used: trivial, Set.Mem, Set.univ, setOf, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ MapsTo f s (range f)

Tactic:
(mapsTo_image f s).mono (Subset.refl s) (image_subset_range _ _)

Premises used: Set.Subset.refl, Set.mapsTo_image, Set.image_subset_range, Set.MapsTo.mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : γ → α
s : Set γ
t : Set β
⊢ MapsTo f (g '' s) t ↔ MapsTo (f ∘ g) s t

Tactic:
⟨fun h c hc => h ⟨c, hc, rfl⟩, fun h _ ⟨_, hc⟩ => hc.2 ▸ h hc.1⟩

Premises used: _private.0.Set.mapsTo_image_iff.match_1, Membership.mem, Eq.rec, And.right, And.left, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g : β → γ
hf : MapsTo f s t
⊢ MapsTo (g ∘ f) s (g '' t)

Tactic:
fun x hx ↦ ⟨f x, hf hx, rfl⟩

Premises used: Set.Mem, setOf, Set.MapsTo, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
s : Set β
t : Set γ
hg : MapsTo g s t
f : α → β
⊢ MapsTo (g ∘ f) (f ⁻¹' s) t

Tactic:
fun _ hx ↦ hg hx

Premises used: Set.Mem, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ MapsTo f univ t ↔ ∀ (x : α), f x ∈ t

Tactic:
⟨fun h _ => h (mem_univ _), fun h x _ => h x⟩

Premises used: Iff.intro, Set.mem_univ
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ MapsTo f univ t ↔ range f ⊆ t

Tactic:
mapsTo_univ_iff.trans range_subset_iff.symm

Premises used: Set.mapsTo_univ_iff, Iff.trans, Set.range_subset_iff, Iff.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
t : Set β
f : α → β
g : ι → α
⊢ MapsTo f (range g) t ↔ ∀ (i : ι), f (g i) ∈ t

Tactic:
forall_mem_range

Premises used: Set.forall_mem_range, Set.MapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
hc : MapsTo f sᶜ tᶜ
x : α
⊢ f x ∈ t ↔ x ∈ s

Tactic:
⟨fun ht => by_contra fun hs => hc hs ht, fun hx => h hx⟩

Premises used: Iff.intro, by_contra
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Subsingleton
f : α → β
⊢ InjOn f s

Tactic:
fun _ hx _ hy _ =>
  hs hx hy

Premises used: Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ InjOn f ∅

Tactic:
subsingleton_empty.injOn f

Premises used: Set.subsingleton_empty, Set.Subsingleton.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ InjOn f {a}

Tactic:
subsingleton_singleton.injOn f

Premises used: Set.subsingleton_singleton, Set.Subsingleton.injOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
a b : α
⊢ (∀ ⦃x₁ : α⦄,
      Membership.mem (γ := Set α) {a, b} x₁ →
        ∀ ⦃x₂ : α⦄, Membership.mem (γ := Set α) {a, b} x₂ → f x₁ = f x₂ → x₁ = x₂) ↔
    f a = f b → a = b

Tactic:
aesop
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : ∀ (x y : α), f x = f y ↔ x = y
⊢ InjOn f s

Tactic:
fun x _ y _ => (h x y).mp

Premises used: Iff.mp, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x y : α
h : InjOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y ↔ x = y

Tactic:
⟨h hx hy, fun h => h ▸ rfl⟩

Premises used: Eq.rec, Iff.intro, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
x y : α
h : InjOn f s
hx : x ∈ s
hy : y ∈ s
⊢ f x ≠ f y ↔ x ≠ y

Tactic:
(h.eq_iff hx hy).not

Premises used: Set.InjOn.eq_iff, Iff.not
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
h₁ : InjOn f₁ s
h : EqOn f₁ f₂ s
⊢ InjOn f₂ s

Tactic:
fun _ hx _ hy =>
  h hx ▸ h hy ▸ h₁ hx hy

Premises used: Eq.rec, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
H : EqOn f₁ f₂ s
⊢ InjOn f₁ s ↔ InjOn f₂ s

Tactic:
⟨fun h => h.congr H, fun h => h.congr H.symm⟩

Premises used: Set.InjOn.congr, Iff.intro, Set.EqOn.symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : s₁ ⊆ s₂
ht : InjOn f s₂
⊢ InjOn f s₁

Tactic:
fun _ hx _ hy H =>
  ht (h hx) (h hy) H

Premises used: Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.intro, Iff.intro, Set.InjOn.mono
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
refine_1 : ∀ (H : InjOn f (s₁ ∪ s₂)) (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
refine_2 : (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y

Tactic:
refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x = y

Tactic:
H (Or.inl hx) (Or.inr hy) hxy

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ x ∈ s₂

Tactic:
obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy

Premises used: Or.inl, Or.inr, rfl