awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst : DecidablePred P
rw :
  #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}) =
    #(S p ×ˢ
        {r ∈
            piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i))
              (p.removeNth (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) |
          P r})
rw₁ :
  #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}) =
    #(map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}))
⊢ #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}) =
    #(S p) *
      #({r ∈
            piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i))
              (p.removeNth (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) |
          P r})
have rw₂ : #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}) = #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)})
Tactic: rw [← card_product, ← map_insertNthEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
⊢ Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n
have elim0 : Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 0) Fin.elim0 ↔ Eq (α := ℕ) (∑ i : Fin 0, i.elim0) 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n : ℕ
elim0 : Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 0) Fin.elim0 ↔ Eq (α := ℕ) (∑ i : Fin 0, i.elim0) 0
⊢ Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n
have elim0₁ : ∀ (n : ℕ), Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 (n + 1)) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons : Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
    (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
  x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₁ : Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
    (flatMap
      (fun (ni : ℕ × ℕ) ↦
        map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
          (antidiagonalTuple n_1 ni.2))
      (antidiagonal n))
    (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
  x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₂ : (∃ a ∈ antidiagonal n,
    Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
        (antidiagonalTuple n_1 a.2))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
  x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₃ : (∃ a ∈ antidiagonal n,
    ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
      Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
  x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₄ : (∃ (a : ℕ × ℕ),
    a.1 + a.2 = n ∧
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
  x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₅ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₅ :
  (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₆ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ x ∈ antidiagonalTuple n_1 a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₅ :
  (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₆ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ x ∈ antidiagonalTuple n_1 a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₇ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∑ i : Fin n_1, x i = a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₅ :
  (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₆ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ x ∈ antidiagonalTuple n_1 a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₇ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∑ i : Fin n_1, x i = a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₈ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ a.2 = ∑ i : Fin n_1, x i ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₅ :
  (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₆ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ x ∈ antidiagonalTuple n_1 a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₇ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∑ i : Fin n_1, x i = a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₈ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ a.2 = ∑ i : Fin n_1, x i ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₉ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ a.1 = x₀ ∧ a.2 = ∑ i : Fin n_1, x i) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.NatAntidiagonal (goal)
Goal:
k n_1 x₀ : ℕ
x : Fin n_1 → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n_1 n ↔ ∑ i : Fin n_1, x i = n
n : ℕ
cons :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₁ :
  Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
      (flatMap
        (fun (ni : ℕ × ℕ) ↦
          map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) ni.1 x)
            (antidiagonalTuple n_1 ni.2))
        (antidiagonal n))
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₂ :
  (∃ a ∈ antidiagonal n,
      Membership.mem (γ := List (Fin (n_1 + 1) → ℕ))
        (map (fun (x : (i : Fin n_1) → ℕ) ↦ Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 x)
          (antidiagonalTuple n_1 a.2))
        (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₃ :
  (∃ a ∈ antidiagonal n,
      ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
        Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
          (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₄ :
  (∃ (a : ℕ × ℕ),
      a.1 + a.2 = n ∧
        ∃ a_1 ∈ antidiagonalTuple n_1 a.2,
          Eq (α := Fin (n_1 + 1) → ℕ) (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) a.1 a_1)
            (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x)) ↔
    x₀ + ∑ i : Fin n_1, x i = n
cons₅ :
  (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n_1 a.2, a.1 = x₀ ∧ a_1 = x) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₆ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ x ∈ antidiagonalTuple n_1 a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₇ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ ∑ i : Fin n_1, x i = a.2 ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₈ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ a.2 = ∑ i : Fin n_1, x i ∧ a.1 = x₀) ↔ x₀ + ∑ i : Fin n_1, x i = n
cons₉ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ a.1 = x₀ ∧ a.2 = ∑ i : Fin n_1, x i) ↔ x₀ + ∑ i : Fin n_1, x i = n
⊢ Membership.mem (γ := List (Fin (n_1 + 1) → ℕ)) (antidiagonalTuple (n_1 + 1) n)
      (Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x) ↔
    ∑ i : Fin (n_1 + 1), Fin.cons (α := fun (a : Fin (n_1 + 1)) ↦ ℕ) x₀ x i = n
have cons₁₀ : (∃ (a : ℕ × ℕ), a.1 + a.2 = n ∧ (a.1, a.2) = (x₀, ∑ i : Fin n_1, x i)) ↔ x₀ + ∑ i : Fin n_1, x i = n
Tactic: 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]