[GOAL]
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
[PROOFSTEP]
induction x using Fin.consInduction generalizing n with
| h0 =>
  cases n
  · simp
  · simp [eq_comm]
| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
[PROOFSTEP]
induction x using Fin.consInduction generalizing n with
| h0 =>
  cases n
  · simp
  · simp [eq_comm]
| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
case h0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i : Fin 0, Fin.elim0 i = n
[PROOFSTEP]

| h0 =>
  cases n
  · simp
  · simp [eq_comm]
[GOAL]
case h0
k n : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 n ↔ ∑ i : Fin 0, Fin.elim0 i = n
[PROOFSTEP]
cases n
[GOAL]
case h0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 Nat.zero ↔ ∑ i : Fin 0, Fin.elim0 i = Nat.zero
[PROOFSTEP]
simp
[GOAL]
case h0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (Nat.succ n✝) ↔ ∑ i : Fin 0, Fin.elim0 i = Nat.succ n✝
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i : Fin (n✝ + 1), Fin.cons x₀ x i = n
[PROOFSTEP]

| h x₀ x ih =>
  simp_rw [Fin.sum_cons]
  rw [antidiagonalTuple]
    -- porting note: simp_rw doesn't use the equation lemma properly
  simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
    @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
    exists_eq_right]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i : Fin (n✝ + 1), Fin.cons x₀ x i = n
[PROOFSTEP]
simp_rw [Fin.sum_cons]
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ x₀ + ∑ i : Fin n✝, x i = n
[PROOFSTEP]
rw [antidiagonalTuple]
  -- porting note: simp_rw doesn't use the equation lemma properly
[GOAL]
case h
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i : Fin n✝, x i = n
n : ℕ
⊢ (Fin.cons x₀ x ∈
      List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple n✝ ni.snd)) ↔
    x₀ + ∑ i : Fin n✝, x i = n
[PROOFSTEP]
simp_rw [List.mem_bind, List.mem_map, List.Nat.mem_antidiagonal, Fin.cons_eq_cons, exists_eq_right_right, ih,
  @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _), ← Prod.mk.inj_iff (a₁ := Prod.fst _), Prod.mk.eta,
  exists_eq_right]
