awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
s : Set α
n : ℕ
ih :
  HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
f : α →₀ ℕ
h : Membership.mem (γ := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s} f
f_deg : (degree : (a : α →₀ ℕ) → ℕ) f = n + 1
f_supp : (↑f.support : Set α) ⊆ s
i : α
hi : i ∈ f.support
⊢ f ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)
have succ : ∀ (x : α →₀ ℕ) (hx : f = x + single i 1),
  f ∈
    HAdd.hAdd (α := Set (α →₀ ℕ)) {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
      ((fun (x : α) ↦ single x 1) '' s)
Tactic: obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
n : ℕ
s : Set α
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have zero : HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
  {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
Tactic: induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
n : ℕ
s : Set α
zero :
  HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have succ : ∀ (n : ℕ)
  (ih :
    HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}),
  HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
Tactic: induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
n : ℕ
s : Set α
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have zero : HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
  {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
Tactic: classical
  induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
n : ℕ
s : Set α
zero :
  HSMul.hSMul (α := ℕ) (β := Set (α →₀ ℕ)) 0 ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | Eq (α := ℕ) ((degree : (a : α →₀ ℕ) → ℕ) x : ℕ) (0 : ℕ) ∧ (↑x.support : Set α) ⊆ s}
⊢ HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have succ : ∀ (n : ℕ)
  (ih :
    HSMul.hSMul (β := Set (α →₀ ℕ)) n ((fun (x : α) ↦ single x 1) '' s) =
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}),
  HSMul.hSMul (β := Set (α →₀ ℕ)) (n + 1) ((fun (x : α) ↦ single x 1) '' s) =
    {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n + 1 ∧ (↑x.support : Set α) ⊆ s}
Tactic: classical
  induction n with
  | zero => aesop (add simp degree_eq_zero_iff)
  | succ n ih =>
    rw [succ_nsmul, ih]
    refine subset_antisymm ?_ fun f ⟨f_deg, f_supp⟩ ↦ ?_
    · simp [Set.subset_def, Set.mem_add, @forall_comm (α →₀ ℕ)]; grind
    obtain ⟨i, hi⟩ : f.support.Nonempty := by aesop
    obtain ⟨x, hx⟩ := le_iff_exists_add'.mp
      (show single i 1 ≤ f by simpa [Nat.one_le_iff_ne_zero] using hi)
    exact ⟨x, by aesop (add simp Set.subset_def), _, ⟨_, f_supp (by simp_all), rfl⟩, hx.symm⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have suffices : ∀ (s : Set (α →₀ ℕ)),
  HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
Tactic: suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s_1 : Set α
s : Set (α →₀ ℕ)
⊢ HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
have refine : Eq.{u_6 + 1} (α := Set β)
  ((⇑{
          toFun :=
            (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
              (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
          map_one' := sorry, map_mul' := sorry } :
      (a : Multiplicative (α →₀ ℕ)) → β) ''
    s ^ n)
  ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s))
Tactic: refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have suffices : ∀ (s : Set (α →₀ ℕ)),
  HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
Tactic: classical
  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
  intro s
  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
α : Type u_5
β : Type u_6
inst : CommMonoid β
f : α → β
n : ℕ
s : Set α
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (s : Set (α →₀ ℕ)),
    HPow.hPow (α := Set β) ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' s) n =
      (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s)
⊢ (f '' s) ^ n =
    (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ''
      {x : α →₀ ℕ | (degree : (a : α →₀ ℕ) → ℕ) x = n ∧ (↑x.support : Set α) ⊆ s}
have suffices₄ : ∀ (s : Set (α →₀ ℕ)),
  Eq.{u_6 + 1} (α := Set β)
    ((⇑{
            toFun :=
              (fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) ∘
                (⇑Multiplicative.toAdd : (a : Multiplicative (α →₀ ℕ)) → α →₀ ℕ),
            map_one' := sorry, map_mul' := sorry } :
        (a : Multiplicative (α →₀ ℕ)) → β) ''
      s ^ n)
    ((fun (x : α →₀ ℕ) ↦ x.prod fun (x1 : α) (x2 : ℕ) ↦ f x1 ^ x2) '' (n • s))
Tactic: classical
  suffices ∀ (s : Set (α →₀ ℕ)), ((·.prod (f · ^ ·)) '' s) ^ n = (·.prod (f · ^ ·)) '' (n • s) by
    simp [← nsmul_single_one_image, ← this, Set.image_image]
  intro s
  refine (Set.image_pow (⟨⟨(·.prod (f · ^ ·)) ∘ Multiplicative.toAdd, by simp⟩,
    by simp [Finsupp.prod_add_index, pow_add]⟩ : Multiplicative (α →₀ ℕ) →* β) _ _).symm.trans ?_
  simp [-Function.comp_apply, Set.image_comp, show Multiplicative.toAdd '' s = s from
    Set.image_id _]
-- Lean 4 proof step from Mathlib.Data.Finsupp.WellFounded (goal)
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
⊢ Acc (Finsupp.Lex r s) x
have rw : Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x
Tactic: rw [lex_eq_invImage_dfinsupp_lex]
-- Lean 4 proof step from Mathlib.Data.Finsupp.WellFounded (goal)
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x
have refine : ∀ i ∈ x.toDFinsupp.support (β := fun (x : α) ↦ N), Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) i
Tactic: refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)
-- Lean 4 proof step from Mathlib.Data.Finsupp.WellFounded (goal)
Goal:
α : Type u_1
N : Type u_2
inst : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex (α := fun (x : α) ↦ N) r fun (x : α) ↦ s) toDFinsupp) x
have refine : ∀ i ∈ x.toDFinsupp.support (β := fun (x : α) ↦ N), Acc (rᶜ ⊓ fun (x1 x2 : α) ↦ x1 ≠ x2) i
Tactic: classical
    refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)
    simpa only [toDFinsupp_support] using h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
