-- Mathlib/Data/Holor.lean
theorem sum_unitVec_mul_slice [Ring α] (x : Holor α (d :: ds)) :
    (∑ i ∈ (Finset.range d).attach,
        unitVec d i ⊗ slice x i (Nat.succ_le_of_lt (Finset.mem_range.1 i.prop))) =
      x

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice = x.slice

Tactic:
ext i hid

Result:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice i hid = x.slice i hid

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ i ≠ ↑b

Tactic:
simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm

Result:
no goals

Proof state:
case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
exfalso

Result:
case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ False

Proof state:
case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm

Result:
case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
hbi' : i ≠ ↑b
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Proof state:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid

Tactic:
simp only [slice_unitVec_mul hid]

Result:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = ↑x_1 then x.slice ↑x_1 ⋯ else 0) = x.slice i hid

Proof state:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Tactic:
intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))

Result:
case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Proof state:
case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
intro (b : { x // x ∈ Finset.range d }) (_ : b ∈ (Finset.range d).attach) (hbi : b ≠ ⟨i, _⟩)

Result:
case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Proof state:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ ∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯ = x

Tactic:
apply slice_eq _ _ _

Result:
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice = x.slice

Proof state:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = ↑x_1 then x.slice ↑x_1 ⋯ else 0) = x.slice i hid

Tactic:
rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]

Result:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = x.slice i hid

case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∀ b ∈ (Finset.range d).attach, b ≠ ⟨i, ⋯⟩ → (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ⟨i, ⋯⟩ ∉ (Finset.range d).attach → (if i = ↑⟨i, ⋯⟩ then x.slice ↑⟨i, ⋯⟩ ⋯ else 0) = 0

Proof state:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (∑ i ∈ (Finset.range d).attach, unitVec d ↑i ⊗ x.slice ↑i ⋯).slice i hid = x.slice i hid

Tactic:
rw [← slice_sum]

Result:
case h.h
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ ∑ x_1 ∈ (Finset.range d).attach, (unitVec d ↑x_1 ⊗ x.slice ↑x_1 ⋯).slice i hid = x.slice i hid

Proof state:
case h.h.h₁
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : ⟨i, ⋯⟩ ∉ (Finset.range d).attach
⊢ False

Tactic:
exact absurd (Finset.mem_attach _ _) hid'

Result:
no goals

Proof state:
case h.h.h₀
α : Type
d : ℕ
ds : List ℕ
inst✝ : Ring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : { x // x ∈ Finset.range d }
x✝ : b ∈ (Finset.range d).attach
hbi : b ≠ ⟨i, ⋯⟩
hbi' : i ≠ ↑b
⊢ (if i = ↑b then x.slice ↑b ⋯ else 0) = 0

Tactic:
simp [hbi']

Result:
no goals