awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst : DecidablePred P
unfold :
  map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.succ}) =
    SProd.sprod (α := Finset (α 0)) (β := Finset ((i : Fin n) → α i.succ)) (S 0)
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) fun (i : Fin n) ↦ S i.succ | P r})
⊢ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) =
    SProd.sprod (α := Finset (α 0)) (S 0)
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r})

Tactic:
unfold tail

Premises used: Fin.tail
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst : DecidablePred P
h :
  ∀ (a : α 0 × ((i : Fin n) → α i.succ)),
    a ∈ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.succ}) ↔
      a ∈
        SProd.sprod (α := Finset (α 0)) (β := Finset ((i : Fin n) → α i.succ)) (S 0)
          ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) fun (i : Fin n) ↦ S i.succ | P r})
⊢ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.succ}) =
    SProd.sprod (α := Finset (α 0)) (β := Finset ((i : Fin n) → α i.succ)) (S 0)
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) fun (i : Fin n) ↦ S i.succ | P r})

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst : DecidablePred P
a : α 0 × ((i : Fin n) → α i.succ)
⊢ a ∈ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.succ}) ↔
    a ∈
      SProd.sprod (α := Finset (α 0)) (β := Finset ((i : Fin n) → α i.succ)) (S 0)
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) fun (i : Fin n) ↦ S i.succ | P r})

Tactic:
simp [Fin.forall_iff_succ, and_assoc]

Premises used: Fin.forall_iff_succ, and_assoc
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst : DecidablePred P
unfold :
  map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.castSucc}) =
    SProd.sprod (α := Finset (α (last n))) (β := Finset ((i : Fin n) → α i.castSucc)) (S (last n))
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) fun (i : Fin n) ↦ S i.castSucc | P r})
⊢ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) =
    SProd.sprod (α := Finset (α (last n))) (S (last n))
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r})

Tactic:
unfold init

Premises used: Fin.init
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst : DecidablePred P
h :
  ∀ (a : α (last n) × ((i : Fin n) → α i.castSucc)),
    a ∈ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.castSucc}) ↔
      a ∈
        SProd.sprod (α := Finset (α (last n))) (β := Finset ((i : Fin n) → α i.castSucc)) (S (last n))
          ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) fun (i : Fin n) ↦ S i.castSucc | P r})
⊢ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.castSucc}) =
    SProd.sprod (α := Finset (α (last n))) (β := Finset ((i : Fin n) → α i.castSucc)) (S (last n))
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) fun (i : Fin n) ↦ S i.castSucc | P r})

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst : DecidablePred P
a : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ a ∈ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r i.castSucc}) ↔
    a ∈
      SProd.sprod (α := Finset (α (last n))) (β := Finset ((i : Fin n) → α i.castSucc)) (S (last n))
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) fun (i : Fin n) ↦ S i.castSucc | P r})

Tactic:
simp [Fin.forall_iff_castSucc, and_assoc]

Premises used: Fin.forall_iff_castSucc, and_assoc
-- Module: Mathlib.Data.Fin.Tuple.Finset
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
unfold :
  map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r (p.succAbove i)}) =
    SProd.sprod (β := Finset ((i : Fin n) → α (p.succAbove i))) (S p)
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i)) fun (i : Fin n) ↦ S (p.succAbove i) | P r})
⊢ map (insertNthEquiv α p).symm.toEmbedding ({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}

Tactic:
unfold removeNth

Premises used: Fin.removeNth
-- Module: Mathlib.Data.Fin.Tuple.Finset
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
h :
  ∀ (a : α p × ((i : Fin n) → α (p.succAbove i))),
    a ∈ map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r (p.succAbove i)}) ↔
      a ∈
        SProd.sprod (β := Finset ((i : Fin n) → α (p.succAbove i))) (S p)
          ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i)) fun (i : Fin n) ↦ S (p.succAbove i) | P r})
⊢ map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r (p.succAbove i)}) =
    SProd.sprod (β := Finset ((i : Fin n) → α (p.succAbove i))) (S p)
      ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i)) fun (i : Fin n) ↦ S (p.succAbove i) | P r})

