awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
s : Finset α
inst : DecidablePred fun (x : α) ↦ x ∈ s
a : ↥s
⊢ Membership.mem (γ := Finset ↥s) (Finset.subtype (fun (x : α) ↦ x ∈ s) s) a ↔ a ∈ s.attach

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
s : Finset { x : α // p x }
a : α
h : a ∈ map (Embedding.subtype fun (x : α) ↦ p x) s
rcases :
  ∀ x ∈ s,
    ∀
      (h :
        Membership.mem (α := α) (map (Embedding.subtype fun (x : α) ↦ p x) s)
          ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x : α)),
      p ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x)
⊢ p a

Tactic:
rcases mem_map.1 h with ⟨x, _, rfl⟩

Premises used: Iff.mp, Finset.mem_map, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
s : Finset { x : α // p x }
x : { x : α // p x }
left : x ∈ s
h :
  Membership.mem (α := α) (map (Embedding.subtype fun (x : α) ↦ p x) s)
    ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x : α)
⊢ p ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x)

Tactic:
x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
s : Finset { x : α // p x }
x : { x : α // p x }
left : x ∈ s
h :
  Membership.mem (α := α) (map (Embedding.subtype fun (x : α) ↦ p x) s)
    ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x : α)
⊢ p ((Embedding.subtype fun (x : α) ↦ p x : (a : { x : α // p x }) → α) x)

Tactic:
exact x.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
p : α → Prop
s : Finset { x : α // p x }
a : α
h : ¬p a
⊢ a ∉ map (Embedding.subtype fun (x : α) ↦ p x) s

Tactic:
mt s.property_of_mem_map_subtype h

Premises used: Finset.property_of_mem_map_subtype, mt
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
t : Set α
s : Finset (↑t : Type u_1)
a : α
ha : a ∈ (↑(map (Embedding.subtype fun (x : α) ↦ x ∈ t) s) : Set α)
⊢ a ∈ map (Embedding.subtype fun (x : α) ↦ x ∈ t) s

Tactic:
rw [mem_coe] at ha

Premises used: Finset.mem_coe
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
t : Set α
s : Finset (↑t : Type u_1)
a : α
ha : a ∈ map (Embedding.subtype fun (x : α) ↦ x ∈ t) s
⊢ a ∈ t

Tactic:
property_of_mem_map_subtype s ha

Premises used: Finset.property_of_mem_map_subtype
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
t : Set α
s : Finset (↑t : Type u_1)
a : α
ha : a ∈ map (Embedding.subtype fun (x : α) ↦ x ∈ t) s
⊢ a ∈ t

Tactic:
convert! property_of_mem_map_subtype s ha

Premises used: Finset.property_of_mem_map_subtype
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
t : Finset β
f : α → β
mp : (↑t : Set β) ⊆ f '' s → ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t
mpr : (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t) → (↑t : Set β) ⊆ f '' s
⊢ (↑t : Set β) ⊆ f '' s ↔ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : (↑t : Set β) ⊆ f '' s
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
⊢ ∀ x ∈ t, x ∈ f '' s

Tactic:
h

Premises used: Set.Subset
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : (↑t : Set β) ⊆ f '' s
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
mp :
  ∀ (t : Finset (↑s : Type u_1)),
    ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
⊢ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t

Tactic:
lift t to Finset s using h

Premises used: Finset, Set.Elem
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
t : Finset (↑s : Type u_1)
⊢ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t

Tactic:
⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩

Premises used: Finset.map_subtype_subset, Finset.map, And.intro, Exists.intro, Function.Embedding.subtype
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
t : Finset (↑s : Type u_1)
mp : image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
⊢ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t

Tactic:
refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
t : Finset (↑s : Type u_1)
mp :
  ∀ (y : β),
    y ∈ image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) ↔
      y ∈ image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
⊢ image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t

Tactic:
ext y
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
f : α → β
this : CanLift β (↑s : Type u_1) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) fun (y : β) ↦ y ∈ f '' s := ⋯
t : Finset (↑s : Type u_1)
y : β
⊢ y ∈ image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t) → (↑t : Set β) ⊆ f '' s

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

Tactic:
simp only [← coe_subset, coe_image, subset_set_image_iff]

Premises used: Finset.coe_image, Finset.subset_set_image_iff, Finset.coe_subset
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : DecidableEq β
t : Finset β
f : α → β
⊢ t ⊆ image f univ ↔ ∃ (s' : Finset α), image f s' = t

Tactic:
simp [subset_image_iff]

Premises used: Finset.subset_image_iff
-- Module: Mathlib.Data.Finset.Image
Goal:
⊢ range (HAdd.hAdd (α := ℕ) 0 1) \ {0} = image Nat.succ (range 0)

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
rw : image Nat.succ (insert k (range k))
| image Nat.succ (range (k + 1))

Tactic:
rw [range_add_one]

Premises used: Finset.range_add_one
-- Module: Mathlib.Data.Finset.Image
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
succ : range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))

Tactic:
conv_rhs => rw [range_add_one]

Premises used: Finset.range_add_one
-- Module: Mathlib.Data.Finset.Image
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
succ : k + 1 ∉ {0}
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))

