cardinality of Set.iUnion to sum of cardinalities (stuck)

Stream: new members

[Ilmārs Cīrulis]

import Mathlib

theorem THM: (⋃ r ∈ Finset.Icc 2 7, ⋃ t ∈ Finset.Icc 1 (500 / r ^ 3),
    {x | x = ![t, t * r, t * r ^ 2, t * r ^ 3]}).ncard = 94 := by
  sorry

Is there some lemma or something, that I'm missing?
My goal is to change these iUnion over these finite sets to sums of cardinalities over the finite sets.

Thank you!

[Ilmārs Cīrulis]

Probably will have to prove the finiteness of the sets anyway :thinking:

[Aaron Liu]

import Mathlib

theorem THM: (⋃ r ∈ Finset.Icc 2 7, ⋃ t ∈ Finset.Icc 1 (500 / r ^ 3),
    {x | x = ![t, t * r, t * r ^ 2, t * r ^ 3]}).ncard = 94 := by
  have h1 : Set.PairwiseDisjoint (Finset.Icc 2 7) fun r =>
      (Finset.Icc 1 (500 / r ^ 3)).biUnion fun t => {![t, t * r, t * r ^ 2, t * r ^ 3]} := by
    sorry
  have h2 (r : Nat) : Set.PairwiseDisjoint (Finset.Icc 1 (500 / r ^ 3)) fun t =>
      ({![t, t * r, t * r ^ 2, t * r ^ 3]} : Finset (Fin 4 → Nat)) := by
    sorry
  simp_rw [Set.setOf_eq_eq_singleton, ← Finset.mem_coe, ← Finset.coe_singleton,
    ← Finset.coe_biUnion, Set.ncard_coe_Finset]
  conv =>
    rw [Finset.card_biUnion h1]
    enter [1, 2, r]
    rw [Finset.card_biUnion (h2 r)]
    enter [2, t]
    rw [Finset.card_singleton]
  sorry

[Ilmārs Cīrulis]

Thank you very much! :heart: