internlm/Lean-Github huggingface dataset:
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
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')
Tactic:
apply hf.mono_left (nhds_left'_le_nhds_ne a)
Proof state after:
no goals
Theorem: Tutorial.IsLocalMax.hasDerivAt_eq_zero
Proof state before:
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
Tactic:
linarith
Proof state after:
no goals
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, x < a
h✝ : ∀ᶠ (x : ℝ) in 𝓝[<] a, f x ≤ f a
x : ℝ
ha : x < a
h : f x ≤ f a
⊢ x - a ≤ 0
Tactic:
linarith
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:
suffices -f' = 0 from neg_eq_zero.mp this
Proof state after:
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ -f' = 0
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:
apply IsLocalMax.hasDerivAt_eq_zero
Proof state after:
case h
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ IsLocalMax ?f ?a

case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt ?f (-f') ?a

case f
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ → ℝ

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ
Theorem: Tutorial.IsLocalMin.hasDerivAt_eq_zero
Proof state before:
case h
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ IsLocalMax ?f ?a

case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt ?f (-f') ?a

case f
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ → ℝ

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ ℝ
Tactic:
apply IsLocalMin.neg h
Proof state after:
case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun x => -f x) (-f') a
Theorem: Tutorial.IsLocalMin.hasDerivAt_eq_zero
Proof state before:
case hf
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ HasDerivAt (fun x => -f x) (-f') a
Tactic:
apply hf.neg
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:
apply IsLocalExtr.elim h
Proof state after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMin f a → f' = 0

case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMax f a → f' = 0
Theorem: Tutorial.IsLocalExtr.hasDerivAt_eq_zero
Proof state before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMin f a → f' = 0
Tactic:
intro h
Proof state after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMin f a
⊢ f' = 0
Theorem: Tutorial.IsLocalExtr.hasDerivAt_eq_zero
Proof state before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMin f a
⊢ f' = 0
Tactic:
apply IsLocalMin.hasDerivAt_eq_zero h hf
Proof state after:
no goals
Theorem: Tutorial.IsLocalExtr.hasDerivAt_eq_zero
Proof state before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h : IsLocalExtr f a
hf : HasDerivAt f f' a
⊢ IsLocalMax f a → f' = 0
Tactic:
intro h
Proof state after:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMax f a
⊢ f' = 0
Theorem: Tutorial.IsLocalExtr.hasDerivAt_eq_zero
Proof state before:
case a
f : ℝ → ℝ
f' x a b : ℝ
h✝ : IsLocalExtr f a
hf : HasDerivAt f f' a
h : IsLocalMax f a
⊢ f' = 0
Tactic:
apply IsLocalMax.hasDerivAt_eq_zero h hf
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 ∈ 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
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
  apply isCompact_Icc.exists_isMinOn ne hfc
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 ∈ Icc a b, IsMaxOn f (Icc a b) C
Tactic:
apply isCompact_Icc.exists_isMaxOn ne hfc
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:
apply isCompact_Icc.exists_isMinOn ne hfc
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:
have ⟨c, cmem, hc⟩ := exists_local_extr_Ioo hab hfc hfI
Proof state after:
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 : ℝ
cmem : c ∈ Ioo a b
hc : IsLocalExtr f c
⊢ ∃ c ∈ Ioo a b, f' c = 0
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 : ℝ
cmem : c ∈ Ioo a b
hc : IsLocalExtr f c
⊢ ∃ c ∈ Ioo a b, f' c = 0
Tactic:
exact ⟨c, cmem, IsLocalExtr.hasDerivAt_eq_zero hc <| hff' c cmem⟩
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
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:
have hI : h a = h b := by ring
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)
hI : h a = h 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)
hI : h a = h b
⊢ ∃ 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
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
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
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
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 hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
  intro x hx
  apply ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
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)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) 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
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have ⟨c, cmem, hc⟩ := exists_hasDerivAt_eq_zero hab hhc hI hhh'
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)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ 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)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
exact ⟨c, cmem, sub_eq_zero.mp hc⟩
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
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ h a = h b
Tactic:
ring
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
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
Tactic:
intro x hx
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)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
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)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
Tactic:
apply ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
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:
have ⟨c, cmem, hc⟩ := exists_ratio_hasDerivAt_eq_ratio_slope hab hfc hff'
  continuousOn_id fun x _ ↦ hasDerivAt_id 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
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
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 : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic:
exact ⟨c, cmem, by rw [eq_div_iff (by linarith), mul_comm]; simpa using hc⟩
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 : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)
Tactic:
rw [eq_div_iff (by linarith), mul_comm]
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
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ (b - a) * f' c = f b - f a
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 : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ (b - a) * f' c = f b - f a
Tactic:
simpa using hc
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 : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ b - a ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Tutorial.inv_smul_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ a⁻¹ • a • x = x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.smul_inv_smul
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x : X
⊢ a • a⁻¹ • x = x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
⊢ Function.Injective fun x => a • x
Tactic:
intro x y (h : a • x = a • y)
Proof state after:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = y
Theorem: Tutorial.GroupAction.injective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
x y : X
h : a • x = a • y
⊢ x = y
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupAction.surjective
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
a : G
⊢ Function.Surjective fun x => a • x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.orbit_eq_orbit_iff_mem_orbit
Proof state before:
G X : Type
inst✝¹ : Group G
inst✝ : GroupAction G X
x y : X
⊢ orbit G x = orbit G y ↔ y ∈ orbit G x
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
⊢ a * b ∈ N → b * a ∈ N
Tactic:
intro hab
Proof state after:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a ∈ N
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a ∈ N
Tactic:
calc
  b * a = b * a⁻¹⁻¹ := by simp
  _ = a⁻¹ * (a * b) * a⁻¹⁻¹ := by simp
  _ ∈ N := by
    apply Normal.conj_mem a⁻¹ (a * b) hab
