awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.BigOperators
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)
rw₁ 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))
⊢ #({f ∈ piFinset (δ := α) s | f 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]

Premises used: Fintype.piFinset_update_singleton_eq_filter_piFinset_eq, Fintype.card_piFinset
-- Module: Mathlib.Data.Fintype.BigOperators
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
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
⊢ #(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

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
j : ι
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:
simp [*]
-- Module: Mathlib.Data.Fintype.BigOperators
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 : ι
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:
simp [*]
-- Module: Mathlib.Data.Fintype.BigOperators
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
⊢ Eq (α := ℕ) (∏ j : ι, Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j)
    (∏ j ∈ erase univ i, #(s j))

Tactic:
simp [prod_update_of_mem, erase_eq]

Premises used: Finset.erase_eq, Finset.prod_update_of_mem
-- Module: Mathlib.Data.Fintype.BigOperators
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)
_₁ :
  Eq (α := ℕ) (∏ j : ι, Function.update (β := fun (j : ι) ↦ ℕ) (fun (j : ι) ↦ #(s j)) i 1 j)
    (∏ j ∈ erase univ i, #(s j))
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ 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]

Premises used: Fintype.prod_congr
-- Module: Mathlib.Data.Fintype.BigOperators
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)
rw₂ rw₃ : #s ^ (card ι - 1) = #s ^ (card ι - 1)
⊢ ∏ j ∈ erase univ i, #s = #s ^ (card ι - 1)

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Premises used: Finset.mem_univ, Finset.card_univ, Finset.card_erase_of_mem, Finset.prod_const, Finset.card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
pos : ∀ (h : a ∈ s i), #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ b ∈ erase univ i, #(s b)
neg : ∀ (h : a ∉ s i), #({f ∈ piFinset (δ := α) s | f i = a}) = 0
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = if a ∈ s i then ∏ b ∈ erase univ i, #(s b) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∈ s i
pos pos₁ : Eq (α := ℕ) (∏ j ∈ erase univ i, #(s j)) (∏ b ∈ erase univ i, #(s b))
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ b ∈ erase univ i, #(s b)

Tactic:
rw [card_filter_piFinset_eq_of_mem _ _ h]

Premises used: Fintype.card_filter_piFinset_eq_of_mem
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
α : ι → Type u_6
inst : DecidableEq ι
inst_1 : Fintype ι
inst_2 : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
h : a ∉ s i
neg : Finset.card (α := (a : ι) → α a) ∅ = 0
neg₁ neg₂ : Eq (α := ℕ) 0 0
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = 0

Tactic:
rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]

Premises used: Fintype.filter_piFinset_of_notMem, Finset.card_empty
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
ι : Type u_4
κ : Type u_5
inst : DecidableEq ι
inst_1 : DecidableEq κ
inst_2 : Fintype ι
s : Finset κ
i : ι
j : κ
rw : (if j ∈ s then #s ^ #(erase univ i) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
rw₁ : (if j ∈ s then #s ^ (Finset.card.{u_4} (α := ι) univ - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
rw₂ rw₃ : (if j ∈ s then #s ^ (card ι - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
⊢ (if j ∈ s then ∏ b ∈ erase univ i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0

Tactic:
rw [prod_const #s, card_erase_of_mem (mem_univ _), card_univ]

Premises used: Finset.mem_univ, Finset.card_univ, Finset.card_erase_of_mem, Finset.prod_const, Finset.card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : Fintype β
⊢ card (α → β) = card β ^ card α

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
n : ℕ
rw : Fintype.card.{u_1} (Fin n → α) = Fintype.card α ^ n
⊢ Fintype.card.{u_1} (List.Vector α n) = Fintype.card α ^ n

Tactic:
rw [Fintype.ofEquiv_card]

Premises used: Fintype.ofEquiv_card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
n : ℕ
⊢ Fintype.card.{u_1} (Fin n → α) = Fintype.card α ^ n

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : {x ∈ T | x.length = s} ⊆ image (α := Fin s → α) List.ofFn univ
⊢ #({x ∈ T | x.length = s}) ≤ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ)

Tactic:
apply Finset.card_le_card

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := ⋯
j : Fin s
⊢ (↑j : ℕ) < a.length

Tactic:
simp [hlen]
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := ⋯
⊢ Membership.mem (γ := Finset (Fin s → α)) univ fun (j : Fin s) ↦ a.get ⟨(↑j : ℕ), ⋯⟩

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := ⋯
⊢ List.length.{u_1} (α := α) (List.ofFn (n := s) fun (j : Fin s) ↦ a.get (⟨(↑j : ℕ), ⋯⟩ : Fin a.length)) = a.length

Tactic:
simp [hlen]
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := ⋯
⊢ ∀ (n : ℕ) (h₁ : n < List.length.{u_1} (α := α) (List.ofFn (n := s) fun (j : Fin s) ↦ a.get ⟨(↑j : ℕ), ⋯⟩))
    (h₂ : n < a.length),
    List.get (List.ofFn (n := s) fun (j : Fin s) ↦ a.get (⟨(↑j : ℕ), ⋯⟩ : Fin a.length))
        (⟨n, h₁⟩ :
          Fin
            (List.length.{u_1} (α := α) (List.ofFn (n := s) fun (j : Fin s) ↦ a.get (⟨(↑j : ℕ), ⋯⟩ : Fin a.length)))) =
      a.get (⟨n, h₂⟩ : Fin a.length)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
a : List α
ha : a ∈ {x ∈ T | x.length = s}
hlen : a ∈ T ∧ a.length = s := ⋯
⊢ Membership.mem (γ := Finset (List α)) (image (α := Fin s → α) List.ofFn univ) a

Tactic:
exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩

Premises used: Iff.mpr, Finset.mem_image, List.get, Fin.mk, List.ext_get, Fin.val, And.intro, Exists.intro
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
⊢ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ) = Fintype.card α ^ s

Tactic:
simp [card_image_of_injective univ List.ofFn_injective]

Premises used: Finset.univ, List.ofFn_injective, Finset.card_image_of_injective
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
_ : #({x ∈ T | x.length = s}) ≤ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ)
_₁ : card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ) = Fintype.card α ^ s
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s

Tactic:
calc
    _ ≤ (Finset.univ.image List.ofFn).card := by
          apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩
    _ = Fintype.card α ^ s := by
          simp [card_image_of_injective univ List.ofFn_injective]

Premises used: Finset.univ, List.ofFn, Fintype.card, Finset.card, Finset.image
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
_ : #({x ∈ T | x.length = s}) ≤ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ)
_₁ : card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ) = Fintype.card α ^ s
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s

Tactic:
classical
  calc
    _ ≤ (Finset.univ.image List.ofFn).card := by
          apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩
    _ = Fintype.card α ^ s := by
          simp [card_image_of_injective univ List.ofFn_injective]

Premises used: Finset.univ, List.ofFn, Fintype.card, Finset.card, Finset.image
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : ℕ), x < n ↔ x ∈ range n

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : CommMonoid α
f : ℕ → α
n : ℕ
⊢ ∀ (x : Fin n),
    f (↑x : ℕ) =
      f
        (↑((Equiv.trans equivSubtype
                  (Equiv.subtypeEquivRight (p := fun (i : ℕ) ↦ i < n) (q := Membership.mem (range n)) ⋯) :
                (a : Fin n) → ↥(range n))
              x) :
          ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
inst : CommMonoid α
f : ℕ → α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (∏ i ∈ (range n).attach, f (↑i : ℕ)) (∏ i ∈ range n, f i)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (∏ x ∈ range n, f x) (∏ i ∈ range n, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ↥(range n), f (↑i : ℕ)) (∏ i ∈ range n, f i)

Tactic:
rw [← attach_eq_univ, prod_attach]

Premises used: Finset.attach_eq_univ, Finset.prod_attach
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
β : Type u_2
inst : CommMonoid β
n : ℕ
c : Fin n → β
rw : ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) univ x → c x = if h : (↑x : ℕ) < n then c ⟨(↑x : ℕ), h⟩ else 1
⊢ Eq.{u_2 + 1} (α := β) (∏ i : Fin n, c i) (∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1)

Tactic:
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]

Premises used: Finset.prod_congr, Fin.prod_univ_eq_prod_range, rfl
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
β : Type u_2
inst : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
h : Membership.mem (γ := Finset (Fin n)) univ (⟨i, hi⟩ : Fin n)
⊢ c (⟨i, hi⟩ : Fin n) = if h : (↑(⟨i, hi⟩ : Fin n) : ℕ) < n then c ⟨(↑(⟨i, hi⟩ : Fin n) : ℕ), h⟩ else 1

Tactic:
simp only [hi, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
f : α → M
h : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ Set.toFinset {x : α | p x}, f a) (∏ a : Subtype p, f (↑a : α))

Tactic:
rw [← Finset.prod_subtype]

Premises used: Finset.prod_subtype
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
f : α → M
h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | p x} x ↔ p x
⊢ ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x

