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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have pos : Eq (α := G →L[𝕜] F) (fderiv 𝕜 (⇑iso : (a : E) → F) (f x) ∘SL fderivWithin 𝕜 f s x)
  ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
Tactic: rw [fderiv_comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]
-- 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
pos :
  Eq (α := G →L[𝕜] F) (fderiv 𝕜 (⇑iso : (a : E) → F) (f x) ∘SL fderivWithin 𝕜 f s x)
    ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have pos₁ : Eq (α := G →L[𝕜] F) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
Tactic: rw [fderiv_comp_fderivWithin x iso.differentiableAt h hxs, iso.fderiv]
-- 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have this : ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
Tactic: have : ¬DifferentiableWithinAt 𝕜 (iso ∘ f) s x := mt iso.comp_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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have neg : Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.comp_zero]
-- 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
neg :
  Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have neg₁ : Eq (α := G →L[𝕜] F) 0 ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.comp_zero]
-- 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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
this : ¬DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
neg :
  Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
neg₁ : Eq (α := G →L[𝕜] F) 0 ((↑iso : E →L[𝕜] F).comp (σ₁₂ := RingHom.id 𝕜) 0)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have neg₂ : Eq (α := G →L[𝕜] F) 0 0
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt this, ContinuousLinearMap.comp_zero]
-- 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 : G → E
x : G
⊢ Eq (α := G →L[𝕜] F) (fderiv 𝕜 ((⇑iso : (a : E) → F) ∘ f) x) ((↑iso : E →L[𝕜] F) ∘SL fderiv 𝕜 f x)
have rw : Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) univ x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f univ x)
Tactic: rw [← fderivWithin_univ, ← fderivWithin_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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderivWithin 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
have change : Eq (α := E →L[𝕜] F →L[𝕜] G')
  (fderivWithin 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) s x)
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
Tactic: change fderivWithin 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) s 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderivWithin 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) s x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
have rw : Eq (α := E →L[𝕜] F →L[𝕜] G')
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderivWithin 𝕜 f s x)
Tactic: rw [ContinuousLinearEquiv.comp_fderivWithin _ hs]
-- 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
have change : Eq (α := E →L[𝕜] F →L[𝕜] G')
  (fderiv 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) x)
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
Tactic: change fderiv 𝕜 (((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘ f) 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ Eq (α := E →L[𝕜] F →L[𝕜] G')
    (fderiv 𝕜 ((⇑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (a : F →L[𝕜] G) → F →L[𝕜] G') ∘ f) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
have rw : Eq (α := E →L[𝕜] F →L[𝕜] G')
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
  ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x)
Tactic: rw [ContinuousLinearEquiv.comp_fderiv]
-- 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
G' : Type u_5
inst_7 : NormedAddCommGroup G'
inst_8 : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
⊢ Eq (α := (x : E) → E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) fun (x : E) ↦
    (↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘SL fderiv 𝕜 f x
have h : ∀ (x : E),
  Eq (α := E →L[𝕜] F →L[𝕜] G') (fderiv 𝕜 (fun (x : E) ↦ (↑L : G →L[𝕜] G') ∘SL f x) x)
    ((↑(arrowCongr (ContinuousLinearEquiv.refl 𝕜 F) L) : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G') ∘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
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
⊢ DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
have refine : ∀ (H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x),
  DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
Tactic: refine ⟨fun H => ?_, fun H => H.comp x iso.differentiableWithinAt (mapsTo_preimage _ s)⟩
-- 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
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)
have H₁ : DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
  ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F) : E)
Tactic: rw [← iso.symm_apply_apply x] at H
Cleared hypotheses: 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
H :
  DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) ((iso : (a : E) → F) x : F) : E)
⊢ DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → 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.differentiableWithinAt
-- 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
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
⊢ DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
have this : DifferentiableWithinAt 𝕜
  (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
  ((iso : (a : E) → F) x)
Tactic: have : DifferentiableWithinAt 𝕜 ((f ∘ iso) ∘ iso.symm) s (iso x) := by
    rw [← iso.symm_apply_apply x] at H
    apply H.comp (iso x) iso.symm.differentiableWithinAt
    intro y hy
    simpa only [mem_preimage, apply_symm_apply] using hy
-- 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
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
this :
  DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)
⊢ DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
have rwa : ∀
  (this :
    DifferentiableWithinAt 𝕜
      (f ∘ Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑iso : (a : E) → F) (⇑iso.symm : (a : F) → E)) s
      ((iso : (a : E) → F) x)),
  DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
Tactic: rwa [Function.comp_assoc, iso.self_comp_symm] at this
Cleared hypotheses: this
-- 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
H : DifferentiableWithinAt 𝕜 (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) x
this :
  DifferentiableWithinAt 𝕜
    (Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)) s
    ((iso : (a : E) → F) x)
