[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : ¬HasPDF X ℙ
⊢ pdf X ℙ = 0
[PROOFSTEP]
simp only [pdf, dif_neg h]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
⊢ HasPDF X ℙ
[PROOFSTEP]
by_contra hpdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
hpdf : ¬HasPDF X ℙ
⊢ False
[PROOFSTEP]
simp [pdf, hpdf] at h
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
⊢ Measurable X
[PROOFSTEP]
by_contra hX
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
h : pdf X ℙ ≠ 0
hX : ¬Measurable X
⊢ False
[PROOFSTEP]
exact h (pdf_eq_zero_of_not_measurable hX)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
⊢ Measurable (pdf X ℙ)
[PROOFSTEP]
unfold pdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
⊢ Measurable (if hX : HasPDF X ℙ then Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f) else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
h : HasPDF X ℙ
⊢ Measurable (Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f))
case neg
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
h : ¬HasPDF X ℙ
⊢ Measurable 0
[PROOFSTEP]
exacts [(Classical.choose_spec h.1.2).1, measurable_zero]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
⊢ map X ℙ = withDensity μ (pdf X ℙ)
[PROOFSTEP]
simp only [pdf, dif_pos hX]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
⊢ map X ℙ = withDensity μ (Classical.choose (_ : ∃ f, Measurable f ∧ map X ℙ = withDensity μ f))
[PROOFSTEP]
exact (Classical.choose_spec hX.pdf'.2).2
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
hX : HasPDF X ℙ
s : Set E
hs : MeasurableSet s
⊢ ↑↑(map X ℙ) s = ∫⁻ (x : E) in s, pdf X ℙ x ∂μ
[PROOFSTEP]
rw [← withDensity_apply _ hs, map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ x ∂μ = ↑↑ℙ Set.univ
[PROOFSTEP]
rw [← set_lintegral_univ, ← map_eq_set_lintegral_pdf X ℙ μ MeasurableSet.univ,
  Measure.map_apply (HasPDF.measurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
by_cases hpdf : HasPDF X ℙ μ
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf : HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
haveI := hpdf
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
refine' ae_lt_top (measurable_pdf X ℙ μ) _
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ∫⁻ (x : E), pdf X ℙ x ∂μ ≠ ⊤
[PROOFSTEP]
rw [lintegral_eq_measure_univ]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf this : HasPDF X ℙ
⊢ ↑↑ℙ Set.univ ≠ ⊤
[PROOFSTEP]
exact (measure_lt_top _ _).ne
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ✝ : Measure E
inst✝ : IsFiniteMeasure ℙ
μ : Measure E
X : Ω → E
hpdf : ¬HasPDF X ℙ
⊢ ∀ᵐ (x : E) ∂μ, pdf X ℙ x < ⊤
[PROOFSTEP]
simp [pdf, hpdf]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
⊢ (Integrable fun x => f (X x)) ↔ Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
erw [← integrable_map_measure hf.aestronglyMeasurable (HasPDF.measurable X ℙ μ).aemeasurable,
  map_eq_withDensity_pdf X ℙ μ, integrable_withDensity_iff (measurable_pdf _ _ _) ae_lt_top]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
by_cases hpdf : Integrable (fun x => f x * (pdf X ℙ μ x).toReal) μ
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
rw [← integral_map (HasPDF.measurable X ℙ μ).aemeasurable hf.aestronglyMeasurable, map_eq_withDensity_pdf X ℙ μ,
  integral_eq_lintegral_pos_part_sub_lintegral_neg_part hpdf, integral_eq_lintegral_pos_part_sub_lintegral_neg_part,
  lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf X ℙ μ) hf.neg.ennreal_ofReal,
  lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf X ℙ μ) hf.ennreal_ofReal]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ENNReal.toReal (∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ) -
      ENNReal.toReal (∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ) =
    ENNReal.toReal (∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ) -
      ENNReal.toReal (∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ)
[PROOFSTEP]
congr 2
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
have : ∀ x, ENNReal.ofReal (f x * (pdf X ℙ μ x).toReal) = ENNReal.ofReal (pdf X ℙ μ x).toReal * ENNReal.ofReal (f x) :=
  fun x ↦ by rw [mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
x : E
⊢ ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) = ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
[PROOFSTEP]
rw [mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (f a * ENNReal.toReal (pdf X ℙ a)) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
simp_rw [this]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (f x * ENNReal.toReal (pdf X ℙ x)) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (ENNReal.toReal (pdf X ℙ a)) * ENNReal.ofReal (f a) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (f x)) a ∂μ
[PROOFSTEP]
exact lintegral_congr_ae (Filter.EventuallyEq.mul ofReal_toReal_ae_eq (ae_eq_refl _))
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
have :
  ∀ x, ENNReal.ofReal (-(f x * (pdf X ℙ μ x).toReal)) = ENNReal.ofReal (pdf X ℙ μ x).toReal * ENNReal.ofReal (-f x) :=
  by
  intro x
  rw [neg_mul_eq_neg_mul, mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
[PROOFSTEP]
intro x
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
x : E
⊢ ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
    ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
[PROOFSTEP]
rw [neg_mul_eq_neg_mul, mul_comm, ENNReal.ofReal_mul ENNReal.toReal_nonneg]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (-(f a * ENNReal.toReal (pdf X ℙ a))) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
simp_rw [this]
[GOAL]
case pos.e_a.e_a
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this :
  ∀ (x : E),
    ENNReal.ofReal (-(f x * ENNReal.toReal (pdf X ℙ x))) =
      ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x)) * ENNReal.ofReal (-f x)
⊢ ∫⁻ (a : E), ENNReal.ofReal (ENNReal.toReal (pdf X ℙ a)) * ENNReal.ofReal (-f a) ∂μ =
    ∫⁻ (a : E), (pdf X ℙ * fun x => ENNReal.ofReal (-f x)) a ∂μ
[PROOFSTEP]
exact lintegral_congr_ae (Filter.EventuallyEq.mul ofReal_toReal_ae_eq (ae_eq_refl _))
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ Integrable fun y => f y
[PROOFSTEP]
refine' ⟨hf.aestronglyMeasurable, _⟩
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ HasFiniteIntegral fun y => f y
[PROOFSTEP]
rw [HasFiniteIntegral, lintegral_withDensity_eq_lintegral_mul _ (measurable_pdf _ _ _) hf.nnnorm.coe_nnreal_ennreal]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫⁻ (a : E), (pdf X ℙ * fun x => ↑‖f x‖₊) a ∂μ < ⊤
[PROOFSTEP]
have : (fun x => (pdf X ℙ μ * fun x => (‖f x‖₊ : ℝ≥0∞)) x) =ᵐ[μ] fun x => ‖f x * (pdf X ℙ μ x).toReal‖₊ :=
  by
  simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul]
  rw [smul_eq_mul, mul_comm]
  refine' Filter.EventuallyEq.mul (ae_eq_refl _) (ae_eq_trans ofReal_toReal_ae_eq.symm _)
  simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => (pdf X ℙ • fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
rw [smul_eq_mul, mul_comm]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => ((fun x => ↑‖f x‖₊) * pdf X ℙ) x) =ᶠ[ae μ] fun x => ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) (ae_eq_trans ofReal_toReal_ae_eq.symm _)
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae μ] fun x => ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this : (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : E), (pdf X ℙ * fun x => ↑‖f x‖₊) a ∂μ < ⊤
[PROOFSTEP]
rw [lintegral_congr_ae this]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
this : (fun x => (pdf X ℙ * fun x => ↑‖f x‖₊) x) =ᶠ[ae μ] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : E), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ ∂μ < ⊤
[PROOFSTEP]
exact hpdf.2
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : ¬Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ∫ (x : E), f x * ENNReal.toReal (pdf X ℙ x) ∂μ = ∫ (x : Ω), f (X x) ∂ℙ
[PROOFSTEP]
rw [integral_undef hpdf, integral_undef]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ
f : E → ℝ
hf : Measurable f
hpdf : ¬Integrable fun x => f x * ENNReal.toReal (pdf X ℙ x)
⊢ ¬Integrable fun x => f (X x)
[PROOFSTEP]
rwa [← integrable_iff_integrable_mul_pdf hf] at hpdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ map X ℙ ≪ μ
[PROOFSTEP]
rw [map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ
⊢ withDensity μ (pdf X ℙ) ≪ μ
[PROOFSTEP]
exact withDensity_absolutelyContinuous _ _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX' : HasPDF X ℙ
⊢ Measurable (0, pdf X ℙ).snd ∧ (0, pdf X ℙ).fst ⟂ₘ μ ∧ map X ℙ = (0, pdf X ℙ).fst + withDensity μ (0, pdf X ℙ).snd
[PROOFSTEP]
simp only [zero_add, measurable_pdf X ℙ μ, true_and_iff, MutuallySingular.zero_left, map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ HasPDF X ℙ ↔ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
constructor
[GOAL]
case mp
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ HasPDF X ℙ → Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
intro hX'
[GOAL]
case mp
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX' : HasPDF X ℙ
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
exact ⟨hX'.pdf'.1, haveLebesgueDecomposition_of_hasPDF, map_absolutelyContinuous⟩
[GOAL]
case mpr
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ → HasPDF X ℙ
[PROOFSTEP]
rintro ⟨hX, h_decomp, h⟩
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
⊢ HasPDF X ℙ
[PROOFSTEP]
haveI := h_decomp
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
this : HaveLebesgueDecomposition (map X ℙ) μ
⊢ HasPDF X ℙ
[PROOFSTEP]
refine' ⟨⟨hX, (Measure.map X ℙ).rnDeriv μ, measurable_rnDeriv _ _, _⟩⟩
[GOAL]
case mpr.intro.intro
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
h_decomp : HaveLebesgueDecomposition (map X ℙ) μ
h : map X ℙ ≪ μ
this : HaveLebesgueDecomposition (map X ℙ) μ
⊢ map X ℙ = withDensity μ (rnDeriv (map X ℙ) μ)
[PROOFSTEP]
rwa [withDensity_rnDeriv_eq]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
⊢ HasPDF X ℙ ↔ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
rw [hasPDF_iff]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
hX : Measurable X
⊢ Measurable X ∧ HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ ↔
    HaveLebesgueDecomposition (map X ℙ) μ ∧ map X ℙ ≪ μ
[PROOFSTEP]
simp only [hX, true_and]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ HasPDF (g ∘ X) ℙ
[PROOFSTEP]
rw [hasPDF_iff, ← map_map hg.measurable (HasPDF.measurable X ℙ μ)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ Measurable (g ∘ X) ∧ HaveLebesgueDecomposition (map g (map X ℙ)) ν ∧ map g (map X ℙ) ≪ ν
[PROOFSTEP]
refine' ⟨hg.measurable.comp (HasPDF.measurable X ℙ μ), hmap, _⟩
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ map g (map X ℙ) ≪ ν
[PROOFSTEP]
rw [map_eq_withDensity_pdf X ℙ μ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
⊢ map g (withDensity μ (pdf X ℙ)) ≪ ν
[PROOFSTEP]
refine' AbsolutelyContinuous.mk fun s hsm hs => _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
⊢ ↑↑(map g (withDensity μ (pdf X ℙ))) s = 0
[PROOFSTEP]
rw [map_apply hg.measurable hsm, withDensity_apply _ (hg.measurable hsm)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
have := hg.absolutelyContinuous hs
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
this : ↑↑(map g μ) s = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
rw [map_apply hg.measurable hsm] at this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ
g : E → F
hg : QuasiMeasurePreserving g
hmap : HaveLebesgueDecomposition (map g (map X ℙ)) ν
s : Set F
hsm : MeasurableSet s
hs : ↑↑ν s = 0
this : ↑↑μ (g ⁻¹' s) = 0
⊢ ∫⁻ (a : E) in g ⁻¹' s, pdf X ℙ a ∂μ = 0
[PROOFSTEP]
exact set_lintegral_measure_zero _ _ this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HasPDF X ℙ ↔ map X ℙ ≪ volume
[PROOFSTEP]
rw [hasPDF_iff_of_measurable hX]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HaveLebesgueDecomposition (map X ℙ) volume ∧ map X ℙ ≪ volume ↔ map X ℙ ≪ volume
[PROOFSTEP]
exact and_iff_right inferInstance
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
by_cases hX : Measurable X
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
rw [Real.hasPDF_iff_of_measurable hX, iff_and_self]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : Measurable X
⊢ map X ℙ ≪ volume → Measurable X
[PROOFSTEP]
exact fun _ => hX
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
hX : ¬Measurable X
⊢ HasPDF X ℙ ↔ Measurable X ∧ map X ℙ ≪ volume
[PROOFSTEP]
exact ⟨fun h => False.elim (hX h.pdf'.1), fun h => False.elim (hX h.1)⟩
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ HasFiniteIntegral fun x => f x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
rw [HasFiniteIntegral]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ ∫⁻ (a : ℝ), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ < ⊤
[PROOFSTEP]
have : (fun x => ↑‖f x‖₊ * g x) =ᵐ[volume] fun x => ‖f x * (pdf X ℙ volume x).toReal‖₊ :=
  by
  refine'
    ae_eq_trans
      (Filter.EventuallyEq.mul (ae_eq_refl fun x => (‖f x‖₊ : ℝ≥0∞)) (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) _
  simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul, smul_eq_mul]
  refine' Filter.EventuallyEq.mul (ae_eq_refl _) _
  simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * g x) =ᶠ[ae volume] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine'
  ae_eq_trans
    (Filter.EventuallyEq.mul (ae_eq_refl fun x => (‖f x‖₊ : ℝ≥0∞)) (ae_eq_trans hg.symm ofReal_toReal_ae_eq.symm)) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x =>
    ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp_rw [← smul_eq_mul, nnnorm_smul, ENNReal.coe_mul, smul_eq_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ↑‖f x‖₊ * ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x =>
    ↑‖f x‖₊ * ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
⊢ (fun x => ENNReal.ofReal (ENNReal.toReal (pdf X ℙ x))) =ᶠ[ae volume] fun x => ↑‖ENNReal.toReal (pdf X ℙ x)‖₊
[PROOFSTEP]
simp only [Real.ennnorm_eq_ofReal ENNReal.toReal_nonneg, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
inst✝ : IsFiniteMeasure ℙ
X : Ω → ℝ
f : ℝ → ℝ
g : ℝ → ℝ≥0∞
hg : pdf X ℙ =ᶠ[ae volume] g
hgi : ∫⁻ (x : ℝ), ↑‖f x‖₊ * g x ≠ ⊤
this : (fun x => ↑‖f x‖₊ * g x) =ᶠ[ae volume] fun x => ↑‖f x * ENNReal.toReal (pdf X ℙ x)‖₊
⊢ ∫⁻ (a : ℝ), ↑‖f a * ENNReal.toReal (pdf X ℙ a)‖₊ < ⊤
[PROOFSTEP]
rwa [lt_top_iff_ne_top, ← lintegral_congr_ae this]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hu : IsUniform X s ℙ
⊢ pdf X ℙ ≠ 0
[PROOFSTEP]
intro hpdf
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hu : IsUniform X s ℙ
hpdf : pdf X ℙ = 0
⊢ False
[PROOFSTEP]
simp only [IsUniform, hpdf] at hu
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
⊢ False
[PROOFSTEP]
suffices μ (s ∩ Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞))) = 0
  by
  have heq : Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) = Set.univ :=
    by
    ext x
    rw [Function.mem_support]
    simp [hnt]
  rw [heq, Set.inter_univ] at this
  exact hns this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
⊢ False
[PROOFSTEP]
have heq : Function.support ((μ s)⁻¹ • (1 : E → ℝ≥0∞)) = Set.univ :=
  by
  ext x
  rw [Function.mem_support]
  simp [hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
⊢ Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
[PROOFSTEP]
ext x
[GOAL]
case h
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
x : E
⊢ x ∈ Function.support ((↑↑μ s)⁻¹ • 1) ↔ x ∈ Set.univ
[PROOFSTEP]
rw [Function.mem_support]
[GOAL]
case h
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
x : E
⊢ ((↑↑μ s)⁻¹ • 1) x ≠ 0 ↔ x ∈ Set.univ
[PROOFSTEP]
simp [hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
heq : Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
⊢ False
[PROOFSTEP]
rw [heq, Set.inter_univ] at this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
this : ↑↑μ s = 0
heq : Function.support ((↑↑μ s)⁻¹ • 1) = Set.univ
⊢ False
[PROOFSTEP]
exact hns this
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hpdf : pdf X ℙ = 0
hu : 0 =ᶠ[ae μ] Set.indicator s ((↑↑μ s)⁻¹ • 1)
⊢ ↑↑μ (s ∩ Function.support ((↑↑μ s)⁻¹ • 1)) = 0
[PROOFSTEP]
exact Set.indicator_ae_eq_zero.1 hu.symm
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
⊢ ↑↑ℙ (X ⁻¹' A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
haveI := hu.hasPDF hns hnt
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ ↑↑ℙ (X ⁻¹' A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
rw [← Measure.map_apply (HasPDF.measurable X ℙ μ) hA, map_eq_set_lintegral_pdf X ℙ μ hA, lintegral_congr_ae hu.restrict]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ ∫⁻ (a : E) in A, Set.indicator s ((↑↑μ s)⁻¹ • 1) a ∂μ = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
simp only [hms, hA, lintegral_indicator, Pi.smul_apply, Pi.one_apply, Algebra.id.smul_eq_mul, mul_one, lintegral_const,
  restrict_apply', Set.univ_inter]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
A : Set E
hA : MeasurableSet A
this : HasPDF X ℙ
⊢ (↑↑μ s)⁻¹ * ↑↑μ (s ∩ A) = ↑↑μ (s ∩ A) / ↑↑μ s
[PROOFSTEP]
rw [ENNReal.div_eq_inv_mul]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
⊢ ↑↑ℙ Set.univ = 1
[PROOFSTEP]
have : X ⁻¹' Set.univ = Set.univ := by simp only [Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
⊢ X ⁻¹' Set.univ = Set.univ
[PROOFSTEP]
simp only [Set.preimage_univ]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m✝ : MeasurableSpace Ω
ℙ✝ : Measure Ω
μ✝ : Measure E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : Measure E
s : Set E
hns : ↑↑μ s ≠ 0
hnt : ↑↑μ s ≠ ⊤
hms : MeasurableSet s
hu : IsUniform X s ℙ
this : X ⁻¹' Set.univ = Set.univ
⊢ ↑↑ℙ Set.univ = 1
[PROOFSTEP]
rw [← this, hu.measure_preimage hns hnt hms MeasurableSet.univ, Set.inter_univ, ENNReal.div_self hns hnt]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
by_cases hsupp : volume s = ∞
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
have : pdf X ℙ =ᵐ[volume] 0 := by
  refine' ae_eq_trans huX _
  simp [hsupp, ae_eq_refl]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ pdf X ℙ =ᶠ[ae volume] 0
[PROOFSTEP]
refine' ae_eq_trans huX _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
⊢ Set.indicator s ((↑↑volume s)⁻¹ • 1) =ᶠ[ae volume] 0
[PROOFSTEP]
simp [hsupp, ae_eq_refl]
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' Integrable.congr (integrable_zero _ _ _) _
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => 0) =ᶠ[ae volume] fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
rw [(by simp : (fun x => 0 : ℝ → ℝ) = fun x => x * (0 : ℝ≥0∞).toReal)]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => 0) = fun x => x * ENNReal.toReal 0
[PROOFSTEP]
simp
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ↑↑volume s = ⊤
this : pdf X ℙ =ᶠ[ae volume] 0
⊢ (fun x => x * ENNReal.toReal 0) =ᶠ[ae volume] fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' Filter.EventuallyEq.mul (ae_eq_refl _) (Filter.EventuallyEq.fun_comp this.symm ENNReal.toReal)
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ Integrable fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
constructor
  -- porting note: `refine` was failing, don't know why
[GOAL]
case neg.left
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ AEStronglyMeasurable (fun x => x * ENNReal.toReal (pdf X ℙ x)) volume
[PROOFSTEP]
exact aestronglyMeasurable_id.mul (measurable_pdf X ℙ).aemeasurable.ennreal_toReal.aestronglyMeasurable
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ HasFiniteIntegral fun x => x * ENNReal.toReal (pdf X ℙ x)
[PROOFSTEP]
refine' hasFiniteIntegral_mul huX _
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ((↑↑volume s)⁻¹ • 1) x ≠ ⊤
[PROOFSTEP]
set ind := (volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x ≠ ⊤
[PROOFSTEP]
have : ∀ x, ↑‖x‖₊ * s.indicator ind x = s.indicator (fun x => ‖x‖₊ * ind x) x := fun x =>
  (s.indicator_mul_right (fun x => ↑‖x‖₊) ind).symm
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ ∫⁻ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x ≠ ⊤
[PROOFSTEP]
simp only [this, lintegral_indicator _ hms, mul_one, Algebra.id.smul_eq_mul, Pi.one_apply, Pi.smul_apply]
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ ∫⁻ (x : ℝ) in s, ↑‖x‖₊ * (↑↑volume s)⁻¹ ≠ ⊤
[PROOFSTEP]
rw [lintegral_mul_const _ measurable_nnnorm.coe_nnreal_ennreal]
[GOAL]
case neg.right
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
inst✝ : IsFiniteMeasure ℙ
hcs : IsCompact s
huX : IsUniform X s ℙ
hsupp : ¬↑↑volume s = ⊤
ind : ℝ → ℝ≥0∞ := (↑↑volume s)⁻¹ • 1
this : ∀ (x : ℝ), ↑‖x‖₊ * Set.indicator s ind x = Set.indicator s (fun x => ↑‖x‖₊ * ind x) x
⊢ (∫⁻ (a : ℝ) in s, ↑‖a‖₊) * (↑↑volume s)⁻¹ ≠ ⊤
[PROOFSTEP]
refine'
  (ENNReal.mul_lt_top (set_lintegral_lt_top_of_isCompact hsupp hcs continuous_nnnorm).ne
      (ENNReal.inv_lt_top.2 (pos_iff_ne_zero.mpr hns)).ne).ne
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
haveI := hasPDF hns hnt huX
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this : HasPDF X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
haveI := huX.isProbabilityMeasure hns hnt hms
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [← integral_mul_eq_integral]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (x : ℝ), x * ENNReal.toReal (pdf (fun x => X x) ℙ x) = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [integral_congr_ae (Filter.EventuallyEq.mul (ae_eq_refl _) (pdf_toReal_ae_eq huX))]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∫ (a : ℝ), a * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) a) =
    ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
have :
  ∀ x,
    x * (s.indicator ((volume s)⁻¹ • (1 : ℝ → ℝ≥0∞)) x).toReal =
      x * s.indicator ((volume s)⁻¹.toReal • (1 : ℝ → ℝ)) x :=
  by
  refine' fun x => congr_arg ((· * ·) x) _
  by_cases hx : x ∈ s
  · simp [Set.indicator_of_mem hx]
  · simp [Set.indicator_of_not_mem hx]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
⊢ ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
refine' fun x => congr_arg ((· * ·) x) _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
by_cases hx : x ∈ s
[GOAL]
case pos
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
hx : x ∈ s
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
simp [Set.indicator_of_mem hx]
[GOAL]
case neg
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝ : HasPDF X ℙ
this : IsProbabilityMeasure ℙ
x : ℝ
hx : ¬x ∈ s
⊢ ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) = Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
[PROOFSTEP]
simp [Set.indicator_of_not_mem hx]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (a : ℝ), a * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) a) =
    ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
simp_rw [this, ← s.indicator_mul_right fun x => x, integral_indicator hms]
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (a : ℝ) in s, a * (ENNReal.toReal (↑↑volume s)⁻¹ • 1) a = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
change ∫ x in s, x * (volume s)⁻¹.toReal • (1 : ℝ) = _
[GOAL]
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → ℝ
s : Set ℝ
hms : MeasurableSet s
hns : ↑↑volume s ≠ 0
hnt : ↑↑volume s ≠ ⊤
huX : IsUniform X s ℙ
this✝¹ : HasPDF X ℙ
this✝ : IsProbabilityMeasure ℙ
this :
  ∀ (x : ℝ),
    x * ENNReal.toReal (Set.indicator s ((↑↑volume s)⁻¹ • 1) x) =
      x * Set.indicator s (ENNReal.toReal (↑↑volume s)⁻¹ • 1) x
⊢ ∫ (x : ℝ) in s, x * ENNReal.toReal (↑↑volume s)⁻¹ • 1 = ENNReal.toReal (↑↑volume s)⁻¹ * ∫ (x : ℝ) in s, x
[PROOFSTEP]
rw [integral_mul_right, mul_comm, smul_eq_mul, mul_one]


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.61, max u v} (SimplicialObject C)
[PROOFSTEP]
dsimp only [SimplicialObject]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.61, max u v} (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplicialObject C)
[PROOFSTEP]
dsimp [SimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplicialObject C)
[PROOFSTEP]
dsimp [SimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), NatTrans.app f n = NatTrans.app g n
⊢ f.app = g.app
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), NatTrans.app f n = NatTrans.app g n
x✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app f x✝ = NatTrans.app g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n m : ℕ
h : n = m
⊢ op [n] = op [m]
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ eqToIso X h = Iso.refl (X.obj (op [n]))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj (op [n]))).hom
[PROOFSTEP]
simp [eqToIso]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ X (Fin.succ j) ≫ δ X i = δ X (Fin.castSucc i) ≫ δ X j
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
hj : j = 0
⊢ False
[PROOFSTEP]
simp [hj, Fin.not_lt_zero] at H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ X j ≫ δ X i = δ X (Fin.castSucc i) ≫ δ X (Fin.pred j (_ : j = 0 → False))
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.succ j) ≫ δ X (Fin.castLT i (_ : ↑i < n + 2)) = δ X i ≫ δ X j
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.δ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.succ i)).op ≫ X.map (SimplexCategory.δ i).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = Fin.castSucc i
⊢ δ X j ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
[PROOFSTEP]
rw [δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ σ X (Fin.succ j) ≫ δ X (Fin.castSucc i) = δ X i ≫ σ X j
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.σ (Fin.succ j)).op ≫ X.map (SimplexCategory.δ (Fin.castSucc i)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.castSucc i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.castSucc i)).op = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.castSucc i
⊢ σ X i ≫ δ X j = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.castSucc i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
rw [δ_comp_σ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.succ i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_succ, op_id, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ σ X i ≫ δ X j = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ σ X i ≫ δ X (Fin.succ i) = 𝟙 (X.obj (op [n]))
[PROOFSTEP]
rw [δ_comp_σ_succ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ σ X (Fin.castSucc j) ≫ δ X (Fin.succ i) = δ X i ≫ σ X j
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ X.map (SimplexCategory.σ (Fin.castSucc j)).op ≫ X.map (SimplexCategory.δ (Fin.succ i)).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
hi : i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.not_lt_zero, hi] at H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ σ X j ≫ δ X i = δ X (Fin.pred i (_ : i = 0 → False)) ≫ σ X (Fin.castLT j (_ : ↑j < n + 1))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False))).op ≫
      X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ X j ≫ σ X (Fin.castSucc i) = σ X i ≫ σ X (Fin.succ j)
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.σ (Fin.castSucc i)).op =
    X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.σ (Fin.succ j)).op
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
⊢ Category.{?u.68325, max u v} (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
⊢ Category.{?u.68325, max u v} ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J ((SimplexCategory.Truncated n)ᵒᵖ ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
⊢ Category.{?u.76503, max u v} (Augmented C)
[PROOFSTEP]
dsimp only [Augmented]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
⊢ Category.{?u.76503, max u v} (Comma (𝟭 (SimplicialObject C)) (const C))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map (NatTrans.app (drop.map η) (op [0])) ≫
      ((fun X => { left := (drop.obj X).obj (op [0]), right := point.obj X, hom := NatTrans.app X.hom (op [0]) })
          Y✝).hom =
    ((fun X => { left := (drop.obj X).obj (op [0]), right := point.obj X, hom := NatTrans.app X.hom (op [0]) })
          X✝).hom ≫
      (𝟭 C).map (point.map η)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app η.left (op [0]) ≫ NatTrans.app Y✝.hom (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
rw [← NatTrans.comp_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app (η.left ≫ Y✝.hom) (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
erw [η.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ NatTrans.app (X✝.hom ≫ (const C).map η.right) (op [0]) = NatTrans.app X✝.hom (op [0]) ≫ η.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ : SimplicialObject C
X Y : Augmented C
f : X ⟶ Y
⊢ NatTrans.app (drop.map f) (op [0]) ≫ NatTrans.app Y.hom (op [0]) = NatTrans.app X.hom (op [0]) ≫ point.map f
[PROOFSTEP]
convert congr_app f.w (op (SimplexCategory.mk 0))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
      ((fun X =>
            { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
              hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
          Y✝).hom =
    ((fun X =>
            { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
              hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
          X✝).hom ≫
      (const D).map (F.map η.right)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      ((𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
        ((fun X =>
              { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
                hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
            Y✝).hom)
      n✝ =
    NatTrans.app
      (((fun X =>
              { left := ((whiskering C D).obj F).obj (drop.obj X), right := F.obj (point.obj X),
                hom := whiskerRight X.hom F ≫ (Functor.constComp SimplexCategoryᵒᵖ X.right F).hom })
            X✝).hom ≫
        (const D).map (F.map η.right))
      n✝
[PROOFSTEP]
dsimp [whiskerRight]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app η.left n✝) ≫ F.map (NatTrans.app Y✝.hom n✝) ≫ 𝟙 (F.obj Y✝.right) =
    (F.map (NatTrans.app X✝.hom n✝) ≫ 𝟙 (F.obj X✝.right)) ≫ F.map η.right
[PROOFSTEP]
simp only [Category.comp_id, ← F.map_comp, ← NatTrans.comp_app]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app (η.left ≫ Y✝.hom) n✝) = F.map (NatTrans.app X✝.hom n✝ ≫ η.right)
[PROOFSTEP]
erw [η.w]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{?u.105136, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ F.map (NatTrans.app (X✝.hom ≫ (const C).map η.right) n✝) = F.map (NatTrans.app X✝.hom n✝ ≫ η.right)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (𝟭 (SimplicialObject D)).map (whiskerLeft (drop.obj A) η) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (const D).map (NatTrans.app η (point.obj A))
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategoryᵒᵖ
⊢ NatTrans.app ((𝟭 (SimplicialObject D)).map (whiskerLeft (drop.obj A) η) ≫ ((whiskeringObj C D Y✝).obj A).hom) n =
    NatTrans.app (((whiskeringObj C D X✝).obj A).hom ≫ (const D).map (NatTrans.app η (point.obj A))) n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategoryᵒᵖ
⊢ NatTrans.app η (A.left.obj n) ≫ Y✝.map (NatTrans.app A.hom n) ≫ 𝟙 (Y✝.obj A.right) =
    (X✝.map (NatTrans.app A.hom n) ≫ 𝟙 (X✝.obj A.right)) ≫ NatTrans.app η A.right
[PROOFSTEP]
rw [Category.comp_id, Category.comp_id, η.naturality]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := whiskeringObj C D,
          map := fun {X Y} η =>
            NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
      (x✝¹ ≫ x✝) =
    { obj := whiskeringObj C D,
            map := fun {X Y} η =>
              NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
        x✝¹ ≫
      { obj := whiskeringObj C D,
            map := fun {X Y} η =>
              NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case w.h.h₁.h
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
n✝ : SimplexCategoryᵒᵖ
⊢ NatTrans.app
      (NatTrans.app
          ({ obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            (x✝² ≫ x✝¹))
          x✝).left
      n✝ =
    NatTrans.app
      (NatTrans.app
          ({ obj := whiskeringObj C D,
                  map := fun {X Y} η =>
                    NatTrans.mk fun A =>
                      CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
              x✝² ≫
            { obj := whiskeringObj C D,
                  map := fun {X Y} η =>
                    NatTrans.mk fun A =>
                      CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
              x✝¹)
          x✝).left
      n✝
[PROOFSTEP]
rfl
[GOAL]
case w.h.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Augmented C
⊢ (NatTrans.app
        ({ obj := whiskeringObj C D,
              map := fun {X Y} η =>
                NatTrans.mk fun A => CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
          (x✝² ≫ x✝¹))
        x✝).right =
    (NatTrans.app
        ({ obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            x✝² ≫
          { obj := whiskeringObj C D,
                map := fun {X Y} η =>
                  NatTrans.mk fun A =>
                    CommaMorphism.mk (whiskerLeft (drop.obj A) η) (NatTrans.app η (point.obj A)) }.map
            x✝¹)
        x✝).right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f_1 : X_1 ⟶ Y),
    ((𝟭 (SimplicialObject C)).obj X).map f_1 ≫ (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) Y =
      (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) X_1 ≫ ((const C).obj X₀).map f_1
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ ((𝟭 (SimplicialObject C)).obj X).map g ≫ (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) j =
    (fun i => X.map (SimplexCategory.const i.unop 0).op ≫ f) i ≫ ((const C).obj X₀).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g ≫ X.map (SimplexCategory.const j.unop 0).op ≫ f = (X.map (SimplexCategory.const i.unop 0).op ≫ f) ≫ 𝟙 X₀
[PROOFSTEP]
rw [← g.op_unop]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
i j : SimplexCategoryᵒᵖ
g : i ⟶ j
⊢ X.map g.unop.op ≫ X.map (SimplexCategory.const j.unop 0).op ≫ f =
    (X.map (SimplexCategory.const i.unop 0).op ≫ f) ≫ 𝟙 X₀
[PROOFSTEP]
simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ NatTrans.app (augment X X₀ f w).hom (op [0]) = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X.obj (op [0]) ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ X.map (SimplexCategory.const [0] 0).op ≫ f = f
[PROOFSTEP]
rw [SimplexCategory.hom_zero_zero ([0].const 0), op_id, X.map_id, Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.208707, max u v} (CosimplicialObject C)
[PROOFSTEP]
dsimp only [CosimplicialObject]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.208707, max u v} (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (CosimplicialObject C)
[PROOFSTEP]
dsimp [CosimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (CosimplicialObject C)
[PROOFSTEP]
dsimp [CosimplicialObject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), NatTrans.app f n = NatTrans.app g n
⊢ f.app = g.app
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), NatTrans.app f n = NatTrans.app g n
x✝ : SimplexCategory
⊢ NatTrans.app f x✝ = NatTrans.app g x✝
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n m : ℕ
h : n = m
⊢ [n] = [m]
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ eqToIso X h = Iso.refl (X.obj [n])
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
h : n = n
⊢ (eqToIso X h).hom = (Iso.refl (X.obj [n])).hom
[PROOFSTEP]
simp [eqToIso]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ δ X i ≫ δ X (Fin.succ j) = δ X j ≫ δ X (Fin.castSucc i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ (Fin.castSucc i))
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
hj : j = 0
⊢ False
[PROOFSTEP]
simp only [hj, Fin.not_lt_zero] at H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ δ X i ≫ δ X j = δ X (Fin.pred j (_ : j = 0 → False)) ≫ δ X (Fin.castSucc i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))) ≫ X.map (SimplexCategory.δ (Fin.castSucc i))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.castLT i (_ : ↑i < n + 2)) ≫ δ X (Fin.succ j) = δ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X i ≫ δ X (Fin.castSucc i) = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
dsimp [δ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.castSucc i)) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ i))
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = Fin.castSucc i
⊢ δ X i ≫ δ X j = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X i ≫ δ X (Fin.castSucc i) = δ X i ≫ δ X (Fin.succ i)
[PROOFSTEP]
rw [δ_comp_δ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ δ X (Fin.castSucc i) ≫ σ X (Fin.succ j) = σ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ (Fin.succ j)) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_le H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.castSucc i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_self, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.castSucc i
⊢ δ X j ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.castSucc i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
rw [δ_comp_σ_self]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.map (SimplexCategory.δ (Fin.succ i)) ≫ X.map (SimplexCategory.σ i) = 𝟙 (X.obj [n])
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_succ, X.map_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ δ X j ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
subst H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
[PROOFSTEP]
rw [δ_comp_σ_succ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ δ X (Fin.succ i) ≫ σ X (Fin.castSucc j) = σ X j ≫ δ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : Fin.castSucc j < i
⊢ X.map (SimplexCategory.δ (Fin.succ i)) ≫ X.map (SimplexCategory.σ (Fin.castSucc j)) =
    X.map (SimplexCategory.σ j) ≫ X.map (SimplexCategory.δ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_gt H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
hi : i = 0
⊢ False
[PROOFSTEP]
simp only [Fin.not_lt_zero, hi] at H
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ δ X i ≫ σ X j = σ X (Fin.castLT j (_ : ↑j < n + 1)) ≫ δ X (Fin.pred i (_ : i = 0 → False))
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) ≫
      X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False)))
[PROOFSTEP]
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ X (Fin.castSucc i) ≫ σ X j = σ X (Fin.succ j) ≫ σ X i
[PROOFSTEP]
dsimp [δ, σ]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ (Fin.castSucc i)) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.succ j)) ≫ X.map (SimplexCategory.σ i)
[PROOFSTEP]
simp only [← X.map_comp, SimplexCategory.σ_comp_σ H]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
⊢ Category.{?u.295628, max u v} (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
⊢ Category.{?u.295628, max u v} (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (Truncated C n)
[PROOFSTEP]
dsimp [Truncated]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory.Truncated n ⥤ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
⊢ Category.{?u.303800, max u v} (Augmented C)
[PROOFSTEP]
dsimp only [Augmented]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
⊢ Category.{?u.303800, max u v} (Comma (const C) (𝟭 (CosimplicialObject C)))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (𝟭 C).map (point.map η) ≫
      ((fun X => { left := point.obj X, right := (drop.obj X).obj [0], hom := NatTrans.app X.hom [0] }) Y✝).hom =
    ((fun X => { left := point.obj X, right := (drop.obj X).obj [0], hom := NatTrans.app X.hom [0] }) X✝).hom ≫
      (𝟭 C).map (NatTrans.app (drop.map η) [0])
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app X✝.hom [0] ≫ NatTrans.app η.right [0]
[PROOFSTEP]
rw [← NatTrans.comp_app]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app (X✝.hom ≫ η.right) [0]
[PROOFSTEP]
erw [← η.w]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ η.left ≫ NatTrans.app Y✝.hom [0] = NatTrans.app ((const C).map η.left ≫ Y✝.hom) [0]
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
⊢ (const D).map (F.map η.left) ≫
      ((fun X =>
            { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
              hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
          Y✝).hom =
    ((fun X =>
            { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
              hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
          X✝).hom ≫
      (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ NatTrans.app
      ((const D).map (F.map η.left) ≫
        ((fun X =>
              { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
                hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
            Y✝).hom)
      n✝ =
    NatTrans.app
      (((fun X =>
              { left := F.obj (point.obj X), right := ((whiskering C D).obj F).obj (drop.obj X),
                hom := (Functor.constComp SimplexCategory (point.obj X) F).inv ≫ whiskerRight X.hom F })
            X✝).hom ≫
        (𝟭 (CosimplicialObject D)).map (whiskerRight η.right F))
      n✝
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map η.left ≫ 𝟙 (F.obj Y✝.left) ≫ F.map (NatTrans.app Y✝.hom n✝) =
    (𝟙 (F.obj X✝.left) ≫ F.map (NatTrans.app X✝.hom n✝)) ≫ F.map (NatTrans.app η.right n✝)
[PROOFSTEP]
rw [Category.id_comp, Category.id_comp, ← F.map_comp, ← F.map_comp, ← NatTrans.comp_app]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ NatTrans.app Y✝.hom n✝) = F.map (NatTrans.app (X✝.hom ≫ η.right) n✝)
[PROOFSTEP]
erw [← η.w]
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u_1
inst✝ : Category.{?u.334362, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategory
⊢ F.map (η.left ≫ NatTrans.app Y✝.hom n✝) = F.map (NatTrans.app ((const C).map η.left ≫ Y✝.hom) n✝)
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (const D).map (NatTrans.app η (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)
[PROOFSTEP]
ext n
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategory
⊢ NatTrans.app ((const D).map (NatTrans.app η (point.obj A)) ≫ ((whiskeringObj C D Y✝).obj A).hom) n =
    NatTrans.app (((whiskeringObj C D X✝).obj A).hom ≫ (𝟭 (CosimplicialObject D)).map (whiskerLeft (drop.obj A) η)) n
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
n : SimplexCategory
⊢ NatTrans.app η A.left ≫ 𝟙 (Y✝.obj A.left) ≫ Y✝.map (NatTrans.app A.hom n) =
    (𝟙 (X✝.obj A.left) ≫ X✝.map (NatTrans.app A.hom n)) ≫ NatTrans.app η (A.right.obj n)
[PROOFSTEP]
rw [Category.id_comp, Category.id_comp, η.naturality]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ (whiskeringObj C D X✝).map f ≫
      (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝ =
    (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
      (whiskeringObj C D Y✝).map f
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ ((whiskeringObj C D X✝).map f ≫
        (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝).left =
    ((fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
        (whiskeringObj C D Y✝).map f).left
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ NatTrans.app
      ((whiskeringObj C D X✝).map f ≫
          (fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝).right
      n✝ =
    NatTrans.app
      ((fun A => CommaMorphism.mk (NatTrans.app η (point.obj A)) (whiskerLeft (drop.obj A) η)) x✝¹ ≫
          (whiskeringObj C D Y✝).map f).right
      n✝
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
⊢ X✝.map f.left ≫ NatTrans.app η x✝.left = NatTrans.app η x✝¹.left ≫ Y✝.map f.left
[PROOFSTEP]
simp
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
X : CosimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
x✝¹ x✝ : Augmented C
f : x✝¹ ⟶ x✝
n✝ : SimplexCategory
⊢ X✝.map (NatTrans.app f.right n✝) ≫ NatTrans.app η (x✝.right.obj n✝) =
    NatTrans.app η (x✝¹.right.obj n✝) ≫ Y✝.map (NatTrans.app f.right n✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f_1 : X_1 ⟶ Y),
    ((const C).obj X₀).map f_1 ≫ (fun i => f ≫ X.map (SimplexCategory.const i 0)) Y =
      (fun i => f ≫ X.map (SimplexCategory.const i 0)) X_1 ≫ ((𝟭 (CosimplicialObject C)).obj X).map f_1
[PROOFSTEP]
intro i j g
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
i j : SimplexCategory
g : i ⟶ j
⊢ ((const C).obj X₀).map g ≫ (fun i => f ≫ X.map (SimplexCategory.const i 0)) j =
    (fun i => f ≫ X.map (SimplexCategory.const i 0)) i ≫ ((𝟭 (CosimplicialObject C)).obj X).map g
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
i j : SimplexCategory
g : i ⟶ j
⊢ 𝟙 X₀ ≫ f ≫ X.map (SimplexCategory.const j 0) = (f ≫ X.map (SimplexCategory.const i 0)) ≫ X.map g
[PROOFSTEP]
simpa [← X.map_comp] using w _ _ _
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ NatTrans.app (augment X X₀ f w).hom [0] = f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ X : CosimplicialObject C
X₀ : C
f : X₀ ⟶ X.obj [0]
w : ∀ (i : SimplexCategory) (g₁ g₂ : [0] ⟶ i), f ≫ X.map g₁ = f ≫ X.map g₂
⊢ f ≫ X.map (SimplexCategory.const [0] 0) = f
[PROOFSTEP]
rw [SimplexCategory.hom_zero_zero ([0].const 0), X.map_id, Category.comp_id]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Augmented C
⊢ (CosimplicialObject.Augmented.leftOp (rightOp X)).right = X.right
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X : Augmented Cᵒᵖ
⊢ (SimplicialObject.Augmented.rightOp (leftOp X)).left = X.left
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ ((fun X => SimplicialObject.Augmented.rightOp X.unop) Y✝).hom =
    ((fun X => SimplicialObject.Augmented.rightOp X.unop) X✝).hom ≫
      (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ NatTrans.app
      ((CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫
        ((fun X => SimplicialObject.Augmented.rightOp X.unop) Y✝).hom)
      x =
    NatTrans.app
      (((fun X => SimplicialObject.Augmented.rightOp X.unop) X✝).hom ≫
        (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left))
      x
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ f.unop.right.op ≫ (NatTrans.app Y✝.unop.hom (op x)).op =
    (NatTrans.app X✝.unop.hom (op x)).op ≫ (NatTrans.app f.unop.left (op x)).op
[PROOFSTEP]
simp_rw [← op_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ (NatTrans.app Y✝.unop.hom (op x) ≫ f.unop.right).op =
    (NatTrans.app f.unop.left (op x) ≫ NatTrans.app X✝.unop.hom (op x)).op
[PROOFSTEP]
congr 1
[GOAL]
case h.e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ NatTrans.app Y✝.unop.hom (op x) ≫ f.unop.right = NatTrans.app f.unop.left (op x) ≫ NatTrans.app X✝.unop.hom (op x)
[PROOFSTEP]
exact (congr_app f.unop.w (op x)).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ (CosimplicialObject.Augmented.leftOp X✝).hom =
    (CosimplicialObject.Augmented.leftOp Y✝).hom ≫ (SimplicialObject.const C).map f.left.unop
[PROOFSTEP]
ext x
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app ((𝟭 (SimplicialObject C)).map (NatTrans.leftOp f.right) ≫ (CosimplicialObject.Augmented.leftOp X✝).hom)
      x =
    NatTrans.app ((CosimplicialObject.Augmented.leftOp Y✝).hom ≫ (SimplicialObject.const C).map f.left.unop) x
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app f.right x.unop).unop ≫ (NatTrans.app X✝.hom x.unop).unop =
    (NatTrans.app Y✝.hom x.unop).unop ≫ f.left.unop
[PROOFSTEP]
simp_rw [← unop_comp]
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app X✝.hom x.unop ≫ NatTrans.app f.right x.unop).unop = (f.left ≫ NatTrans.app Y✝.hom x.unop).unop
[PROOFSTEP]
congr 1
[GOAL]
case h.e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app X✝.hom x.unop ≫ NatTrans.app f.right x.unop = f.left ≫ NatTrans.app Y✝.hom x.unop
[PROOFSTEP]
exact (congr_app f.w (unop x)).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (𝟭 (SimplicialObject.Augmented C)ᵒᵖ).map f ≫
      ((fun X => Iso.op (SimplicialObject.Augmented.rightOpLeftOpIso X.unop)) Y✝).hom =
    ((fun X => Iso.op (SimplicialObject.Augmented.rightOpLeftOpIso X.unop)) X✝).hom ≫
      (simplicialToCosimplicialAugmented C ⋙ cosimplicialToSimplicialAugmented C).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f ≫ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom.op =
    (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom.op ≫
      (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.left)) f.unop.right).op
[PROOFSTEP]
rw [← f.op_unop]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.op ≫ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom.op =
    (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom.op ≫
      (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right).op
[PROOFSTEP]
simp_rw [← op_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom ≫ f.unop).op =
    (CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right ≫
        (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom).op
[PROOFSTEP]
congr 1
[GOAL]
case e_f
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (SimplicialObject.Augmented.rightOpLeftOpIso Y✝.unop).hom ≫ f.unop =
    CommaMorphism.mk (NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left)) f.unop.op.unop.right ≫
      (SimplicialObject.Augmented.rightOpLeftOpIso X✝.unop).hom
[PROOFSTEP]
aesop_cat