Theorem: PMF.map_ofFintype (LeanCamCombi/Mathlib/Probability/ProbabilityMassFunction/Constructions.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
Tactic:
have :
  ((univ : Finset β) : Set β).PairwiseDisjoint fun b ↦
    univ.filter fun a : α ↦ g a = b := by
  refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
  simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
  exact hb (ha₁.symm.trans ha₂)
State after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ a : β, (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) a = 1
Tactic:
rw [← sum_disjiUnion _ _ this]
State after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ x ∈ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this, f x = 1

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ ∑ x ∈ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this, f x = 1
Tactic:
convert h
State after:
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this = univ

State before:
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
this : (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
⊢ univ.disjiUnion (fun b => Finset.filter (fun a => g a = b) univ) this = univ
Tactic:
exact eq_univ_of_forall fun a ↦
  mem_disjiUnion.2 ⟨_, mem_univ _, mem_filter.2 ⟨mem_univ _, rfl⟩⟩
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ (↑univ).PairwiseDisjoint fun b => Finset.filter (fun a => g a = b) univ
Tactic:
refine' fun b₁ _ b₂ _ hb ↦ disjoint_left.2 fun a ha₁ ha₂ ↦ _
State after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₁
ha₂ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₂
⊢ False

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₁
ha₂ : a ∈ (fun b => Finset.filter (fun a => g a = b) univ) b₂
⊢ False
Tactic:
simp only [mem_filter, mem_univ, true_and_iff] at ha₁ ha₂
State after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : g a = b₁
ha₂ : g a = b₂
⊢ False

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b₁ : β
x✝¹ : b₁ ∈ ↑univ
b₂ : β
x✝ : b₂ ∈ ↑univ
hb : b₁ ≠ b₂
a : α
ha₁ : g a = b₁
ha₂ : g a = b₂
⊢ False
Tactic:
exact hb (ha₁.symm.trans ha₂)
State after:
no goals

State before:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
⊢ map g (ofFintype f h) = ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯
Tactic:
ext b : 1
State after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯) b

State before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (map g (ofFintype f h)) b = (ofFintype (fun b => ∑ a ∈ Finset.filter (fun a => g a = b) univ, f a) ⋯) b
Tactic:
simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]
State after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0

State before:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ℝ≥0∞
h : ∑ a : α, f a = 1
g : α → β
b : β
⊢ (∑' (a : α), if b = g a then f a else 0) = ∑ a : α, if b = g a then f a else 0
Tactic:
exact tsum_eq_sum fun _ h ↦ (h $ mem_univ _).elim
State after:
no goals