mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ (- -n)) z

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕝 : Type u_8
inst✝¹ : NormedDivisionRing 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
f : E → 𝕝
z : E
n : ℤ
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hn : ¬0 ≤ n
⊢ AnalyticAt 𝕜 (f ^ (- -n)) z
Module: Mathlib.Analysis.Analytic.Inverse

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 (a - a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : OpenPartialHomeomorph E F
a : E
i : E ≃L[𝕜] F
h0 : a ∈ f.source
p : FormalMultilinearSeries 𝕜 E F
h : HasFPowerSeriesAt (↑f) p a
hp : p 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm ↑i
A : HasFPowerSeriesAt (↑f.symm ∘ ↑f) ((p.leftInv i a).comp p) a
B : ∀ᶠ (y : E) in 𝓝 (a - a), HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f (a + y) - ↑f a) (↑f.symm (↑f (a + y)))
⊢ ∀ᶠ (y : E) in 𝓝 a, HasSum (fun n ↦ (p.leftInv i a n) fun x ↦ ↑f y - ↑f a) (↑f.symm (↑f y))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case mpr
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ AnalyticAt 𝕜 (f⁻¹ • f • g) z

pp: case mpr
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g

Tactic:
]

Goal state after:
case mpr
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ AnalyticAt 𝕜 (f⁻¹ • f • g) z

case mpr
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
⊢ g =ᶠ[𝓝 z] (f⁻¹ • f) • g
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
y : E
hy : ¬f y = 0
⊢ g y = ((f⁻¹ • f) • g) y

Tactic:
]

Goal state after:
𝕜 : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
𝕝 : Type u_8
inst✝⁴ : NormedDivisionRing 𝕝
inst✝³ : NormedAlgebra 𝕜 𝕝
inst✝² : Module 𝕝 F
inst✝¹ : IsBoundedSMul 𝕝 F
inst✝ : IsScalarTower 𝕜 𝕝 F
f : E → 𝕝
g : E → F
z : E
h₁f : AnalyticAt 𝕜 f z
h₂f : f z ≠ 0
hprod : AnalyticAt 𝕜 (fun z ↦ f z • g z) z
y : E
hy : ¬f y = 0
⊢ g y = ((f⁻¹ • f) • g) y
Module: Mathlib.Analysis.Analytic.Composition

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
r : FormalMultilinearSeries 𝕜 G H
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
v : Fin n → E
f : (a : Composition n) × Composition a.length → H :=
  fun c ↦ (r c.snd.length) (q.applyComposition c.snd (p.applyComposition c.fst v))
g : (c : Composition n) × ((i : Fin c.length) → Composition (c.blocksFun i)) → H :=
  fun c ↦ (r c.fst.length) fun i ↦ (q (c.snd i).length) (p.applyComposition (c.snd i) (v ∘ ⇑(c.fst.embedding i)))
a : Composition n
b : Composition a.length
a✝ : ⟨a, b⟩ ∈ Finset.univ
i : ℕ
hi1 : i < b.length
hi2 : i < (a.gather b).length
j : ℕ
hj1 : j < b.blocksFun ⟨i, hi1⟩
hj2 : j < (a.sigmaCompositionAux b ⟨↑⟨i, hi1⟩, ⋯⟩).length
k : ℕ
hk1 : k < a.blocksFun ((b.embedding ⟨i, hi1⟩) ⟨j, hj1⟩)
hk2 : k < (a.sigmaCompositionAux b ⟨↑⟨i, hi1⟩, ⋯⟩).blocksFun ⟨↑⟨j, hj1⟩, ⋯⟩
⊢ a.sizeUpTo (b.sizeUpTo i + j) + k = a.sizeUpTo (b.sizeUpTo i + j) + k

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt 𝕜 1 c

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst✝¹ : NormedCommRing A
inst✝ : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt 𝕜 1 c
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius

Tactic:
]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
⊢ r ≤ pf.radius
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
y : E
hy : x + y ∈ insert x s
⊢ y ∈ Metric.eball 0 r → HasSum (fun n ↦ (pf.unshift z n) fun x ↦ y) (z + (f (x + y)) (x + y - x))

Tactic:
h'y

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : y ∈ Metric.eball 0 r
⊢ HasSum (fun n ↦ (pf.unshift z n) fun x ↦ y) (z + (f (x + y)) (x + y - x))
Module: Mathlib.Analysis.Analytic.Constructions

Goal state before:
pp: 𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius

Tactic:
]

Goal state after:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius
Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderiv 𝕜 b p = h.deriv p
Module: Mathlib.Analysis.Calculus.FDeriv.Bilinear

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
b : E × F → G
u : Set (E × F)
h : IsBoundedBilinearMap 𝕜 b
p : E × F
hxs : UniqueDiffWithinAt 𝕜 u p
⊢ fderivWithin 𝕜 b u p = h.deriv p

Tactic:
by
  rw [DifferentiableAt.fderivWithin (h.differentiableAt p) hxs]
  exact h.fderiv p

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (id ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
H : DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x
this : DifferentiableWithinAt 𝕜 (id ∘ f) s x
⊢ DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : E → F
x : E
R : Type u_4
inst✝⁴ : Monoid R
inst✝³ : DistribMulAction R F
inst✝² : SMulCommClass 𝕜 R F
inst✝¹ : ContinuousConstSMul R F
c : R
inst✝ : Invertible c
⊢ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableWithinAt 𝕜 f univ x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ (∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ (∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) univ ↔ DifferentiableOn 𝕜 f univ
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
⊢ Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← differentiableOn_univ]
  exact iso.comp_differentiableOn_iff

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt (⇑iso ∘ f) f' s x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderivWithin 𝕜 (⇑iso ∘ f) s x = ↑iso ∘SL fderivWithin 𝕜 f s x

Tactic:
fderiv_comp_fderivWithin x iso.differentiableAt h hxs,

Goal state after:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ fderiv 𝕜 (⇑iso) (f x) ∘SL fderivWithin 𝕜 f s x = ↑iso ∘SL fderivWithin 𝕜 f s x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ ↑iso ∘SL fderivWithin 𝕜 f s x = ↑iso ∘SL fderivWithin 𝕜 f s x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : 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 𝕜 (⇑iso ∘ f) s x
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Add

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ 0 = 0

pp: case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x

Tactic:
]

Goal state after:
case neg
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt 𝕜 (fun y ↦ -f y) s x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderivWithin 𝕜 (⇑iso ∘ f) univ x = ↑iso ∘SL fderivWithin 𝕜 f univ x

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
x : G
⊢ fderivWithin 𝕜 (⇑iso ∘ f) univ x = ↑iso ∘SL fderivWithin 𝕜 f univ x
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
x : E
s : Set E
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
hs : UniqueDiffWithinAt 𝕜 s x
⊢ ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderivWithin 𝕜 f s x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_5
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
L : G ≃L[𝕜] G'
f : E → F →L[𝕜] G
x : E
⊢ ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x =
    ↑((ContinuousLinearEquiv.refl 𝕜 F).arrowCongr L) ∘SL fderiv 𝕜 f x

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ⇑iso) ∘ ⇑iso.symm) s (iso x)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm (iso x))
⊢ DifferentiableWithinAt 𝕜 ((f ∘ ⇑iso) ∘ ⇑iso.symm) s (iso x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
this : DifferentiableWithinAt 𝕜 (f ∘ id) s (iso x)
⊢ DifferentiableWithinAt 𝕜 f s (iso x)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
x : E
H : DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x
this : DifferentiableWithinAt 𝕜 (f ∘ id) s (iso x)
⊢ DifferentiableWithinAt 𝕜 f s (iso x)
Module: Mathlib.Analysis.Calculus.FDeriv.Equiv

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm y)

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
s : Set F
H : DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s)
y : F
hy : y ∈ s
⊢ DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) (iso.symm y)