awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.ToFinsupp
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)
rw₄ rw₅ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [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]

Premises used: Finsupp.embDomain_single, addLeftEmbedding_apply, List.toFinsupp_singleton, add_zero, List.toFinsupp_append
-- Module: Mathlib.Data.List.ToFinsupp
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)
classical₄ classical₅ :
  HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x) =
    HAdd.hAdd (α := ℕ →₀ R) xs.toFinsupp (Finsupp.single xs.length x)
⊢ (xs ++ [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]

Premises used: Finsupp.embDomain_single, addLeftEmbedding_apply, List.toFinsupp_singleton, add_zero, List.toFinsupp_append
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddMonoid R
l : List R
inst_1 : DecidablePred fun (x : ℕ) ↦ l.getD x 0 ≠ 0
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))
⊢ Eq (α := ℕ →₀ R) l.toFinsupp (sum (mapIdx (fun (n : ℕ) (r : R) ↦ Finsupp.single n r) l))

Tactic:
revert l
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddMonoid R
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:
toFinsupp_nil

Premises used: List.sum, List.foldr, List.toFinsupp_nil
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddMonoid R
⊢ ∀ [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:
exact toFinsupp_nil

Premises used: List.toFinsupp_nil
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddMonoid R
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:
simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]

Premises used: List.toFinsupp_concat_eq_toFinsupp_add_single, List.sum_append
-- Module: Mathlib.Data.List.ToFinsupp
Goal:
R : Type u_2
inst : AddMonoid R
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:
classical simp [toFinsupp_concat_eq_toFinsupp_add_single, sum_append, ih]

Premises used: List.toFinsupp_concat_eq_toFinsupp_add_single, List.sum_append
-- Module: Mathlib.Data.List.ToFinsupp
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) []))
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])))
⊢ ∀ [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))

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]

Premises used: List.toFinsupp_concat_eq_toFinsupp_add_single, List.sum_append, List.toFinsupp_nil, List.nil
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
a : α
l : List α
p : α → α → α → Prop
⊢ Triplewise p (a :: l) ↔ Pairwise (p a) l ∧ Triplewise p l

Tactic:
grind [triplewise_iff]

Premises used: List.triplewise_iff
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
a : α
p : α → α → α → Prop
⊢ Triplewise p [a]

Tactic:
simp [triplewise_cons]

Premises used: List.triplewise_cons
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
a b : α
p : α → α → α → Prop
⊢ Triplewise p [a, b]

Tactic:
simp [triplewise_cons]

Premises used: List.triplewise_cons
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
a b c : α
p : α → α → α → Prop
⊢ Triplewise p [a, b, c] ↔ p a b c

Tactic:
simp [triplewise_cons]

Premises used: List.triplewise_cons
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
⊢ Triplewise q []

Tactic:
.nil

Premises used: List.Triplewise.nil
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
⊢ Triplewise q []

Tactic:
exact .nil
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
a : α
l_1 : List α
head : Pairwise (p a) l_1
tail : Triplewise p l_1
ih : Triplewise q l_1
⊢ Triplewise q (a :: l_1)

Tactic:
.cons (head.imp h) ih

Premises used: List.Triplewise.cons, List.Pairwise.imp
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p q : α → α → α → Prop
h : ∀ {a b c : α}, p a b c → q a b c
a : α
l_1 : List α
head : Pairwise (p a) l_1
tail : Triplewise p l_1
ih : Triplewise q l_1
⊢ Triplewise q (a :: l_1)

Tactic:
exact .cons (head.imp h) ih
-- Module: Mathlib.Data.List.Triplewise
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 []
cons :
  ∀ {a : α} {l : List α} (head : Pairwise (p a) l) (tail : Triplewise p l) (ih : Triplewise q l), Triplewise q (a :: l)
⊢ Triplewise q l

Tactic:
induction hl with
  | nil => exact .nil
  | cons head tail ih => exact .cons (head.imp h) ih

Premises used: List.head, List.Triplewise.cons, List.tail, List.Triplewise.nil
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
⊢ Triplewise p' (map f []) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) []

Tactic:
simp
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
β : Type u_2
l : List α
f : α → β
p' : β → β → β → Prop
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:
simp [map, triplewise_cons, ih, pairwise_map]

Premises used: List.triplewise_cons, List.map, List.pairwise_map
-- Module: Mathlib.Data.List.Triplewise
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)) []
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)
⊢ Triplewise p' (map f l) ↔ Triplewise (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l

Tactic:
induction l with
  | nil => simp
  | cons h t ih => simp [map, triplewise_cons, ih, pairwise_map]

Premises used: List.triplewise_cons, List.map, List.pairwise_map, List.cons, List.nil
-- Module: Mathlib.Data.List.Triplewise
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 (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l

Tactic:
rw [triplewise_map] at hl

Premises used: List.triplewise_map
-- Module: Mathlib.Data.List.Triplewise
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 (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l
⊢ Triplewise p l

Tactic:
hl.imp h

Premises used: List.Triplewise.imp
-- Module: Mathlib.Data.List.Triplewise
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 (fun (a b c : α) ↦ p' (f a) (f b) (f c)) l
⊢ Triplewise p l

Tactic:
exact hl.imp h

Premises used: List.Triplewise.imp
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
β : Type u_2
l : List α
p : α → α → α → Prop
f : α → β
p' : β → β → β → Prop
h : ∀ {a b c : α}, p a b c → p' (f a) (f b) (f c)
hl : Triplewise p l
⊢ Triplewise p' (List.map f l)

Tactic:
triplewise_map.2 (hl.imp h)

Premises used: Iff.mpr, List.triplewise_map, List.Triplewise.imp
-- Module: Mathlib.Data.List.Triplewise
Goal:
α : Type u_1
l : List α
p : α → α → α → Prop
⊢ Triplewise p [] ↔
    ∀ (i j k : Nat) (hij : i < j) (hjk : j < k) (hk : k < length.{u_1} (α := α) []),
      p (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] i ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] j ⋯)
        (getElem (valid := fun (as : List α) (i : Nat) ↦ i < as.length) [] k hk)

Tactic:
simp
-- Module: Mathlib.Data.List.Triplewise
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)
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 ⋯)
          (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)) ↔
    ∀ (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 ⋯)
        (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)
⊢ 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)

Tactic:
simp only [triplewise_cons, length_cons, pairwise_iff_getElem, ih]

Premises used: List.triplewise_cons, List.length_cons, List.pairwise_iff_getElem
-- Module: Mathlib.Data.List.Triplewise
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)
⊢ ((∀ (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 ⋯)
          (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)) ↔
    ∀ (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 ⋯)
        (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)

Tactic:
⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩

Premises used: _private.0.List.triplewise_iff_getElem.match_1, List.cons, GetElem.getElem, List.triplewise_iff_getElem._proof_4, List.triplewise_iff_getElem._proof_2, And.intro, Iff.intro
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  (∀ (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 ⋯)
        (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)
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length + 1
hh :
  ∀ (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)
ht :
  ∀ (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)
⊢ 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)

Tactic:
grind
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ 0 < i + 1

Tactic:
lia
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ i + 1 < j + 1

Tactic:
lia
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j : Nat
hi : i < tail.length
hj : j < tail.length
hij : i < j
⊢ j + 1 < tail.length + 1

Tactic:
lia
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
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)

Tactic:
simpa using h 0 (i + 1) (j + 1) (by lia) (by lia) (by lia)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ i + 1 < j + 1

Tactic:
lia
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ j + 1 < k + 1

Tactic:
lia
-- Module: Mathlib.Data.List.Triplewise
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)
h :
  ∀ (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 ⋯)
      (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)
i j k : Nat
hij : i < j
hjk : j < k
hk : k < tail.length
⊢ k + 1 < tail.length + 1

Tactic:
lia