awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ Eq.{u_3 + 1} (α := Multiset γ)
    (Multiset.map (comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β)) s.val)
    (Multiset.map (⇑(f.trans g) : (a : α) → γ) s.val)

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
β' : Type u_4
f : β ↪ γ
g : α ↪ β
f' : α ↪ β'
g' : β' ↪ γ
h_comm :
  ∀ (a : α),
    Eq.{u_3 + 1} (α := γ) ((f : (a : β) → γ) ((g : (a : α) → β) a : β) : γ)
      ((g' : (a : β') → γ) ((f' : (a : α) → β') a : β') : γ)
simp_rw : map (g.trans f) s = map (f'.trans g') s
simp_rw₁ :
  map { toFun := comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β), inj' := ⋯ : α ↪ γ }
      s =
    map
      { toFun := comp.{u_1 + 1, u_4 + 1, u_3 + 1} (β := β') (⇑g' : (a : β') → γ) (⇑f' : (a : α) → β'), inj' := ⋯ :
        α ↪ γ }
      s
simp_rw₂ :
  map { toFun := fun (x : α) ↦ (f : (a : β) → γ) ((g : (a : α) → β) x : β), inj' := ⋯ : α ↪ γ } s =
    map { toFun := fun (x : α) ↦ (g' : (a : β') → γ) ((f' : (a : α) → β') x : β'), inj' := ⋯ : α ↪ γ } s
⊢ map f (map g s) = map g' (map f' s)

Tactic:
simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]

Premises used: Function.comp_def, Function.Embedding.trans, Finset.map_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
ga : α ↪ α
gb : β ↪ β
h : Semiconj (α := α) (β := β) (⇑f : (a : α) → β) (⇑ga : (a : α) → α) (⇑gb : (a : β) → β)
⊢ Semiconj (map f) (map ga) (map gb)

Tactic:
fun _ =>
  map_comm h

Premises used: Finset.map_comm, Function.Semiconj
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
f g : α ↪ α
h : Function.Commute (α := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α)
⊢ Function.Commute (map f) (map g)

Tactic:
Function.Semiconj.finset_map h

Premises used: Function.Semiconj.finset_map, Function.Commute
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ map f s₁ ⊆ map f s₂

Tactic:
simp [subset_def, Multiset.map_subset_map h]

Premises used: Finset.subset_def, Multiset.map_subset_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
mp : s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t
mpr : map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ Membership.mem (α := α) s ((f.symm : (a : β) → α) x : α)

Tactic:
simp only [mem_map_equiv] at hx

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : Membership.mem (α := α) s ((f.symm : (a : β) → α) x : α)
⊢ x ∈ t

Tactic:
simpa using h hx
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
mpr : Membership.mem (α := β) t ((f.symm.symm : (a : α) → β) x : β)
⊢ x ∈ map f.symm.toEmbedding t

Tactic:
simp only [mem_map_equiv]

Premises used: Finset.mem_map_equiv
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ Membership.mem (α := β) (map f.toEmbedding s) ((f.symm.symm : (a : α) → β) x : β)

Tactic:
simp [hx]
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ Membership.mem (α := β) t ((f.symm.symm : (a : α) → β) x : β)

Tactic:
exact h (by simp [hx])
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.symm.toEmbedding t ⊆ s ↔ t ⊆ map f.toEmbedding s

Tactic:
simp only [← subset_map_symm, Equiv.symm_symm]

Premises used: Equiv.symm_symm, Finset.subset_map_symm
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
⊢ map f s₁ = map f s₂ ↔ s₁ = s₂

Tactic:
(mapEmbedding f).injective.eq_iff

Premises used: RelEmbedding.injective, Function.Injective.eq_iff, Finset.map, Finset.mapEmbedding
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
⊢ Injective (map f)

Tactic:
(mapEmbedding f).injective

Premises used: RelEmbedding.injective, Finset.map, Finset.mapEmbedding
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s t : Finset α
⊢ map f s ⊂ map f t ↔ s ⊂ t

Tactic:
(mapEmbedding f).lt_iff_lt

Premises used: Set.Mem, setOf, Set.Subset, OrderEmbedding.lt_iff_lt, Finset.mapEmbedding
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (mapEmbedding f : (a : Finset α) → Finset β) s = map f s

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
p : β → Prop
inst : DecidablePred p
⊢ filter p (map f s) = map f (filter (p ∘ (⇑f : (a : α) → β)) s)

Tactic:
eq_of_veq (Multiset.filter_map _ _ _)

Premises used: Finset.eq_of_veq, Multiset.filter_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
inst : DecidablePred p
f : α ↪ β
s : Finset α
inst_1 : DecidablePred fun (x : β) ↦ ∃ (a : α), p a ∧ (f : (a : α) → β) a = x
⊢ map f (filter p s) = {b ∈ map f s | ∃ (a : α), p a ∧ (f : (a : α) → β) a = b}

Tactic:
simp [filter_map]

Premises used: Finset.filter_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
p : ↥s → Prop
inst_1 : DecidablePred p
⊢ filter p s.attach =
    map
      {
        toFun :=
          Subtype.map (p := Membership.mem ({x ∈ s | ∃ (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)}))
            (q := Membership.mem s) id ⋯,
        inj' := ⋯ }
      {x ∈ s | ∃ (h : x ∈ s), p (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)}.attach

Tactic:
eq_of_veq <| Multiset.filter_attach' _ _

Premises used: Finset.eq_of_veq, Multiset.filter_attach'
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ {a ∈ s.attach | p (↑a : α)} =
    map ((Embedding.refl α).subtypeMap (p := Membership.mem (filter p s)) (q := Membership.mem s) ⋯) (filter p s).attach

Tactic:
eq_of_veq <| Multiset.filter_attach _ _

Premises used: Finset.eq_of_veq, Multiset.filter_attach
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
p : α → Prop
inst : DecidablePred p
⊢ map f.toEmbedding (filter p s) = filter (p ∘ (⇑f.symm : (a : β) → α)) (map f.toEmbedding s)

Tactic:
simp only [filter_map, Function.comp_def, Equiv.toEmbedding_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, Equiv.toEmbedding_apply, Function.comp_def, Finset.filter_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
s t : Finset α
f : α ↪ β
⊢ Disjoint (map f s) (map f t) ↔ Disjoint s t

Tactic:
mod_cast Set.disjoint_image_iff f.injective (s := s) (t := t)

Premises used: congrArg, Disjoint, cast, Set.disjoint_image_iff, Iff, Finset.disjoint_coe._simp_1, congr, Function.Embedding.injective, Finset.coe_map._simp_1, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h : Disjoint s₁ s₂
h' : Disjoint (map f s₁) (map f s₂)
⊢ map f (s₁.disjUnion s₂ h) = (map f s₁).disjUnion (map f s₂) h'

Tactic:
eq_of_veq <| Multiset.map_add _ _ _

Premises used: Finset.eq_of_veq, Multiset.map_add
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s₁ s₂ : Finset α
h' : Disjoint (map f s₁) (map f s₂)
h : Disjoint s₁ s₂
⊢ map f (s₁.disjUnion s₂ h) = (map f s₁).disjUnion (map f s₂) h'

Tactic:
map_disjUnion _ _ _

Premises used: Iff.mpr, Finset.disjoint_map, Finset.map_disjUnion
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ map f (s₁ ∪ s₂) = map f s₁ ∪ map 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, Finset.map, cast, SetLike.coe, congr, Finset.coe_map._simp_1, Set.image, Union.union, Eq, DFunLike.coe, Eq.trans, Set.image_union
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ map f (s₁ ∩ s₂) = map f s₁ ∩ map f s₂

Tactic:
mod_cast Set.image_inter f.injective (s := s₁) (t := s₂)

Premises used: congrArg, SetLike.coe_set_eq._simp_1, Finset.map, cast, Set.image_inter, Inter.inter, Finset.coe_inter._simp_1, congr, Function.Embedding.injective, Finset.coe_map._simp_1, Set.image, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
s₁ s₂ : Finset α
⊢ map f (s₁ \ s₂) = map f s₁ \ map f s₂

Tactic:
mod_cast Set.image_diff f.injective (s := s₁) (t := s₂)

Premises used: congrArg, SetLike.coe_set_eq._simp_1, Set.image_diff, Finset.map, cast, Finset.coe_sdiff._simp_1, SDiff.sdiff, SetLike.coe, congr, Function.Embedding.injective, Finset.coe_map._simp_1, Set.image, Eq, DFunLike.coe, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
a : α
⊢ (↑(map f {a}) : Set β) = (↑(singleton (α := β) ((f : (a : α) → β) a : β)) : Set β)

Tactic:
simp only [coe_map, coe_singleton, Set.image_singleton]

Premises used: Finset.coe_singleton, Set.image_singleton, Finset.coe_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (α := β) ((f : (a : α) → β) a : β) (map f s)

Tactic:
simp only [insert_eq, map_union, map_singleton]

Premises used: Finset.insert_eq, Finset.map_singleton, Finset.map_union
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f_1 : α ↪ β
s_1 : Finset α
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ ((f : (a : α) → β) a : β) ∉ map f s

Tactic:
simpa using ha
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
a : α
s : Finset α
ha : a ∉ s
⊢ map f (cons a s ha) = cons ((f : (a : α) → β) a) (map f s) ⋯

Tactic:
eq_of_veq <| Multiset.map_cons f a s.val

Premises used: Multiset.map_cons, Finset.eq_of_veq, Finset.val, DFunLike.coe
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ map f s = ∅ ↔ s = ∅

Tactic:
(map_injective f).eq_iff' (map_empty f)

Premises used: Function.Injective.eq_iff', Finset.map_injective, Finset.map_empty
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
rw : map f s = ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ ∅ = map f s ↔ s = ∅

Tactic:
rw [eq_comm, map_eq_empty]

Premises used: eq_comm, Finset.map_eq_empty
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (map f s).Nonempty ↔ s.Nonempty

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

Premises used: Set.image_nonempty, Finset.coe_nonempty._simp_1, congrArg, cast, Iff, Set.Nonempty, congr, Finset.coe_map._simp_1, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ (map f s).Nontrivial ↔ s.Nontrivial

Tactic:
mod_cast Set.image_nontrivial f.injective (s := s)

Premises used: Set.image_nontrivial, congrArg, cast, Iff, congr, Function.Embedding.injective, Finset.coe_map._simp_1, Set.Nontrivial, Finset.nontrivial_coe._simp_1, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
rw : Multiset.map (⇑(Embedding.subtype fun (x : α) ↦ x ∈ s) : (a : ↥s) → α) s.val.attach = s.val
⊢ (map (Embedding.subtype fun (x : α) ↦ x ∈ s) s.attach).val = s.val

Tactic:
rw [map_val, attach_val]

Premises used: Finset.map_val, Finset.attach_val
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun (x : α) ↦ x ∈ s) : (a : ↥s) → α) s.val.attach = s.val

Tactic:
Multiset.attach_map_val _

Premises used: Set.Mem, setOf, Multiset.attach_map_val, Multiset.Mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun (x : α) ↦ x ∈ s) : (a : ↥s) → α) s.val.attach = s.val

