awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k : ℕ
⊢ Eq (α := List (Fin (k + 1) → ℕ)) (antidiagonalTuple (k + 1) 0) [0]
have rw : Eq (α := List (Fin (k + 1) → ℕ)) [Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, 0).1 0] [0]
Tactic: rw [antidiagonalTuple, antidiagonal_zero, List.flatMap_singleton,
      antidiagonalTuple_zero_right k, List.map_singleton]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]
have simp_rw : HAppend.hAppend (α := List (Fin (HAdd.hAdd (α := ℕ) 0 1) → ℕ))
    (flatMap
      (fun (a : ℕ) ↦
        map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) a x)
          (antidiagonalTuple 0 (n - a)))
      (range n))
    (map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) n x)
      (antidiagonalTuple 0 0)) =
  [![n]]
Tactic: simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
    Nat.sub_self, List.flatMap_append, List.flatMap_singleton, List.flatMap_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ HAppend.hAppend (α := List (Fin (HAdd.hAdd (α := ℕ) 0 1) → ℕ))
      (flatMap
        (fun (a : ℕ) ↦
          map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) a x)
            (antidiagonalTuple 0 (n - a)))
        (range n))
      (map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) n x)
        (antidiagonalTuple 0 0)) =
    [] ++ [![n]]
have e_a : Eq (α := List (Fin (HAdd.hAdd (α := ℕ) 0 1) → ℕ))
  (flatMap
    (fun (a : ℕ) ↦
      map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) a x)
        (antidiagonalTuple 0 (n - a)))
    (range n))
  []
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Eq (α := List (Fin (HAdd.hAdd (α := ℕ) 0 1) → ℕ))
    (flatMap
      (fun (a : ℕ) ↦
        map (fun (x : (i : Fin 0) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 0 1)) ↦ ℕ) a x)
          (antidiagonalTuple 0 (n - a)))
      (range n))
    []
have e_a : ∀ x < n, Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (n - x)) []
Tactic: simp_rw [List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n x : ℕ
hx : x < n
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (n - x)) []
have e_a : ∀ (m : ℕ) (hx : x < x + m + 1), Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []
Tactic: obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
Cleared hypotheses: n, hx
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
x m : ℕ
hx : x < x + m + 1
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []
have e_a : Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + (m + 1) - x)) []
Tactic: rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
x m : ℕ
hx : x < x + m + 1
e_a : Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + (m + 1) - x)) []
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []
have e_a₁ : Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (m + 1)) []
Tactic: rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
x m : ℕ
hx : x < x + m + 1
e_a : Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + (m + 1) - x)) []
e_a₁ : Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (m + 1)) []
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []
have e_a₂ : Eq (α := List ((i : Fin 0) → ℕ)) [] []
Tactic: rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Eq (α := List (Fin 2 → ℕ))
    (flatMap
      (fun (ni : ℕ × ℕ) ↦
        map (fun (x : (i : Fin 1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℕ) ni.1 x)
          (antidiagonalTuple 1 ni.2))
      (antidiagonal n))
    (map (fun (i : ℕ × ℕ) ↦ ![i.1, i.2]) (antidiagonal n))
have simp_rw : Eq (α := List (Fin 2 → ℕ))
  (flatMap (fun (ni : ℕ × ℕ) ↦ [Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℕ) ni.1 ![ni.2]])
    (antidiagonal n))
  (map (fun (i : ℕ × ℕ) ↦ ![i.1, i.2]) (antidiagonal n))
Tactic: simp_rw [antidiagonalTuple_one, List.map_singleton]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Eq (α := List (Fin 2 → ℕ))
    (flatMap (fun (ni : ℕ × ℕ) ↦ [Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℕ) ni.1 ![ni.2]])
      (antidiagonal n))
    (map (fun (i : ℕ × ℕ) ↦ ![i.1, i.2]) (antidiagonal n))
have rw : Eq (α := List (Fin 2 → ℕ))
  (flatMap (fun (ni : ℕ × ℕ) ↦ [Fin.cons (α := fun (a : Fin (HAdd.hAdd (α := ℕ) 1 1)) ↦ ℕ) ni.1 ![ni.2]])
    (antidiagonal n))
  (flatMap (fun (x : ℕ × ℕ) ↦ [![x.1, x.2]]) (antidiagonal n))
Tactic: rw [List.map_eq_flatMap]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ Pairwise (α := (i : Fin (k + 1)) → ℕ)
    (Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2) fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦
      x1 < x2)
    (antidiagonalTuple (k + 1) n)
