awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)
⊢ Disjoint (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl)))
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
        (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr)))

Tactic:
exact disjoint_image_of_injective Subtype.val_injective
      (isCompl_range_inl_range_inr.disjoint.preimage f)

Premises used: Subtype.val_injective, Set.isCompl_range_inl_range_inr, DFunLike.coe, IsCompl.disjoint, Disjoint.preimage, Set.disjoint_image_of_injective
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
f : (↑s : Type u_1) ≃ (↑s : Type u_1) ⊕ (↑s : Type u_1)
⊢ #(↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
            (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
              (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inl))) :
        Type u_1) =
    #(↑(image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
            (preimage (β := (↑s : Type u_1) ⊕ (↑s : Type u_1))
              (⇑f : (a : (↑s : Type u_1)) → (↑s : Type u_1) ⊕ (↑s : Type u_1)) (range Sum.inr))) :
        Type u_1)

Tactic:
simp [mk_image_eq Subtype.val_injective]

Premises used: Subtype.val_injective, Cardinal.mk_image_eq
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
inl : ∀ (hs : s.Infinite), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
inr : ∀ (hs : s.Finite), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
obtain hs | hs := s.infinite_or_finite

Premises used: Set.infinite_or_finite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
hs.exists_union_disjoint_cardinal_eq_of_infinite

Premises used: Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Infinite
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
exact hs.exists_union_disjoint_cardinal_eq_of_infinite

Premises used: Set.Infinite.exists_union_disjoint_cardinal_eq_of_infinite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
⊢ Even #(hs.toFinset (s := s))

Tactic:
rw [ncard_eq_toFinset_card s hs] at he