Tactic:
exact Multiset.attach_map_val _

Premises used: Multiset.attach_map_val
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
n i j : ℕ
⊢ Eq (α := ℕ) ((fun (i : ℕ) ↦ i + 1) i) ((fun (i : ℕ) ↦ i + 1) j) → i = j

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
n : ℕ
h :
  0 ∈ range (n + 1) ↔
    Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))) 0
h₁ :
  ∀ (n_1 : ℕ),
    n_1 + 1 ∈ range (n + 1) ↔
      Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))) (n_1 + 1)
⊢ range (n + 1) = insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))

Tactic:
ext (⟨⟩ | ⟨n⟩)
-- Module: Mathlib.Data.Finset.Image
Goal:
n : ℕ
⊢ 0 ∈ range (n + 1) ↔
    Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))) 0

Tactic:
simp [Nat.zero_lt_succ n]

Premises used: Nat.zero_lt_succ
-- Module: Mathlib.Data.Finset.Image
Goal:
n_1 n : ℕ
⊢ n + 1 ∈ range (n_1 + 1) ↔
    Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n_1))) (n + 1)

Tactic:
simp [Nat.zero_lt_succ n]

Premises used: Nat.zero_lt_succ
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).val = (Multiset.map f s.val).dedup

Tactic:
rfl

Premises used: Multiset.dedup, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
⊢ image f ∅ = ∅

