awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.FunLike.Module (goal)
Goal:
M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M β
inst_1 : SMul M' β
inst_2 : SMul M F
inst_3 : SMul M' F
inst_4 : IsSMulApply M F α β
inst_5 : IsSMulApply M' F α β
inst_6 : SMulCommClass M M' β
x : M
x_1 : M'
x_2 : F
⊢ x • x_1 • x_2 = x_1 • x • x_2
have h : ∀ (x_3 : α), Eq.{u_5 + 1} (α := β) ((x • x_1 • x_2 : (a : α) → β) x_3 : β) ((x_1 • x • x_2 : (a : α) → β) x_3 : β)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Module (goal)
Goal:
M : Type u_1
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst : SMul M F
inst_1 : SMul.{u_1, u_3} Mᵐᵒᵖ F
inst_2 : SMul M β
inst_3 : SMul.{u_1, u_5} Mᵐᵒᵖ β
inst_4 : IsCentralScalar M β
inst_5 : IsSMulApply M F α β
inst_6 : IsSMulApply.{u_1, u_3, u_4, u_5} Mᵐᵒᵖ F α β
a : M
b : F
⊢ MulOpposite.op a • b = a • b
have h : ∀ (x : α), Eq.{u_5 + 1} (α := β) ((MulOpposite.op a • b : (a : α) → β) x : β) ((a • b : (a : α) → β) x : β)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x x_1 x_2 : F
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have h : ∀ (x_3 : α), Eq (α := α) ((x * x_1 * x_2 : (a : α) → α) x_3 : α) ((x * (x_1 * x_2) : (a : α) → α) x_3 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ 1 * x = x
have h : ∀ (x_1 : α), Eq (α := α) ((1 * x : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ x * 1 = x
have h : ∀ (x_1 : α), Eq (α := α) ((x * 1 : (a : α) → α) x_1 : α) ((x : (a : α) → α) x_1 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
x : F
⊢ 0 * x = 0
have h : ∀ (x_1 : α), Eq (α := α) ((0 * x : (a : α) → α) x_1 : α) ((0 : (a : α) → α) x_1 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Zero α
inst_5 : IsZeroApply F α α
inst_6 : IsOneApplyEqSelf F α
inst_7 : IsMulApplyEqComp F α
inst_8 : ZeroHomClass F α α
f : F
⊢ f * 0 = 0
have h : ∀ (x : α), Eq (α := α) ((f * 0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
f g h : F
⊢ f * (g + h) = f * g + f * h
have h₁ : ∀ (x : α), Eq (α := α) ((f * (g + h) : (a : α) → α) x : α) ((f * g + f * h : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
x x_1 x_2 : F
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2
have h : ∀ (x_3 : α), Eq (α := α) (((x + x_1) * x_2 : (a : α) → α) x_3 : α) ((x * x_2 + x_1 * x_2 : (a : α) → α) x_3 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
⊢ Eq.{u_1 + 1} (α := F) (↑0) 0
have h : ∀ (x : α), Eq (α := α) ((↑0 : (a : α) → α) x : α) ((0 : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : AddCommMonoid α
inst_6 : IsZeroApply F α α
inst_7 : IsAddApply F α α
inst_8 : IsOneApplyEqSelf F α
inst_9 : IsMulApplyEqComp F α
inst_10 : SMul ℕ F
inst_11 : IsSMulApply ℕ F α α
inst_12 : AddMonoidHomClass F α α
inst_13 : NatCast F
inst_14 : IsNatCastApply F α
n : ℕ
⊢ ↑(n + 1) = HAdd.hAdd (α := F) (↑n) 1
have h : ∀ (x : α), Eq (α := α) ((↑(n + 1) : (a : α) → α) x : α) ((HAdd.hAdd (α := F) (↑n) 1 : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
x : ℕ
⊢ Eq.{u_1 + 1} (α := F) (IntCast.intCast (↑x : ℤ)) (↑x : F)
have h : ∀ (x_1 : α), Eq (α := α) ((IntCast.intCast (↑x : ℤ) : (a : α) → α) x_1 : α) (((↑x : F) : (a : α) → α) x_1 : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.FunLike.Ring (goal)
Goal:
F : Type u_1
α : Type u_2
inst : FunLike F α α
inst_1 : Zero F
inst_2 : One F
inst_3 : Mul F
inst_4 : Add F
inst_5 : Neg F
inst_6 : Sub F
inst_7 : AddCommGroup α
inst_8 : IsZeroApply F α α
inst_9 : IsAddApply F α α
inst_10 : IsOneApplyEqSelf F α
inst_11 : IsMulApplyEqComp F α
inst_12 : IsNegApply F α α
inst_13 : IsSubApply F α α
inst_14 : SMul ℕ F
inst_15 : IsSMulApply ℕ F α α
inst_16 : SMul ℤ F
inst_17 : IsSMulApply ℤ F α α
inst_18 : AddMonoidHomClass F α α
inst_19 : NatCast F
inst_20 : IsNatCastApply F α
inst_21 : IntCast F
inst_22 : IsIntCastApply F α
n : ℕ
⊢ Eq.{u_1 + 1} (α := F) (IntCast.intCast (Int.negSucc n)) (-(↑(n + 1) : F))
have h : ∀ (x : α), Eq (α := α) ((IntCast.intCast (Int.negSucc n) : (a : α) → α) x : α) ((-(↑(n + 1) : F) : (a : α) → α) x : α)
Tactic: apply DFunLike.ext
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
ds₁ ds₂ is : List ℕ
eq : ds₁ = ds₂
h : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁
⊢ (↑(cast ⋯ (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁) is h)) : List ℕ) = is
have subst : (↑(cast sorry (Subtype.mk (p := fun (is : List ℕ) ↦ Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) is ds₁) is h)) : List ℕ) = is
Tactic: subst eq
Cleared hypotheses: ds₂, eq
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds₁ ds₂ : List ℕ
eq : ds₁ = ds₂
a : Holor α ds₁
⊢ cast ⋯ a = fun (t : HolorIndex ds₂) ↦ a (cast ⋯ t)
have subst : cast sorry a = fun (t : HolorIndex ds₁) ↦ a (cast sorry t)
Tactic: subst eq
Cleared hypotheses: ds₂, eq
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ (x ⊗ y ⊗ z) t = (x ⊗ (y ⊗ z)).assocLeft t
have rw : (x ⊗ y ⊗ z) t = cast sorry (x ⊗ (y ⊗ z)) t
Tactic: rw [assocLeft]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
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 ⋯ (x ⊗ (y ⊗ z)) t
have unfold : x t.take.take * y t.take.drop * z t.drop =
  cast sorry (fun (t : HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
Tactic: unfold mul
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
⊢ x t.take.take * y t.take.drop * z t.drop =
    cast ⋯ (fun (t : HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
have rw : x t.assocRight.take * (y t.assocRight.drop.take * z t.assocRight.drop.drop) =
  (fun (t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)) ↦ x (cast sorry t).take * (y (cast sorry t).drop.take * z (cast sorry t).drop.drop)) t
Tactic: rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds₁ ds₂ ds₃ : List ℕ
inst : Semigroup α
x : Holor α ds₁
y : Holor α ds₂
z : Holor α ds₃
t : HolorIndex (ds₁ ++ ds₂ ++ ds₃)
rw :
  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
⊢ x t.take.take * y t.take.drop * z t.drop =
    cast ⋯ (fun (t : HolorIndex (ds₁ ++ (ds₂ ++ ds₃))) ↦ x t.take * (y t.drop.take * z t.drop.drop)) t
have eq : ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ ds₂ ++ ds₃
Tactic: rw [mul_assoc, ← HolorIndex.take_take, ← HolorIndex.drop_take, ← HolorIndex.drop_drop,
      cast_type]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
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₃
have eq : ds₁ ++ (ds₂ ++ ds₃) = ds₁ ++ (ds₂ ++ ds₃)
Tactic: rw [append_assoc]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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) (i :: is) (d :: ds)
have rw : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)
Tactic: rw [← h]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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) (i :: is) (d :: ds)
have rw : Forall₂ (fun (x1 x2 : ℕ) ↦ x1 < x2) (↑t : List ℕ) (d :: ds)
Tactic: rw [← hiis]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ 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)
have 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)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
have simp : Eq (α := α) 0 (0 t)
Tactic: simp [slice, mul, HolorIndex.take, unitVec, HolorIndex.drop, h]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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)
have refine_1 : Eq (α := Holor α ds) (∑ x ∈ ∅, (f x).slice i hid) (slice (∑ x ∈ ∅, f x) i hid)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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)
⊢ Eq (α := Holor α ds) (∑ x ∈ s, (f x).slice i hid) (slice (∑ x ∈ s, f x) i hid)
have 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)
Tactic: refine Finset.induction_on s ?_ ?_
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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)
⊢ Eq (α := Holor α ds) (∑ x ∈ insert a s_1, (f x).slice i hid) (slice (∑ x ∈ insert a s_1, f x) i hid)
have 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
Tactic: rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ Eq (α := Holor α ds) (∑ x ∈ insert a s_1, (f x).slice i hid) (slice (∑ x ∈ insert a s_1, f x) i hid)
have 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
Tactic: rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ Eq (α := Holor α ds) (∑ x ∈ insert a s_1, (f x).slice i hid) (slice (∑ x ∈ insert a s_1, f x) i hid)
have refine_2₂ : (f a + ∑ x ∈ 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]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ Eq (α := Holor α ds) (∑ x ∈ insert a s_1, (f x).slice i hid) (slice (∑ x ∈ insert a s_1, f x) i hid)
have refine_2₃ : (f a + ∑ x ∈ s_1, f x).slice i hid = (f a + ∑ x ∈ s_1, f x).slice i hid
Tactic: rw [Finset.sum_insert h_not_in, ih, slice_add, Finset.sum_insert h_not_in]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
⊢ ∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯ = x
have apply : slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry) = x.slice
Tactic: apply slice_eq _ _ _
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
⊢ slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) = x.slice
have h : ∀ (i : ℕ) (hid : i < d),
  slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry) i hid = x.slice i hid
Tactic: ext i hid
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
x : Holor α (d :: ds)
i : ℕ
hid : i < d
⊢ slice (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯) i hid = x.slice i hid
have h : ∑ x_1 ∈ (Finset.range d).attach, (unitVec d (↑x_1 : ℕ) ⊗ x.slice (↑x_1 : ℕ) sorry).slice i hid = x.slice i hid
Tactic: rw [← slice_sum]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
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
have h : (∑ x_1 ∈ (Finset.range d).attach, if i = (↑x_1 : ℕ) then x.slice (↑x_1 : ℕ) sorry else 0) = x.slice i hid
Tactic: simp only [slice_unitVec_mul hid]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
d : ℕ
ds : List ℕ
inst : Semiring α
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
have h : (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i sorry) : ℕ) then
    x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i sorry) : ℕ) sorry
  else 0) =
  x.slice i hid