Premises used: Set.ncard_eq_toFinset_card
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Finite
he : Even #(hs.toFinset (s := s))
inr :
  ∀ (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u) (hctu : #t = #u),
    ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he

Premises used: Finset.exists_disjoint_union_of_even_card
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Finite
he : Even #(hs.toFinset (s := s))
t u : Finset α
hutu : t ∪ u = hs.toFinset (s := s)
hdtu : Disjoint t u
hctu : #t = #u
h :
  (↑t : Set α) ∪ (↑u : Set α) = s ∧
    Disjoint (↑t : Set α) (↑u : Set α) ∧ #(↑(↑t : Set α) : Type u_1) = #(↑(↑u : Set α) : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
use t, u
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
hs : s.Finite
he : Even #(hs.toFinset (s := s))
t u : Finset α
hutu : t ∪ u = hs.toFinset (s := s)
hdtu : Disjoint t u
hctu : #t = #u
⊢ (↑t : Set α) ∪ (↑u : Set α) = s ∧
    Disjoint (↑t : Set α) (↑u : Set α) ∧ #(↑(↑t : Set α) : Type u_1) = #(↑(↑u : Set α) : Type u_1)

Tactic:
simp [← Finset.coe_union, *]

Premises used: Finset.coe_union
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
hs : s.Finite
inr inr₁ inr₂ :
  ∀ (he : Even #(hs.toFinset (s := s))),
    ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
inr₃ :
  ∀ (he : Even #(hs.toFinset (s := s))) (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u)
    (hctu : #t = #u), ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)
h :
  ∀ (he : Even #(hs.toFinset (s := s))) (t u : Finset α) (hutu : t ∪ u = hs.toFinset (s := s)) (hdtu : Disjoint t u)
    (hctu : #t = #u),
    (↑t : Set α) ∪ (↑u : Set α) = s ∧
      Disjoint (↑t : Set α) (↑u : Set α) ∧ #(↑(↑t : Set α) : Type u_1) = #(↑(↑u : Set α) : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
classical
  rw [ncard_eq_toFinset_card s hs] at he
  obtain ⟨t, u, hutu, hdtu, hctu⟩ := Finset.exists_disjoint_union_of_even_card he
  use t, u
  simp [← Finset.coe_union, *]

Premises used: Set.ncard_eq_toFinset_card, Finset.coe_union
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
obtain :
  ∀ (t u : Set α) (hutu : t ∪ u = s) (hdtu : Disjoint t u) (hctu : #(↑t : Type u_1) = #(↑u : Type u_1)),
    ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
obtain ⟨t, u, hutu, hdtu, hctu⟩ := exists_union_disjoint_cardinal_eq_of_even he

Premises used: Set.exists_union_disjoint_cardinal_eq_of_even
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩

Premises used: congrArg, Cardinal.toNat, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
he : Even s.ncard
t u : Set α
hutu : t ∪ u = s
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
⊢ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ t.ncard = u.ncard

Tactic:
exact ⟨t, u, hutu, hdtu, congrArg Cardinal.toNat hctu⟩
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
s : Set α
mpr : (∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)) → Even s.ncard
⊢ Even s.ncard ↔ ∃ (t : Set α) (u : Set α), t ∪ u = s ∧ Disjoint t u ∧ #(↑t : Type u_1) = #(↑u : Type u_1)

Tactic:
use exists_union_disjoint_cardinal_eq_of_even

Premises used: Set.exists_union_disjoint_cardinal_eq_of_even
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
mpr : ∀ (hfin : (t ∪ u).Finite), Even (t ∪ u).ncard
mpr₁ : ∀ (hnfin : (t ∪ u).Infinite), Even (t ∪ u).ncard
⊢ Even (t ∪ u).ncard

Tactic:
obtain hfin | hnfin := (t ∪ u).finite_or_infinite

Premises used: Set.finite_or_infinite, Union.union
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : (t ∪ u).Finite
⊢ t.Finite ∧ u.Finite

Tactic:
rw [finite_union] at hfin

Premises used: Set.finite_union
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
⊢ t.ncard = u.ncard

Tactic:
have hn : t.ncard = u.ncard := congrArg Cardinal.toNat hctu
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
mpr : Even (u.ncard + u.ncard)
⊢ Even (t ∪ u).ncard

Tactic:
rw [ncard_union_eq hdtu hfin.1 hfin.2, hn]

Premises used: Set.ncard_union_eq, And.right, And.left
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)

Tactic:
Even.add_self u.ncard

Premises used: Even.add_self, Set.ncard
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hfin : t.Finite ∧ u.Finite
hn : t.ncard = u.ncard
⊢ Even (u.ncard + u.ncard)

Tactic:
exact Even.add_self u.ncard

Premises used: Even.add_self, Set.ncard
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #(↑t : Type u_1) = #(↑u : Type u_1)
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Tactic:
simp [hnfin.ncard]

Premises used: Set.Infinite.ncard
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
rw :
  Eq (α := ℕ) (∑ᶠ (i : α) (_ : Membership.mem (γ := Set α) (⋃ i ∈ t, s i) i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
rw₁ : Eq (α := ℕ) (∑ᶠ (i : ι) (_ : i ∈ t) (j : α) (_ : j ∈ s i), 1) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
rw₂ rw₃ : Eq (α := ℕ) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard)
⊢ ncard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
rw [← finsum_one, finsum_mem_biUnion h ht hs, finsum_mem_congr rfl fun i hi ↦ finsum_one]

Premises used: finsum_one, finsum_mem_congr, finsum_mem_biUnion, rfl
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ ∀ (i : ι), Membership.mem (γ := Set ι) univ i → (s i).Finite

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
rw :
  ncard.{u_1} (α := α) (⋃ (i : ι), s i) =
    ncard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)
⊢ ncard.{u_1} (α := α) (⋃ (i : ι), s i) = ∑ᶠ (i : ι), (s i).ncard

Tactic:
rw [← finsum_mem_univ, ← finite_univ.ncard_biUnion (by simpa) (fun _ _ _ _ hab ↦ h hab)]

Premises used: finsum_mem_univ, Set.Finite.ncard_biUnion, Set.finite_univ
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : ∀ (i : ι), (s i).Finite
h : Pairwise (Disjoint on s)
⊢ ncard.{u_1} (α := α) (⋃ (i : ι), s i) =
    ncard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg : ∀ (h : ∃ i ∈ t, (s i).Infinite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
by_cases! h : ∀ i ∈ t, (s i).Finite
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
⊢ Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)

Tactic:
have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∀ i ∈ t, (s i).Finite
this : Set.Finite.{u_1} (α := α) (⋃ i ∈ t, s i)
pos : Eq (α := ℕ∞) (↑(ncard.{u_1} (α := α) (⋃ i ∈ t, s i)) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
pos₁ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard)
pos₂ : Eq (α := ℕ∞) (↑(∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard) : ℕ∞) (∑ᶠ (i : ι) (_ : i ∈ t), (↑(s i).ncard : ℕ∞))
pos₃ pos₄ : Eq (α := ℕ∞) (∑ᶠ (x : ι) (_ : x ∈ t), (↑(s x).ncard : ℕ∞)) (∑ᶠ (i : ι) (_ : i ∈ t), (↑(s i).ncard : ℕ∞))
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]

Premises used: Nat.cast_finsum_mem, finsum_mem_congr, Set.Finite.ncard_biUnion, Set.Finite.cast_ncard_eq, rfl
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
h : ∃ i ∈ t, (s i).Infinite
neg :
  ∀ (i : ι) (hi : i ∈ t) (hn : (s i).Infinite),
    encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
neg :
  encard.{u_1} (α := α) (⋃ i_1 ∈ insert i (t \ {i}), s i_1) =
    (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]

Premises used: Set.mem_singleton, Set.notMem_diff_of_mem, Set.Finite.diff, finsum_mem_insert, Set.insert_diff_self_of_mem
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
i : ι
hi : i ∈ t
hn : (s i).Infinite
⊢ encard.{u_1} (α := α) (⋃ i_1 ∈ insert i (t \ {i}), s i_1) =
    (s i).encard + ∑ᶠ (i_1 : ι) (_ : i_1 ∈ t \ {i}), (s i_1).encard

Tactic:
simp [hn]
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : t.PairwiseDisjoint s
pos : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg : ∀ (h : ¬∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
pos₁ : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg₁ : ∀ (h : ¬∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
pos₂ : ∀ (h : ∀ i ∈ t, (s i).Finite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
neg₂ neg₃ : ∀ (h : ∃ i ∈ t, (s i).Infinite), encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
classical
  by_cases! h : ∀ i ∈ t, (s i).Finite
  · have : (⋃ i ∈ t, s i).Finite := ht.biUnion (fun i hi ↦ h i hi)
    rw [← this.cast_ncard_eq, ncard_biUnion ht h hs,
      ← finsum_mem_congr rfl fun i hi ↦ (h i hi).cast_ncard_eq, Nat.cast_finsum_mem ht]
  · obtain ⟨i, hi, (hn : (s i).Infinite)⟩ := h
    rw [← Set.insert_diff_self_of_mem hi,
      finsum_mem_insert _ (notMem_diff_of_mem <| mem_singleton i) ht.diff]
    simp [hn]

Premises used: Nat.cast_finsum_mem
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
rw :
  encard.{u_1} (α := α) (⋃ (i : ι), s i) =
    encard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)
⊢ encard.{u_1} (α := α) (⋃ (i : ι), s i) = ∑ᶠ (i : ι), (s i).encard

Tactic:
rw [← finsum_mem_univ, ← finite_univ.encard_biUnion (fun a _ b _ hab ↦ hs hab)]

Premises used: finsum_mem_univ, Set.finite_univ, Set.Finite.encard_biUnion
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
hs : Pairwise (Disjoint on s)
⊢ encard.{u_1} (α := α) (⋃ (i : ι), s i) =
    encard.{u_1} (α := α) (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), s i)

Tactic:
simp
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
⊢ ncard.{u_1} (α := α) (⋃ i ∈ t, s i) ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
simpa [← finsum_mem_eq_finite_toFinset_sum] using ht.toFinset.set_ncard_biUnion_le s

Premises used: finsum_mem_eq_finite_toFinset_sum, Finset.set_ncard_biUnion_le, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
⊢ encard.{u_1} (α := α) (⋃ i ∈ t, s i) ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
simpa [← finsum_mem_eq_finite_toFinset_sum] using ht.toFinset.set_encard_biUnion_le s

Premises used: Finset.set_encard_biUnion_le, finsum_mem_eq_finite_toFinset_sum, Set.Finite.toFinset
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Fintype ι
s : ι → Set α
⊢ ncard.{u_1} (α := α) (⋃ (i : ι), s i) ≤ ∑ i : ι, (s i).ncard

Tactic:
simpa using Finset.univ.set_ncard_biUnion_le s

Premises used: Finset.univ, Finset.set_ncard_biUnion_le
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Fintype ι
s : ι → Set α
⊢ encard.{u_1} (α := α) (⋃ (i : ι), s i) ≤ ∑ i : ι, (s i).encard

Tactic:
simpa using Finset.univ.set_encard_biUnion_le s

Premises used: Finset.set_encard_biUnion_le, Finset.univ
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
⊢ ncard.{u_1} (α := α) (⋃ (i : ι), s i) ≤ ∑ᶠ (i : ι), (s i).ncard

Tactic:
simpa using finite_univ.ncard_biUnion_le s

Premises used: Set.Finite.ncard_biUnion_le, Set.finite_univ
-- Module: Mathlib.Data.Set.Card.Arithmetic
Goal:
α : Type u_1
ι : Type u_2
inst : Finite ι
s : ι → Set α
⊢ encard.{u_1} (α := α) (⋃ (i : ι), s i) ≤ ∑ᶠ (i : ι), (s i).encard

Tactic:
simpa using finite_univ.encard_biUnion_le s

Premises used: Set.finite_univ, Set.Finite.encard_biUnion_le
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_3
rw : ENat.card.{u_3} (↑univ : Type u_3) = ENat.card α
rw₁ rw₂ : ENat.card α = ENat.card α
⊢ encard.{u_3} (α := α) univ = ENat.card α

Tactic:
rw [encard, ENat.card_congr (Equiv.Set.univ α)]

Premises used: ENat.card_congr, Set.encard, Equiv.Set.univ
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ ENat.card.{u_1} (↑s : Type u_1) = s.encard

Tactic:
rfl

Premises used: Set.encard, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Finite
have : ∀ (this : Fintype (↑s : Type u_1)), s.encard = (↑h.toFinset (s := s).card : ℕ∞)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)

Tactic:
have := h.fintype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Finite
this : Fintype (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = (↑h.toFinset (s := s).card : ℕ∞)
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑h.toFinset (s := s).card : ℕ∞)
rw₂ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑s.toFinset.card : ℕ∞)
rw₃ rw₄ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞)
⊢ s.encard = (↑h.toFinset (s := s).card : ℕ∞)

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, toFinite_toFinset, toFinset_card]

Premises used: Set.encard, Set.toFinite_toFinset, Set.toFinset_card, ENat.card_eq_coe_fintype_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ s.Finite

Tactic:
have h := toFinite s
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
h : s.Finite
rw : Eq (α := ℕ∞) (↑h.toFinset (s := s).card : ℕ∞) (↑s.toFinset.card : ℕ∞)
rw₁ rw₂ : Eq (α := ℕ∞) (↑s.toFinset.card : ℕ∞) (↑s.toFinset.card : ℕ∞)
⊢ s.encard = (↑s.toFinset.card : ℕ∞)

Tactic:
rw [h.encard_eq_coe_toFinset_card, toFinite_toFinset]

Premises used: Set.toFinite_toFinset, Set.Finite.encard_eq_coe_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Cardinal.mk (↑s : Type u_1)) = s.encard

