Analysis I, Section 11.10: Consequences of the fundamental theorems

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

namespace Chapter11open BoundedInterval Chapter9 Chapter10

Proposition 11.10.1 (Integration by parts formula) / Exercise 11.10.1

theorem declaration uses 'sorry'integ_of_mul_deriv {a b:ℝ} (hab: a ≤ b) {F G: ℝ → ℝ} (hF: DifferentiableOn ℝ F (Icc a b)) (hG : DifferentiableOn ℝ G (Icc a b)) (hF': IntegrableOn (derivWithin F (Icc a b)) (Icc a b)) (hG': IntegrableOn (derivWithin G (Icc a b)) (Icc a b)) : integ (F * derivWithin G (Icc a b)) (Icc a b) = F b * G b - F a * G a - integ (G * derivWithin F (Icc a b)) (Icc a b) := a:ℝb:ℝhab:a ≤ bF:ℝ → ℝG:ℝ → ℝhF:DifferentiableOn ℝ F ↑(Icc a b)hG:DifferentiableOn ℝ G ↑(Icc a b)hF':IntegrableOn (derivWithin F ↑(Icc a b)) (Icc a b)hG':IntegrableOn (derivWithin G ↑(Icc a b)) (Icc a b)⊢ integ (F * derivWithin G ↑(Icc a b)) (Icc a b) = F b * G b - F a * G a - integ (G * derivWithin F ↑(Icc a b)) (Icc a b) All goals completed! 🐙

Theorem 11.10.2. Need to add continuity of α due to our conventions on α-length

