[GOAL]
c : Char
⊢ 0 < utf8Size c
[PROOFSTEP]
simp only [utf8Size]
[GOAL]
c : Char
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1 then UInt32.ofNatCore 1 utf8Size.proof_2
    else
      if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
      else
        if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
        else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
repeat (split; decide)
[GOAL]
c : Char
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1 then UInt32.ofNatCore 1 utf8Size.proof_2
    else
      if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
      else
        if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
        else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
split
[GOAL]
case inl
c : Char
h✝ : c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 < UInt32.ofNatCore 1 utf8Size.proof_2
case inr
c : Char
h✝ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
    else
      if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
      else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
decide
[GOAL]
case inr
c : Char
h✝ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3 then UInt32.ofNatCore 2 utf8Size.proof_4
    else
      if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
      else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
split
[GOAL]
case inr.inl
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 < UInt32.ofNatCore 2 utf8Size.proof_4
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
    else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
decide
[GOAL]
case inr.inr
c : Char
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
⊢ 0 <
    if c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5 then UInt32.ofNatCore 3 utf8Size.proof_6
    else UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
split
[GOAL]
case inr.inr.inl
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 3 utf8Size.proof_6
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
decide
[GOAL]
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
split
[GOAL]
case inr.inr.inr
c : Char
h✝² : ¬c.val ≤ UInt32.ofNatCore 127 utf8Size.proof_1
h✝¹ : ¬c.val ≤ UInt32.ofNatCore 2047 utf8Size.proof_3
h✝ : ¬c.val ≤ UInt32.ofNatCore 65535 utf8Size.proof_5
⊢ 0 < UInt32.ofNatCore 4 utf8Size.proof_7
[PROOFSTEP]
decide
[GOAL]
c : Char
h : isValidCharNat (toNat c)
⊢ ofNat (toNat c) = c
[PROOFSTEP]
rw [Char.ofNat, dif_pos h]
[GOAL]
c : Char
h : isValidCharNat (toNat c)
⊢ ofNatAux (toNat c) h = c
[PROOFSTEP]
rfl


