awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
a₁ :
  ((if ¬a = a then count a (↑m : Multiset α) else 0) + if a = a then count a (↑m : Multiset α) else 0) =
    count a (↑m : Multiset α)
⊢ ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
have a₂ : ∀ (h : a ≠ b),
  ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
Tactic: obtain rfl | h := eq_or_ne a b
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
⊢ ((if ¬a = a then count a (↑m : Multiset α) else 0) + if a = a then count a (↑m : Multiset α) else 0) =
    count a (↑m : Multiset α)
have a₁ : (if ¬a = a then count a (↑m : Multiset α) else 0) + count a (↑m : Multiset α) = count a (↑m : Multiset α)
Tactic: rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
a₁ : (if ¬a = a then count a (↑m : Multiset α) else 0) + count a (↑m : Multiset α) = count a (↑m : Multiset α)
⊢ ((if ¬a = a then count a (↑m : Multiset α) else 0) + if a = a then count a (↑m : Multiset α) else 0) =
    count a (↑m : Multiset α)
have a₂ : 0 + count a (↑m : Multiset α) = count a (↑m : Multiset α)
Tactic: rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
a₁ : (if ¬a = a then count a (↑m : Multiset α) else 0) + count a (↑m : Multiset α) = count a (↑m : Multiset α)
a₂ : 0 + count a (↑m : Multiset α) = count a (↑m : Multiset α)
⊢ ((if ¬a = a then count a (↑m : Multiset α) else 0) + if a = a then count a (↑m : Multiset α) else 0) =
    count a (↑m : Multiset α)
have a₃ : count a (↑m : Multiset α) = count a (↑m : Multiset α)
Tactic: rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
have a₁ : (count b (↑m : Multiset α) + if a = b then count a (↑m : Multiset α) else 0) = count b (↑m : Multiset α)
Tactic: rw [if_pos h, if_neg h, add_zero]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
a₁ : (count b (↑m : Multiset α) + if a = b then count a (↑m : Multiset α) else 0) = count b (↑m : Multiset α)
⊢ ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
have a₂ : count b (↑m : Multiset α) + 0 = count b (↑m : Multiset α)
Tactic: rw [if_pos h, if_neg h, add_zero]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
a₁ : (count b (↑m : Multiset α) + if a = b then count a (↑m : Multiset α) else 0) = count b (↑m : Multiset α)
a₂ : count b (↑m : Multiset α) + 0 = count b (↑m : Multiset α)
⊢ ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
have a₃ : count b (↑m : Multiset α) = count b (↑m : Multiset α)
Tactic: rw [if_pos h, if_neg h, add_zero]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ))
h : a ∉ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
⊢ (↑((filterNe a
              (fill a (m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
                (m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))))).snd
          (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) :
      Multiset α) =
    (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α)
have rw : filter (fun (x : α) ↦ a ≠ x)
    ((↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α) +
      (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)) =
  (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α)
Tactic: rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ))
h : a ∉ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
⊢ filter (fun (x : α) ↦ a ≠ x)
      ((↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α) +
        (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)) =
    (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α)
have rw : ∀ (a_1 : α),
  a_1 ∉
    filter (fun (x : α) ↦ a ≠ x)
      (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)
Tactic: rw [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ))
h : a ∉ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
rw :
  ∀ (a_1 : α),
    a_1 ∉
      filter (fun (x : α) ↦ a ≠ x)
        (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)
⊢ filter (fun (x : α) ↦ a ≠ x)
      ((↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α) +
        (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)) =
    (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α)
have rw₁ : ∀ a_1 ∈ (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α), a ≠ a_1
Tactic: rw [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ))
h : a ∉ m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))
b : α
hb :
  b ∈
    filter (fun (x : α) ↦ a ≠ x)
      (↑(replicate (↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) a) : Multiset α)
