-- Mathlib/Topology/Order/Rolle.lean
theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
    ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ 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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : ¬f C = f a
⊢ C = b → f C = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]

Result:
no goals

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C :=
  isCompact_Icc.exists_isMaxOn ne hfc

Result:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
h : c = b
⊢ f c = f a

Tactic:
rw [h, hfI]

Result:
no goals

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : f c = f a
hC : f C = f a
this : ∀ 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}

Tactic:
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]

Result:
no goals

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩

Result:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ 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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ 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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
⊢ c = b → f c = f a

Tactic:
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]

Result:
no goals

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
C : X
Cmem : C ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
hc : ¬f c = f a
h : a = c
⊢ f c = f a

Tactic:
rw [h]

Result:
no goals

Proof state:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

Tactic:
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x :=
  isCompact_Icc.exists_isMinOn ne hfc

Result:
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
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : (Icc a b).Nonempty
c : X
cmem : c ∈ Icc a b
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c