awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
⊢ Monotone (image f)

Tactic:
fun _ _ => image_subset_image

Premises used: Monotone, Finset.image_subset_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
hf : Injective f
⊢ Injective (image f)

Tactic:
simpa only [funext (map_eq_image _)] using map_injective ⟨f, hf⟩

Premises used: Function.Embedding.mk, Finset.map_injective, funext, Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s = image f t ↔ s = t

Tactic:
(image_injective hf).eq_iff

Premises used: Finset.image_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s ⊆ image f t ↔ s ⊆ t

Tactic:
mod_cast Set.image_subset_image_iff hf (s := s) (t := t)

Premises used: SetLike.coe_subset_coe._simp_1, congrArg, cast, HasSubset.Subset, Finset.coe_image._simp_3, Iff, Set.image_subset_image_iff, congr, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s s₁ s₂ : Finset α
ht : Set.InjOn f (↑s : Set α)
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ image f s₁ ⊆ image f s₂ ↔ s₁ ⊆ s₂

Tactic:
exact_mod_cast ht.image_subset_image_iff (mod_cast h₁) (mod_cast h₂)

Premises used: Set.InjOn.image_subset_image_iff
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s s₁ s₂ : Finset α
ht : Set.InjOn f (↑s : Set α)
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ image f s₁ = image f s₂ ↔ s₁ = s₂

Tactic:
exact_mod_cast ht.image_eq_image_iff (mod_cast h₁) (mod_cast h₂)

Premises used: Set.InjOn.image_eq_image_iff
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s < image f t ↔ s < t

Tactic:
lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

Premises used: Finset.image_subset_image_iff, lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s t : Finset α
hf : Injective f
⊢ image f s < image f t ↔ s < t

Tactic:
exact lt_iff_lt_of_le_iff_le' (image_subset_image_iff hf) (image_subset_image_iff hf)

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (↑(image f s) : Set β) ⊆ Set.range f

Tactic:
calc
    ↑(s.image f) = f '' ↑s := coe_image
    _ ⊆ Set.range f := Set.image_subset_range f ↑s

