-- 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:
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a_2 b => Pi.Lex (fun x1 x2 => x1 < x2) (fun x x1 x2 => x1 < x2) (Fin.cons a a_2) (Fin.cons a b))
          (antidiagonalTuple k b)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            Pi.Lex (fun x1 x2 => x1 < x2) (fun x x1 x2 => x1 < x2) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2))
      (antidiagonal n)

Tactic:
simp only [Fin.pi_lex_lt_cons_cons, eq_self_iff_true, true_and, lt_self_iff_false,
  false_or]

Result:
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a b => Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a b) (antidiagonalTuple k b)) ∧
    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)

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 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)

Tactic:
simp_rw [Nat.succ_inj', Nat.succ_lt_succ_iff]

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 < b.1 ∨ a.1 = b.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a_1 a_3)
    (antidiagonal n)

Proof state:
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a b => Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a b) (antidiagonalTuple k b)) ∧
    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)

Tactic:
refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩

Result:
k n : ℕ
⊢ 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)

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)
    (antidiagonal 0)

Tactic:
rw [antidiagonal_zero]

Result:
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)]

Proof state:
k n : ℕ
⊢ 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)

Tactic:
induction' n with n n_ih

Result:
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)
    (antidiagonal 0)

case succ
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₁ 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 + 1))

Proof state:
k n : ℕ
⊢ Pairwise (Pi.Lex (fun x1 x2 => x1 < x2) fun x x1 x2 => x1 < x2) (antidiagonalTuple (k + 1) n)

Tactic:
simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map,
  forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Result:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise (fun a_2 b => Pi.Lex (fun x1 x2 => x1 < x2) (fun x x1 x2 => x1 < x2) (Fin.cons a.1 a_2) (Fin.cons a.1 b))
        (antidiagonalTuple k a.2)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            Pi.Lex (fun x1 x2 => x1 < x2) (fun x x1 x2 => x1 < x2) (Fin.cons a₁.1 a) (Fin.cons a₂.1 a_2))
      (antidiagonal n)

Proof state:
case succ
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₁ 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 + 1))

Tactic:
rw [antidiagonal_succ, List.pairwise_cons, List.pairwise_map]

Result:
case succ
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)
⊢ (∀ a' ∈ map (Prod.map Nat.succ id) (antidiagonal n),
      ∀ a ∈ antidiagonalTuple k (0, n + 1).2,
        ∀ a_2 ∈ antidiagonalTuple k a'.2,
          (0, n + 1).1 < a'.1 ∨ (0, n + 1).1 = a'.1 ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i x1 x2 => x1 < x2) a a_2) ∧
    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)