Cardinality of subtype as a sum

Stream: Is there code for X?

[Heather Macbeth]

The sum of a characteristic function is the cardinality of the subtype it defines: is this (1) true, (2) in mathlib?

import set_theory.cardinal

universes u v
open_locale cardinal

example {α : Type v} (P : α → Prop) [∀ a, decidable (P a)] :
  cardinal.lift.{u} (#(subtype P)) = cardinal.sum (λ a, ite (P a) (1 : cardinal.{u}) 0) :=
sorry

[Scott Morrison]

import set_theory.cardinal

universes u v
open_locale cardinal

example {α : Type v} (P : α → Prop) [∀ a, decidable (P a)] :
  cardinal.lift.{u} (#(subtype P)) = cardinal.sum (λ a, ite (P a) (1 : cardinal.{u}) 0) :=
begin
  have : ∀ a, ite (P a) (1 : cardinal.{u}) 0 = #(ite (P a) punit pempty), sorry,
  simp [this],
  apply cardinal.eq.mpr,
  split,
end

seems like a plausible start.

[Scott Morrison]

import set_theory.cardinal

universes u v
open_locale cardinal

instance (P : Prop) [decidable P] : subsingleton (ite P punit pempty) :=
by { split_ifs; apply_instance }

def foo {α : Type v} (P : α → Prop) [∀ a, decidable (P a)] :
  ulift (subtype P) ≃ Σ (i : α), ite (P i) punit pempty :=
{ to_fun := λ x, ⟨x.1, by { erw [if_pos x.down.2], constructor, }⟩,
  inv_fun := λ x, by { cases x with a h, split_ifs at h with h₁ h₂, exact ⟨⟨a, h₁⟩⟩, cases h, },
  left_inv := λ x, by { rcases x with ⟨⟨a, h⟩⟩, dsimp, simp [dif_pos h], },
  right_inv := λ x, by { rcases x with ⟨a, h⟩, dsimp, split_ifs at h with h₁ h₂, { simp [h₁], apply subsingleton.helim, simp [h₁], }, cases h, }, }

example {α : Type v} (P : α → Prop) [∀ a, decidable (P a)] :
  cardinal.lift.{u} (#(subtype P)) = cardinal.sum (λ a, ite (P a) (1 : cardinal.{u}) 0) :=
begin
  have : ∀ a, ite (P a) (1 : cardinal.{u}) 0 = #(ite (P a) punit pempty),
  { intro a, split_ifs; simp, },
  simp [this],
  apply cardinal.eq.mpr,
  split,
  apply foo,
end

Ugly, but works.