[GOAL]
k n : ℕ
⊢ Nodup (antidiagonalTuple k n)
[PROOFSTEP]
induction' k with k ih generalizing n
[GOAL]
case zero
n✝ n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero n)
[PROOFSTEP]
cases n
[GOAL]
case zero.zero
n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case zero.succ
n n✝ : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero (Nat.succ n✝))
[PROOFSTEP]
simp [eq_comm]
[GOAL]
case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Nodup (antidiagonalTuple (Nat.succ k) n)
[PROOFSTEP]
simp_rw [antidiagonalTuple, List.nodup_bind]
[GOAL]
case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ (∀ (x : ℕ × ℕ), x ∈ antidiagonal n → Nodup (map (fun x_1 => Fin.cons x.fst x_1) (antidiagonalTuple k x.snd))) ∧
    Pairwise
      (fun a b =>
        Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
          (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
      (antidiagonal n)
[PROOFSTEP]
constructor
[GOAL]
case succ.left
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ ∀ (x : ℕ × ℕ), x ∈ antidiagonal n → Nodup (map (fun x_1 => Fin.cons x.fst x_1) (antidiagonalTuple k x.snd))
[PROOFSTEP]
intro i _
[GOAL]
case succ.left
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ Nodup (map (fun x => Fin.cons i.fst x) (antidiagonalTuple k i.snd))
[PROOFSTEP]
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)
[GOAL]
case succ.right
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case succ.right.zero
n k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal Nat.zero)
[PROOFSTEP]
exact List.pairwise_singleton _ _
[GOAL]
case succ.right.succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal (Nat.succ n))
[PROOFSTEP]
rw [List.Nat.antidiagonal_succ]
[GOAL]
case succ.right.succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n))
[PROOFSTEP]
refine' List.Pairwise.cons (fun a ha x hx₁ hx₂ => _) (n_ih.map _ fun a b h x hx₁ hx₂ => _)
[GOAL]
case succ.right.succ.refine'_1
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
ha : a ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (Nat.succ k) → ℕ
hx₁ : x ∈ map (fun x => Fin.cons (0, n + 1).fst x) (antidiagonalTuple k (0, n + 1).snd)
hx₂ : x ∈ map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd)
⊢ False
[PROOFSTEP]
rw [List.mem_map] at hx₁ hx₂ ha 
[GOAL]
case succ.right.succ.refine'_1
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
ha : ∃ a_1, a_1 ∈ antidiagonal n ∧ Prod.map Nat.succ id a_1 = a
x : Fin (Nat.succ k) → ℕ
hx₁ : ∃ a, a ∈ antidiagonalTuple k (0, n + 1).snd ∧ Fin.cons (0, n + 1).fst a = x
hx₂ : ∃ a_1, a_1 ∈ antidiagonalTuple k a.snd ∧ Fin.cons a.fst a_1 = x
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
[GOAL]
case succ.right.succ.refine'_1.intro.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).fst x₂ = Fin.cons (0, n + 1).fst x₁
⊢ False
[PROOFSTEP]
rw [Fin.cons_eq_cons] at h 
[GOAL]
case succ.right.succ.refine'_1.intro.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : (Prod.map Nat.succ id a).fst = (0, n + 1).fst ∧ x₂ = x₁
⊢ False
[PROOFSTEP]
injection h.1
[GOAL]
case succ.right.succ.refine'_2
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x : Fin (Nat.succ k) → ℕ
hx₁ : x ∈ map (fun x => Fin.cons (Prod.map Nat.succ id a).fst x) (antidiagonalTuple k (Prod.map Nat.succ id a).snd)
hx₂ : x ∈ map (fun x => Fin.cons (Prod.map Nat.succ id b).fst x) (antidiagonalTuple k (Prod.map Nat.succ id b).snd)
⊢ False
[PROOFSTEP]
rw [List.mem_map] at hx₁ hx₂ 
[GOAL]
case succ.right.succ.refine'_2
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x : Fin (Nat.succ k) → ℕ
hx₁ : ∃ a_1, a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd ∧ Fin.cons (Prod.map Nat.succ id a).fst a_1 = x
hx₂ : ∃ a, a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd ∧ Fin.cons (Prod.map Nat.succ id b).fst a = x
⊢ False
[PROOFSTEP]
obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : Fin.cons (Prod.map Nat.succ id b).fst x₂ = Fin.cons (Prod.map Nat.succ id a).fst x₁
⊢ False
[PROOFSTEP]
dsimp at h₁₂ 
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : Fin.cons (Nat.succ b.fst) x₂ = Fin.cons (Nat.succ a.fst) x₁
⊢ False
[PROOFSTEP]
rw [Fin.cons_eq_cons, Nat.succ_inj'] at h₁₂ 
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst ∧ x₂ = x₁
⊢ False
[PROOFSTEP]
obtain ⟨h₁₂, rfl⟩ := h₁₂
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
⊢ False
[PROOFSTEP]
rw [h₁₂] at h 
[GOAL]
case succ.right.succ.refine'_2.intro.intro.intro.intro.intro
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
n_ih :
  Pairwise
    (fun a b =>
      Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
        (map (fun x => Fin.cons b.fst x) (antidiagonalTuple k b.snd)))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  Disjoint (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k a.snd))
    (map (fun x => Fin.cons a.fst x) (antidiagonalTuple k b.snd))
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).snd
h₁₂ : b.fst = a.fst
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).snd
⊢ False
[PROOFSTEP]
exact h (List.mem_map_of_mem _ hx₁) (List.mem_map_of_mem _ hx₂)
[GOAL]
k : ℕ
⊢ antidiagonalTuple (k + 1) 0 = [0]
[PROOFSTEP]
rw [antidiagonalTuple, antidiagonal_zero, List.bind_singleton, antidiagonalTuple_zero_right k, List.map_singleton]
[GOAL]
k : ℕ
⊢ [Fin.cons (0, 0).fst 0] = [0]
[PROOFSTEP]
exact congr_arg (fun x => [x]) Matrix.cons_zero_zero
[GOAL]
n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]
[PROOFSTEP]
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton, tsub_self,
  List.append_bind, List.bind_singleton, List.map_bind]
