awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
have trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
Tactic: trans s ×ˢ t
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
have trans₁ : s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
Tactic: trans s ×ˢ t
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
have rw : Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
  (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
Tactic: rw [product_eq_biUnion]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
have rw : Eq (α := Finset (α_1 × β_1)) (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
  (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
Tactic: rw [product_eq_biUnion_right]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
have trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
Tactic: trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β : Type u
inst : (P : Prop) → Decidable P
α_1 β_1 : Type u_1
s : Finset α_1
t : Finset β_1
trans : (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t) = s ×ˢ t
⊢ Eq (α := Finset (α_1 × β_1)) (s.biUnion fun (a : α_1) ↦ image (fun (b : β_1) ↦ (a, b)) t)
    (t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s)
have trans₁ : s ×ˢ t = t.biUnion fun (b : β_1) ↦ image (fun (a : α_1) ↦ (a, b)) s
Tactic: trans s ×ˢ t <;> [rw [product_eq_biUnion]; rw [product_eq_biUnion_right]]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α : Type u
inst : DecidableEq α
s : Finset α
⊢ Eq (α := Id (Finset α)) (traverse pure s) (pure s)
have rw : Eq (α := Id (Finset α)) (Multiset.toFinset <$> pure s.val) (pure s)
Tactic: rw [traverse, Multiset.id_traverse]
-- Lean 4 proof step from Mathlib.Data.Finset.Functor (goal)
Goal:
α β γ : Type u
G : Type u → Type u
inst : Applicative G
inst_1 : CommApplicative G
g : α → G β
h : β → γ
s : Finset α
⊢ Functor.map h <$> traverse g s = traverse (Functor.map h ∘ g) s
have unfold : Functor.map h <$> Multiset.toFinset <$> Multiset.traverse g s.val =
  Multiset.toFinset <$> Multiset.traverse (Functor.map h ∘ g) s.val
Tactic: unfold traverse
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Multiset α
h : s ⋖ t
⊢ s.card ⋖ t.card
have obtain : ∀ (a : α) (h : s ⋖ a ::ₘ s), s.card ⋖ (a ::ₘ s).card
Tactic: obtain ⟨a, rfl⟩ := h.exists_multiset_cons
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s : Multiset α
a : α
h : s ⋖ a ::ₘ s
⊢ s.card ⋖ (a ::ₘ s).card
have rw : s.card ⋖ s.card + 1
Tactic: rw [card_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s_1 t : Multiset α
a : α
s : Multiset α
hs : IsMin s
⊢ IsMin s.card
have rw : IsMin (card.{u_1} (α := α) ⊥)
Tactic: rw [isMin_iff_eq_bot.1 hs]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ t ⋖ s ↔ t ⊆ s ∧ #(s \ t) = 1
have rw : (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1
Tactic: rw [covBy_iff_exists_insert]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1
have mp : (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
mp : (∃ a ∉ t, insert a t = s) → t ⊆ s ∧ #(s \ t) = 1
⊢ (∃ a ∉ t, insert a t = s) ↔ t ⊆ s ∧ #(s \ t) = 1
have mpr : t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ t ⊆ s ∧ #(s \ t) = 1 → ∃ a ∉ t, insert a t = s
have mpr : (t ⊆ s ∧ ∃ (a : α), s \ t = {a}) → ∃ a ∉ t, insert a t = s
Tactic: simp_rw [card_eq_one]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ ∃ a ∉ t, insert a t = s
have mpr : insert a t = s
Tactic: refine ⟨a, (mem_sdiff.1 <| superset_of_eq ha <| mem_singleton_self _).2, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
⊢ insert a t = s
have mpr : {a} ∪ t = s
Tactic: rw [insert_eq, ← ha, sdiff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
mpr : {a} ∪ t = s
⊢ insert a t = s
have mpr₁ : s \ t ∪ t = s
Tactic: rw [insert_eq, ← ha, sdiff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hts : t ⊆ s
a : α
ha : s \ t = {a}
mpr : {a} ∪ t = s
mpr₁ : s \ t ∪ t = s
⊢ insert a t = s
have mpr₂ : s = s
Tactic: rw [insert_eq, ← ha, sdiff_union_of_subset hts]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
⊢ IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ
have simp_rw : IsAtom sᶜ ↔ ∃ (a : α), s = {a}ᶜ
Tactic: simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
simp_rw : IsAtom sᶜ ↔ ∃ (a : α), s = {a}ᶜ
⊢ IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ
have simp_rw₁ : (∃ (a : α), sᶜ = {a}) ↔ ∃ (a : α), s = {a}ᶜ
Tactic: simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s : Finset α
inst : Fintype α
inst_1 : DecidableEq α
simp_rw : IsAtom sᶜ ↔ ∃ (a : α), s = {a}ᶜ
simp_rw₁ : (∃ (a : α), sᶜ = {a}) ↔ ∃ (a : α), s = {a}ᶜ
⊢ IsCoatom s ↔ ∃ (a : α), s = {a}ᶜ
have simp_rw₂ : (∃ (a : α), IsCompl s {a}) ↔ ∃ (a : α), s = {a}ᶜ
Tactic: simp_rw [← isAtom_compl, Finset.isAtom_iff, compl_eq_iff_isCompl, eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin s.val
have rw : IsMin.{u_1} (α := Multiset α) (val ⊥)
Tactic: rw [isMin_iff_eq_bot.1 hs]
-- Lean 4 proof step from Mathlib.Data.Finset.Grade (goal)
Goal:
α : Type u_1
s_1 t : Finset α
a : α
s : Finset α
hs : IsMin s
⊢ IsMin #s
have rw : IsMin (card.{u_1} (α := α) ⊥)
Tactic: rw [isMin_iff_eq_bot.1 hs]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
f : α ≃ β
b : β
⊢ b ∈ map f.toEmbedding s ↔ Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
have simp : (∃ a ∈ s, (f : (a : α) → β) a = b) ↔ Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
Tactic: simp only [mem_map, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α β : Type u_4
h : α = β
s : Finset α
⊢ map (Equiv.cast h).toEmbedding s ≍ s
have subst : map (Equiv.cast sorry).toEmbedding s ≍ s
Tactic: subst h
Cleared hypotheses: β, h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (f.trans g) s).val
have simp : 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: simp only [map_val, Multiset.map_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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 : β') : γ)
⊢ map f (map g s) = map g' (map f' s)
have simp_rw : map (g.trans f) s = map (f'.trans g') s
Tactic: simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ map f (map g s) = map g' (map f' s)
have simp_rw₁ : map { toFun := comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑f : (a : β) → γ) (⇑g : (a : α) → β), inj' := sorry : α ↪ γ } s =
  map
    { toFun := comp.{u_1 + 1, u_4 + 1, u_3 + 1} (β := β') (⇑g' : (a : β') → γ) (⇑f' : (a : α) → β'), inj' := sorry : α ↪ γ }
    s
Tactic: simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ map f (map g s) = map g' (map f' s)
have simp_rw₂ : map { toFun := fun (x : α) ↦ (f : (a : β) → γ) ((g : (a : α) → β) x : β), inj' := sorry : α ↪ γ } s =
  map { toFun := fun (x : α) ↦ (g' : (a : β') → γ) ((f' : (a : α) → β') x : β'), inj' := sorry : α ↪ γ } s
Tactic: simp_rw [map_map, Embedding.trans, Function.comp_def, h_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t
have mp : s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
mp : s ⊆ map f.symm.toEmbedding t → map f.toEmbedding s ⊆ t
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t
have mpr : map f.toEmbedding s ⊆ t → s ⊆ map f.symm.toEmbedding t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (hypothesis)
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
⊢ x ∈ t
have hx₁ : Membership.mem (α := α) s ((f.symm : (a : β) → α) x : α)
Tactic: simp only [mem_map_equiv] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t
have mpr : Membership.mem (α := β) t ((f.symm.symm : (a : α) → β) x : β)
Tactic: simp only [mem_map_equiv]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
⊢ ∅ = map f s ↔ s = ∅
have rw : map f s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, map_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α ↪ β
s : Finset α
rw : map f s = ∅ ↔ s = ∅
⊢ ∅ = map f s ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, map_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (map (Embedding.subtype fun (x : α) ↦ x ∈ s) s.attach).val = s.val
have rw : Multiset.map (⇑(Embedding.subtype fun (x : α) ↦ x ∈ s) : (a : ↥s) → α) s.val.attach = s.val
Tactic: rw [map_val, attach_val]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))
have h : 0 ∈ range (n + 1) ↔
  Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := sorry } (range n))) 0
Tactic: ext (⟨⟩ | ⟨n⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
n : ℕ
h :
  0 ∈ range (n + 1) ↔
    Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))) 0
⊢ range (n + 1) = insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := ⋯ } (range n))
have h₁ : ∀ (n_1 : ℕ),
  n_1 + 1 ∈ range (n + 1) ↔
    Membership.mem (γ := Finset ℕ) (insert 0 (map { toFun := fun (i : ℕ) ↦ i + 1, inj' := sorry } (range n))) (n_1 + 1)
Tactic: ext (⟨⟩ | ⟨n⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ ∃ (y : Finset α), image c y = { val := Quot.mk (⇑(List.isSetoid β) : List β → List β → Prop) l, nodup := hd }
have 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 }
Tactic: lift l to List α using hl
Cleared hypotheses: l, hd, hl
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
⊢ image f s = image g s
have h₁ : ∀ (a : β), a ∈ image f s ↔ a ∈ image g s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g (↑s : Set α)
a : β
⊢ a ∈ image f s ↔ a ∈ image g s
have h₁ : (∃ (x : α) (_ : x ∈ s), f x = a) ↔ ∃ (x : α) (_ : x ∈ s), g x = a
Tactic: simp_rw [mem_image, ← bex_def]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ f x = a ↔ g x = a
have rw : g x = a ↔ g x = a
Tactic: rw [h hx]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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)
⊢ image f (image g s) = image g' (image f' s)
have simp_rw : image (f ∘ g) s = image (g' ∘ f') s
Tactic: simp_rw [image_image, comp_def, h_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ image f (image g s) = image g' (image f' s)
have simp_rw₁ : Eq.{u_3 + 1} (α := Finset γ) (image (fun (x : α) ↦ f (g x)) s) (image (fun (x : α) ↦ g' (f' x)) s)
Tactic: simp_rw [image_image, comp_def, h_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ image f s ⊆ t ↔ f '' (↑s : Set α) ⊆ (↑t : Set β)
have norm_cast : image f s ⊆ t ↔ image f s ≤ t
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ (↑t : Set β) ⊆ f '' (↑s : Set α) ↔ t ⊆ image f s
have norm_cast : t ≤ image f s ↔ t ⊆ image f s
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α → β
s t : Finset α
hf : Set.InjOn f ((↑s : Set α) ∪ (↑t : Set α))
⊢ (↑(image f (s ∩ t)) : Set β) = (↑(image f s ∩ image f t) : Set β)
have push_cast : f '' ((↑s : Set α) ∩ (↑t : Set α)) = f '' (↑s : Set α) ∩ f '' (↑t : Set α)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
⊢ ∅ = image f s ↔ s = ∅
have rw : image f s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, image_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
f : α → β
s : Finset α
rw : image f s = ∅ ↔ s = ∅
⊢ ∅ = image f s ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, image_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
have mp : a ∈ Set.range f → Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ a ∈ Set.range f ↔ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
have mpr : Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a → a ∈ Set.range f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ Membership.mem (γ := Finset α) (image (fun (i : ℕ) ↦ f i) (range n)) a
have mp : ∃ a_1 < n, f a_1 = a
Tactic: simp only [mem_image, mem_range]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (hypothesis)
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 ∈ Set.range f
have h₁ : ∃ a_1 < n, f a_1 = a
Tactic: simp only [mem_image, Set.mem_range, mem_range] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ ∃ (y : ℕ), f y = a
have mpr : ∀ i < n, ∀ (ha : f i = a), ∃ (y : ℕ), f y = a
Tactic: rcases h with ⟨i, _, ha⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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 : ℤ)).toNat < n ∧ f (↑(i % (↑n : ℤ)).toNat : ℤ) = a
have rw : i % (↑n : ℤ) < (↑n : ℤ) ∧ f (i % (↑n : ℤ)) = a
Tactic: rw [← Int.ofNat_lt, Int.toNat_of_nonneg this]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ f (HMod.hMod (α := ℤ) (↑i : ℤ) (↑n : ℤ)) = a
have rw₁ : a = a
Tactic: rw [Int.emod_eq_of_lt (Int.natCast_nonneg _) (Int.ofNat_lt_ofNat_of_lt hi), ha]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ (image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach).val = s.val
have rw : (Multiset.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach.val).dedup = s.val
Tactic: rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : (Multiset.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach.val).dedup = s.val
⊢ (image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach).val = s.val
have rw₁ : (Multiset.map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.val.attach).dedup = s.val
Tactic: rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach).val = s.val
have rw₂ : s.val.dedup = s.val
Tactic: rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
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
⊢ (image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach).val = s.val
have rw₃ : s.val = s.val
Tactic: rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
a : α
s : Finset α
ha : a ∉ s
⊢ (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) ⋯
have 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 sorry)
        (map
          { toFun := fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ cons a s ha) (↑x : α) sorry, inj' := sorry :
            ↥s ↪ ↥(cons a s ha) }
          s.attach)
        sorry
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a : α
⊢ (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)
have 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 sorry)
        (image (fun (x : ↥s) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) (↑x : α) sorry) s.attach))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ insert a s) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : DecidableEq α
f : α ↪ β
s : Finset α
a : α
⊢ map f (s.erase a) = (map f s).erase ((f : (a : α) → β) a)
have simp_rw : Eq.{u_2 + 1} (α := Finset β) (image (⇑f : (a : α) → β) (s.erase a) : Finset β)
  (erase (image (⇑f : (a : α) → β) s) ((f : (a : α) → β) a) : Finset β)
Tactic: simp_rw [map_eq_image]