α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
⊢ CPRankMax (prod (d :: ds)) x
have h_summands :
  ∀ i : { x // x ∈ Finset.range d },
    CPRankMax ds.prod (unitVec d i.1 ⊗ slice x i.1 (mem_range.1 i.2)) :=
  fun i => cprankMax_mul _ _ _ (cprankMax_upper_bound (slice x i.1 (mem_range.1 i.2)))
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
⊢ CPRankMax (prod (d :: ds)) x
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
have h_dds_prod : (List.cons d ds).prod = Finset.card (Finset.range d) * prod ds := by
  simp [Finset.card_range]
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
⊢ CPRankMax (prod (d :: ds)) x
have :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d),
      unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) :=
  cprankMax_sum (Finset.range d).attach _ fun i _ => h_summands i
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
have h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d),
      unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) := by rwa [Finset.card_attach] at this
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d))
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) x
rw [← sum_unitVec_mul_slice x]
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d))
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (prod (d :: ds)) (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d))
rw [h_dds_prod]
no goals
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_cprankMax_sum :
  CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d))
exact h_cprankMax_sum
no goals
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ prod (d :: ds) = Finset.card (Finset.range d) * prod ds
simp [Finset.card_range]
no goals
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : { x // x ∈ Finset.range d }), CPRankMax (prod ds) (unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
h_dds_prod : prod (d :: ds) = Finset.card (Finset.range d) * prod ds
this :
  CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
⊢ CPRankMax (Finset.card (Finset.range d) * prod ds)
    (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : ↑i < d))
rwa [Finset.card_attach] at this