awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
    (fun (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) ↦ x (cast ⋯ t).take * (y (cast ⋯ t).drop.take * z (cast ⋯ t).drop.drop)) t

Tactic:
rfl
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
eq eq₁ : ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ (ds₂ ++ ds₃)
⊢ ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃

Tactic:
rw [append_assoc]

Premises used: List.append_assoc
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
⊢ x ⊗ y ⊗ z ≍ x ⊗ (y ⊗ z)

Tactic:
simp [cast_heq, mul_assoc0, assocLeft]

Premises used: Holor.assocLeft, cast_heq, Holor.mul_assoc0
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ : List ℕ
inst : Distrib α
x : Holor α ds₁
y z : Holor α ds₂
⊢ x ⊗ (y + z) = x ⊗ y + x ⊗ z

Tactic:
funext fun t => left_distrib (x t.take) (y t.drop) (z t.drop)

Premises used: funext, HolorIndex.take, Holor, HolorIndex.drop, left_distrib
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds₁ ds₂ : List ℕ
inst : Distrib α
x y : Holor α ds₁
z : Holor α ds₂
⊢ (x + y) ⊗ z = x ⊗ z + y ⊗ z

Tactic:
funext fun t => add_mul (x t.take) (y t.take) (z t.drop)

Premises used: add_mul, funext, HolorIndex.take, Holor, HolorIndex.drop
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ : List ℕ
α : Type
inst : MulZeroClass α
x : Holor α ds₂
⊢ Eq (α := Holor α (ds₁ ++ ds₂)) (0 ⊗ x) 0

Tactic:
funext fun t => zero_mul (x (HolorIndex.drop t))

Premises used: MulZeroClass.zero_mul, funext, Holor, HolorIndex.drop
-- Module: Mathlib.Data.Holor
Goal:
ds₁ ds₂ : List ℕ
α : Type
inst : MulZeroClass α
x : Holor α ds₁
⊢ Eq (α := Holor α (ds₁ ++ ds₂)) (x ⊗ 0) 0

Tactic:
funext fun t => mul_zero (x (HolorIndex.take t))

Premises used: MulZeroClass.mul_zero, funext, HolorIndex.take, Holor
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
x : Holor α []
y : Holor α ds
⊢ x ⊗ y = x (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is []) [] ⋯) • y

Tactic:
simp +unfoldPartialApp [mul, SMul.smul, HolorIndex.take, HolorIndex.drop,
    HSMul.hSMul]

Premises used: HolorIndex.take, HSMul.hSMul, Holor.mul, HolorIndex.drop, SMul.smul
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : (↑t : List ℕ) = i :: is
rw : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← h]
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : (↑t : List ℕ) = i :: is
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)

Tactic:
t.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds ds₁ ds₂ ds₃ : List ℕ
p : HolorIndex (d :: ds) → Prop
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
h : (↑t : List ℕ) = i :: is
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)

Tactic:
exact t.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : (↑t : List ℕ) = i :: is
rw : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← hiis]
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : (↑t : List ℕ) = i :: is
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)

Tactic:
t.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : (↑t : List ℕ) = i :: is
⊢ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)

Tactic:
exact t.2

Premises used: Subtype.property
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : (↑t : List ℕ) = i :: is
hiisdds : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds
rw rw₁ :
  y.slice i hid (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds) is hisds) =
    y.slice i hid (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds) is hisds)
⊢ x.slice i hid (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds) is hisds) =
    y.slice i hid (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds) is hisds)

Tactic:
rw [h]
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : i = j
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Premises used: Holor.slice, HolorIndex.take, Holor.mul, HolorIndex.drop, Holor.unitVec
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
simp : Eq (α := α) 0 (0 t)
⊢ (unitVec d j ⊗ x).slice i hid t = (if i = j then x else 0) t

Tactic:
simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]

Premises used: Holor.slice, HolorIndex.take, Holor.mul, HolorIndex.drop, Holor.unitVec
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
i j : ℕ
hid : i < d
x : Holor α ds
t : HolorIndex ds
h : ¬i = j
⊢ Eq (α := α) 0 (0 t)

Tactic:
rfl
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Add α
i : ℕ
hid : i < d
x y : Holor α (d :: ds)
t : HolorIndex ds
⊢ (x.slice i hid + y.slice i hid) t = (x + y).slice i hid t

Tactic:
simp [slice, (· + ·), Add.add]

Premises used: Add.add, Holor.slice, HAdd.hAdd
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Zero α
i : ℕ
hid : i < d
⊢ Eq (α := Holor α ds) (slice 0 i hid) 0

Tactic:
rfl

Premises used: Holor.slice, rfl
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid)

Tactic:
Finset.induction_on s ?_ ?_