Tactic:
ext
-- Module: Mathlib.Data.Fin.Tuple.Finset
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
a : α p × ((i : Fin n) → α (p.succAbove i))
⊢ a ∈ map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P fun (i : Fin n) ↦ r (p.succAbove i)}) ↔
    a ∈
      SProd.sprod (β := Finset ((i : Fin n) → α (p.succAbove i))) (S p)
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i)) fun (i : Fin n) ↦ S (p.succAbove i) | P r})

Tactic:
simp [Fin.forall_iff_succAbove p, and_assoc]

Premises used: and_assoc, Fin.forall_iff_succAbove
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst : DecidablePred P
⊢ {r ∈ piFinset (δ := α) S | P (tail (α := α) r)} =
    map (consEquiv α).toEmbedding
      (SProd.sprod (α := Finset (α 0)) (S 0)
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r}))

Tactic:
simp [← map_consEquiv_filter_piFinset, map_map]

Premises used: Finset.map_consEquiv_filter_piFinset, Finset.map_map
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst : DecidablePred P
⊢ {r ∈ piFinset (δ := α) S | P (init (α := α) r)} =
    map (snocEquiv α).toEmbedding
      (SProd.sprod (α := Finset (α (last n))) (S (last n))
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) |
          P r}))

Tactic:
simp [← map_snocEquiv_filter_piFinset, map_map]

Premises used: Finset.map_snocEquiv_filter_piFinset, Finset.map_map
-- Module: Mathlib.Data.Fin.Tuple.Finset
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
⊢ {r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)} =
    map (insertNthEquiv α p).toEmbedding
      (S p ×ˢ
        {r ∈
            piFinset (δ := fun (i : Fin n) ↦ α (p.succAbove i))
              (p.removeNth (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) |
          P r})

Tactic:
simp [← map_insertNthEquiv_filter_piFinset, map_map]

Premises used: Finset.map_insertNthEquiv_filter_piFinset, Finset.map_map
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst : DecidablePred P
rw :
  #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) =
    #(SProd.sprod (α := Finset (α 0)) (S 0)
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r}))
rw₁ :
  #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) =
    #(map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}))
rw₂ rw₃ : #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) = #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)})
⊢ #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) =
    card (α := α 0) (S 0) *
      #({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r})

Tactic:
rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]

Premises used: Finset.map_consEquiv_filter_piFinset, Finset.card_product, Finset.card_map
-- Module: Mathlib.Data.Fin.Tuple.Finset
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst : DecidablePred P
rw :
  #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) =
    #(SProd.sprod (α := Finset (α (last n))) (S (last n))
        ({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) |
          P r}))
rw₁ :
  #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) =
    #(map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (init (α := α) r)}))
rw₂ rw₃ : #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) = #({r ∈ piFinset (δ := α) S | P (init (α := α) r)})
⊢ #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) =
    card (α := α (last n)) (S (last n)) *
      #({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.castSucc) (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r})

Tactic:
rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]

Premises used: Finset.map_snocEquiv_filter_piFinset, Finset.card_product, Finset.card_map
-- Module: Mathlib.Data.Fin.Tuple.Finset
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)}))
rw₂ rw₃ :
  #({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}) = #({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})

Tactic:
rw [← card_product, ← map_insertNthEquiv_filter_piFinset, card_map]

Premises used: Finset.card_product, Finset.card_map, Finset.map_insertNthEquiv_filter_piFinset
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
⊢ antidiagonalTuple 0 0 = [![]]

Tactic:
rfl

Premises used: List.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Eq (α := List (Fin 0 → ℕ)) (antidiagonalTuple 0 (n + 1)) []

Tactic:
rfl

Premises used: List.Nat.antidiagonalTuple, rfl
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
elim0 : Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 0) Fin.elim0 ↔ Eq (α := ℕ) (∑ i : Fin 0, i.elim0) 0
elim0₁ :
  ∀ (n : ℕ),
    Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 (n + 1)) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n + 1
⊢ Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n

