  34  deriving DecidableEq, Repr, BEq, Fintype
  35
  36theorem hallmarkCount : Fintype.card HallmarkCluster = 5 := by decide
  37theorem modalityCount : Fintype.card TreatmentModality = 5 := by decide
  38theorem oncogeneCount : Fintype.card OncogeneFamily = 5 := by decide
  39
  40abbrev CancerTarget : Type :=
  41  HallmarkCluster × TreatmentModality × OncogeneFamily
  42
  43theorem cancerTargetCount : Fintype.card CancerTarget = 125 := by
  44  simp only [CancerTarget, Fintype.card_prod,
  45    hallmarkCount, modalityCount, oncogeneCount]
  46
  47theorem hallmark_surj : Function.Surjective (fun t : CancerTarget => t.1) := by
  48  intro x
  49  exact ⟨(x, TreatmentModality.surgery, OncogeneFamily.ras), rfl⟩
  50
  51theorem modality_surj :
  52    Function.Surjective (fun t : CancerTarget => t.2.1) := by
  53  intro x
  54  exact ⟨(HallmarkCluster.proliferation, x, OncogeneFamily.ras), rfl⟩
  55
  56theorem oncogene_surj :
  57    Function.Surjective (fun t : CancerTarget => t.2.2) := by
  58  intro x
  59  exact ⟨(HallmarkCluster.proliferation, TreatmentModality.surgery, x), rfl⟩
  60
  61/-- Multiplicative, not additive: 125 > 15 = 5+5+5. -/
  62theorem product_exceeds_sum :
  63    Fintype.card CancerTarget > Fintype.card HallmarkCluster
  64      + Fintype.card TreatmentModality
  65      + Fintype.card OncogeneFamily := by
  66  rw [cancerTargetCount, hallmarkCount, modalityCount, oncogeneCount]
  67  decide

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.