awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap (hypothesis)
Goal:
𝕜 : Type u_1
ι : Type u_2
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : (i : ι) → NormedAddCommGroup (F i)
inst_2 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_5 : NormedAddCommGroup H
inst_6 : NormedSpace 𝕜 H
inst_7 : Fintype ι
inst_8 : DecidableEq ι
fg : ContinuousMultilinearMap 𝕜 G H × ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
⊢ HasStrictFDerivAt
    (fun
        (fg :
          ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))) ↦
      fg.1.compContinuousLinearMap (M₁ := F) (M₁' := G) fg.2)
    (HAdd.hAdd (α :=
      ContinuousMultilinearMap 𝕜 G H ×
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
        ContinuousMultilinearMap 𝕜 F H)
      (β :=
      ContinuousMultilinearMap 𝕜 G H ×
          ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
        ContinuousMultilinearMap 𝕜 F H)
      (compContinuousLinearMapL (E := F) (E₁ := G) fg.2 ∘SL
          ContinuousLinearMap.fst 𝕜 (ContinuousMultilinearMap 𝕜 G H)
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H)
      (fg.1.fderivCompContinuousLinearMap (E := F) (E₁ := G) fg.2 ∘SL
          ContinuousLinearMap.snd 𝕜 (ContinuousMultilinearMap 𝕜 G H)
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) :
        ContinuousMultilinearMap 𝕜 G H ×
            ((i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)) →L[𝕜]
          ContinuousMultilinearMap 𝕜 F H))
    fg
have this : HasStrictFDerivAt (𝕜 := 𝕜) (F := ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
  (⇑(compContinuousLinearMapContinuousMultilinear 𝕜 F G H) :
    (a : (i : ι) → F i →L[𝕜] G i) → ContinuousMultilinearMap 𝕜 G H →L[𝕜] ContinuousMultilinearMap 𝕜 F H)
  (linearDeriv (M₁ := fun (i : ι) ↦ ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i))
    (compContinuousLinearMapContinuousMultilinear 𝕜 F G H) fg.2)
  fg.2
Tactic: have := (compContinuousLinearMapContinuousMultilinear 𝕜 F G H).hasStrictFDerivAt fg.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
s : Set E
x : E
inst_9 : Finite ι
hf : DifferentiableWithinAt 𝕜 f s x
hg : ∀ (i : ι), DifferentiableWithinAt 𝕜 (g i) s x
⊢ DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x
have intro : ∀ (val : Fintype ι),
  DifferentiableWithinAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) s x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap (goal)
Goal:
𝕜 : Type u_1
ι : Type u_2
E : Type u_3
F : ι → Type u_4
G : ι → Type u_5
H : Type u_6
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : (i : ι) → NormedAddCommGroup (F i)
inst_4 : (i : ι) → NormedSpace.{u_1, u_4} 𝕜 (F i)
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_5} 𝕜 (G i)
inst_7 : NormedAddCommGroup H
inst_8 : NormedSpace 𝕜 H
f : E → ContinuousMultilinearMap 𝕜 G H
g : (i : ι) → E → ContinuousLinearMap.{u_1, u_1, u_4, u_5} (RingHom.id 𝕜) (F i) (G i)
x : E
inst_9 : Finite ι
hf : DifferentiableAt 𝕜 f x
hg : ∀ (i : ι), DifferentiableAt 𝕜 (g i) x
⊢ DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x
have intro : ∀ (val : Fintype ι),
  DifferentiableAt 𝕜 (F := ContinuousMultilinearMap 𝕜 F H)
    (fun (x : E) ↦ (f x).compContinuousLinearMap (M₁ := F) (M₁' := G) fun (x_1 : ι) ↦ g x_1 x) x
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
⊢ Eq (α := (x : E) → E →L[𝕜] F) (fderivWithin 𝕜 f univ) (fderiv 𝕜 f)
have h : ∀ (x x_1 : E),
  Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F) ((fderiv 𝕜 f x : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Defs (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F) ((fderiv 𝕜 f x : (a : E) → F) x_1 : F)
have h : Eq.{u_3 + 1} (α := F) ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F)
  ((fderivWithin 𝕜 f univ x : (a : E) → F) x_1 : F)
Tactic: rw [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
⊢ DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x
have refine : ∀ (H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x), DifferentiableWithinAt 𝕜 f s x
Tactic: refine ⟨fun H => ?_, fun H => iso.differentiable.differentiableAt.comp_differentiableWithinAt x H⟩
-- 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
H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
have this : DifferentiableWithinAt.{u_1, u_4, u_2} 𝕜 (F := E)
  (Function.comp.{u_4 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) ((⇑iso : (a : E) → F) ∘ f)) s x
Tactic: have : DifferentiableWithinAt 𝕜 (iso.symm ∘ iso ∘ f) s x :=
    iso.symm.differentiable.differentiableAt.comp_differentiableWithinAt x 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
H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
this :
  DifferentiableWithinAt.{u_1, u_4, u_2} 𝕜 (F := E)
    (Function.comp.{u_4 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) ((⇑iso : (a : E) → F) ∘ f)) s x
⊢ DifferentiableWithinAt 𝕜 f s x
have rwa : ∀
  (this :
    DifferentiableWithinAt 𝕜 (F := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) (⇑iso : (a : E) → F) ∘ f) s x),
  DifferentiableWithinAt 𝕜 f s x
Tactic: rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] 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 : G → E
s : Set G
x : G
H : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) s x
this :
  DifferentiableWithinAt.{u_1, u_4, u_2} 𝕜 (F := E)
    (Function.comp.{u_4 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) ((⇑iso : (a : E) → F) ∘ f)) s x
