f f' : ℝ → ℝ
a b : ℝ
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
f f' : ℝ → ℝ
a b : ℝ
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
have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
case intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
f f' : ℝ → ℝ
a b : ℝ
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
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
  isCompact_Icc.exists_forall_le ne hfc
case intro.intro.intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
case intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
  isCompact_Icc.exists_forall_ge ne hfc
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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

case neg
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
case intro.intro.intro.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
by_cases hc : f c = f a
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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

case neg
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
by_cases hC : f C = f a
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
case pos.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
case pos
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
case pos.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ {x | (fun x => f c' ≤ f x) x}
case pos.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
⊢ ∃ c, c ∈ Ioo a b ∧ IsExtrOn f (Icc a b) c
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
no goals
case pos.intro
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ (x : ℝ), x ∈ Icc a b → f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
x : ℝ
hx : x ∈ Icc a b
⊢ x ∈ {x | (fun x => f c' ≤ f x) x}
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
case neg.refine'_1
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
case neg
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
refine' ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt _ hC, lt_of_le_of_ne Cmem.2 <| mt _ hC⟩, Or.inr Cge⟩
no goals
case neg.refine'_1
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
no goals
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
rw [h]
no goals
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
rw [h, hfI]
case neg.refine'_1
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a

case neg.refine'_2
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a
case neg
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (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
refine' ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt _ hc, lt_of_le_of_ne cmem.2 <| mt _ hc⟩, Or.inl cle⟩
no goals
case neg.refine'_1
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ a = c → f c = f a

case neg.refine'_2
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
no goals
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : a = c
⊢ f c = f a
rw [h]
no goals
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
c : ℝ
cmem : c ∈ Icc a b
cle : ∀ (x : ℝ), x ∈ Icc a b → f c ≤ f x
C : ℝ
Cmem : C ∈ Icc a b
Cge : ∀ (x : ℝ), x ∈ Icc a b → f x ≤ f C
hc : ¬f c = f a
h : c = b
⊢ f c = f a
rw [h, hfI]