awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d

Tactic:
H
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
h : dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d
h₁ :
  (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))

Tactic:
convert! H using 1
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d

Tactic:
simp [field, dist_comm a]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
h : dist b a * dist c d + dist b c * dist d a = dist b c * dist d a + dist b a * dist c d
⊢ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d

Tactic:
simp [field, dist_comm a]

Premises used: dist_comm
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist b a * dist c d + dist b c * dist d a = dist b c * dist d a + dist b a * dist c d

Tactic:
ring
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
α : Type u_3
x c : P
R : ℝ
l : Filter α
fc fx : α → P
fR : α → ℝ
hc : Tendsto fc l (𝓝 c)
hR : Tendsto fR l (𝓝 R)
hx : Tendsto fx l (𝓝 x)
hne : x ≠ c
⊢ Tendsto (fun (a : α) ↦ inversion (fc a) (fR a) (fx a)) l (𝓝 (inversion c R x))

Tactic:
(((hR.div (hx.dist hc) <| dist_ne_zero.2 hne).pow 2).smul (hx.vsub hc)).vadd hc

Premises used: Iff.mpr, dist_ne_zero, Filter.Tendsto.vsub, Filter.Tendsto.div, Filter.Tendsto.pow, Filter.Tendsto.dist, Filter.Tendsto.vadd, EuclideanGeometry.inversion, Filter.Tendsto.smul, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
X : Type u_3
inst_4 : TopologicalSpace X
c x : X → P
R : X → ℝ
a₀ : X
s : Set X
hc : ContinuousWithinAt c s a₀
hR : ContinuousWithinAt R s a₀
hx : ContinuousWithinAt x s a₀
hne : x a₀ ≠ c a₀
⊢ ContinuousWithinAt.{u_3, u_2} (Y := P) (fun (a : X) ↦ inversion (c a) (R a) (x a)) s a₀

Tactic:
hc.inversion hR hx hne

Premises used: ContinuousWithinAt, Filter.Tendsto.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
X : Type u_3
inst_4 : TopologicalSpace X
c x : X → P
R : X → ℝ
a₀ : X
hc : ContinuousAt c a₀
hR : ContinuousAt R a₀
hx : ContinuousAt x a₀
hne : x a₀ ≠ c a₀
⊢ ContinuousAt.{u_3, u_2} (Y := P) (fun (a : X) ↦ inversion (c a) (R a) (x a)) a₀

Tactic:
hc.inversion hR hx hne

Premises used: ContinuousAt, Filter.Tendsto.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
X : Type u_3
inst_4 : TopologicalSpace X
c x : X → P
R : X → ℝ
s : Set X
hc : ContinuousOn c s
hR : ContinuousOn R s
hx : ContinuousOn x s
hne : ∀ a ∈ s, x a ≠ c a
⊢ ContinuousOn.{u_3, u_2} (Y := P) (fun (a : X) ↦ inversion (c a) (R a) (x a)) s

Tactic:
fun a ha ↦
  (hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)

Premises used: ContinuousWithinAt.inversion, ContinuousOn
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
X : Type u_3
inst_4 : TopologicalSpace X
c x : X → P
R : X → ℝ
hc : Continuous[inst_4, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] c
hR : Continuous[inst_4, _] R
hx : Continuous[inst_4, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] x
hne : ∀ (a : X), x a ≠ c a
⊢ Continuous[inst_4, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (a : X) ↦ inversion (c a) (R a) (x a)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦
    hc.continuousAt.inversion hR.continuousAt hx.continuousAt (hne _)

Premises used: Iff.mpr, Continuous.continuousAt, continuous_iff_continuousAt, ContinuousAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
a : E
n : ℕ∞
hc : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) c s a
hR : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) R s a
hx : ContDiffWithinAt ℝ (↑n : WithTop ℕ∞) x s a
hne : x a ≠ c a
⊢ ContDiffWithinAt.{0, u_1, u_2} ℝ (F := F) (↑n : WithTop ℕ∞) (fun (a : E) ↦ inversion (c a) (R a) (x a)) s a