[GOAL]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
[PROOFSTEP]
conv_rhs => rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
| [![n]]
[PROOFSTEP]
rw [← List.nil_append [![n]]]
[GOAL]
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]
[PROOFSTEP]
congr 1
[GOAL]
case e_a
n : ℕ
⊢ (List.bind (range n) fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) = []
[PROOFSTEP]
simp_rw [List.bind_eq_nil, List.mem_range, List.map_eq_nil]
[GOAL]
case e_a
n : ℕ
⊢ ∀ (x : ℕ), x < n → antidiagonalTuple 0 (n - x) = []
[PROOFSTEP]
intro x hx
[GOAL]
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
[PROOFSTEP]
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx
[GOAL]
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]
[GOAL]
n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
rw [antidiagonalTuple]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => map (fun x => Fin.cons ni.fst x) (antidiagonalTuple 1 ni.snd)) =
    map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
simp_rw [antidiagonalTuple_one, List.map_singleton]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) = map (fun i => ![i.fst, i.snd]) (antidiagonal n)
[PROOFSTEP]
rw [List.map_eq_bind]
[GOAL]
n : ℕ
⊢ (List.bind (antidiagonal n) fun ni => [Fin.cons ni.fst ![ni.snd]]) =
    List.bind (antidiagonal n) fun x => [![x.fst, x.snd]]
[PROOFSTEP]
rfl
[GOAL]
k n : ℕ
⊢ Pairwise (Pi.Lex (fun x x_1 => x < x_1) fun x x x_1 => x < x_1) (antidiagonalTuple (k + 1) n)
[PROOFSTEP]
simp_rw [antidiagonalTuple, List.pairwise_bind, List.pairwise_map, List.mem_map, forall_exists_index, and_imp,
  forall_apply_eq_imp_iff₂]
[GOAL]
k n : ℕ
⊢ (∀ (a : ℕ × ℕ),
      a ∈ antidiagonal n →
        Pairwise
          (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a.fst a_2) (Fin.cons a.fst b))
          (antidiagonalTuple (Nat.add k 0) a.snd)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.fst a) (Fin.cons a₂.fst a_2))
      (antidiagonal n)
[PROOFSTEP]
simp only [mem_antidiagonal, Prod.forall, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a_2 b => Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a a_2) (Fin.cons a b))
          (antidiagonalTuple (Nat.add k 0) b)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                Pi.Lex (fun x x_1 => x < x_1) (fun x x x_1 => x < x_1) (Fin.cons a₁.fst a) (Fin.cons a₂.fst a_2))
      (antidiagonal n)