rwa :
  ∀
    (this :
      DifferentiableWithinAt 𝕜 (F := E)
        (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F) (⇑iso.symm : (a : F) → E) (⇑iso : (a : E) → F) ∘ f) s x),
    DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 f s x
have rwa₁ : ∀ (this : DifferentiableWithinAt 𝕜 (id ∘ f) s x), DifferentiableWithinAt 𝕜 f s x
Tactic: rwa [← Function.comp_assoc iso.symm iso f, iso.symm_comp_self] 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 : G → E
x : G
⊢ DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) x ↔ DifferentiableAt 𝕜 f x
have rw : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔ DifferentiableAt 𝕜 f x
Tactic: rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
    iso.comp_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 : G → E
x : G
rw : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔ DifferentiableAt 𝕜 f x
⊢ DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) x ↔ DifferentiableAt 𝕜 f x
have rw₁ : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔ DifferentiableWithinAt 𝕜 f univ x
Tactic: rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
    iso.comp_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 : G → E
x : G
rw : DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔ DifferentiableAt 𝕜 f x
rw₁ :
  DifferentiableWithinAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ x ↔
    DifferentiableWithinAt 𝕜 f univ x
⊢ DifferentiableAt.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) x ↔ DifferentiableAt 𝕜 f x
have rw₂ : DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableWithinAt 𝕜 f univ x
Tactic: rw [← differentiableWithinAt_univ, ← differentiableWithinAt_univ,
    iso.comp_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 : G → E
⊢ Differentiable.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) ↔ Differentiable 𝕜 f
have rw : DifferentiableOn.{u_1, u_4, u_3} 𝕜 (F := F) ((⇑iso : (a : E) → F) ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
Tactic: rw [← differentiableOn_univ, ← differentiableOn_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 ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] E
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x ↔ HasFDerivWithinAt f f' s x
have refine : ∀ (H : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') s x), HasFDerivWithinAt f f' s x
Tactic: refine ⟨fun H => ?_, fun H => iso.hasFDerivAt.comp_hasFDerivWithinAt x 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
x : G
f' : G →L[𝕜] E
⊢ HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x ↔ HasStrictFDerivAt f f' x
have refine : ∀ (H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x), HasStrictFDerivAt f f' x
Tactic: refine ⟨fun H => ?_, fun H => iso.hasStrictFDerivAt.comp x 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
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
⊢ HasStrictFDerivAt f f' x
have h : f = fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x)
Tactic: convert! iso.symm.hasStrictFDerivAt.comp x H using 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 : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
h : f = fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x)
⊢ HasStrictFDerivAt f f' x
have h₁ : f' = (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f'
Tactic: convert! iso.symm.hasStrictFDerivAt.comp x H using 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 : G → E
x : G
f' : G →L[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
⊢ f = fun (x : G) ↦ (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) x)
have h : ∀ (z : G), f z = (iso.symm : (a : F) → E) (((⇑iso : (a : E) → F) ∘ f) z)
Tactic: ext z
-- 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
f' : G →L[𝕜] E
H : HasStrictFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x
⊢ f' = (↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f'
have h : ∀ (z : G),
  Eq.{u_2 + 1} (α := E) ((f' : (a : G) → E) z : E)
    (((↑iso.symm : F →L[𝕜] E) ∘SL (↑iso : E →L[𝕜] F) ∘SL f' : (a : G) → E) z : E)
Tactic: ext z
-- 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
f' : G →L[𝕜] E
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') x ↔ HasFDerivAt f f' x
have simp_rw : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL f') univ x ↔ HasFDerivWithinAt f f' univ x
Tactic: simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_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 : G → E
s : Set G
x : G
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') s x
have rw : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL f') s x
Tactic: rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_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 : G → E
s : Set G
x : G
f' : G →L[𝕜] F
rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL f') s x
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') s x
have rw₁ : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL f') s x
Tactic: rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_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 : G → E
s : Set G
x : G
f' : G →L[𝕜] F
rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL f') s x
rw₁ :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL f') s x
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') s x
have rw₂ : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (ContinuousLinearMap.id 𝕜 F ∘SL f') s x
Tactic: rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_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 : G → E
s : Set G
x : G
f' : G →L[𝕜] F
rw :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) ((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E) ∘SL f') s x
rw₁ :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (((↑iso : E →L[𝕜] F) ∘SL (↑iso.symm : F →L[𝕜] E)) ∘SL f') s x
rw₂ :
  HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔
    HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) (ContinuousLinearMap.id 𝕜 F ∘SL f') s x
⊢ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') s x
have rw₃ : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x ↔ HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' s x
Tactic: rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
    ContinuousLinearMap.id_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 : G → E
x : G
f' : G →L[𝕜] F
⊢ HasFDerivAt ((⇑iso : (a : E) → F) ∘ f) f' x ↔ HasFDerivAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') x
have simp_rw : HasFDerivWithinAt ((⇑iso : (a : E) → F) ∘ f) f' univ x ↔ HasFDerivWithinAt f ((↑iso.symm : F →L[𝕜] E) ∘SL f') univ x
Tactic: simp_rw [← hasFDerivWithinAt_univ, iso.comp_hasFDerivWithinAt_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 : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 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 : ∀ (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)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 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
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (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)
⊢ Eq (α := G →L[𝕜] F) (fderivWithin 𝕜 ((⇑iso : (a : E) → F) ∘ f) s x) ((↑iso : E →L[𝕜] F) ∘SL fderivWithin 𝕜 f s x)
have neg : ∀ (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)
Tactic: by_cases h : DifferentiableWithinAt 𝕜 f s x