Tactic:
rfl

Premises used: Multiset.toFinset, Multiset.dedup, List.dedup, Multiset.zero, Finset.empty, Multiset.ofList, List.pwFilter, List.foldr, Finset.image, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
b : β
⊢ b ∈ image f s ↔ ∃ a ∈ s, f a = b

Tactic:
simp only [mem_def, image_val, mem_dedup, Multiset.mem_map]

Premises used: Multiset.mem_map, Multiset.mem_dedup, Finset.image_val, Finset.mem_def
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
f : α → β
a : α
h : a ∈ s
⊢ f a ∈ image f s

Tactic:
mem_image.2 ⟨_, h, rfl⟩

Premises used: Iff.mpr, Finset.mem_image, And.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
p : β → Prop
⊢ (∀ y ∈ image f s, p y) ↔ ∀ ⦃x : α⦄, x ∈ s → p (f x)

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

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α ↪ β
s : Finset α
⊢ map f s = image (⇑f : (a : α) → β) s

Tactic:
eq_of_veq (s.map f).2.dedup.symm

Premises used: Finset.eq_of_veq, Finset.map, Finset.nodup, Multiset.Nodup.dedup, Eq.symm
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
b c : β
⊢ c ∈ image (const α b) s ↔ s.Nonempty ∧ b = c

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
b : β
⊢ b ∈ image (const α b) s ↔ s.Nonempty

