awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
a : α
⊢ (OrderIso.symm orderIsoSumLexPUnit : (a : _root_.Lex (α ⊕ PUnit)) → WithTop α)
      ((toLex : (a : α ⊕ PUnit) → _root_.Lex (α ⊕ PUnit)) (inl a)) =
    (↑a : WithTop α)

Tactic:
rfl

Premises used: WithTop.some, rfl, Sum.elim
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
⊢ Injective.{u_1 + 1, u_1 + 1} (α := Sym α n) toMultiset

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective, Sym, Sym.toMultiset
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s₁ s₂ : Sym α n
⊢ (↑s₁ : Multiset α) = (↑s₂ : Multiset α) ↔ s₁ = s₂

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, Sym.coe_injective
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s₁ s₂ : Sym α n
h : (↑s₁ : Multiset α) = (↑s₂ : Multiset α)
⊢ s₁ = s₂

Tactic:
coe_injective h

Premises used: Sym.coe_injective
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
⊢ (↑s : Multiset α) = (↑s : Multiset α)

Tactic:
rfl

Premises used: Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (↑nil : Multiset α) 0

Tactic:
rfl

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

Tactic:
rw [Multiset.card_cons, s.2]

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

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

Premises used: Subtype.ext_iff, Sym, Iff.trans, Multiset.cons_inj_right, Iff.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a a' : α
s : Sym α n
⊢ a ::ₛ s = a' ::ₛ s ↔ a = a'

Tactic:
Subtype.ext_iff.trans <| Multiset.cons_inj_left _

Premises used: Subtype.ext_iff, Sym, Iff.trans, Multiset.cons_inj_left
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
s : Sym α n
⊢ a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s

Tactic:
Subtype.ext <| Multiset.cons_swap a b s.1

Premises used: Multiset.cons_swap, Sym, Subtype.val, Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ (↑(a ::ₛ s) : Multiset α) = a ::ₘ (↑s : Multiset α)

Tactic:
rfl

Premises used: Multiset.cons, Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Sym α 0) (ofVector Vector.nil) nil

Tactic:
rfl

