awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
succ :
  ∀ (a : ℕ × ℕ) (ha : a ∈ map (Prod.map Nat.succ id) (antidiagonal n)) (x : Fin (k + 1) → ℕ)
    (hx₁ :
      Membership.mem (γ := List (Fin (k + 1) → ℕ))
        ((fun (ni : ℕ × ℕ) ↦
            (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x)
                (antidiagonalTuple k ni.2) :
              List (Fin (k + 1) → ℕ)))
          (0, n + 1))
        x)
    (hx₂ :
      Membership.mem (γ := List (Fin (k + 1) → ℕ))
        ((fun (ni : ℕ × ℕ) ↦
            (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x)
                (antidiagonalTuple k ni.2) :
              List (Fin (k + 1) → ℕ)))
          a)
        x),
    False
succ₁ :
  ∀ (a b : ℕ × ℕ)
    (h :
      Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
        a b)
    (x : Fin (k + 1) → ℕ)
    (hx₁ :
      Membership.mem (γ := List (Fin (k + 1) → ℕ))
        ((fun (ni : ℕ × ℕ) ↦
            (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x)
                (antidiagonalTuple k ni.2) :
              List (Fin (k + 1) → ℕ)))
          (Prod.map Nat.succ id a))
        x)
    (hx₂ :
      Membership.mem (γ := List (Fin (k + 1) → ℕ))
        ((fun (ni : ℕ × ℕ) ↦
            (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x)
                (antidiagonalTuple k ni.2) :
              List (Fin (k + 1) → ℕ)))
          (Prod.map Nat.succ id b))
        x),
    False
⊢ Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n))

Tactic:
refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)

Premises used: List.Pairwise.cons, List.Pairwise.map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
ha : a ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (k + 1) → ℕ
hx₁ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      (0, n + 1))
    x
hx₂ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      a)
    x
succ :
  ∀ (ha : ∃ a_1 ∈ antidiagonal n, Prod.map Nat.succ id a_1 = a) (x : Fin (k + 1) → ℕ)
    (hx₁ : ∃ a ∈ antidiagonalTuple k (0, n + 1).2, Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, n + 1).1 a = x)
    (hx₂ : ∃ a_1 ∈ antidiagonalTuple k a.2, Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 a_1 = x), False
⊢ False

Tactic:
rw [List.mem_map] at hx₁ hx₂ ha

Premises used: List.mem_map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
ha : ∃ a_1 ∈ antidiagonal n, Prod.map Nat.succ id a_1 = a
x : Fin (k + 1) → ℕ
hx₁ : ∃ a ∈ antidiagonalTuple k (0, n + 1).2, Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, n + 1).1 a = x
hx₂ : ∃ a_1 ∈ antidiagonalTuple k a.2, Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 a_1 = x
succ :
  ∀ (a : ℕ × ℕ) (x₁ x₂ : (i : Fin k) → ℕ)
    (h :
      Eq (α := Fin (k + 1) → ℕ) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 x₂)
        (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, n + 1).1 x₁)),
    False
⊢ False

Tactic:
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂

Premises used: rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : (i : Fin k) → ℕ
h :
  Eq (α := Fin (k + 1) → ℕ) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 x₂)
    (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, n + 1).1 x₁)
⊢ (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁

Tactic:
rw [Fin.cons_inj] at h

Premises used: Fin.cons_inj
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : (i : Fin k) → ℕ
h : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False

Tactic:
injection h.1

Premises used: And.left
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x : Fin (k + 1) → ℕ
hx₁ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      (Prod.map Nat.succ id a))
    x
hx₂ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      (Prod.map Nat.succ id b))
    x
⊢ ∃ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2,
    Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 a_1 = x

Tactic:
rw [List.mem_map] at hx₁ hx₂

Premises used: List.mem_map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x : Fin (k + 1) → ℕ
hx₁ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      (Prod.map Nat.succ id a))
    x
hx₂ :
  Membership.mem (γ := List (Fin (k + 1) → ℕ))
    ((fun (ni : ℕ × ℕ) ↦
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2) :
          List (Fin (k + 1) → ℕ)))
      (Prod.map Nat.succ id b))
    x
hx₃ :
  ∃ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2,
    Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 a_1 = x
⊢ ∃ a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2,
    Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id b).1 a = x

Tactic:
rw [List.mem_map] at hx₁ hx₂

Premises used: List.mem_map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x : Fin (k + 1) → ℕ
hx₁ :
  ∃ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2,
    Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 a_1 = x
hx₂ :
  ∃ a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2,
    Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id b).1 a = x
succ :
  ∀ (x₁ : (i : Fin k) → ℕ) (hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2) (x₂ : (i : Fin k) → ℕ)
    (hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2)
    (h₁₂ :
      Eq (α := Fin (k + 1) → ℕ) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id b).1 x₂)
        (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (Prod.map Nat.succ id a).1 x₁)),
    False
⊢ False

Tactic:
obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂

Premises used: rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x₁ : (i : Fin k) → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ :
  Eq (α := Fin (k + 1) → ℕ) (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (b.1 + 1) x₂)
    (Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (a.1 + 1) x₁)