Premises used: Finset.induction_on
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
refine_1 : Eq (α := Holor α ds) (∑ x ∈ ∅, (f x).slice i hid) (slice (∑ x ∈ ∅, f x) i hid)
refine_2 :
  ∀ (a : β) (s : Finset β),
    a ∉ s →
      Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid) →
        Eq (α := Holor α ds) (∑ x ∈ insert a s, (f x).slice i hid) (slice (∑ x ∈ insert a s, f x) i hid)
⊢ Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid)

Tactic:
refine Finset.induction_on s ?_ ?_
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
⊢ Eq (α := Holor α ds) (∑ x ∈ ∅, (f x).slice i hid) (slice (∑ x ∈ ∅, f x) i hid)

Tactic:
simp [slice_zero]

Premises used: Holor.slice_zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a : β
refine_2 :
  ∀ (s : Finset β),
    a ∉ s →
      Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid) →
        Eq (α := Holor α ds) (∑ x ∈ insert a s, (f x).slice i hid) (slice (∑ x ∈ insert a s, f x) i hid)
⊢ ∀ (s : Finset β),
    a ∉ s →
      Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid) →
        Eq (α := Holor α ds) (∑ x ∈ insert a s, (f x).slice i hid) (slice (∑ x ∈ insert a s, f x) i hid)

Tactic:
_
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : AddCommMonoid α
β : Type
i : ℕ
hid : i < d
s : Finset β
f : β → Holor α (d :: ds)
this : DecidableEq β := Classical.decEq β
a : β
s_1 : Finset β
h_not_in : a ∉ s_1
ih : Eq (α := Holor α ds) (∑ x ∈ s_1, (f x).slice i hid) (slice (∑ x ∈ s_1, f x) i hid)
refine_2 : (f a).slice i hid + ∑ x ∈ s_1, (f x).slice i hid = slice (∑ x ∈ insert a s_1, f x) i hid
refine_2₁ : (f a).slice i hid + slice (∑ x ∈ s_1, f x) i hid = slice (∑ x ∈ insert a s_1, f x) i hid
refine_2₂ : (f a + ∑ x ∈ s_1, f x).slice i hid = slice (∑ x ∈ insert a s_1, f x) i hid
refine_2₃ refine_2₄ : (f a + ∑ x ∈ s_1, f x).slice i hid = (f a + ∑ x ∈ s_1, f x).slice i hid
⊢ Eq (α := Holor α ds) (∑ x ∈ insert a s_1, (f x).slice i hid) (slice (∑ x ∈ insert a s_1, f x) i hid)

Tactic:
rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]

Premises used: Holor.slice_add, Finset.sum_insert
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
apply : slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) = x.slice
⊢ ∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯ = x

Tactic:
apply slice_eq _ _ _

Premises used: Holor.slice_eq
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
h :
  ∀ (i : ℕ) (hid : i < d),
    slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) i hid = x.slice i hid
⊢ slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) = x.slice

Tactic:
ext i hid
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
h : ∑ x_1 ∈ (Finset.range d).attach, (unitVec d (↑x_1 : ℕ) ⊗ x.slice (↑x_1 : ℕ) ⋯).slice i hid = x.slice i hid
⊢ slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) i hid = x.slice i hid

Tactic:
rw [← slice_sum]

Premises used: Holor.slice_sum
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
h : (∑ x_1 ∈ (Finset.range d).attach, if i = (↑x_1 : ℕ) then x.slice (↑x_1 : ℕ) ⋯ else 0) = x.slice i hid
⊢ ∑ 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]

Premises used: Holor.slice_unitVec_mul
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
h :
  (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) then
      x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) ⋯
    else 0) =
    x.slice i hid
h₁ :
  ∀ b ∈ (Finset.range d).attach,
    b ≠ Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯ → (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0
h₂ :
  Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯ ∉ (Finset.range d).attach →
    (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) then
        x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) ⋯
      else 0) =
      0
⊢ (∑ 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)]

Premises used: Iff.mpr, Finset.mem_range, Finset.sum_eq_single, Subtype.mk
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) then
      x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) ⋯
    else 0) =
    x.slice i hid