Premises used: Sym.nil, Multiset.zero, Multiset.ofList, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    Eq (α := Sym α n.succ) (ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
      (a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v

Tactic:
cases v
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
⊢ Eq (α := Sym α n.succ) (ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
    (a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
⊢ (↑s : Multiset α).card = n

Tactic:
s.prop

Premises used: Subtype.prop, Sym.toMultiset
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Multiset α
h : s.card = n
⊢ (↑(mk s h) : Multiset α) = s

Tactic:
rfl

Premises used: Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
s : Multiset α
h : s.card = n
⊢ a ∈ mk s h ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

Premises used: Sym
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
p : Sym α n → Prop
⊢ (∃ (s : Sym α n), p s) ↔ ∃ (s : Multiset α) (hs : s.card = n), p (mk s hs)

Tactic:
simp [Sym]

Premises used: Sym
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
a : α
⊢ a ∉ nil

Tactic:
Multiset.notMem_zero a

Premises used: Multiset.notMem_zero
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a b : α
⊢ a ∈ b ::ₛ s ↔ a = b ∨ a ∈ s

Tactic:
Multiset.mem_cons

Premises used: Multiset.cons, Multiset.mem_cons
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ a ∈ (↑s : Multiset α) ↔ a ∈ s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Sym.toMultiset
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a b : α
h : a ∈ s
⊢ a ∈ b ::ₛ s

Tactic:
Multiset.mem_cons_of_mem h

Premises used: Multiset.mem_cons_of_mem, Multiset.cons
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
s : Sym α n
⊢ a ∈ a ::ₛ s

Tactic:
Multiset.mem_cons_self a s.1

Premises used: Multiset.cons, Multiset.mem_cons_self, Subtype.val
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
mk :
  ∀ (val : List α) (property : val.length = n),
    (↑(a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α) =
      (↑(ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α)
⊢ (↑(a ::ₛ ofVector v) : Multiset α) = (↑(ofVector (a ::ᵥ v)) : Multiset α)

Tactic:
cases v
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
val : List α
property : val.length = n
⊢ (↑(a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α) =
    (↑(ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α)

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a b : List.Vector α n
h : (↑a : List α) ~ (↑b : List α)
⊢ ofVector a = ofVector b

Tactic:
Subtype.ext <| Quotient.sound h

Premises used: Sym, Quotient.sound, Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
rw : m.card.pred = n
rw₁ : (n + 1).pred = n
rw₂ : n.succ.pred = n
rw₃ rw₄ : n = n
⊢ (m.erase a).card = n

Tactic:
rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]

Premises used: Multiset.card_erase_of_mem, Nat.pred_succ, Nat.add_one
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (mk m hc).erase a h = mk (m.erase a) ⋯

Tactic:
rfl

Premises used: Sym.erase, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
a : α
h : a ∈ s
⊢ (↑(s.erase a h) : Multiset α) = (↑s : Multiset α).erase a

Tactic:
rfl

Premises used: Multiset.erase, Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n.succ
a : α
h : a ∈ s
⊢ a ::ₛ s.erase a h = s

Tactic:
coe_injective <| Multiset.cons_erase h

Premises used: Multiset.cons_erase, Sym.coe_injective
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
inst : DecidableEq α
s : Sym α n
a : α
h : a ∈ a ::ₛ s
⊢ (a ::ₛ s).erase a h = s

Tactic:
coe_injective <| Multiset.erase_cons_head a s.1

Premises used: Multiset.erase_cons_head, Sym.coe_injective, Subtype.val
-- Module: Mathlib.Data.Sym.Basic
Goal:
α_1 : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α_1 n_1
a b : α_1
α : Type u_3
n : ℕ
x : List α
⊢ x.length = n ↔ Multiset.card ⟦x⟧ = n

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α_1 : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α_1 n_1
a b : α_1
α : Type u_3
n : ℕ
x x_1 : { l : List α // l.length = n }
⊢ (Vector.Perm.isSetoid α n : { l : List α // l.length = n } → { l : List α // l.length = n } → Prop) x x_1 ↔
    (List.isSetoid α : List α → List α → Prop) (↑x : List α) (↑x_1 : List α)

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
a : α
s : Sym α n
mk :
  ∀ (val : Multiset α) (l : List α)
    (property : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) = n),
    Eq (α := Sym' α n.succ)
      (a ::
        (symEquivSym' : (a : Sym α n) → Sym' α n)
          (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
            property))
      ((symEquivSym' : (a : Sym α n.succ) → Sym' α n.succ)
        (a ::ₛ
          Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
            property))
⊢ Eq (α := Sym' α n.succ) (a :: (symEquivSym' : (a : Sym α n) → Sym' α n) s)
    ((symEquivSym' : (a : Sym α n.succ) → Sym' α n.succ) (a ::ₛ s))

Tactic:
rcases s with ⟨⟨l⟩, _⟩
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
a : α
val : Multiset α
l : List α
property : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) = n
⊢ Eq (α := Sym' α n.succ)
    (a ::
      (symEquivSym' : (a : Sym α n) → Sym' α n)
        (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
          property))
    ((symEquivSym' : (a : Sym α n.succ) → Sym' α n.succ)
      (a ::ₛ
        Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
          property))

Tactic:
rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Multiset α) (↑0 : Multiset α) 0

Tactic:
rfl

Premises used: Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
s : Sym α 0
⊢ s = nil

Tactic:
Subtype.ext <| Multiset.card_eq_zero.1 s.2

Premises used: Multiset.card_eq_zero, Sym, Iff.mp, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
a : α
n : ℕ
⊢ replicate n.succ a = a ::ₛ replicate n a

Tactic:
rfl

Premises used: List.replicate, Sym.cons, Sym.replicate, Multiset.cons, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
⊢ (↑(replicate n a) : Multiset α) = Multiset.replicate n a

Tactic:
rfl

Premises used: Multiset.ofList, Sym.toMultiset, Multiset.replicate, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a : α
rw : (↑(replicate n a) : Multiset α) = Multiset.replicate n a
rw₁ rw₂ : Multiset.replicate n a = Multiset.replicate n a
⊢ (↑(replicate n a) : Multiset α) = Multiset.replicate n a

Tactic:
rw [val_eq_coe, coe_replicate]

Premises used: Sym.val_eq_coe, Sym.coe_replicate
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
a b : α
⊢ b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

Tactic:
Multiset.mem_replicate

Premises used: Multiset.mem_replicate, Multiset.ofList, Multiset.replicate
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
rw : ((↑s : Multiset α).card = n ∧ ∀ b ∈ (↑s : Multiset α), b = a) ↔ ∀ b ∈ s, b = a
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
rw [Subtype.ext_iff, val_replicate, Multiset.eq_replicate]

Premises used: Subtype.ext_iff, Multiset.eq_replicate, Sym.val_replicate
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s : Multiset α).card = n ∧ ∀ b ∈ (↑s : Multiset α), b = a) ↔ ∀ b ∈ s, b = a

Tactic:
and_iff_right s.2

Premises used: and_iff_right, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ((↑s : Multiset α).card = n ∧ ∀ b ∈ (↑s : Multiset α), b = a) ↔ ∀ b ∈ s, b = a

Tactic:
exact and_iff_right s.2

Premises used: and_iff_right, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ (a : α), a ∈ s

Tactic:
Multiset.card_pos_iff_exists_mem.1 <| s.2.symm ▸ n.succ_pos

Premises used: Eq.rec, Nat.succ_pos, Iff.mp, Multiset.card_pos_iff_exists_mem, Eq.symm, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h : a ∈ s
obtain : ∀ (m : Multiset α) (h : (↑s : Multiset α) = a ::ₘ m), ∃ (t : Sym α n), s = a ::ₛ t
⊢ ∃ (t : Sym α n), s = a ::ₛ t

Tactic:
obtain ⟨m, h⟩ := Multiset.exists_cons_of_mem h

Premises used: Multiset.exists_cons_of_mem
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
⊢ (↑s : Multiset α).card = (a ::ₘ m).card

Tactic:
apply_fun Multiset.card at h

Premises used: Multiset.card
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α).card = (a ::ₘ m).card
⊢ n = m.card

Tactic:
rw [s.2, Multiset.card_cons, add_left_inj] at h

Premises used: add_left_inj, Multiset.card_cons, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : n = m.card
⊢ m.card = n

Tactic:
h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : n = m.card
⊢ m.card = n

Tactic:
exact h.symm

Premises used: Eq.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
⊢ m.card = n

Tactic:
have : Multiset.card m = n := by
    apply_fun Multiset.card at h
    rw [s.2, Multiset.card_cons, add_left_inj] at h
    exact h.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
h₁ : s = a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this
⊢ ∃ (t : Sym α n), s = a ::ₛ t

Tactic:
use ⟨m, this⟩
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
h₁ : (↑s : Multiset α) = (↑(a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this) : Multiset α)
⊢ s = a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
⊢ (↑s : Multiset α) = (↑(a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this) : Multiset α)

Tactic:
h

Premises used: Multiset.cons
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
⊢ (↑s : Multiset α) = (↑(a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this) : Multiset α)

Tactic:
exact h
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
obtain : ∀ (a : α) (ha : a ∈ s), ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'
⊢ ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'

Tactic:
obtain ⟨a, ha⟩ := exists_mem s

Premises used: Sym.exists_mem
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'

Tactic:
⟨a, s.erase a ha, (cons_erase ha).symm⟩

Premises used: Sym.erase, Sym.cons_erase, Exists.intro, Eq.symm
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'

Tactic:
exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
a : α
ha : a ∈ s
⊢ ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'

Tactic:
classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
a : α
n : ℕ
s : Sym α n
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
Subtype.ext_iff.trans <| Multiset.eq_replicate.trans <| and_iff_right s.prop

Premises used: and_iff_right, Subtype.ext_iff, Multiset.eq_replicate, Subtype.prop, Sym, Iff.trans
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
inst : Subsingleton α
a : α
n : ℕ
s : Sym α n
⊢ s = replicate n a

Tactic:
eq_replicate.2 fun _ _ => Subsingleton.elim _ _

Premises used: Iff.mpr, Subsingleton.elim, Sym.eq_replicate
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α n_1
a b : α
inst : Subsingleton α
n : ℕ
zero : ∀ (a b : Sym α 0), a = b
succ : ∀ (n : ℕ) (a b : Sym α (n + 1)), a = b
⊢ ∀ (a b : Sym α n), a = b

Tactic:
cases n
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
inst : Subsingleton α
⊢ ∀ (a b : Sym α 0), a = b

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
inst : Subsingleton α
n_1 : ℕ
s s' : Sym α (n_1 + 1)
succ : ∀ (b : α), s = s'
⊢ s = s'

Tactic:
obtain ⟨b, -⟩ := exists_mem s

Premises used: Sym.exists_mem
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b_1 : α
inst : Subsingleton α
n_1 : ℕ
s s' : Sym α (n_1 + 1)
b : α
succ : s = replicate (n_1 + 1) b
succ₁ succ₂ : Eq (α := Sym α (n_1 + 1)) (replicate (n_1 + 1) b) (replicate (n_1 + 1) b)
⊢ s = s'

Tactic:
rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]

Premises used: Sym.eq_replicate_of_subsingleton
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s_1 : Sym α n_1
a b : α
n : ℕ
inst : IsEmpty α
s : Sym α n.succ
obtain : ∀ (a : α), False
⊢ False

Tactic:
obtain ⟨a, -⟩ := exists_mem s

Premises used: Sym.exists_mem
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s_1 : Sym α n_1
a_1 b : α
n : ℕ
inst : IsEmpty α
s : Sym α n.succ
a : α
⊢ False

Tactic:
isEmptyElim a

Premises used: isEmptyElim
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s_1 : Sym α n_1
a_1 b : α
n : ℕ
inst : IsEmpty α
s : Sym α n.succ
a : α
⊢ False

Tactic:
exact isEmptyElim a
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
a b : α
n : ℕ
h : n ≠ 0
⊢ replicate n a = replicate n b ↔ a = b

Tactic:
Subtype.ext_iff.trans (Multiset.replicate_right_inj h)

Premises used: Multiset.replicate_right_inj, Subtype.ext_iff, Sym, Iff.trans
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
h : n ≠ 0
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (replicate n)

Tactic:
fun _ _ => (replicate_right_inj h).1

Premises used: Iff.mp, Function.Injective, Sym.replicate_right_inj
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α n_1
a b : α
n : ℕ
inst : Nontrivial α
⊢ Nontrivial.{u_1} (Sym α (n + 1))

Tactic:
(replicate_right_injective n.succ_ne_zero).nontrivial

Premises used: Function.Injective.nontrivial, Nat.succ_ne_zero, Sym.replicate_right_injective
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α n_1
a b : α
n : ℕ
f : α → β
x : Sym α n
⊢ (Multiset.map f (↑x : Multiset α)).card = n

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : α → β
b : β
l : Sym α n
⊢ b ∈ map f l ↔ ∃ a ∈ l, f a = b

Tactic:
Multiset.mem_map

Premises used: Multiset.map, Multiset.mem_map
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
s : Sym α n
h : (↑(map (fun (x : α) ↦ x) s) : Multiset α) = (↑s : Multiset α)
⊢ map (fun (x : α) ↦ x) s = s

Tactic:
ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
s : Sym α n
⊢ (↑(map (fun (x : α) ↦ x) s) : Multiset α) = (↑s : Multiset α)

Tactic:
simp only [map, Multiset.map_id', ← val_eq_coe]

Premises used: Sym.val_eq_coe, Multiset.map_id', Sym.map
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
s : Sym α n
h : (↑(map id s) : Multiset α) = (↑s : Multiset α)
⊢ map id s = s

Tactic:
ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
n : ℕ
s : Sym α n
⊢ (↑(map id s) : Multiset α) = (↑s : Multiset α)

Tactic:
simp only [map, id_eq, Multiset.map_id', ← val_eq_coe]

Premises used: Sym.val_eq_coe, Multiset.map_id', Sym.map, id_eq
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
dsimp : Multiset.map g (Multiset.map f (↑s : Multiset α)) = Multiset.map (g ∘ f) (↑s : Multiset α)
⊢ (↑(map g (map f s)) : Multiset γ) = (↑(map (g ∘ f) s) : Multiset γ)

Tactic:
dsimp only [Sym.map]

Premises used: Sym.map
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f (↑s : Multiset α)) = Multiset.map (g ∘ f) (↑s : Multiset α)

Tactic:
simp
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ Eq (α := Sym β 0) (map f 0) 0

Tactic:
rfl

Premises used: Multiset.map, List.map, Multiset.zero, Multiset.ofList, Sym.map, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : α → β
a : α
s : Sym α n
⊢ map f (a ::ₛ s) = f a ::ₛ map f s

Tactic:
ext <| Multiset.map_cons _ _ _

Premises used: Multiset.map_cons, Sym.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f g : α → β
s : Sym α n
h : ∀ x ∈ s, f x = g x
⊢ map f s = map g s

Tactic:
Subtype.ext <| Multiset.map_congr rfl h

Premises used: Sym, Multiset.map_congr, rfl, Subtype.ext
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a b : α
f : α → β
m : Multiset α
hc : m.card = n
⊢ (Multiset.map f m).card = n

Tactic:
simp [hc]
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : α → β
m : Multiset α
hc : m.card = n
⊢ map f (mk m hc) = mk (Multiset.map f m) ⋯

Tactic:
rfl

Premises used: Sym.map, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n : ℕ
s : Sym α n
f : α → β
⊢ (↑(map f s) : Multiset β) = Multiset.map f (↑s : Multiset α)

Tactic:
rfl

Premises used: Multiset.map, Sym.toMultiset, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
n : ℕ
⊢ Injective (α := Sym α n) (map f)

Tactic:
fun _ _ h =>
  coe_injective <| Multiset.map_injective hf <| coe_inj.2 h

Premises used: Iff.mpr, Sym.coe_inj, Sym.coe_injective, Multiset.map_injective, Function.Injective
-- Module: Mathlib.Data.Sym.Basic
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
rw₂ rw₃ : x = x
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) x) = x

Tactic:
rw [map_map, Equiv.symm_comp_self, map_id]

Premises used: Sym.map_id, Equiv.symm_comp_self, Sym.map_map
-- Module: Mathlib.Data.Sym.Basic
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
rw₂ rw₃ : x = x
⊢ map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (map (⇑e.symm : (a : β) → α) x) = x

Tactic:
rw [map_map, Equiv.self_comp_symm, map_id]

Premises used: Sym.map_id, Equiv.self_comp_symm, Sym.map_map
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
s : Sym α n
rw : (↑s : Multiset α).attach.card
| n

Tactic:
rw [← s.2, ← Multiset.card_attach]

Premises used: Multiset.card_attach, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
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
conv_rhs₁ : (↑s : Multiset α).attach.card = (↑s : Multiset α).attach.card
⊢ (↑s : Multiset α).attach.card = n

Tactic:
conv_rhs => rw [← s.2, ← Multiset.card_attach]

Premises used: Multiset.card_attach, Subtype.property
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
m : Multiset α
hc : m.card = n
⊢ (mk m hc).attach = mk m.attach ⋯

Tactic:
rfl

Premises used: Sym.attach, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
⊢ (↑s.attach : Multiset { x : α // x ∈ s }) = (↑s : Multiset α).attach

Tactic:
rfl

Premises used: Multiset.pmap, Sym.toMultiset, Multiset.attach, rfl
-- Module: Mathlib.Data.Sym.Basic
Goal:
α : Type u_1
n : ℕ
s : Sym α n
⊢ map (Subtype.val (p := fun (x : α) ↦ x ∈ s)) s.attach = s

Tactic:
coe_injective <| Multiset.attach_map_val _

Premises used: Multiset.attach_map_val, Sym.coe_injective