⊢ False
have hb₁ : ((↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ b = a) ∧ a ≠ b
Tactic: rw [mem_filter, Sym.mem_coe, mem_replicate] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - (↑i : ℕ))
hx : x ≠ a
⊢ count x (↑(fill a i s) : Multiset α) = count x (↑s : Multiset α)
have suffices : x ∉ Multiset.replicate (↑i : ℕ) a
Tactic: suffices x ∉ Multiset.replicate i a by simp [coe_fill, coe_replicate, this]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
⊢ decode (encode s) = s
have pos : ∀ (h : none ∈ s), decode (encode s) = s
Tactic: by_cases h : none ∈ s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
pos : ∀ (h : none ∈ s), decode (encode s) = s
⊢ decode (encode s) = s
have neg : ∀ (h : none ∉ s), decode (encode s) = s
Tactic: by_cases h : none ∈ s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ decode (encode s) = s
have neg : map (fun (x : { x : Option α // x ∈ s }) ↦ (↑x : Option α)) s.attach = s
Tactic: simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n ⊕ Sym α n.succ
⊢ encode (decode s) = s
have inl : ∀ (s : Sym (Option α) n), encode (decode (Sum.inl s)) = Sum.inl s
Tactic: obtain s | s := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n ⊕ Sym α n.succ
inl : ∀ (s : Sym (Option α) n), encode (decode (Sum.inl s)) = Sum.inl s
⊢ encode (decode s) = s
have inr : ∀ (s : Sym α n.succ), encode (decode (Sum.inr s)) = Sum.inr s
Tactic: obtain s | s := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
⊢ Eq (α := Sym (Option α) n ⊕ Sym α n.succ)
    (if h : none ∈ decode (Sum.inr s) then Sum.inl ((decode (Sum.inr s)).erase none h)
    else
      Sum.inr
        (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯)
          (decode (Sum.inr s)).attach))
    (Sum.inr s)
have pos : ∀ (h : none ∈ decode (Sum.inr s)), False
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
pos : ∀ (h : none ∈ decode (Sum.inr s)), False
⊢ Eq (α := Sym (Option α) n ⊕ Sym α n.succ)
    (if h : none ∈ decode (Sum.inr s) then Sum.inl ((decode (Sum.inr s)).erase none h)
    else
      Sum.inr
        (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯)
          (decode (Sum.inr s)).attach))
    (Sum.inr s)
have neg : ∀ (h : none ∉ decode (Sum.inr s)),
  Eq (α := Sym (Option α) n ⊕ Sym α n.succ)
    (Sum.inr
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get sorry) (decode (Sum.inr s)).attach))
    (Sum.inr s)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
⊢ False
have pos : ∀ a ∈ (↑s : Multiset α),
  ∀ (ha : Eq (α := Option α) ((Embedding.some : (a : α) → Option α) a : Option α) (none : Option α)), False
Tactic: obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ Eq (α := Sym (Option α) n ⊕ Sym α n.succ)
    (Sum.inr
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach))
    (Sum.inr s)
have neg : map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get sorry) (decode (Sum.inr s)).attach = s
Tactic: refine congr_arg Sum.inr ?_
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach = s
have neg : map some
    (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get sorry) (decode (Sum.inr s)).attach) =
  map some s
Tactic: refine map_injective (Option.some_injective _) _ ?_
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach) =
    map some s
have neg : map some
    (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get sorry) (decode (Sum.inr s)).attach) =
  map (Subtype.val (p := fun (x : Option α) ↦ x ∈ decode (Sum.inr s))) (decode (Sum.inr s)).attach
Tactic: refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_)
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
neg :
  map some
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach) =
    map (Subtype.val (p := fun (x : Option α) ↦ x ∈ decode (Sum.inr s))) (decode (Sum.inr s)).attach
⊢ map some
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach) =
    map some s