Tactic:
(((hR.div (hx.dist ℝ hc hne) (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc

Premises used: ContDiffWithinAt.sub, Iff.mpr, dist_ne_zero, Real, ContDiffWithinAt.add, ContDiffWithinAt.smul, ContDiffWithinAt.dist, EuclideanGeometry.inversion, ContDiffWithinAt.div, ContDiffWithinAt.pow
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
n : ℕ∞
hc : ContDiffOn ℝ (↑n : WithTop ℕ∞) c s
hR : ContDiffOn ℝ (↑n : WithTop ℕ∞) R s
hx : ContDiffOn ℝ (↑n : WithTop ℕ∞) x s
hne : ∀ a ∈ s, x a ≠ c a
⊢ ContDiffOn.{0, u_1, u_2} ℝ (F := F) (↑n : WithTop ℕ∞) (fun (a : E) ↦ inversion (c a) (R a) (x a)) s

Tactic:
fun a ha ↦
  (hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)

Premises used: ContDiffOn, ContDiffWithinAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
n : ℕ∞
hc : ContDiffAt ℝ (↑n : WithTop ℕ∞) c a
hR : ContDiffAt ℝ (↑n : WithTop ℕ∞) R a
hx : ContDiffAt ℝ (↑n : WithTop ℕ∞) x a
hne : x a ≠ c a
⊢ ContDiffAt.{0, u_1, u_2} ℝ (F := F) (↑n : WithTop ℕ∞) (fun (a : E) ↦ inversion (c a) (R a) (x a)) a

Tactic:
hc.inversion hR hx hne

Premises used: ContDiffAt, ContDiffWithinAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
n : ℕ∞
hc : ContDiff ℝ (↑n : ℕ∞ω) c
hR : ContDiff ℝ (↑n : ℕ∞ω) R
hx : ContDiff ℝ (↑n : ℕ∞ω) x
hne : ∀ (a : E), x a ≠ c a
⊢ ContDiff.{0, u_1, u_2} ℝ (F := F) (↑n : ℕ∞ω) fun (a : E) ↦ inversion (c a) (R a) (x a)

Tactic:
contDiff_iff_contDiffAt.2 fun a ↦ hc.contDiffAt.inversion hR.contDiffAt hx.contDiffAt (hne a)

Premises used: Iff.mpr, ContDiffAt.inversion, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
a : E
hc : DifferentiableWithinAt ℝ c s a
hR : DifferentiableWithinAt ℝ R s a
hx : DifferentiableWithinAt ℝ x s a
hne : x a ≠ c a
⊢ DifferentiableWithinAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) s a

Tactic:
(((hR.mul <| (hx.dist ℝ hc hne).inv (dist_ne_zero.2 hne)).pow _).smul (hx.sub hc)).add hc

Premises used: Iff.mpr, dist_ne_zero, Real, DifferentiableWithinAt.add, DifferentiableWithinAt.dist, DifferentiableWithinAt.mul, DivInvMonoid.div', DifferentiableWithinAt.sub, DifferentiableWithinAt.inv, DifferentiableWithinAt.pow, EuclideanGeometry.inversion, DifferentiableWithinAt.smul
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
s : Set E
hc : DifferentiableOn ℝ c s
hR : DifferentiableOn ℝ R s
hx : DifferentiableOn ℝ x s
hne : ∀ a ∈ s, x a ≠ c a
⊢ DifferentiableOn.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) s

Tactic:
fun a ha ↦
  (hc a ha).inversion (hR a ha) (hx a ha) (hne a ha)

Premises used: DifferentiableWithinAt.inversion, DifferentiableOn
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableAt ℝ c a
hR : DifferentiableAt ℝ R a
hx : DifferentiableAt ℝ x a
hne : x a ≠ c a
rw :
  ∀ (hc : DifferentiableWithinAt ℝ c univ a) (hR : DifferentiableWithinAt ℝ R univ a)
    (hx : DifferentiableWithinAt ℝ x univ a) (hne : x a ≠ c a),
    DifferentiableWithinAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) univ a
⊢ DifferentiableAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) a

Tactic:
rw [← differentiableWithinAt_univ] at *

Premises used: differentiableWithinAt_univ
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) univ a

Tactic:
hc.inversion hR hx hne

Premises used: DifferentiableWithinAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
a : E
hc : DifferentiableWithinAt ℝ c univ a
hR : DifferentiableWithinAt ℝ R univ a
hx : DifferentiableWithinAt ℝ x univ a
hne : x a ≠ c a
⊢ DifferentiableWithinAt.{0, u_1, u_2} ℝ (F := F) (fun (a : E) ↦ inversion (c a) (R a) (x a)) univ a

Tactic:
exact hc.inversion hR hx hne

Premises used: DifferentiableWithinAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ F
c x : E → F
R : E → ℝ
hc : Differentiable ℝ c
hR : Differentiable ℝ R
hx : Differentiable ℝ x
hne : ∀ (a : E), x a ≠ c a
⊢ Differentiable.{0, u_1, u_2} ℝ (F := F) fun (a : E) ↦ inversion (c a) (R a) (x a)

Tactic:
fun a ↦
  (hc a).inversion (hR a) (hx a) (hne a)

