awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₅ : ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
  ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₅ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₆ : ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
  (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
  ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₅ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₆ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₇ : ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
  (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
  let f := seqOfForallFinsetExistsAux P r h';
  ∀ (hf : f = seqOfForallFinsetExistsAux P r h'),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₅ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₆ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₇ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h'),
      ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₈ : ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
  (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
  let f := seqOfForallFinsetExistsAux P r h';
  ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
have : Nonempty α
have₁ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₂ : Nonempty α
have₃ have₄ : ∀ (this : Nonempty α), ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₅ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₆ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₇ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h'),
      ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have₈ :
  ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
    (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
    let f := seqOfForallFinsetExistsAux P r h';
    ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)),
      ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
have have₉ : ∀ (this : Nonempty α) (F : (s : Finset α) → α) (hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s))
  (h' : ∀ (s : Finset α), ∃ (y : α), (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y),
  let f := seqOfForallFinsetExistsAux P r h';
  ∀ (hf : f = seqOfForallFinsetExistsAux P r h') (A : ∀ (n : ℕ), P (f n)) (m n : ℕ) (hmn : m < n), r (f m) (f n)
Tactic: classical
    have : Nonempty α := by
      rcases h ∅ (by simp) with ⟨y, _⟩
      exact ⟨y⟩
    choose! F hF using h
    have h' : ∀ s : Finset α, ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y := fun s => ⟨F s, hF s⟩
    set f := seqOfForallFinsetExistsAux P r h' with hf
    have A : ∀ n : ℕ, P (f n) := by
      intro n
      induction n using Nat.strong_induction_on with | _ n IH
      have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2
      rw [hf, seqOfForallFinsetExistsAux]
      exact
        (Classical.choose_spec
            (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n))))
            (by simp [IH'])).1
    refine ⟨f, A, fun m n hmn => ?_⟩
    conv_rhs => rw [hf]
    rw [seqOfForallFinsetExistsAux]
    apply
      (Classical.choose_spec
          (h' (Finset.image (fun i : Fin n => f i) (Finset.univ : Finset (Fin n)))) (by simp [A])).2
    exact Finset.mem_image.2 ⟨⟨m, hmn⟩, Finset.mem_univ _, rfl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)
have rcases : ∀ (f : ℕ → α) (hf : ∀ (n : ℕ), P (f n)) (hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)),
  ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)
Tactic: rcases exists_seq_of_forall_finset_exists P r h with ⟨f, hf, hf'⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Basic (goal)
Goal:
α : Type u_4
P : α → Prop
r : α → α → Prop
inst : Std.Symm r
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ (y : α), P y ∧ ∀ x ∈ s, r x y
f : ℕ → α
hf : ∀ (n : ℕ), P (f n)
hf' : ∀ (m n : ℕ), m < n → r (f m) (f n)
⊢ ∃ (f : ℕ → α), (∀ (n : ℕ), P (f n)) ∧ Pairwise (r on f)
have refine : ∀ (m n : ℕ) (hmn : m ≠ n), (r on f) m n
Tactic: refine ⟨f, hf, fun m n hmn => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommMonoid α
s : Finset ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)
have rw : Eq.{u_1 + 1} (α := α) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
Tactic: rw [← prod_filter, filter_mem_eq_inter, univ_inter]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommMonoid α
s : Finset ι
f : ι → α
rw : Eq.{u_1 + 1} (α := α) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)
have rw₁ : Eq.{u_1 + 1} (α := α) (∏ a ∈ univ ∩ s, f a) (∏ i ∈ s, f i)
Tactic: rw [← prod_filter, filter_mem_eq_inter, univ_inter]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
ι : Type u_4
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : CommMonoid α
s : Finset ι
f : ι → α
rw : Eq.{u_1 + 1} (α := α) (∏ a : ι with a ∈ s, f a) (∏ i ∈ s, f i)
rw₁ : Eq.{u_1 + 1} (α := α) (∏ a ∈ univ ∩ s, f a) (∏ i ∈ s, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ι, if i ∈ s then f i else 1) (∏ i ∈ s, f i)
have rw₂ : Eq.{u_1 + 1} (α := α) (∏ a ∈ s, f a) (∏ i ∈ s, f i)
Tactic: rw [← prod_filter, filter_mem_eq_inter, univ_inter]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
⊢ ∏ x : α, f x = f a * f b
have ha : a ∉ Finset.univ → f a = 1
Tactic: apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
f : α → M
a b : α
h₁ : a ≠ b
h₂ : ∀ (x : α), x ≠ a ∧ x ≠ b → f x = 1
ha : a ∉ Finset.univ → f a = 1
⊢ ∏ x : α, f x = f a * f b
have hb : b ∉ Finset.univ → f b = 1
Tactic: apply Finset.prod_eq_mul a b h₁ fun x _ hx => h₂ x hx
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
inst_2 : DecidableEq α
f : α → M
a : α
⊢ ∏ i : α, f i = f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
have simp_rw : ∏ i : Option { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) i) =
  f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
