awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
hf₁ :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
rw [(nhdsGT_basis a).tendsto_left_iff] at hf

Premises used: nhdsGT_basis, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
hf₁ :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a₁ : ContinuousWithinAt f (Ici a) a
⊢ Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))

Tactic:
rw [(nhdsGT_basis a).tendsto_left_iff] at hf

Premises used: nhdsGT_basis, Filter.HasBasis.tendsto_left_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
obtain :
  ∀ (b : ℝ) (hab : a < b) (hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))),
    ∃ (i : ℝ),
      a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1

Tactic:
obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)

Premises used: Set.Ioi, Filter.Ioi_mem_atTop, derivWithin, HAdd.hAdd, Max.max, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1

Tactic:
⟨b, hab, fun x hx z hz => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))
refine :
  ∀ (x : ℝ) (hx : x ∈ Ioo a b) (z : ℝ) (hz : z ∈ Ioc a x), max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) z
⊢ ∃ (i : ℝ),
    a < i ∧ ∀ ⦃x : ℝ⦄, x ∈ Ioo a i → ∀ x_1 ∈ Ioc a x, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x_1

Tactic:
refine ⟨b, hab, fun x hx z hz => ?_⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
hb : MapsTo (derivWithin f (Ioi a)) (Ioo a b) (Ioi (max (derivWithin f (Ioi a) a + 1) 0))
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
⊢ ∀ ⦃x : ℝ⦄, a < x → x < b → max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x

Tactic:
simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb

Premises used: Set.mem_Ioo, and_imp, Set.mem_Ioi, Set.MapsTo
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
hb : ∀ ⦃x : ℝ⦄, a < x → x < b → max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) z

Tactic:
hb hz.1 <| hz.2.trans_lt hx.2

Premises used: And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf :
  ∀ (t : Set ℝ), Membership.mem (γ := Filter ℝ) atTop t → ∃ (i : ℝ), a < i ∧ MapsTo (derivWithin f (Ioi a)) (Ioo a i) t
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
b : ℝ
hab : a < b
x : ℝ
hx : x ∈ Ioo a b
z : ℝ
hz : z ∈ Ioc a x
hb : ∀ ⦃x : ℝ⦄, a < x → x < b → max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) z

Tactic:
exact hb hz.1 <| hz.2.trans_lt hx.2

Premises used: And.right, And.left, LE.le.trans_lt
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x

Tactic:
have h₀ : ∀ᶠ b in 𝓝[>] a,
        ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x := by
      rw [(nhdsGT_basis a).eventually_iff]
      rw [(nhdsGT_basis a).tendsto_left_iff] at hf
      obtain ⟨b, hab, hb⟩ := hf (Ioi (max (derivWithin f (Ioi a) a + 1) 0)) (Ioi_mem_atTop _)
      refine ⟨b, hab, fun x hx z hz => ?_⟩
      simp only [MapsTo, mem_Ioo, mem_Ioi, and_imp] at hb
      exact hb hz.1 <| hz.2.trans_lt hx.2
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2

Tactic:
rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff

Premises used: nhds_basis_Ioo, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hdiff₁ :
  ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x

Tactic:
rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff

