α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ slice (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d)) = slice x
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ ∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d) = x
apply slice_eq _ _ _
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ slice (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d)) i hid = slice x i hid
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ slice (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d)) = slice x
ext (i hid)
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 in Finset.attach (Finset.range d), slice (unitVec d ↑x_1 ⊗ slice x ↑x_1 (_ : Nat.succ ↑x_1 ≤ d)) i hid =
    slice x i hid
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ slice (∑ i in Finset.attach (Finset.range d), unitVec d ↑i ⊗ slice x ↑i (_ : Nat.succ ↑i ≤ d)) i hid = slice x i hid
rw [← slice_sum]
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ x_1 in Finset.attach (Finset.range d), if i = ↑x_1 then slice x ↑x_1 (_ : Nat.succ ↑x_1 ≤ d) else 0) =
    slice x i hid
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 in Finset.attach (Finset.range d), slice (unitVec d ↑x_1 ⊗ slice x ↑x_1 (_ : Nat.succ ↑x_1 ≤ d)) i hid =
    slice x i hid
simp only [slice_unitVec_mul hid]
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
      slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
        (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
    else 0) =
    slice x i hid

case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ (b : { x // x ∈ Finset.range d }),
    b ∈ Finset.attach (Finset.range d) →
      b ≠ { val := i, property := (_ : i ∈ Finset.range d) } →
        (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0

case h.h.h₁
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d) →
    (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
        slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
          (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
      else 0) =
      0
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ x_1 in Finset.attach (Finset.range d), if i = ↑x_1 then slice x ↑x_1 (_ : Nat.succ ↑x_1 ≤ d) else 0) =
    slice x i hid
rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
no goals
case h.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
      slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
        (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
    else 0) =
    slice x i hid
simp
case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ Finset.attach (Finset.range d)
hbi : b ≠ { val := i, property := (_ : i ∈ Finset.range d) }
⊢ (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0
case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ (b : { x // x ∈ Finset.range d }),
    b ∈ Finset.attach (Finset.range d) →
      b ≠ { val := i, property := (_ : i ∈ Finset.range d) } →
        (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0
intro (b : { x // x ∈ Finset.range d }) (_ : b ∈ (Finset.range d).attach)(hbi : b ≠ ⟨i, _⟩)
case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ Finset.attach (Finset.range d)
hbi : b ≠ { val := i, property := (_ : i ∈ Finset.range d) }
hbi' : i ≠ ↑b
⊢ (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0
case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ Finset.attach (Finset.range d)
hbi : b ≠ { val := i, property := (_ : i ∈ Finset.range d) }
⊢ (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0
have hbi' : i ≠ b := by simpa only [Ne.def, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
no goals
case h.h.h₀
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ Finset.attach (Finset.range d)
hbi : b ≠ { val := i, property := (_ : i ∈ Finset.range d) }
hbi' : i ≠ ↑b
⊢ (if i = ↑b then slice x ↑b (_ : Nat.succ ↑b ≤ d) else 0) = 0
simp [hbi']
no goals
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ Finset.attach (Finset.range d)
hbi : b ≠ { val := i, property := (_ : i ∈ Finset.range d) }
⊢ i ≠ ↑b
simpa only [Ne.def, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
case h.h.h₁
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d)
⊢ (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
      slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
        (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
    else 0) =
    0
case h.h.h₁
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d) →
    (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
        slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
          (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
      else 0) =
      0
intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
case h.h.h₁.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d)
⊢ False
case h.h.h₁
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d)
⊢ (if i = ↑{ val := i, property := (_ : i ∈ Finset.range d) } then
      slice x ↑{ val := i, property := (_ : i ∈ Finset.range d) }
        (_ : Nat.succ ↑{ val := i, property := (_ : i ∈ Finset.range d) } ≤ d)
    else 0) =
    0
exfalso
no goals
case h.h.h₁.h
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ¬{ val := i, property := (_ : i ∈ Finset.range d) } ∈ Finset.attach (Finset.range d)
⊢ False
exact absurd (Finset.mem_attach _ _) hid'