awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
M : Type u_1
inst : Zero M
inst_1 : DecidablePred fun (i : ℕ) ↦ Ne.{u_1 + 1} (α := M) (getD [] i 0) 0
⊢ Eq.{u_1 + 1} (α := ℕ →₀ M) (toFinsupp []) 0
have h : ∀ (a : ℕ), Eq.{u_1 + 1} (α := M) ((toFinsupp [] : (a : ℕ) → M) a : M) ((0 : (a : ℕ) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
M : Type u_1
inst : Zero M
x : M
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ [x].getD x_1 0 ≠ 0
⊢ Eq (α := ℕ →₀ M) [x].toFinsupp (Finsupp.single 0 x)
have h : Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) 0 : M) ((Finsupp.single 0 x : (a : ℕ) → M) 0 : M)
Tactic: ext ⟨_ | i⟩
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
M : Type u_1
inst : Zero M
x : M
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ [x].getD x_1 0 ≠ 0
h : Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) 0 : M) ((Finsupp.single 0 x : (a : ℕ) → M) 0 : M)
⊢ Eq (α := ℕ →₀ M) [x].toFinsupp (Finsupp.single 0 x)
have h₁ : ∀ (n : ℕ), Eq (α := M) (([x].toFinsupp : (a : ℕ) → M) (n + 1) : M) ((Finsupp.single 0 x : (a : ℕ) → M) (n + 1) : M)
Tactic: ext ⟨_ | i⟩
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
⊢ (l₁ ++ l₂).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp)
have h : ∀ (n : ℕ),
  Eq (α := R) (((l₁ ++ l₂).toFinsupp : (a : ℕ) → R) n : R)
    ((HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) : (a : ℕ) → R)
        n :
      R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ Eq (α := R) (((l₁ ++ l₂).toFinsupp : (a : ℕ) → R) n : R)
    ((HAdd.hAdd (α := ℕ →₀ R) l₁.toFinsupp (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) : (a : ℕ) → R)
        n :
      R)
have h : (l₁ ++ l₂).getD n 0 =
  HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)
Tactic: simp only [toFinsupp_apply, Finsupp.add_apply]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
h : n < l₁.length
⊢ (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)
have h₁ : n ∉ Set.range (ι := ℕ) (⇑(addLeftEmbedding l₁.length) : (a : ℕ) → ℕ)
Tactic: rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
h : l₁.length ≤ n
⊢ (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)
have h₁ : ∀ (k : ℕ) (h : l₁.length ≤ l₁.length + k),
  (l₁ ++ l₂).getD (l₁.length + k) 0 =
    HAdd.hAdd (β := R) (l₁.getD (l₁.length + k) 0)
      ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k) : R)
Tactic: rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
k : ℕ
h : l₁.length ≤ l₁.length + k
⊢ (l₁ ++ l₂).getD (l₁.length + k) 0 =
    HAdd.hAdd (β := R) (l₁.getD (l₁.length + k) 0)
      ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k) : R)
have h₁ : l₂.getD k 0 = (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) (l₁.length + k)
Tactic: rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (hypothesis)
Goal:
R : Type u_2
inst : AddZeroClass R
l₁ l₂ : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ l₁.getD x 0 ≠ 0
inst_3 : DecidablePred fun (x : ℕ) ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ (l₁ ++ l₂).getD n 0 =
    HAdd.hAdd (β := R) (l₁.getD n 0) ((Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp : (a : ℕ) → R) n : R)
have x : n < l₁.length ∨ l₁.length ≤ n
Tactic: cases lt_or_ge n l₁.length with
  | inl h =>
    rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
    rintro ⟨k, rfl : length l₁ + k = n⟩
    lia
  | inr h =>
    rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
    rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
    exact Eq.symm (Finsupp.embDomain_apply_self _ _ _)
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)
have h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
Tactic: convert! toFinsupp_append [x] xs using 3
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)
have h₁ : addRightEmbedding 1 = addLeftEmbedding [x].length
Tactic: convert! toFinsupp_append [x] xs using 3
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ addRightEmbedding 1 = addLeftEmbedding [x].length
have h : ∀ (n : ℕ), Eq (α := ℕ) ((addRightEmbedding 1 : (a : ℕ) → ℕ) n : ℕ) ((addLeftEmbedding [x].length : (a : ℕ) → ℕ) n : ℕ)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)
have h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
Tactic: classical
    convert! toFinsupp_append [x] xs using 3
    · exact (toFinsupp_singleton x).symm
    · ext n
      exact add_comm n 1
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x :: xs).getD x_1 0 ≠ 0
inst_2 : DecidablePred fun (x : ℕ) ↦ xs.getD x 0 ≠ 0
h : Eq (α := ℕ →₀ R) (Finsupp.single 0 x) [x].toFinsupp
⊢ (x :: xs).toFinsupp =
    HAdd.hAdd (α := ℕ →₀ R) (Finsupp.single 0 x) (Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp)