Premises used: Trans.trans, Finset.coe_image, Set.image_subset_range, SetLike.coe
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
inst_1 : DecidablePred p
⊢ filter p (image f s) = image f ({a ∈ s | p (f a)})

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
y : β
⊢ {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s

Tactic:
simp [Finset.Nonempty]

Premises used: Finset.Nonempty
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s₁ s₂ : Finset α
⊢ image f (s₁ ∪ s₂) = image f s₁ ∪ image f s₂

Tactic:
mod_cast Set.image_union f s₁ s₂

Premises used: congrArg, SetLike.coe_set_eq._simp_1, Finset.coe_union._simp_1, cast, Finset.coe_image._simp_3, SetLike.coe, congr, Set.image, Union.union, Eq, Finset.image, Eq.trans, Set.image_union
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
⊢ image f (s ∩ t) ⊆ image f s ∩ image f t

Tactic:
(image_mono f).map_inf_le s t

Premises used: Set.Mem, setOf, Monotone.map_inf_le, Finset.image_mono
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f ((↑s : Set α) ∪ (↑t : Set α))
push_cast : f '' ((↑s : Set α) ∩ (↑t : Set α)) = f '' (↑s : Set α) ∩ f '' (↑t : Set α)
⊢ (↑(image f (s ∩ t)) : Set β) = (↑(image f s ∩ image f t) : Set β)

Tactic:
push_cast
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f ((↑s : Set α) ∪ (↑t : Set α))
⊢ f '' ((↑s : Set α) ∩ (↑t : Set α)) = f '' (↑s : Set α) ∩ f '' (↑t : Set α)

Tactic:
Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

Premises used: Set.image_inter_on, Or.inl, Or.inr
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f ((↑s : Set α) ∪ (↑t : Set α))
⊢ f '' ((↑s : Set α) ∩ (↑t : Set α)) = f '' (↑s : Set α) ∩ f '' (↑t : Set α)

Tactic:
exact Set.image_inter_on fun a ha b hb => hf (Or.inr ha) <| Or.inl hb

Premises used: Set.image_inter_on, Or.inl, Or.inr
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
inst_1 : DecidableEq α
s₁ s₂ : Finset α
hf : Injective f
⊢ image f (s₁ ∩ s₂) = image f s₁ ∩ image f s₂

Tactic:
image_inter_of_injOn _ _ hf.injOn

Premises used: Finset.image_inter_of_injOn, Function.Injective.injOn
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
a : α
⊢ image f {a} = {f a}

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
a : α
s : Finset α
⊢ image f (insert a s) = insert (f a) (image f s)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s : Finset α
a : α
⊢ (image f s).erase (f a) ⊆ image f (s.erase a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
hf : Injective f
s : Finset α
a : α
⊢ image f (s.erase a) = (image f s).erase (f a)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ image f s = ∅ ↔ s = ∅

Tactic:
mod_cast Set.image_eq_empty (f := f) (s := s)

Premises used: congrArg, cast, Set.image_eq_empty, Finset.coe_image._simp_3, Iff, congr, Finset.coe_eq_empty._simp_1, congrFun', EmptyCollection.emptyCollection, Eq, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
rw : image f s = ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ ∅ = image f s ↔ s = ∅

Tactic:
rw [eq_comm, image_eq_empty]

Premises used: Finset.image_eq_empty, eq_comm
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
hf : Injective f
⊢ image f (s \ t) = image f s \ image f t

Tactic:
mod_cast Set.image_diff hf s t

Premises used: congrArg, SetLike.coe_set_eq._simp_1, Set.image_diff, cast, Finset.coe_sdiff._simp_1, SDiff.sdiff, Finset.coe_image._simp_3, SetLike.coe, congr, Set.image, Eq, Finset.image, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
inst_1 : DecidableEq α
t : Finset α
hf : Set.InjOn f (↑s : Set α)
hts : t ⊆ s
⊢ image f (s \ t) = image f s \ image f t

Tactic:
mod_cast Set.image_diff_of_injOn hf <| coe_subset.2 hts

Premises used: Iff.mpr, congrArg, SetLike.coe_set_eq._simp_1, cast, Set.image_diff_of_injOn, Finset.coe_sdiff._simp_1, SDiff.sdiff, Finset.coe_image._simp_3, congr, Set.image, Eq, Finset.image, Eq.trans, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s t : Finset α
f : α → β
h : Disjoint (image f s) (image f t)
⊢ Disjoint s t

Tactic:
disjoint_iff_ne.2 fun _ ha _ hb =>
    ne_of_apply_ne f <| h.forall_ne_finset (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)

Premises used: Iff.mpr, Finset.disjoint_iff_ne, Disjoint.forall_ne_finset, ne_of_apply_ne, Finset.mem_image_of_mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
mp : a ∈ Set.range f → Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
mpr : Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a → a ∈ Set.range f
⊢ a ∈ Set.range f ↔ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
mp : ∃ a_1 < n, f a_1 = a
⊢ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a

Tactic:
simp only [mem_image, mem_range]

Premises used: Finset.mem_image, Finset.mem_range
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a

Tactic:
⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩

Premises used: Nat.mod_lt, Eq.congr, HMod.hMod, And.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a

Tactic:
exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h_1 : ∀ (i : ℕ), f (i % n) = f i
h : Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
⊢ ∃ a_1 < n, f a_1 = a

Tactic:
simp only [mem_image, Set.mem_range, mem_range] at *

Premises used: Set.mem_range, Finset.mem_image, Finset.mem_range
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h_1 : ∀ (i : ℕ), f (i % n) = f i
h : ∃ a_1 < n, f a_1 = a
mpr : ∀ i < n, ∀ (ha : f i = a), ∃ (y : ℕ), f y = a
⊢ ∃ (y : ℕ), f y = a

Tactic:
rcases h with ⟨i, _, ha⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
left : i < n
ha : f i = a
⊢ ∃ (y : ℕ), f y = a

Tactic:
⟨i, ha⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
left : i < n
ha : f i = a
⊢ ∃ (y : ℕ), f y = a

Tactic:
exact ⟨i, ha⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % (↑n : ℤ)) = f i
hn' : LT.lt (α := ℤ) 0 (↑n : ℤ)
h_1 : ∃ (i : ℤ), f (i % (↑n : ℤ)) = a
i : ℤ
hi : f (i % (↑n : ℤ)) = a
this : 0 ≤ i % (↑n : ℤ)
rw : i % (↑n : ℤ) < (↑n : ℤ) ∧ f (i % (↑n : ℤ)) = a
⊢ (i % (↑n : ℤ)).toNat < n ∧ f (↑(i % (↑n : ℤ)).toNat : ℤ) = a

Tactic:
rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]

