awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α β : Type u
f : α → β
p : PMF α
⊢ f <$> p = map f p

Tactic:
rfl

Premises used: PMF.map, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ Eq (α := ℝ≥0∞) ((map f p : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    (∑' (a : α), if b = f a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞)

Tactic:
simp [map]

Premises used: PMF.map
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ b ∈ f '' p.support

Tactic:
simp [map, @eq_comm β b]

Premises used: PMF.map, eq_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
b : β
⊢ b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
⊢ p.bind (pure ∘ f) = map f p

Tactic:
rfl

Premises used: PMF.map, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
⊢ map id p = p

Tactic:
bind_pure _

Premises used: PMF.map, PMF.pure, PMF.bind_pure
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : PMF α
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p

Tactic:
simp [map, Function.comp_def]

Premises used: PMF.map, Function.comp_def
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f (pure a) = pure (f a)

Tactic:
pure_bind _ _

Premises used: PMF.map, PMF.pure_bind, PMF.pure
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : α → PMF β
f : β → γ
⊢ map f (p.bind q) = p.bind fun (a : α) ↦ map f (q a)

Tactic:
bind_bind _ _ _

Premises used: PMF.bind_bind, PMF.map
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → β
q : β → PMF γ
⊢ (map f p).bind q = p.bind (q ∘ f)

Tactic:
(bind_bind _ _ _).trans (congr_arg _ (funext fun _ => pure_bind _ _))

Premises used: PMF.bind_bind, PMF.map, PMF.pure_bind, congr_arg, funext, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
p : PMF α
b : β
⊢ map (Function.const α b) p = pure b

Tactic:
simp only [map, Function.comp_def, bind_const, Function.const]

Premises used: PMF.map, Function.comp_def, PMF.bind_const, Function.const
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
simp :
  Eq (α := ℝ≥0∞) (∑' (a : α), if f a ∈ s then (p : (a : α) → ℝ≥0∞) a else 0)
    (∑' (x : α), if x ∈ f ⁻¹' s then (p : (a : α) → ℝ≥0∞) x else 0)
⊢ Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]

Premises used: PMF.map, Set.indicator, Set.preimage, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), if f a ∈ s then (p : (a : α) → ℝ≥0∞) a else 0)
    (∑' (x : α), if x ∈ f ⁻¹' s then (p : (a : α) → ℝ≥0∞) x else 0)

Tactic:
rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
rw [toMeasure_apply_eq_toOuterMeasure_apply _ hs,
    toMeasure_apply_eq_toOuterMeasure_apply _ (measurableSet_preimage hf hs)]

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, measurableSet_preimage
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
toOuterMeasure_map_apply f p s

Premises used: PMF.toOuterMeasure_map_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : PMF α
s : Set β
mα : MeasurableSpace α
mβ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((map f p).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((p.toOuterMeasure : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)

Tactic:
exact toOuterMeasure_map_apply f p s

Premises used: PMF.toOuterMeasure_map_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
h :
  ∀ (s : Set β) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Measure β) (Measure.map f p.toMeasure) (map f p).toMeasure

Tactic:
ext s hs : 1
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
f : α → β
mα : MeasurableSpace α
mβ : MeasurableSpace β
p : PMF α
hf : Measurable f
s : Set β
hs : MeasurableSet s
h :
  Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
h₁ h₂ :
  Eq (α := ℝ≥0∞) (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
    (((p.toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((Measure.map f p.toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((map f p).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [PMF.toMeasure_map_apply _ _ _ hf hs, Measure.map_apply hf hs]

Premises used: MeasureTheory.Measure.map_apply, PMF.toMeasure_map_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α β : Type u
q : PMF (α → β)
p : PMF α
⊢ q <*> p = q.seq p

Tactic:
rfl

Premises used: PMF.seq, PMF.pure, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
simp :
  Eq (α := ℝ≥0∞)
    (∑' (a : α → β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (a_1 : α), if b = a a_1 then (p : (a : α) → ℝ≥0∞) a_1 else 0 : ℝ≥0∞))
    (∑' (f : α → β) (a : α),
      if b = f a then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      else 0)
⊢ Eq (α := ℝ≥0∞) ((q.seq p : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    (∑' (f : α → β) (a : α),
        if b = f a then
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        else 0 :
      ℝ≥0∞)

Tactic:
simp only [seq, mul_boole, bind_apply, pure_apply]

Premises used: mul_boole, PMF.seq, PMF.bind_apply, PMF.pure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α → β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (a_1 : α), if b = a a_1 then (p : (a : α) → ℝ≥0∞) a_1 else 0 : ℝ≥0∞))
    (∑' (f : α → β) (a : α),
      if b = f a then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      else 0)

Tactic:
tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)

Premises used: ENNReal.tsum_mul_left, tsum_congr, Eq.symm, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
refine :
  ∀ (f : α → β) (a : α),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞)
        (if b = f a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) =
      if b = f a then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      else 0
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α → β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (a_1 : α), if b = a a_1 then (p : (a : α) → ℝ≥0∞) a_1 else 0 : ℝ≥0∞))
    (∑' (f : α → β) (a : α),
      if b = f a then
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      else 0)

Tactic:
refine tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => ?_)

Premises used: ENNReal.tsum_mul_left, tsum_congr, Eq.symm, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
f : α → β
a : α
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞)
      (if b = f a then (p : (a : α) → ℝ≥0∞) a else 0 : ℝ≥0∞) =
    if b = f a then
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : α → β) → ℝ≥0∞) f : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
    else 0

Tactic:
simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0

Premises used: mul_ite, MulZeroClass.mul_zero, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ b ∈ (q.seq p).support ↔ Membership.mem (γ := Set β) (⋃ f ∈ q.support, f '' p.support) b

Tactic:
simp [-mem_support_iff, seq, @eq_comm β b]

Premises used: eq_comm, PMF.seq, PMF.mem_support_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
q : PMF (α → β)
p : PMF α
b : β
⊢ b ∈ (q.seq p).support ↔ ∃ f ∈ q.support, b ∈ f '' p.support

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ LawfulMonad PMF

Tactic:
LawfulMonad.mk'
  (bind_pure_comp := fun _ _ => rfl)
  (id_map := id_map)
  (pure_bind := pure_bind)
  (bind_assoc := bind_bind)

Premises used: PMF.bind_bind, PMF.pure_bind, LawfulMonad.mk', LawfulFunctor.id_map, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 : Type u
β_1 : Type v
e : α_1 ≃ β_1
a : PMF α_1
⊢ map.{v, u} (α := β_1) (⇑e.symm : (a : β_1) → α_1) (map (⇑e : (a : α_1) → β_1) a) = a

Tactic:
simp [map_comp, map_id]

Premises used: PMF.map_comp, PMF.map_id
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
α_1 : Type u
β_1 : Type v
e : α_1 ≃ β_1
a : PMF β_1
⊢ map.{u, v} (α := α_1) (⇑e : (a : α_1) → β_1) (map (⇑e.symm : (a : β_1) → α_1) a) = a

Tactic:
simp [map_comp, map_id]

Premises used: PMF.map_comp, PMF.map_id
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ (ofFinset f s h h' : (a : α) → ℝ≥0∞) a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ a ∈ (ofFinset f s h h').support ↔ a ∈ (↑s : Set α) ∩ Function.support f

Tactic:
simpa [mem_support_iff] using mt (h' a)

Premises used: mt, PMF.mem_support_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
a : α
⊢ a ∈ (ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
a : α
ha : a ∉ s
⊢ Eq (α := ℝ≥0∞) ((ofFinset f s h h' : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h' a ha
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
t : Set α
⊢ Eq (α := ℝ≥0∞) (((ofFinset f s h h').toOuterMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (x : α), t.indicator f x : ℝ≥0∞)

Tactic:
toOuterMeasure_apply (ofFinset f s h h') t

Premises used: PMF.ofFinset, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
h : Eq (α := ℝ≥0∞) (∑ a ∈ s, f a) 1
h' : ∀ a ∉ s, f a = 0
t : Set α
inst : MeasurableSpace α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((((ofFinset f s h h').toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (∑' (x : α), t.indicator f x : ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_ofFinset_apply h h' t)

Premises used: PMF.toOuterMeasure_ofFinset_apply, PMF.toMeasure_apply_eq_toOuterMeasure_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
a : α
⊢ (ofFintype f h : (a : α) → ℝ≥0∞) a = f a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
⊢ (ofFintype f h).support = Function.support f

Tactic:
rfl

Premises used: PMF.support, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
a : α
⊢ a ∈ (ofFintype f h).support ↔ f a ≠ 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, PMF.support, Function.support, Not
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Fintype α
f_1 : α → ℝ≥0∞
h_1 : Eq (α := ℝ≥0∞) (∑ a : α, f_1 a) 1
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
⊢ Eq (α := ℝ≥0∞) (∑ a : β, (fun (b : β) ↦ (∑ a : α with g a = b, f a : ℝ≥0∞)) a) 1

Tactic:
simpa [Finset.sum_fiberwise_eq_sum_filter univ univ g f]

Premises used: Finset.univ, Finset.sum_fiberwise_eq_sum_filter
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
h₁ :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) ((map g (ofFintype f h) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      ((ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
⊢ map g (ofFintype f h) = ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) ⋯

Tactic:
ext b : 1
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
b : β
h₁ : Eq (α := ℝ≥0∞) (∑' (a : α), if b = g a then f a else 0) (∑ a : α, if b = g a then f a else 0)
⊢ Eq (α := ℝ≥0∞) ((map g (ofFintype f h) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    ((ofFintype (fun (b : β) ↦ ∑ a : α with g a = b, f a) ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]

Premises used: eq_comm, Finset.sum_filter, PMF.ofFintype_apply, PMF.map_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
b : β
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), if b = g a then f a else 0) (∑ a : α, if b = g a then f a else 0)

Tactic:
tsum_eq_sum fun _ h ↦ (h <| mem_univ _).elim

Premises used: Finset.mem_univ, False.elim, tsum_eq_sum
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : Fintype α
inst_1 : Fintype β
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
g : α → β
b : β
⊢ Eq (α := ℝ≥0∞) (∑' (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

Premises used: Finset.mem_univ, False.elim, tsum_eq_sum
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
s : Set α
⊢ Eq (α := ℝ≥0∞) (((ofFintype f h).toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (x : α), s.indicator f x : ℝ≥0∞)

Tactic:
toOuterMeasure_apply (ofFintype f h) s

Premises used: PMF.ofFintype, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
inst : Fintype α
f : α → ℝ≥0∞
h : Eq (α := ℝ≥0∞) (∑ a : α, f a) 1
s : Set α
inst_1 : MeasurableSpace α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((ofFintype f h).toMeasure : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (x : α), s.indicator f x : ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply _ hs).trans (toOuterMeasure_ofFintype_apply h s)

Premises used: PMF.toMeasure_apply_eq_toOuterMeasure_apply, PMF.toOuterMeasure_ofFintype_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ∞
a : α
⊢ (normalize f hf0 hf : (a : α) → ℝ≥0∞) a = f a * (∑' (x : α), f x)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ∞
a : α
⊢ a ∈ (normalize f hf0 hf).support ↔ a ∈ Function.support f

Tactic:
simp [hf, mem_support_iff]

Premises used: PMF.mem_support_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ∞
a : α
⊢ a ∈ (normalize f hf0 hf).support ↔ f a ≠ 0

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
⊢ Ne (α := ℝ≥0∞) (tsum (s.indicator (⇑p : (a : α) → ℝ≥0∞))) 0

Tactic:
simpa using h
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw :
  (normalize (s.indicator (⇑p : (a : α) → ℝ≥0∞)) ⋯ ⋯ : (a : α) → ℝ≥0∞) a =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (x : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) x)⁻¹ =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹
⊢ (p.filter s h : (a : α) → ℝ≥0∞) a =
    HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹

Tactic:
rw [filter, normalize_apply]

Premises used: PMF.filter, PMF.normalize_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
ha : a ∉ s
rw :
  HMul.hMul (α := ℝ≥0∞) (s.indicator (⇑p : (a : α) → ℝ≥0∞) a) (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
rw₁ : HMul.hMul (α := ℝ≥0∞) 0 (∑' (a' : α), s.indicator (⇑p : (a : α) → ℝ≥0∞) a')⁻¹ = 0
rw₂ rw₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]

Premises used: Iff.mpr, MulZeroClass.zero_mul, absurd, PMF.filter_apply, Set.indicator_apply_eq_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ a ∈ (p.filter s h).support ↔ a ∈ s ∧ a ∈ p.support

Tactic:
(mem_support_normalize_iff _ _ _).trans Set.indicator_apply_ne_zero

Premises used: Set.Mem, PMF.mem_support_normalize_iff, PMF.filter, Iff.trans, Set.indicator_apply_ne_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
⊢ (p.filter s h).support = s ∩ p.support

Tactic:
Set.ext fun _ => mem_support_filter_iff _

Premises used: Set.ext, PMF.mem_support_filter_iff
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : a ∉ (p.filter s h).support ↔ a ∉ s ∨ a ∉ p.support
rw₁ : a ∉ s ∩ p.support ↔ a ∉ s ∨ a ∉ p.support
rw₂ : ¬(a ∈ s ∧ a ∈ p.support) ↔ a ∉ s ∨ a ∉ p.support
rw₃ rw₄ : a ∉ s ∨ a ∉ p.support ↔ a ∉ s ∨ a ∉ p.support
⊢ Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∉ s ∨ a ∉ p.support

Tactic:
rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]

Premises used: Set.mem_inter_iff, PMF.support_filter, PMF.apply_eq_zero_iff, not_and_or
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
rw : ¬Eq (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support
rw₁ : ¬(a ∉ s ∨ a ∉ p.support) ↔ a ∈ s ∧ a ∈ p.support
rw₂ : ¬a ∉ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
rw₃ : a ∈ s ∧ ¬a ∉ p.support ↔ a ∈ s ∧ a ∈ p.support
rw₄ rw₅ : a ∈ s ∧ a ∈ p.support ↔ a ∈ s ∧ a ∈ p.support
⊢ Ne (α := ℝ≥0∞) ((p.filter s h : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) ↔ a ∈ s ∧ a ∈ p.support

Tactic:
rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]

Premises used: Classical.not_not, PMF.filter_apply_eq_zero_iff, Ne, not_or
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0
h : p ≤ 1
⊢ Eq (α := ℝ≥0∞) (∑ a : Bool, (fun (b : Bool) ↦ bif b then (↑p : ℝ≥0∞) else 1 - (↑p : ℝ≥0∞)) a) 1

Tactic:
simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
simp : (bif b then (↑p : ℝ≥0∞) else 1 - (↑p : ℝ≥0∞)) = (↑(bif b then p else 1 - p) : ℝ≥0∞)
⊢ (bernoulli p h : (a : Bool) → ℝ≥0∞) b = (↑(bif b then p else 1 - p) : ℝ≥0∞)

Tactic:
simp only [bernoulli, ofFintype_apply]

Premises used: PMF.bernoulli, PMF.ofFintype_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bif b then (↑p : ℝ≥0∞) else 1 - (↑p : ℝ≥0∞)) = (↑(bif b then p else 1 - p) : ℝ≥0∞)

Tactic:
Eq.symm (Bool.apply_cond ofNNReal)

Premises used: ENNReal.ofNNReal, Bool.apply_cond, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ (bif b then (↑p : ℝ≥0∞) else 1 - (↑p : ℝ≥0∞)) = (↑(bif b then p else 1 - p) : ℝ≥0∞)

Tactic:
exact Eq.symm (Bool.apply_cond ofNNReal)

Premises used: ENNReal.ofNNReal, Bool.apply_cond, Eq.symm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
⊢ (bernoulli p h).support = {b : Bool | bif b then p ≠ 0 else p ≠ 1}

Tactic:
Set.ext fun b => ?_

Premises used: Set.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
refine :
  ∀ (b : Bool), b ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} b
⊢ (bernoulli p h).support = {b : Bool | bif b then p ≠ 0 else p ≠ 1}

Tactic:
refine Set.ext fun b => ?_

Premises used: Set.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Constructions
Goal:
p : ℝ≥0
h : p ≤ 1
b : Bool
false :
  Bool.false ∈ (bernoulli p h).support ↔
    Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} Bool.false
true :
  Bool.true ∈ (bernoulli p h).support ↔
    Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} Bool.true
⊢ b ∈ (bernoulli p h).support ↔ Membership.mem (γ := Set Bool) {b : Bool | bif b then p ≠ 0 else p ≠ 1} b

Tactic:
induction b