-- Mathlib/Analysis/Calculus/FDeriv/Extend.lean
theorem hasDerivAt_of_hasDerivAt_of_ne {f g : ℝ → E} {x : ℝ}
    (f_diff : ∀ y ≠ x, HasDerivAt f (g y) y) (hf : ContinuousAt f x)
    (hg : ContinuousAt g x) : HasDerivAt f (g x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto (fun x => deriv f x) (𝓝[<] x) (𝓝 (g x))

Tactic:
have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
⊢ Tendsto (fun x => deriv f x) (𝓝[<] x) (𝓝 (g x))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
⊢ ∀ y ∈ Iio x, y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}

Tactic:
intros y hy

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivAt f (g x) x

Tactic:
have B : HasDerivWithinAt f (g x) (Iic x) x := by
  have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
    (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt
  apply
    hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
      self_mem_nhdsWithin
  have : Tendsto g (𝓝[<] x) (𝓝 (g x)) := tendsto_inf_left hg
  apply this.congr' _
  apply mem_of_superset self_mem_nhdsWithin fun y hy => _
  intros y hy
  exact (f_diff y (ne_of_lt hy)).deriv.symm

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
B : HasDerivWithinAt f (g x) (Iic x) x
⊢ HasDerivAt f (g x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
⊢ HasDerivWithinAt f (g x) (Iic x) x

Tactic:
have diff : DifferentiableOn ℝ f (Iio x) := fun y hy =>
  (f_diff y (ne_of_lt hy)).differentiableAt.differentiableWithinAt

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ HasDerivWithinAt f (g x) (Iic x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ HasDerivWithinAt f (g x) (Iic x) x

Tactic:
apply
  hasDerivWithinAt_Iic_of_tendsto_deriv diff hf.continuousWithinAt
    self_mem_nhdsWithin

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
⊢ Tendsto (fun x => deriv f x) (𝓝[<] x) (𝓝 (g x))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ HasDerivWithinAt f (g x) (Ici x) x

Tactic:
have diff : DifferentiableOn ℝ f (Ioi x) := fun y hy =>
  (f_diff y (ne_of_gt hy)).differentiableAt.differentiableWithinAt

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ HasDerivWithinAt f (g x) (Ici x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[>] x] fun x => deriv f x

Tactic:
apply mem_of_superset self_mem_nhdsWithin fun y hy => _

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ ∀ y ∈ Ioi x, y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Ioi x
⊢ y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}

Tactic:
exact (f_diff y (ne_of_gt hy)).deriv.symm

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ HasDerivWithinAt f (g x) (Ici x) x

Tactic:
apply
  hasDerivWithinAt_Ici_of_tendsto_deriv diff hf.continuousWithinAt
    self_mem_nhdsWithin

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
⊢ Tendsto (fun x => deriv f x) (𝓝[>] x) (𝓝 (g x))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
A : HasDerivWithinAt f (g x) (Ici x) x
diff : DifferentiableOn ℝ f (Iio x)
this : Tendsto g (𝓝[<] x) (𝓝 (g x))
y : ℝ
hy : y ∈ Iio x
⊢ y ∈ {x | (fun x => g x = (fun x => deriv f x) x) x}

Tactic:
exact (f_diff y (ne_of_lt hy)).deriv.symm

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ Tendsto (fun x => deriv f x) (𝓝[>] x) (𝓝 (g x))

Tactic:
apply this.congr' _

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
x : ℝ
f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y
hf : ContinuousAt f x
hg : ContinuousAt g x
diff : DifferentiableOn ℝ f (Ioi x)
this : Tendsto g (𝓝[>] x) (𝓝 (g x))
⊢ g =ᶠ[𝓝[>] x] fun x => deriv f x