-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem msymm_one : msymm σ R (.indiscrete 1) = ∑ i, X i

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i : σ, X i

Tactic:
have : (fun (x : Sym σ 1) ↦ x ∈ Set.univ) =
    (fun x ↦ Nat.Partition.ofSym x = Nat.Partition.indiscrete 1) := by
  simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i : σ, X i

Proof state:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : { x // x ∈ Set.univ }
⊢ (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((Equiv.subtypeEquivProp this) x)).prod

Tactic:
congr

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ (Multiset.map X {x}).prod = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
congr

Result:
no goals

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ msymm σ R (Nat.Partition.indiscrete 1) = ∑ i : σ, X i

Tactic:
symm

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ i : σ, X i = msymm σ R (Nat.Partition.indiscrete 1)

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ i : σ, X i = msymm σ R (Nat.Partition.indiscrete 1)

Tactic:
rw [Fintype.sum_equiv (Equiv.trans Sym.oneEquiv (Equiv.Set.univ (Sym σ 1)).symm)
  _ (fun s ↦ (s.1.1.map X).prod)]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ x : ↑Set.univ, (Multiset.map X ↑↑x).prod = msymm σ R (Nat.Partition.indiscrete 1)

σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : σ), X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : σ), X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
intro x

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Proof state:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : { x // x ∈ Set.univ }), (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((Equiv.subtypeEquivProp this) x)).prod

Tactic:
intro x

Result:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : { x // x ∈ Set.univ }
⊢ (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((Equiv.subtypeEquivProp this) x)).prod

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ X x = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Tactic:
rw [← Multiset.prod_singleton (X x), ← Multiset.map_singleton]

Result:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
x : σ
⊢ (Multiset.map X {x}).prod = (Multiset.map X ↑↑((Sym.oneEquiv.trans (Equiv.Set.univ (Sym σ 1)).symm) x)).prod

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∑ x : ↑Set.univ, (Multiset.map X ↑↑x).prod = msymm σ R (Nat.Partition.indiscrete 1)

Tactic:
apply Fintype.sum_equiv (Equiv.subtypeEquivProp this)

Result:
case h
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
this : (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1
⊢ ∀ (x : { x // x ∈ Set.univ }), (Multiset.map X ↑↑x).prod = (Multiset.map X ↑↑((Equiv.subtypeEquivProp this) x)).prod

Proof state:
σ : Type u_5
R : Type u_6
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
⊢ (fun x => x ∈ Set.univ) = fun x => Nat.Partition.ofSym x = Nat.Partition.indiscrete 1

Tactic:
simp_rw [Set.mem_univ, Nat.Partition.ofSym_one]

Result:
no goals