Analysis I, Section 9.7: The intermediate value theorem

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 Chapter9

Theorem 9.7.1 (Intermediate value theorem)

theorem declaration uses 'sorry'intermediate_value {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) {y:ℝ} (hy: y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)) : ∃ c ∈ Set.Icc a b, f c = y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y -- This proof is written to follow the structure of the original text. a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_right:y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:y = f a⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:y = f a⊢ a ∈ Set.Icc a b ∧ f a = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f a⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:y = f b⊢ ∃ c ∈ Set.Icc a b, f c = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:y = f b⊢ b ∈ Set.Icc a b ∧ f b = ya:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:y ∈ Set.Icc (f a) (f b)hya:¬y = f ahyb:¬y = f b⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhya:¬y = f ahyb:¬y = f bhy_left:f a ≤ y ∧ y ≤ f b⊢ ∃ c ∈ Set.Icc a b, f c = y replace hya : f a < y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace hyb : y < f b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_Icc⊢ ∃ c ∈ Set.Icc a b, f c = y have hEa : a ∈ E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have hE_nonempty : E.Nonempty := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ ∃ c ∈ Set.Icc a b, f c = y have hc : c ∈ Set.Icc a b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ a ≤ c ∧ c ≤ b; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ a ≤ ca:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ c ≤ b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ a ≤ c All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647⊢ b = sSup (Set.Icc a b) All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968⊢ f c = y have hfc_upper : f c ≤ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y have hxe (n:ℕ) : ∃ x ∈ E, c - 1/(n+1:ℝ) < x := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c - 1/(n+1:ℝ) < sSup E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)⊢ f c ≤ y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))⊢ f c ≤ y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ f c ≤ y have : Filter.atTop.Tendsto x (nhds c) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ Filter.Tendsto (fun j => c - 1 / (↑j + 1)) Filter.atTop (nhds c)a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ Filter.Tendsto (fun j => c) Filter.atTop (nhds c)a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ (fun j => c - 1 / (↑j + 1)) ≤ xa:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ x ≤ fun j => c a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ Filter.Tendsto (fun j => c - 1 / (↑j + 1)) Filter.atTop (nhds c) a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ c = c - 0;All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ Filter.Tendsto (fun j => c) Filter.atTop (nhds c) All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).right⊢ (fun j => c - 1 / (↑j + 1)) ≤ x All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx1:∀ (n : ℕ), @_fvar.28811 n ∈ _fvar.10647 := fun n => (Exists.choose_spec (@_fvar.20806 n)).left (Exists.choose (@_fvar.20806 n) ∈ _fvar.10647) (_fvar.14696 - 1 / (↑n + 1) < Exists.choose (@_fvar.20806 n))hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).rightthis:?_mvar.31280 := Filter.Tendsto.comp_of_continuous _fvar.14969 (ContinuousOn.continuousWithinAt _fvar.479 _fvar.14969) (fun n => @_fvar.10942 (@_fvar.28811 n) (@_fvar.29108 n)) _fvar.29616⊢ f c ≤ y have hfxny (n:ℕ) : f (x n) ≤ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).rightthis:?_mvar.31280 := Filter.Tendsto.comp_of_continuous _fvar.14969 (ContinuousOn.continuousWithinAt _fvar.479 _fvar.14969) (fun n => @_fvar.10942 (@_fvar.28811 n) (@_fvar.29108 n)) _fvar.29616n:ℕhx1:x n ∈ E⊢ f (x n) ≤ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hxe:∀ (n : ℕ), ∃ x ∈ _fvar.10647, _fvar.14696 - 1 / (↑n + 1) < x := fun n => @?_mvar.20805 nx:ℕ → ℝ := fun n => Exists.choose (@_fvar.20806 n)hx2:∀ (n : ℕ), _fvar.14696 - 1 / (↑n + 1) < @_fvar.28811 n := fun n => (Exists.choose_spec (@_fvar.20806 n)).rightthis:?_mvar.31280 := Filter.Tendsto.comp_of_continuous _fvar.14969 (ContinuousOn.continuousWithinAt _fvar.479 _fvar.14969) (fun n => @_fvar.10942 (@_fvar.28811 n) (@_fvar.29108 n)) _fvar.29616n:ℕhx1:(a ≤ x n ∧ x n ≤ b) ∧ f (x n) < y⊢ f (x n) ≤ y; All goals completed! 🐙 All goals completed! 🐙 have hne : c < b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have hfc_lower : y ≤ f c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y have : ∃ N:ℕ, ∀ n ≥ N, (c+1/(n+1:ℝ)) < b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑N⊢ ∃ N, ∀ n ≥ N, c + 1 / (↑n + 1) < b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑N⊢ ∀ n ≥ N, c + 1 / (↑n + 1) < b; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ N⊢ c + 1 / (↑n + 1) < b have hpos : 0 < b-c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 have : 1/(n+1:ℝ) < b-c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 1 / (b - c) < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 0 < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 0 < b - c a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 1 / (b - c) < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 0 < ↑n + 1a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ 0 < b - c (try All goals completed! 🐙); a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ ↑N < ↑n + 1; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:1 / (b - c) < ↑Nn:ℕhn:n ≥ Nhpos:0 < _fvar.476 - _fvar.14696 := ?_mvar.42172⊢ N < n + 1; All goals completed! 🐙 All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < b⊢ y ≤ f c have hmem : ∀ n ≥ N, (c + 1/(n+1:ℝ)) ∈ Set.Icc a b := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bn:ℕhn:n ≥ N⊢ c + 1 / (↑n + 1) ∈ Set.Icc a b a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bn:ℕhn:n ≥ N⊢ a ≤ c + 1 / (↑n + 1) have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c + 1/(n+1:ℝ) > c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 have : ∀ n ≥ N, c + 1/(n+1:ℝ) ∉ E := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260n:ℕa✝:n ≥ N⊢ c + 1 / (↑n + 1) ∉ E have : 1/(n+1:ℝ) > 0 := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 replace : c + 1/(n+1:ℝ) > c := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙 All goals completed! 🐙 replace : ∀ n ≥ N, f (c + 1/(n+1:ℝ)) ≥ y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∉ _fvar.10647 := ?_mvar.76679n:ℕhn:n ≥ N⊢ f (c + 1 / (↑n + 1)) ≥ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260n:ℕhn:n ≥ Nthis:c + 1 / (↑n + 1) ∉ E⊢ f (c + 1 / (↑n + 1)) ≥ y; a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260n:ℕhn:n ≥ Nthis:f (c + 1 / (↑n + 1)) < y⊢ c + 1 / (↑n + 1) ∈ E a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260n:ℕhn:n ≥ Nthis:f (c + 1 / (↑n + 1)) < y⊢ (a ≤ c + (↑n + 1)⁻¹ ∧ c + (↑n + 1)⁻¹ ≤ b) ∧ f (c + (↑n + 1)⁻¹) < y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260n:ℕhn:n ≥ Nthis✝:f (c + 1 / (↑n + 1)) < ythis:?_mvar.92598 := @_fvar.61261 _fvar.86954 _fvar.86957⊢ (a ≤ c + (↑n + 1)⁻¹ ∧ c + (↑n + 1)⁻¹ ≤ b) ∧ f (c + (↑n + 1)⁻¹) < y All goals completed! 🐙 have hconv : Filter.atTop.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) (nhds c) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945⊢ c = c + 0; All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:?_mvar.122028 := ContinuousWithinAt.tendsto (ContinuousOn.continuousWithinAt _fvar.479 _fvar.14969)⊢ y ≤ f c a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))⊢ y ≤ f c have hconv' : Filter.atTop.Tendsto (fun n:ℕ ↦ c + 1/(n+1:ℝ)) (.principal (.Icc a b)) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b)⊢ ∃ c ∈ Set.Icc a b, f c = y a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))⊢ ∃ a_1, ∀ (b_1 : ℕ), a_1 ≤ b_1 → c + 1 / (↑b_1 + 1) ∈ Set.Icc a b; All goals completed! 🐙 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':?_mvar.128805 := Filter.tendsto_inf.mpr ⟨_fvar.120616, _fvar.122748⟩⊢ y ≤ f c a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':?_mvar.128805 := Filter.tendsto_inf.mpr ⟨_fvar.120616, _fvar.122748⟩⊢ ∀ᶠ (c_1 : ℕ) in Filter.atTop, y ≤ (f ∘ fun n => c + 1 / (↑n + 1)) c_1 a:ℝb:ℝhab:a < bf:ℝ → ℝy:ℝhy_left:f a ≤ y ∧ y ≤ f bhya:@_fvar.478 _fvar.475 < _fvar.480 := ?_mvar.6730hyb:_fvar.480 < @_fvar.478 _fvar.476 := ?_mvar.8623E:Set ℝ := {x | x ∈ Set.Icc _fvar.475 _fvar.476 ∧ @_fvar.478 x < _fvar.480}hE:_fvar.10647 ⊆ Set.Icc _fvar.475 _fvar.476 := fun x x_1 => match x_1 with | ⟨hx₁, hx₂⟩ => hx₁hE_bdd:BddAbove _fvar.10647 := BddAbove.mono _fvar.10942 bddAbove_IcchEa:_fvar.475 ∈ _fvar.10647 := ?_mvar.11251hE_nonempty:Set.Nonempty _fvar.10647 := ?_mvar.14664c:ℝ := sSup _fvar.10647hc:_fvar.14696 ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.14968hfc_upper:@_fvar.478 _fvar.14696 ≤ _fvar.480 := ?_mvar.20457hne:_fvar.14696 < _fvar.476 := ?_mvar.39327N:ℕhN:∀ n ≥ N, c + 1 / (↑n + 1) < bhmem:∀ n ≥ _fvar.60822, _fvar.14696 + 1 / (↑n + 1) ∈ Set.Icc _fvar.475 _fvar.476 := ?_mvar.61260this:∀ n ≥ _fvar.60822, @_fvar.478 (_fvar.14696 + 1 / (↑n + 1)) ≥ _fvar.480 := ?_mvar.86945hconv:Filter.Tendsto (fun n => _fvar.14696 + 1 / (↑n + 1)) Filter.atTop (nhds _fvar.14696) := ?_mvar.120615hf:Filter.Tendsto f (nhds c ⊓ Filter.principal (Set.Icc a b)) (nhds (f c))hconv':?_mvar.128805 := Filter.tendsto_inf.mpr ⟨_fvar.120616, _fvar.122748⟩⊢ ∃ a, ∀ (b : ℕ), a ≤ b → y ≤ f (c + 1 / (↑b + 1)); All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙
open Classical in noncomputable abbrev f_9_7_1 : ℝ → ℝ := fun x ↦ if x ≤ 0 then -1 else 1declaration uses 'sorry'example : 0 ∈ Set.Icc (f_9_7_1 (-1)) (f_9_7_1 1) ∧ ¬ ∃ x ∈ Set.Icc (-1) 1, f_9_7_1 x = 0 := ⊢ 0 ∈ Set.Icc (f_9_7_1 (-1)) (f_9_7_1 1) ∧ ¬∃ x ∈ Set.Icc (-1) 1, f_9_7_1 x = 0 All goals completed! 🐙

