[GOAL]
ds₁ ds₂ ds₃ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun x x_1 => x < x_1) is ds₁
⊢ ↑(cast (_ : HolorIndex ds₁ = HolorIndex ds₂) { val := is, property := h }) = is
[PROOFSTEP]
subst eq
[GOAL]
ds₁ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is ds₁
⊢ ↑(cast (_ : HolorIndex ds₁ = HolorIndex ds₁) { val := is, property := h }) = is
[PROOFSTEP]
rfl
[GOAL]
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(take (assocRight { val := is, property := h })) = ↑(take (take { val := is, property := h }))
[PROOFSTEP]
simp [assocRight, take, cast_type, List.take_take, Nat.le_add_right, min_eq_left]
[GOAL]
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(take (drop (assocRight { val := is, property := h }))) = ↑(drop (take { val := is, property := h }))
[PROOFSTEP]
simp [assocRight, take, drop, cast_type, List.drop_take]
[GOAL]
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x x_1 => x < x_1) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(drop (drop (assocRight { val := is, property := h }))) = ↑(drop { val := is, property := h })
[PROOFSTEP]
simp [add_comm, assocRight, drop, cast_type, List.drop_drop]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast (_ : Holor α ds₁ = Holor α ds₂) a = fun t => a (cast (_ : HolorIndex ds₂ = HolorIndex ds₁) t)
[PROOFSTEP]
subst eq
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₃ : List ℕ
a : Holor α ds₁
⊢ cast (_ : Holor α ds₁ = Holor α ds₁) a = fun t => a (cast (_ : HolorIndex ds₁ = HolorIndex ds₁) t)
[PROOFSTEP]
rfl
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = assocLeft (x ⊗ (y ⊗ z)) t
[PROOFSTEP]
rw [assocLeft]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃)) (x ⊗ (y ⊗ z)) t
[PROOFSTEP]
unfold mul
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.take t)) * y (HolorIndex.drop (HolorIndex.take t)) * z (HolorIndex.drop t) =
    cast (_ : Holor α (ds₁ ++ (ds₂ ++ ds₃)) = Holor α (ds₁ ++ ds₂ ++ ds₃))
      (fun t =>
        x (HolorIndex.take t) * (y (HolorIndex.take (HolorIndex.drop t)) * z (HolorIndex.drop (HolorIndex.drop t))))
      t
[PROOFSTEP]
rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop, cast_type]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x (HolorIndex.take (HolorIndex.assocRight t)) *
      (y (HolorIndex.take (HolorIndex.drop (HolorIndex.assocRight t))) *
        z (HolorIndex.drop (HolorIndex.drop (HolorIndex.assocRight t)))) =
    (fun t =>
        x (HolorIndex.take (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)) *
          (y
              (HolorIndex.take
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t))) *
            z
              (HolorIndex.drop
                (HolorIndex.drop (cast (_ : HolorIndex (ds₁ ++ ds₂ ++ ds₃) = HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) t)))))
      t
case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
[PROOFSTEP]
rfl
[GOAL]
case eq
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
[PROOFSTEP]
rw [append_assoc]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
⊢ HEq (x ⊗ y ⊗ z) (x ⊗ (y ⊗ z))
[PROOFSTEP]
simp [cast_heq, mul_assoc0, assocLeft]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Monoid α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x { val := [], property := (_ : Forall₂ (fun x x_1 => x < x_1) [] []) } • y
[PROOFSTEP]
simp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop, HSMul.hSMul]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
[PROOFSTEP]
exact t.2
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)
[PROOFSTEP]
rw [← hiis]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x x_1 => x < x_1) (↑t) (d :: ds)
[PROOFSTEP]
exact t.2
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
x y : Holor α (d :: ds)
h : slice x = slice y
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x x_1 => x < x_1) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x x_1 => x < x_1) is ds
⊢ slice x i hid { val := is, property := hisds } = slice y i hid { val := is, property := hisds }
[PROOFSTEP]
rw [h]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ slice (unitVec d j ⊗ x) i hid t = ite (i = j) x 0 t
[PROOFSTEP]
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ slice (unitVec d j ⊗ x) i hid t = ite (i = j) x 0 t
[PROOFSTEP]
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ 0 = OfNat.ofNat 0 t
[PROOFSTEP]
rfl
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Add α
i : ℕ
hid : i < d
x y : Holor α (d :: ds)
t : HolorIndex ds
⊢ (slice x i hid + slice y i hid) t = slice (x + y) i hid t
[PROOFSTEP]
simp [slice, (· + ·), Add.add]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
⊢ ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid
[PROOFSTEP]
letI := Classical.decEq β
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid
[PROOFSTEP]
refine' Finset.induction_on s _ _
[GOAL]
case refine'_1
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∑ x in ∅, slice (f x) i hid = slice (∑ x in ∅, f x) i hid
[PROOFSTEP]
simp [slice_zero]
[GOAL]
case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s →
      ∑ x in s, slice (f x) i hid = slice (∑ x in s, f x) i hid →
        ∑ x in insert a s, slice (f x) i hid = slice (∑ x in insert a s, f x) i hid
