awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
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)
⊢ 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)

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

Premises used: and_imp, forall_exists_index, List.pairwise_map, List.Nat.antidiagonalTuple, List.pairwise_flatMap, List.mem_map, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
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)
⊢ (∀ 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 only [mem_antidiagonal, Prod.forall]

Premises used: List.Nat.mem_antidiagonal, Prod.forall
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
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)
⊢ (∀ (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 [Fin.pi_lex_lt_cons_cons, true_and, lt_self_iff_false,
      false_or]

Premises used: false_or, Fin.pi_lex_lt_cons_cons, lt_self_iff_false, true_and
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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)

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

Premises used: And.intro
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
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)
⊢ (∀ (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:
refine ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, ?_⟩
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    [(0, 0)]

Tactic:
List.pairwise_singleton _ _

Premises used: List.pairwise_singleton
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
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 (i : Fin k) ↦ ℕ) (fun (x1 x2 : Fin k) ↦ x1 < x2) (fun (i : Fin k) (x1 x2 : ℕ) ↦ x1 < x2)
                a a_2)
    [(0, 0)]

Tactic:
exact List.pairwise_singleton _ _

Premises used: List.pairwise_singleton
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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)
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))
⊢ 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:
simp
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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)
⊢ (∀ (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:
grind
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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)
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))
⊢ 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:
induction n with
    | zero =>
      rw [antidiagonal_zero]
      exact List.pairwise_singleton _ _
    | succ n n_ih =>
      simp
      grind

Premises used: List.pairwise_singleton, List.Nat.antidiagonal_zero
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
⊢ Eq (α := Multiset (Fin 0 → ℕ)) (antidiagonalTuple 0 0) {![]}

Tactic:
rfl

Premises used: Multiset.cons, Multiset.ofList, List.Nat.antidiagonalTuple, Multiset.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Multiset (Fin 0 → ℕ)) (antidiagonalTuple 0 n.succ) 0

Tactic:
rfl

Premises used: Multiset.zero, Multiset.ofList, List.Nat.antidiagonalTuple, Multiset.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n

Tactic:
List.Nat.mem_antidiagonalTuple

Premises used: Multiset.Mem, List.Nat.mem_antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
⊢ (antidiagonalTuple k n).Nodup

Tactic:
List.Nat.nodup_antidiagonalTuple _ _

Premises used: Multiset.Nodup, List.Nat.nodup_antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
⊢ antidiagonalTuple k 0 = {0}

Tactic:
congr_arg _ (List.Nat.antidiagonalTuple_zero_right k)

Premises used: Multiset.cons, List.Nat.antidiagonalTuple_zero_right, congr_arg, Multiset.ofList, Multiset.Nat.antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Multiset (Fin 1 → ℕ)) (antidiagonalTuple 1 n) {![n]}

Tactic:
congr_arg _ (List.Nat.antidiagonalTuple_one n)

Premises used: List.Nat.antidiagonalTuple_one, Multiset.cons, congr_arg, Multiset.ofList, Multiset.Nat.antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Multiset (Fin 2 → ℕ)) (antidiagonalTuple 2 n) (map (fun (i : ℕ × ℕ) ↦ ![i.1, i.2]) (antidiagonal n))

Tactic:
congr_arg _ (List.Nat.antidiagonalTuple_two n)

Premises used: List.Nat.antidiagonalTuple_two, Multiset.map, congr_arg, Multiset.Nat.antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
⊢ Eq (α := Finset (Fin 0 → ℕ)) (antidiagonalTuple 0 0) {![]}

Tactic:
rfl

Premises used: Finset.Nat.antidiagonalTuple, Multiset.cons, Multiset.ofList, List.Nat.antidiagonalTuple, Multiset.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin 0 → ℕ)) (antidiagonalTuple 0 n.succ) ∅

Tactic:
rfl

Premises used: Finset.Nat.antidiagonalTuple, Multiset.zero, Finset.empty, Multiset.ofList, List.Nat.antidiagonalTuple, Multiset.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n

