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

Proof state:
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₁ : ∃ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2, Fin.cons (Prod.map Nat.succ id a).1 a_1 = x
hx₂ : ∃ a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2, Fin.cons (Prod.map Nat.succ id b).1 a = x
⊢ False

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

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 (Prod.map Nat.succ id b).1 x₂ = Fin.cons (Prod.map Nat.succ id a).1 x₁
⊢ False

Proof state:
case zero.zero

⊢ (antidiagonalTuple 0 0).Nodup

Tactic:
simp

Result:
no goals

Proof state:
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)

Tactic:
induction' n with n n_ih

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

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))
    (antidiagonal (n + 1))

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))
    (antidiagonal (n + 1))

Tactic:
rw [List.Nat.antidiagonal_succ]

Result:
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))

Proof state:
case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
a✝ : i ∈ antidiagonal n
⊢ (map (fun x => Fin.cons i.1 x) (antidiagonalTuple k i.2)).Nodup

Tactic:
exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)

Result:
no goals

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

Tactic:
exact List.pairwise_singleton _ _

Result:
no goals

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

Tactic:
simp [eq_comm]

Result:
no goals

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 : 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 b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ False

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

Result:
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

Proof state:
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

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

Result:
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₁ : ∃ a_1 ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2, Fin.cons (Prod.map Nat.succ id a).1 a_1 = x
hx₂ : ∃ a ∈ antidiagonalTuple k (Prod.map Nat.succ id b).2, Fin.cons (Prod.map Nat.succ id b).1 a = 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₁₂ : b.1 = a.1 ∧ x₂ = x₁
⊢ False

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

Result:
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 : 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 b).2
h₁₂ : b.1 = a.1
hx₁ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
⊢ 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 : Fin.cons (Prod.map Nat.succ id a).1 x₂ = Fin.cons (0, n + 1).1 x₁
⊢ False

Tactic:
rw [Fin.cons_inj] at h

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 : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False