Premises used: Int.toNat_of_nonneg, Int.ofNat_lt
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % (↑n : ℤ)) = f i
hn' : LT.lt (α := ℤ) 0 (↑n : ℤ)
h_1 : ∃ (i : ℤ), f (i % (↑n : ℤ)) = a
i : ℤ
hi : f (i % (↑n : ℤ)) = a
this : 0 ≤ i % (↑n : ℤ)
⊢ i % (↑n : ℤ) < (↑n : ℤ) ∧ f (i % (↑n : ℤ)) = a

Tactic:
⟨Int.emod_lt_of_pos i hn', hi⟩

Premises used: And.intro, Int.emod_lt_of_pos
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % (↑n : ℤ)) = f i
hn' : LT.lt (α := ℤ) 0 (↑n : ℤ)
h_1 : ∃ (i : ℤ), f (i % (↑n : ℤ)) = a
i : ℤ
hi : f (i % (↑n : ℤ)) = a
this : 0 ≤ i % (↑n : ℤ)
⊢ i % (↑n : ℤ) < (↑n : ℤ) ∧ f (i % (↑n : ℤ)) = a

Tactic:
exact ⟨Int.emod_lt_of_pos i hn', hi⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % (↑n : ℤ)) = f i
hn' : LT.lt (α := ℤ) 0 (↑n : ℤ)
h_1 : ∃ i < n, f (↑i : ℤ) = a
i : ℕ
hi : i < n
ha rw : f (↑i : ℤ) = a
rw₁ rw₂ : a = a
⊢ f (HMod.hMod (α := ℤ) (↑i : ℤ) (↑n : ℤ)) = a

Tactic:
rw [Int.emod_eq_of_lt (Int.natCast_nonneg _) (Int.ofNat_lt_ofNat_of_lt hi), ha]

Premises used: Int.emod_eq_of_lt, Int.ofNat_lt_ofNat_of_lt, Int.natCast_nonneg
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
f : ℤ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℤ), f (i % (↑n : ℤ)) = f i
this : (∃ (i : ℤ), f (i % (↑n : ℤ)) = a) ↔ ∃ i < n, f (↑i : ℤ) = a
⊢ a ∈ Set.range f ↔ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f (↑i : ℤ)) (range n)) a

Tactic:
simpa [h]
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : (Multiset.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach.val).dedup = s.val
rw₁ : (Multiset.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.val.attach).dedup = s.val
rw₂ : s.val.dedup = s.val
rw₃ rw₄ : s.val = s.val
⊢ (image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach).val = s.val

Tactic:
rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]