Proof state after:
no goals
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a = b * a⁻¹⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ b * a⁻¹⁻¹ = a⁻¹ * (a * b) * a⁻¹⁻¹
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.Subgroup.mem_comm
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Normal N
a b : G
hab : a * b ∈ N
⊢ a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ N
Tactic:
apply Normal.conj_mem a⁻¹ (a * b) hab
Proof state after:
no goals
Theorem: Tutorial.mem_of_eq_one
Proof state before:
G : Type
inst✝¹ : Group G
N : Subgroup G
inst✝ : Subgroup.Normal N
a : G
⊢ LeftQuotient.mk a = 1 ↔ a ∈ N
Tactic:
simp [N.inv_mem_iff]
Proof state after:
no goals
Theorem: Tutorial.Subgroup.coe_one
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
K : Subgroup G
⊢ 1 ∈ K
Tactic:
simp
Proof state after:
no goals
Theorem: Tutorial.GroupHom.rangeKerLift_injective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ Function.Injective ⇑(rangeKerLift f)
Tactic:
rw [injective_iff_map_eq_one]
Proof state after:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ (a : G ⧸ ker f), (rangeKerLift f) a = 1 → a = 1
Theorem: Tutorial.GroupHom.rangeKerLift_injective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ ∀ (a : G ⧸ ker f), (rangeKerLift f) a = 1 → a = 1
Tactic:
rintro ⟨_⟩
Proof state after:
case mk
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
a✝¹ : G ⧸ ker f
a✝ : G
⊢ (rangeKerLift f) (Quot.mk Setoid.r a✝) = 1 → Quot.mk Setoid.r a✝ = 1
Theorem: Tutorial.GroupHom.rangeKerLift_injective
Proof state before:
case mk
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
a✝¹ : G ⧸ ker f
a✝ : G
⊢ (rangeKerLift f) (Quot.mk Setoid.r a✝) = 1 → Quot.mk Setoid.r a✝ = 1
Tactic:
simp_all
Proof state after:
no goals
Theorem: Tutorial.GroupHom.rangeKerLift_surjective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ Function.Surjective ⇑(rangeKerLift f)
Tactic:
intro ⟨y, hy⟩
Proof state after:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
hy : y ∈ range f
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := hy }
Theorem: Tutorial.GroupHom.rangeKerLift_surjective
Proof state before:
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
hy : y ∈ range f
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := hy }
Tactic:
rcases hy with ⟨x, hxy⟩
Proof state after:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := ⋯ }
Theorem: Tutorial.GroupHom.rangeKerLift_surjective
Proof state before:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ ∃ a, (rangeKerLift f) a = { val := y, property := ⋯ }
Tactic:
exists LeftQuotient.mk x
Proof state after:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ (rangeKerLift f) (LeftQuotient.mk x) = { val := y, property := ⋯ }
Theorem: Tutorial.GroupHom.rangeKerLift_surjective
Proof state before:
case intro
G H : Type
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
y : H
x : G
hxy : f x = y
⊢ (rangeKerLift f) (LeftQuotient.mk x) = { val := y, property := ⋯ }
Tactic:
simpa
Proof state after:
no goals
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 = 1
Tactic:
have h : f 1 * f 1 = f 1 * 1 := by
  sorry
Proof state after:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
h : f 1 * f 1 = f 1 * 1
⊢ f 1 = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.map_one
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
⊢ f 1 * f 1 = f 1 * 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.map_inv
Proof state before:
G₁ G₂ : Type
inst✝¹ : Group G₁
inst✝ : Group G₂
f : G₁ →* G₂
a : G₁
⊢ f a⁻¹ = (f a)⁻¹
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Injective ⇑f ↔ ∀ (a : G₁), f a = 1 → a = 1
Tactic:
constructor
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Injective ⇑f → ∀ (a : G₁), f a = 1 → a = 1

case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → Function.Injective ⇑f
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ Function.Injective ⇑f → ∀ (a : G₁), f a = 1 → a = 1
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.injective_iff_map_eq_one
Proof state before:
case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → Function.Injective ⇑f
Tactic:
sorry
Proof state after:
no goals
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ Function.Injective ⇑f
Tactic:
rw [injective_iff_map_eq_one]
Proof state after:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ ∀ (a : G₁), f a = 1 → a = 1
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ ↔ ∀ (a : G₁), f a = 1 → a = 1
Tactic:
constructor
Proof state after:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ → ∀ (a : G₁), f a = 1 → a = 1

case mpr
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ (∀ (a : G₁), f a = 1 → a = 1) → ker f = ⊥
Theorem: Tutorial.GroupHom.ker_eq_bot
Proof state before:
case mp
G₁ G₂ G : Type
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G
f : G₁ →* G₂
⊢ ker f = ⊥ → ∀ (a : G₁), f a = 1 → a = 1
Tactic:
sorry
Proof state after:
no goals