Premises used: nhds_basis_Ioo, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff :
  ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1 < derivWithin f (Ioi a) a ∧
    derivWithin f (Ioi a) a < (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff :
  ∀ (i : ℝ × ℝ),
    i.1 < derivWithin f (Ioi a) a ∧ derivWithin f (Ioi a) a < i.2 → ∀ᶠ (x : ℝ) in 𝓝[>] a, slope f a x ∈ Ioo i.1 i.2
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a,
    slope f a x ∈
      Ioo (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1
        (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2

Tactic:
specialize hdiff ⟨derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1⟩ <| by simp

Premises used: Set.Ioi, HSub.hSub, Prod.mk, derivWithin, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hdiff :
  ∀ᶠ (x : ℝ) in 𝓝[>] a,
    slope f a x ∈
      Ioo (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1
        (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2
z : ℝ
hz : slope f a z ∈ Ioo (derivWithin f (Ioi a) a - 1) (derivWithin f (Ioi a) a + 1)
⊢ slope f a z < derivWithin f (Ioi a) a + 1

Tactic:
hz.2

Premises used: And.right
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hdiff :
  ∀ᶠ (x : ℝ) in 𝓝[>] a,
    slope f a x ∈
      Ioo (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1
        (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  slope f a x ∈
                    Ioo (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).1
                      (derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1).2)
                x}
            x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (b : ℝ) ↦ slope f a b < derivWithin f (Ioi a) a + 1) x} x}
      a_1
h₁ h₂ :
  ∀ (z : ℝ) (hz : slope f a z ∈ Ioo (derivWithin f (Ioi a) a - 1) (derivWithin f (Ioi a) a + 1)),
    slope f a z < derivWithin f (Ioi a) a + 1
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1

Tactic:
filter_upwards [hdiff] with z hz using hz.2
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
⊢ ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1

Tactic:
have h₁ : ∀ᶠ b in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1 := by
      rw [(nhds_basis_Ioo _).tendsto_right_iff] at hdiff
      specialize hdiff ⟨derivWithin f (Ioi a) a - 1, derivWithin f (Ioi a) a + 1⟩ <| by simp
      filter_upwards [hdiff] with z hz using hz.2
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
h : ∀ (hab : a < b), False
⊢ b ∈ Ioi a → False

Tactic:
(hab : a < b)
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
h :
  ∀ (b : ℝ) (hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x)
    (hslope : slope f a b < derivWithin f (Ioi a) a + 1) (hab : a < b), False
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] a, False

Tactic:
filter_upwards [h₀, h₁, eventually_mem_nhdsWithin] with b hb hslope (hab : a < b)

Premises used: eventually_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
⊢ DifferentiableWithinAt ℝ f (Ioc a b) z

Tactic:
DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, DifferentiableWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
refine : DifferentiableWithinAt ℝ f (Ioi a) z
⊢ DifferentiableWithinAt ℝ f (Ioc a b) z

Tactic:
refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self

Premises used: Set.Ioc_subset_Ioi_self, DifferentiableWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
⊢ 0 < derivWithin f (Ioi a) z

Tactic:
simp_all only [and_imp, mem_Ioc, max_lt_iff]

Premises used: and_imp, max_lt_iff, Set.mem_Ioc
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
⊢ derivWithin f (Ioi a) z ≠ 0

Tactic:
have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by
          simp_all only [and_imp, mem_Ioc, max_lt_iff]
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
this : derivWithin f (Ioi a) z ≠ 0
⊢ DifferentiableWithinAt ℝ f (Ioi a) z

Tactic:
differentiableWithinAt_of_derivWithin_ne_zero this

Premises used: differentiableWithinAt_of_derivWithin_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
z : ℝ
hz : z ∈ Ioc a b
this : derivWithin f (Ioi a) z ≠ 0
⊢ DifferentiableWithinAt ℝ f (Ioi a) z

Tactic:
exact differentiableWithinAt_of_derivWithin_ne_zero this

Premises used: differentiableWithinAt_of_derivWithin_ne_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
⊢ DifferentiableOn ℝ f (Ioc a b)

Tactic:
have hdiff' : DifferentiableOn ℝ f (Ioc a b) := fun z hz => by
        refine DifferentiableWithinAt.mono (t := Ioi a) ?_ Ioc_subset_Ioi_self
        have : derivWithin f (Ioi a) z ≠ 0 := ne_of_gt <| by
          simp_all only [and_imp, mem_Ioc, max_lt_iff]
        exact differentiableWithinAt_of_derivWithin_ne_zero this
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
(hdiff'.continuousOn z hz'').mono_of_mem_nhdsWithin ?_

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
refine : Ioc a b ∈ 𝓝[Icc a b] z
⊢ ContinuousWithinAt f (Icc a b) z

Tactic:
refine (hdiff'.continuousOn z hz'').mono_of_mem_nhdsWithin ?_

Premises used: DifferentiableOn.continuousOn, ContinuousWithinAt.mono_of_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
⊢ 𝓝[Ioc a b] z = 𝓝[Icc a b] z

Tactic:
nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_

Premises used: Ioi_mem_nhds, nhdsWithin_eq_nhdsWithin', And.left
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
refine : Ioc a b ∩ Ioi a = Icc a b ∩ Ioi a
⊢ 𝓝[Ioc a b] z = 𝓝[Icc a b] z

Tactic:
refine nhdsWithin_eq_nhdsWithin' (s := Ioi a) (Ioi_mem_nhds hz''.1) ?_

Premises used: Ioi_mem_nhds, nhdsWithin_eq_nhdsWithin', And.left
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
simp : Ioc a b = Icc a b ∩ Ioi a
⊢ Ioc a b ∩ Ioi a = Icc a b ∩ Ioi a

Tactic:
simp only [Ioc_inter_Ioi, le_refl, sup_of_le_left]

Premises used: le_refl, Set.Ioc_inter_Ioi, sup_of_le_left
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
h : ∀ (y : ℝ), y ∈ Ioc a b ↔ y ∈ Icc a b ∩ Ioi a
⊢ Ioc a b = Icc a b ∩ Ioi a

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.MeanValue
Goal:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (derivWithin f (Ioi a)) (𝓝[>] a) atTop
hcont_at_a : ContinuousWithinAt f (Ici a) a
hdiff : Tendsto (slope f a) (𝓝[>] a) (𝓝 (derivWithin f (Ioi a) a))
h₀ : ∀ᶠ (b : ℝ) in 𝓝[>] a, ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
h₁ : ∀ᶠ (b : ℝ) in 𝓝[>] a, slope f a b < derivWithin f (Ioi a) a + 1
b : ℝ
hb : ∀ x ∈ Ioc a b, max (derivWithin f (Ioi a) a + 1) 0 < derivWithin f (Ioi a) x
hslope : slope f a b < derivWithin f (Ioi a) a + 1
hab : a < b
hdiff' : DifferentiableOn ℝ f (Ioc a b)
z : ℝ
hz'' : z ∈ Ioc a b
y : ℝ
⊢ y ∈ Ioc a b ↔ y ∈ Icc a b ∩ Ioi a

Tactic:
⟨fun h => ⟨mem_Icc_of_Ioc h, mem_of_mem_inter_left h⟩, fun ⟨H1, H2⟩ => ⟨H2, H1.2⟩⟩

Premises used: _private.0.not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi.match_7, Set.Ioc, Set.mem_Icc_of_Ioc, Membership.mem, Set.mem_of_mem_inter_left, And.right, And.intro, Iff.intro