case zero
n✝ n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero n)

case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Nodup (antidiagonalTuple (Nat.succ k) n)
k n : ℕ
⊢ Nodup (antidiagonalTuple k n)
induction' k with k ih generalizing n
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)
case succ
n✝ k : ℕ
ih : ∀ (n : ℕ), Nodup (antidiagonalTuple k n)
n : ℕ
⊢ Nodup (antidiagonalTuple (Nat.succ k) n)
simp_rw [antidiagonalTuple, List.nodup_bind]
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))

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

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))
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)
induction' n with n n_ih
case zero.zero
n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero Nat.zero)

case zero.succ
n n✝ : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero (Nat.succ n✝))
case zero
n✝ n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero n)
cases n
no goals
case zero.zero
n : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero Nat.zero)
simp
no goals
case zero.succ
n n✝ : ℕ
⊢ Nodup (antidiagonalTuple Nat.zero (Nat.succ n✝))
simp [eq_comm]
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))
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))
intro i _
no goals
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))
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)
no goals
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)
exact List.pairwise_singleton _ _
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))
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))
rw [List.Nat.antidiagonal_succ]
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

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
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))
refine' List.Pairwise.cons (fun a ha x hx₁ hx₂ => _) (n_ih.map _ fun a b h x hx₁ hx₂ => _)
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
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
rw [List.mem_map] at hx₁ hx₂ ha
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
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
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
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
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
rw [Fin.cons_eq_cons] at h
no goals
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
injection h.1
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
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
rw [List.mem_map] at hx₁ hx₂
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
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
obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
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
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
dsimp at h₁₂
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
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
rw [Fin.cons_eq_cons, Nat.succ_inj'] at h₁₂
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
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
obtain ⟨h₁₂, rfl⟩ := h₁₂
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
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
rw [h₁₂] at h
no goals
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
exact h (List.mem_map_of_mem _ hx₁) (List.mem_map_of_mem _ hx₂)