[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ esymm (map f s.val) n = ∑ t in Finset.powersetLen n s, Finset.prod t f
[PROOFSTEP]
simp only [esymm, powersetLen_map, ← Finset.map_val_val_powersetLen, map_map]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ sum (map ((fun x => prod x) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetLen n s).val) =
    ∑ t in Finset.powersetLen n s, Finset.prod t f
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha : a✝ ∈ setOf IsSymmetric
hb : b✝ ∈ setOf IsSymmetric
e : Perm σ
⊢ ↑(rename ↑e) (a✝ * b✝) = a✝ * b✝
[PROOFSTEP]
rw [AlgHom.map_mul, ha, hb]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝ : CommSemiring R
a✝ b✝ : MvPolynomial σ R
ha :
  a✝ ∈
    {
          toSubsemigroup :=
            { carrier := setOf IsSymmetric,
              mul_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ setOf IsSymmetric → b ∈ setOf IsSymmetric → ∀ (e : Perm σ), ↑(rename ↑e) (a * b) = a * b) },
          one_mem' := (_ : 1 ∈ setOf IsSymmetric) }.toSubsemigroup.carrier
hb :
  b✝ ∈
    {
          toSubsemigroup :=
            { carrier := setOf IsSymmetric,
              mul_mem' :=
                (_ :
                  ∀ {a b : MvPolynomial σ R},
                    a ∈ setOf IsSymmetric → b ∈ setOf IsSymmetric → ∀ (e : Perm σ), ↑(rename ↑e) (a * b) = a * b) },
          one_mem' := (_ : 1 ∈ setOf IsSymmetric) }.toSubsemigroup.carrier
e : Perm σ
⊢ ↑(rename ↑e) (a✝ + b✝) = a✝ + b✝
[PROOFSTEP]
rw [AlgHom.map_add, ha, hb]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
φ ψ : MvPolynomial σ R
hφ : IsSymmetric φ
f : R →+* S
e : Perm σ
⊢ ↑(rename ↑e) (↑(MvPolynomial.map f) φ) = ↑(MvPolynomial.map f) φ
[PROOFSTEP]
rw [← map_rename, hφ]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R = Multiset.esymm (Multiset.map X univ.val)
[PROOFSTEP]
refine' funext fun n => (Finset.esymm_map_val X _ n).symm
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Algebra R S
f : σ → S
n : ℕ
⊢ ↑(aeval f) (esymm σ R n) = Multiset.esymm (Multiset.map f univ.val) n
[PROOFSTEP]
simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, Finset.esymm_map_val]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ t in powersetLen n univ, ↑(monomial (∑ i in t, Finsupp.single i 1)) 1
[PROOFSTEP]
simp_rw [monomial_sum_one]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ x in powersetLen n univ, ∏ x in x, ↑(monomial (Finsupp.single x 1)) 1
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R 0 = 1
[PROOFSTEP]
simp only [esymm, powersetLen_zero, sum_singleton, prod_empty]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
f : R →+* S
⊢ ↑(map f) (esymm σ R n) = esymm σ S n
[PROOFSTEP]
simp_rw [esymm, map_sum, map_prod, map_X]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ↑(rename ↑e) (esymm σ R n) = ∑ x in powersetLen n univ, ∏ i in x, X (↑e i)
[PROOFSTEP]
simp_rw [esymm, map_sum, map_prod, rename_X]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ i in x, X (↑e i) =
    ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i
[PROOFSTEP]
simp [Finset.powersetLen_map, -Finset.map_univ_equiv]
  --Porting note: Why did `mapEmbedding_apply` not work?
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in ↑(mapEmbedding (Equiv.toEmbedding e)) x, X i
[PROOFSTEP]
dsimp [mapEmbedding, OrderEmbedding.ofMapLEIff]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ x in powersetLen n univ, ∏ x in x, X (↑e x) =
    ∑ x in powersetLen n univ, ∏ i in Finset.map (Equiv.toEmbedding e) x, X i
[PROOFSTEP]
simp
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ∑ t in powersetLen n (Finset.map (Equiv.toEmbedding e) univ), ∏ i in t, X i = ∑ t in powersetLen n univ, ∏ i in t, X i
[PROOFSTEP]
rw [Finset.map_univ_equiv]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ IsSymmetric (esymm σ R n)
[PROOFSTEP]
intro
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e✝ : Perm σ
⊢ ↑(rename ↑e✝) (esymm σ R n) = esymm σ R n
[PROOFSTEP]
rw [rename_esymm]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [esymm_eq_sum_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (∑ t in powersetLen n univ, ↑(monomial (∑ i in t, Finsupp.single i 1)) 1) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
simp only [← single_eq_monomial]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (∑ x in powersetLen n univ, Finsupp.single (∑ i in x, Finsupp.single i 1) 1) =
    Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
refine' Finsupp.support_sum_eq_biUnion (powersetLen n (univ : Finset σ)) _
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ ∀ (i₁ i₂ : Finset σ),
    i₁ ≠ i₂ →
      Disjoint (Finsupp.single (∑ i in i₁, Finsupp.single i 1) 1).support
        (Finsupp.single (∑ i in i₂, Finsupp.single i 1) 1).support
[PROOFSTEP]
intro s t hst
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ Disjoint (Finsupp.single (∑ i in s, Finsupp.single i 1) 1).support
    (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [Finset.disjoint_left, Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i in s, Finsupp.single i 1} → ¬a ∈ (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero _ one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a ∈ {∑ i in s, Finsupp.single i 1} → ¬a ∈ {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
simp only [one_ne_zero, mem_singleton, Finsupp.mem_support_iff]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
⊢ ∀ ⦃a : σ →₀ ℕ⦄, a = ∑ i in s, Finsupp.single i 1 → ¬a = ∑ i in t, Finsupp.single i 1
[PROOFSTEP]
rintro a h rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
⊢ False
[PROOFSTEP]
have := congr_arg Finsupp.support h
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ False
[PROOFSTEP]
rw [Finsupp.support_sum_eq_biUnion, Finsupp.support_sum_eq_biUnion] at this 
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have hsingle : ∀ s : Finset σ, ∀ x : σ, x ∈ s → (Finsupp.single x 1).support = { x } :=
  by
  intros _ x _
  rw [Finsupp.support_single_ne_zero x one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
⊢ ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
[PROOFSTEP]
intros _ x _
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
s✝ : Finset σ
x : σ
a✝ : x ∈ s✝
⊢ (Finsupp.single x 1).support = {x}
[PROOFSTEP]
rw [Finsupp.support_single_ne_zero x one_ne_zero]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have hs := biUnion_congr (of_eq_true (eq_self s)) (hsingle s)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
have ht := biUnion_congr (of_eq_true (eq_self t)) (hsingle t)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = Finset.biUnion s fun i => (Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
⊢ False
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
rw [hs, ht] at this 
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun a => {a}) = Finset.biUnion s fun a => {a}
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
⊢ False
[PROOFSTEP]
simp only [biUnion_singleton_eq_self] at this 
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝¹ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this✝ : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
hsingle : ∀ (s : Finset σ) (x : σ), x ∈ s → (Finsupp.single x 1).support = {x}
hs : (Finset.biUnion s fun a => (Finsupp.single a 1).support) = Finset.biUnion s fun a => {a}
ht : (Finset.biUnion t fun a => (Finsupp.single a 1).support) = Finset.biUnion t fun a => {a}
this : t = s
⊢ False
[PROOFSTEP]
exact absurd this hst.symm
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
all_goals intro x y; simp [Finsupp.support_single_disjoint]
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
intro x y
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this✝ : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
this : (Finset.biUnion t fun i => (Finsupp.single i 1).support) = (∑ i in s, Finsupp.single i 1).support
x y : σ
⊢ x ≠ y → Disjoint (Finsupp.single x 1).support (Finsupp.single y 1).support
[PROOFSTEP]
simp [Finsupp.support_single_disjoint]
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
⊢ ∀ (i₁ i₂ : σ), i₁ ≠ i₂ → Disjoint (Finsupp.single i₁ 1).support (Finsupp.single i₂ 1).support
[PROOFSTEP]
intro x y
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
s t : Finset σ
hst : s ≠ t
h : ∑ i in t, Finsupp.single i 1 = ∑ i in s, Finsupp.single i 1
this : (∑ i in t, Finsupp.single i 1).support = (∑ i in s, Finsupp.single i 1).support
x y : σ
⊢ x ≠ y → Disjoint (Finsupp.single x 1).support (Finsupp.single y 1).support
[PROOFSTEP]
simp [Finsupp.support_single_disjoint]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) = Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
rw [support_esymm'']
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support) =
    Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
congr
[GOAL]
case e_t
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (fun t => (Finsupp.single (∑ i in t, Finsupp.single i 1) 1).support) = fun t => {∑ i in t, Finsupp.single i 1}
[PROOFSTEP]
funext
[GOAL]
case e_t.h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
x✝ : Finset σ
⊢ (Finsupp.single (∑ i in x✝, Finsupp.single i 1) 1).support = {∑ i in x✝, Finsupp.single i 1}
[PROOFSTEP]
exact Finsupp.support_single_ne_zero _ one_ne_zero
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ support (esymm σ R n) = image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
[PROOFSTEP]
rw [support_esymm']
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Fintype σ
inst✝² : Fintype τ
n : ℕ
inst✝¹ : DecidableEq σ
inst✝ : Nontrivial R
⊢ (Finset.biUnion (powersetLen n univ) fun t => {∑ i in t, Finsupp.single i 1}) =
    image (fun t => ∑ i in t, Finsupp.single i 1) (powersetLen n univ)
[PROOFSTEP]
exact biUnion_singleton
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
classical
have : (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i : σ in t, Finsupp.single i 1) = Finset.val :=
  by
  funext
  simp [Finsupp.toMultiset_sum_single]
rw [degrees_def, support_esymm, sup_image, this]
have : ((powersetLen n univ).sup (fun (x : Finset σ) => x)).val = sup (powersetLen n univ) val :=
  by
  refine' comp_sup_eq_sup_comp _ _ _
  · intros
    simp only [union_val, sup_eq_union]
    congr
  · rfl
rw [← this]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
simpa using powersetLen_sup _ _ (Nat.lt_of_succ_le hn)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
have : (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i : σ in t, Finsupp.single i 1) = Finset.val :=
  by
  funext
  simp [Finsupp.toMultiset_sum_single]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
[PROOFSTEP]
funext
[GOAL]
case h
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
x✝ : Finset σ
⊢ (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) x✝ = x✝.val
[PROOFSTEP]
simp [Finsupp.toMultiset_sum_single]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ degrees (esymm σ R n) = univ.val
[PROOFSTEP]
rw [degrees_def, support_esymm, sup_image, this]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ sup (powersetLen n univ) val = univ.val
[PROOFSTEP]
have : ((powersetLen n univ).sup (fun (x : Finset σ) => x)).val = sup (powersetLen n univ) val :=
  by
  refine' comp_sup_eq_sup_comp _ _ _
  · intros
    simp only [union_val, sup_eq_union]
    congr
  · rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
[PROOFSTEP]
refine' comp_sup_eq_sup_comp _ _ _
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ∀ (x y : Finset σ), (x ⊔ y).val = x.val ⊔ y.val
[PROOFSTEP]
intros
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ (x✝ ⊔ y✝).val = x✝.val ⊔ y✝.val
[PROOFSTEP]
simp only [union_val, sup_eq_union]
[GOAL]
case refine'_1
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
x✝ y✝ : Finset σ
⊢ x✝.val ∪ y✝.val = x✝.val ⊔ y✝.val
[PROOFSTEP]
congr
[GOAL]
case refine'_2
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
⊢ ⊥.val = ⊥
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ sup (powersetLen n univ) val = univ.val
[PROOFSTEP]
rw [← this]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
n : ℕ
hpos : 0 < n
hn : n ≤ Fintype.card σ
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
this : (sup (powersetLen n univ) fun x => x).val = sup (powersetLen n univ) val
⊢ (sup (powersetLen n univ) fun x => x).val = univ.val
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
[GOAL]
case intro
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Fintype σ
inst✝¹ : Fintype τ
inst✝ : Nontrivial R
this✝ : (↑Finsupp.toMultiset ∘ fun t => ∑ i in t, Finsupp.single i 1) = val
k : ℕ
hpos : 0 < Nat.succ k
hn : Nat.succ k ≤ Fintype.card σ
this : (sup (powersetLen (Nat.succ k) univ) fun x => x).val = sup (powersetLen (Nat.succ k) univ) val
⊢ (sup (powersetLen (Nat.succ k) univ) fun x => x).val = univ.val
[PROOFSTEP]
simpa using powersetLen_sup _ _ (Nat.lt_of_succ_le hn)
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ psum σ R 0 = ↑(Fintype.card σ)
[PROOFSTEP]
simp only [psum, _root_.pow_zero, ← cast_card]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ ↑(card univ) = ↑(Fintype.card σ)
[PROOFSTEP]
exact rfl
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ psum σ R 1 = ∑ i : σ, X i
[PROOFSTEP]
simp only [psum, _root_.pow_one]
[GOAL]
σ : Type u_1
R : Type u_2
τ : Type u_3
S : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
e : σ ≃ τ
⊢ ↑(rename ↑e) (psum σ R n) = psum τ R n
[PROOFSTEP]
simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
