awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i_1 : ℕ
a : 𝕜
i : ℕ
hi :
  ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
        (iteratedFDeriv 𝕜 i f (a • x))
hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f
v : E
x : (i : Fin (i + 1)) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (i + 1) (fun (z : E) ↦ f (a • z)) v : (a : (i : Fin (i + 1)) → E) → F) x : F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
            (iteratedFDeriv 𝕜 (i + 1) f (a • v)) :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
have succ : Eq.{uF + 1} (α := F)
  ((comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                  ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
            (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
              ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
          (fderiv 𝕜 (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z))) v :
        (a : (i : Fin (i + 1)) → E) → F)
      x :
    F)
  ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
          (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                  (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
              (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
            (fderiv 𝕜 (iteratedFDeriv 𝕜 i f)) (a • v)) :
        (a : (i : Fin (i + 1)) → E) → F)
      x :
    F)
Tactic: rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑i : ℕ∞ω) f
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
      (iteratedFDeriv 𝕜 i f (a • x))
have zero : ∀ (hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
      (iteratedFDeriv 𝕜 0 f (a • x))
Tactic: induction i with
  | zero => ext; simp
  | succ i hi =>
    ext v
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply,
      ContinuousMultilinearMap.smul_apply]
    rw [fderiv_fun_const_smul, fderiv_comp_smul, smul_smul, ← pow_succ]
    · simp
    rw [← Function.comp_def (g := (a • ·))]
    apply DifferentiableAt.comp
    · exact hf.contDiffAt.differentiableAt_iteratedFDeriv (Nat.cast_lt.2 i.lt_succ_self)
    · exact differentiableAt_id.const_smul _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑i : ℕ∞ω) f
