awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - (↑i : ℕ))
hx : x ≠ a
⊢ x ∉ Multiset.replicate (↑i : ℕ) a

Tactic:
simp [Multiset.mem_replicate, hx]

Premises used: Multiset.mem_replicate
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ encode s = Sum.inl (s.erase none h)

Tactic:
dif_pos h

Premises used: dif_pos, SymOptionSuccEquiv.encode
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ encode s = Sum.inr (map (fun (o : { x : Option α // x ∈ s }) ↦ (↑o : Option α).get ⋯) s.attach)

Tactic:
dif_neg h

Premises used: dif_neg, SymOptionSuccEquiv.encode
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym (Option α) n
⊢ decode (Sum.inl s) = none ::ₛ s

Tactic:
rfl

Premises used: SymOptionSuccEquiv.decode, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ decode (Sum.inr s) = map (⇑Embedding.some : (a : α) → Option α) s

Tactic:
rfl

Premises used: SymOptionSuccEquiv.decode, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
pos : ∀ (h : none ∈ s), decode (encode s) = s
neg : ∀ (h : none ∉ s), decode (encode s) = s
⊢ decode (encode s) = s

Tactic:
by_cases h : none ∈ s

Premises used: Option.none
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∈ s
⊢ decode (encode s) = s

Tactic:
simp [h]
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
neg : map (fun (x : { x : Option α // x ∈ s }) ↦ (↑x : Option α)) s.attach = s
⊢ decode (encode s) = s

Tactic:
simp only [decode, h, not_false_iff, encode_of_none_notMem, Embedding.some_apply, map_map,
      comp_apply, Option.some_get]

Premises used: SymOptionSuccEquiv.encode_of_none_notMem, SymOptionSuccEquiv.decode, Option.some_get, Function.comp_apply, Sym.map_map, Function.Embedding.some_apply, not_false_iff
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ map (Subtype.val (p := fun (x : Option α) ↦ x ∈ s)) s.attach = s

Tactic:
s.attach_map_coe

Premises used: Sym.attach_map_coe
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n.succ
h : none ∉ s
⊢ map (fun (x : { x : Option α // x ∈ s }) ↦ (↑x : Option α)) s.attach = s

Tactic:
convert! s.attach_map_coe

Premises used: Sym.attach_map_coe
-- Module: Mathlib.Data.Sym.Basic
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
inr : ∀ (s : Sym α n.succ), encode (decode (Sum.inr s)) = Sum.inr s
⊢ encode (decode s) = s

Tactic:
obtain s | s := s
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym (Option α) n
⊢ encode (decode (Sum.inl s)) = Sum.inl s

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
pos : ∀ (h : none ∈ decode (Sum.inr s)), False
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 ⋯)
          (decode (Sum.inr s)).attach))
      (Sum.inr s)
⊢ 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)

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
pos :
  ∀ a ∈ (↑s : Multiset α),
    ∀ (ha : Eq (α := Option α) ((Embedding.some : (a : α) → Option α) a : Option α) (none : Option α)), False
⊢ False

Tactic:
obtain ⟨a, _, ha⟩ := Multiset.mem_map.mp h

Premises used: Multiset.mem_map, Iff.mp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
a : α
left : a ∈ (↑s : Multiset α)
ha : Eq (α := Option α) ((Embedding.some : (a : α) → Option α) a : Option α) (none : Option α)
⊢ False

Tactic:
Option.some_ne_none _ ha

Premises used: Option.some_ne_none
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∈ decode (Sum.inr s)
a : α
left : a ∈ (↑s : Multiset α)
ha : Eq (α := Option α) ((Embedding.some : (a : α) → Option α) a : Option α) (none : Option α)
⊢ False

Tactic:
exact Option.some_ne_none _ ha

Premises used: Option.some_ne_none
-- Module: Mathlib.Data.Sym.Basic
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)

Tactic:
congr_arg Sum.inr ?_

Premises used: congr_arg, Sum.inr
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
neg : map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach = 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)

Tactic:
refine congr_arg Sum.inr ?_

Premises used: congr_arg, Sum.inr
-- Module: Mathlib.Data.Sym.Basic
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

Tactic:
map_injective (Option.some_injective _) _ ?_

Premises used: Sym.map_injective, Option.some_injective
-- Module: Mathlib.Data.Sym.Basic
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 some s
⊢ map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach = s

Tactic:
refine map_injective (Option.some_injective _) _ ?_

Premises used: Sym.map_injective, Option.some_injective
-- Module: Mathlib.Data.Sym.Basic
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

Tactic:
Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_)

Premises used: SymOptionSuccEquiv.decode, Sym.attach_map_coe, Sum.inr, Eq.trans
-- Module: Mathlib.Data.Sym.Basic
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
neg₁ : decode (Sum.inr s) = map some s
⊢ map some
      (map (fun (o : { x : Option α // x ∈ decode (Sum.inr s) }) ↦ (↑o : Option α).get ⋯) (decode (Sum.inr s)).attach) =
    map some s

Tactic:
refine Eq.trans ?_ (.trans (SymOptionSuccEquiv.decode (Sum.inr s)).attach_map_coe ?_)

Premises used: SymOptionSuccEquiv.decode, Sym.attach_map_coe, Sum.inr, Eq.trans
-- Module: Mathlib.Data.Sym.Basic
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 (Subtype.val (p := fun (x : Option α) ↦ x ∈ decode (Sum.inr s))) (decode (Sum.inr s)).attach

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ decode (Sum.inr s) = map some s

Tactic:
simp
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }
⊢ (fun (s : Sym (Fin n.succ) k) ↦
        (Subtype.mk (p := fun (s : Sym (Fin (n + 1)) (k + 1)) ↦ 0 ∈ s) (0 ::ₛ s) ⋯ :
          { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }))
      ((fun (s : { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }) ↦ (↑s : Sym (Fin (n + 1)) (k + 1)).erase 0 ⋯) s) =
    s

Tactic:
simp
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : Sym (Fin n.succ) k
⊢ (fun (s : { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }) ↦ (↑s : Sym (Fin (n + 1)) (k + 1)).erase 0 ⋯)
      ((fun (s : Sym (Fin n.succ) k) ↦
          (Subtype.mk (p := fun (s : Sym (Fin (n + 1)) (k + 1)) ↦ 0 ∈ s) (0 ::ₛ s) ⋯ :
            { s : Sym (Fin (n + 1)) (k + 1) // 0 ∈ s }))
        s) =
    s

Tactic:
simp
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
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) ⋯ :
              { 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)
⊢ (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

Tactic:
ext1
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
a : map (Fin.succAbove 0 ∘ Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k) = (↑s : Sym (Fin n.succ.succ) k)
⊢ (↑((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)

Tactic:
simp only [map_map]

Premises used: Sym.map_map
-- Module: Mathlib.Data.Sym.Card
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)

Tactic:
(Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)

Premises used: Sym.map_id', Sym.map_congr, Eq.trans
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
a : ∀ (v : Fin (n.succ + 1)) (hv : v ∈ (↑s : Sym (Fin n.succ.succ) k)), (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v
⊢ map (Fin.succAbove 0 ∘ Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k) = (↑s : Sym (Fin n.succ.succ) k)

Tactic:
refine (Sym.map_congr fun v hv ↦ ?_).trans (map_id' _)

Premises used: Sym.map_id', Sym.map_congr, Eq.trans
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
v : Fin (n.succ + 1)
hv : v ∈ (↑s : Sym (Fin n.succ.succ) k)
⊢ (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v

Tactic:
Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)

Premises used: Fin.succAbove, Fin.succ, Fin.succAbove_predAbove, ne_of_mem_of_not_mem, Subtype.property, ite
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }
v : Fin (n.succ + 1)
hv : v ∈ (↑s : Sym (Fin n.succ.succ) k)
⊢ (Fin.succAbove 0 ∘ Fin.predAbove 0) v = v

Tactic:
exact Fin.succAbove_predAbove (ne_of_mem_of_not_mem hv s.2)
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
n_1 n k : ℕ
s : Sym (Fin n.succ) k
⊢ (fun (s : { s : Sym (Fin n.succ.succ) k // 0 ∉ s }) ↦ map (Fin.predAbove 0) (↑s : Sym (Fin n.succ.succ) k))
      ((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 }))
        s) =
    s

Tactic:
simp only [map_map, comp_apply, ← Fin.castSucc_zero, Fin.predAbove_succAbove, map_id']

Premises used: Fin.predAbove_succAbove, Sym.map_id', Fin.castSucc_zero, Function.comp_apply, Sym.map_map
-- Module: Mathlib.Data.Sym.Card
Goal:
n : ℕ
⊢ Fintype.card (Sym (Fin n) 0) = n.multichoose 0

Tactic:
simp
-- Module: Mathlib.Data.Sym.Card
Goal:
k : ℕ
rw : Fintype.card (Sym (Fin 0) (k + 1)) = 0
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = multichoose 0 (k + 1)

Tactic:
rw [multichoose_zero_succ]

Premises used: Nat.multichoose_zero_succ
-- Module: Mathlib.Data.Sym.Card
Goal:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0

Tactic:
card_eq_zero

Premises used: Fintype.card_eq_zero
-- Module: Mathlib.Data.Sym.Card
Goal:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 0

Tactic:
exact card_eq_zero

Premises used: Finset.card_eq_zero
-- Module: Mathlib.Data.Sym.Card
Goal:
k : ℕ
⊢ Fintype.card (Sym (Fin 1) (k + 1)) = multichoose 1 (k + 1)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Card
Goal:
n k : ℕ
rw : Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (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]

Premises used: Fintype.card, add_comm, Nat.multichoose_succ_succ, HAdd.hAdd, OfNat.ofNat, Fintype.card_sum
-- Module: Mathlib.Data.Sym.Card
Goal:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))

Tactic:
Fintype.card_congr (Equiv.symm ?_)

Premises used: Fintype.card_congr, Equiv.symm
-- Module: Mathlib.Data.Sym.Card
Goal:
n k : ℕ
refine : Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = Fintype.card (Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1))

Tactic:
refine Fintype.card_congr (Equiv.symm ?_)

Premises used: Fintype.card_congr, Equiv.symm
-- Module: Mathlib.Data.Sym.Card
Goal:
n k : ℕ
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)
⊢ Sym (Fin (n + 2)) k ⊕ Sym (Fin (n + 1)) (k + 1) ≃ Sym (Fin (n + 2)) (k + 1)

Tactic:
apply (Sym.e1.symm.sumCongr Sym.e2.symm).trans

Premises used: Equiv.trans, Sym.e2, Equiv.sumCongr, Sym.e1, Equiv.symm
-- Module: Mathlib.Data.Sym.Card
Goal:
n k : ℕ
⊢ { 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 Equiv.sumCompl

Premises used: Equiv.sumCompl
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_2
k : ℕ
inst : Fintype α
inst_1 : Fintype (Sym α k)
rw : Fintype.card.{u_2} (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
⊢ Fintype.card.{u_2} (Sym α k) = (Fintype.card α).multichoose k

Tactic:
rw [← card_sym_fin_eq_multichoose]

Premises used: Sym.card_sym_fin_eq_multichoose
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_2
k : ℕ
inst : Fintype α
inst_1 : Fintype (Sym α k)
⊢ Fintype.card.{u_2} (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)

Tactic:
card_congr (equivCongr (equivFin α))

Premises used: Fintype.card_congr, Fintype.equivFin, Sym.equivCongr
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_2
k : ℕ
inst : Fintype α
inst_1 : Fintype (Sym α k)
⊢ Fintype.card.{u_2} (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)

Tactic:
exact card_congr (equivCongr (equivFin α))

Premises used: Fintype.card_congr, Fintype.equivFin, Sym.equivCongr
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_2
inst : Fintype α
k : ℕ
inst_1 : Fintype (Sym α k)
rw : (Fintype.card α).multichoose k = (Fintype.card α + k - 1).choose k
rw₁ rw₂ : (Fintype.card α + k - 1).choose k = (Fintype.card α + k - 1).choose k
⊢ Fintype.card.{u_2} (Sym α k) = (Fintype.card α + k - 1).choose k

Tactic:
rw [card_sym_eq_multichoose, Nat.multichoose_eq]

Premises used: Nat.multichoose_eq, Sym.card_sym_eq_multichoose
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ #(image (uncurry Sym2.mk) s.diag) = #s

Tactic:
simp [card_image_of_injOn]

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
rw : ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2
⊢ 2 * #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag

Tactic:
rw [card_eq_sum_card_image (Sym2.mk.uncurry : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]

Premises used: Sym2.mk, Finset.sum_const_nat, Finset.card_eq_sum_card_image, Sym2.ind, mul_comm, Function.uncurry
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
a b : α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b ∨ b ≠ a
⊢ (a, b) ∉ {(b, a)}

Tactic:
simpa [eq_comm] using hab

Premises used: eq_comm
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
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)} ⋯

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
⊢ ∀ (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)} ⋯

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
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
s : Finset α
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)} ⋯
⊢ ∀ (x y : α), s(x, y) ∈ image (uncurry Sym2.mk) s.offDiag → #({a ∈ s.offDiag | uncurry Sym2.mk a = s(x, y)}) = 2

Tactic:
aesop
-- Module: Mathlib.Data.Sym.Card
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
rw₄ rw₅ : #(image (uncurry Sym2.mk) s.offDiag) = #(image (uncurry Sym2.mk) s.offDiag)
⊢ #(image (uncurry Sym2.mk) s.offDiag) = (#s).choose 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]

Premises used: Nat.mul_sub_left_distrib, Nat.choose_two_right, Finset.offDiag_card, Nat.div_eq_of_eq_mul_right, Nat.zero_lt_two, mul_one, Sym2.two_mul_card_image_offDiag, Eq.symm
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (Finset.diag univ)) = Finset.card.{u_1} (α := α) univ

Tactic:
card_image_diag (univ : Finset α)

Premises used: Finset.univ, Sym2.card_image_diag
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h :
  Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (Finset.diag univ))
⊢ Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } = Fintype.card α

Tactic:
convert! card_image_diag (univ : Finset α)

Premises used: Finset.univ, Sym2.card_image_diag
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h :
  ∀ (x : Sym2 α),
    x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | x.IsDiag} ↔ x.IsDiag
⊢ Fintype.card.{u_1} { a : Sym2 α // a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (Finset.diag univ))

Tactic:
rw [← filter_image_mk_isDiag, Fintype.card_of_subtype]

Premises used: Sym2.filter_image_mk_isDiag, Fintype.card_of_subtype
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
h : (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
⊢ x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | x.IsDiag} ↔ x.IsDiag

Tactic:
rw [mem_filter, univ_product_univ, mem_image]

Premises used: Finset.mem_image, Finset.univ_product_univ, Finset.mem_filter
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
h :
  ∀ (a : α × α) (ha : Quot.mk (Rel α) a = x),
    (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Tactic:
obtain ⟨a, ha⟩ := Quot.exists_rep x

Premises used: Quot.exists_rep
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Tactic:
and_iff_right ⟨a, mem_univ _, ha⟩

Premises used: Finset.mem_univ, and_iff_right, And.intro, Exists.intro
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
a : α × α
ha : Quot.mk (Rel α) a = x
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag

Tactic:
exact and_iff_right ⟨a, mem_univ _, ha⟩

Premises used: and_iff_right
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (offDiag univ)) = (Finset.card.{u_1} (α := α) univ).choose 2

Tactic:
card_image_offDiag (univ : Finset α)

Premises used: Finset.univ, Sym2.card_image_offDiag
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h :
  Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (offDiag univ))
⊢ Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } = (Fintype.card α).choose 2

Tactic:
convert! card_image_offDiag (univ : Finset α)

Premises used: Finset.univ, Sym2.card_image_offDiag
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
h :
  ∀ (x : Sym2 α),
    x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag
⊢ Fintype.card.{u_1} { a : Sym2 α // ¬a.IsDiag } =
    Finset.card.{u_1} (α := Sym2 α) (image (uncurry Sym2.mk) (offDiag univ))

Tactic:
rw [← filter_image_mk_not_isDiag, Fintype.card_of_subtype]

Premises used: Sym2.filter_image_mk_not_isDiag, Fintype.card_of_subtype
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
h : (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
⊢ x ∈ {x ∈ image (uncurry Sym2.mk) (SProd.sprod (α := Finset α) (β := Finset α) univ univ) | ¬x.IsDiag} ↔ ¬x.IsDiag

Tactic:
rw [mem_filter, univ_product_univ, mem_image]

Premises used: Finset.mem_image, Finset.univ_product_univ, Finset.mem_filter
-- Module: Mathlib.Data.Sym.Card
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : Sym2 α
h :
  ∀ (a : α × α) (ha : Quot.mk (Rel α) a = x),
    (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag
⊢ (∃ (a : α × α), Membership.mem (γ := Finset (α × α)) univ a ∧ uncurry Sym2.mk a = x) ∧ ¬x.IsDiag ↔ ¬x.IsDiag

Tactic:
obtain ⟨a, ha⟩ := Quot.exists_rep x

Premises used: Quot.exists_rep