Tactic: simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
inst_2 : DecidableEq α
f : α → M
a : α
simp_rw :
  ∏ i : Option { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) i) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
⊢ ∏ i : α, f i = f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
have simp_rw₁ : f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) none) *
    ∏ i : { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some i)) =
  f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
Tactic: simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : Fintype α
inst_1 : CommMonoid M
inst_2 : DecidableEq α
f : α → M
a : α
simp_rw :
  ∏ i : Option { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) i) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
simp_rw₁ :
  f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) none) *
      ∏ i : { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some i)) =
    f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
⊢ ∏ i : α, f i = f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
have simp_rw₂ : f a * ∏ i : { b : α // b ≠ a }, f ((Equiv.optionSubtypeNe a : (a : Option { b : α // b ≠ a }) → α) (some i)) =
  f a * ∏ i : { i : α // i ≠ a }, f (↑i : α)
Tactic: simp_rw [← (Equiv.optionSubtypeNe a).prod_comp, prod_option, Equiv.optionSubtypeNe_none,
    Equiv.optionSubtypeNe_some]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) =
    ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
have rw : #(piFinset (δ := α) (Function.update (β := fun (a : ι) ↦ Finset (α a)) s i {a})) =
  ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
Tactic: rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
rw :
  #(piFinset (δ := α) (Function.update (β := fun (a : ι) ↦ Finset (α a)) s i {a})) =
    ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) =
    ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
have rw₁ : Eq (α := ℕ) (∏ i_1 : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) i_1))
  (∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j))
Tactic: rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
⊢ #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j) =
    Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j
have inl : ∀ {a : α j} (ha : a ∈ s j),
  #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s j ({a} : Finset (α j)) j) =
    Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) j 1 j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i, a, ha
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
j : ι
inl :
  ∀ {a : α j} (ha : a ∈ s j),
    #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s j ({a} : Finset (α j)) j) =
      Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) j 1 j
⊢ #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j) =
    Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j
have inr : ∀ (hji : j ≠ i),
  #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j) =
    Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j
Tactic: obtain rfl | hji := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ j ∈ erase univ i, #(s j)
have _ : #({f ∈ piFinset (δ := α) s | f i = a}) =
  ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
Tactic: calc
    _ = ∏ j, #(Function.update s i {a} j) := by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
    _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
    _ = _ := by simp [prod_update_of_mem, erase_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
_ :
  #({f ∈ piFinset (δ := α) s | f i = a}) =
    ∏ j : ι, #(Function.update (β := fun (a : ι) ↦ Finset (α a)) s i ({a} : Finset (α i)) j)
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ j ∈ erase univ i, #(s j)
have _₁ : Eq (α := ℕ) (∏ j : ι, Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j) (∏ j ∈ erase univ i, #(s j))
Tactic: calc
    _ = ∏ j, #(Function.update s i {a} j) := by
      rw [← piFinset_update_singleton_eq_filter_piFinset_eq _ _ ha, Fintype.card_piFinset]
    _ = ∏ j, Function.update (fun j ↦ #(s j)) i 1 j :=
      Fintype.prod_congr _ _ fun j ↦ by obtain rfl | hji := eq_or_ne j i <;> simp [*]
    _ = _ := by simp [prod_update_of_mem, erase_eq]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
κ : Type u_5
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
⊢ ∏ j ∈ erase univ i, #s = #s ^ (card ι - 1)
have rw : #s ^ #(erase univ i) = #s ^ (card ι - 1)
Tactic: rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
κ : Type u_5
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
rw : #s ^ #(erase univ i) = #s ^ (card ι - 1)
⊢ ∏ j ∈ erase univ i, #s = #s ^ (card ι - 1)
have rw₁ : #s ^ (Finset.card.{u_4} (α := ι) univ - 1) = #s ^ (card ι - 1)
Tactic: rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
ι : Type u_4
κ : Type u_5
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
s : Finset κ
i : ι
x : κ
hx : x ∈ s
rw : #s ^ #(erase univ i) = #s ^ (card ι - 1)
rw₁ : #s ^ (Finset.card.{u_4} (α := ι) univ - 1) = #s ^ (card ι - 1)
⊢ ∏ j ∈ erase univ i, #s = #s ^ (card ι - 1)
have rw₂ : #s ^ (card ι - 1) = #s ^ (card ι - 1)
Tactic: rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]