Tactic: rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = (↑x_1 : ℕ) then x.slice (↑x_1 : ℕ) ⋯ else 0) = x.slice i hid
have h₁ : ∀ b ∈ (Finset.range d).attach,
  b ≠ Subtype.mk (p := Membership.mem (Finset.range d)) i sorry → (if i = (↑b : ℕ) then x.slice (↑b : ℕ) sorry else 0) = 0
Tactic: rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ (∑ x_1 ∈ (Finset.range d).attach, if i = (↑x_1 : ℕ) then x.slice (↑x_1 : ℕ) ⋯ else 0) = x.slice i hid
have h₂ : Subtype.mk (p := Membership.mem (Finset.range d)) i sorry ∉ (Finset.range d).attach →
  (if i = (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i sorry) : ℕ) then
      x.slice (↑(Subtype.mk (p := Membership.mem (Finset.range d)) i sorry) : ℕ) sorry
    else 0) =
    0
Tactic: rw [Finset.sum_eq_single (Subtype.mk i <| Finset.mem_range.2 hid)]
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
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 ⋯
⊢ (if i = (↑b : ℕ) then x.slice (↑b : ℕ) ⋯ else 0) = 0
have hbi' : i ≠ (↑b : ℕ)
Tactic: have hbi' : i ≠ b := by simpa only [Ne, Subtype.ext_iff, Subtype.coe_mk] using hbi.symm
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ (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
have h : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
inst : Mul α
inst_1 : AddMonoid α
x : Holor α []
⊢ CPRankMax 1 x
have h : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
Tactic: have h := CPRankMax.succ 0 x 0 (CPRankMax1.nil x) CPRankMax.zero
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
inst : Mul α
inst_1 : AddMonoid α
x : Holor α []
h : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
⊢ CPRankMax 1 x
have rwa : ∀ (h : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) x), CPRankMax 1 x
Tactic: rwa [add_zero x, zero_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
⊢ CPRankMax 1 x
have h' : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
Tactic: have h' := CPRankMax.succ 0 x 0 h CPRankMax.zero
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds : List ℕ
inst : Mul α
inst_1 : AddMonoid α
x : Holor α ds
h : x.CPRankMax1
h' : CPRankMax (HAdd.hAdd (α := ℕ) 0 1) (x + 0)
⊢ CPRankMax 1 x
have rwa : ∀ (h' : CPRankMax 1 (x + 0)), CPRankMax 1 x
Tactic: rwa [zero_add, add_zero] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ CPRankMax 1 x
have rwa₁ : ∀ (h' : CPRankMax 1 x), CPRankMax 1 x
Tactic: rwa [zero_add, add_zero] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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 + 1 + n) (x₁ + x₂ + y)
have suffices : CPRankMax (m + n + 1) (x₁ + (x₂ + y))
Tactic: suffices CPRankMax (m + n + 1) (x₁ + (x₂ + y)) by
      simpa only [add_comm, add_assoc, add_left_comm] using this
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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
⊢ CPRankMax (m + n + 1) (x₁ + (x₂ + y))
have a₁ : CPRankMax (m + n) (x₂ + y)
Tactic: apply CPRankMax.succ
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
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 (α := α) ((insert x s).card * n) (ds := ds) (∑ x ∈ insert x s, f x)
have simp : CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)
Tactic: simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_notMem h_x_notin_s]