Remark 9.7.2

abbrev f_9_7_2 : ℝ → ℝ := fun x ↦ x^3 - x
declaration uses 'sorry'example : f_9_7_2 (-2) = -6 := ⊢ f_9_7_2 (-2) = -6 All goals completed! 🐙declaration uses 'sorry'example : f_9_7_2 2 = 6 := ⊢ f_9_7_2 2 = 6 All goals completed! 🐙declaration uses 'sorry'example : f_9_7_2 (-1) = 0 := ⊢ f_9_7_2 (-1) = 0 All goals completed! 🐙declaration uses 'sorry'example : f_9_7_2 0 = 0 := ⊢ f_9_7_2 0 = 0 All goals completed! 🐙declaration uses 'sorry'example : f_9_7_2 1 = 0 := ⊢ f_9_7_2 1 = 0 All goals completed! 🐙

Remark 9.7.3

declaration uses 'sorry'example : ∃ x:ℝ, 0 ≤ x ∧ x ≤ 2 ∧ x^2 = 2 := ⊢ ∃ x, 0 ≤ x ∧ x ≤ 2 ∧ x ^ 2 = 2 All goals completed! 🐙

Corollary 9.7.4 (Images of continuous functions) / Exercise 9.7.1

theorem declaration uses 'sorry'continuous_image_Icc {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) {y:ℝ} (hy: sInf (f '' .Icc a b) ≤ y ∧ y ≤ sSup (f '' .Icc a b)) : ∃ c ∈ Set.Icc a b, f c = y := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)y:ℝhy:sInf (f '' Set.Icc a b) ≤ y ∧ y ≤ sSup (f '' Set.Icc a b)⊢ ∃ c ∈ Set.Icc a b, f c = y All goals completed! 🐙
theorem declaration uses 'sorry'continuous_image_Icc' {a b:ℝ} (hab: a < b) {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc a b)) : f '' .Icc a b = .Icc (sInf (f '' .Icc a b)) (sSup (f '' .Icc a b)) := a:ℝb:ℝhab:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)⊢ f '' Set.Icc a b = Set.Icc (sInf (f '' Set.Icc a b)) (sSup (f '' Set.Icc a b)) All goals completed! 🐙

Exercise 9.7.2

theorem declaration uses 'sorry'exists_fixed_pt {f:ℝ → ℝ} (hf: ContinuousOn f (.Icc 0 1)) (hmap: f '' .Icc 0 1 ⊆ .Icc 0 1) : ∃ x ∈ Set.Icc 0 1, f x = x := f:ℝ → ℝhf:ContinuousOn f (Set.Icc 0 1)hmap:f '' Set.Icc 0 1 ⊆ Set.Icc 0 1⊢ ∃ x ∈ Set.Icc 0 1, f x = x All goals completed! 🐙
end Chapter9