awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
x : E
G : Type u_4
inst_3 : GroupWithZero G
inst_4 : DistribMulAction G E
inst_5 : ContinuousConstSMul G E
inst_6 : SMulCommClass G 𝕜 E
c : G
hc : c ≠ 0
h : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ UniqueDiffWithinAt 𝕜 s x

Tactic:
simpa [hc] using h.smul (inv_ne_zero hc)

Premises used: UniqueDiffWithinAt.smul, inv_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
inl :
  HasFDerivWithinAt (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) (HSMul.hSMul (α := 𝕜) 0 f') s x ↔
    HasFDerivWithinAt f f' (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)
inr : ∀ (hc : c ≠ 0), HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) (HSMul.hSMul (α := 𝕜) 0 f') s x ↔
    HasFDerivWithinAt f f' (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)

Tactic:
simp [hasFDerivWithinAt_const, HasFDerivWithinAt.of_subsingleton (subsingleton_zero_smul_set _)]

Premises used: hasFDerivWithinAt_const, HasFDerivWithinAt.of_subsingleton, Set.subsingleton_zero_smul_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
⊢ IsUnit c

Tactic:
IsUnit.mk0 c hc

Premises used: IsUnit.mk0
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
inr :
  ∀ (c : 𝕜ˣ) (hc : (↑c : 𝕜) ≠ 0),
    HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
      HasFDerivWithinAt f f' ((↑c : 𝕜) • s) ((↑c : 𝕜) • x)
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) (c • f') s x ↔ HasFDerivWithinAt f f' (c • s) (c • x)

Tactic:
lift c to 𝕜ˣ using IsUnit.mk0 c hc

Premises used: IsUnit.mk0
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
h :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F)
      ((f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) : (a : E) → F) x : F)
      ((c • f' : (a : E) → F) x : F)
⊢ f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
x_1 : E
⊢ Eq.{u_3 + 1} (α := F)
    ((f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) : (a : E) → F) x_1 : F)
    ((c • f' : (a : E) → F) x_1 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
⊢ f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'

Tactic:
have A : f'.comp ((ContinuousLinearEquiv.smulLeft c : E ≃L[𝕜] E) : E →L[𝕜] E) = c • f' := by
      ext; simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
A : f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'
inr :
  HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt (f ∘ (⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E))
      (c • f')
      ((⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E) ⁻¹' ((↑c : 𝕜) • s)) x
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt f f' ((↑c : 𝕜) • s) ((↑c : 𝕜) • x)

Tactic:
rw [← Units.smul_def c x, ← ContinuousLinearEquiv.smulLeft_apply_apply (R₁ := 𝕜),
      ← ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, A]

Premises used: ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff, ContinuousLinearEquiv.smulLeft_apply_apply, Units.smul_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
A : f' ∘SL (↑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c) : E →L[𝕜] E) = c • f'
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x ↔
    HasFDerivWithinAt (f ∘ (⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E))
      (c • f')
      ((⇑((ContinuousLinearEquiv.smulLeft : (a : 𝕜ˣ) → E ≃L[𝕜] E) c : E ≃L[𝕜] E) : (a : E) → E) ⁻¹' ((↑c : 𝕜) • s)) x

Tactic:
simp [Function.comp_def, ← Units.smul_def, ← preimage_smul_inv, preimage_preimage]

Premises used: Set.preimage_preimage, Set.preimage_smul_inv, Function.comp_def, Units.smul_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
simp : HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (fun (x : E) ↦ c • f (c • x)) (c • f') s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (c • f) f' (c • s) (c • x)

Tactic:
simp only [← hasFDerivWithinAt_comp_smul_smul_iff, Pi.smul_apply]

Premises used: hasFDerivWithinAt_comp_smul_smul_iff, Pi.smul_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜
hc : c ≠ 0
lift :
  ∀ (c : 𝕜ˣ) (hc : (↑c : 𝕜) ≠ 0),
    HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) f' s x ↔
      HasFDerivWithinAt (fun (x : E) ↦ (↑c : 𝕜) • f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (c • x)) f' s x ↔ HasFDerivWithinAt (fun (x : E) ↦ c • f (c • x)) (c • f') s x

Tactic:
lift c to 𝕜ˣ using IsUnit.mk0 c hc

Premises used: IsUnit.mk0
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) f' s x ↔
    HasFDerivWithinAt (fun (x : E) ↦ (↑c : 𝕜) • f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x

Tactic:
(ContinuousLinearEquiv.smulLeft c).comp_hasFDerivWithinAt_iff.symm

Premises used: ContinuousLinearMap.comp, ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, DFunLike.coe, Iff.symm, ContinuousLinearEquiv.smulLeft
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
f' : E →L[𝕜] F
x : E
c : 𝕜ˣ
hc : (↑c : 𝕜) ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ f ((↑c : 𝕜) • x)) f' s x ↔
    HasFDerivWithinAt (fun (x : E) ↦ (↑c : 𝕜) • f ((↑c : 𝕜) • x)) ((↑c : 𝕜) • f') s x

Tactic:
exact (ContinuousLinearEquiv.smulLeft c).comp_hasFDerivWithinAt_iff.symm

Premises used: ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff, DFunLike.coe, Iff.symm, ContinuousLinearEquiv.smulLeft
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
inl :
  Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) 0 f) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
inr :
  ∀ (hc : c ≠ 0),
    Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) 0 f) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hc : c ≠ 0
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))

Tactic:
simp only [fderivWithin, DifferentiableWithinAt, hasFDerivWithinAt_comp_smul_iff_smul hc]

Premises used: hasFDerivWithinAt_comp_smul_iff_smul, fderivWithin, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hc : c ≠ 0
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x) (fderivWithin 𝕜 (c • f) (c • s) (c • x))

Tactic:
classical
    simp only [fderivWithin, DifferentiableWithinAt, hasFDerivWithinAt_comp_smul_iff_smul hc]

Premises used: hasFDerivWithinAt_comp_smul_iff_smul, fderivWithin, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
inl :
  fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
inr :
  ∀ (hc : c ≠ 0),
    fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) s x =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s) (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
inr : UniqueDiffWithinAt 𝕜 (c • s) (c • x)
⊢ fderivWithin 𝕜 (fun (x : E) ↦ f (c • x)) s x = HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (c • s) (c • x))

Tactic:
rw [fderivWithin_comp_smul_eq_fderivWithin_smul, fderivWithin_const_smul_field]

Premises used: fderivWithin_comp_smul_eq_fderivWithin_smul, fderivWithin_const_smul_field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
⊢ UniqueDiffWithinAt 𝕜 (c • s) (c • x)

Tactic:
hs.smul hc

Premises used: UniqueDiffWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
c : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
hc : c ≠ 0
⊢ UniqueDiffWithinAt 𝕜 (c • s) (c • x)

Tactic:
exact hs.smul hc

Premises used: UniqueDiffWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
rw :
  HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
⊢ fderiv 𝕜 (fun (x : E) ↦ f (c • x)) x = HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))

Tactic:
rw [← fderivWithin_univ, fderivWithin_comp_smul _ uniqueDiffWithinAt_univ]

Premises used: fderivWithin_univ, uniqueDiffWithinAt_univ, fderivWithin_comp_smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
inl :
  HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 univ)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0 (fderiv 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))
inr :
  ∀ (hc : c ≠ 0),
    HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
      HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))
⊢ HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))

Tactic:
rcases eq_or_ne c 0 with rfl | hc

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
⊢ HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0
      (fderivWithin 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 univ)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x)) =
    HSMul.hSMul (α := 𝕜) (β := E →L[𝕜] F) 0 (fderiv 𝕜 f (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x))

Tactic:
simp [smul_set_univ₀, *]

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : 𝕜
hc : c ≠ 0
⊢ HSMul.hSMul (β := E →L[𝕜] F) c (fderivWithin 𝕜 f (HSMul.hSMul (β := Set E) c univ) (c • x)) =
    HSMul.hSMul (β := E →L[𝕜] F) c (fderiv 𝕜 f (c • x))

Tactic:
simp [smul_set_univ₀, *]

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (HSMul.hSMul (α := 𝕜) (-1) x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) (-1) f) (HSMul.hSMul (α := 𝕜) (-1) s) (HSMul.hSMul (α := 𝕜) (-1) x))