Tactic:
cases n
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
⊢ Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 0) Fin.elim0 ↔ Eq (α := ℕ) (∑ i : Fin 0, i.elim0) 0

Tactic:
decide
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
⊢ Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 (n + 1)) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n + 1

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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
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
⊢ 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

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]

Premises used: exists_eq_right_right, Fin.cons_inj, Prod.mk_inj, Fin.sum_cons, exists_eq_right, and_comm, eq_comm, List.Nat.antidiagonalTuple, List.Nat.mem_antidiagonal, List.mem_flatMap, List.mem_map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n k : ℕ
x : Fin k → ℕ
elim0 : ∀ {n : ℕ}, Membership.mem (γ := List (Fin 0 → ℕ)) (antidiagonalTuple 0 n) Fin.elim0 ↔ ∑ i : Fin 0, i.elim0 = n
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
⊢ x ∈ antidiagonalTuple k n ↔ ∑ i : Fin k, x i = 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]

Premises used: exists_eq_right_right, Fin.cons_inj, Prod.mk_inj, Fin.sum_cons, exists_eq_right, and_comm, eq_comm, List.cons, List.Nat.antidiagonalTuple, List.Nat.mem_antidiagonal, List.mem_flatMap, List.mem_map
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
zero : Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 0)
zero₁ : ∀ (n : ℕ), Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 (n + 1))
⊢ Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 n)

Tactic:
cases n
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
⊢ Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 0)

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
n : ℕ
⊢ Nodup (α := Fin 0 → ℕ) (antidiagonalTuple 0 (n + 1))

Tactic:
simp
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ Nodup (α := Fin (k + 1) → ℕ) (antidiagonalTuple (k + 1) n)

Tactic:
?_
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k n : ℕ
succ :
  ∀ (k : ℕ) (ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup) (n : ℕ),
    Nodup (α := Fin (k + 1) → ℕ) (antidiagonalTuple (k + 1) n)
⊢ (antidiagonalTuple k n).Nodup

Tactic:
induction k generalizing n with
  | zero => cases n <;> simp
  | succ k ih => ?_
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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))) ∧
    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)
⊢ Nodup (α := Fin (k + 1) → ℕ) (antidiagonalTuple (k + 1) n)

Tactic:
simp_rw [antidiagonalTuple, List.nodup_flatMap]

Premises used: List.nodup_flatMap, List.Nat.antidiagonalTuple
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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))
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)
⊢ (∀ 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:
constructor
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
succ :
  i ∈ antidiagonal n →
    Nodup (α := Fin (k + 1) → ℕ)
      (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) i.1 x) (antidiagonalTuple k i.2))
⊢ i ∈ antidiagonal n →
    Nodup (α := Fin (k + 1) → ℕ)
      (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) i.1 x) (antidiagonalTuple k i.2))

Tactic:
_
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
h : i ∈ antidiagonal n
⊢ Nodup (α := Fin (k + 1) → ℕ)
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) i.1 x) (antidiagonalTuple k i.2))

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

Premises used: Prod.fst, List.Nodup.map, Fin.cons_right_injective, Prod.snd
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
i : ℕ × ℕ
h : i ∈ antidiagonal n
⊢ Nodup (α := Fin (k + 1) → ℕ)
    (map (fun (x : (i : Fin k) → ℕ) ↦ Fin.cons (α := fun (a : Fin (k + 1)) ↦ ℕ) i.1 x) (antidiagonalTuple k i.2))

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

Premises used: Prod.fst, List.Nodup.map, Fin.cons_right_injective, Prod.snd
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
⊢ 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:
List.pairwise_singleton _ _

Premises used: List.map, List.pairwise_singleton, List.Nat.antidiagonal
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
Goal:
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
⊢ 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:
exact List.pairwise_singleton _ _

Premises used: List.pairwise_singleton
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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 :
  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))
⊢ 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:
rw [List.Nat.antidiagonal_succ]

Premises used: List.Nat.antidiagonal_succ
-- Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal
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))

Tactic:
List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)

Premises used: List.Pairwise.cons, List.Pairwise.map