Tactic:
rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]

Premises used: Finset.insert_sdiff_of_notMem, Finset.range_add_one, Finset.image_insert
-- Module: Mathlib.Data.Finset.Image
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ k + 1 ∉ {0}

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
n : ℕ
zero : range (HAdd.hAdd (α := ℕ) 0 1) \ {0} = image Nat.succ (range 0)
succ :
  ∀ (k : ℕ) (hk : range (k + 1) \ {0} = image Nat.succ (range k)),
    range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))
⊢ range (n + 1) \ {0} = image Nat.succ (range n)

Tactic:
induction n with
  | zero => simp
  | succ k hk =>
    conv_rhs => rw [range_add_one]
    rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
    simp

Premises used: Finset.insert_sdiff_of_notMem, Finset.range_add_one, Finset.image_insert
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : DecidableEq β
f : α → β
m : Multiset α
⊢ (map f m).toFinset = Finset.image f m.toFinset

Tactic:
Finset.val_inj.1 (Multiset.dedup_map_dedup_eq _ _).symm

Premises used: Iff.mp, Eq.symm, Finset.val_inj, Multiset.dedup_map_dedup_eq
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset α
⊢ (fun (s : Finset β) ↦ Finset.map e.symm.toEmbedding s) ((fun (s : Finset α) ↦ Finset.map e.toEmbedding s) s) = s

Tactic:
simp [Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
s : Finset β
⊢ (fun (s : Finset α) ↦ Finset.map e.toEmbedding s) ((fun (s : Finset β) ↦ Finset.map e.symm.toEmbedding s) s) = s

Tactic:
simp [Finset.map_map]

Premises used: Finset.map_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Finset α
⊢ (e.finsetCongr : (a : Finset α) → Finset β) s = Finset.map e.toEmbedding s

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
H :
  ∀ (x : Finset α) (a : α),
    Membership.mem (γ := Finset α) (((Equiv.refl α).finsetCongr : (a : Finset α) → Finset α) x : Finset α) a ↔
      Membership.mem (γ := Finset α) ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) x : Finset α) a
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)

Tactic:
ext
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
x : Finset α
a : α
⊢ Membership.mem (γ := Finset α) (((Equiv.refl α).finsetCongr : (a : Finset α) → Finset α) x : Finset α) a ↔
    Membership.mem (γ := Finset α) ((Equiv.refl (Finset α) : (a : Finset α) → Finset α) x : Finset α) a

Tactic:
simp
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ e.finsetCongr.symm = e.symm.finsetCongr

Tactic:
rfl