inst : Finite α
⊢ Nonempty.{u_4 + 1} (Fintype α)
have rcases : ∀ (n : ℕ) (e : α ≃ Fin n), Nonempty.{u_4 + 1} (Fintype α)
Tactic: rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
⊢ (finRange n).toFinset = univ
have h : ∀ (a : Fin n), a ∈ (finRange n).toFinset ↔ Membership.mem (γ := Finset (Fin n)) univ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ image i.succAbove univ = {i}ᶜ
have h : ∀ (m : Fin (n + 1)), m ∈ image i.succAbove univ ↔ Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ m
Tactic: ext m
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin (n + 1))) (image succ univ) {0}ᶜ
have rw : Eq (α := Finset (Fin (n + 1))) (image (succAbove 0) univ) {0}ᶜ
Tactic: rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
rw : Eq (α := Finset (Fin (n + 1))) (image (succAbove 0) univ) {0}ᶜ
⊢ Eq (α := Finset (Fin (n + 1))) (image succ univ) {0}ᶜ
have rw₁ : Eq (α := Finset (Fin (n + 1))) {0}ᶜ {0}ᶜ
Tactic: rw [← Fin.succAbove_zero, Fin.image_succAbove_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin (n + 1))) (image castSucc univ) {last n}ᶜ
have rw : image (last n).succAbove univ = {last n}ᶜ
Tactic: rw [← Fin.succAbove_last, Fin.image_succAbove_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
n : ℕ
rw : image (last n).succAbove univ = {last n}ᶜ
⊢ Eq (α := Finset (Fin (n + 1))) (image castSucc univ) {last n}ᶜ
have rw₁ : Eq (α := Finset (Fin (n + 1))) {last n}ᶜ {last n}ᶜ
Tactic: rw [← Fin.succAbove_last, Fin.image_succAbove_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
s : Multiset α
l : List α
h : ∃ (x : α), x ∈ ⟦l⟧
h_1 : ∃ (x : α), x ∈ ⟦[]⟧
⊢ False
have tauto : ∀ w ∈ ⟦l⟧, ∀ w ∈ ⟦[]⟧, False
Tactic: tauto
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
e : α ≃ β
⊢ Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ)) (val univ)
have rw : map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ) = (Finset.map e.toEmbedding univ).val
Tactic: rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
e : α ≃ β
rw : map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ) = (Finset.map e.toEmbedding univ).val
⊢ Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ)) (val univ)
have rw₁ : Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
  (map.{u_2, u_1} (α := α) (⇑e.toEmbedding : (a : α) → β) (val univ))
Tactic: rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
e : α ≃ β
rw : map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ) = (Finset.map e.toEmbedding univ).val
rw₁ :
  Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
    (map.{u_2, u_1} (α := α) (⇑e.toEmbedding : (a : α) → β) (val univ))
⊢ Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ)) (val univ)
have rw₂ : Eq.{u_2 + 1} (α := Multiset β) (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
  (map.{u_2, u_1} (α := α) (⇑e : (a : α) → β) (val univ))
Tactic: rw [← congr_arg Finset.val (Finset.map_univ_equiv e), Finset.map_val, Equiv.coe_toEmbedding]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ Nonempty α
have rcases : ∀ (y : α), (P y ∧ ∀ (x : α), Membership.mem (γ := Finset α) ∅ x → r x y) → Nonempty α
Tactic: rcases h ∅ (by simp) with ⟨y, _⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (hypothesis)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have this : Nonempty α
Tactic: have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
this : Nonempty α
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have choose! : ∀ (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
  ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: choose! F hF using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (hypothesis)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
Tactic: have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (hypothesis)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have hf : let f := seqOfForallFinsetExistsAux P r h';
f = seqOfForallFinsetExistsAux P r h'
Tactic: set f := seqOfForallFinsetExistsAux P r h' with hf
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
⊢ P (f n)
have h : ∀ (n : ℕ) (IH : ∀ m < n, P (f m)), P (f n)
Tactic: induction n using Nat.strong_induction_on with | _ n IH
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)
have h : ∀ (IH' : ∀ (x : Fin n), P (f (↑x : ℕ))), P (f n)
Tactic: have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f (↑x : ℕ))
⊢ P (f n)
have h : P
  (Classical.choose (p := fun (x : α) ↦
    (∀ (x : α),
        Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
          P x) →
      P x ∧
        ∀ (x_1 : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
              x_1 →
            r x_1 x)
    sorry)
Tactic: rw [hf, seqOfForallFinsetExistsAux]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (hypothesis)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have A : ∀ (n : ℕ), P (f n)
Tactic: have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have refine : ∀ (m n : ℕ) (hmn : m < n), r (f m) (f n)
Tactic: refine ⟨f, A, fun m n hmn => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)
have rw : r (f m)
  (Classical.choose (p := fun (x : α) ↦
    (∀ (x : α),
        Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
          P x) →
      P x ∧
        ∀ (x_1 : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
              x_1 →
            r x_1 x)
    sorry)
Tactic: rw [seqOfForallFinsetExistsAux]
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : (s : Finset α) → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m)
    (Classical.choose (p := fun (x : α) ↦
      (∀ (x : α),
          Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ) x →
            P x) →
        P x ∧
          ∀ (x_1 : α),
            Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ seqOfForallFinsetExistsAux P r h' (↑i : ℕ)) univ)
                x_1 →
              r x_1 x)
      ⋯)
have a : Membership.mem (γ := Finset α) (image (fun (i : Fin n) ↦ f (↑i : ℕ)) univ) (f m)
Tactic: apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have : Nonempty α
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