[PROOFSTEP]
simp only [Fin.pi_lex_lt_cons_cons, eq_self_iff_true, true_and_iff, lt_self_iff_false, false_or_iff]
[GOAL]
k n : ℕ
⊢ (∀ (a b : ℕ),
      a + b = n →
        Pairwise (fun a b => Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a b)
          (antidiagonalTuple (Nat.add k 0) b)) ∧
    Pairwise
      (fun a₁ a₂ =>
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
                a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
      (antidiagonal n)
[PROOFSTEP]
refine' ⟨fun _ _ _ => antidiagonalTuple_pairwise_pi_lex k _, _⟩
[GOAL]
k n : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal Nat.zero)
[PROOFSTEP]
rw [antidiagonal_zero]
[GOAL]
case zero
k : ℕ
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    [(0, 0)]
[PROOFSTEP]
exact List.pairwise_singleton _ _
[GOAL]
case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal (Nat.succ n))
[PROOFSTEP]
rw [antidiagonal_succ, List.pairwise_cons, List.pairwise_map]
[GOAL]
case succ
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ (∀ (a' : ℕ × ℕ),
      a' ∈ map (Prod.map Nat.succ id) (antidiagonal n) →
        ∀ (a : Fin (Nat.add k 0) → ℕ),
          a ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd →
            ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
              a_2 ∈ antidiagonalTuple (Nat.add k 0) a'.snd →
                (0, n + 1).fst < a'.fst ∨
                  (0, n + 1).fst = a'.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2) ∧
    Pairwise
      (fun a b =>
        ∀ (a_1 : Fin (Nat.add k 0) → ℕ),
          a_1 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id a).snd →
            ∀ (a_3 : Fin (Nat.add k 0) → ℕ),
              a_3 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id b).snd →
                (Prod.map Nat.succ id a).fst < (Prod.map Nat.succ id b).fst ∨
                  (Prod.map Nat.succ id a).fst = (Prod.map Nat.succ id b).fst ∧
                    Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
      (antidiagonal n)
[PROOFSTEP]
refine' ⟨fun p hp x hx y hy => _, _⟩
[GOAL]
case succ.refine'_1
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
p : ℕ × ℕ
hp : p ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
hy : y ∈ antidiagonalTuple (Nat.add k 0) p.snd
⊢ (0, n + 1).fst < p.fst ∨ (0, n + 1).fst = p.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
rw [List.mem_map, Prod.exists] at hp 
[GOAL]
case succ.refine'_1
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
p : ℕ × ℕ
hp : ∃ a b, (a, b) ∈ antidiagonal n ∧ Prod.map Nat.succ id (a, b) = p
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
hy : y ∈ antidiagonalTuple (Nat.add k 0) p.snd
⊢ (0, n + 1).fst < p.fst ∨ (0, n + 1).fst = p.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
obtain ⟨a, b, _, rfl : (Nat.succ a, b) = p⟩ := hp
[GOAL]
case succ.refine'_1.intro.intro.intro
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
x : Fin (Nat.add k 0) → ℕ
hx : x ∈ antidiagonalTuple (Nat.add k 0) (0, n + 1).snd
y : Fin (Nat.add k 0) → ℕ
a b : ℕ
left✝ : (a, b) ∈ antidiagonal n
hy : y ∈ antidiagonalTuple (Nat.add k 0) (Nat.succ a, b).snd
⊢ (0, n + 1).fst < (Nat.succ a, b).fst ∨
    (0, n + 1).fst = (Nat.succ a, b).fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) x y
[PROOFSTEP]
exact Or.inl (Nat.zero_lt_succ _)
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin (Nat.add k 0) → ℕ),
        a_1 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id a).snd →
          ∀ (a_3 : Fin (Nat.add k 0) → ℕ),
            a_3 ∈ antidiagonalTuple (Nat.add k 0) (Prod.map Nat.succ id b).snd →
              (Prod.map Nat.succ id a).fst < (Prod.map Nat.succ id b).fst ∨
                (Prod.map Nat.succ id a).fst = (Prod.map Nat.succ id b).fst ∧
                  Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
dsimp
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin k → ℕ),
        a_1 ∈ antidiagonalTuple k a.snd →
          ∀ (a_3 : Fin k → ℕ),
            a_3 ∈ antidiagonalTuple k b.snd →
              Nat.succ a.fst < Nat.succ b.fst ∨
                Nat.succ a.fst = Nat.succ b.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
simp_rw [Nat.succ_inj', Nat.succ_lt_succ_iff]
[GOAL]
case succ.refine'_2
k n : ℕ
n_ih :
  Pairwise
    (fun a₁ a₂ =>
      ∀ (a : Fin (Nat.add k 0) → ℕ),
        a ∈ antidiagonalTuple (Nat.add k 0) a₁.snd →
          ∀ (a_2 : Fin (Nat.add k 0) → ℕ),
            a_2 ∈ antidiagonalTuple (Nat.add k 0) a₂.snd →
              a₁.fst < a₂.fst ∨ a₁.fst = a₂.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a a_2)
    (antidiagonal n)
⊢ Pairwise
    (fun a b =>
      ∀ (a_1 : Fin k → ℕ),
        a_1 ∈ antidiagonalTuple k a.snd →
          ∀ (a_3 : Fin k → ℕ),
            a_3 ∈ antidiagonalTuple k b.snd →
              a.fst < b.fst ∨ a.fst = b.fst ∧ Pi.Lex (fun x x_1 => x < x_1) (fun i x x_1 => x < x_1) a_1 a_3)
    (antidiagonal n)
[PROOFSTEP]
exact n_ih
