awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
h :
  ∀ (x_1 : E),
    Eq.{u_7 + 1} (α := 𝔸')
      ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
              (∑ i ∈ u.attach,
                (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
              (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
            (a : E) → 𝔸')
          x_1 :
        𝔸')
      ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (∑ i ∈ u.attach,
        (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
x_1 : E
⊢ Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (∑ i ∈ u.attach,
              (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')

Tactic:
simp [Finset.prod_erase_attach (g · x), ← u.sum_attach]

Premises used: Finset.sum_attach, Finset.prod_erase_attach
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x
⊢ HasFDerivAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸') (fun (x : E) ↦ ∏ i ∈ u, g i x)
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i) x

Tactic:
simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasFDerivAt_finsetProd.comp x <| hasFDerivAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Premises used: Finset.prod_attach
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
h :
  ∀ (x_1 : E),
    Eq.{u_7 + 1} (α := 𝔸')
      ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
              (∑ i ∈ u.attach,
                (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
              (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
            (a : E) → 𝔸')
          x_1 :
        𝔸')
      ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')
⊢ Eq (α := E →L[𝕜] 𝔸')
    (ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
      (∑ i ∈ u.attach,
        (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
      (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)))
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
x_1 : E
⊢ Eq.{u_7 + 1} (α := 𝔸')
    ((ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) (M₂ := (i : Subtype (Membership.mem u)) → 𝔸')
            (∑ i ∈ u.attach,
              (∏ j ∈ u.attach.erase i, g (↑j : ι) x) •> proj (φ := fun (a : Subtype (Membership.mem u)) ↦ 𝔸') i)
            (pi (φ := fun (i : Subtype (Membership.mem u)) ↦ 𝔸') fun (i : Subtype (Membership.mem u)) ↦ g' (↑i : ι)) :
          (a : E) → 𝔸')
        x_1 :
      𝔸')
    ((∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i : (a : E) → 𝔸') x_1 : 𝔸')

Tactic:
simp [Finset.prod_erase_attach (g · x), ← u.sum_attach]

Premises used: Finset.sum_attach, Finset.prod_erase_attach
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_7} (𝕜 := 𝕜) (F := 𝔸') (fun (x : E) ↦ ∏ i ∈ u, g i x)
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> g' i) s x

Tactic:
simpa [← Finset.prod_attach u] using .congr_fderiv
    (hasFDerivAt_finsetProd.comp_hasFDerivWithinAt x <|
      hasFDerivWithinAt_pi.mpr fun i ↦ hg (Subtype.val i) i.prop :)
    (by ext; simp [Finset.prod_erase_attach (g · x), ← u.sum_attach])

Premises used: Finset.prod_attach
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
inst_5 : DecidableEq ι
x : E
hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x
⊢ Eq (α := E →L[𝕜] 𝔸') (fderiv 𝕜 (fun (x : E) ↦ ∏ i ∈ u, g i x) x)
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> fderiv 𝕜 (g i) x)

Tactic:
(HasFDerivAt.finsetProd fun i hi ↦ (hg i hi).hasFDerivAt).fderiv

Premises used: HasFDerivAt.finsetProd, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
ι : Type u_5
𝔸' : Type u_7
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
inst_5 : DecidableEq ι
x : E
hxs : UniqueDiffWithinAt 𝕜 s x
hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x
⊢ Eq (α := E →L[𝕜] 𝔸') (fderivWithin 𝕜 (fun (x : E) ↦ ∏ i ∈ u, g i x) s x)
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) •> fderivWithin 𝕜 (g i) s x)

Tactic:
(HasFDerivWithinAt.finsetProd fun i hi ↦ (hg i hi).hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.finsetProd, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
⊢ IsLittleO (E := R) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * t * (↑x⁻¹ : R)) id

Tactic:
have : (fun t : R => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] id :=
    (inverse_add_norm_diff_second_order x).trans_isLittleO (isLittleO_norm_pow_id one_lt_two)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
this : IsLittleO (E := R) (𝓝 0) (fun (t : R) ↦ ((↑x : R) + t)⁻¹ʳ - (↑x⁻¹ : R) + (↑x⁻¹ : R) * t * (↑x⁻¹ : R)) id
⊢ HasFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Ring.inverse
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
        (↑x⁻¹ : R))
    (↑x : R)

Tactic:
simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this

Premises used: hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : R
hx : IsUnit x
⊢ DifferentiableAt 𝕜 Ring.inverse x

Tactic:
let ⟨u, hu⟩ := hx; hu ▸ (hasFDerivAt_ringInverse u).differentiableAt

Premises used: DifferentiableAt, hasFDerivAt_ringInverse, _private.0.differentiableAt_inverse.match_1, Eq.rec, Ring.inverse, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : R
hx : IsUnit x
s : Set R
⊢ DifferentiableWithinAt 𝕜 Ring.inverse s x

Tactic:
(differentiableAt_inverse hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
⊢ DifferentiableOn.{u_1, u_5, u_5} 𝕜 (E := R) Ring.inverse {x : R | IsUnit x}

Tactic:
fun _x hx => differentiableWithinAt_inverse hx _

Premises used: setOf, IsUnit, DifferentiableOn, differentiableWithinAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
⊢ Eq (α := R →L[𝕜] R) (fderiv 𝕜 Ring.inverse (↑x : R))
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
        (↑x⁻¹ : R))

Tactic:
(hasFDerivAt_ringInverse x).fderiv

Premises used: hasFDerivAt_ringInverse, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
⊢ HasStrictFDerivAt Ring.inverse (fderiv 𝕜 Ring.inverse (↑x : R)) (↑x : R)

Tactic:
(analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt

Premises used: AnalyticAt.hasStrictFDerivAt, analyticAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
h :
  Eq.{u_5 + 1} (α := AddCommGroup R) toAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) (β := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) →
      Eq (α := R →L[𝕜] R)
        (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
              (↑x⁻¹ : R) :
          R →L[𝕜] R)
        (fderiv 𝕜 Ring.inverse (↑x : R) : R →L[𝕜] R)
⊢ HasStrictFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Ring.inverse
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
        (↑x⁻¹ : R))
    (↑x : R)

Tactic:
convert! (analyticAt_inverse (𝕜 := 𝕜) x).hasStrictFDerivAt

Premises used: AnalyticAt.hasStrictFDerivAt, analyticAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
e_4 : Eq.{u_5 + 1} (α := AddCommGroup R) toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) (β := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R)
⊢ Eq (α := R →L[𝕜] R)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
          (↑x⁻¹ : R) :
      R →L[𝕜] R)
    (fderiv 𝕜 Ring.inverse (↑x : R) : R →L[𝕜] R)

Tactic:
(fderiv_inverse x).symm

Premises used: fderiv_inverse, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedRing R
inst_2 : HasSummableGeomSeries R
inst_3 : NormedAlgebra 𝕜 R
x : Rˣ
e_4 : Eq.{u_5 + 1} (α := AddCommGroup R) toAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R) (β := Module 𝕜 R) (NormedSpace.toModule : Module 𝕜 R)
⊢ Eq (α := R →L[𝕜] R)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) (↑x⁻¹ : R) : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R)
          (↑x⁻¹ : R) :
      R →L[𝕜] R)
    (fderiv 𝕜 Ring.inverse (↑x : R) : R →L[𝕜] R)

Tactic:
exact (fderiv_inverse x).symm

Premises used: fderiv_inverse, Eq.symm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedRing R
inst_4 : HasSummableGeomSeries R
inst_5 : NormedAlgebra 𝕜 R
h : E → R
z : E
S : Set E
hf : DifferentiableWithinAt 𝕜 h S z
hz : IsUnit (h z)
⊢ DifferentiableWithinAt.{u_1, u_2, u_5} 𝕜 (F := R) (fun (x : E) ↦ (h x)⁻¹ʳ) S z

Tactic:
(differentiableAt_inverse hz).comp_differentiableWithinAt z hf

Premises used: Ring.inverse, dite, DifferentiableAt.comp_differentiableWithinAt, differentiableAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedRing R
inst_4 : HasSummableGeomSeries R
inst_5 : NormedAlgebra 𝕜 R
h : E → R
z : E
hf : DifferentiableAt 𝕜 h z
hz : IsUnit (h z)
⊢ DifferentiableAt.{u_1, u_2, u_5} 𝕜 (F := R) (fun (x : E) ↦ (h x)⁻¹ʳ) z

Tactic:
(differentiableAt_inverse hz).comp z hf

Premises used: Ring.inverse, dite, DifferentiableAt.comp, differentiableAt_inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedRing R
inst_4 : HasSummableGeomSeries R
inst_5 : NormedAlgebra 𝕜 R
h : E → R
S : Set E
hf : DifferentiableOn 𝕜 h S
hz : ∀ x ∈ S, IsUnit (h x)
⊢ DifferentiableOn.{u_1, u_2, u_5} 𝕜 (F := R) (fun (x : E) ↦ (h x)⁻¹ʳ) S

Tactic:
fun x h => (hf x h).inverse (hz x h)

Premises used: DifferentiableWithinAt.inverse, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedRing R
inst_4 : HasSummableGeomSeries R
inst_5 : NormedAlgebra 𝕜 R
h : E → R
hf : Differentiable 𝕜 h
hz : ∀ (x : E), IsUnit (h x)
⊢ Differentiable.{u_1, u_2, u_5} 𝕜 (F := R) fun (x : E) ↦ (h x)⁻¹ʳ

Tactic:
fun x => (hf x).inverse (hz x)

Premises used: Differentiable, DifferentiableAt.inverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ HasStrictFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Inv.inv
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹) x

Tactic:
simpa using hasStrictFDerivAt_ringInverse (Units.mk0 _ hx)

Premises used: Units.mk0, hasStrictFDerivAt_ringInverse
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ HasFDerivAt.{u_1, u_5, u_5} (𝕜 := 𝕜) Inv.inv
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹) x

Tactic:
simpa using hasFDerivAt_ringInverse (Units.mk0 _ hx)

Premises used: hasFDerivAt_ringInverse, Units.mk0
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ DifferentiableAt 𝕜 Inv.inv x

Tactic:
(hasFDerivAt_inv' hx).differentiableAt

Premises used: HasFDerivAt.differentiableAt, hasFDerivAt_inv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
s : Set R
⊢ DifferentiableWithinAt 𝕜 (F := R) (fun (x : R) ↦ x⁻¹) s x

Tactic:
(differentiableAt_inv hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
⊢ DifferentiableOn 𝕜 (F := R) (fun (x : R) ↦ x⁻¹) {x : R | x ≠ 0}

Tactic:
fun _x hx =>
  differentiableWithinAt_inv hx _

Premises used: differentiableWithinAt_inv, setOf, Ne, DifferentiableOn, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
x : R
hx : x ≠ 0
⊢ Eq (α := R →L[𝕜] R) (fderiv 𝕜 Inv.inv x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)

Tactic:
(hasFDerivAt_inv' hx).fderiv

Premises used: HasFDerivAt.fderiv, hasFDerivAt_inv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
rw :
  Eq (α := R →L[𝕜] R) (fderiv 𝕜 Inv.inv x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)
⊢ Eq (α := R →L[𝕜] R) (fderivWithin 𝕜 (fun (x : R) ↦ x⁻¹) s x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)

Tactic:
rw [DifferentiableAt.fderivWithin (differentiableAt_inv hx) hxs]

Premises used: DifferentiableAt.fderivWithin, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := R →L[𝕜] R) (fderiv 𝕜 Inv.inv x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)

Tactic:
fderiv_inv' hx

Premises used: fderiv_inv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
R : Type u_5
inst_1 : NormedDivisionRing R
inst_2 : NormedAlgebra 𝕜 R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := R →L[𝕜] R) (fderiv 𝕜 Inv.inv x)
    (-(((mulLeftRight 𝕜 R : (a : R) → R →L[𝕜] R →L[𝕜] R) x⁻¹ : R →L[𝕜] R →L[𝕜] R) : (a : R) → R →L[𝕜] R) x⁻¹)

Tactic:
exact fderiv_inv' hx

Premises used: fderiv_inv'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
h : E → R
z : E
S : Set E
hf : DifferentiableWithinAt 𝕜 h S z
hz : h z ≠ 0
⊢ DifferentiableWithinAt 𝕜 h⁻¹ S z

Tactic:
(differentiableAt_inv hz).comp_differentiableWithinAt z hf

Premises used: DifferentiableAt.comp_differentiableWithinAt, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
h : E → R
z : E
hf : DifferentiableAt 𝕜 h z
hz : h z ≠ 0
⊢ DifferentiableAt 𝕜 h⁻¹ z

Tactic:
(differentiableAt_inv hz).comp z hf

Premises used: DifferentiableAt.comp, differentiableAt_inv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
h : E → R
S : Set E
hf : DifferentiableOn 𝕜 h S
hz : ∀ x ∈ S, h x ≠ 0
⊢ DifferentiableOn 𝕜 h⁻¹ S

Tactic:
fun x h => (hf x h).inv (hz x h)

Premises used: DifferentiableWithinAt.inv, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
R : Type u_5
inst_3 : NormedDivisionRing R
inst_4 : NormedAlgebra 𝕜 R
h : E → R
hf : Differentiable 𝕜 h
hz : ∀ (x : E), h x ≠ 0
⊢ Differentiable 𝕜 h⁻¹

Tactic:
fun x => (hf x).inv (hz x)

Premises used: Differentiable, DifferentiableAt.inv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
obtain : ∀ (x : E) (hx : 0 < ‖x‖), ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0

Tactic:
obtain ⟨x, hx⟩ := NormedSpace.exists_lt_norm ℝ E 0

Premises used: Real, OfNat.ofNat, NormedSpace.exists_lt_norm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
⊢ DifferentiableAt ℝ Norm.norm (HSMul.hSMul (α := ℝ) 0 x)

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
⊢ DifferentiableAt.{0, 0, u_1} ℝ (F := E) (fun (t : ℝ) ↦ t • x) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0

Tactic:
have : DifferentiableAt ℝ (fun t : ℝ ↦ ‖t • x‖) 0 := DifferentiableAt.comp _ (by simpa) (by simp)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ ‖t • x‖) 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0

Tactic:
simp_rw [norm_smul, norm_eq_abs] at this

Premises used: norm_smul, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
⊢ Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)

Tactic:
field_simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Norm
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : Nontrivial E
x : E
hx : 0 < ‖x‖
h : DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ ‖x‖) 0
this : DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ |t| * ‖x‖) 0
⊢ Eq (α := (a : ℝ) → ℝ) abs fun (t : ℝ) ↦ 1 / ‖x‖ * (|t| * ‖x‖)

Tactic:
have aux : abs = fun t ↦ (1 / ‖x‖) * (|t| * ‖x‖) := by field_simp