Tactic:
have t1 := fderivWithin_comp_smul_eq_fderivWithin_smul (-1 : 𝕜) (f := f) (s := s) (x := x)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t1 :
  Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (HSMul.hSMul (α := 𝕜) (-1) x)) s x)
    (fderivWithin 𝕜 (HSMul.hSMul (α := 𝕜) (-1) f) (HSMul.hSMul (α := 𝕜) (-1) s) (HSMul.hSMul (α := 𝕜) (-1) x))
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (-x)) s x) (fderivWithin 𝕜 (-f) (-s) (-x))

Tactic:
simp only [neg_smul, one_smul, Set.neg_smul_set] at t1

Premises used: neg_smul, one_smul, Set.neg_smul_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t1 : Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (-x)) s x) (fderivWithin 𝕜 (-f) (-s) (-x))
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin.{u_1, u_1, u_3} 𝕜 (F := F) (fun (a : 𝕜) ↦ f (-a)) s x : 𝕜 →L[𝕜] F)
    (-fderivWithin 𝕜 f (-s) (-x) : 𝕜 →L[𝕜] F)

Tactic:
t1.trans fderivWithin_neg'

Premises used: fderivWithin_neg', Eq.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Equiv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
x : 𝕜
t1 : Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 (fun (x : 𝕜) ↦ f (-x)) s x) (fderivWithin 𝕜 (-f) (-s) (-x))
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin.{u_1, u_1, u_3} 𝕜 (F := F) (fun (a : 𝕜) ↦ f (-a)) s x : 𝕜 →L[𝕜] F)
    (-fderivWithin 𝕜 f (-s) (-x) : 𝕜 →L[𝕜] F)

Tactic:
exact t1.trans fderivWithin_neg'

Premises used: fderivWithin_neg', Eq.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
obtain : ∀ (b : ℝ) (ab : a < b) (sab : Ioc a b ⊆ s), HasDerivWithinAt f e (Ici a) a
⊢ HasDerivWithinAt f e (Ici a) a

Tactic:
obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ := mem_nhdsGT_iff_exists_Ioc_subset.1 hs

Premises used: mem_nhdsGT_iff_exists_Ioc_subset, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
⊢ t ⊆ s

Tactic:
have ts : t ⊆ s := Subset.trans Ioo_subset_Ioc_self sab
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
⊢ DifferentiableOn ℝ f t

Tactic:
have t_diff : DifferentiableOn ℝ f t := f_diff.mono ts
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
⊢ Convex ℝ t

Tactic:
have t_conv : Convex ℝ t := convex_Ioo a b
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
⊢ IsOpen t

Tactic:
have t_open : IsOpen t := isOpen_Ioo
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
⊢ closure t = Icc a b

Tactic:
have t_closure : closure t = Icc a b := closure_Ioo ab.ne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
rw : ∀ y ∈ Icc a b, ContinuousWithinAt f t y
⊢ ∀ y ∈ closure t, ContinuousWithinAt f t y

Tactic:
rw [t_closure]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
pos : ∀ (h : y = a), ContinuousWithinAt f t y
neg : ∀ (h : ¬y = a), ContinuousWithinAt f t y
⊢ ContinuousWithinAt f t y

Tactic:
by_cases h : y = a
-- Module: Mathlib.Analysis.Calculus.FDeriv.Extend
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set ℝ
e : E
a : ℝ
f : ℝ → E
f_diff : DifferentiableOn ℝ f s
f_lim : ContinuousWithinAt f s a
hs : s ∈ 𝓝[>] a
f_lim' : Tendsto (fun (x : ℝ) ↦ deriv f x) (𝓝[>] a) (𝓝 e)
b : ℝ
ab : a < b
sab : Ioc a b ⊆ s
t : Set ℝ := Ioo a b
ts : t ⊆ s
t_diff : DifferentiableOn ℝ f t
t_conv : Convex ℝ t
t_open : IsOpen t
t_closure : closure t = Icc a b
y : ℝ
hy : y ∈ Icc a b
h : y = a
pos : ContinuousWithinAt f t a
⊢ ContinuousWithinAt f t y

Tactic:
rw [h]