-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem nodup_antidiagonalTuple (k n : ℕ) : List.Nodup (antidiagonalTuple k n)

Proof state:
case succ.right.succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
⊢ Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons 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₂ => ?_)

Result:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons 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₁ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (0, n + 1)
hx₂ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a
⊢ False

case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id a)
hx₂ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id b)
⊢ False

Proof state:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons 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₁ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (0, n + 1)
hx₂ : x ∈ (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a
⊢ False

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

Result:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons 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 (0, n + 1).1 a = x
hx₂ : ∃ a_1 ∈ antidiagonalTuple k a.2, Fin.cons a.1 a_1 = x
⊢ False

Proof state:
case succ.right.succ.refine_2.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : Fin.cons (Prod.map Nat.succ id b).1 x₂ = Fin.cons (Prod.map Nat.succ id a).1 x₁
⊢ False

Tactic:
dsimp at h₁₂

Result:
case succ.right.succ.refine_2.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x₁ : Fin k → ℕ
hx₁ : x₁ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
x₂ : Fin k → ℕ
hx₂ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2
h₁₂ : Fin.cons (b.1 + 1) x₂ = Fin.cons (a.1 + 1) x₁
⊢ False

Proof state:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons 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 (0, n + 1).1 a = x
hx₂ : ∃ a_1 ∈ antidiagonalTuple k a.2, Fin.cons a.1 a_1 = x
⊢ False

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

Result:
case succ.right.succ.refine_1.intro.intro.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).1 x₂ = Fin.cons (0, n + 1).1 x₁
⊢ False

Proof state:
case succ.right.succ.refine_1.intro.intro.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False

Tactic:
injection h.1

Result:
no goals

Proof state:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (antidiagonalTuple (k + 1) n).Nodup

Tactic:
simp_rw [antidiagonalTuple, List.nodup_flatMap]

Result:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (∀ x ∈ antidiagonal n, (map (fun x_1 => Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup) ∧
    Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
      (antidiagonal n)

Proof state:
case zero
n : ℕ
⊢ (antidiagonalTuple 0 n).Nodup

Tactic:
cases n

Result:
case zero.zero

⊢ (antidiagonalTuple 0 0).Nodup

case zero.succ
n✝ : ℕ
⊢ (antidiagonalTuple 0 (n✝ + 1)).Nodup

Proof state:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (∀ x ∈ antidiagonal n, (map (fun x_1 => Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup) ∧
    Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
      (antidiagonal n)

Tactic:
constructor

Result:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ ∀ x ∈ antidiagonal n, (map (fun x_1 => Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup

case succ.right
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)

Proof state:
k n : ℕ
⊢ (antidiagonalTuple k n).Nodup

Tactic:
induction' k with k ih generalizing n

Result:
case zero
n : ℕ
⊢ (antidiagonalTuple 0 n).Nodup

case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (antidiagonalTuple (k + 1) n).Nodup

Proof state:
case succ.right.succ.refine_2.intro.intro.intro.intro.intro
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni => map (fun x => Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal n)
a b : ℕ × ℕ
h :
  (map (fun x => Fin.cons a.1 x) (antidiagonalTuple k a.2)).Disjoint
    (map (fun x => Fin.cons a.1 x) (antidiagonalTuple k b.2))
x₂ : 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₂)

Result:
no goals