awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
t : Set F
hl : DifferentiableWithinAt 𝕜 l t (f x)
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
l : F → E
y : F
t : Set F
hl : DifferentiableWithinAt 𝕜 l t y
hf : DifferentiableWithinAt 𝕜 f s x
hs : MapsTo f s t
hy : y = f x
⊢ derivWithin (l ∘ f) s x = (fderivWithin 𝕜 l t (f x) : (a : F) → E) (derivWithin f s x)
have hl₁ : DifferentiableWithinAt 𝕜 l t (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hs, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Comp (hypothesis)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
f : 𝕜 → F
x : 𝕜
l : F → E
y : F
hl : DifferentiableAt 𝕜 l y
hf : DifferentiableAt 𝕜 f x
hy : y = f x
⊢ deriv (l ∘ f) x = (fderiv 𝕜 l (f x) : (a : F) → E) (deriv f x)
have hl₁ : DifferentiableAt 𝕜 l (f x)
Tactic: rw [hy] at hl
Cleared hypotheses: hl, hf, hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (c * x)) s x = c • derivWithin f (c • s) (c * x)
have simp : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
Tactic: simp only [← smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
have rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
Tactic: rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
have rw₁ : ((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 =
  derivWithin (c • f) (c • s) (c • x)
Tactic: rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
rw₁ :
  ((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 =
    derivWithin (c • f) (c • s) (c • x)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
have rw₂ : Eq.{u_2 + 1} (α := E)
  (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
  (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
Tactic: rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
rw₁ :
  ((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 =
    derivWithin (c • f) (c • s) (c • x)
rw₂ :
  Eq.{u_2 + 1} (α := E)
    (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
have rw₃ : Eq.{u_2 + 1} (α := E) (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
  (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
Tactic: rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.CompMul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
f : 𝕜 → E
s : Set 𝕜
x : 𝕜
rw : derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = derivWithin (c • f) (c • s) (c • x)
rw₁ :
  ((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 =
    derivWithin (c • f) (c • s) (c • x)
rw₂ :
  Eq.{u_2 + 1} (α := E)
    (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (x : 𝕜) ↦ f (c • x)) s x : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
rw₃ :
  Eq.{u_2 + 1} (α := E) (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
    (((fderivWithin 𝕜 (c • f) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
⊢ derivWithin (fun (x : 𝕜) ↦ f (c • x)) s x = c • derivWithin f (c • s) (c • x)
have rw₄ : Eq.{u_2 + 1} (α := E) (((fderivWithin 𝕜 (fun (i : 𝕜) ↦ c • f i) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
  (((fderivWithin.{u_1, u_1, u_2} 𝕜 (F := E) (fun (i : 𝕜) ↦ c • f i) (c • s) (c • x) : 𝕜 →L[𝕜] E) : (a : 𝕜) → E) 1 : E)
Tactic: rw [← derivWithin_const_smul_field, derivWithin, derivWithin,
    fderivWithin_comp_smul_eq_fderivWithin_smul, Pi.smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
⊢ HasStrictDerivAt Inv.inv (-(HPow.hPow (β := ℕ) x 2)⁻¹) x
have refine : (𝓝 (x, x)).EventuallyEq (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
  HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹) ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜)
Tactic: refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
⊢ (𝓝 (x, x)).EventuallyEq (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹) ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜)
have refine : ∀ (x_1 : 𝕜 × 𝕜),
  SProd.sprod (α := Set 𝕜) (β := Set 𝕜) {y : 𝕜 | y ≠ 0} {y : 𝕜 | y ≠ 0} x_1 →
    Eq.{u + 1} (α := 𝕜) ((fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) x_1)
      ((fun (p : 𝕜 × 𝕜) ↦
          HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹)
            ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜))
        x_1)
Tactic: refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
this :
  IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
y z : 𝕜
hy : y ≠ 0
hz : z ≠ 0
⊢ Eq.{u + 1} (α := 𝕜) ((fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) (y, z))
    ((fun (p : 𝕜 × 𝕜) ↦
        HSub.hSub (β := 𝕜) (p.1⁻¹ - p.2⁻¹)
          ((toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : (a : 𝕜) → 𝕜) (p.1 - p.2) : 𝕜))
      (y, z))
have simp : (y - z) * (y * z - HPow.hPow (β := ℕ) x 2) = HPow.hPow (β := ℕ) x 2 * (z - y) + y * z * (y - z)
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ HasStrictDerivAt Inv.inv (-(HPow.hPow (β := ℕ) x 2)⁻¹) x
have p : IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
  (p.1 - p.2) * 1
Tactic: suffices
    (fun p : 𝕜 × 𝕜 => (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) =o[𝓝 (x, x)] fun p =>
      (p.1 - p.2) * 1 by
    refine .of_isLittleO <| this.congr' ?_ (Eventually.of_forall fun _ => mul_one _)
    refine Eventually.mono ((isOpen_ne.prod isOpen_ne).mem_nhds ⟨hx, hx⟩) ?_
    rintro ⟨y, z⟩ ⟨hy, hz⟩
    simp only [mem_setOf_eq] at hy hz
    simp [field]
    ring
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ IsLittleO (E := 𝕜) (F := 𝕜) (𝓝 (x, x)) (fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) * ((x * x)⁻¹ - (p.1 * p.2)⁻¹)) fun (p : 𝕜 × 𝕜) ↦
    (p.1 - p.2) * 1
have refine : Tendsto (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)
Tactic: refine (isBigO_refl (fun p : 𝕜 × 𝕜 => p.1 - p.2) _).mul_isLittleO ((isLittleO_one_iff 𝕜).2 ?_)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
hx : x ≠ 0
⊢ Tendsto (β := 𝕜) (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 0)
have rw : Tendsto (fun (p : 𝕜 × 𝕜) ↦ (x * x)⁻¹ - (p.1 * p.2)⁻¹) (𝓝 (x, x)) (𝓝 ((x * x)⁻¹ - (x * x)⁻¹))
Tactic: rw [← sub_self (x * x)⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹
have inl : deriv (fun (x : 𝕜) ↦ x⁻¹) 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
Tactic: rcases eq_or_ne x 0 with (rfl | hne)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
inl : deriv (fun (x : 𝕜) ↦ x⁻¹) 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹
have inr : ∀ (hne : x ≠ 0), deriv (fun (x : 𝕜) ↦ x⁻¹) x = -(HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rcases eq_or_ne x 0 with (rfl | hne)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
⊢ deriv (fun (x : 𝕜) ↦ x⁻¹) 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
have inl : 0 = -(HPow.hPow (α := 𝕜) (β := ℕ) 0 2)⁻¹
Tactic: rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (x : 𝕜) ↦ x⁻¹) s x = -(HPow.hPow (β := ℕ) x 2)⁻¹
have rw : deriv Inv.inv x = -(HPow.hPow (β := ℕ) x 2)⁻¹
Tactic: rw [DifferentiableAt.derivWithin (differentiableAt_inv x_ne_zero) hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) x : 𝕜 →L[𝕜] 𝕜)
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : 𝕜 →L[𝕜] 𝕜)
have rw : Eq (α := 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (deriv (fun (x : 𝕜) ↦ x⁻¹) x)) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
Tactic: rw [← toSpanSingleton_deriv, deriv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
rw :
  Eq (α := 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (deriv (fun (x : 𝕜) ↦ x⁻¹) x))
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) x : 𝕜 →L[𝕜] 𝕜)
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : 𝕜 →L[𝕜] 𝕜)
have rw₁ : Eq (α := 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹)) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
Tactic: rw [← toSpanSingleton_deriv, deriv_inv]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
x_ne_zero : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderivWithin 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ x⁻¹) s x : 𝕜 →L[𝕜] 𝕜)
    (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹) : 𝕜 →L[𝕜] 𝕜)
have rw : Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 Inv.inv x : 𝕜 →L[𝕜] 𝕜) (toSpanSingleton 𝕜 (-(HPow.hPow (β := ℕ) x 2)⁻¹))
Tactic: rw [DifferentiableAt.fderivWithin (differentiableAt_inv x_ne_zero) hxs]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivWithinAt c c' s x
hx : c x ≠ 0
⊢ HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) s x
have h : -c' / HPow.hPow (β := ℕ) (c x) 2 = -(HPow.hPow (β := ℕ) (c x) 2)⁻¹ * c'
Tactic: convert! (hasDerivAt_inv hx).comp_hasDerivWithinAt x hc using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
hc : HasDerivAt c c' x
hx : c x ≠ 0
⊢ HasDerivAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (hx : c x ≠ 0), HasDerivWithinAt c⁻¹ (-c' / HPow.hPow (β := ℕ) (c x) 2) univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
c : 𝕜 → 𝕜
hc : DifferentiableWithinAt 𝕜 c s x
hx : c x ≠ 0
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
⊢ derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (x : 𝕜) ↦ (c x)⁻¹) s x = -derivWithin c s x / HPow.hPow (β := ℕ) (c x) 2
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) s x
have h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) i
Tactic: convert! hc.fun_mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) i
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) s x
have h₁ : (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
  c' * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
Tactic: convert! hc.fun_mul ((hasDerivAt_inv hx).comp_hasDerivWithinAt x hd) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * ((fun (y : 𝕜') ↦ y⁻¹) ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
have h : c' * d x - c x * d' = c' * d x + -(c x * d')
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x
have h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * (Inv.inv ∘ d) i
Tactic: convert! hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
h : Eq (α := 𝕜 → 𝕜') (fun (y : 𝕜) ↦ c y / d y) fun (i : 𝕜) ↦ c i * (Inv.inv ∘ d) i
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x
have h₁ : (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 = c' * (Inv.inv ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
Tactic: convert! hc.fun_mul ((hasStrictDerivAt_inv hx).comp x hd) using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
hx : d x ≠ 0
⊢ (c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2 =
    c' * (Inv.inv ∘ d) x + c x * (-(HPow.hPow (β := ℕ) (d x) 2)⁻¹ * d')
have h : c' * d x - c x * d' = c' * d x + -(c x * d')
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
c' d' : 𝕜'
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
hx : d x ≠ 0
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) x
have rw : ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x) (hx : d x ≠ 0),
  HasDerivWithinAt (fun (y : 𝕜) ↦ c y / d y) ((c' * d x - c x * d') / HPow.hPow (β := ℕ) (d x) 2) univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hc, hd, hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
have pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inv (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst_1 : NontriviallyNormedField 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c d : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hx : d x ≠ 0
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
      (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
have neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
  derivWithin (fun (x : 𝕜) ↦ c x / d x) s x =
    (derivWithin c s x * d x - c x * derivWithin d s x) / HPow.hPow (β := ℕ) (d x) 2
Tactic: by_cases hsx : UniqueDiffWithinAt 𝕜 s x
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f g h : 𝕜 → 𝕜
f' h' a : 𝕜
hst : ContinuousAt g a
hf : HasDerivAt f f' (g a)
hh : HasDerivAt h h' a
hf' : f' ≠ 0
hcomp : f ∘ g =ᶠ[𝓝 a] h
⊢ HasDerivAt g (h' / f') a
have h₁ : h' / f' = (ContinuousLinearMap.toSpanSingleton 𝕜 f'⁻¹ ∘SL ContinuousLinearMap.toSpanSingleton 𝕜 h' : (a : 𝕜) → 𝕜) 1
Tactic: convert hf.hasFDerivAt.of_comp_of_leftInverse hst hh hcomp (f'symm := .toSpanSingleton 𝕜 f'⁻¹)
    (fun _ ↦ by simp [hf']) |>.hasDerivAt using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)
have simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
Tactic: simp [dist_eq_norm_sub, ← sub_smul, norm_smul]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
have field_simp : ‖x_1 - x_2‖ ≤ ‖x_1 - x_2‖
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.Deriv.Inverse (goal)
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
s : Set 𝕜
x : 𝕜
c : F
h : HasDerivWithinAt f f' s x
hf' : f' ≠ 0
x_1 x_2 : 𝕜
⊢ dist x_1 x_2 ≤
    (↑‖f'‖₊⁻¹ : ℝ) *
      dist.{v} (α := F) ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_1 : F)
        ((ContinuousLinearMap.toSpanSingleton 𝕜 f' : (a : 𝕜) → F) x_2 : F)
have simp : ‖x_1 - x_2‖ ≤ ‖f'‖⁻¹ * (‖x_1 - x_2‖ * ‖f'‖)
Tactic: simp [dist_eq_norm_sub, ← sub_smul, norm_smul]