have h₁ : addRightEmbedding 1 = addLeftEmbedding [x].length
Tactic: classical
    convert! toFinsupp_append [x] xs using 3
    · exact (toFinsupp_singleton x).symm
    · ext n
      exact add_comm n 1
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have rw : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
rw :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have rw₁ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
rw :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have rw₂ : HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
    (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
rw :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₂ :
  HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
      (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have rw₃ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single (xs.length + 0) x) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
rw :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₂ :
  HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
      (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
rw₃ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single (xs.length + 0) x) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have rw₄ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have classical : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
classical :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have classical₁ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
classical :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have classical₂ : HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
    (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
classical :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₂ :
  HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
      (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have classical₃ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single (xs.length + 0) x) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddZeroClass R
x : R
xs : List R
inst_1 : DecidablePred fun (i : ℕ) ↦ (xs ++ [x]).getD i 0 ≠ 0
inst_2 : DecidablePred fun (i : ℕ) ↦ xs.getD i 0 ≠ 0
classical :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) [x].toFinsupp) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₁ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.embDomain (addLeftEmbedding xs.length) (Finsupp.single 0 x)) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₂ :
  HAdd.hAdd (α := ℕ →₀ R) (β := ℕ →₀ R) xs.toFinsupp
      (Finsupp.single ((addLeftEmbedding xs.length : (a : ℕ) → ℕ) 0) x : ℕ →₀ R) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
classical₃ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single (xs.length + 0) x) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [x]).toFinsupp = HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
have classical₄ : HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x) =
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
Tactic: classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single,
    addLeftEmbedding_apply, add_zero]
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddMonoid R
l : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
⊢ Eq (α := ℕ →₀ R) l.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) l))
have revert : ∀ (l : List R) [inst_2 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0],
  Eq (α := ℕ →₀ R) l.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) l))
Tactic: revert l
Cleared hypotheses: l, inst_1
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddMonoid R
l : List R
⊢ ∀ [inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0],
    Eq (α := ℕ →₀ R) l.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) l))
have nil : ∀ [inst_1 : DecidablePred fun (x : ℕ) ↦ Ne.{u_2 + 1} (α := R) (getD [] x 0) 0],
  Eq.{u_2 + 1} (α := ℕ →₀ R) (toFinsupp []) (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) []))
Tactic: induction l using List.reverseRecOn with
  | nil => exact toFinsupp_nil
  | append_singleton x xs ih =>
    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.ToFinsupp (goal)
Goal:
R : Type u_2
inst : AddMonoid R
l : List R
nil :
  ∀ [inst_1 : DecidablePred fun (x : ℕ) ↦ Ne.{u_2 + 1} (α := R) (getD [] x 0) 0],
    Eq.{u_2 + 1} (α := ℕ →₀ R) (toFinsupp []) (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) []))
⊢ ∀ [inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0],
    Eq (α := ℕ →₀ R) l.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) l))
have append_singleton : ∀ (x : List R) (xs : R)
  (ih :
    ∀ [inst_1 : DecidablePred fun (x_1 : ℕ) ↦ x.getD x_1 0 ≠ 0],
      Eq (α := ℕ →₀ R) x.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) x)))
  [inst_1 : DecidablePred fun (x_1 : ℕ) ↦ (x ++ [xs]).getD x_1 0 ≠ 0],
  Eq (α := ℕ →₀ R) (x ++ [xs]).toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) (x ++ [xs])))
Tactic: induction l using List.reverseRecOn with
  | nil => exact toFinsupp_nil
  | append_singleton x xs ih =>
    classical simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
hl : Triplewise p l
⊢ Triplewise q l
have nil : Triplewise q []
Tactic: induction hl with
  | nil => exact .nil
  | cons head tail ih => exact .cons (head.imp h) ih
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
hl : Triplewise p l
nil : Triplewise q []
⊢ Triplewise q l
have cons : ∀ {a : α} {l : List α} (head : Pairwise (p a) l) (tail : Triplewise p l) (ih : Triplewise q l), Triplewise q (a :: l)
Tactic: induction hl with
  | nil => exact .nil
  | cons head tail ih => exact .cons (head.imp h) ih
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
⊢ Triplewise p' (map f l) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l
have nil : Triplewise p' (map f []) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) []
Tactic: induction l with
  | nil => simp
  | cons h t ih => simp [map, triplewise_cons, ih, pairwise_map]
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
nil : Triplewise p' (map f []) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) []
⊢ Triplewise p' (map f l) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l
have cons : ∀ (h : α) (t : List α) (ih : Triplewise p' (map f t) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) t),
  Triplewise p' (map f (h :: t)) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) (h :: t)
Tactic: induction l with
  | nil => simp
  | cons h t ih => simp [map, triplewise_cons, ih, pairwise_map]
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (hypothesis)
Goal:
α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p' (f a) (f b) (f c) → p a b c
hl : Triplewise p' (map f l)
⊢ Triplewise p l
have hl₁ : Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l
Tactic: rw [triplewise_map] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.List.Triplewise (goal)
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
head : α
tail : List α
ih :
  Triplewise p tail ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)
⊢ Triplewise p (head :: tail) ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < (head :: tail).length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) k hk)
have cons : ((∀ (i j : Nat) (_hi : i < tail.length) (_hj : j < tail.length) (_hij : i < j),
      p head (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i _hi)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j _hj)) ∧
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail i sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail j sorry)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) tail k hk)) ↔
  ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < tail.length + 1),
    p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) i sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) j sorry)
      (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) (head :: tail) k hk)
Tactic: simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]