awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ (image f)^[n + 1] s = image f^[n + 1] s
have succ : image f ((image f)^[n] s) = image f^[n + 1] s
Tactic: rw [iterate_succ_apply', iterate_succ', ih, image_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (image f)^[n + 1] s = image f^[n + 1] s
have succ₁ : image f ((image f)^[n] s) = image (f ∘ f^[n]) s
Tactic: rw [iterate_succ_apply', iterate_succ', ih, image_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (image f)^[n + 1] s = image f^[n + 1] s
have succ₂ : image f (image f^[n] s) = image (f ∘ f^[n]) s
Tactic: rw [iterate_succ_apply', iterate_succ', ih, image_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (image f)^[n + 1] s = image f^[n + 1] s
have succ₃ : image (f ∘ f^[n]) s = image (f ∘ f^[n]) s
Tactic: rw [iterate_succ_apply', iterate_succ', ih, image_image]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
f : α → α
n : ℕ
⊢ (image f)^[n] s = image f^[n] s
have zero : (image f)^[0] s = image f^[0] s
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ_apply', iterate_succ', ih, image_image]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
f : α → α
n : ℕ
zero : (image f)^[0] s = image f^[0] s
⊢ (image f)^[n] s = image f^[n] s
have succ : ∀ (n : ℕ) (ih : (image f)^[n] s = image f^[n] s), (image f)^[n + 1] s = image f^[n + 1] s
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ_apply', iterate_succ', ih, image_image]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s
have h : ∀ (x : α), x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ Finset.subtype (fun (x : α) ↦ x ∈ s) s = s.attach
have h : ∀ (a : ↥s), Membership.mem (γ := Finset ↥s) (Finset.subtype (fun (x : α) ↦ x ∈ s) s) a ↔ a ∈ s.attach
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
p : α → Prop
s : Finset { x : α // p x }
a : α
h : a ∈ map (Embedding.subtype fun (x : α) ↦ p x) s
⊢ p a
have 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)
Tactic: rcases mem_map.1 h with ⟨x, _, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (hypothesis)
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 ∈ t
have ha₁ : a ∈ map (Embedding.subtype fun (x : α) ↦ x ∈ t) s
Tactic: rw [mem_coe] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (↑t : Set β) ⊆ f '' s ↔ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t
have mp : (↑t : Set β) ⊆ f '' s → ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (↑t : Set β) ⊆ f '' s ↔ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t
have mpr : (∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t) → (↑t : Set β) ⊆ f '' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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 := ⋯
⊢ ∃ (s' : Finset α), (↑s' : Set α) ⊆ s ∧ image f s' = t
have 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
Tactic: lift t to Finset s using h
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
have mp : image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
Tactic: refine ⟨t.map (Embedding.subtype _), map_subtype_subset _, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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)
⊢ image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) = image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
have mp : ∀ (y : β),
  y ∈ image f (map (Embedding.subtype fun (x : α) ↦ x ∈ s) t) ↔ y ∈ image (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) t
Tactic: ext y
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
| image Nat.succ (range (k + 1))
have rw : image Nat.succ (insert k (range k))
Tactic: rw [range_add_one]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))
have succ : range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))
Tactic: conv_rhs => rw [range_add_one]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
k : ℕ
hk : range (k + 1) \ {0} = image Nat.succ (range k)
⊢ range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))
have succ : k + 1 ∉ {0}
Tactic: rw [range_add_one, image_insert, ← hk, insert_sdiff_of_notMem]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
n : ℕ
⊢ range (n + 1) \ {0} = image Nat.succ (range n)
have zero : range (HAdd.hAdd (α := ℕ) 0 1) \ {0} = image Nat.succ (range 0)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
n : ℕ
zero : range (HAdd.hAdd (α := ℕ) 0 1) \ {0} = image Nat.succ (range 0)
⊢ range (n + 1) \ {0} = image Nat.succ (range n)
have succ : ∀ (k : ℕ) (hk : range (k + 1) \ {0} = image Nat.succ (range k)),
  range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
⊢ (Equiv.refl α).finsetCongr = Equiv.refl (Finset α)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : 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) =
    s