Premises used: Differentiable, DifferentiableAt.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c x : F
R : ℝ
hx : x ≠ c
rcases :
  ∀ (x : F) (hx : (fun (x : F) ↦ c + x) x ≠ c),
    HasFDerivAt (inversion c R)
      (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
        (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
      ((fun (x : F) ↦ c + x) x)
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist x c) 2)
      (↑(↑(Submodule.reflection (ℝ ∙ (x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
    x

Tactic:
rcases add_left_surjective c x with ⟨x, rfl⟩

Premises used: add_left_surjective, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
simp :
  HasFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)

Tactic:
simp +unfoldPartialApp only [inversion]

Premises used: EuclideanGeometry.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
simp_rw :
  HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ HasFDerivAt (fun (x : F) ↦ HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)

Tactic:
simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]

Premises used: dist_eq_norm, div_eq_mul_inv, div_pow
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
⊢ HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)

Tactic:
have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2 ≠ 0

Tactic:
simpa using hx
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ HasFDerivAt
    (fun (y : F) ↦
      HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) y)
    (HPow.hPow (β := ℕ) R 2 •
      -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
            (ContinuousLinearMap.id ℝ F)))
    (c + x)

Tactic:
have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
      (R ^ 2)
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
B :
  HasFDerivAt
    (fun (y : F) ↦
      HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) y)
    (HPow.hPow (β := ℕ) R 2 •
      -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
            (ContinuousLinearMap.id ℝ F)))
    (c + x)
⊢ HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)

Tactic:
(B.smul A).add_const c

Premises used: HasFDerivAt.add_const, HasFDerivAt.smul
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
A : HasFDerivAt (fun (x : F) ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
B :
  HasFDerivAt
    (fun (y : F) ↦
      HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) y)
    (HPow.hPow (β := ℕ) R 2 •
      -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
        HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
          (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ) ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c))
            (ContinuousLinearMap.id ℝ F)))
    (c + x)
⊢ HasFDerivAt (fun (x : F) ↦ (HPow.hPow (β := ℕ) R 2 * (HPow.hPow (β := ℕ) ‖x - c‖ 2)⁻¹) • (x -ᵥ c) +ᵥ c)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)

Tactic:
exact (B.smul A).add_const c

Premises used: HasFDerivAt.add_const, HasFDerivAt.smul
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)

Tactic:
have : HasFDerivAt (inversion c R) (?_ : F →L[ℝ] F) (c + x) := by
    simp +unfoldPartialApp only [inversion]
    simp_rw [dist_eq_norm, div_pow, div_eq_mul_inv]
    have A := (hasFDerivAt_id (𝕜 := ℝ) (c + x)).sub_const c
    have B := ((hasDerivAt_inv <| by simpa using hx).comp_hasFDerivAt _ A.norm_sq).const_mul
      (R ^ 2)
    exact (B.smul A).add_const c
-- Module: Mathlib.Geometry.Euclidean.Inversion.Calculus
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun (x : F) ↦ c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F)
        (HPow.hPow (β := ℕ) R 2 * ((fun (y : ℝ) ↦ y⁻¹) ∘ fun (x : F) ↦ HPow.hPow (β := ℕ) ‖_root_.id x - c‖ 2) (c + x))
        (ContinuousLinearMap.id ℝ F) +
      (HPow.hPow (β := ℕ) R 2 •
            -(HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ‖_root_.id (c + x) - c‖ 2) 2)⁻¹ •
              HSMul.hSMul (α := ℕ) (β := F →L[ℝ] ℝ) 2
                (ContinuousLinearMap.comp (σ₂₃ := RingHom.id ℝ)
                  ((innerSL ℝ : (a : F) → F →L[ℝ] ℝ) (_root_.id (c + x) - c)) (ContinuousLinearMap.id ℝ F))).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ HasFDerivAt (inversion c R)
    (HSMul.hSMul (β := F →L[ℝ] F) (HPow.hPow (β := ℕ) (R / dist ((fun (x : F) ↦ c + x) x) c) 2)
      (↑(↑(Submodule.reflection (ℝ ∙ ((fun (x : F) ↦ c + x) x - c))ᗮ) : F ≃L[ℝ] F) : F →L[ℝ] F))
    ((fun (x : F) ↦ c + x) x)

Tactic:
this.congr_fderiv (LinearMap.ext_on_codisjoint
    (Submodule.isCompl_orthogonal_of_hasOrthogonalProjection (K := ℝ ∙ x)).codisjoint
    (LinearMap.eqOn_span' ?_) fun y hy ↦ ?_)

Premises used: LinearMap.ext_on_codisjoint, HasFDerivAt.congr_fderiv, Submodule.isCompl_orthogonal_of_hasOrthogonalProjection, IsCompl.codisjoint