awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n k : ℕ
x : Fin k → ℕ
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
have elim0 : ∀ {n : ℕ}, Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n
Tactic: induction x using Fin.consInduction generalizing n with
  | elim0 =>
    cases n
    · decide
    · simp
  | cons x₀ x ih =>
    simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map,
      List.Nat.mem_antidiagonal, Fin.cons_inj, exists_eq_right_right, ih,
      @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _),
      ← Prod.mk_inj (a₁ := Prod.fst _), exists_eq_right]
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n k : ℕ
x : Fin k → ℕ
elim0 : ∀ {n : ℕ}, Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = n
have cons : ∀ {n : ℕ} (x₀ : ℕ) (x : Fin n → ℕ) (ih : ∀ {n_1 : ℕ}, x ∈ antidiagonalTuple n n_1 ↔ ∑ i : Fin n, x i = n_1) {n_1 : ℕ},
  Membership.mem (γ := List (Fin (n + 1) → ℕ)) (antidiagonalTuple (n + 1) n_1)
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n + 1), Fin.cons (α := fun (a : Fin (n + 1)) ↦ ℕ) x₀ x i = n_1
Tactic: induction x using Fin.consInduction generalizing n with
  | elim0 =>
    cases n
    · decide
    · simp
  | cons x₀ x ih =>
    simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map,
      List.Nat.mem_antidiagonal, Fin.cons_inj, exists_eq_right_right, ih,
      @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _),
      ← Prod.mk_inj (a₁ := Prod.fst _), exists_eq_right]
Cleared hypotheses: n, x
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
⊢ Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 n)
have zero : Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 0)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
n : ℕ
zero : Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 0)
⊢ Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 n)
have zero₁ : ∀ (n : ℕ), Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 (n + 1))
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ (antidiagonalTuple k n).Nodup
have succ : ∀ (k : ℕ) (ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup) (n : ℕ),
  Nodup (α := Fin (k + 1) → ℕ) (antidiagonalTuple (k + 1) n)
Tactic: induction k generalizing n with
  | zero => cases n <;> simp
  | succ k ih => ?_
Cleared hypotheses: k, n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ Nodup (α := Fin (k + 1) → ℕ) (antidiagonalTuple (k + 1) n)
have succ : (∀ x ∈ antidiagonal n,
    Nodup (α := Fin (k + 1) → ℕ)
      (map (fun (x_1 : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) x.1 x_1)
        (antidiagonalTuple k x.2))) ∧
  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: simp_rw [antidiagonalTuple, List.nodup_flatMap]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (∀ x ∈ antidiagonal n,
      Nodup (α := Fin (k + 1) → ℕ)
        (map (fun (x_1 : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) x.1 x_1)
          (antidiagonalTuple k x.2))) ∧
    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)
have succ : ∀ x ∈ antidiagonal n,
  Nodup (α := Fin (k + 1) → ℕ)
    (map (fun (x_1 : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) x.1 x_1) (antidiagonalTuple k x.2))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
succ :
  ∀ x ∈ antidiagonal n,
    Nodup (α := Fin (k + 1) → ℕ)
      (map (fun (x_1 : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) x.1 x_1) (antidiagonalTuple k x.2))
⊢ (∀ x ∈ antidiagonal n,
      Nodup (α := Fin (k + 1) → ℕ)
        (map (fun (x_1 : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) x.1 x_1)
          (antidiagonalTuple k x.2))) ∧
    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)
have 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 n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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)
⊢ 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))
have 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))
  ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n))
Tactic: rw [List.Nat.antidiagonal_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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)
⊢ 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))
have 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
Tactic: refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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
⊢ 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))
have 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
Tactic: refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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
⊢ False
have 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
Tactic: rw [List.mem_map] at hx₁ hx₂ ha
Cleared hypotheses: ha, x, hx₁, hx₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
Cleared hypotheses: a, ha, x, hx₁, hx₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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₁)
⊢ False
have h₁ : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
Tactic: rw [Fin.cons_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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
⊢ False
have 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
Tactic: rw [List.mem_map] at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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
⊢ False
have 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
Tactic: rw [List.mem_map] at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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
⊢ False
have 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
Tactic: obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
Cleared hypotheses: x, hx₁, hx₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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₁)
⊢ False
have h₁₃ : b.1 = a.1 ∧ x₂ = x₁
Tactic: rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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₁
⊢ False
have h₁₃ : b.1 = a.1
Tactic: obtain ⟨h₁₂, rfl⟩ := h₁₂
Cleared hypotheses: x₁, hx₁, h₁₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (hypothesis)
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
⊢ False
have hx₃ : x₂ ∈ antidiagonalTuple k (Prod.map Nat.succ id a).2
Tactic: obtain ⟨h₁₂, rfl⟩ := h₁₂
Cleared hypotheses: x₁, hx₁, h₁₂
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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
⊢ False
have 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
Tactic: rw [Function.onFun, h₁₂] at h
Cleared hypotheses: h, x₂, hx₂, h₁₂, hx₁
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
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)
have 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)
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₂)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
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)
⊢ 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)
have 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))
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₂)
Cleared hypotheses: n