have simp_rw : (∀ a ∈ antidiagonal n,
    Pairwise
      (fun (a_2 b : (i : Fin k) → ℕ) ↦
        Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
          (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 a_2)
          (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) 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 (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
            (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₁.1 a)
            (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₂.1 a_2))
    (antidiagonal n)
Tactic: simp_rw [antidiagonalTuple, List.pairwise_flatMap, List.pairwise_map, List.mem_map,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ (∀ a ∈ antidiagonal n,
      Pairwise
        (fun (a_2 b : (i : Fin k) → ℕ) ↦
          Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
            (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 a_2)
            (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) 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 (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
              (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₁.1 a)
              (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₂.1 a_2))
      (antidiagonal n)
have simp : (∀ (a b : ℕ),
    a + b = n →
      Pairwise
        (fun (a_2 b : (i : Fin k) → ℕ) ↦
          Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
            (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a a_2)
            (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a b))
        (antidiagonalTuple k b)) ∧
  Pairwise
    (fun (a₁ a₂ : ℕ × ℕ) ↦
      ∀ a ∈ antidiagonalTuple k a₁.2,
        ∀ a_2 ∈ antidiagonalTuple k a₂.2,
          Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
            (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₁.1 a)
            (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₂.1 a_2))
    (antidiagonal n)
Tactic: simp only [mem_antidiagonal, Prod.forall]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise
          (fun (a_2 b : (i : Fin k) → ℕ) ↦
            Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
              (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a a_2)
              (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a b))
          (antidiagonalTuple k b)) ∧
    Pairwise
      (fun (a₁ a₂ : ℕ × ℕ) ↦
        ∀ a ∈ antidiagonalTuple k a₁.2,
          ∀ a_2 ∈ antidiagonalTuple k a₂.2,
            Pi.Lex (β := fun (a : Fin (k + 1)) ↦ ℕ) (fun (x1 x2 : Fin (k + 1)) ↦ x1 < x2)
              (fun (x : Fin (k + 1)) (x1 x2 : ℕ) ↦ x1 < x2) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₁.1 a)
              (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a₂.1 a_2))
      (antidiagonal n)
have simp : (∀ (a b : ℕ),
    a + b = n →
      Pairwise
        (fun (a b : (i : Fin k) → ℕ) ↦
          Pi.Lex (β := fun (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal n)
Tactic: simp only [Fin.pi_lex_lt_cons_cons, true_and, lt_self_iff_false,
      false_or]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise
          (fun (a b : (i : Fin k) → ℕ) ↦
            Pi.Lex (β := fun (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2)
                  (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2) a a_2)
      (antidiagonal n)
have refine : 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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2) a
              a_2)
  (antidiagonal n)
Tactic: refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal (n + 1))
have succ : (∀ (a b x x_1 : ℕ),
    x + x_1 = n →
      x + 1 = a →
        x_1 = b →
          ∀ a_4 ∈ antidiagonalTuple k (n + 1),
            ∀ a_6 ∈ antidiagonalTuple k b,
              0 < a ∨
                0 = a ∧
                  Pi.Lex (β := fun (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2)
                    (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2) a_4 a_6) ∧
  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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (map (Prod.map Nat.succ id) (antidiagonal n))
Tactic: simp
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal n)
have zero : 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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2) a
              a_2)
  (antidiagonal 0)
Tactic: induction n with
    | zero =>
      rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    | succ n n_ih =>
      simp
      grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
zero :
  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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal 0)
⊢ 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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal n)
have succ : ∀ (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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2)
                  (fun (i : Fin k) (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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    (antidiagonal (n + 1))
Tactic: induction n with
    | zero =>
      rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    | succ n n_ih =>
      simp
      grind
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ seq f v i = f i (v i)
have simp_rw : Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
Tactic: simp_rw [seq, seq_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
⊢ Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
have refine_1 : Matrix.vecCons (n := n) (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)
Tactic: refine i.cases ?_ fun i => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
refine_1 : Matrix.vecCons (n := n) (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) 0 = f 0 (v 0)
⊢ Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)
have refine_2 : ∀ (i : Fin n),
  Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i.succ = f i.succ (v i.succ)
Tactic: refine i.cases ?_ fun i => ?_
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i_1 : Fin (n + 1)
i : Fin n
⊢ Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i.succ = f i.succ (v i.succ)
have refine_2 : Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)
Tactic: rw [Matrix.cons_val_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x
have simp : P ![] ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))
Tactic: simp only [Forall, Fin.forall_fin_zero_pi]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ Exists P ↔ ∃ (x : Fin 0 → α), P x
have simp : P Fin.elim0 ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))
Tactic: simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
⊢ prod a = ∏ i : Fin (n + 2), a i
have rw : prod a = (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
Tactic: rw [Fin.prod_univ_castSucc, prod, prod_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
rw : prod a = (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
⊢ prod a = ∏ i : Fin (n + 2), a i
have rw₁ : (prod (m := n + 1) fun (i : Fin (n + 1)) ↦ a i.castSucc) * a (Fin.last (n + 1)) =
  (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
Tactic: rw [Fin.prod_univ_castSucc, prod, prod_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Reflection (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
a : Fin (n + 2) → α
rw : prod a = (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
rw₁ :
  (prod (m := n + 1) fun (i : Fin (n + 1)) ↦ a i.castSucc) * a (Fin.last (n + 1)) =
    (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
⊢ prod a = ∏ i : Fin (n + 2), a i
have rw₂ : (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1)) = (∏ i : Fin (n + 1), a i.castSucc) * a (Fin.last (n + 1))
Tactic: rw [Fin.prod_univ_castSucc, prod, prod_eq]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ (graph f).card = n
have rw : Finset.card (α := Fin n) Finset.univ = n
Tactic: rw [graph, Finset.card_image_of_injective]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
rw : Finset.card (α := Fin n) Finset.univ = n
⊢ (graph f).card = n
have H : Function.Injective.{1, u_1 + 1} (β := Lex (α × Fin n)) fun (i : Fin n) ↦ (f i, i)
Tactic: rw [graph, Finset.card_image_of_injective]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
a₁ a₂ : Fin n
⊢ Eq.{u_1 + 1} (α := Lex (α × Fin n)) ((fun (i : Fin n) ↦ (f i, i)) a₁) ((fun (i : Fin n) ↦ (f i, i)) a₂) → a₁ = a₂
have H : Eq.{u_1 + 1} (α := α) ((fun (i : Fin n) ↦ (f i, i)) a₁).1 ((fun (i : Fin n) ↦ (f i, i)) a₂).1 ∧
    Eq (α := Fin n) ((fun (i : Fin n) ↦ (f i, i)) a₁).2 ((fun (i : Fin n) ↦ (f i, i)) a₂).2 →
  a₁ = a₂
Tactic: rw [Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Monotone (α := Fin n) (f ∘ (⇑(sort f) : (a : Fin n) → Fin n))
have rw : Monotone (α := Fin n) (β := α)
  (Function.comp (β := ↥(graph f)) graph.proj (⇑(graphEquiv₂ f) : (a : Fin n) → ↥(graph f)))
Tactic: rw [self_comp_sort]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
have mp : σ = sort f → StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
mp :
  σ = sort f → StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
⊢ σ = sort f ↔ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
have mpr : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) → σ = sort f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : σ = sort f
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
have mp : StrictMono (α := Fin n) (β := ↥(graph f))
  (⇑(Equiv.trans
        (RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(graph f)) ↦ x1 ≤ x2) (graphEquiv₂ f))
        (Equiv.refl ↥(graph f))) :
    (a : Fin n) → ↥(graph f))
Tactic: rw [h, sort, Equiv.trans_assoc, Equiv.symm_trans_self]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (hypothesis)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
⊢ σ = sort f
have this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h sorry
Tactic: have := Subsingleton.elim (graphEquiv₂ f) (h.orderIsoOfSurjective _ <| Equiv.surjective _)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f))
this : graphEquiv₂ f = StrictMono.orderIsoOfSurjective (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) h ⋯
⊢ σ = sort f
have mpr : ∀ (x : Fin n), Eq (α := Fin n) ((σ : (a : Fin n) → Fin n) x : Fin n) ((sort f : (a : Fin n) → Fin n) x : Fin n)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ σ = sort f ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
have rw : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
  Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
    ∀ (i j : Fin n),
      i < j →
        f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
          LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
Tactic: rw [eq_sort_iff']
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Sort (goal)
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
σ : Equiv.Perm (Fin n)
⊢ StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)) ↔
    Monotone (α := Fin n) (f ∘ (⇑σ : (a : Fin n) → Fin n)) ∧
      ∀ (i j : Fin n),
        i < j →
          f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j) →
            LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
have refine_1 : ∀ (h : StrictMono (α := Fin n) (β := ↥(graph f)) (⇑(Equiv.trans σ (graphEquiv₁ f)) : (a : Fin n) → ↥(graph f)))
  (i j : Fin n) (hij : i < j) (hfij : f ((σ : (a : Fin n) → Fin n) i) = f ((σ : (a : Fin n) → Fin n) j)),
  LT.lt (α := Fin n) ((σ : (a : Fin n) → Fin n) i : Fin n) ((σ : (a : Fin n) → Fin n) j : Fin n)
Tactic: refine ⟨fun h => ⟨(monotone_proj f).comp h.monotone, fun i j hij hfij => ?_⟩, fun h i j hij => ?_⟩