-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic [CompleteSpace E]
    (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Iic a)) :
    Tendsto f atBot (𝓝 (limUnder atBot f))

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ -x ∈ Iic a

Tactic:
simp only [mem_Iic, mem_Ioi, neg_le] at *

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hderiv : ∀ x ≤ a, HasDerivAt f (f' x) x
hx : -a < x
⊢ -a ≤ x

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hderiv : ∀ x ≤ a, HasDerivAt f (f' x) x
hx : -a < x
⊢ -a ≤ x

Tactic:
exact hx.le

Result:
no goals

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ Ioi (-a) ⊆ Neg.neg ⁻¹' Iic a

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
⊢ ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x

Tactic:
intro x hx

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ HasDerivAt g (-f' (-x)) x

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ Tendsto f atBot (𝓝 (limUnder atTop g))

Tactic:
have : Tendsto (fun x ↦ g (-x)) atBot (𝓝 (limUnder atTop g)) := L.comp tendsto_neg_atBot_atTop

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
this : Tendsto (fun x => g (-x)) atBot (𝓝 (limUnder atTop g))
⊢ Tendsto f atBot (𝓝 (limUnder atTop g))

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hx : x ∈ Ioi (-a)
this : -x ∈ Iic a
⊢ HasDerivAt g (-f' (-x)) x

Tactic:
simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)

Result:
no goals

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Tactic:
let g := f ∘ (fun x ↦ -x)

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ Tendsto g atTop (𝓝 (limUnder atTop g))

Tactic:
apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ IntegrableOn (fun x => -f' (-x)) (Ioi (-a)) volume

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
this : Tendsto (fun x => g (-x)) atBot (𝓝 (limUnder atTop g))
⊢ Tendsto f atBot (𝓝 (limUnder atTop g))

Tactic:
simpa [g] using this

Result:
no goals

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Tactic:
have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x := by
  intro x hx
  have : -x ∈ Iic a := by simp only [mem_Iic, mem_Ioi, neg_le] at *; exact hx.le
  simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
⊢ Tendsto f atBot (𝓝 (limUnder atBot f))

Tactic:
suffices ∃ a, Tendsto f atBot (𝓝 a) from tendsto_nhds_limUnder this

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ ∃ a, Tendsto f atBot (𝓝 a)

Tactic:
refine ⟨limUnder atTop g, ?_⟩

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ Tendsto f atBot (𝓝 (limUnder atTop g))

Proof state:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ HasDerivAt g (-f' (-x)) x

Tactic:
have : -x ∈ Iic a := by simp only [mem_Iic, mem_Ioi, neg_le] at *; exact hx.le

Result:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn f' (Iic a) volume
g : ℝ → E := f ∘ fun x => -x
x : ℝ
hx : x ∈ Ioi (-a)
this : -x ∈ Iic a
⊢ HasDerivAt g (-f' (-x)) x