Premises used: Finset.dedup_eq_self, Multiset.attach_map_val, Finset.attach_val, Finset.image_val
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s_1 : Finset α
t : Finset β
a_1 : α
b c : β
a : α
s : Finset α
ha : a ∉ s
x y : ↥s
⊢ Eq.{u_1 + 1} (α := ↥(cons a s ha))
      ((fun (x : ↥s) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯ : ↥(cons a s ha))) x)
      ((fun (x : ↥s) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯ : ↥(cons a s ha))) y) →
    x = y

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s_1 : Finset α
t : Finset β
a_1 : α
b c : β
a : α
s : Finset α
ha : a ∉ s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) a ⋯ ∉
    map { toFun := fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯, inj' := ⋯ } s.attach

Tactic:
simpa
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
h :
  ∀ (x : α) (hx : x ∈ cons a s ha),
    Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) x hx ∈ (cons a s ha).attach ↔
      Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) x hx ∈
        cons (Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) a ⋯)
          (map
            { toFun := fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯, inj' := ⋯ :
              ↥s ↪ ↥(cons a s ha) }
            s.attach)
          ⋯
⊢ (cons a s ha).attach =
    cons (Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) a ⋯)
      (map { toFun := fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯, inj' := ⋯ } s.attach) ⋯

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
x : α
hx : x ∈ cons a s ha
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) x hx ∈ (cons a s ha).attach ↔
    Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) x hx ∈
      cons (Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) a ⋯)
        (map
          { toFun := fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) ⋯, inj' := ⋯ :
            ↥s ↪ ↥(cons a s ha) }
          s.attach)
        ⋯

Tactic:
simpa using hx
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
h :
  ∀ (x : α) (hx : x ∈ insert a s),
    Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) x hx ∈ (insert a s).attach ↔
      Membership.mem (γ := Finset ↥(insert a s))
        (insert (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) a ⋯)
          (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑x : α) ⋯) s.attach))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) x hx)
⊢ (insert a s).attach =
    insert (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) a ⋯)
      (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑x : α) ⋯) s.attach)

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a x : α
hx : x ∈ insert a s
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) x hx ∈ (insert a s).attach ↔
    Membership.mem (γ := Finset ↥(insert a s))
      (insert (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) a ⋯)
        (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑x : α) ⋯) s.attach))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) x hx)

Tactic:
simpa using hx
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s t : Finset α
f : α → β
hf : Injective f
⊢ Disjoint (image f s) (image f t) ↔ Disjoint s t

Tactic:
mod_cast Set.disjoint_image_iff hf (s := s) (t := t)

Premises used: congrArg, Disjoint, cast, Set.disjoint_image_iff, Finset.coe_image._simp_3, Iff, Finset.disjoint_coe._simp_1, congr, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
h : s.Nonempty
b : β
⊢ Eq (α := Finset β) (image (fun (x : α) ↦ b) s) {b}

Tactic:
mod_cast Set.Nonempty.image_const (coe_nonempty.2 h) b

Premises used: Iff.mpr, Finset.coe_nonempty, congrArg, cast, Set.Nonempty.image_const, Finset.coe_eq_singleton._simp_1, Finset.coe_image._simp_3, congrFun', Singleton.singleton, Eq, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α ↪ β
s : Finset α
a : α
simp_rw :
  Eq.{u_2 + 1} (α := Finset β) (image (⇑f : (a : α) → β) (s.erase a) : Finset β)
    (erase (image (⇑f : (a : α) → β) s) ((f : (a : α) → β) a) : Finset β)
⊢ map f (s.erase a) = (map f s).erase ((f : (a : α) → β) a)

Tactic:
simp_rw [map_eq_image]

Premises used: Finset.map_eq_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ Eq.{u_2 + 1} (α := Finset β) (image (⇑f : (a : α) → β) (s.erase a) : Finset β)
    (erase (image (⇑f : (a : α) → β) s) ((f : (a : α) → β) a) : Finset β)

Tactic:
s.image_erase f.2 a

Premises used: Function.Embedding.inj', Finset.image_erase
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ Eq.{u_2 + 1} (α := Finset β) (image (⇑f : (a : α) → β) (s.erase a) : Finset β)
    (erase (image (⇑f : (a : α) → β) s) ((f : (a : α) → β) a) : Finset β)

Tactic:
exact s.image_erase f.2 a

