[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
have ne : (Icc a b).Nonempty :=
  nonempty_Icc.2
    (le_of_lt hab)
      -- Consider absolute min and max points
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x := isCompact_Icc.exists_forall_le ne hfc
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C := isCompact_Icc.exists_forall_ge ne hfc
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
by_cases hc : f c = f a
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
by_cases hC : f C = f a
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
have : ∀ x ∈ Icc a b, f x = f a := fun x hx =>
  le_antisymm (hC ▸ Cge x hx)
    (hc ▸ cle x hx)
      -- `f` is a constant, so we can take any point in `Ioo a b`
[GOAL]
case pos
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
[GOAL]
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
c' : X
hc' : c' ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
[GOAL]
case pos.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : X), x ∈ Icc a b → f x = f a
c' : X
hc' : c' ∈ Ioo a b
x : X
hx : x ∈ Icc a b
⊢ x ∈ {x | (fun x => f c' ≤ f x) x}
[PROOFSTEP]
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩
[GOAL]
case neg.refine'_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a
case neg.refine'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ C = b → f C = f a
[PROOFSTEP]
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : a = C
⊢ f C = f a
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
h : C = b
⊢ f C = f a
[PROOFSTEP]
rw [h, hfI]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
[PROOFSTEP]
refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩
[GOAL]
case neg.refine'_1
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a
case neg.refine'_2
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a
[PROOFSTEP]
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : a = c
⊢ f c = f a
[PROOFSTEP]
rw [h]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : X
cmem : c ∈ Icc a b
cle : ∀ (x : X), x ∈ Icc a b → f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ (x : X), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : c = b
⊢ f c = f a
[PROOFSTEP]
rw [h, hfI]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
[GOAL]
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
  exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hab.ne hfc ha hb)
    ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder X
inst✝⁵ : DenselyOrdered X
inst✝⁴ : TopologicalSpace X
inst✝³ : OrderTopology X
inst✝² : LinearOrder Y
inst✝¹ : TopologicalSpace Y
inst✝ : OrderTopology Y
f : X → Y
a b : X
l : Y
hab : a < b
hfc✝ : ContinuousOn f (Ioo a b)
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 l)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 l)
h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b)
c : X
hc : c ∈ Ioo a b
hfc : IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Ioo a b) c
[PROOFSTEP]
exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩
