-- 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)
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)
      (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)
cons₁ :
  ∀
    (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)
⊢ ((∀ (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)
have cons₂ : ∀
  (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 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))
  (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)
Tactic: refine ⟨fun ⟨hh, ht⟩ i j k hij hjk hk ↦ ?_,
            fun h ↦ ⟨fun i j hi hj hij ↦ ?_, fun i j k hij hjk hk ↦ ?_⟩⟩