awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
rw : f' = f' ∘SL (↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)
rw₁ : f' = f' ∘SL ContinuousLinearMap.id 𝕜 F
⊢ f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
have rw₂ : f' = f'
Tactic: rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
⊢ HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
have B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
Tactic: have B : f' = (f'.comp (iso : E →L[𝕜] F)).comp (iso.symm : F →L[𝕜] E) := by
    rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
⊢ HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
have rw : HasFDerivWithinAt
  (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E))
  ((f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
Tactic: rw [A, B]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : F →L[𝕜] G
H :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s)
    ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F))
A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
B : f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
⊢ HasFDerivWithinAt
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E))
    ((f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
have apply : MapsTo.{u_3, u_2} (β := E) (⇑iso.symm : (a : F) → E) s ((⇑iso : (a : E) → F) ⁻¹' s)
Tactic: apply H.comp (iso x) iso.symm.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f (f' ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
have rw : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) ((f' ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL (↑iso : E →L[𝕜] F))
    ((⇑iso : (a : E) → F) ⁻¹' s) x
Tactic: rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
rw :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) ((f' ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f (f' ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
have rw₁ : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F))
    ((⇑iso : (a : E) → F) ⁻¹' s) x
Tactic: rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
rw :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) ((f' ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₁ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f (f' ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
have rw₂ : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL ContinuousLinearMap.id 𝕜 E) ((⇑iso : (a : E) → F) ⁻¹' s) x
Tactic: rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
f' : E →L[𝕜] G
rw :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) ((f' ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₁ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F))
      ((⇑iso : (a : E) → F) ⁻¹' s) x
rw₂ :
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL ContinuousLinearMap.id 𝕜 E) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f (f' ∘SL (↑iso.symm : F →L[𝕜] E)) s ((iso : (a : E) → F) x)
have rw₃ : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
  HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) f' ((⇑iso : (a : E) → F) ⁻¹' s) x
Tactic: rw [← iso.comp_right_hasFDerivWithinAt_iff, ContinuousLinearMap.comp_assoc,
    iso.coe_symm_comp_coe, ContinuousLinearMap.comp_id]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have pos : ∀ (h : DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)),
  Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)),
    Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
      (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have neg : ∀ (h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)),
  Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s (iso x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have this : ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
Tactic: have : ¬DifferentiableWithinAt 𝕜 (f ∘ iso) (iso ⁻¹' s) x := by
      intro h'
      exact h (iso.comp_right_differentiableWithinAt_iff.1 h')
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have neg : Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
  (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
neg :
  Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have neg₁ : Eq (α := E →L[𝕜] G) 0 (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
hxs : UniqueDiffWithinAt 𝕜 ((⇑iso : (a : E) → F) ⁻¹' s) x
h : ¬DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
this : ¬DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
neg :
  Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
neg₁ : Eq (α := E →L[𝕜] G) 0 (comp (σ₂₃ := RingHom.id 𝕜) 0 (↑iso : E →L[𝕜] F))
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x)
    (fderivWithin 𝕜 f s ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have neg₂ : Eq (α := E →L[𝕜] G) 0 0
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.zero_comp]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
x : E
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (f ∘ (⇑iso : (a : E) → F)) x)
    (fderiv 𝕜 f ((iso : (a : E) → F) x) ∘SL (↑iso : E →L[𝕜] F))
have rw : UniqueDiffWithinAt 𝕜 (preimage.{u_2, u_3} (β := F) (⇑iso : (a : E) → F) univ) x
Tactic: rw [← fderivWithin_univ, ← fderivWithin_univ, ← iso.comp_right_fderivWithin, preimage_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ Eq (α := (x : G) → G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f)) fun (x : G) ↦
    (↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x
have h : ∀ (x : G),
  Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑(↑iso : E ≃L[𝕜] F) : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
have obtain : ∀ (C : ℝ≥0) (hC : AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)),
  ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
Tactic: obtain ⟨C, hC⟩ := hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ≥0), AntilipschitzWith.{u_2, u_3} (α := E) (β := F) C (⇑f' : (a : E) → F)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
have hf'₁ : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
Tactic: replace hf' : ∃ C, ∀ z, ‖z‖ ≤ C * ‖f' z‖ := by
    obtain ⟨C, hC⟩ := hf'
    exact ⟨C, fun x ↦ by simpa using hC.le_mul_dist 0 x⟩
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
have A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
Tactic: have A : (fun z ↦ z - x) =O[𝓝[s] x] fun z ↦ f' (z - x) :=
    isBigO_iff.mpr <| hf'.imp fun C hC ↦ Eventually.of_forall fun z ↦ hC (z - x)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
have this : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
Tactic: have : (fun z ↦ f z - f x) ~[𝓝[s] x] fun z ↦ f' (z - x) := h.isLittleO.trans_isBigO A
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (hypothesis)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
have this₁ : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
Tactic: have : ∀ᶠ (x_1 : E) in 𝓝[s] x, x_1 ∈ ({x}ᶜ : Set E) → f x_1 ∈ ({f x}ᶜ : Set F) := by
    simpa [sub_eq_zero, not_imp_not] using (A.trans this.isBigO_symm).eq_zero_imp
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
⊢ Tendsto f (𝓝[s \ {x}] x) (𝓝[≠] f x)
have apply : map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
Tactic: apply le_inf ((map_mono (nhdsWithin_mono x diff_subset)).trans h.continuousWithinAt)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
have rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
Tactic: rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Equiv (goal)
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
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * norm.{u_3} (E := F) ((f' : (a : E) → F) z : F)
A : IsBigO.{u_2, u_2, u_3} (E := E) (F := F) (𝓝[s] x) (fun (z : E) ↦ z - x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this_1 : IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (z : E) ↦ f z - f x) fun (z : E) ↦ (f' : (a : E) → F) (z - x)
this : ∀ᶠ (x_1 : E) in 𝓝[s] x, Membership.mem (γ := Set E) {x}ᶜ x_1 → Membership.mem (γ := Set F) {f x}ᶜ (f x_1)
rwa : {f x}ᶜ ∈ map f (𝓝[s \ {x}] x)
⊢ map f (𝓝[s \ {x}] x) ≤ 𝓟 {f x}ᶜ
have rwa₁ : ∀ᶠ (x_1 : F) in map f (𝓝[s \ {x}] x), Membership.mem (γ := Set F) {f x}ᶜ x_1
Tactic: rwa [le_principal_iff, ← eventually_mem_set, eventually_map, diff_eq, nhdsWithin_inter',
    eventually_inf_principal]