zero :
  ∀ (hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv 𝕜 0 fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
        (iteratedFDeriv 𝕜 0 f (a • x))
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
      (iteratedFDeriv 𝕜 i f (a • x))
have succ : ∀ (i : ℕ)
  (hi :
    ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
      Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
        HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
          (iteratedFDeriv 𝕜 i f (a • x)))
  (hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f),
  Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (i + 1) fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
      (iteratedFDeriv 𝕜 (i + 1) f (a • x))
Tactic: induction i with
  | zero => ext; simp
  | succ i hi =>
    ext v
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply,
      ContinuousMultilinearMap.smul_apply]
    rw [fderiv_fun_const_smul, fderiv_comp_smul, smul_smul, ← pow_succ]
    · simp
    rw [← Function.comp_def (g := (a • ·))]
    apply DifferentiableAt.comp
    · exact hf.contDiffAt.differentiableAt_iteratedFDeriv (Nat.cast_lt.2 i.lt_succ_self)
    · exact differentiableAt_id.const_smul _
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
⊢ ContDiffAt 𝕜 n (Prod.map f g) (x, y)
have hf₁ : ContDiffWithinAt 𝕜 n f univ x
Tactic: rw [ContDiffAt] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
x : E
y : E'
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g y
hf₁ : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffAt 𝕜 n (Prod.map f g) (x, y)
have hg₁ : ContDiffWithinAt 𝕜 n g univ y
Tactic: rw [ContDiffAt] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
E' : Type u_3
inst_5 : NormedAddCommGroup E'
inst_6 : NormedSpace 𝕜 E'
F' : Type u_4
inst_7 : NormedAddCommGroup F'
inst_8 : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n (Prod.map f g)
have rw : ∀ (hf : ∀ (x : E), ContDiffAt 𝕜 n f x) (hg : ∀ (x : E'), ContDiffAt 𝕜 n g x) (x : E × E'),
  ContDiffAt 𝕜 n (Prod.map f g) x
Tactic: rw [contDiff_iff_contDiffAt] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
R : Type u_3
inst_1 : NormedRing R
inst_2 : NormedAlgebra 𝕜 R
inst_3 : HasSummableGeomSeries R
x : Rˣ
⊢ ContDiffAt 𝕜 n Ring.inverse (↑x : R)
have this : ContDiffWithinAt 𝕜 n Ring.inverse {x : R | IsUnit x} (↑x : R)
Tactic: have := AnalyticOnNhd.contDiffOn (analyticOnNhd_inverse (𝕜 := 𝕜) (A := R)) (n := n)
    Units.isOpen.uniqueDiffOn x x.isUnit
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
n : ℕ∞ω
𝕜' : Type u_4
inst_3 : NormedField 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
hf : ContDiff 𝕜 n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff.{u_1, uE, u_4} 𝕜 (F := 𝕜') n fun (x : E) ↦ (f x)⁻¹
have rw : ∀ (x : E), ContDiffAt.{u_1, uE, u_4} 𝕜 (F := 𝕜') n (fun (x : E) ↦ (f x)⁻¹) x
Tactic: rw [contDiff_iff_contDiffAt]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f g : E → 𝕜
n : ℕ∞ω
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
h0 : ∀ (x : E), g x ≠ 0
⊢ ContDiff 𝕜 (F := 𝕜) n fun (x : E) ↦ f x / g x
have simp : ∀ (hf : ∀ (x : E), ContDiffAt 𝕜 n f x) (hg : ∀ (x : E), ContDiffAt 𝕜 n g x) (x : E),
  ContDiffAt 𝕜 (F := 𝕜) n (fun (x : E) ↦ f x / g x) x
Tactic: simp only [contDiff_iff_contDiffAt] at *
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
⊢ ContDiffAt 𝕜 n inverse (↑e : E →L[𝕜] F)
have a : Nontrivial E
Tactic: nontriviality E
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
⊢ ContDiffAt 𝕜 n inverse (↑e : E →L[𝕜] F)
have this : inverse = O₁ ∘ Ring.inverse ∘ O₂
Tactic: have : ContinuousLinearMap.inverse = O₁ ∘ Ring.inverse ∘ O₂ := funext (inverse_eq_ringInverse e)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n inverse (↑e : E →L[𝕜] F)
have rw : ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)
have h₁ : ContDiff 𝕜 n O₁
Tactic: have h₁ : ContDiff 𝕜 n O₁ := contDiff_id.clm_comp contDiff_const
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)
have h₂ : ContDiff 𝕜 n O₂
Tactic: have h₂ : ContDiff 𝕜 n O₂ := contDiff_const.clm_comp contDiff_id
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n (O₁ ∘ Ring.inverse ∘ O₂) (↑e : E →L[𝕜] F)
have refine : ContDiffAt 𝕜 n Ring.inverse (O₂ (↑e : E →L[𝕜] F))
Tactic: refine h₁.contDiffAt.comp _ (ContDiffAt.comp _ ?_ h₂.contDiffAt)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E ≃L[𝕜] F
h : Nontrivial E
O₁ : (E →L[𝕜] E) → F →L[𝕜] E := fun (f : E →L[𝕜] E) ↦ f ∘SL (↑e.symm : F →L[𝕜] E)
O₂ : (E →L[𝕜] F) → E →L[𝕜] E := fun (f : E →L[𝕜] F) ↦ (↑e.symm : F →L[𝕜] E) ∘SL f
this : inverse = O₁ ∘ Ring.inverse ∘ O₂
h₁ : ContDiff 𝕜 n O₁
h₂ : ContDiff 𝕜 n O₂
⊢ ContDiffAt 𝕜 n Ring.inverse (O₂ (↑e : E →L[𝕜] F))
have h : O₂ (↑e : E →L[𝕜] F) = (↑1 : E →L[𝕜] E)
Tactic: convert! contDiffAt_ringInverse 𝕜 (1 : (E →L[𝕜] E)ˣ)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
e : E →L[𝕜] F
he : e.IsInvertible
⊢ ContDiffAt 𝕜 n inverse e
have rcases : ∀ (M : E ≃L[𝕜] F), ContDiffAt 𝕜 n inverse (↑M : E →L[𝕜] F)
Tactic: rcases he with ⟨M, rfl⟩
Cleared hypotheses: e, he
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 ω (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 ω (↑f.symm : F → E) a
have h : AnalyticAt 𝕜 (↑f.symm : F → E) a
Tactic: apply AnalyticAt.contDiffAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
hf : ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 (↑0 : ℕ∞ω) (↑f.symm : F → E) a
have zero : ∃ u ∈ 𝓝 a, ContinuousOn (↑f.symm : F → E) u
Tactic: apply contDiffAt_zero.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
⊢ ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
have succ : ∀ (f' : E → E →L[𝕜] F) (hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)) (u : Set E)
  (hu : u ∈ 𝓝 ((↑f.symm : F → E) a)) (hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x),
  ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
Tactic: obtain ⟨f', ⟨u, hu, hff'⟩, hf'⟩ := contDiffAt_succ_iff_hasFDerivAt.mp hf
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
⊢ ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
have succ : ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a
Tactic: apply contDiffAt_succ_iff_hasFDerivAt.2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
⊢ ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a
have eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
Tactic: have eq_f₀' : f' (f.symm a) = f₀' := (hff' (f.symm a) (mem_of_mem_nhds hu)).unique hf₀'
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
⊢ ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a
have succ : ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
Tactic: refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
succ : ∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) ((inverse ∘ f' ∘ (↑f.symm : F → E)) x) x
⊢ ∃ (f' : F → F →L[𝕜] E), (∃ u ∈ 𝓝 a, ∀ x ∈ u, HasFDerivAt (↑f.symm : F → E) (f' x) x) ∧ ContDiffAt 𝕜 (↑n : ℕ∞ω) f' a
have succ₁ : ContDiffAt 𝕜 (↑n : ℕ∞ω) (inverse ∘ f' ∘ (↑f.symm : F → E)) a
Tactic: refine ⟨inverse ∘ f' ∘ f.symm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Operations (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
n_1 : ℕ∞ω
inst_5 : CompleteSpace E
f : OpenPartialHomeomorph E F
f₀' : E ≃L[𝕜] F
a : F
ha : a ∈ f.target
hf₀' : HasFDerivAt (↑f : E → F) (↑f₀' : E →L[𝕜] F) ((↑f.symm : F → E) a)
n : ℕ
IH :
  ∀ (hf : ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)),
    ContDiffAt 𝕜 (↑(↑n : ℕ∞) : ℕ∞ω) (↑f.symm : F → E) a
hf : ContDiffAt 𝕜 (↑(↑n.succ : ℕ∞) : ℕ∞ω) (↑f : E → F) ((↑f.symm : F → E) a)
f' : E → E →L[𝕜] F
hf' : ContDiffAt 𝕜 (↑n : ℕ∞ω) f' ((↑f.symm : F → E) a)
u : Set E
hu : u ∈ 𝓝 ((↑f.symm : F → E) a)
hff' : ∀ x ∈ u, HasFDerivAt (↑f : E → F) (f' x) x
eq_f₀' : f' ((↑f.symm : F → E) a) = (↑f₀' : E →L[𝕜] F)
⊢ {y : E | ∃ (e : E ≃L[𝕜] F), (↑e : E →L[𝕜] F) = f' y} ∈ 𝓝 ((↑f.symm : F → E) a)
have hf₀'₁ : range (ι := E ≃L[𝕜] F) ContinuousLinearEquiv.toContinuousLinearMap ∈ 𝓝 (↑f₀' : E →L[𝕜] F)
Tactic: have hf₀' := f₀'.nhds