Premises used: Finset.map, Equiv.finsetCongr, Equiv.symm, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
H :
  ∀ (x : Finset α) (a : γ),
    Membership.mem (γ := Finset γ) ((e.finsetCongr.trans e'.finsetCongr : (a : Finset α) → Finset γ) x : Finset γ) a ↔
      Membership.mem (γ := Finset γ) (((e.trans e').finsetCongr : (a : Finset α) → Finset γ) x : Finset γ) a
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Tactic:
ext
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x : Finset α
a : γ
⊢ Membership.mem (γ := Finset γ) ((e.finsetCongr.trans e'.finsetCongr : (a : Finset α) → Finset γ) x : Finset γ) a ↔
    Membership.mem (γ := Finset γ) (((e.trans e').finsetCongr : (a : Finset α) → Finset γ) x : Finset γ) a

Tactic:
simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

Premises used: Equiv.trans_toEmbedding, Finset.mem_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ e.finsetCongr.toEmbedding =
    (Finset.mapEmbedding e.toEmbedding).toEmbedding (r := fun (x1 x2 : Finset α) ↦ x1 ≤ x2) (s :=
      fun (x1 x2 : Finset β) ↦ x1 ≤ x2)

Tactic:
rfl

Premises used: Finset.map, rfl
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
h :
  ∀ (a : { a : α // p a }),
    Membership.mem (γ := Finset { a : α // p a })
        ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
            Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
          ((fun (s : Finset { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                  (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
                { s : Finset α // ∀ a ∈ s, p a }))
            s))
        a ↔
      a ∈ s
⊢ (fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
        Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
      ((fun (s : Finset { a : α // p a }) ↦
          (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
              (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
            { s : Finset α // ∀ a ∈ s, p a }))
        s) =
    s

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
h :
  Membership.mem (γ := Finset { a : α // p a })
      ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
          Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
        ((fun (s : Finset { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
              { s : Finset α // ∀ a ∈ s, p a }))
          s))
      a →
    a ∈ s
h₁ :
  a ∈ s →
    Membership.mem (γ := Finset { a : α // p a })
      ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
          Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
        ((fun (s : Finset { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
              { s : Finset α // ∀ a ∈ s, p a }))
          s))
      a
⊢ Membership.mem (γ := Finset { a : α // p a })
      ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
          Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
        ((fun (s : Finset { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
              { s : Finset α // ∀ a ∈ s, p a }))
          s))
      a ↔
    a ∈ s

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
h :
  Membership.mem (γ := Finset { a : α // p a })
    ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
        Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
      ((fun (s : Finset { a : α // p a }) ↦
          (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
              (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
            { s : Finset α // ∀ a ∈ s, p a }))
        s))
    a
⊢ ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯ ∈ s),
    Subtype.mk (p := fun (x : α) ↦ p x) a_1 ⋯ = a

Tactic:
simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding] at *

Premises used: Finset.mem_attach, Subtype.exists, Subtype.impEmbedding, exists_eq_right, exists_and_right, Function.Embedding.coeFn_mk, Finset.mem_map, true_and
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
h : a ∈ s
h₁ :
  ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯ ∈ s),
    Subtype.mk (p := fun (x : α) ↦ p x) a_1 ⋯ = a
⊢ Membership.mem (γ := Finset { a : α // p a })
    ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
        Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
      ((fun (s : Finset { a : α // p a }) ↦
          (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
              (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
            { s : Finset α // ∀ a ∈ s, p a }))
        s))
    a

Tactic:
simp only [Finset.mem_map, Finset.mem_attach, true_and, Subtype.exists, Embedding.coeFn_mk,
      exists_and_right, exists_eq_right, Subtype.impEmbedding] at *

Premises used: Finset.mem_attach, Subtype.exists, Subtype.impEmbedding, exists_eq_right, exists_and_right, Function.Embedding.coeFn_mk, Finset.mem_map, true_and
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
h :
  ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯ ∈ s),
    Subtype.mk (p := fun (x : α) ↦ p x) a_1 ⋯ = a
⊢ a ∈ s

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
h : a ∈ s
⊢ ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯ ∈ s),
    Subtype.mk (p := fun (x : α) ↦ p x) a_1 ⋯ = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a :
  ∀ (a : α),
    Membership.mem (γ := Finset α)
        (↑((fun (s : Finset { a : α // p a }) ↦
                (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                    (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
                  { s : Finset α // ∀ a ∈ s, p a }))
              ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
                  Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
                s)) :
          Finset α)
        a ↔
      a ∈ (↑s : Finset α)
⊢ (fun (s : Finset { a : α // p a }) ↦
        (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
            (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
          { s : Finset α // ∀ a ∈ s, p a }))
      ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
          Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
        s) =
    s

Tactic:
ext a
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
a₁ :
  Membership.mem (γ := Finset α)
      (↑((fun (s : Finset { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                  (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
                { s : Finset α // ∀ a ∈ s, p a }))
            ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
                Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
              s)) :
        Finset α)
      a →
    a ∈ (↑s : Finset α)
a₂ :
  a ∈ (↑s : Finset α) →
    Membership.mem (γ := Finset α)
      (↑((fun (s : Finset { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                  (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
                { s : Finset α // ∀ a ∈ s, p a }))
            ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
                Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
              s)) :
        Finset α)
      a
⊢ Membership.mem (γ := Finset α)
      (↑((fun (s : Finset { a : α // p a }) ↦
              (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                  (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
                { s : Finset α // ∀ a ∈ s, p a }))
            ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
                Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
              s)) :
        Finset α)
      a ↔
    a ∈ (↑s : Finset α)

Tactic:
constructor
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
h :
  Membership.mem (γ := Finset α)
    (↑((fun (s : Finset { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
              { s : Finset α // ∀ a ∈ s, p a }))
          ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
              Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
            s)) :
      Finset α)
    a
⊢ ∃ (a_1 : α) (h : p a_1),
    (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
        True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a ⋯ = Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯) ∧
      a_1 = a

Tactic:
simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at *

Premises used: Finset.mem_attach, Subtype.exists, Subtype.impEmbedding, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
h : a ∈ (↑s : Finset α)
a₁ :
  ∃ (a_1 : α) (h : p a_1),
    (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
        True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a ⋯ = Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯) ∧
      a_1 = a
⊢ Membership.mem (γ := Finset α)
    (↑((fun (s : Finset { a : α // p a }) ↦
            (Subtype.mk (p := fun (s : Finset α) ↦ ∀ a ∈ s, p a)
                (Finset.map { toFun := fun (a : { a : α // p a }) ↦ (↑a : α), inj' := ⋯ } s) ⋯ :
              { s : Finset α // ∀ a ∈ s, p a }))
          ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
              Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p ⋯) (↑s : Finset α).attach)
            s)) :
      Finset α)
    a

Tactic:
simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at *

Premises used: Finset.mem_attach, Subtype.exists, Subtype.impEmbedding, Function.Embedding.coeFn_mk, Finset.mem_map
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
h :
  ∃ (a_1 : α) (h : p a_1),
    (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
        True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a ⋯ = Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯) ∧
      a_1 = a
⊢ a ∈ (↑s : Finset α)

Tactic:
grind
-- Module: Mathlib.Data.Finset.Image
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
h : a ∈ (↑s : Finset α)
⊢ ∃ (a_1 : α) (h : p a_1),
    (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
        True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a ⋯ = Subtype.mk (p := fun (a : α) ↦ p a) a_1 ⋯) ∧
      a_1 = a

Tactic:
grind
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
⊢ Eq (α := Multiset α) (val {a}) {a}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a b : α
⊢ Membership.mem (γ := Finset α) {a} b ↔ b = a

Tactic:
Multiset.mem_singleton

Premises used: Set.Mem, setOf, Multiset.Mem, Multiset.mem_singleton
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
x y : α
h : Membership.mem (γ := Finset α) {y} x
⊢ x = y

Tactic:
mem_singleton.1 h

Premises used: Finset.mem_singleton, Iff.mp
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a b : α
⊢ a ∉ {b} ↔ a ≠ b

Tactic:
not_congr mem_singleton

Premises used: Finset.mem_singleton, not_congr
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
⊢ Membership.mem (γ := Finset α) {a} a

Tactic:
mem_singleton.mpr rfl

Premises used: Iff.mpr, Finset.mem_singleton, rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
rw : s.val = {a} ↔ s.val = val {a}
⊢ s.val = {a} ↔ s = {a}

Tactic:
rw [← val_inj]

Premises used: Finset.val_inj
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s.val = val {a}

Tactic:
rfl
-- Module: Mathlib.Data.Finset.Insert
Goal:
α : Type u_1
⊢ Injective (β := Finset α) singleton

Tactic:
fun _a _b h =>
  mem_singleton.1 (h ▸ mem_singleton_self _)

Premises used: Finset.mem_singleton, Finset.mem_singleton_self, Eq.rec, Iff.mp, Function.Injective