awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = if a ∈ s i then ∏ b ∈ erase univ i, #(s b) else 0
have pos : ∀ (h : a ∈ s i), #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ b ∈ erase univ i, #(s b)
Tactic: split_ifs with h
-- 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
pos : ∀ (h : a ∈ s i), #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ b ∈ erase univ i, #(s b)
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = if a ∈ s i then ∏ b ∈ erase univ i, #(s b) else 0
have neg : ∀ (h : a ∉ s i), #({f ∈ piFinset (δ := α) s | f i = a}) = 0
Tactic: split_ifs with h
-- 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
h : a ∈ s i
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = ∏ b ∈ erase univ i, #(s b)
have pos : Eq (α := ℕ) (∏ j ∈ erase univ i, #(s j)) (∏ b ∈ erase univ i, #(s b))
Tactic: rw [card_filter_piFinset_eq_of_mem _ _ h]
-- 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
h : a ∉ s i
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = 0
have neg : Finset.card (α := (a : ι) → α a) ∅ = 0
Tactic: rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]
-- 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
h : a ∉ s i
neg : Finset.card (α := (a : ι) → α a) ∅ = 0
⊢ #({f ∈ piFinset (δ := α) s | f i = a}) = 0
have neg₁ : Eq (α := ℕ) 0 0
Tactic: rw [filter_piFinset_of_notMem _ _ _ h, Finset.card_empty]
-- 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 : ι
j : κ
⊢ (if j ∈ s then ∏ b ∈ erase univ i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
have rw : (if j ∈ s then #s ^ #(erase univ i) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
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 : ι
j : κ
rw : (if j ∈ s then #s ^ #(erase univ i) 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
have rw₁ : (if j ∈ s then #s ^ (Finset.card.{u_4} (α := ι) univ - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
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 : ι
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
⊢ (if j ∈ s then ∏ b ∈ erase univ i, #s else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
have rw₂ : (if j ∈ s then #s ^ (card ι - 1) else 0) = if j ∈ s then #s ^ (card ι - 1) else 0
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_1
inst : Fintype α
n : ℕ
⊢ Fintype.card.{u_1} (List.Vector α n) = Fintype.card α ^ n
have rw : Fintype.card.{u_1} (Fin n → α) = Fintype.card α ^ n
Tactic: rw [Fintype.ofEquiv_card]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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)
have a : {x ∈ T | x.length = s} ⊆ image (α := Fin s → α) List.ofFn univ
Tactic: apply Finset.card_le_card
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s
have _ : #({x ∈ T | x.length = s}) ≤ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ)
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]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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)
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s
have _₁ : card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ) = 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]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
inst : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s
have _ : #({x ∈ T | x.length = s}) ≤ card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ)
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]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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)
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s
have _₁ : card.{u_1} (α := List α) (image (α := Fin s → α) List.ofFn univ) = 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]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : ℕ → α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ↥(range n), f (↑i : ℕ)) (∏ i ∈ range n, f i)
have rw : Eq.{u_1 + 1} (α := α) (∏ i ∈ (range n).attach, f (↑i : ℕ)) (∏ i ∈ range n, f i)
Tactic: rw [← attach_eq_univ, prod_attach]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
inst : CommMonoid α
f : ℕ → α
n : ℕ
rw : Eq.{u_1 + 1} (α := α) (∏ i ∈ (range n).attach, f (↑i : ℕ)) (∏ i ∈ range n, f i)
⊢ Eq.{u_1 + 1} (α := α) (∏ i : ↥(range n), f (↑i : ℕ)) (∏ i ∈ range n, f i)
have rw₁ : Eq.{u_1 + 1} (α := α) (∏ x ∈ range n, f x) (∏ i ∈ range n, f i)
Tactic: rw [← attach_eq_univ, prod_attach]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
β : Type u_2
inst : CommMonoid β
n : ℕ
c : Fin n → β
⊢ Eq.{u_2 + 1} (α := β) (∏ i : Fin n, c i) (∏ i ∈ range n, if h : i < n then c ⟨i, h⟩ else 1)
have rw : ∀ (x : Fin n), Membership.mem (γ := Finset (Fin n)) univ x → c x = if h : (↑x : ℕ) < n then c ⟨(↑x : ℕ), h⟩ else 1
Tactic: rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
Goal:
α : Type u_1
M : Type u_4
inst : CommMonoid M
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
f : α → M
⊢ Eq.{u_4 + 1} (α := M) (∏ a ∈ Set.toFinset {x : α | p x}, f a) (∏ a : Subtype p, f (↑a : α))
have h : ∀ (x : α), Membership.mem (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
Tactic: rw [← Finset.prod_subtype]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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 (γ := Finset α) (Set.toFinset {x : α | p x}) x ↔ p x
have h : ∀ (x : α), Membership.mem (γ := Set α) {x : α | p x} x ↔ p x
Tactic: simp_rw [Set.mem_toFinset]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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 → β
⊢ ∏ a : α, dite (p a) (f a) (g a) =
    HMul.hMul (α := β) (∏ a : { a : α // p a }, f (↑a : α) ⋯) (∏ a : { a : α // ¬p a }, g (↑a : α) ⋯)
have simp : HMul.hMul (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) sorry) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) sorry) =
  HMul.hMul (α := β) (∏ a : { a : α // p a }, f (↑a : α) sorry) (∏ a : { a : α // ¬p a }, g (↑a : α) sorry)
Tactic: simp only [prod_dite]
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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 → β
⊢ 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 : α) ⋯)
have e_a : Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | p x}, f (↑x : α) sorry) (∏ a : { a : α // p a }, f (↑a : α) sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Fintype.BigOperators (goal)
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 : α) ⋯)
⊢ 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 : α) ⋯)
have e_a₁ : Eq.{u_2 + 1} (α := β) (∏ x : ↥{x : α | ¬p x}, g (↑x : α) sorry) (∏ a : { a : α // ¬p a }, g (↑a : α) sorry)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
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 } = #s
have rw : card.{u_1} { x : α // p x } = card.{u_1} { x : α // p x }
Tactic: rw [← subtype_card s H]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
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) = #s
have rw : card.{u_1} (↑p : Type u_1) = card.{u_1} (↑p : Type u_1)
Tactic: rw [← card_ofFinset s H]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
β : Type u_5
inst : Fintype α
inst_1 : Fintype β
f : α ≃ β
⊢ card α = card β
have rw : card β = card β
Tactic: rw [← ofEquiv_card f]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α β : Type u_4
inst : Fintype α
inst_1 : Fintype β
h : α = β
⊢ α ≃ β
have rw : β ≃ β
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
hs : #s = Fintype.card α
⊢ card.{u_1} (α := α) univ ≤ #s
have rw : card.{u_1} (α := α) univ ≤ Fintype.card α
Tactic: rw [hs, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Finset α
hs : #s = Fintype.card α
rw : card.{u_1} (α := α) univ ≤ Fintype.card α
⊢ card.{u_1} (α := α) univ ≤ #s
have rw₁ : Fintype.card α ≤ Fintype.card α
Tactic: rw [hs, Finset.card_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ #s + #sᶜ = Fintype.card α
have rw : #s + (Fintype.card α - #s) = Fintype.card α
Tactic: rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
rw : #s + (Fintype.card α - #s) = Fintype.card α
⊢ #s + #sᶜ = Fintype.card α
have rw₁ : #s + Fintype.card α - #s = Fintype.card α
Tactic: rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
rw : #s + (Fintype.card α - #s) = Fintype.card α
rw₁ : #s + Fintype.card α - #s = Fintype.card α
⊢ #s + #sᶜ = Fintype.card α
have rw₂ : Fintype.card α = Fintype.card α
Tactic: rw [Finset.card_compl, ← Nat.add_sub_assoc (card_le_univ s), Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
⊢ #sᶜ + #s = Fintype.card α
have rw : #s + #sᶜ = Fintype.card α
Tactic: rw [Nat.add_comm, card_add_card_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
s : Finset α
rw : #s + #sᶜ = Fintype.card α
⊢ #sᶜ + #s = Fintype.card α
have rw₁ : Fintype.card α = Fintype.card α
Tactic: rw [Nat.add_comm, card_add_card_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have rw : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
Tactic: rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
rw : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have rw₁ : #sᶜ.toFinset = card α - #s.toFinset
Tactic: rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
rw : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
rw₁ : #sᶜ.toFinset = card α - #s.toFinset
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have rw₂ : #sᶜ.toFinset = #s.toFinsetᶜ
Tactic: rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
rw : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
rw₁ : #sᶜ.toFinset = card α - #s.toFinset
rw₂ : #sᶜ.toFinset = #s.toFinsetᶜ
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have rw₃ : #s.toFinsetᶜ = #s.toFinsetᶜ
Tactic: rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have classical : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
Tactic: classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
classical : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have classical₁ : #sᶜ.toFinset = card α - #s.toFinset
Tactic: classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
classical : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
classical₁ : #sᶜ.toFinset = card α - #s.toFinset
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have classical₂ : #sᶜ.toFinset = #s.toFinsetᶜ
Tactic: classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
inst_2 : Fintype (↑sᶜ : Type u_1)
classical : #sᶜ.toFinset = card α - card.{u_1} (↑s : Type u_1)
classical₁ : #sᶜ.toFinset = card α - #s.toFinset
classical₂ : #sᶜ.toFinset = #s.toFinsetᶜ
⊢ card.{u_1} (↑sᶜ : Type u_1) = card α - card.{u_1} (↑s : Type u_1)
have classical₃ : #s.toFinsetᶜ = #s.toFinsetᶜ
Tactic: classical rw [← Set.toFinset_card, ← Set.toFinset_card, ← Finset.card_compl, Set.toFinset_compl]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
h : Fintype (↑Set.univ : Type u_1)
⊢ card.{u_1} (↑Set.univ : Type u_1) = card α
have H : ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ Membership.mem (γ := Set α) Set.univ x
Tactic: apply Fintype.card_of_finset'
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
h : Fintype { _a : α // True }
⊢ card.{u_1} { _a : α // True } = card α
have H : ∀ (x : α), Membership.mem (γ := Finset α) univ x ↔ True
Tactic: apply Fintype.card_of_subtype
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Finite α
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
have intro : ∀ (val : Fintype α), ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
have intro : ∀ (l : List α) (e : ⟦l⟧ = Finset.val univ), ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
Tactic: obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (hypothesis)
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
l : List α
e : ⟦l⟧ = Finset.val univ
⊢ ∃ (l : List α), l.Nodup ∧ ∀ (x : α), x ∈ l
have this : Multiset.Nodup.{u_4} (α := α) (Finset.val univ) ∧ ∀ (x : α), Membership.mem (γ := Multiset α) (Finset.val univ) x
Tactic: have := And.intro (@univ α _).2 (@mem_univ_val α _)
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Finite α
val : Fintype α
l : List α
e : ⟦l⟧ = Finset.val univ
this : Multiset.Nodup.{u_4} (α := α) (Finset.val univ) ∧ ∀ (x : α), Membership.mem (γ := Multiset α) (Finset.val univ) x
⊢ l.Nodup ∧ ∀ (x : α), x ∈ l
have rwa : ∀ (this : Multiset.Nodup ⟦l⟧ ∧ ∀ (x : α), x ∈ ⟦l⟧), l.Nodup ∧ ∀ (x : α), x ∈ l
Tactic: rwa [← e] at this
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
⊢ b ∉ map { toFun := f, inj' := h : α ↪ β } univ
have rwa : b ∉ (↑(map { toFun := f, inj' := h : α ↪ β } univ) : Set β)
Tactic: rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
rwa : b ∉ (↑(map { toFun := f, inj' := h : α ↪ β } univ) : Set β)
⊢ b ∉ map { toFun := f, inj' := h : α ↪ β } univ
have rwa₁ : b ∉ (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) '' (↑univ : Set α)
Tactic: rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
rwa : b ∉ (↑(map { toFun := f, inj' := h : α ↪ β } univ) : Set β)
rwa₁ : b ∉ (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) '' (↑univ : Set α)
⊢ b ∉ map { toFun := f, inj' := h : α ↪ β } univ
have rwa₂ : b ∉ Set.image.{u_1, u_2} (α := α) (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) Set.univ
Tactic: rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → β
h : Injective f
b : β
w : b ∉ Set.range f
rwa : b ∉ (↑(map { toFun := f, inj' := h : α ↪ β } univ) : Set β)
rwa₁ : b ∉ (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) '' (↑univ : Set α)
rwa₂ : b ∉ Set.image.{u_1, u_2} (α := α) (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β) Set.univ
⊢ b ∉ map { toFun := f, inj' := h : α ↪ β } univ
have rwa₃ : b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑{ toFun := f, inj' := h : α ↪ β } : (a : α) → β)
Tactic: rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ card α = 0 ↔ IsEmpty α
have rw : Finset.card.{u_1} (α := α) univ = 0 ↔ IsEmpty α
Tactic: rw [card, Finset.card_eq_zero, univ_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : Finset.card.{u_1} (α := α) univ = 0 ↔ IsEmpty α
⊢ card α = 0 ↔ IsEmpty α
have rw₁ : Eq.{u_1 + 1} (α := Finset α) univ ∅ ↔ IsEmpty α
Tactic: rw [card, Finset.card_eq_zero, univ_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
rw : Finset.card.{u_1} (α := α) univ = 0 ↔ IsEmpty α
rw₁ : Eq.{u_1 + 1} (α := Finset α) univ ∅ ↔ IsEmpty α
⊢ card α = 0 ↔ IsEmpty α
have rw₂ : IsEmpty α ↔ IsEmpty α
Tactic: rw [card, Finset.card_eq_zero, univ_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
⊢ (∃! a : α, p a) ↔ Finset.card.{u_4} (α := α) {x : α | p x} = 1
have rw : (∃! a : α, p a) ↔ ∃ (a : α), Eq (α := Finset α) {x : α | p x} {a}
Tactic: rw [Finset.card_eq_one]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_4
inst : Fintype α
p : α → Prop
inst_1 : DecidablePred p
⊢ (∃! a : α, p a) ↔ ∃ (a : α), Eq (α := Finset α) {x : α | p x} {a}
have refine : ∀ (x : α), ((fun (a : α) ↦ p a) x ∧ ∀ (y : α), (fun (a : α) ↦ p a) y → y = x) ↔ Eq (α := Finset α) {x : α | p x} {x}
Tactic: refine exists_congr fun x => ?_
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
⊢ 2 < card α ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
have simp_rw : 2 < Finset.card.{u_1} (α := α) univ ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Data.Fintype.Card (goal)
Goal:
α : Type u_1
inst : Fintype α
simp_rw : 2 < Finset.card.{u_1} (α := α) univ ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ 2 < card α ↔ ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
have simp_rw₁ : (∃ (a : α) (b : α) (c : α),
    Membership.mem (γ := Finset α) univ a ∧
      Membership.mem (γ := Finset α) univ b ∧ Membership.mem (γ := Finset α) univ c ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) ↔
  ∃ (a : α) (b : α) (c : α), a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]