⊢ b.1 = a.1 ∧ x₂ = x₁

Tactic:
rw [Fin.cons_inj, Nat.succ_inj] at h₁₂

Premises used: Nat.succ_inj, Fin.cons_inj
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x₁ : (i : Fin k) → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ b.1 = a.1

Tactic:
obtain ⟨h₁₂, rfl⟩ := h₁₂

Premises used: rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x₁ : (i : Fin k) → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1 ∧ x₂ = x₁
h₁₃ : b.1 = a.1
⊢ x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2

Tactic:
obtain ⟨h₁₂, rfl⟩ := h₁₂

Premises used: rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint
    (fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    a b
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
succ :
  ∀
    (h :
      Disjoint (α := Fin (k + 1) → ℕ)
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k a.2))
        (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k b.2)))
    (x₂ : (i : Fin k) → ℕ) (hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2) (h₁₂ : b.1 = a.1)
    (hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2), False
⊢ False

Tactic:
rw [Function.onFun, h₁₂] at h

Premises used: Function.onFun
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (α := Fin (k + 1) → ℕ)
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k a.2))
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k b.2))
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

Tactic:
h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

Premises used: List.mem_map_of_mem
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (α := Fin (k + 1) → ℕ)
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k a.2))
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) a.1 x) (antidiagonalTuple k b.2))
x₂ : (i : Fin k) → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

Tactic:
exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

Premises used: List.mem_map_of_mem
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
succ :
  Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal 0)
succ₁ :
  ∀ (n : ℕ)
    (n_ih :
      Pairwise
        (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
        (antidiagonal n)),
    Pairwise
      (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
        map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
      (antidiagonal (n + 1))
⊢ Pairwise
    (Function.onFun (β := List (Fin (k + 1) → ℕ)) Disjoint fun (ni : ℕ × ℕ) ↦
      map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)

Tactic:
induction n with
  | zero => exact List.pairwise_singleton _ _
  | succ n n_ih =>
    rw [List.Nat.antidiagonal_succ]
    refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
    · rw [List.mem_map] at hx₁ hx₂ ha
      obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
      rw [Fin.cons_inj] at h
      injection h.1
    · rw [List.mem_map] at hx₁ hx₂
      obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
      dsimp at h₁₂
      rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
      obtain ⟨h₁₂, rfl⟩ := h₁₂
      rw [Function.onFun, h₁₂] at h
      exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

Premises used: Nat.succ_inj, Fin.cons_inj, Function.onFun, List.pairwise_singleton, List.Nat.antidiagonal_succ, List.mem_map, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
rw : Eq (α := List (Fin (k + 1) → ℕ)) [Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, 0).1 0] [0]
⊢ Eq (α := List (Fin (k + 1) → ℕ)) (antidiagonalTuple (k + 1) 0) [0]

Tactic:
rw [antidiagonalTuple, antidiagonal_zero, List.flatMap_singleton,
      antidiagonalTuple_zero_right k, List.map_singleton]

Premises used: List.map_singleton, List.Nat.antidiagonalTuple, List.flatMap_singleton, List.Nat.antidiagonal_zero
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
⊢ Eq (α := List (Fin (k + 1) → ℕ)) [Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, 0).1 0] [0]

Tactic:
congr_arg (fun x => [x]) Matrix.cons_zero_zero

Premises used: List.cons, congr_arg, Matrix.cons_zero_zero, List.nil
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
⊢ Eq (α := List (Fin (k + 1) → ℕ)) [Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) (0, 0).1 0] [0]

Tactic:
exact congr_arg (fun x => [x]) Matrix.cons_zero_zero

Premises used: List.cons, congr_arg, Matrix.cons_zero_zero, List.nil
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
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]]
⊢ antidiagonalTuple 1 n = [![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]

Premises used: List.map_singleton, Nat.sub_self, List.flatMap_map, List.Nat.antidiagonalTuple, List.map_append, List.flatMap_singleton, List.flatMap_append, List.Nat.antidiagonal, List.range_succ
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
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))
    []
⊢ 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:
congr 1
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
e_a : ∀ x < n, Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (n - x)) []
⊢ 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:
simp_rw [List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff]

Premises used: List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n x : ℕ
hx : x < n
e_a : ∀ (m : ℕ) (hx : x < x + m + 1), Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (n - x)) []

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx

Premises used: Nat.exists_eq_add_of_lt, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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)) []
e_a₂ e_a₃ : Eq (α := List ((i : Fin 0) → ℕ)) [] []
⊢ Eq (α := List ((i : Fin 0) → ℕ)) (antidiagonalTuple 0 (x + m + 1 - x)) []

Tactic:
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]

Premises used: add_assoc, add_tsub_cancel_left, List.Nat.antidiagonalTuple_zero_succ
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
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))
⊢ 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))

Tactic:
simp_rw [antidiagonalTuple_one, List.map_singleton]

Premises used: List.Nat.antidiagonalTuple_one, List.map_singleton
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
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))
⊢ 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:
rw [List.map_eq_flatMap]

Premises used: List.map_eq_flatMap
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ 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:
rfl