have neg₁ : decode (Sum.inr s) = map some s
Tactic: refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_)
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
⊢ (fun (s : Sym (Fin n.succ) k) ↦
        (Subtype.mk (p := fun (s : Sym (Fin n.succ.succ) k) ↦ 0 ∉ s) (map (Fin.succAbove 0) s) ⋯ :
          { s : Sym (Fin n.succ.succ) k // 0 ∉ s }))
      ((fun (s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }) ↦ map (Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k)) s) =
    s
have a : (↑((fun (s : Sym (Fin n.succ) k) ↦
          (Subtype.mk (p := fun (s : Sym (Fin n.succ.succ) k) ↦ 0 ∉ s) (map (Fin.succAbove 0) s) sorry :
            { s : Sym (Fin n.succ.succ) k // 0 ∉ s }))
        ((fun (s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }) ↦ map (Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k))
          s)) :
    Sym (Fin n.succ.succ) k) =
  (↑s : Sym (Fin n.succ.succ) k)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
⊢ (↑((fun (s : Sym (Fin n.succ) k) ↦
            (Subtype.mk (p := fun (s : Sym (Fin n.succ.succ) k) ↦ 0 ∉ s) (map (Fin.succAbove 0) s) ⋯ :
              { s : Sym (Fin n.succ.succ) k // 0 ∉ s }))
          ((fun (s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }) ↦ map (Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k))
            s)) :
      Sym (Fin n.succ.succ) k) =
    (↑s : Sym (Fin n.succ.succ) k)
have a : map (Fin.succAbove 0 ∘ Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k) = (↑s : Sym (Fin n.succ.succ) k)
Tactic: simp only [map_map]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
⊢ map (Fin.succAbove 0 ∘ Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k) = (↑s : Sym (Fin n.succ.succ) k)
have a : ∀ (v : Fin (n.succ + 1)) (hv : v ∈ (↑s : Sym (Fin n.succ.succ) k)), (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v
Tactic: refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)
have rw : Fintype.card (Sym (Fin 0) (k + 1)) = 0
Tactic: rw [multichoose_zero_succ]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (k + 1)
have rw : Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
Tactic: rw [multichoose_succ_succ, ← card_sym_fin_eq_multichoose (n + 1) (k + 1),
      ← card_sym_fin_eq_multichoose (n + 2) k, add_comm (Fintype.card _), ← card_sum]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
have refine : Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
Tactic: refine Fintype.card_congr (Equiv.symm ?_)
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
n k : ℕ
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
have apply : { s : Sym (Fin (n + 1 + 1)) (k + 1) // 0 ∈ s } ⊕ { s : Sym (Fin n.succ.succ) (k + 1) // 0 ∉ s } ≃
  Sym (Fin (n + 2)) (k + 1)
Tactic: apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_2
k : ℕ
inst : Fintype α
inst_1 : Fintype (Sym α k)
⊢ Fintype.card.{u_2} (Sym α k) = (Fintype.card α).multichoose k
have rw : Fintype.card.{u_2} (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
Tactic: rw [← card_sym_fin_eq_multichoose]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_2
inst : Fintype α
k : ℕ
inst_1 : Fintype (Sym α k)
⊢ Fintype.card.{u_2} (Sym α k) = (Fintype.card α + k - 1).choose k
have rw : (Fintype.card α).multichoose k = (Fintype.card α + k - 1).choose k
Tactic: rw [card_sym_eq_multichoose, Nat.multichoose_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_2
inst : Fintype α
k : ℕ
inst_1 : Fintype (Sym α k)
rw : (Fintype.card α).multichoose k = (Fintype.card α + k - 1).choose k
⊢ Fintype.card.{u_2} (Sym α k) = (Fintype.card α + k - 1).choose k
have rw₁ : (Fintype.card α + k - 1).choose k = (Fintype.card α + k - 1).choose k
Tactic: rw [card_sym_eq_multichoose, Nat.multichoose_eq]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ 2 * #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag
have rw : ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2
Tactic: rw [card_eq_sum_card_image (Sym2.mk.uncurry : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2
have this : ∀ (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b ∨ b ≠ a),
  {z ∈ s.offDiag | uncurry Sym2.mk z = s(a, b)} = cons (a, b) {(b, a)} sorry
Tactic: have (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b ∨ b ≠ a) :
      {z ∈ s.offDiag | Sym2.mk.uncurry z = s(a, b)} = .cons (a, b) {(b, a)}
        (by simpa [eq_comm] using hab) := by aesop
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2
have rw : #(image (uncurry Sym2.mk) s.offDiag) = #s * (#s - 1) / 2
Tactic: rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #(image (uncurry Sym2.mk) s.offDiag) = #s * (#s - 1) / 2
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2
have rw₁ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s * 1) / 2
Tactic: rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #(image (uncurry Sym2.mk) s.offDiag) = #s * (#s - 1) / 2
rw₁ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s * 1) / 2
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2
have rw₂ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s) / 2
Tactic: rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #(image (uncurry Sym2.mk) s.offDiag) = #s * (#s - 1) / 2
rw₁ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s * 1) / 2
rw₂ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s) / 2
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2
have rw₃ : #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag / 2
Tactic: rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : #(image (uncurry Sym2.mk) s.offDiag) = #s * (#s - 1) / 2
rw₁ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s * 1) / 2
rw₂ : #(image (uncurry Sym2.mk) s.offDiag) = (#s * #s - #s) / 2
rw₃ : #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag / 2
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 2
have rw₄ : #(image (uncurry Sym2.mk) s.offDiag) = #(image (uncurry Sym2.mk) s.offDiag)
Tactic: rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
    Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } = Fintype.card α
have h : Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } =
  Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (Finset.diag univ))
Tactic: convert! card_image_diag (univ : Finset α)
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (Finset.diag univ))
have h : ∀ (x : Sym2 α),
  x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | x.IsDiag} ↔ x.IsDiag