Tactic:
mem_image_const.trans <| and_iff_left rfl

Premises used: Finset.mem_image_const, and_iff_left, Iff.trans, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c_1 : β
c : α → β
p : β → Prop
inst_1 : CanLift β α c p
val : Multiset β
l : List β
hd : l.Nodup
hl : ∀ x ∈ { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) l, nodup := hd : Finset β }, p x
⊢ ∀ x ∈ l, p x

Tactic:
hl

Premises used: Set.Mem, setOf, Multiset.Mem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c_1 : β
c : α → β
p : β → Prop
inst_1 : CanLift β α c p
val : Multiset β
l : List β
hd : l.Nodup
hl : ∀ x ∈ { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) l, nodup := hd : Finset β }, p x
mk :
  ∀ (l : List α) (hd : (List.map c l).Nodup),
    ∃ (y : Finset α),
      image c y = { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) (List.map c l), nodup := hd }
⊢ ∃ (y : Finset α), image c y = { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) l, nodup := hd }

Tactic:
lift l to List α using hl

Premises used: List
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a_1 : α
b c_1 : β
c : α → β
p : β → Prop
inst_1 : CanLift β α c p
val : Multiset β
l : List α
hd : (List.map c l).Nodup
a : β
⊢ a ∈ image c { val := (↑l : Multiset α), nodup := ⋯ : Finset α } ↔
    a ∈ { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) (List.map c l), nodup := hd : Finset β }

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f g : α → β
s : Finset α
t : Finset β
a : α
b c_1 : β
c : α → β
p : β → Prop
inst_1 : CanLift β α c p
val : Multiset β
l : List α
hd : (List.map c l).Nodup
⊢ ∃ (y : Finset α),
    image c y = { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) (List.map c l), nodup := hd }

Tactic:
exact ⟨⟨l, hd.of_map _⟩, ext fun a => by simp⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
h₁ : ∀ (a : β), a ∈ image f s ↔ a ∈ image g s
⊢ image f s = image g s

Tactic:
ext
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
a : β
h₁ : (∃ (x : α) (_ : x ∈ s), f x = a) ↔ ∃ (x : α) (_ : x ∈ s), g x = a
⊢ a ∈ image f s ↔ a ∈ image g s

Tactic:
simp_rw [mem_image, ← bex_def]

Premises used: Finset.mem_image, bex_def
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
a : β
x : α
hx : x ∈ s
rw rw₁ : g x = a ↔ g x = a
⊢ f x = a ↔ g x = a

Tactic:
rw [h hx]
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
a : β
⊢ (∃ (x : α) (_ : x ∈ s), f x = a) ↔ ∃ (x : α) (_ : x ∈ s), g x = a

Tactic:
exact exists₂_congr fun x hx => by rw [h hx]

Premises used: exists₂_congr
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
a : α
hf : Injective f
⊢ f a ∈ image f s ↔ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ ∀ (x : β), x ∈ (↑(image f s) : Set β) ↔ x ∈ f '' (↑s : Set α)