[PROOFSTEP]
intro _ _ h_not_in ih
[GOAL]
case refine'_2
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a✝ : β
s✝ : Finset β
h_not_in : ¬a✝ ∈ s✝
ih : ∑ x in s✝, slice (f x) i hid = slice (∑ x in s✝, f x) i hid
⊢ ∑ x in insert a✝ s✝, slice (f x) i hid = slice (∑ x in insert a✝ s✝, f x) i hid
[PROOFSTEP]
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]
[GOAL]
α : 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
[PROOFSTEP]
apply slice_eq _ _ _
[GOAL]
α : 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
[PROOFSTEP]
ext i hid
[GOAL]
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
[PROOFSTEP]
rw [← slice_sum]
[GOAL]
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
[PROOFSTEP]
simp only [slice_unitVec_mul hid]
[GOAL]
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
[PROOFSTEP]
rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
[GOAL]
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
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
intro (b : { x // x ∈ Finset.range d }) (_ : b ∈ (Finset.range d).attach) (hbi : b ≠ ⟨i, _⟩)
[GOAL]
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
[PROOFSTEP]
have hbi' : i ≠ b := by simpa only [Ne.def, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
[GOAL]
α : 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
[PROOFSTEP]
simpa only [Ne.def, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
[GOAL]
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
[PROOFSTEP]
simp [hbi']
[GOAL]
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
[PROOFSTEP]
intro (hid' : Subtype.mk i _ ∉ Finset.attach (Finset.range d))
[GOAL]
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
[PROOFSTEP]
exfalso
[GOAL]
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
[PROOFSTEP]
exact absurd (Finset.mem_attach _ _) hid'
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α []
⊢ CPRankMax 1 x
[PROOFSTEP]
have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α []
h : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
[PROOFSTEP]
rwa [add_zero x, zero_add] at h 
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : CPRankMax1 x
⊢ CPRankMax 1 x
[PROOFSTEP]
have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
x : Holor α ds
h : CPRankMax1 x
h' : CPRankMax (0 + 1) (x + 0)
⊢ CPRankMax 1 x
[PROOFSTEP]
rwa [zero_add, add_zero] at h' 
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (x + y)
[PROOFSTEP]
match hx with
| CPRankMax.zero => simp only [zero_add, hy]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)
[PROOFSTEP]
simp only [zero_add, hy]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : CPRankMax1 x₁
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)
[PROOFSTEP]
simp only [add_comm, add_assoc]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : CPRankMax1 x₁
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (n + (m + 1)) (x₁ + (x₂ + y))
[PROOFSTEP]
apply CPRankMax.succ
[GOAL]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : CPRankMax1 x₁
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax1 x₁
[PROOFSTEP]
assumption
[GOAL]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : CPRankMax1 x₁
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (Nat.add n (Nat.add m 0)) (x₂ + y)
[PROOFSTEP]
simp only [Nat.add_eq, add_zero, add_comm n m]
[GOAL]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : CPRankMax1 x₁
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)
[PROOFSTEP]
exact cprankMax_add hx₂ hy
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
x : Holor α [d]
⊢ CPRankMax 0 (x ⊗ 0)
[PROOFSTEP]
simp [mul_zero x, CPRankMax.zero]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ (y₁ + y₂))
[PROOFSTEP]
rw [mul_left_distrib]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ y₁ + x ⊗ y₂)
[PROOFSTEP]
rw [Nat.add_comm]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax (1 + n) (x ⊗ y₁ + x ⊗ y₂)
[PROOFSTEP]
apply cprankMax_add
[GOAL]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax 1 (x ⊗ y₁)
[PROOFSTEP]
exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)
[GOAL]
case a
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : CPRankMax1 y₁
hy₂ : CPRankMax n y₂
⊢ CPRankMax n (x ⊗ y₂)
[PROOFSTEP]
exact cprankMax_mul _ x y₂ hy₂
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ (∀ (x : β), x ∈ ∅ → CPRankMax n (f x)) → CPRankMax (Finset.card ∅ * n) (∑ x in ∅, f x)
[PROOFSTEP]
simp [CPRankMax.zero]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ ∀ ⦃a : β⦄ {s : Finset β},
    ¬a ∈ s →
      ((∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)) →
        (∀ (x : β), x ∈ insert a s → CPRankMax n (f x)) →
          CPRankMax (Finset.card (insert a s) * n) (∑ x in insert a s, f x)