have 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 sorry) (↑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' := sorry } s) sorry :
              { s : Finset α // ∀ a ∈ s, p a }))
          s))
      a ↔
    a ∈ s
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
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
have h : Membership.mem (γ := Finset { a : α // p a })
    ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
        Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p sorry) (↑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' := sorry } s) sorry :
            { s : Finset α // ∀ a ∈ s, p a }))
        s))
    a →
  a ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ 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
have 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 sorry) (↑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' := sorry } s) sorry :
            { s : Finset α // ∀ a ∈ s, p a }))
        s))
    a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (hypothesis)
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
have h₁ : ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 sorry ∈ s),
  Subtype.mk (p := fun (x : α) ↦ p x) a_1 sorry = 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 *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : Finset { a : α // p a }
a : { a : α // p a }
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
have h₁ : ∃ (a_1 : α) (h : ∃ (x : p a_1), Subtype.mk (p := fun (a : α) ↦ p a) a_1 sorry ∈ s),
  Subtype.mk (p := fun (x : α) ↦ p x) a_1 sorry = 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 *
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
⊢ (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
have 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' := sorry } s) sorry :
                { s : Finset α // ∀ a ∈ s, p a }))
            ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
                Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p sorry) (↑s : Finset α).attach)
              s)) :
        Finset α)
      a ↔
    a ∈ (↑s : Finset α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p 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 α)
have 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' := sorry } s) sorry :
              { s : Finset α // ∀ a ∈ s, p a }))
          ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
              Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p sorry) (↑s : Finset α).attach)
            s)) :
      Finset α)
    a →
  a ∈ (↑s : Finset α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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 α)
⊢ 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 α)
have 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' := sorry } s) sorry :
              { s : Finset α // ∀ a ∈ s, p a }))
          ((fun (s : { s : Finset α // ∀ a ∈ s, p a }) ↦
              Finset.map (Subtype.impEmbedding (Membership.mem (↑s : Finset α)) p sorry) (↑s : Finset α).attach)
            s)) :
      Finset α)
    a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (hypothesis)
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 ∈ (↑s : Finset α)
have h₁ : ∃ (a_1 : α) (h : p a_1),
  (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
      True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a sorry = Subtype.mk (p := fun (a : α) ↦ p a) a_1 sorry) ∧
    a_1 = a
Tactic: simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s : Finset α // ∀ a ∈ s, p a }
a : α
h : 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
have a₁ : ∃ (a_1 : α) (h : p a_1),
  (∃ (a : α) (h_1 : a ∈ (↑s : Finset α)),
      True ∧ Subtype.mk (p := fun (x : α) ↦ p x) a sorry = Subtype.mk (p := fun (a : α) ↦ p a) a_1 sorry) ∧
    a_1 = a
Tactic: simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at *
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
a : α
s : Finset α
⊢ s.val = {a} ↔ s = {a}
have rw : s.val = {a} ↔ s.val = val {a}
Tactic: rw [← val_inj]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial
have rw : (↑s : Set α) = {a} ∨ s.Nontrivial
Tactic: rw [← coe_eq_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
m : Multiset α
hm : m.Nodup
⊢ { val := m, nodup := hm : Finset α }.Nonempty ↔ m ≠ 0
have empty : ∀ {hm : Nodup.{u_1} (α := α) 0}, { val := 0, nodup := hm : Finset α }.Nonempty ↔ Ne.{u_1 + 1} (α := Multiset α) 0 0
Tactic: induction m using Multiset.induction_on
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
m : Multiset α
hm : m.Nodup
empty :
  ∀ {hm : Nodup.{u_1} (α := α) 0}, { val := 0, nodup := hm : Finset α }.Nonempty ↔ Ne.{u_1 + 1} (α := Multiset α) 0 0
⊢ { val := m, nodup := hm : Finset α }.Nonempty ↔ m ≠ 0
have cons : ∀ (a : α) (s : Multiset α),
  (∀ {hm : s.Nodup}, { val := s, nodup := hm : Finset α }.Nonempty ↔ s ≠ 0) →
    ∀ {hm : (a ::ₘ s).Nodup}, { val := a ::ₘ s, nodup := hm : Finset α }.Nonempty ↔ a ::ₘ s ≠ 0
Tactic: induction m using Multiset.induction_on
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (↑(cons a s h) : Set α) = insert a (↑s : Set α)
have h₁ : ∀ (x : α), x ∈ (↑(cons a s h) : Set α) ↔ x ∈ insert a (↑s : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa₂ : insert a (↑s : Set α) ⊆ insert a (↑t : Set α) ↔ s ⊆ t
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]
-- Lean 4 proof step from Mathlib.Data.Finset.Insert (goal)
Goal:
α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
rwa : (↑(cons a s hs) : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₁ : insert a (↑s : Set α) ⊆ (↑(cons a t ht) : Set α) ↔ s ⊆ t
rwa₂ : insert a (↑s : Set α) ⊆ insert a (↑t : Set α) ↔ s ⊆ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t
have rwa₃ : (↑s : Set α) ⊆ (↑t : Set α) ↔ s ⊆ t
Tactic: rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]