awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
pos : ∀ (hj : j = 0), 1 = j
⊢ 1 = j
have neg : ∀ (hj : ¬j = 0), 1 = j
Tactic: by_cases hj : j = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (hypothesis)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
hj : j = 0
⊢ 1 = j
have hij₁ : b = a
Tactic: simp [hj] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
x :
  (↑{x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a ≠ b} :
    Type u_1)
a b : α
h :
  Membership.mem (γ := Set (α × α))
    {x : α × α |
      match (motive := α × α → Prop) x with
      | (a, b) => a ≠ b}
    (a, b)
i j : Fin 2
hij :
  Eq.{u_1 + 1} (α := α) ((fun (i : Fin 2) ↦ if i = 0 then a else b) 1) ((fun (i : Fin 2) ↦ if i = 0 then a else b) j)
hi : ¬i = 0
hj : ¬j = 0
⊢ 1 = j
have neg : Eq (α := Fin 2) 1 1
Tactic: rw [eq_one_of_ne_zero j hj]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
e : Fin 2 ↪ α
⊢ (fun
          (x :
            (↑{x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b} :
              Type u_1)) ↦
        (match (motive :=
            (↑{x : α × α |
                    match (motive := α × α → Prop) x with
                    | (a, b) => a ≠ b} :
                Type u_1) →
              Fin 2 ↪ α)
            x with
          | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
          Fin 2 ↪ α))
      ((fun (e : Fin 2 ↪ α) ↦
          (Subtype.mk (p := fun (x : α × α) ↦
              Membership.mem (γ := Set (α × α))
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b}
                x)
              ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
            { x : α × α //
              Membership.mem (γ := Set (α × α))
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a ≠ b}
                x }))
        e) =
    e
have h : ∀ (i : Fin 2),
  Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := sorry } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) sorry :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Embedding (goal)
Goal:
α : Type u_1
e : Fin 2 ↪ α
i : Fin 2
⊢ Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := ⋯ } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) ⋯ :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)
have pos : ∀ (hi : i = 0),
  Eq (α := α)
    (((fun
                (x :
                  (↑{x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b} :
                    Type u_1)) ↦
              (match (motive :=
                  (↑{x : α × α |
                          match (motive := α × α → Prop) x with
                          | (a, b) => a ≠ b} :
                      Type u_1) →
                    Fin 2 ↪ α)
                  x with
                | ⟨(a, b), h⟩ => { toFun := fun (i : Fin 2) ↦ if i = 0 then a else b, inj' := sorry } :
                Fin 2 ↪ α))
            ((fun (e : Fin 2 ↪ α) ↦
                (Subtype.mk (p := fun (x : α × α) ↦
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x)
                    ((e : (a : Fin 2) → α) 0, (e : (a : Fin 2) → α) 1) sorry :
                  { x : α × α //
                    Membership.mem (γ := Set (α × α))
                      {x : α × α |
                        match (motive := α × α → Prop) x with
                        | (a, b) => a ≠ b}
                      x }))
              e) :
          (a : Fin 2) → α)
        i :
      α)
    ((e : (a : Fin 2) → α) i : α)
Tactic: by_cases hi : i = 0
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail))
      (cons (α := α) x_zero x_tail) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
have simp_rw : Membership.mem (γ := Finset (α 0)) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail 0 : Finset (α 0))
      (cons (α := α) x_zero x_tail 0) ∧
    Membership.mem (γ := Finset ((a : Fin n) → α a.succ))
      (piFinset (δ := fun (a : Fin n) ↦ α a.succ)
        (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
          (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail)))
      (tail (α := α) (cons (α := α) x_zero x_tail)) ↔
  x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
Tactic: simp_rw [mem_piFinset_iff_zero_tail, cons_zero, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
simp_rw :
  Membership.mem (γ := Finset (α 0)) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail 0 : Finset (α 0))
        (cons (α := α) x_zero x_tail 0) ∧
      Membership.mem (γ := Finset ((a : Fin n) → α a.succ))
        (piFinset (δ := fun (a : Fin n) ↦ α a.succ)
          (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
            (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail)))
        (tail (α := α) (cons (α := α) x_zero x_tail)) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail))
      (cons (α := α) x_zero x_tail) ↔
    x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