Tactic: rw [← filter_image_mk_isDiag, Fintype.card_of_subtype]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
⊢ x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | x.IsDiag} ↔ x.IsDiag
have h : (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
Tactic: rw [mem_filter, univ_product_univ, mem_image]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
have h : ∀ (a : α × α) (ha : Quot.mk (Rel α) a = x),
  (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
Tactic: obtain ⟨a, ha⟩ := Quot.exists_rep x
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } = (Fintype.card α).choose 2
have h : Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } =
  Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (offDiag univ))
Tactic: convert! card_image_offDiag (univ : Finset α)
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (offDiag univ))
have h : ∀ (x : Sym2 α),
  x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag
Tactic: rw [← filter_image_mk_not_isDiag, Fintype.card_of_subtype]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
⊢ x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag
have h : (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
Tactic: rw [mem_filter, univ_product_univ, mem_image]
-- Lean 4 proof step from Mathlib.Data.Sym.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
have h : ∀ (a : α × α) (ha : Quot.mk (Rel α) a = x),
  (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
Tactic: obtain ⟨a, ha⟩ := Quot.exists_rep x
-- Lean 4 proof step from Mathlib.Data.Sym.Sym2.Finsupp (goal)
Goal:
α : Type u_1
M₀ : Type u_2
inst : CommMonoidWithZero M₀
inst_1 : NoZeroDivisors M₀
f : α →₀ M₀
⊢ (↑f.support.sym2 : Set (Sym2 α)) =
    Set.preimage.{u_1, u_2} (β := Sym2 M₀) (map (⇑f : (a : α) → M₀)) (Function.support mul)
have h : ∀ (x : Sym2 α) (a b : α),
  Quot.mk (Rel α) (a, b) ∈ (↑f.support.sym2 : Set (Sym2 α)) ↔
    Membership.mem (γ := Set (Sym2 α))
      (Set.preimage.{u_1, u_2} (β := Sym2 M₀) (map (⇑f : (a : α) → M₀)) (Function.support mul)) (Quot.mk (Rel α) (a, b))
Tactic: ext ⟨a, b⟩