awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
x : { x : α // x ∈ s }
⊢ x ∈ s.attach

Tactic:
Multiset.mem_attach _ _

Premises used: Multiset.mem_attach, Multiset.pmap, Multiset.attach
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Sym { x : α // Membership.mem (γ := Sym α 0) nil x } 0) (attach nil) nil

Tactic:
rfl

Premises used: Sym.nil, Multiset.zero, List.pmap, Multiset.ofList, Multiset.pmap, Sym.attach, Multiset.attach, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
x : α
s : Sym α n
⊢ (x ::ₛ s).attach =
    Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ x ::ₛ s) x ⋯ ::ₛ
      map (fun (x_1 : { x : α // x ∈ s }) ↦ Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ x ::ₛ s) (↑x_1 : α) ⋯) s.attach

Tactic:
coe_injective <| Multiset.attach_cons _ _

Premises used: Multiset.attach_cons, Sym.coe_injective
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
⊢ (Sym.cast ⋯ : (a : Sym α n) → Sym α n) s = s

Tactic:
Subtype.ext rfl

Premises used: Sym, rfl, Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n n' : ℕ
s : Sym α n
n'' : ℕ
h : n = n'
h' : n' = n''
⊢ Eq (α := Sym α n'')
    ((Sym.cast h' : (a : Sym α n') → Sym α n'') ((Sym.cast h : (a : Sym α n) → Sym α n') s) : Sym α n'')
    ((Sym.cast ⋯ : (a : Sym α n) → Sym α n'') s : Sym α n'')

Tactic:
rfl

Premises used: Sym, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n m : ℕ
s : Sym α n
h : n = m
⊢ (↑((Sym.cast h : (a : Sym α n) → Sym α m) s) : Multiset α) = (↑s : Multiset α)

Tactic:
rfl

Premises used: Sym, Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n m : ℕ
s : Sym α n
a : α
h : n = m
⊢ Membership.mem (γ := Sym α m) ((Sym.cast h : (a : Sym α n) → Sym α m) s : Sym α m) a ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
rw : (↑s : Multiset α).card + (↑s' : Multiset α).card = n + n'
rw₁ : n + (↑s' : Multiset α).card = n + n'
rw₂ rw₃ : n + n' = n + n'
⊢ ((↑s : Multiset α) + (↑s' : Multiset α)).card = n + n'

Tactic:
rw [Multiset.card_add, s.2, s'.2]

Premises used: Multiset.card_add, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n n' : ℕ
s : Sym α n
t t' : Sym α n'
⊢ s.append t = s.append t' ↔ t = t'

Tactic:
Subtype.ext_iff.trans <| (add_right_inj _).trans Subtype.ext_iff.symm

Premises used: Subtype.ext_iff, Sym, Iff.trans, add_right_inj, Iff.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n n' : ℕ
s s' : Sym α n
t : Sym α n'
⊢ s.append t = s'.append t ↔ s = s'

Tactic:
Subtype.ext_iff.trans <| (add_left_inj _).trans Subtype.ext_iff.symm

Premises used: add_left_inj, Subtype.ext_iff, Sym, Iff.trans, Iff.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n' : ℕ
s s' : Sym α n'
⊢ s.append s' = (Sym.cast ⋯ : (a : Sym α (n' + n')) → Sym α (n' + n')) (s'.append s)

Tactic:
simp [append, add_comm]

Premises used: Sym.append, add_comm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n n' : ℕ
s : Sym α n
s' : Sym α n'
⊢ (↑(s.append s') : Multiset α) = (↑s : Multiset α) + (↑s' : Multiset α)

Tactic:
rfl

Premises used: Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n m : ℕ
s : Sym α n
a : α
s' : Sym α m
⊢ a ∈ s.append s' ↔ a ∈ s ∨ a ∈ s'

Tactic:
Multiset.mem_add

Premises used: Multiset.mem_add
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a_1 b a : α
⊢ Multiset.card (α := α) {a} = 1

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α 1
l l' : { x : List α // x.length = 1 }
⊢ (Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1 :
        { x : List α // x.length = 1 } → { x : List α // x.length = 1 } → Prop)
      l l' ↔
    (List.isSetoid α : List α → List α → Prop) (↑l : List α) (↑l' : List α)

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α 1
l : { x : List α // x.length = 1 }
⊢ 0 < (↑l : List α).length

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α 1
x x_1 : { x : List α // x.length = 1 }
val : List α
property : val.length = 1
val_1 : List α
h : val_1.length = 1
perm :
  HasEquiv.Equiv (α := { x : List α // x.length = 1 }) (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property)
    (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val_1 h)
obtain :
  ∀ (a : α) (h : [a].length = 1)
    (perm :
      HasEquiv.Equiv (α := { x : List α // x.length = 1 })
        (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property)
        (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h)),
    Eq.{u_1 + 1} (α := α)
      ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
        (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property))
      ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
        (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h))
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property))
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val_1 h))

Tactic:
obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h

Premises used: List.length_eq_one_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a_1 b : α
s : Sym α 1
x x_1 : { x : List α // x.length = 1 }
val : List α
property : val.length = 1
a : α
h : [a].length = 1
perm :
  HasEquiv.Equiv (α := { x : List α // x.length = 1 }) (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property)
    (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h)
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property))
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h))

Tactic:
List.eq_of_mem_singleton (List.Perm.mem_iff perm |>.mp <| List.head_mem _)

Premises used: List.head_mem, List.eq_of_mem_singleton, Iff.mp, List.Perm.mem_iff
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a_1 b : α
s : Sym α 1
x x_1 : { x : List α // x.length = 1 }
val : List α
property : val.length = 1
a : α
h : [a].length = 1
perm :
  HasEquiv.Equiv (α := { x : List α // x.length = 1 }) (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property)
    (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h)
⊢ Eq.{u_1 + 1} (α := α)
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property))
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h))

Tactic:
exact List.eq_of_mem_singleton (List.Perm.mem_iff perm |>.mp <| List.head_mem _)

Premises used: List.head_mem, List.eq_of_mem_singleton, Iff.mp, List.Perm.mem_iff
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
val : Multiset α
l : List α
h : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) = 1
mk :
  ∀ (a : α) (h : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a]) = 1),
    Eq (α := Sym α 1)
      ((fun (a : α) ↦ (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) {a} ⋯ : { s : Multiset α // s.card = 1 }))
        ((fun (s : Sym α 1) ↦
            (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1)
                ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : List α) ↦ x.length = 1)
                      (fun (x : Quotient (List.isSetoid α)) ↦ Multiset.card x = 1) ⋯ ⋯ :
                    (a : { x : Quotient (List.isSetoid α) // Multiset.card x = 1 }) →
                      Quotient (Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1))
                  s)
                (fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯) ⋯ :
              α))
          (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1)
            (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a]) h)))
      (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a])
        h)
⊢ Eq (α := Sym α 1)
    ((fun (a : α) ↦ (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) {a} ⋯ : { s : Multiset α // s.card = 1 }))
      ((fun (s : Sym α 1) ↦
          (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1)
              ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : List α) ↦ x.length = 1)
                    (fun (x : Quotient (List.isSetoid α)) ↦ Multiset.card x = 1) ⋯ ⋯ :
                  (a : { x : Quotient (List.isSetoid α) // Multiset.card x = 1 }) →
                    Quotient (Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1))
                s)
              (fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯) ⋯ :
            α))
        (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
          h)))
    (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) h)

Tactic:
obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h

Premises used: List.length_eq_one_iff, Iff.mp, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a_1 b : α
val : Multiset α
a : α
h : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a]) = 1
⊢ Eq (α := Sym α 1)
    ((fun (a : α) ↦ (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) {a} ⋯ : { s : Multiset α // s.card = 1 }))
      ((fun (s : Sym α 1) ↦
          (Quotient.liftOn (s := Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1)
              ((Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : List α) ↦ x.length = 1)
                    (fun (x : Quotient (List.isSetoid α)) ↦ Multiset.card x = 1) ⋯ ⋯ :
                  (a : { x : Quotient (List.isSetoid α) // Multiset.card x = 1 }) →
                    Quotient (Subtype.instSetoid_mathlib fun (x : List α) ↦ x.length = 1))
                s)
              (fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head ⋯) ⋯ :
            α))
        (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a])
          h)))
    (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = 1) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) [a]) h)

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
i : Fin (n + 1)
m : Sym α (n - (↑i : ℕ))
⊢ (↑(fill a i m) : Multiset α) = (↑m : Multiset α) + (↑(replicate (↑i : ℕ) a) : Multiset α)