theorem PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv {a b:ℝ} {α f:ℝ → ℝ} (hα_diff: DifferentiableOn ℝ α (Icc a b)) (hαcont: Continuous α) (hα': IntegrableOn (derivWithin α (Icc a b)) (Icc a b)) (hf: PiecewiseConstantOn f (Icc a b)) : IntegrableOn (f * derivWithin α (Icc a b)) (Icc a b) ∧ Chapter11.integ (f * derivWithin α (Icc a b)) (Icc a b) = RS_integ f (Icc a b) α := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:PiecewiseConstantOn f (Icc a b)⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ Chapter11.integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α -- This proof is adapted from the structure of the original text. a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).left⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:PiecewiseConstantOn f (Icc a b)α':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)⊢ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ Chapter11.integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ ∑ J ∈ P.intervals, Chapter11.integ (f * α') J = PiecewiseConstantWith.RS_integ f P α a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f P⊢ ∀ x ∈ P.intervals, Chapter11.integ (f * α') x = constant_value_on f ↑x * α[x]ₗ; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ (f * α') J = constant_value_on f ↑J * α[J]ₗ calc _ = Chapter11.integ ((constant_value_on f (J:Set ℝ)) • α') J := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ (f * α') J = Chapter11.integ (constant_value_on f ↑J • α') J a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Set.EqOn (f * α') (constant_value_on f ↑J • α') ↑J; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ (f * α') x = (constant_value_on f ↑J • α') x a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ f x * α' x = constant_value_on f ↑J * α' x; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalsx:ℝhx:x ∈ ↑J⊢ f x = constant_value_on f ↑J All goals completed! 🐙 _ = constant_value_on f (J:Set ℝ) * Chapter11.integ α' J := ((hα'.mono' (P.contains _ hJ)).smul _).2 _ = _ := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ Chapter11.integ α' J = α[J]ₗ have hJsub (hJab : J.a ≤ J.b) : J ⊆ Ioo (J.a - 1) (J.b + 1) := (subset_Icc J).trans (a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJab:J.a ≤ J.b⊢ Icc J.a J.b ⊆ Ioo (J.a - 1) (J.b + 1) All goals completed! 🐙) a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:0 = J.length⊢ Chapter11.integ α' J = α[J]ₗa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:0 < J.length⊢ Chapter11.integ α' J = α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:0 = J.length⊢ Chapter11.integ α' J = α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:0 = J.length⊢ 0 = α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b < J.a ∨ J.b - J.a = 0⊢ 0 = α[J]ₗ; a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b < J.a⊢ 0 = α[J]ₗa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ 0 = α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b < J.a⊢ 0 = α[J]ₗ All goals completed! 🐙 a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ 0 = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a ≤ J.b a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ 0 = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.b - J.a = 0⊢ J.a ≤ J.b All goals completed! 🐙 a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ Chapter11.integ α' J = α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ Chapter11.integ α' J = α J.b - α J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ J.a - 1 < J.aa:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ J.a ≤ J.ba:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ J.b < J.b + 1a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ J.a ≤ J.b a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.b⊢ Chapter11.integ α' J = α J.b - α J.a have : Icc J.a J.b ⊆ Icc a b := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α[J]ₗ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (@?_mvar.62247 hJab)hJab:J.a < J.bthis:?_mvar.138274 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ Icc J.a J.b ⊆ Icc a b simpa [closure_Ioo (show J.a ≠ J.b a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervals⊢ constant_value_on f ↑J * Chapter11.integ α' J = constant_value_on f ↑J * α[J]ₗ All goals completed! 🐙), subset_iff] using this calc _ = Chapter11.integ α' (Icc J.a J.b) := (hα'.mono' this).eq (subset_Icc J) rfl rfl _ = _ := a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (of_eq_true (Eq.trans (Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv._simp_1 (Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472)) (Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (Eq.trans (congr (congrArg Subset (Chapter11.BoundedInterval.set_Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472))) (Chapter11.BoundedInterval.set_Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) ((fun x_0 x_1 => propext ((fun x_0 x_1 => Set.Icc_subset_Ioo_iff hJab) x_0 x_1)) (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (congr (congrArg And (Eq.trans (div_lt_self_iff._simp_4 (Chapter11.BoundedInterval.a _fvar.60472)) zero_lt_one._simp_1)) (Eq.trans (lt_mul_iff_one_lt_right'._simp_4 (Chapter11.BoundedInterval.b _fvar.60472)) zero_lt_one._simp_1)) (and_self True)))))hJab:J.a < J.bthis:Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472) ⊆ Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ Chapter11.integ α' (Icc J.a J.b) = α J.b - α J.a convert integ_eq_antideriv_sub (a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (of_eq_true (Eq.trans (Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv._simp_1 (Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472)) (Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (Eq.trans (congr (congrArg Subset (Chapter11.BoundedInterval.set_Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472))) (Chapter11.BoundedInterval.set_Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) ((fun x_0 x_1 => propext ((fun x_0 x_1 => Set.Icc_subset_Ioo_iff hJab) x_0 x_1)) (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (congr (congrArg And (Eq.trans (div_lt_self_iff._simp_4 (Chapter11.BoundedInterval.a _fvar.60472)) zero_lt_one._simp_1)) (Eq.trans (lt_mul_iff_one_lt_right'._simp_4 (Chapter11.BoundedInterval.b _fvar.60472)) zero_lt_one._simp_1)) (and_self True)))))hJab:J.a < J.bthis:Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472) ⊆ Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ J.a ≤ J.b All goals completed! 🐙) (hα'.mono' this) _ a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (of_eq_true (Eq.trans (Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv._simp_1 (Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472)) (Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (Eq.trans (congr (congrArg Subset (Chapter11.BoundedInterval.set_Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472))) (Chapter11.BoundedInterval.set_Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) ((fun x_0 x_1 => propext ((fun x_0 x_1 => Set.Icc_subset_Ioo_iff hJab) x_0 x_1)) (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (congr (congrArg And (Eq.trans (div_lt_self_iff._simp_4 (Chapter11.BoundedInterval.a _fvar.60472)) zero_lt_one._simp_1)) (Eq.trans (lt_mul_iff_one_lt_right'._simp_4 (Chapter11.BoundedInterval.b _fvar.60472)) zero_lt_one._simp_1)) (and_self True)))))hJab:J.a < J.bthis:Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472) ⊆ Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ x ∈ Icc a b, HasDerivWithinAt α (α' x) (↑(Icc a b)) x a:ℝb:ℝα:ℝ → ℝf:ℝ → ℝhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αα':ℝ → ℝ := derivWithin _fvar.3558 ↑(Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557)hα':IntegrableOn α' (Icc a b)hf_integ:Chapter11.IntegrableOn _fvar.3559 (Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557) := (Chapter11.integ_of_piecewise_const _fvar.3563).lefthfα'_integ:IntegrableOn (f * α') (Icc a b)P:Partition (Icc a b)hP:PiecewiseConstantWith f PJ:BoundedIntervalhJ:J ∈ P.intervalshJsub:Chapter11.BoundedInterval.a _fvar.60472 ≤ Chapter11.BoundedInterval.b _fvar.60472 → _fvar.60472 ⊆ Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1) := fun hJab => HasSubset.Subset.trans (Chapter11.BoundedInterval.subset_Icc _fvar.60472) (of_eq_true (Eq.trans (Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv._simp_1 (Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472)) (Chapter11.BoundedInterval.Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (Eq.trans (congr (congrArg Subset (Chapter11.BoundedInterval.set_Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472))) (Chapter11.BoundedInterval.set_Ioo (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) ((fun x_0 x_1 => propext ((fun x_0 x_1 => Set.Icc_subset_Ioo_iff hJab) x_0 x_1)) (Chapter11.BoundedInterval.a _fvar.60472 - 1) (Chapter11.BoundedInterval.b _fvar.60472 + 1))) (Eq.trans (congr (congrArg And (Eq.trans (div_lt_self_iff._simp_4 (Chapter11.BoundedInterval.a _fvar.60472)) zero_lt_one._simp_1)) (Eq.trans (lt_mul_iff_one_lt_right'._simp_4 (Chapter11.BoundedInterval.b _fvar.60472)) zero_lt_one._simp_1)) (and_self True)))))hJab:J.a < J.bthis:Chapter11.BoundedInterval.Icc (Chapter11.BoundedInterval.a _fvar.60472) (Chapter11.BoundedInterval.b _fvar.60472) ⊆ Chapter11.BoundedInterval.Icc _fvar.3556 _fvar.3557 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)x✝:ℝa✝:x✝ ∈ Icc a b⊢ HasDerivWithinAt α (α' x✝) (↑(Icc a b)) x✝; All goals completed! 🐙 all_goals All goals completed! 🐙

Corollary 11.10.3

theorem declaration uses 'sorry'RS_integ_eq_integ_of_mul_deriv {a b:ℝ} (hab: a < b) {α f:ℝ → ℝ} (hα: Monotone α) (hα_diff: DifferentiableOn ℝ α (Icc a b)) (hαcont: Continuous α) (hα': IntegrableOn (derivWithin α (Icc a b)) (Icc a b)) (hf: RS_IntegrableOn f (Icc a b) α) : IntegrableOn (f * derivWithin α (Icc a b)) (Icc a b) ∧ integ (f * derivWithin α (Icc a b)) (Icc a b) = RS_integ f (Icc a b) α := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α -- This proof is adapted from the structure of the original text. a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α have hfα'_bound: BddOn (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ M⊢ BddOn (f * α') ↑(Icc a b); a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ N⊢ BddOn (f * α') ↑(Icc a b) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ N⊢ ∀ x ∈ ↑(Icc a b), |(f * α') x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝhM:∀ x ∈ ↑(Icc a b), |f x| ≤ MN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ Nx:ℝhx:x ∈ ↑(Icc a b)⊢ |(f * α') x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝhN:∀ x ∈ ↑(Icc a b), |α' x| ≤ Nx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ M⊢ |(f * α') x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ |(f * α') x| ≤ M * N a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ |f x| * |α' x| ≤ M * N; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)M:ℝN:ℝx:ℝhx:x ∈ ↑(Icc a b)hM:|f x| ≤ MhN:|α' x| ≤ N⊢ 0 ≤ M; All goals completed! 🐙 have hα'_nonneg : MajorizesOn α' 0 (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:x ∈ ↑(Icc a b)⊢ 0 x ≤ α' x a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:x ∈ ↑(Icc a b)⊢ ClusterPt x (Filter.principal (↑(Icc a b) \ {x})) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:x ∈ ↑(Icc a b)⊢ x ∈ closure (↑(Icc a b) \ {x}) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ b⊢ x ∈ closure (↑(Icc a b) \ {x}) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (↑(Icc a b) \ {x})a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (↑(Icc a b) \ {x}) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (↑(Icc a b) \ {x}) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (Set.Ico a x)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ Set.Ico a x ⊆ ↑(Icc a b) \ {x} a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < x⊢ x ∈ closure (Set.Ico a x) All goals completed! 🐙 a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a < xa✝¹:ℝa✝:a✝¹ ∈ Set.Ico a x⊢ a✝¹ ∈ ↑(Icc a b) \ {x}; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)x:ℝa✝¹:ℝhα_diff:DifferentiableOn ℝ α (Set.Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αhα':IntegrableOn α' (Icc a b)hfα'_bound:BddOn (f * α') (Set.Icc a b)hx:a ≤ x ∧ x ≤ bh:a < xa✝:a ≤ a✝¹ ∧ a✝¹ < x⊢ a✝¹ ≤ b ∧ ¬a✝¹ = x; All goals completed! 🐙 a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (Set.Ioc x b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ Set.Ioc x b ⊆ ↑(Icc a b) \ {x} a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a = x⊢ x ∈ closure (Set.Ioc x b) All goals completed! 🐙 a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461x:ℝhx:a ≤ x ∧ x ≤ bh:a = xa✝¹:ℝa✝:a✝¹ ∈ Set.Ioc x b⊢ a✝¹ ∈ ↑(Icc a b) \ {x}; All goals completed! 🐙 a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α have h1 : RS_integ f (Icc a b) α ≤ lower_integral (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ ε > 0, RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b); a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:ε > 0⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b) have ⟨ h, hhminor, hhconst, hh ⟩ := gt_of_lt_lower_RS_integral hf.1 hα (show RS_integ f (Icc a b) α - ε < lower_RS_integral f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < PiecewiseConstantOn.RS_integ h (Icc a b) αthis:?_mvar.225030 := Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv _fvar.157668 _fvar.157669 _fvar.158268 _fvar.224261⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < integ (h * derivWithin α ↑(Icc a b)) (Icc a b)this:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:ε > 0h:ℝ → ℝhhminor:MinorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:RS_integ f (Icc a b) α - ε < integ (h * derivWithin α ↑(Icc a b)) (Icc a b)this:Chapter11.lower_integral (_fvar.224257 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) = Chapter11.integ (_fvar.224257 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ RS_integ f (Icc a b) α - ε ≤ lower_integral (f * α') (Icc a b) have why : lower_integral (h * α') (Icc a b) ≤ lower_integral (f * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙 All goals completed! 🐙 have h2 : upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961⊢ ∀ (ε : ℝ), 0 < ε → upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε; a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961ε:ℝhε:0 < ε⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε have ⟨ h, hhmajor, hhconst, hh ⟩ := lt_of_gt_upper_RS_integral hf.1 hα (show upper_RS_integral f (Icc a b) α + ε > RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙) a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961ε:ℝhε:0 < εh:ℝ → ℝhhmajor:MajorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:PiecewiseConstantOn.RS_integ h (Icc a b) α < upper_RS_integral f (Icc a b) α + εthis:?_mvar.227724 := Chapter11.PiecewiseConstantOn.RS_integ_eq_integ_of_mul_deriv _fvar.157668 _fvar.157669 _fvar.158268 _fvar.226924⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961ε:ℝhε:0 < εh:ℝ → ℝhhmajor:MajorizesOn h f (Icc a b)hhconst:PiecewiseConstantOn h (Icc a b)hh:integ (h * derivWithin α ↑(Icc a b)) (Icc a b) < upper_RS_integral f (Icc a b) α + εthis:IntegrableOn (h * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (h * derivWithin α ↑(Icc a b)) (Icc a b) = PiecewiseConstantOn.RS_integ h (Icc a b) α⊢ upper_integral (f * α') (Icc a b) ≤ RS_integ f (Icc a b) α + ε have why : upper_integral (f * α') (Icc a b) ≤ upper_integral (h * α') (Icc a b) := a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhα':IntegrableOn (derivWithin α ↑(Icc a b)) (Icc a b)hf:RS_IntegrableOn f (Icc a b) α⊢ IntegrableOn (f * derivWithin α ↑(Icc a b)) (Icc a b) ∧ integ (f * derivWithin α ↑(Icc a b)) (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961h2:Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 := ?_mvar.226391h3:Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := Chapter11.lower_integral_le_upper _fvar.158462⊢ IntegrableOn (f * α') (Icc a b) ∧ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961h2:Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 := ?_mvar.226391h3:Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := Chapter11.lower_integral_le_upper _fvar.158462⊢ lower_integral (f * α') (Icc a b) = upper_integral (f * α') (Icc a b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961h2:Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 := ?_mvar.226391h3:Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := Chapter11.lower_integral_le_upper _fvar.158462⊢ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961h2:Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 := ?_mvar.226391h3:Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := Chapter11.lower_integral_le_upper _fvar.158462⊢ lower_integral (f * α') (Icc a b) = upper_integral (f * α') (Icc a b)a:ℝb:ℝhab:a < bα:ℝ → ℝf:ℝ → ℝhα:Monotone αhα_diff:DifferentiableOn ℝ α ↑(Icc a b)hαcont:Continuous αhf:RS_IntegrableOn f (Icc a b) αα':ℝ → ℝ := derivWithin _fvar.157665 ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663)hα':IntegrableOn α' (Icc a b)hfα'_bound:Chapter9.BddOn (_fvar.157666 * _fvar.158198) ↑(Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.158461hα'_nonneg:Chapter11.MajorizesOn _fvar.158198 0 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.178370h0:?_mvar.223835 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)h1:Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 ≤ Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := ?_mvar.223961h2:Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.RS_integ _fvar.157666 (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) _fvar.157665 := ?_mvar.226391h3:Chapter11.lower_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) ≤ Chapter11.upper_integral (_fvar.157666 * _fvar.158198) (Chapter11.BoundedInterval.Icc _fvar.157662 _fvar.157663) := Chapter11.lower_integral_le_upper _fvar.158462⊢ integ (f * α') (Icc a b) = RS_integ f (Icc a b) α All goals completed! 🐙

Lemma 11.10.5 / Exercise 11.10.2

theorem declaration uses 'sorry'PiecewiseConstantOn.RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f:ℝ → ℝ} (hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: PiecewiseConstantOn f (Icc (φ a) (φ b))) : PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) -- This proof is adapted from the structure of the original text. a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) replace hf : PiecewiseConstantWith f P := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468J:BoundedIntervalhJ:J ∈ P⊢ ConstantOn f ↑J; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))hf:PiecewiseConstantWith f P'P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468J:BoundedIntervalhJ:J ∈ P'.intervals ∧ (↑J).Nonempty⊢ ConstantOn f ↑J; All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = PiecewiseConstantWith.integ f P a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length have hφ_inv_bounded (J: P.intervals) : Bornology.IsBounded (φ_inv J) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)J:{ x // x ∈ P.intervals }⊢ φ_inv J ⊆ Set.Icc a b; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)J:{ x // x ∈ P.intervals }a✝:ℝ⊢ a✝ ∈ φ_inv J → a✝ ∈ Set.Icc a b; All goals completed! 🐙 have hφ_inv_connected (J: P.intervals) : (φ_inv J).OrdConnected := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length have hφ_inv_nonempty (J:P.intervals) : (φ_inv J).Nonempty := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 have hφ_inv_const {J:P.intervals} : ConstantOn (f ∘ φ) (φ_inv' J) ∧ constant_value_on (f ∘ φ) (φ_inv' J) = constant_value_on f J := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 set Q : Partition (Icc a b) := { intervals := .image φ_inv' .univ exists_unique x := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := fun J hJ => @_fvar.230472 J ⋯φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)x:ℝ⊢ x ∈ Icc a b → ∃! J, J ∈ Finset.image φ_inv' Finset.univ ∧ x ∈ J All goals completed! 🐙 contains K hK := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := fun J hJ => @_fvar.230472 J ⋯φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)K:BoundedIntervalhK:K ∈ Finset.image φ_inv' Finset.univ⊢ K ⊆ Icc a b All goals completed! 🐙 } have hfφ_piecewise : PiecewiseConstantWith (f ∘ φ) Q := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ RS_integ (f ∘ φ) (Icc a b) φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ PiecewiseConstantWith.RS_integ (f ∘ φ) Q φ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ ∑ J ∈ Q.intervals, constant_value_on (f ∘ φ) ↑J * φ[J]ₗ = ∑ J ∈ P.intervals, constant_value_on f ↑J * J.length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ ∑ x, constant_value_on (f ∘ φ) ↑(φ_inv' x) * φ[φ_inv' x]ₗ = ∑ i, constant_value_on f ↑↑i * (↑i).lengtha:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ Set.InjOn φ_inv' ↑Finset.univ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ ∑ x, constant_value_on (f ∘ φ) ↑(φ_inv' x) * φ[φ_inv' x]ₗ = ∑ i, constant_value_on f ↑↑i * (↑i).length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554⊢ ∀ x ∈ Finset.univ, constant_value_on (f ∘ φ) ↑(φ_inv' x) * φ[φ_inv' x]ₗ = constant_value_on f ↑↑x * (↑x).length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) * φ[φ_inv' J]ₗ = constant_value_on f ↑↑J * (↑J).length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝:J ∈ Finset.univ⊢ φ[φ_inv' J]ₗ = (↑J).length a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝:J ∈ Finset.univ⊢ constant_value_on (f ∘ φ) ↑(φ_inv' J) = constant_value_on f ↑↑J All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' K⊢ J = K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)⊢ J = K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:_fvar.245419 ∈ @_fvar.231268 _fvar.245393 := Set.Nonempty.some_mem (@_fvar.242662 _fvar.245393)⊢ J = K have h2 : x ∈ φ_inv K := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) rwa [hφ_inv' J, hJK, ←hφ_inv' Ka:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:x ∈ φ_inv K⊢ x ∈ φ_inv K at h1 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑K⊢ J = K have h3 : φ x ∈ Icc (φ a) (φ b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:PiecewiseConstantOn f (Icc (φ a) (φ b))⊢ PiecewiseConstantOn (f ∘ φ) (Icc a b) ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kthis:?_mvar.257712 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ φ x ∈ Icc (φ a) (φ b) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kthis:↑↑J ⊆ ↑(Icc (φ a) (φ b))⊢ φ x ∈ ↑(Icc (φ a) (φ b)) All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:@_fvar.230461 _fvar.245419 ∈ Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459) := ?_mvar.257706⊢ ↑J = ↑K; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:@_fvar.230461 _fvar.245419 ∈ Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459) := ?_mvar.257706⊢ ↑J ∈ P.intervals ∧ φ x ∈ ↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:@_fvar.230461 _fvar.245419 ∈ Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459) := ?_mvar.257706⊢ ↑K ∈ P.intervals ∧ φ x ∈ ↑K a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:@_fvar.230461 _fvar.245419 ∈ Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459) := ?_mvar.257706⊢ ↑J ∈ P.intervals ∧ φ x ∈ ↑Ja:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φP':Partition (Icc (φ a) (φ b))P:Chapter11.Partition (Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459)) := Chapter11.Partition.remove_empty _fvar.230468hf:Chapter11.PiecewiseConstantWith _fvar.230462 _fvar.230482 := ?_mvar.230593φ_inv:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_bounded:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_connected:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)φ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_nonempty:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hφ_inv_const:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)Q:Chapter11.Partition (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := { intervals := Finset.image _fvar.242283 Finset.univ, exists_unique := ⋯, contains := ⋯ }hfφ_piecewise:Chapter11.PiecewiseConstantWith (_fvar.230462 ∘ _fvar.230461) _fvar.243351 := ?_mvar.243553hfφ_piecewise':Chapter11.PiecewiseConstantOn (_fvar.230462 ∘ _fvar.230461) (Chapter11.BoundedInterval.Icc _fvar.230458 _fvar.230459) := Exists.intro _fvar.243351 _fvar.243554J:{ x // x ∈ P.intervals }a✝¹:J ∈ ↑Finset.univK:{ x // x ∈ P.intervals }a✝:K ∈ ↑Finset.univhJK:φ_inv' J = φ_inv' Kx:ℝ := Set.Nonempty.some (@_fvar.242662 _fvar.245393)h1:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Jh2:(a ≤ x ∧ x ≤ b) ∧ φ x ∈ ↑↑Kh3:@_fvar.230461 _fvar.245419 ∈ Chapter11.BoundedInterval.Icc (@_fvar.230461 _fvar.230458) (@_fvar.230461 _fvar.230459) := ?_mvar.257706⊢ ↑K ∈ P.intervals ∧ φ x ∈ ↑K All goals completed! 🐙

Proposition 11.10.6 (Change of variables formula II)

theorem declaration uses 'sorry'RS_integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ} (hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hf: IntegrableOn f (Icc (φ a) (φ b))) : RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) -- This proof is adapted from the structure of the original text. a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) have hfφ_bdd : BddOn (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) have hupper : upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ ∀ (ε : ℝ), 0 < ε → upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < ε⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε choose f_up hf_upmajor hf_upconst hf_up using lt_of_gt_upper_integral hf.1 (show upper_integral f (Icc (φ a) (φ b)) + ε > integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b)) < upper_integral f (Icc (φ a) (φ b)) + εhpc:?_mvar.265916 := Chapter11.PiecewiseConstantOn.RS_integ_of_comp _fvar.258845 _fvar.258848 _fvar.258849 _fvar.265908⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))⊢ upper_RS_integral (f ∘ φ) (Icc a b) φ ≤ upper_integral f (Icc (φ a) (φ b)) + ε have : MajorizesOn (f_up ∘ φ) (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝa✝:x✝ ∈ ↑(Icc a b)⊢ (f ∘ φ) x✝ ≤ (f_up ∘ φ) x✝; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)a✝:a ≤ x✝ ∧ x✝ ≤ b⊢ f (φ x✝) ≤ f_up (φ x✝); a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ε:ℝhε:0 < εf_up:ℝ → ℝhf_upmajor:MajorizesOn f_up f (Icc (φ a) (φ b))hf_upconst:PiecewiseConstantOn f_up (Icc (φ a) (φ b))hf_up:PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ < upper_integral f (Icc (φ a) (φ b)) + εhpc:PiecewiseConstantOn (f_up ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_up ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_up (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)a✝:a ≤ x✝ ∧ x✝ ≤ b⊢ φ x✝ ∈ ↑(Icc (φ a) (φ b)); All goals completed! 🐙 All goals completed! 🐙 have hlower : lower_integral f (Icc (φ a) (φ b)) ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012⊢ ∀ ε > 0, lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝhε:ε > 0⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ choose f_low hf_lowminor hf_lowconst hf_low using gt_of_lt_lower_integral hf.1 (show lower_integral f (Icc (φ a) (φ b)) - ε < lower_integral f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))hpc:?_mvar.482285 := Chapter11.PiecewiseConstantOn.RS_integ_of_comp _fvar.258845 _fvar.258848 _fvar.258849 _fvar.482277⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))⊢ lower_integral f (Icc (φ a) (φ b)) - ε ≤ lower_RS_integral (f ∘ φ) (Icc a b) φ have : MinorizesOn (f_low ∘ φ) (f ∘ φ) (Icc a b) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝhε:ε > 0f_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝa✝:x✝ ∈ ↑(Icc a b)⊢ (f_low ∘ φ) x✝ ≤ (f ∘ φ) x✝; a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝf_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)hε:0 < εa✝:a ≤ x✝ ∧ x✝ ≤ b⊢ f_low (φ x✝) ≤ f (φ x✝); a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012ε:ℝf_low:ℝ → ℝhf_lowminor:MinorizesOn f_low f (Icc (φ a) (φ b))hf_lowconst:PiecewiseConstantOn f_low (Icc (φ a) (φ b))hf_low:lower_integral f (Icc (φ a) (φ b)) - ε < PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φhpc:PiecewiseConstantOn (f_low ∘ φ) (Icc a b) ∧ PiecewiseConstantOn.RS_integ (f_low ∘ φ) (Icc a b) φ = PiecewiseConstantOn.integ f_low (Icc (φ a) (φ b))x✝:ℝhf_bdd:BddOn f (Set.Icc (φ a) (φ b))hfφ_bdd:BddOn (f ∘ φ) (Set.Icc a b)hε:0 < εa✝:a ≤ x✝ ∧ x✝ ≤ b⊢ φ x✝ ∈ ↑(Icc (φ a) (φ b)); All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012hlower:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) ≤ Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := ?_mvar.473148hle:Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := Chapter11.lower_RS_integral_le_upper _fvar.258967 _fvar.258849⊢ RS_IntegrableOn (f ∘ φ) (Icc a b) φ ∧ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012hlower:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) ≤ Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := ?_mvar.473148hle:Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := Chapter11.lower_RS_integral_le_upper _fvar.258967 _fvar.258849⊢ lower_RS_integral (f ∘ φ) (Icc a b) φ = upper_RS_integral (f ∘ φ) (Icc a b) φa:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012hlower:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) ≤ Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := ?_mvar.473148hle:Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := Chapter11.lower_RS_integral_le_upper _fvar.258967 _fvar.258849⊢ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012hlower:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) ≤ Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := ?_mvar.473148hle:Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := Chapter11.lower_RS_integral_le_upper _fvar.258967 _fvar.258849⊢ lower_RS_integral (f ∘ φ) (Icc a b) φ = upper_RS_integral (f ∘ φ) (Icc a b) φa:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_cont:Continuous φhφ_mono:Monotone φhf:IntegrableOn f (Icc (φ a) (φ b))hf_bdd:?_mvar.258853 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hfφ_bdd:Chapter9.BddOn (_fvar.258847 ∘ _fvar.258846) ↑(Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) := ?_mvar.258966heq:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) = Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hupper:Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) := ?_mvar.259012hlower:Chapter11.lower_integral _fvar.258847 (Chapter11.BoundedInterval.Icc (@_fvar.258846 _fvar.258843) (@_fvar.258846 _fvar.258844)) ≤ Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := ?_mvar.473148hle:Chapter11.lower_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 ≤ Chapter11.upper_RS_integral (_fvar.258847 ∘ _fvar.258846) (Chapter11.BoundedInterval.Icc _fvar.258843 _fvar.258844) _fvar.258846 := Chapter11.lower_RS_integral_le_upper _fvar.258967 _fvar.258849⊢ RS_integ (f ∘ φ) (Icc a b) φ = integ f (Icc (φ a) (φ b)) All goals completed! 🐙

Proposition 11.10.7 (Change of variables formula III)

theorem integ_of_comp {a b:ℝ} (hab: a < b) {φ f: ℝ → ℝ} (hφ_diff: DifferentiableOn ℝ φ (Icc a b)) (hφ_cont: Continuous φ) (hφ_mono: Monotone φ) (hφ': IntegrableOn (derivWithin φ (Icc a b)) (Icc a b)) (hf: IntegrableOn f (Icc (φ a) (φ b))) : IntegrableOn (f ∘ φ * derivWithin φ (Icc a b)) (Icc a b) ∧ integ (f ∘ φ * derivWithin φ (Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) := a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧ integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:?_mvar.740519 := Chapter11.RS_integ_of_comp _fvar.740509 _fvar.740513 _fvar.740514 _fvar.740516⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧ integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:?_mvar.740519 := Chapter11.RS_integ_of_comp _fvar.740509 _fvar.740513 _fvar.740514 _fvar.740516h2:?_mvar.740550 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ IntegrableOn (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) ∧ integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) refine ⟨ h2.1, a:ℝb:ℝhab:a < bφ:ℝ → ℝf:ℝ → ℝhφ_diff:DifferentiableOn ℝ φ ↑(Icc a b)hφ_cont:Continuous φhφ_mono:Monotone φhφ':IntegrableOn (derivWithin φ ↑(Icc a b)) (Icc a b)hf:IntegrableOn f (Icc (φ a) (φ b))h1:Chapter11.RS_IntegrableOn (_fvar.740511 ∘ _fvar.740510) (Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508) _fvar.740510 ∧ Chapter11.RS_integ (_fvar.740511 ∘ _fvar.740510) (Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508) _fvar.740510 = Chapter11.integ _fvar.740511 (Chapter11.BoundedInterval.Icc (@_fvar.740510 _fvar.740507) (@_fvar.740510 _fvar.740508)) := Chapter11.RS_integ_of_comp _fvar.740509 _fvar.740513 _fvar.740514 _fvar.740516h2:Chapter11.IntegrableOn (_fvar.740511 ∘ _fvar.740510 * derivWithin _fvar.740510 ↑(Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508)) (Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508) ∧ Chapter11.integ (_fvar.740511 ∘ _fvar.740510 * derivWithin _fvar.740510 ↑(Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508)) (Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508) = Chapter11.RS_integ (_fvar.740511 ∘ _fvar.740510) (Chapter11.BoundedInterval.Icc _fvar.740507 _fvar.740508) _fvar.740510 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)⊢ integ (f ∘ φ * derivWithin φ ↑(Icc a b)) (Icc a b) = integ f (Icc (φ a) (φ b)) All goals completed! 🐙 ⟩

Exercise 11.10.3

declaration uses 'sorry'example {a b:ℝ} (hab: a < b) {f: ℝ → ℝ} (hf: IntegrableOn f (Icc a b)) : IntegrableOn (fun x ↦ f (-x)) (Icc (-b) (-a)) ∧ integ (fun x ↦ f (-x)) (Icc (-b) (-a)) = -integ f (Icc a b) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:IntegrableOn f (Icc a b)⊢ IntegrableOn (fun x => f (-x)) (Icc (-b) (-a)) ∧ integ (fun x => f (-x)) (Icc (-b) (-a)) = -integ f (Icc a b) All goals completed! 🐙
/- Exercise 11.10.4: state and prove a version of `integ_of_comp` in which `φ` is `Antitone` rather than `Monotone`. -/ end Chapter11