Analysis I, Section 11.7: A non-Riemann integrable function

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

Proposition 11.7.1

theorem not_integrable : BddOn f_9_3_21 (Icc 0 1) ∧ ¬ IntegrableOn f_9_3_21 (Icc 0 1) := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) -- This proof is adapted from the structure of the original text. have hbdd: BddOn f_9_3_21 (Icc 0 1):= ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) ⊢ ∀ x ∈ ↑(Icc 0 1), |f_9_3_21 x| ≤ 1; x:ℝa✝:x ∈ ↑(Icc 0 1)⊢ |f_9_3_21 x| ≤ 1; x:ℝa✝:x ∈ ↑(Icc 0 1)h:∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1x:ℝa✝:x ∈ ↑(Icc 0 1)h:¬∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1 x:ℝa✝:x ∈ ↑(Icc 0 1)h:∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1x:ℝa✝:x ∈ ↑(Icc 0 1)h:¬∃ y, ↑y = x⊢ |f_9_3_21 x| ≤ 1 All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256⊢ ¬IntegrableOn f_9_3_21 (Icc 0 1) have hsup (P: Partition (Icc 0 1)) : ∀ J ∈ P.intervals, (sSup (f_9_3_21 '' (J:Set ℝ))) * |J|ₗ = |J|ₗ := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervals⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length; hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.lengthhbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0hJ0':?_mvar.8355 := _fvar.4184⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) * J.length = J.length hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) = 1 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) ≤ 1hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ 1 ≤ sSup (f_9_3_21 '' ↑J) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sSup (f_9_3_21 '' ↑J) ≤ 1 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonemptyhbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ b ∈ f_9_3_21 '' ↑J, b ≤ 1 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonempty hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':¬J.length = 0hJ0:f_9_3_21 '' ↑J = ∅⊢ Subsingleton ↑↑J; All goals completed! 🐙 All goals completed! 🐙 apply le_csSup_of_le _ _ (show (1:ℝ) ≤ 1 ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) All goals completed! 🐙) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ BddAbove (f_9_3_21 '' ↑J) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∃ x, ∀ y ∈ f_9_3_21 '' ↑J, y ≤ x; hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ y ∈ f_9_3_21 '' ↑J, y ≤ 1; All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.b⊢ 1 ∈ f_9_3_21 '' ↑J; hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.bz:ℝhz:z ∈ Set.range Rat.casthz':z ∈ Set.Ioo J.a J.b⊢ 1 ∈ f_9_3_21 '' ↑J P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz:∃ y, ↑y = zhz':J.a < z ∧ z < J.b⊢ ∃ x ∈ ↑J, ∃ y, ↑y = x; P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialq:ℚhz':J.a < ↑q ∧ ↑q < J.b⊢ ∃ x ∈ ↑J, ∃ y, ↑y = x exact ⟨ ↑q, (subset_iff _ _).mp (Ioo_subset J) (P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialq:ℚhz':J.a < ↑q ∧ ↑q < J.b⊢ ↑q ∈ ↑(Ioo J.a J.b) All goals completed! 🐙), q, rfl ⟩ have hupper (P: Partition (Icc 0 1)) : upper_riemann_sum f_9_3_21 P = 1 := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 PP:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = 1 calc _ = ∑ J ∈ P.intervals, |J|ₗ := hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sSup (f_9_3_21 '' ↑J) * J.length = ∑ J ∈ P.intervals, J.length hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)P:Partition (Icc 0 1)⊢ ∀ x ∈ P.intervals, sSup (f_9_3_21 '' ↑x) * x.length = x.length; All goals completed! 🐙 _ = _ := hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, J.length = 1 All goals completed! 🐙 replace hupper : upper_integral f_9_3_21 (Icc 0 1) = 1 := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) All goals completed! 🐙 have hinf (P: Partition (Icc 0 1)) : ∀ J ∈ P.intervals, (sInf (f_9_3_21 '' (J:Set ℝ))) * |J|ₗ = 0 := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervals⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0; hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0 All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬J.length = 0hJ0':?_mvar.75275 := _fvar.71051⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) * J.length = 0 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) = 0 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) ≤ 0hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ 0 ≤ sInf (f_9_3_21 '' ↑J) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ sInf (f_9_3_21 '' ↑J) ≤ 0 apply csInf_le_of_le _ _ (show (0:ℝ) ≤ 0 ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) All goals completed! 🐙) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ BddBelow (f_9_3_21 '' ↑J) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∃ x, ∀ y ∈ f_9_3_21 '' ↑J, x ≤ y; hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ y ∈ f_9_3_21 '' ↑J, 0 ≤ y; All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.b⊢ 0 ∈ f_9_3_21 '' ↑J hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':J.a < J.bz:ℝhz:z ∈ {x | Irrational x}hz':z ∈ Set.Ioo J.a J.b⊢ 0 ∈ f_9_3_21 '' ↑J hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.b⊢ ∃ x ∈ ↑J, ∀ (x_1 : ℚ), ¬↑x_1 = x refine ⟨ z, (subset_iff _ _).mp (Ioo_subset J) (hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)hupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.trans (Chapter11.upper_integ_eq_inf_upper_sum _fvar.257) (Eq.trans (congrArg sInf (Eq.trans (congrArg Set.range (funext fun P => (@fun P => @_fvar.47746 P) P)) Set.range_const)) (csInf_singleton 1)))) (eq_self 1))P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.b⊢ z ∈ ↑(Ioo J.a J.b) All goals completed! 🐙), ?_ ⟩ hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhz:Irrational zhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.bq:ℚ⊢ ¬↑q = z; hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':J.a < J.bz:ℝhbdd:BddOn f_9_3_21 (Set.Icc 0 1)hJ0:(↑J).Nontrivialhz':J.a < z ∧ z < J.bq:ℚhz:↑q = z⊢ ¬Irrational z; All goals completed! 🐙 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonemptyhbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ ∀ b ∈ f_9_3_21 '' ↑J, 0 ≤ b hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0:¬Subsingleton ↑↑JhJ0':¬J.length = 0⊢ (f_9_3_21 '' ↑J).Nonempty hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425P:Partition (Icc 0 1)J:BoundedIntervalhJ:J ∈ P.intervalshJ0':¬J.length = 0hJ0:f_9_3_21 '' ↑J = ∅⊢ Subsingleton ↑↑J; All goals completed! 🐙 All goals completed! 🐙 have hlower (P: Partition (Icc 0 1)) : lower_riemann_sum f_9_3_21 P = 0 := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := ?_mvar.256hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P => @?_mvar.4106 Phupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := ?_mvar.68425hinf:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sInf (Chapter9.f_9_3_21 '' ↑J) * J.length = 0 := fun P => @?_mvar.70973 PP:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = 0; calc _ = ∑ J ∈ P.intervals, (0:ℝ) := hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)hupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.trans (Chapter11.upper_integ_eq_inf_upper_sum _fvar.257) (Eq.trans (congrArg sInf (Eq.trans (congrArg Set.range (funext fun P => (@fun P => @_fvar.47746 P) P)) Set.range_const)) (csInf_singleton 1)))) (eq_self 1))hinf:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sInf (Chapter9.f_9_3_21 '' ↑J) * J.length = 0 := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congrArg (fun x => x = 0) (Eq.trans (congrArg (HMul.hMul (sInf (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sInf (Chapter9.f_9_3_21 '' ↑J))))) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sInf (Chapter9.f_9_3_21 '' ↑J) * J.length) (0 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sInf (Chapter9.f_9_3_21 '' ↑J)) 0 (le_antisymm (csInf_le_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddBelow_def))) (Exists.intro 0 (Chapter11.not_integrable._proof_6 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 0) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_right_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) one_ne_zero._simp_1) imp_false._simp_1) not_exists._simp_1)))))) (Exists.intro z ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => z ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).1)) (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).2)) (and_self True)))), fun q => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_not_eq (↑q = z)) (Eq.refl ¬Irrational z))) fun hz => of_eq_true (Eq.trans (congrArg Not (Eq.trans (congrArg Irrational (Eq.symm hz)) (Rat.not_irrational._simp_1 q))) not_false_eq_true)) x.left⟩)) (Classical.choose (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Eq.refl true); this)) (le_csInf (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_7 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) J.length J.length (Eq.refl J.length))) 0 0 (Eq.refl 0))) (zero_mul J.length)P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, sInf (f_9_3_21 '' ↑J) * J.length = ∑ J ∈ P.intervals, 0 hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)hupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.trans (Chapter11.upper_integ_eq_inf_upper_sum _fvar.257) (Eq.trans (congrArg sInf (Eq.trans (congrArg Set.range (funext fun P => (@fun P => @_fvar.47746 P) P)) Set.range_const)) (csInf_singleton 1)))) (eq_self 1))hinf:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sInf (Chapter9.f_9_3_21 '' ↑J) * J.length = 0 := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congrArg (fun x => x = 0) (Eq.trans (congrArg (HMul.hMul (sInf (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sInf (Chapter9.f_9_3_21 '' ↑J))))) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sInf (Chapter9.f_9_3_21 '' ↑J) * J.length) (0 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sInf (Chapter9.f_9_3_21 '' ↑J)) 0 (le_antisymm (csInf_le_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddBelow_def))) (Exists.intro 0 (Chapter11.not_integrable._proof_6 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 0) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_right_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) one_ne_zero._simp_1) imp_false._simp_1) not_exists._simp_1)))))) (Exists.intro z ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => z ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).1)) (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).2)) (and_self True)))), fun q => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_not_eq (↑q = z)) (Eq.refl ¬Irrational z))) fun hz => of_eq_true (Eq.trans (congrArg Not (Eq.trans (congrArg Irrational (Eq.symm hz)) (Rat.not_irrational._simp_1 q))) not_false_eq_true)) x.left⟩)) (Classical.choose (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Eq.refl true); this)) (le_csInf (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_7 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) J.length J.length (Eq.refl J.length))) 0 0 (Eq.refl 0))) (zero_mul J.length)P:Partition (Icc 0 1)⊢ ∀ x ∈ P.intervals, sInf (f_9_3_21 '' ↑x) * x.length = 0; All goals completed! 🐙 _ = _ := hbdd:Chapter9.BddOn Chapter9.f_9_3_21 ↑(Chapter11.BoundedInterval.Icc 0 1) := Exists.intro 1 fun x a => if h : ∃ y, ↑y = x then of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_true 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_true h)))) abs_one)) (le_refl._simp_1 1)) else of_eq_true (Eq.trans (congrArg (fun x => x ≤ 1) (Eq.trans (congrArg abs (ite_cond_eq_false 1 0 (Eq.trans (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) (eq_false h)))) abs_zero)) zero_le_one._simp_1)hsup:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sSup (Chapter9.f_9_3_21 '' ↑J) * J.length = J.length := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congr (congrArg Eq (Eq.trans (congrArg (HMul.hMul (sSup (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sSup (Chapter9.f_9_3_21 '' ↑J))))) hJ0) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sSup (Chapter9.f_9_3_21 '' ↑J) * J.length) (1 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sSup (Chapter9.f_9_3_21 '' ↑J)) 1 (le_antisymm (csSup_le (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_3 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0')) (le_csSup_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddAbove_def))) (Exists.intro 1 (Chapter11.not_integrable._proof_4 _fvar.257 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 1) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_left_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg Not (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1)) not_exists._simp_1) zero_ne_one._simp_1) imp_false._simp_1) (Eq.trans Classical.not_forall._simp_1 (congrArg Exists (funext fun x_1 => Decidable.not_not._simp_1))))))))) (Exists.casesOn (Eq.mp Set.mem_range._simp_1 x.left) fun q h => Eq.ndrec (motive := fun z => J.a < z ∧ z < J.b → ∃ x ∈ ↑J, ∃ y, ↑y = x) (fun hz' => Exists.intro ↑q ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => ↑q ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true hz'.1)) (eq_true hz'.2)) (and_self True)))), Exists.intro q rfl⟩) h (Eq.mp Set.mem_Ioo._simp_1 x.right))) (Classical.choose (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between Rat.denseRange_cast (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl true); this))) J.length J.length (Eq.refl J.length))) J.length J.length (Eq.refl J.length))) (one_mul J.length)hupper:Chapter11.upper_integral Chapter9.f_9_3_21 (Chapter11.BoundedInterval.Icc 0 1) = 1 := of_eq_true (Eq.trans (congrArg (fun x => x = 1) (Eq.trans (Chapter11.upper_integ_eq_inf_upper_sum _fvar.257) (Eq.trans (congrArg sInf (Eq.trans (congrArg Set.range (funext fun P => (@fun P => @_fvar.47746 P) P)) Set.range_const)) (csInf_singleton 1)))) (eq_self 1))hinf:∀ (P : Chapter11.Partition (Chapter11.BoundedInterval.Icc 0 1)), ∀ J ∈ P.intervals, sInf (Chapter9.f_9_3_21 '' ↑J) * J.length = 0 := fun P J hJ => if hJ0 : J.length = 0 then of_eq_true (Eq.trans (congrArg (fun x => x = 0) (Eq.trans (congrArg (HMul.hMul (sInf (Chapter9.f_9_3_21 '' ↑J))) hJ0) (mul_zero (sInf (Chapter9.f_9_3_21 '' ↑J))))) (eq_self 0)) else have hJ0' := hJ0; Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (sInf (Chapter9.f_9_3_21 '' ↑J) * J.length) (0 * J.length) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 a'_1 e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_5 ≍ x → a * a_1 ≍ a' * a'_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_5 : a = a'), e_5 ≍ Eq.refl a → a * a_1 ≍ a' * a'_1) (fun e_5 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_6 ≍ x → a * a_1 ≍ a * a'_1) e'_6 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_6 : a_1 = a'), e_6 ≍ Eq.refl a_1 → a * a_1 ≍ a * a') (fun e_6 h => HEq.refl (a * a_1)) (Eq.symm h) e'_6) (Eq.refl a'_1) (HEq.refl e'_6)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) ℝ ℝ ℝ instHMul (sInf (Chapter9.f_9_3_21 '' ↑J)) 0 (le_antisymm (csInf_le_of_le (Eq.mpr (id (congrArg (fun _a => _a) (propext bddBelow_def))) (Exists.intro 0 (Chapter11.not_integrable._proof_6 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) ((fun z x => Eq.mpr (id (Eq.trans (Set.mem_image._simp_1 Chapter9.f_9_3_21 (↑J) 0) (congrArg Exists (funext fun x => congrArg (And (x ∈ ↑J)) (Eq.trans ite_eq_right_iff._simp_1 (Eq.trans (Eq.trans (implies_congr (Eq.trans (congrArg (fun x_1 => x ∈ x_1) Set.image_univ) Set.mem_range._simp_1) one_ne_zero._simp_1) imp_false._simp_1) not_exists._simp_1)))))) (Exists.intro z ⟨(Chapter11.BoundedInterval.subset_iff (Chapter11.BoundedInterval.Ioo J.a J.b) J).mp (Chapter11.BoundedInterval.Ioo_subset J) (of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => z ∈ x) (Chapter11.BoundedInterval.set_Ioo J.a J.b)) Set.mem_Ioo._simp_1) (Eq.trans (congr (congrArg And (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).1)) (eq_true (Eq.mp Set.mem_Ioo._simp_1 x.right).2)) (and_self True)))), fun q => Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_not_eq (↑q = z)) (Eq.refl ¬Irrational z))) fun hz => of_eq_true (Eq.trans (congrArg Not (Eq.trans (congrArg Irrational (Eq.symm hz)) (Rat.not_irrational._simp_1 q))) not_false_eq_true)) x.left⟩)) (Classical.choose (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0'))) (Classical.choose_spec (Dense.exists_between dense_irrational (Eq.mp (Eq.trans (congrArg Not (Eq.trans sup_eq_right._simp_1 (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le J.b) (zero_add J.a))))) not_le._simp_1) hJ0')))) (have this := Mathlib.Meta.NormNum.isNat_le_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Eq.refl true); this)) (le_csInf (Mathlib.Tactic.Contrapose.mtr (Eq.mpr (id (implies_congr (Mathlib.Tactic.PushNeg.not_nonempty_eq (Chapter9.f_9_3_21 '' ↑J)) (Mathlib.Tactic.PushNeg.not_not_eq (Subsingleton ↑↑J)))) fun hJ0 => of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => Subsingleton ↑x) (id (Eq.mp Set.image_eq_empty._simp_1 hJ0))) (Set.subsingleton_coe._simp_1 ∅)) Set.subsingleton_empty._simp_1)) (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0)) (Chapter11.not_integrable._proof_7 _fvar.257 _fvar.4107 _fvar.68426 P J hJ (Eq.mp (congrArg (fun _a => ¬_a) (Eq.symm (propext Chapter11.BoundedInterval.length_of_subsingleton))) hJ0) hJ0'))) J.length J.length (Eq.refl J.length))) 0 0 (Eq.refl 0))) (zero_mul J.length)P:Partition (Icc 0 1)⊢ ∑ J ∈ P.intervals, 0 = 0 All goals completed! 🐙 replace hlower : lower_integral f_9_3_21 (Icc 0 1) = 0 := ⊢ BddOn f_9_3_21 ↑(Icc 0 1) ∧ ¬IntegrableOn f_9_3_21 (Icc 0 1) All goals completed! 🐙 All goals completed! 🐙
end Chapter11