Tactic:
rfl

Premises used: Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - (↑i : ℕ))
rw :
  Membership.mem (γ := Sym α n)
      ((Sym.cast ⋯ : (a : Sym α (n - (↑i : ℕ) + (↑i : ℕ))) → Sym α n) (s.append (replicate (↑i : ℕ) b)) : Sym α n) a ↔
    (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
rw₁ :
  Membership.mem (γ := Sym α (n - (↑i : ℕ) + (↑i : ℕ))) (s.append (replicate (↑i : ℕ) b)) a ↔
    (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
rw₂ : a ∈ s ∨ Membership.mem (γ := Sym α (↑i : ℕ)) (replicate (↑i : ℕ) b) a ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
rw₃ : Membership.mem (γ := Sym α (↑i : ℕ)) (replicate (↑i : ℕ) b) a ∨ a ∈ s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
rw₄ rw₅ : (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]

Premises used: Sym.fill, Sym.mem_replicate, Sym.mem_cast, Sym.mem_append_iff, or_comm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
rw : n < n + 1
rw₁ rw₂ : n ≤ n
⊢ (↑m : Multiset α).card < n + 1

Tactic:
rw [m.2, Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
rw :
  (↑(⟨count a (↑m : Multiset α), ⋯⟩ : Fin (n + 1)) : ℕ) + countP (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) =
    (↑m : Multiset α).card
⊢ (filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α)).card + (↑(⟨count a (↑m : Multiset α), ⋯⟩ : Fin (n + 1)) : ℕ) =
    (↑m : Multiset α).card

Tactic:
rw [← countP_eq_card_filter, add_comm]

Premises used: add_comm, Multiset.countP_eq_card_filter
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
simp :
  (↑m : Multiset α).card =
    countP (fun (x : α) ↦ a = x) (↑m : Multiset α) + countP (fun (x : α) ↦ ¬a = x) (↑m : Multiset α)
⊢ (↑(⟨count a (↑m : Multiset α), ⋯⟩ : Fin (n + 1)) : ℕ) + countP (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) =
    (↑m : Multiset α).card

Tactic:
simp only [eq_comm, Ne, count]

Premises used: Multiset.count, Ne, eq_comm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
rw rw₁ : (↑m : Multiset α).card = (↑m : Multiset α).card
⊢ (↑m : Multiset α).card =
    countP (fun (x : α) ↦ a = x) (↑m : Multiset α) + countP (fun (x : α) ↦ ¬a = x) (↑m : Multiset α)

Tactic:
rw [← card_eq_countP_add_countP _ _]

Premises used: Multiset.card_eq_countP_add_countP
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
m₁ m₂ : (i : Fin (n + 1)) × Sym α (n - (↑i : ℕ))
h :
  (↑(m₁.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α) =
    (↑(m₂.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α)
rw :
  n - (n - (↑(m₁.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)) =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₁ :
  n - (↑(m₁.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α).card =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₂ :
  n - (↑(m₁.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α).card =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₃ :
  n - (↑(m₂.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α).card =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₄ :
  n - (↑(m₂.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α).card =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₅ :
  n - (n - (↑(m₂.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ)) =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
rw₆ rw₇ :
  (↑(m₂.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)
⊢ (↑(m₁.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ) =
    (↑(m₂.fst (β := fun (a : Fin (n + 1)) ↦ { s : Multiset α // s.card = n - (↑a : ℕ) })) : ℕ)

Tactic:
rw [← Nat.sub_sub_self (Nat.le_of_lt_succ m₁.1.is_lt), ← m₁.2.2, val_eq_coe, h,
        ← val_eq_coe, m₂.2.2, Nat.sub_sub_self (Nat.le_of_lt_succ m₂.1.is_lt)]

Premises used: Sym.val_eq_coe, Nat.sub_sub_self, Fin.is_lt, Sigma.fst, Nat.le_of_lt_succ, Sigma.snd, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
rw :
  filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α) =
    (↑m : Multiset α)
⊢ (↑(fill a ((filterNe a m).fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))
          ((filterNe a m).snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ))))) :
      Multiset α) =
    (↑m : Multiset α)

Tactic:
rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]

Premises used: Subtype.coe_mk, Sym.val_eq_coe, Fin.val_mk, Sym.coe_fill, Sym.filterNe
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
a₁ :
  ∀ (b : α),
    count b
        (filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α)) =
      count b (↑m : Multiset α)
⊢ filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α) =
    (↑m : Multiset α)

Tactic:
ext b
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
a₁ :
  ((if ¬a = b then count b (↑m : Multiset α) else 0) + if a = b then count a (↑m : Multiset α) else 0) =
    count b (↑m : Multiset α)
⊢ count b
      (filter (fun (x : α) ↦ ¬a = x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α)) =
    count b (↑m : Multiset α)

Tactic:
rw [count_add, count_filter, Sym.coe_replicate, count_replicate]

Premises used: Multiset.count_replicate, Multiset.count_add, Multiset.count_filter, Sym.coe_replicate
-- Module: Mathlib.Data.Sym.Basic
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 α)
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 α)
⊢ ((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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Sym.Basic
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 α)
a₃ a₄ : 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 α)

Tactic:
rw [if_pos rfl, if_neg (not_not.2 rfl), zero_add]

Premises used: Iff.mpr, Classical.not_not, if_pos, zero_add, if_neg, rfl
-- Module: Mathlib.Data.Sym.Basic
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 α)
a₃ a₄ : count b (↑m : Multiset α) = 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 α)

Tactic:
rw [if_pos h, if_neg h, add_zero]

Premises used: if_pos, add_zero, if_neg
-- Module: Mathlib.Data.Sym.Basic
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 :
  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 α)
⊢ (↑((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 α)

Tactic:
rw [filterNe, ← val_eq_coe, Subtype.coe_mk, val_eq_coe, coe_fill]

Premises used: Subtype.coe_mk, Sym.val_eq_coe, Sym.coe_fill, Sym.filterNe
-- Module: Mathlib.Data.Sym.Basic
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 α)
rw₁ : ∀ a_1 ∈ (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α), a ≠ a_1
⊢ 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 [filter_add, filter_eq_self.2, add_eq_left, eq_zero_iff_forall_notMem]

Premises used: Iff.mpr, Multiset.filter_eq_self, Multiset.eq_zero_iff_forall_notMem, add_eq_left, Multiset.filter_add
-- Module: Mathlib.Data.Sym.Basic
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 α)
⊢ ((↑(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

Premises used: Sym.mem_replicate, Multiset.mem_filter, Sym.mem_coe
-- Module: Mathlib.Data.Sym.Basic
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 : ((↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False

Tactic:
hb.2 hb.1.2.symm

Premises used: And.right, And.left, Eq.symm
-- Module: Mathlib.Data.Sym.Basic
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 : ((↑(m.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) ≠ 0 ∧ b = a) ∧ a ≠ b
⊢ False

Tactic:
exact hb.2 hb.1.2.symm

Premises used: And.right, And.left, Eq.symm
-- Module: Mathlib.Data.Sym.Basic
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 : ℕ)))
⊢ ∀ a_1 ∈ (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α), a ≠ a_1

Tactic:
fun a ha ha' => h <| ha'.symm ▸ ha

Premises used: Eq.rec, Eq.symm, Not
-- Module: Mathlib.Data.Sym.Basic
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 : ℕ)))
⊢ ∀ a_1 ∈ (↑(m.snd (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : Multiset α), a ≠ a_1

Tactic:
exact fun a ha ha' => h <| ha'.symm ▸ ha
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
i : Fin (n + 1)
s : Sym α (n - (↑i : ℕ))
hx : a ∉ s
⊢ count a (↑(fill a i s) : Multiset α) = (↑i : ℕ)

Tactic:
simp [coe_fill, coe_replicate, hx]

Premises used: Sym.coe_fill, Sym.coe_replicate
-- 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
this : x ∉ Multiset.replicate (↑i : ℕ) a
⊢ count x (↑(fill a i s) : Multiset α) = count x (↑s : Multiset α)

Tactic:
simp [coe_fill, coe_replicate, this]

Premises used: Sym.coe_fill, Sym.coe_replicate
-- 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
suffices : x ∉ Multiset.replicate (↑i : ℕ) a
⊢ count x (↑(fill a i s) : Multiset α) = count x (↑s : Multiset α)

Tactic:
suffices x ∉ Multiset.replicate i a by simp [coe_fill, coe_replicate, this]