awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
rw : map (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) x = x
rw₁ : map id x = x
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) x) = x
have rw₂ : x = x
Tactic: rw [map_map, Equiv.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) x) = x
have rw : map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) x = x
Tactic: rw [map_map, Equiv.self_comp_symm, map_id]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
rw : map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) x = x
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) x) = x
have rw₁ : map id x = x
Tactic: rw [map_map, Equiv.self_comp_symm, map_id]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym β n
rw : map (comp.{u_2 + 1, u_1 + 1, u_2 + 1} (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) x = x
rw₁ : map id x = x
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) x) = x
have rw₂ : x = x
Tactic: rw [map_map, Equiv.self_comp_symm, map_id]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
| n
have rw : (↑s : Multiset α).attach.card
Tactic: rw [← s.2, ← Multiset.card_attach]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
⊢ (↑s : Multiset α).attach.card = n
have conv_rhs : (↑s : Multiset α).attach.card = n
Tactic: conv_rhs => rw [← s.2, ← Multiset.card_attach]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
conv_rhs : (↑s : Multiset α).attach.card = n
⊢ (↑s : Multiset α).attach.card = n
have conv_rhs₁ : (↑s : Multiset α).attach.card = (↑s : Multiset α).attach.card
Tactic: conv_rhs => rw [← s.2, ← Multiset.card_attach]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
s' : Sym α n'
⊢ ((↑s : Multiset α) + (↑s' : Multiset α)).card = n + n'
have rw : (↑s : Multiset α).card + (↑s' : Multiset α).card = n + n'
Tactic: rw [Multiset.card_add, s.2, s'.2]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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'
⊢ ((↑s : Multiset α) + (↑s' : Multiset α)).card = n + n'
have rw₁ : n + (↑s' : Multiset α).card = n + n'
Tactic: rw [Multiset.card_add, s.2, s'.2]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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'
⊢ ((↑s : Multiset α) + (↑s' : Multiset α)).card = n + n'
have rw₂ : n + n' = n + n'
Tactic: rw [Multiset.card_add, s.2, s'.2]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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)
⊢ 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))
have 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 sorry)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) val property))
    ((fun (l : { x : List α // x.length = 1 }) ↦ (↑l : List α).head sorry)
      (Subtype.mk (p := fun (x : List α) ↦ x.length = 1) [a] h))
Tactic: obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h
Cleared hypotheses: val_1, h, perm
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ 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)
have 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} sorry : { 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) sorry sorry :
                  (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 sorry) sorry :
            α))
        (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: obtain ⟨a, rfl⟩ := List.length_eq_one_iff.mp h
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - (↑i : ℕ))
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
have rw : Membership.mem (γ := Sym α n)
    ((Sym.cast sorry : (a : Sym α (n - (↑i : ℕ) + (↑i : ℕ))) → Sym α n) (s.append (replicate (↑i : ℕ) b)) : Sym α n) a ↔
  (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
Tactic: rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
have rw₁ : Membership.mem (γ := Sym α (n - (↑i : ℕ) + (↑i : ℕ))) (s.append (replicate (↑i : ℕ) b)) a ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
Tactic: rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
have rw₂ : a ∈ s ∨ Membership.mem (γ := Sym α (↑i : ℕ)) (replicate (↑i : ℕ) b) a ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
Tactic: rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
have rw₃ : Membership.mem (γ := Sym α (↑i : ℕ)) (replicate (↑i : ℕ) b) a ∨ a ∈ s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
Tactic: rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ a ∈ fill b i s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
have rw₄ : (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s ↔ (↑i : ℕ) ≠ 0 ∧ a = b ∨ a ∈ s
Tactic: rw [fill, mem_cast, mem_append_iff, or_comm, mem_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
⊢ (↑m : Multiset α).card < n + 1
have rw : n < n + 1
Tactic: rw [m.2, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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
⊢ (↑m : Multiset α).card < n + 1
have rw₁ : n ≤ n
Tactic: rw [m.2, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
⊢ (filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α)).card + (↑(⟨count a (↑m : Multiset α), ⋯⟩ : Fin (n + 1)) : ℕ) =
    (↑m : Multiset α).card
have rw : (↑(⟨count a (↑m : Multiset α), sorry⟩ : Fin (n + 1)) : ℕ) + countP (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) =
  (↑m : Multiset α).card
Tactic: rw [← countP_eq_card_filter, add_comm]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
⊢ (↑(⟨count a (↑m : Multiset α), ⋯⟩ : Fin (n + 1)) : ℕ) + countP (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) =
    (↑m : Multiset α).card
have simp : (↑m : Multiset α).card =
  countP (fun (x : α) ↦ a = x) (↑m : Multiset α) + countP (fun (x : α) ↦ ¬a = x) (↑m : Multiset α)
Tactic: simp only [eq_comm, Ne, count]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
a : α
m : Sym α n
⊢ (↑m : Multiset α).card =
    countP (fun (x : α) ↦ a = x) (↑m : Multiset α) + countP (fun (x : α) ↦ ¬a = x) (↑m : Multiset α)
have rw : (↑m : Multiset α).card = (↑m : Multiset α).card
Tactic: rw [← card_eq_countP_add_countP _ _]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 α)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have 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 : ℕ) })) : ℕ)
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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
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 : ℕ) })) : ℕ)
⊢ (↑(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 : ℕ) })) : ℕ)
have rw₆ : (↑(m₂.fst (β := fun (i : Fin (n + 1)) ↦ Sym α (n - (↑i : ℕ)))) : ℕ) =
  (↑(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)]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
⊢ (↑(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 α)
have rw : filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α) =
  (↑m : Multiset α)
Tactic: rw [coe_fill, filterNe, ← val_eq_coe, Subtype.coe_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
⊢ filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α) =
    (↑m : Multiset α)
have a₁ : ∀ (b : α),
  count b (filter (fun (x : α) ↦ a ≠ x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α)) =
    count b (↑m : Multiset α)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
b : α
⊢ count b
      (filter (fun (x : α) ↦ ¬a = x) (↑m : Multiset α) + (↑(replicate (count a (↑m : Multiset α)) a) : Multiset α)) =
    count b (↑m : Multiset α)
have 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 α)
Tactic: rw [count_add, count_filter, Sym.coe_replicate, count_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
a : α
m : Sym α n
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₁ : ((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: obtain rfl | h := eq_or_ne a b
Cleared hypotheses: b