have simp_rw₁ : x_zero ∈ s_zero ∧
    Membership.mem (γ := Finset ((a : Fin n) → α a.succ))
      (piFinset (δ := fun (a : Fin n) ↦ α a.succ)
        (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
          (cons (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_zero s_tail)))
      (tail (α := α) (cons (α := α) x_zero x_tail)) ↔
  x_zero ∈ s_zero ∧ x_tail ∈ piFinset (δ := fun (a : Fin n) ↦ α a.succ) s_tail
Tactic: simp_rw [mem_piFinset_iff_zero_tail, cons_zero, tail_cons]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last))
      (snoc (α := α) x_init x_last) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
have simp_rw : Membership.mem (γ := Finset (α (last n)))
      (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last (last n) : Finset (α (last n)))
      (snoc (α := α) x_init x_last (last n)) ∧
    Membership.mem (γ := Finset ((a : Fin n) → α a.castSucc))
      (piFinset (δ := fun (a : Fin n) ↦ α a.castSucc)
        (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
          (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last)))
      (init (α := α) (snoc (α := α) x_init x_last)) ↔
  x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
Tactic: simp_rw [mem_piFinset_iff_last_init, init_snoc, snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
simp_rw :
  Membership.mem (γ := Finset (α (last n)))
        (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last (last n) : Finset (α (last n)))
        (snoc (α := α) x_init x_last (last n)) ∧
      Membership.mem (γ := Finset ((a : Fin n) → α a.castSucc))
        (piFinset (δ := fun (a : Fin n) ↦ α a.castSucc)
          (init (α := fun (i : Fin (n + 1)) ↦ Finset (α i))
            (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last)))
        (init (α := α) (snoc (α := α) x_init x_last)) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
⊢ Membership.mem (γ := Finset ((a : Fin (n + 1)) → α a))
      (piFinset (δ := α) (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last))
      (snoc (α := α) x_init x_last) ↔
    x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
have simp_rw₁ : Membership.mem (γ := Finset (α (last n)))
      (snoc (α := fun (a : Fin (n + 1)) ↦ Finset (α a)) s_init s_last (last n) : Finset (α (last n)))
      (snoc (α := α) x_init x_last (last n)) ∧
    x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init ↔
  x_last ∈ s_last ∧ x_init ∈ piFinset (δ := fun (a : Fin n) ↦ α a.castSucc) s_init
Tactic: simp_rw [mem_piFinset_iff_last_init, init_snoc, snoc_last]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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
⊢ 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})
have 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})
Tactic: unfold tail
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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
⊢ 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})
have 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})
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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
⊢ 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})
have 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})
Tactic: unfold init
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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
⊢ 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})
have 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})
Tactic: ext
-- 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
⊢ 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}
have 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})
Tactic: unfold removeNth
-- 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
⊢ 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})
have 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})
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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)}) =
    card (α := α 0) (S 0) *
      #({r ∈ piFinset (δ := fun (i : Fin n) ↦ α i.succ) (tail (α := fun (i : Fin (n + 1)) ↦ Finset (α i)) S) | P r})
have 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}))
Tactic: rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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}))
⊢ #({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})
have rw₁ : #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) =
  #(map (consEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}))
Tactic: rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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)}))
⊢ #({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})
have rw₂ : #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)}) = #({r ∈ piFinset (δ := α) S | P (tail (α := α) r)})
Tactic: rw [← card_product, ← map_consEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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)}) =
    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})
have 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}))
Tactic: rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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}))
⊢ #({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})
have rw₁ : #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) =
  #(map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (init (α := α) r)}))
Tactic: rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]
-- Lean 4 proof step from Mathlib.Data.Fin.Tuple.Finset (goal)
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)}))
⊢ #({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})
have rw₂ : #({r ∈ piFinset (δ := α) S | P (init (α := α) r)}) = #({r ∈ piFinset (δ := α) S | P (init (α := α) r)})
Tactic: rw [← card_product, ← map_snocEquiv_filter_piFinset, card_map]
-- 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
⊢ #({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)}) =
  #(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]
-- 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})
⊢ #({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)}) =
  #(map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset (δ := α) S | P (p.removeNth (α := α) r)}))
Tactic: rw [← card_product, ← map_insertNthEquiv_filter_piFinset, card_map]