Tactic:
simp only [mem_coe, mem_image, Set.mem_image, implies_true]

Premises used: Finset.mem_image, Set.mem_image, implies_true, Finset.mem_coe
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ (image f s).Nonempty ↔ s.Nonempty

Tactic:
mod_cast Set.image_nonempty (f := f) (s := (s : Set α))

Premises used: Set.image_nonempty, Finset.coe_nonempty._simp_1, congrArg, cast, Finset.coe_image._simp_3, Iff, Set.Nonempty, congr, Eq.trans
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Finset α
h : s.Nonempty
f : α → β
⊢ (image f s).Nonempty

Tactic:
image_nonempty.2 h

Premises used: Iff.mpr, Finset.image_nonempty
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
inst_1 : DecidableEq α
s : Multiset α
x : β
⊢ x ∈ image f s.toFinset ↔ x ∈ (Multiset.map f s).toFinset

Tactic:
simp only [mem_image, Multiset.mem_toFinset, Multiset.mem_map]

Premises used: Finset.mem_image, Multiset.mem_map, Multiset.mem_toFinset
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
H : Set.InjOn f (↑s : Set α)
⊢ (image f s).val = Multiset.map f s.val

Tactic:
(s.2.map_on H).dedup

Premises used: Multiset.dedup, Finset.nodup, Multiset.Nodup.dedup, Multiset.Nodup.map_on
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
x : α
⊢ x ∈ image id s ↔ x ∈ s

Tactic:
simp only [mem_image, id, exists_eq_right]

Premises used: Finset.mem_image, exists_eq_right, id
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ image (fun (x : α) ↦ x) s = s

Tactic:
image_id

Premises used: Finset.image_id
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
f : α → β
s : Finset α
inst_1 : DecidableEq γ
g : β → γ
⊢ (image g (image f s)).val = (image (g ∘ f) s).val

Tactic:
simp only [image_val, dedup_map_dedup_eq, Multiset.map_map]

Premises used: Multiset.map_map, Finset.image_val, Multiset.dedup_map_dedup_eq
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq β
s : Finset α
β' : Type u_4
inst_1 : DecidableEq β'
inst_2 : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
simp_rw : image (f ∘ g) s = image (g' ∘ f') s
simp_rw₁ : Eq.{u_3 + 1} (α := Finset γ) (image (fun (x : α) ↦ f (g x)) s) (image (fun (x : α) ↦ g' (f' x)) s)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
simp_rw [image_image, comp_def, h_comm]

Premises used: Function.comp_def, Finset.image_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
ga : α → α
gb : β → β
h : Semiconj f ga gb
⊢ Semiconj (image f) (image ga) (image gb)

Tactic:
fun _ =>
  image_comm h

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

Tactic:
Function.Semiconj.finset_image h

Premises used: Function.Commute, Function.Semiconj.finset_image
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s₁ s₂ : Finset α
h : s₁ ⊆ s₂
⊢ image f s₁ ⊆ image f s₂

Tactic:
simp only [subset_def, image_val, subset_dedup', dedup_subset', Multiset.map_subset_map h]

Premises used: Finset.subset_def, Multiset.map_subset_map, Multiset.subset_dedup', Multiset.dedup_subset', Finset.image_val
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : image f s ⊆ t ↔ image f s ≤ t
⊢ image f s ⊆ t ↔ f '' (↑s : Set α) ⊆ (↑t : Set β)

Tactic:
norm_cast
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ Set.MapsTo f (↑s : Set α) (↑t : Set β) ↔ image f s ⊆ t

Tactic:
simp [Set.MapsTo, image_subset_iff]

Premises used: Finset.image_subset_iff, Set.MapsTo
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : t ≤ image f s ↔ t ⊆ image f s
⊢ (↑t : Set β) ⊆ f '' (↑s : Set α) ↔ t ⊆ image f s

Tactic:
norm_cast
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s = t ↔ Set.SurjOn f (↑s : Set α) (↑t : Set β) ∧ Set.MapsTo f (↑s : Set α) (↑t : Set β)

Tactic:
grind [mapsTo_iff_image_subset, surjOn_iff_subset_image]

Premises used: Finset.surjOn_iff_subset_image, Finset.mapsTo_iff_image_subset