Tactic:
List.Nat.mem_antidiagonalTuple

Premises used: Set.Mem, setOf, Multiset.Mem, List.Nat.mem_antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
⊢ antidiagonalTuple k 0 = {0}

Tactic:
Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_zero_right k)

Premises used: Multiset.Nat.antidiagonalTuple_zero_right, Finset.eq_of_veq
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := Finset (Fin 1 → ℕ)) (antidiagonalTuple 1 n) {![n]}

Tactic:
Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_one n)

Premises used: Multiset.Nat.antidiagonalTuple_one, Finset.eq_of_veq
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ antidiagonalTuple 2 n =
    map (Equiv.toEmbedding (Equiv.symm (piFinTwoEquiv fun (x : Fin 2) ↦ ℕ))) (@antidiagonal _ Nat.instAddMonoid _ n)

Tactic:
Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_two n)

Premises used: Finset.eq_of_veq, Multiset.Nat.antidiagonalTuple_two
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 1)
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)
⊢ seq f v i = f i (v i)

Tactic:
simp_rw [seq, seq_eq]

Premises used: FinVec.seq
-- Module: Mathlib.Data.Fin.Tuple.Reflection
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)

Tactic:
i.cases ?_ fun i => ?_

Premises used: Fin.cases
-- Module: Mathlib.Data.Fin.Tuple.Reflection
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)
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)
⊢ Matrix.vecCons (f 0 (v 0)) (fun (i : Fin n) ↦ Matrix.vecTail f i (Matrix.vecTail v i)) i = f i (v i)

Tactic:
refine i.cases ?_ fun i => ?_
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i : Fin (n + 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:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
β : Type u_2
n : ℕ
f : Fin (n + 1) → α → β
v : Fin (n + 1) → α
i_1 : Fin (n + 1)
i : Fin n
refine_2 : Matrix.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)
⊢ 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:
rw [Matrix.cons_val_succ]

Premises used: Matrix.cons_val_succ
-- Module: Mathlib.Data.Fin.Tuple.Reflection
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.vecTail f i (Matrix.vecTail v i) = f i.succ (v i.succ)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
f₁ f₂ : α → β
a₁ a₂ : α
⊢ seq ![f₁, f₂] ![a₁, a₂] = ![f₁ a₁, f₂ a₂]

Tactic:
rfl

Premises used: Eq.mpr, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, FinVec.seq, Matrix.vecTail, Matrix.vecCons, rfl
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
β : Type u_2
f : α → β
m : ℕ
v : Fin m → α
⊢ map f v = f ∘ v

Tactic:
seq_eq _ _

Premises used: FinVec.map, FinVec.seq_eq
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
f : α → β
a₁ a₂ : α
⊢ f ∘ ![a₁, a₂] = ![f a₁, f a₂]

Tactic:
(map_eq _ _).symm

Premises used: Eq.mpr, FinVec.map, Fin.cons, Fin.induction.go, Fin.induction, FinVec.map_eq, Fin.cases, FinVec.seq, Eq.symm, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
m : ℕ
v : Fin m → α
⊢ etaExpand v = v

Tactic:
map_eq id v

Premises used: FinVec.etaExpand, id, FinVec.map_eq
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
a : Fin 2 → α
⊢ a = ![a 0, a 1]

Tactic:
(etaExpand_eq _).symm

Premises used: FinVec.etaExpand_eq, FinVec.etaExpand, FinVec.map, Fin.succ, Fin.ofNat, FinVec.seq, Eq.symm, Matrix.vecTail
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
simp : P ![] ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))
⊢ Forall P ↔ ∀ (x : Fin 0 → α), P x

Tactic:
simp only [Forall, Fin.forall_fin_zero_pi]

Premises used: FinVec.Forall, Fin.forall_fin_zero_pi
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P ![] ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Forall P ↔ ∀ (x : Fin n.succ → α), P x

