-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem antidiagonalTuple_pairwise_pi_lex :
    ∀ k n, (antidiagonalTuple k n).Pairwise (Pi.Lex (· < ·) @fun _ => (· < ·))
  | 0, 0 => List.pairwise_singleton _ _
  | 0, _ + 1 => List.Pairwise.nil
  | k + 1, n => by
    simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    simp only [mem_antidiagonal, Prod.forall, and_imp, forall_apply_eq_imp_iff₂]
    simp only [Fin.pi_lex_lt_cons_cons, eq_self_iff_true, true_and, lt_self_iff_false,
      false_or]
    refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩
    induction' n with n n_ih
    · rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    · rw [antidiagonal_succ, List.pairwise_cons, List.pairwise_map]
      refine ⟨fun p hp x hx y hy => ?_, ?_⟩
      · rw [List.mem_map, Prod.exists] at hp
        obtain ⟨a, b, _, rfl : (Nat.succ a, b) = p⟩ := hp
        exact Or.inl (Nat.zero_lt_succ _)
      dsimp
      simp_rw [Nat.succ_inj', Nat.succ_lt_succ_iff]
      exact n_ih

Proof state:
case succ.refine_1.intro.intro.intro
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a a_2)
    (antidiagonal n)
x : Fin k → ℕ
hx : x ∈ antidiagonalTuple k (0, n + 1).2
y : Fin k → ℕ
a b : ℕ
left✝ : (a, b) ∈ antidiagonal n
hy : y ∈ antidiagonalTuple k (a.succ, b).2
⊢ (0, n + 1).1 < (a.succ, b).1 ∨
    (0, n + 1).1 = (a.succ, b).1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) x y

Tactic:
exact Or.inl (Nat.zero_lt_succ _)

Result:
no goals

Proof state:
case succ.refine_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2,
        ∀ a_3 ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2,
          (Prod.map Nat.succ id a).1 < (Prod.map Nat.succ id b).1 ∨
            (Prod.map Nat.succ id a).1 = (Prod.map Nat.succ id b).1 ∧
              Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a_1 a_3)
    (antidiagonal n)

Tactic:
dsimp

Result:
case succ.refine_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ a_1 ∈ antidiagonalTuple k a.2,
        ∀ a_3 ∈ antidiagonalTuple k b.2,
          a.1 + 1 < b.1 + 1 ∨ a.1 + 1 = b.1 + 1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a_1 a_3)
    (antidiagonal n)

Proof state:
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          a₁.1 < a₂.1 ∨ a₁.1 = a₂.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a a_2)
    [(0, 0)]

Tactic:
exact List.pairwise_singleton _ _

Result:
no goals