[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ ↑(map f p) b = ∑' (a : α), if b = f a then ↑p a else 0
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b✝ b : β
⊢ b ∈ support (map f p) ↔ b ∈ f '' support p
[PROOFSTEP]
simp [map, @eq_comm β b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ b ∈ support (map f p) ↔ ∃ a, a ∈ support p ∧ f a = b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
g : β → γ
⊢ map g (map f p) = map (g ∘ f) p
[PROOFSTEP]
simp [map, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
⊢ map (Function.const α b) p = pure b
[PROOFSTEP]
simp only [map, Function.comp, bind_const, Function.const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
[PROOFSTEP]
simp [map, Set.indicator, toOuterMeasure_apply p (f ⁻¹' s)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑↑(toMeasure (map f p)) s = ↑↑(toMeasure p) (f ⁻¹' s)
[PROOFSTEP]
rw [toMeasure_apply_eq_toOuterMeasure_apply _ s hs,
  toMeasure_apply_eq_toOuterMeasure_apply _ (f ⁻¹' s) (measurableSet_preimage hf hs)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
p : Pmf α
b : β
s : Set β
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
hf : Measurable f
hs : MeasurableSet s
⊢ ↑(toOuterMeasure (map f p)) s = ↑(toOuterMeasure p) (f ⁻¹' s)
[PROOFSTEP]
exact toOuterMeasure_map_apply f p s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ ↑(seq q p) b = ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
simp only [seq, mul_boole, bind_apply, pure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ (∑' (a : α → β), ↑q a * ∑' (a_1 : α), if b = a a_1 then ↑p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
refine' tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
f : α → β
a : α
⊢ (↑q f * if b = f a then ↑p a else 0) = if b = f a then ↑q f * ↑p a else 0
[PROOFSTEP]
simpa only [mul_zero] using mul_ite (b = f a) (q f) (p a) 0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b✝ b : β
⊢ b ∈ support (seq q p) ↔ b ∈ ⋃ (f : α → β) (_ : f ∈ support q), f '' support p
[PROOFSTEP]
simp [-mem_support_iff, seq, @eq_comm β b]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
q : Pmf (α → β)
p : Pmf α
b : β
⊢ b ∈ support (seq q p) ↔ ∃ f, f ∈ support q ∧ b ∈ f '' support p
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
s : Finset α
h : ∑ a in s, f a = 1
h' : ∀ (a : α), ¬a ∈ s → f a = 0
a : α
⊢ a ∈ support (ofFinset f s h h') ↔ a ∈ ↑s ∩ Function.support f
[PROOFSTEP]
simpa [mem_support_iff] using mt (h' a)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
s : Finset α
h : ∑ a in s, f a = 1
h' : ∀ (a : α), ¬a ∈ s → f a = 0
a : α
⊢ a ∈ support (ofFinset f s h h') ↔ a ∈ s ∧ f a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ support (normalize f hf0 hf) ↔ a ∈ Function.support f
[PROOFSTEP]
simp [hf, mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → ℝ≥0∞
hf0 : tsum f ≠ 0
hf : tsum f ≠ ⊤
a : α
⊢ a ∈ support (normalize f hf0 hf) ↔ f a ≠ 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
⊢ tsum (Set.indicator s ↑p) ≠ 0
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = Set.indicator s (↑p) a * (∑' (a' : α), Set.indicator s (↑p) a')⁻¹
[PROOFSTEP]
rw [filter, normalize_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
ha : ¬a ∈ s
⊢ ↑(filter p s h) a = 0
[PROOFSTEP]
rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, zero_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = 0 ↔ ¬a ∈ s ∨ ¬a ∈ support p
[PROOFSTEP]
erw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ support p
[PROOFSTEP]
rw [Ne.def, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
⊢ ∑ a : Bool, (fun b => bif b then p else 1 - p) a = 1
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ support (bernoulli p h) = {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
refine' Set.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b✝ b : Bool
⊢ b ∈ support (bernoulli p h) ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
induction b
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ false ∈ support (bernoulli p h) ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne.def, tsub_eq_zero_iff_le, not_le]
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
[PROOFSTEP]
exact ⟨ne_of_lt, lt_of_le_of_ne h⟩
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ true ∈ support (bernoulli p h) ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}
[PROOFSTEP]
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ b ∈ support (bernoulli p h) ↔ bif b then p ≠ 0 else p ≠ 1
[PROOFSTEP]
simp


[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ =
    Compatibility.τ₁
      (eqToIso (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
      (eqToIso
        (_ :
          (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
            Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
      N₁Γ₀
[PROOFSTEP]
ext K : 3
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Compatibility.τ₀.hom K =
    NatTrans.app
      (Compatibility.τ₁
          (eqToIso
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (eqToIso
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          N₁Γ₀).hom
      K
[PROOFSTEP]
simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app, eqToIso.hom]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app Preadditive.DoldKan.equivalence.counitIso.hom ((toKaroubiEquivalence (ChainComplex C ℕ)).functor.obj K) =
    Preadditive.DoldKan.equivalence.functor.map
        (NatTrans.app
          (eqToHom
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          K) ≫
      NatTrans.app
          (eqToHom
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (Γ.obj K) ≫
        NatTrans.app N₁Γ₀.hom K
[PROOFSTEP]
refine' (N₂Γ₂_compatible_with_N₁Γ₀ K).trans _
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
⊢ NatTrans.app N₂Γ₂ToKaroubiIso.hom K ≫ NatTrans.app N₁Γ₀.hom K =
    Preadditive.DoldKan.equivalence.functor.map
        (NatTrans.app
          (eqToHom
            (_ :
              (toKaroubiEquivalence (ChainComplex C ℕ)).functor ⋙ Preadditive.DoldKan.equivalence.inverse =
                Γ ⋙ (toKaroubiEquivalence (SimplicialObject C)).functor))
          K) ≫
      NatTrans.app
          (eqToHom
            (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))
          (Γ.obj K) ≫
        NatTrans.app N₁Γ₀.hom K
[PROOFSTEP]
simp only [N₂Γ₂ToKaroubiIso_hom, eqToHom_map, eqToHom_app, eqToHom_trans_assoc]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.υ
      (eqToIso
        (_ : (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁)) =
    Γ₂N₁
[PROOFSTEP]
ext1
[GOAL]
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ (Compatibility.υ
        (eqToIso
          (_ :
            (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor = N₁))).hom =
    Γ₂N₁.hom
[PROOFSTEP]
rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
[GOAL]
case w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Γ₂N₁.inv ≫
      (Compatibility.υ
          (eqToIso
            (_ :
              (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                N₁))).hom =
    𝟙 (N₁ ⋙ Γ₂)
[PROOFSTEP]
ext X : 2
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app
      (Γ₂N₁.inv ≫
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom)
      X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [NatTrans.comp_app]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app Γ₂N₁.inv X ≫
      NatTrans.app
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom
        X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
erw [compatibility_Γ₂N₁_Γ₂N₂_natTrans X]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ((compatibility_Γ₂N₁_Γ₂N₂.app X).inv ≫ NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X)) ≫
      NatTrans.app
        (Compatibility.υ
            (eqToIso
              (_ :
                (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                  N₁))).hom
        X =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [Compatibility.υ_hom_app, Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      NatTrans.app Γ₂N₂.natTrans ((toKaroubi (SimplicialObject C)).obj X) ≫
        NatTrans.app Γ₂N₂.hom ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X) ≫
          Preadditive.DoldKan.equivalence.inverse.map
            (NatTrans.app
              (eqToIso
                  (_ :
                    (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                      N₁)).hom
              X) =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
erw [← NatTrans.comp_app_assoc, IsIso.hom_inv_id]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      NatTrans.app (𝟙 (N₂ ⋙ Γ₂)) ((toKaroubi (SimplicialObject C)).obj X) ≫
        Preadditive.DoldKan.equivalence.inverse.map
          (NatTrans.app
            (eqToIso
                (_ :
                  (toKaroubiEquivalence (SimplicialObject C)).functor ⋙ Preadditive.DoldKan.equivalence.functor =
                    N₁)).hom
            X) =
    NatTrans.app (𝟙 (N₁ ⋙ Γ₂)) X
[PROOFSTEP]
rw [NatTrans.id_app, id_comp, NatTrans.id_app, eqToIso.hom, eqToHom_app, eqToHom_map]
[GOAL]
case w.w.h
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ NatTrans.app compatibility_Γ₂N₁_Γ₂N₂.inv X ≫
      eqToHom
        (_ :
          Preadditive.DoldKan.equivalence.inverse.obj
              (Preadditive.DoldKan.equivalence.functor.obj
                ((toKaroubiEquivalence (SimplicialObject C)).functor.obj X)) =
            Preadditive.DoldKan.equivalence.inverse.obj (N₁.obj X)) =
    𝟙 ((N₁ ⋙ Γ₂).obj X)
[PROOFSTEP]
rw [compatibility_Γ₂N₁_Γ₂N₂_inv_app, eqToHom_trans, eqToHom_refl]