Tactic:
simp only [Forall, forall_iff, Fin.forall_fin_succ_pi, Matrix.vecCons]

Premises used: FinVec.Forall, Fin.forall_fin_succ_pi, Matrix.vecCons
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
P : (Fin 2 → α) → Prop
⊢ (∀ (f : Fin 2 → α), P f) ↔ ∀ (a₀ a₁ : α), P ![a₀, a₁]

Tactic:
(forall_iff _).symm

Premises used: FinVec.Forall, FinVec.forall_iff, Iff.symm
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
simp : P Fin.elim0 ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))
⊢ Exists P ↔ ∃ (x : Fin 0 → α), P x

Tactic:
simp only [Exists, Fin.exists_fin_zero_pi, Matrix.vecEmpty]

Premises used: Fin.exists_fin_zero_pi, FinVec.Exists, Matrix.vecEmpty
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
P : (Fin 0 → α) → Prop
⊢ P Fin.elim0 ↔ P (finZeroElim (α := fun (i : Fin 0) ↦ α))

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
α : Type u_1
n : ℕ
P : (Fin n.succ → α) → Prop
⊢ Exists P ↔ ∃ (x : Fin n.succ → α), P x

Tactic:
simp only [Exists, exists_iff, Fin.exists_fin_succ_pi, Matrix.vecCons]

Premises used: Fin.exists_fin_succ_pi, FinVec.Exists, Matrix.vecCons
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
P : (Fin 2 → α) → Prop
⊢ (∃ (f : Fin 2 → α), P f) ↔ ∃ (a₀ : α) (a₁ : α), P ![a₀, a₁]

Tactic:
(exists_iff _).symm

Premises used: FinVec.exists_iff, FinVec.Exists, Iff.symm
-- Module: Mathlib.Data.Fin.Tuple.Reflection
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))
rw₂ 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))
⊢ prod a = ∏ i : Fin (n + 2), a i

Tactic:
rw [Fin.prod_univ_castSucc, prod, prod_eq]

Premises used: Fin.prod_univ_castSucc, FinVec.prod
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
inst : CommMonoid α
a : Fin 3 → α
⊢ ∏ i : Fin 3, a i = a 0 * a 1 * a 2

Tactic:
(prod_eq _).symm

Premises used: FinVec.prod_eq, Fin.ofNat, FinVec.prod, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Reflection
Goal:
m : ℕ
α : Type u_1
β : Type u_2
inst : AddCommMonoid α
a : Fin 3 → α
⊢ ∑ i : Fin 3, a i = a 0 + a 1 + a 2

Tactic:
(sum_eq _).symm

Premises used: Fin.ofNat, FinVec.sum_eq, FinVec.sum, Eq.symm
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
rw : Finset.card (α := Fin n) Finset.univ = n
H : Function.Injective.{1, u_1 + 1} (β := Lex (α × Fin n)) fun (i : Fin n) ↦ (f i, i)
⊢ (graph f).card = n

Tactic:
rw [graph, Finset.card_image_of_injective]

Premises used: Tuple.graph, Finset.card_image_of_injective
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Finset.card (α := Fin n) Finset.univ = n

Tactic:
Finset.card_fin _

Premises used: Finset.card_fin
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
⊢ Finset.card (α := Fin n) Finset.univ = n

Tactic:
exact Finset.card_fin _

Premises used: Finset.card_fin
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
a₁ : Fin n
H :
  ∀ ⦃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₂
⊢ ∀ ⦃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₂

Tactic:
_
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
a₁ a₂ : Fin n
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₂
⊢ 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₂

Tactic:
rw [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
a₁ a₂ : Fin n
⊢ 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:
simp
-- Module: Mathlib.Data.Fin.Tuple.Sort
Goal:
n : ℕ
α : Type u_1
inst : LinearOrder α
f : Fin n → α
i : Fin n
⊢ (f i, i) ∈ graph f

Tactic:
simp [graph]

Premises used: Tuple.graph