Premises used: Function.Embedding.inj', Finset.image_erase
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
f : α → α
⊢ (image f)^[0] s = image f^[0] s

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

Tactic:
rw [iterate_succ_apply', iterate_succ', ih, image_image]

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

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

Premises used: Function.iterate_succ_apply', Function.iterate_succ', Finset.image_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
s' : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ (filterMap f s' f_inj).val = Multiset.filterMap f s'.val

Tactic:
rfl

Premises used: Multiset.filterMap, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ filterMap f ∅ f_inj = ∅

Tactic:
rfl

Premises used: Multiset.filterMap, Multiset.zero, Finset.filterMap, Finset.empty, Multiset.ofList, List.filterMap, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
s : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
b : β
⊢ b ∈ filterMap f s f_inj ↔ ∃ a ∈ s, f a = some b

Tactic:
s.val.mem_filterMap f

Premises used: Multiset.filterMap, Set.Mem, setOf, Finset.val, Multiset.mem_filterMap, Multiset.Mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
s : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (x : β), x ∈ (↑(filterMap f s f_inj) : Set β) ↔ Membership.mem (γ := Set β) {b : β | ∃ a ∈ s, f a = some b} x

Tactic:
simp only [mem_coe, mem_filterMap, Set.mem_setOf_eq, implies_true]

Premises used: Finset.mem_filterMap, Set.mem_setOf_eq, implies_true, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
s' s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
⊢ ∀ (a a' b : α), b ∈ some a → b ∈ some a' → a = a'

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
x : α
⊢ x ∈ filterMap some s ⋯ ↔ x ∈ s

Tactic:
simp only [mem_filterMap, Option.some.injEq, exists_eq_right]

Premises used: Option.some.injEq, exists_eq_right, Finset.mem_filterMap
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
s t : Finset α
f_inj : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
h : s ⊆ t
⊢ filterMap f s f_inj ⊆ filterMap f t f_inj

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α → Option β
inst : DecidableEq α
inst_1 : DecidableEq β
f_inj : ∀ (a a' : α) (b : β), f a = some b → f a' = some b → a = a'
s : List α
⊢ (List.filterMap f s).toFinset = filterMap f s.toFinset f_inj

Tactic:
simp [← Finset.coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Data.Finset.Image
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
p : α → Prop
inst : DecidablePred p
s : Finset α
x : ↥(filter p s)
⊢ p (↑x : α)

Tactic:
simpa using (Finset.mem_filter.1 x.2).2

Premises used: And.right, Iff.mp, Finset.mem_filter, Subtype.property
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
a : α
ha : p a
⊢ Subtype.mk (p := p) a ha ∈ Finset.subtype p s ↔ (↑(Subtype.mk (p := p) a ha) : α) ∈ s

Tactic:
simp [Finset.subtype, ha]

Premises used: Finset.subtype
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ Finset.subtype p s = ∅ ↔ ∀ (x : α), p x → x ∉ s

Tactic:
simp [Finset.ext_iff, Subtype.forall]

Premises used: Subtype.forall, Finset.ext_iff
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
⊢ Monotone (Finset.subtype p)

Tactic:
fun _ _ h _ hx => mem_subtype.2 <| h <| mem_subtype.1 hx

Premises used: Iff.mpr, Monotone, Finset.mem_subtype, Iff.mp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
h : ∀ (x : α), x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
ext x
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s

Tactic:
simp [@and_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

Premises used: and_comm
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
h : ∀ x ∈ s, p x
⊢ ∀ (a : α), a ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ a ∈ s

Tactic:
simpa [subtype_map] using h

Premises used: Finset.subtype_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
inst : DecidablePred fun (x : α) ↦ x ∈ s
h : ∀ (a : ↥s), Membership.mem (γ := Finset ↥s) (Finset.subtype (fun (x : α) ↦ x ∈ s) s) a ↔ a ∈ s.attach
⊢ Finset.subtype (fun (x : α) ↦ x ∈ s) s = s.attach

Tactic:
ext