Tactic:
simp_rw [Set.mem_toFinset]

Premises used: Set.mem_toFinset
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
f : α → M
x : α
⊢ Membership.mem (γ := Set α) {x : α | p x} x ↔ p x

Tactic:
rfl
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
simp :
  HMul.hMul (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) ⋯) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) ⋯) =
    HMul.hMul (α := β) (∏ a : { a : α // p a }, f (↑a : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)
⊢ ∏ a : α, dite (p a) (f a) (g a) =
    HMul.hMul (α := β) (∏ a : { a : α // p a }, f (↑a : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)

Tactic:
simp only [prod_dite]

Premises used: Fintype.prod_dite
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
e_a : Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) ⋯) (∏ a : { a : α // p a }, f (↑a : α) ⋯)
e_a₁ : Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)
⊢ HMul.hMul (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) ⋯) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) ⋯) =
    HMul.hMul (α := β) (∏ a : { a : α // p a }, f (↑a : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)

Tactic:
congr 1
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {x : α | p x} x ↔ p x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) ⋯) (∏ a : { a : α // p a }, f (↑a : α) ⋯)

Tactic:
exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // p x } => f x x.2

Premises used: Equiv.subtypeEquivRight, Equiv.prod_comp, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ ∀ (x : α), Membership.mem (γ := Finset α) {x : α | ¬p x} x ↔ ¬p x

Tactic:
simp
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
inst_2 : CommMonoid β
f : (a : α) → p a → β
g : (a : α) → ¬p a → β
⊢ Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)

Tactic:
exact (Equiv.subtypeEquivRight <| by simp).prod_comp fun x : { x // ¬p x } => g x x.2

Premises used: Equiv.subtypeEquivRight, Equiv.prod_comp, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α₁ : Type u_4
α₂ : Type u_5
M : Type u_6
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid M
f : α₁ → M
g : α₂ → M
⊢ ∏ x : α₁ ⊕ α₂, Sum.elim f g x = HMul.hMul (α := M) (∏ a₁ : α₁, f a₁) (∏ a₂ : α₂, g a₂)

Tactic:
prod_disjSum _ _ _

Premises used: Finset.univ, Finset.disjSum, Finset.prod_disjSum, Sum.elim
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
α₁ : Type u_4
α₂ : Type u_5
M : Type u_6
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid M
f : α₁ ⊕ α₂ → M
⊢ ∏ x : α₁ ⊕ α₂, f x = HMul.hMul (α := M) (∏ a₁ : α₁, f (Sum.inl a₁)) (∏ a₂ : α₂, f (Sum.inr a₂))

Tactic:
prod_disjSum _ _ _

Premises used: Finset.univ, Finset.disjSum, Finset.prod_disjSum
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid γ
f : α₁ × α₂ → γ
⊢ Eq.{u_3 + 1} (α := γ) (∏ x : α₁ × α₂, f x) (∏ x : α₁, ∏ y : α₂, f (x, y))

Tactic:
Finset.prod_product ..

Premises used: Finset.univ, Finset.prod_product
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid γ
f : α₁ → α₂ → γ
⊢ Eq.{u_3 + 1} (α := γ) (∏ x : α₁ × α₂, f x.1 x.2) (∏ x : α₁, ∏ y : α₂, f x y)

Tactic:
Finset.prod_product' ..

Premises used: Finset.univ, Finset.prod_product'
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid γ
f : α₁ × α₂ → γ
⊢ Eq.{u_3 + 1} (α := γ) (∏ x : α₁ × α₂, f x) (∏ y : α₂, ∏ x : α₁, f (x, y))

Tactic:
Finset.prod_product_right ..

Premises used: Finset.univ, Finset.prod_product_right
-- Module: Mathlib.Data.Fintype.BigOperators
Goal:
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : CommMonoid γ
f : α₁ → α₂ → γ
⊢ Eq.{u_3 + 1} (α := γ) (∏ x : α₁ × α₂, f x.1 x.2) (∏ y : α₂, ∏ x : α₁, f x y)

Tactic:
Finset.prod_product_right' ..

Premises used: Finset.univ, Finset.prod_product_right'
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
⊢ card.{u_1} { x : α // p x } = #s

Tactic:
Multiset.card_pmap _ _ _

Premises used: Fintype.card, Multiset.card_pmap, Multiset.pmap, Finset.card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst : Fintype { x : α // p x }
rw : card.{u_1} { x : α // p x } = card.{u_1} { x : α // p x }
⊢ card.{u_1} { x : α // p x } = #s

Tactic:
rw [← subtype_card s H]

Premises used: Fintype.subtype_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : α → Prop
s : Finset α
H : ∀ (x : α), x ∈ s ↔ p x
inst : Fintype { x : α // p x }
⊢ card.{u_1} { x : α // p x } = card.{u_1} { x : α // p x }

Tactic:
congr!
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
⊢ card.{u_1} (↑p : Type u_1) = #s

Tactic:
Fintype.subtype_card s H

Premises used: Fintype.subtype_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst : Fintype (↑p : Type u_1)
rw : card.{u_1} (↑p : Type u_1) = card.{u_1} (↑p : Type u_1)
⊢ card.{u_1} (↑p : Type u_1) = #s

Tactic:
rw [← card_ofFinset s H]

Premises used: Fintype.card_ofFinset
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
inst : Fintype (↑p : Type u_1)
⊢ card.{u_1} (↑p : Type u_1) = card.{u_1} (↑p : Type u_1)

Tactic:
congr!
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
f : α ≃ β
⊢ card β = card α

Tactic:
Multiset.card_map _ _

Premises used: Multiset.map, Fintype.card, Finset.card, Multiset.card_map
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
f : α ≃ β
rw : card β = card β
⊢ card α = card β

Tactic:
rw [← ofEquiv_card f]

Premises used: Fintype.ofEquiv_card
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
f : α ≃ β
⊢ card β = card β

Tactic:
congr!
-- Module: Mathlib.Data.Fintype.Card
Goal:
α β : Type u_4
inst : Fintype α
inst_1 : Fintype β
h : α = β
rw rw₁ : β ≃ β
⊢ α ≃ β

Tactic:
rw [h]
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
a : α
inst : Subsingleton α
⊢ card α = 1

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Unique α
h : Fintype α
⊢ card α = 1

Tactic:
Subsingleton.elim (ofSubsingleton default) h ▸ card_ofSubsingleton _

Premises used: Inhabited.default, Fintype.ofSubsingleton, Eq.rec, Fintype.card_ofSubsingleton, Subsingleton.elim
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : IsEmpty α
⊢ card α = 0

Tactic:
rfl

Premises used: Fintype.card, Finset.card, Multiset.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_4
s : Set α
inst : Fintype (↑s : Type u_4)
⊢ #s.toFinset = Fintype.card.{u_4} (↑s : Type u_4)

Tactic:
Multiset.card_map Subtype.val Finset.univ.val

Premises used: Finset.univ, Multiset.map, Fintype.card, Finset.val, Finset.card, Subtype.val, Multiset.card_map
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (α := α) univ = Fintype.card α

Tactic:
rfl

Premises used: Fintype.card, rfl
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
hs : #s = Fintype.card α
rw : card.{u_1} (α := α) univ ≤ Fintype.card α
rw₁ rw₂ : Fintype.card α ≤ Fintype.card α
⊢ card.{u_1} (α := α) univ ≤ #s

Tactic:
rw [hs, Finset.card_univ]

Premises used: Finset.card_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (α := α) univ = Fintype.card α

Tactic:
Finset.card_univ

Premises used: Finset.card_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
⊢ card.{u_1} (α := α) univ = Fintype.card α

Tactic:
exact Finset.card_univ

Premises used: Finset.card_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ #s ≤ Fintype.card α

Tactic:
card_le_card (subset_univ s)

Premises used: Finset.card_le_card, Fintype.card, Finset.subset_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
x : α
hx : x ∉ s
⊢ #s < Fintype.card α

Tactic:
card_lt_card ⟨subset_univ s, not_forall.2 ⟨x, fun hx' => hx (hx' <| mem_univ x)⟩⟩

Premises used: Iff.mpr, Finset.mem_univ, Fintype.card, Finset.card_lt_card, And.intro, Exists.intro, Classical.not_forall, Finset.subset_univ
-- Module: Mathlib.Data.Fintype.Card
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
⊢ #s < Fintype.card α ↔ s ≠ univ

Tactic:
s.card_le_univ.lt_iff_ne.trans (not_congr s.card_eq_iff_eq_univ)

Premises used: Finset.card_eq_iff_eq_univ, Finset.card_le_univ, LE.le.lt_iff_ne, Iff.trans, not_congr