rwa :
  ∀
    (this :
      DifferentiableWithinAt 𝕜
        (f ∘ Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑iso : (a : E) → F) (⇑iso.symm : (a : F) → E)) s
        ((iso : (a : E) → F) x)),
    DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
⊢ DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
have rwa₁ : ∀ (this : DifferentiableWithinAt 𝕜 (f ∘ id) s ((iso : (a : E) → F) x)),
  DifferentiableWithinAt 𝕜 f s ((iso : (a : E) → F) x)
Tactic: rwa [Function.comp_assoc, iso.self_comp_symm] at this
Cleared hypotheses: this
-- 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
⊢ DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s) ↔
    DifferentiableOn 𝕜 f s
have refine : ∀ (H : DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s)) (y : F)
  (hy : y ∈ s), DifferentiableWithinAt 𝕜 f s y
Tactic: refine ⟨fun H y hy => ?_, fun H y hy => iso.comp_right_differentiableWithinAt_iff.2 (H _ hy)⟩
-- 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
H : DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 f s y
have rw : DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
  ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) y : E)
Tactic: rw [← iso.apply_symm_apply y, ← comp_right_differentiableWithinAt_iff]
-- 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
H : DifferentiableOn.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F)) ((⇑iso : (a : E) → F) ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt.{u_1, u_2, u_4} 𝕜 (E := E) (f ∘ (⇑iso : (a : E) → F) : E → G)
    ((⇑iso : (a : E) → F) ⁻¹' s : Set E) ((iso.symm : (a : F) → E) y : E)
have a : Membership.mem.{u_2, u_2} (α := E) (γ := Set E) ((⇑iso : (a : E) → F) ⁻¹' s) ((iso.symm : (a : F) → E) y : E)
Tactic: apply 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
f' : F →L[𝕜] G
⊢ HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s) x ↔
    HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
have refine : ∀ (H : HasFDerivWithinAt (f ∘ (⇑iso : (a : E) → F)) (f' ∘SL (↑iso : E →L[𝕜] F)) ((⇑iso : (a : E) → F) ⁻¹' s) x),
  HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
Tactic: refine ⟨fun H => ?_, fun H => H.comp x iso.hasFDerivWithinAt (mapsTo_preimage _ s)⟩
-- 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) x
⊢ HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
have 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))
Tactic: rw [← iso.symm_apply_apply x] at H
Cleared hypotheses: 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
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))
⊢ f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
have rw : f = f ∘ id
Tactic: rw [Function.comp_assoc, iso.self_comp_symm]
-- 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))
⊢ HasFDerivWithinAt f f' s ((iso : (a : E) → F) x)
have A : f = Function.comp.{u_3 + 1, u_2 + 1, u_4 + 1} (β := E) (f ∘ (⇑iso : (a : E) → F)) (⇑iso.symm : (a : F) → E)
Tactic: have A : f = (f ∘ iso) ∘ iso.symm := by
    rw [Function.comp_assoc, iso.self_comp_symm]
    rfl
-- 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)
⊢ f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
have rw : f' = f' ∘SL (↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)
Tactic: 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)
rw : f' = f' ∘SL (↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)
⊢ f' = (f' ∘SL (↑iso : E →L[𝕜] F)) ∘SL (↑iso.symm : F →L[𝕜] E)
have rw₁ : f' = f' ∘SL ContinuousLinearMap.id 𝕜 F
Tactic: rw [ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm, ContinuousLinearMap.comp_id]