internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[>] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, a < x
h✝ : ∀ᶠ (x : ℝ) in 𝓝[>] a, f x ≤ f a
x : ℝ
ha : a < x
h : f x ≤ f a
⊢ 0 ≤ x - a
Tactic:
linarith only [ha]
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.IsLocalMin.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.IsLocalExtr.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ f' = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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)
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
  sorry
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
  sorry
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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⟩
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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:
sorry
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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:
sorry
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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)
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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'⟩
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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 ↦ ?_⟩
Proof 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}
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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')]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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⟩
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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⟩
Proof 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
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]
Proof state after:
no goals
Theorem: Tutorial.exists_local_extr_Ioo
Proof 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]
Proof state after:
no goals
Theorem: Tutorial.exists_hasDerivAt_eq_zero
Proof state before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hfI : f a = f b
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = 0
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.exists_ratio_hasDerivAt_eq_ratio_slope
Proof state before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
let h x := (g b - g a) * f x - (f b - f a) * g x
Proof state after:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Theorem: Tutorial.exists_ratio_hasDerivAt_eq_ratio_slope
Proof state before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have hhc : ContinuousOn h (Icc a b) :=
  (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
Proof state after:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Theorem: Tutorial.exists_ratio_hasDerivAt_eq_ratio_slope
Proof state before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.exists_hasDerivAt_eq_slope
Proof state before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.comp_app
Proof state before:
C : Type u
inst✝ : Category C
a b c d e : C
X Y Z : Type
f : Hom X Y
g : Hom Y Z
x : X
⊢ (f ≫ g) x = g (f x)
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.id_app
Proof state before:
C : Type u
inst✝ : Category C
a b c d e : C
X : Type
x : X
⊢ 𝟙 X x = x
Tactic:
rfl
Proof state after:
no goals
Theorem: Tutorial.Category.Initial.uniq'
Proof state before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ f = h.fromInitial b
Tactic:
rw [h.uniq f]
Proof state after:
no goals
Theorem: Tutorial.Category.Initial.uniq'
Proof state before:
C : Type u
inst✝ : Category C
a : C
h : Initial a
b : C
f g : Hom a b
⊢ h.fromInitial b = g
Tactic:
rw [h.uniq g]
Proof state after:
no goals
Theorem: Tutorial.Coequalizer.hom_id
Proof state before:
J : Type u₁
inst✝¹ : Category J
C : Type u₂
inst✝ : Category C
F : Functor J C
i : Shape
⊢ ShapeHom.id i = 𝟙 i
Tactic:
cases i <;> rfl
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ 0 ≤ f'
Tactic:
have hf : Tendsto (fun x ↦ (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f') := by
  rw [hasDerivAt_iff_tendsto_slope] at hf
  apply hf.mono_left (nhds_left'_le_nhds_ne a)
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ 0 ≤ f'
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ 0 ≤ f'
Tactic:
suffices ∀ᶠ x in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0 from ge_of_tendsto hf this
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
have ha : ∀ᶠ x in 𝓝[<] a, x < a := eventually_nhdsWithin_of_forall fun x hx ↦ hx
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
have h : ∀ᶠ x in 𝓝[<] a, f x ≤ f a := h.filter_mono nhdsWithin_le_nhds
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ᶠ (x : ℝ) in 𝓝[<] a, (f x - f a) / (x - a) ≥ 0
Tactic:
filter_upwards [ha, h]
Proof state after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ a_1 < a, f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≥ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
⊢ ∀ a_1 < a, f a_1 ≤ f a → (f a_1 - f a) / (a_1 - a) ≥ 0
Tactic:
intro x ha h
Proof state after:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≥ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
case h
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ (f x - f a) / (x - a) ≥ 0
Tactic:
apply div_nonneg_of_nonpos
Proof state after:
case h.ha
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ f x - f a ≤ 0

case h.hb
f : ℝ → ℝ
f' x✝ a b : ℝ
h✝¹ : IsLocalMax f a
hf✝ : HasDerivAt f f' a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
ha✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ x - a ≤ 0
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : HasDerivAt f f' a
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')
Tactic:
rw [hasDerivAt_iff_tendsto_slope] at hf
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMax f a
hf : Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[≠] a) (𝓝 f')
⊢ Tendsto (fun x => (f x - f a) / (x - a)) (𝓝[<] a) (𝓝 f')