Tactic:
rfl

Premises used: Set.encard, ENat.card, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
P : α → Prop
⊢ (Cardinal.toENat : (a : Cardinal.{u_1}) → ℕ∞) (Cardinal.mk { x : α // P x }) = encard.{u_1} (α := α) {x : α | P x}

Tactic:
rfl

Premises used: Set.encard, Set.Mem, setOf, ENat.card, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
inst : Fintype (↑s : Type u_1)
⊢ (↑(Fintype.card.{u_1} (↑s : Type u_1)) : ℕ∞) = s.encard

Tactic:
simp [encard_eq_coe_toFinset_card]

Premises used: Set.encard_eq_coe_toFinset_card
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Finset α
rw : Eq (α := ℕ∞) (↑⋯.toFinset (s := (↑s : Set α)).card : ℕ∞) (↑s.card : ℕ∞)
⊢ (↑s : Set α).encard = (↑s.card : ℕ∞)

Tactic:
rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]

Premises used: Set.Finite.encard_eq_coe_toFinset_card, Finset.finite_toSet
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Finset α
⊢ Eq (α := ℕ∞) (↑⋯.toFinset (s := (↑s : Set α)).card : ℕ∞) (↑s.card : ℕ∞)

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Infinite
⊢ Infinite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := h.to_subtype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
rw : ENat.card.{u_1} (↑s : Type u_1) = ⊤
rw₁ rw₂ : Eq (α := ℕ∞) ⊤ ⊤
⊢ s.encard = ⊤

Tactic:
rw [encard, ENat.card_eq_top_of_infinite]

Premises used: Set.encard, ENat.card_eq_top_of_infinite
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : ENat.card.{u_1} (↑s : Type u_1) = 0 ↔ s = ∅
rw₁ : IsEmpty.{u_1 + 1} (↑s : Type u_1) ↔ s = ∅
rw₂ : (∀ (x : α), x ∉ s) ↔ s = ∅
rw₃ rw₄ : (∀ (x : α), x ∉ s) ↔ ∀ (x : α), x ∉ s
⊢ s.encard = 0 ↔ s = ∅

Tactic:
rw [encard, ENat.card_eq_zero_iff_empty, isEmpty_subtype, eq_empty_iff_forall_notMem]

Premises used: Set.encard, ENat.card_eq_zero_iff_empty, Set.eq_empty_iff_forall_notMem, isEmpty_subtype
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
rw rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
⊢ encard.{u_1} (α := α) ∅ = 0

Tactic:
rw [encard_eq_zero]

Premises used: Set.encard_eq_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard ≠ 0
rwa : s ≠ ∅
rwa₁ : ¬s = ∅
rwa₂ rwa₃ rwa₄ rwa₅ : ¬s.encard = 0
⊢ s.Nonempty

Tactic:
rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]