[PROOFSTEP]
intro x s (h_x_notin_s : x ∉ s) ih h_cprank
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ CPRankMax (Finset.card (insert x s) * n) (∑ x in insert x s, f x)
[PROOFSTEP]
simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_not_mem h_x_notin_s]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ CPRankMax ((Finset.card s + 1) * n) (f x + ∑ x in s, f x)
[PROOFSTEP]
rw [Nat.right_distrib]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ CPRankMax (Finset.card s * n + 1 * n) (f x + ∑ x in s, f x)
[PROOFSTEP]
simp only [Nat.one_mul, Nat.add_comm]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ CPRankMax (n + Finset.card s * n) (f x + ∑ x in s, f x)
[PROOFSTEP]
have ih' : CPRankMax (Finset.card s * n) (∑ x in s, f x) :=
  by
  apply ih
  intro (x : β) (h_x_in_s : x ∈ s)
  simp only [h_cprank, Finset.mem_insert_of_mem, h_x_in_s]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ CPRankMax (Finset.card s * n) (∑ x in s, f x)
[PROOFSTEP]
apply ih
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
⊢ ∀ (x : β), x ∈ s → CPRankMax n (f x)
[PROOFSTEP]
intro (x : β) (h_x_in_s : x ∈ s)
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x✝ : β
s : Finset β
h_x_notin_s : ¬x✝ ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x : β), x ∈ insert x✝ s → CPRankMax n (f x)
x : β
h_x_in_s : x ∈ s
⊢ CPRankMax n (f x)
[PROOFSTEP]
simp only [h_cprank, Finset.mem_insert_of_mem, h_x_in_s]
[GOAL]
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : ¬x ∈ s
ih : (∀ (x : β), x ∈ s → CPRankMax n (f x)) → CPRankMax (Finset.card s * n) (∑ x in s, f x)
h_cprank : ∀ (x_1 : β), x_1 ∈ insert x s → CPRankMax n (f x_1)
ih' : CPRankMax (Finset.card s * n) (∑ x in s, f x)
⊢ CPRankMax (n + Finset.card s * n) (f x + ∑ x in s, f x)
[PROOFSTEP]
exact cprankMax_add (h_cprank x (Finset.mem_insert_self x s)) ih'
[GOAL]
α : Type
d✝ : ℕ
ds✝ ds₁ ds₂ ds₃ : List ℕ
inst✝ : Ring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
⊢ CPRankMax (prod (d :: ds)) x
[PROOFSTEP]
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)))
[GOAL]
α : 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
[PROOFSTEP]
have h_dds_prod : (List.cons d ds).prod = Finset.card (Finset.range d) * prod ds := by simp [Finset.card_range]
[GOAL]
α : 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
[PROOFSTEP]
simp [Finset.card_range]
[GOAL]
α : 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
[PROOFSTEP]
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
[GOAL]
α : 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
[PROOFSTEP]
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 
[GOAL]
α : 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))
[PROOFSTEP]
rwa [Finset.card_attach] at this 
[GOAL]
α : 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
[PROOFSTEP]
rw [← sum_unitVec_mul_slice x]
[GOAL]
α : 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))
[PROOFSTEP]
rw [h_dds_prod]
[GOAL]
α : 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))
[PROOFSTEP]
exact h_cprankMax_sum