Tactic:
simp
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
h :
  b ∈ (Finset.range d).attach →
    b ≠ Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯ → (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0
⊢ b ∈ (Finset.range d).attach →
    b ≠ Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯ → (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0

Tactic:
(_ : b ∈ (Finset.range d).attach)
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
h_1 : b ∈ (Finset.range d).attach
h :
  ∀ (hbi : b ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯),
    (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0
⊢ b ≠ Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯ → (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0

Tactic:
(hbi : b ≠ ⟨i, _⟩)
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
h : b ∈ (Finset.range d).attach
hbi : b ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯
⊢ i ≠ (↑b : ℕ)

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

Premises used: Subtype.coe_mk, Ne, Ne.symm, Subtype.ext_iff
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
h : b ∈ (Finset.range d).attach
hbi : b ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯
⊢ i ≠ (↑b : ℕ)

Tactic:
have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
b : ↥(Finset.range d)
h : b ∈ (Finset.range d).attach
hbi : b ≠ Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯
hbi' : i ≠ (↑b : ℕ)
⊢ (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0

Tactic:
simp [hbi']
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯ ∉ (Finset.range d).attach
h : False
⊢ (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) then
      x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i ⋯) : ℕ) ⋯
    else 0) =
    0

Tactic:
exfalso
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯ ∉ (Finset.range d).attach
⊢ False

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

Premises used: Finset.mem_attach, absurd
-- Module: Mathlib.Data.Holor
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
hid' : Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Finset.range d) i ⋯ ∉ (Finset.range d).attach
⊢ False

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

Premises used: Finset.mem_attach, absurd
-- Module: Mathlib.Data.Holor
Goal:
α : Type
inst : Mul α
inst_1 : AddMonoid α
x : Holor α []
⊢ CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)

Tactic:
have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
inst : Mul α
inst_1 : AddMonoid α
x : Holor α []
h : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
rwa : ∀ (h : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) x), CPRankMax 1 x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : CPRankMax 1 x), CPRankMax 1 x
⊢ CPRankMax 1 x

Tactic:
rwa [add_zero x, zero_add] at h

Premises used: zero_add, add_zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
⊢ CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)

Tactic:
have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
rwa : ∀ (h' : CPRankMax 1 (x + 0)), CPRankMax 1 x
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h' : CPRankMax 1 x), CPRankMax 1 x
⊢ CPRankMax 1 x

Tactic:
rwa [zero_add, add_zero] at h'

Premises used: zero_add, add_zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)

Tactic:
simp only [zero_add, hy]

Premises used: zero_add
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (x + y)

Tactic:
match hx with
    | CPRankMax.zero => simp only [zero_add, hy]
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
this : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
simpa only [add_comm, add_assoc, add_left_comm] using this

Premises used: add_left_comm, add_assoc, add_comm
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
suffices : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
suffices CPRankMax (m + n + 1) (x₁ + (x₂ + y)) by
      simpa only [add_comm, add_assoc, add_left_comm] using this
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
a : x₁.CPRankMax1
a₁ : CPRankMax (m + n) (x₂ + y)
⊢ CPRankMax (m + n + 1) (x₁ + (x₂ + y))

Tactic:
apply CPRankMax.succ

Premises used: Holor.CPRankMax.succ
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1

Tactic:
assumption
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Tactic:
cprankMax_add hx₂ hy
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Tactic:
exact cprankMax_add hx₂ hy
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
⊢ (∀ (x : β), Membership.mem (γ := Finset β) ∅ x → CPRankMax n (f x)) →
    CPRankMax (α := α) (Finset.card.{u_1} (α := β) ∅ * n) (ds := ds) (∑ x ∈ ∅, f x)

Tactic:
simp [CPRankMax.zero]

Premises used: Holor.CPRankMax.zero
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
x₁ :
  ∀ (h_x_notin_s : x ∉ s),
    ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)) →
      (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) →
        CPRankMax (α := α) ((insert x s).card * n) (ds := ds) (∑ x ∈ insert x s, f x)
⊢ x ∉ s →
    ((∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)) →
      (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) →
        CPRankMax (α := α) ((insert x s).card * n) (ds := ds) (∑ x ∈ insert x s, f x)

Tactic:
(h_x_notin_s : x ∉ s)
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
simp : CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)
⊢ CPRankMax (α := α) ((insert x s).card * n) (ds := ds) (∑ x ∈ insert x s, f x)

Tactic:
simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_notMem h_x_notin_s]

Premises used: Finset.card_insert_of_notMem, Finset.sum_insert
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
rw : CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)
⊢ CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)

Tactic:
rw [Nat.right_distrib]

Premises used: Nat.right_distrib
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
simp : CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
⊢ CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)

Tactic:
simp only [Nat.one_mul, Nat.add_comm]

Premises used: Nat.one_mul, Nat.add_comm
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)

Tactic:
grind
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)

Tactic:
have ih' : CPRankMax (Finset.card s * n) (∑ x ∈ s, f x) := by grind
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
ih' : CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
⊢ CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)

Tactic:
cprankMax_add (h_cprank x (Finset.mem_insert_self x s)) ih'

Premises used: Finset.mem_insert_self, Holor.cprankMax_add
-- Module: Mathlib.Data.Holor
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
ih' : CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
⊢ CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)

Tactic:
exact cprankMax_add (h_cprank x (Finset.mem_insert_self x s)) ih'

Premises used: Finset.mem_insert_self, Holor.cprankMax_add
-- Module: Mathlib.Data.Holor
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
⊢ ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)

Tactic:
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)))