Theorem: Tutorial.exists_local_extr_Ioo (Solution/Advanced/Analysis/Lecture2.lean)

State before:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsLocalExtr f c
Tactic:
suffices ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c by
  rcases this with ⟨c, cmem, hc⟩
  exists c, cmem
  apply hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2
State after:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab)
State after:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
have ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, IsMaxOn f (Icc a b) C := by
  apply isCompact_Icc.exists_isMaxOn ne hfc
State after:
f : ℝ → ℝ
f' x 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
Cge : IsMaxOn f (Icc a b) C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x 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
Cge : IsMaxOn f (Icc a b) C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
have ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, IsMinOn f (Icc a b) c := by
  apply isCompact_Icc.exists_isMinOn ne hfc
State after:
f : ℝ → ℝ
f' x 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
Cge : IsMaxOn f (Icc a b) C
c : ℝ
cmem : c ∈ Icc a b
cle : IsMinOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x 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
Cge : IsMaxOn f (Icc a b) C
c : ℝ
cmem : c ∈ Icc a b
cle : IsMinOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
change ∀ x ∈ Icc a b, f x ≤ f C at Cge
State after:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
cle : IsMinOn f (Icc a b) c
Cge : ∀ x ∈ Icc a b, f x ≤ f C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
cle : IsMinOn f (Icc a b) c
Cge : ∀ x ∈ Icc a b, f x ≤ f C
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
change ∀ x ∈ Icc a b, f c ≤ f x at cle
State after:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
by_cases hc : f c = f a
State after:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

case neg
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
this : ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsLocalExtr f c
Tactic:
rcases this with ⟨c, cmem, hc⟩
State after:
case intro.intro
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
c : ℝ
cmem : c ∈ Ioo a b
hc : IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsLocalExtr f c

State before:
case intro.intro
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
c : ℝ
cmem : c ∈ Ioo a b
hc : IsExtrOn f (Icc a b) c
⊢ ∃ c ∈ Ioo a b, IsLocalExtr f c
Tactic:
exists c, cmem
State after:
case intro.intro
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
c : ℝ
cmem : c ∈ Ioo a b
hc : IsExtrOn f (Icc a b) c
⊢ IsLocalExtr f c

State before:
case intro.intro
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
c : ℝ
cmem : c ∈ Ioo a b
hc : IsExtrOn f (Icc a b) c
⊢ IsLocalExtr f c
Tactic:
apply hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2
State after:
no goals

State before:
f : ℝ → ℝ
f' x a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
ne : Set.Nonempty (Icc a b)
⊢ ∃ C ∈ Icc a b, IsMaxOn f (Icc a b) C
Tactic:
apply isCompact_Icc.exists_isMaxOn ne hfc
State after:
no goals

State before:
f : ℝ → ℝ
f' x 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
Cge : IsMaxOn f (Icc a b) C
⊢ ∃ c ∈ Icc a b, IsMinOn f (Icc a b) c
Tactic:
apply isCompact_Icc.exists_isMinOn ne hfc
State after:
no goals

State before:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
by_cases hC : f C = f a
State after:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

case neg
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
have : ∀ x ∈ Icc a b, f x = f a := fun x hx ↦ le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx)
State after:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
case pos
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
State after:
case pos.intro
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c

State before:
case pos.intro
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ x ∈ Icc a b, f x = f a
c' : ℝ
hc' : c' ∈ Ioo a b
⊢ ∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
Tactic:
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
State after:
case pos.intro
f : ℝ → ℝ
f' x✝ 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ 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}

State before:
case pos.intro
f : ℝ → ℝ
f' x✝ 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : f C = f a
this : ∀ 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}
Tactic:
simp [this x hx, this c' (Ioo_subset_Icc_self hc')]
State after:
no goals

State before:
case neg
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
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.inr Cge⟩
State after:
case neg.refine_1
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a

case neg.refine_2
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
⊢ C = b → f C = f a

State before:
case neg.refine_1
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
⊢ a = C → f C = f a

case neg.refine_2
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
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]]
State after:
no goals

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
h : a = C
⊢ f C = f a
Tactic:
rw [h]
State after:
no goals

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : f c = f a
hC : ¬f C = f a
h : C = b
⊢ f C = f a
Tactic:
rw [h, hfI]
State after:
no goals

State before:
case neg
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
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⟩
State after:
case neg.refine_1
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
⊢ a = c → f c = f a

case neg.refine_2
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
⊢ c = b → f c = f a

State before:
case neg.refine_1
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
⊢ a = c → f c = f a

case neg.refine_2
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
⊢ c = b → f c = f a
Tactic:
exacts [fun h ↦ by rw [h], fun h ↦ by rw [h, hfI]]
State after:
no goals

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
h : a = c
⊢ f c = f a
Tactic:
rw [h]
State after:
no goals

State before:
f : ℝ → ℝ
f' x 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
c : ℝ
cmem : c ∈ Icc a b
Cge : ∀ x ∈ Icc a b, f x ≤ f C
cle : ∀ x ∈ Icc a b, f c ≤ f x
hc : ¬f c = f a
h : c = b
⊢ f c = f a
Tactic:
rw [h, hfI]
State after:
no goals