Premises used: Set.encard_eq_zero, Ne, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : ¬s.encard = 0 ↔ s.Nonempty
rw₁ : ¬s = ∅ ↔ s.Nonempty
rw₂ rw₃ : ¬s = ∅ ↔ s ≠ ∅
⊢ s.encard ≠ 0 ↔ s.Nonempty

Tactic:
rw [ne_eq, encard_eq_zero, nonempty_iff_ne_empty]

Premises used: Set.encard_eq_zero, ne_eq, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard ≠ 0 ↔ s.Nonempty
rw₁ rw₂ : s.Nonempty ↔ s.Nonempty
⊢ 0 < s.encard ↔ s.Nonempty

Tactic:
rw [pos_iff_ne_zero, encard_ne_zero]

Premises used: Set.encard_ne_zero, pos_iff_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ s.encard ≠ 0

Tactic:
(encard_pos.mpr ⟨a, h⟩).ne.symm

Premises used: Iff.mpr, Ne.symm, Exists.intro, Set.encard_pos, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
e : α
rw : ENat.card.{u_1} (↑{e} : Type u_1) = 1
rw₁ : Eq (α := ℕ∞) (↑(Fintype.card.{u_1} (↑{e} : Type u_1)) : ℕ∞) 1
rw₂ : Eq (α := ℕ∞) (↑1 : ℕ∞) 1
rw₃ rw₄ : Eq (α := ℕ∞) 1 1
⊢ encard (α := α) {e} = 1

Tactic:
rw [encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one]

Premises used: Set.encard, ENat.card_eq_coe_fintype_card, Fintype.card_ofSubsingleton, Nat.cast_one