[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


[GOAL]
α : Sort u_1
a : α
⊢ out (mk a) = a
[PROOFSTEP]
let h := (mk a).2
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
⊢ out (mk a) = a
[PROOFSTEP]
show Classical.choose h = a
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
⊢ Classical.choose h = a
[PROOFSTEP]
have := Classical.choose_spec h
[GOAL]
α : Sort u_1
a : α
h : ∃ a_1, (fun b => a_1 = b) = (mk a).fst := (mk a).snd
this : (fun b => Classical.choose h = b) = (mk a).fst
⊢ Classical.choose h = a
[PROOFSTEP]
exact cast (congr_fun this a).symm rfl
[GOAL]
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ mk (out { fst := s, snd := h }) = { fst := s, snd := h }
[PROOFSTEP]
simp [mk]
[GOAL]
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ { fst := fun b => out { fst := s, snd := h } = b,
      snd := (_ : ∃ a, (fun b => a = b) = fun b => out { fst := s, snd := h } = b) } =
    { fst := s, snd := h }
[PROOFSTEP]
congr
[GOAL]
case e_fst
α : Sort u_1
s : α → Prop
h : ∃ a, (fun b => a = b) = s
⊢ (fun b => out { fst := s, snd := h } = b) = s
[PROOFSTEP]
exact Classical.choose_spec h
[GOAL]
α : Sort u_1
a b : Erased α
h : out a = out b
⊢ a = b
[PROOFSTEP]
simpa using congr_arg mk h
[GOAL]
α : Sort u_1
β : Sort u_2
f : α → β
a : Erased α
⊢ out (map f a) = f (out a)
[PROOFSTEP]
simp [map]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529}, Functor.mapConst = Functor.map ∘ Function.const β
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
[PROOFSTEP]
ext
[GOAL]
case h.h.h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝¹ : α✝
x✝ : Erased β✝
⊢ out (Functor.mapConst x✝¹ x✝) = out ((Functor.map ∘ Function.const β✝) x✝¹ x✝)
[PROOFSTEP]
simp [Functor.mapConst]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α : Type ?u.5529} (x : Erased α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ : Type ?u.5529
x✝ : Erased α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ : Type ?u.5529
x✝ : Erased α✝
⊢ out (id <$> x✝) = out x✝
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : Erased α) (y : Erased β),
    (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (SeqLeft.seqLeft x✝ fun x => y✝) = Seq.seq (Function.const β✝ <$> x✝) fun x => y✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ out (SeqLeft.seqLeft x✝ fun x => y✝) = out (Seq.seq (Function.const β✝ <$> x✝) fun x => y✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqLeft.seqLeft]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : Erased α) (y : Erased β),
    (SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α id <$> x) fun x => y
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ (SeqRight.seqRight x✝ fun x => y✝) = Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : Erased α✝
y✝ : Erased β✝
⊢ out (SeqRight.seqRight x✝ fun x => y✝) = out (Seq.seq (Function.const α✝ id <$> x✝) fun x => y✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqRight.seqRight]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (g : α → β) (x : Erased α), (Seq.seq (pure g) fun x_1 => x) = g <$> x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (Seq.seq (pure g✝) fun x => x✝) = g✝ <$> x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ out (Seq.seq (pure g✝) fun x => x✝) = out (g✝ <$> x✝)
[PROOFSTEP]
simp [Seq.seq, Functor.mapConst, SeqRight.seqRight]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (out do
      let a ← x✝
      pure (f✝ a)) =
    out (f✝ <$> x✝)
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (f : Erased (α → β)) (x : Erased α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      Seq.seq f fun x_1 => x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    Seq.seq f✝ fun x => x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (out do
      let x ← f✝
      x <$> x✝) =
    out (Seq.seq f✝ fun x => x✝)
[PROOFSTEP]
simp [Seq.seq]
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β : Type ?u.5529} (x : α) (f : α → Erased β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ : Type ?u.5529
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ out (pure x✝ >>= f✝) = out (f✝ x✝)
[PROOFSTEP]
simp
[GOAL]
src✝ : Monad Erased := Erased.Monad
⊢ ∀ {α β γ : Type ?u.5529} (x : Erased α) (f : α → Erased β) (g : β → Erased γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
src✝ : Monad Erased := Erased.Monad
α✝ β✝ γ✝ : Type ?u.5529
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
ext
[GOAL]
case h
src✝ : Monad Erased := Erased.Monad
α✝ β✝ γ✝ : Type ?u.5529
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ out (x✝ >>= f✝ >>= g✝) = out (x✝ >>= fun x => f✝ x >>= g✝)
[PROOFSTEP]
simp


[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
⊢ size ≠ 0
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : n < size
⊢ Nat.isValidChar ↑(UInt32.ofNat n).val
[PROOFSTEP]
rw [UInt32.val_eq_of_lt]
[GOAL]
n : ℕ
h : n < size
⊢ Nat.isValidChar n
n : ℕ h : n < size ⊢ n < UInt32.size
[PROOFSTEP]
exact Or.inl $ Nat.lt_trans h $ by decide
[GOAL]
n : ℕ
h : n < size
⊢ size < 55296
[PROOFSTEP]
decide
[GOAL]
n : ℕ
h : n < size
⊢ n < UInt32.size
[PROOFSTEP]
exact Nat.lt_trans h $ by decide
[GOAL]
n : ℕ
h : n < size
⊢ size < UInt32.size
[PROOFSTEP]
decide


[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec n
x : G α✝
⊢ (fun {α} p => FG_abs (abs p)) ((fun {α} x => repr (FG_repr x)) x) = x
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ : TypeVec n
x : G α✝
⊢ FG_abs (abs (repr (FG_repr x))) = x
[PROOFSTEP]
rw [abs_repr, FG_abs_repr]
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec n
f : α✝ ⟹ β✝
p : MvPFunctor.Obj (P F) α✝
⊢ (fun {α} p => FG_abs (abs p)) (f <$$> p) = f <$$> (fun {α} p => FG_abs (abs p)) p
[PROOFSTEP]
dsimp
[GOAL]
n : ℕ
F : TypeVec n → Type u
inst✝¹ : MvFunctor F
q : MvQPF F
G : TypeVec n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec n} → F α → G α
FG_repr : {α : TypeVec n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec n
f : α✝ ⟹ β✝
p : MvPFunctor.Obj (P F) α✝
⊢ FG_abs (abs (f <$$> p)) = f <$$> FG_abs (abs p)
[PROOFSTEP]
rw [abs_map, FG_abs_map]