mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (f x).ofLp i) t y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
y : H
⊢ (∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (f x).ofLp i) t y
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (f x).ofLp i) y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
y : H
⊢ (∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (f x).ofLp i) y
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (f x).ofLp i) t

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (f x).ofLp i) t
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal
Module: Mathlib.Analysis.Calculus.ContDiff.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff 𝕜 n fun x ↦ (f x).ofLp i

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
n : WithTop ℕ∞
f : H → PiLp p E
⊢ (∀ (i : ι), ContDiff 𝕜 n fun x ↦ (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), ContDiff 𝕜 n fun x ↦ (f x).ofLp i
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : dist (‖f‖ ^ p.toReal) (∑ b ∈ s, ‖↑f b‖ ^ p.toReal) < ε ^ p.toReal
⊢ dist (∑ b ∈ s, lp.single p b (↑f b)) f ^ p.toReal < ε ^ p.toReal
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ (f x).ofLp i) t y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) t y) ↔
    ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x ↦ (f x).ofLp i) t y
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x ↦ (f x).ofLp i) y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableAt 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) y) ↔
    ∀ (i : ι), DifferentiableAt 𝕜 (fun x ↦ (f x).ofLp i) y
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (f x).ofLp i) t

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
this : Fintype ι
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x ↦ (f x).ofLp i) t
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
this : Fintype ι
⊢ (∀ (i : ι), Differentiable 𝕜 fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x ↦ (f x).ofLp i

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
this : Fintype ι
⊢ (∀ (i : ι), Differentiable 𝕜 fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i) ↔
    ∀ (i : ι), Differentiable 𝕜 fun x ↦ (f x).ofLp i
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal
H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal| < ε ^ p.toReal
H : ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal
⊢ ‖∑ b ∈ s, lp.single p b (↑f b) - f‖ ^ p.toReal < ε ^ p.toReal
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        (ContinuousLinearMap.proj i ∘SL ↑(continuousLinearEquiv p 𝕜 E) ∘SL f') y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasStrictFDerivAt (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        (ContinuousLinearMap.proj i ∘SL ↑(continuousLinearEquiv p 𝕜 E) ∘SL f') y) ↔
    ∀ (i : ι), HasStrictFDerivAt (fun x ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)

Tactic:
]

Goal state after:
case inr
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
Module: Mathlib.Analysis.Calculus.FDeriv.WithLp

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        (ContinuousLinearMap.proj i ∘SL ↑(continuousLinearEquiv p 𝕜 E) ∘SL f') t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y

Tactic:
]

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Finite ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
f' : H →L[𝕜] PiLp p E
t : Set H
y : H
this : Fintype ι
⊢ (∀ (i : ι),
      HasFDerivWithinAt (fun x ↦ (⇑(continuousLinearEquiv p 𝕜 E) ∘ f) x i)
        (ContinuousLinearMap.proj i ∘SL ↑(continuousLinearEquiv p 𝕜 E) ∘SL f') t y) ↔
    ∀ (i : ι), HasFDerivWithinAt (fun x ↦ (f x).ofLp i) (PiLp.proj p E i ∘SL f') t y
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝² : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝¹ : l.NeBot
hr : 0 < r
this✝ :
  TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
this :
  TendstoUniformlyOn ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)

Tactic:
]

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝³ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝² : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this✝¹ : l.NeBot
hr : 0 < r
this✝ :
  TendstoUniformlyOn (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (Metric.ball x r) ∧
    TendstoUniformlyOn (fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (Metric.ball x r)
this :
  TendstoUniformlyOn ((-fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) + -fun n x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l)
    (Metric.ball x r)
⊢ TendstoUniformlyOn (fun n z ↦ -f n.1 z + f n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i ↦ lp.single p i (↑x i)) x
⊢ ∑' (b : α), (⇑f ∘ fun i ↦ lp.single p i (↑x i)) b = ∑' (b : α), (⇑g ∘ fun i ↦ lp.single p i (↑x i)) b

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
x : ↥(lp E p)
this : HasSum (fun i ↦ lp.single p i (↑x i)) x
⊢ ∑' (b : α), (⇑f ∘ fun i ↦ lp.single p i (↑x i)) b = ∑' (b : α), (⇑g ∘ fun i ↦ lp.single p i (↑x i)) b
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.left
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ ∀ ε > 0,
    ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 x)) < ε

Tactic:
]

Goal state after:
case inr.left
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : ∀ ε > 0, ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (-f' n.1 x_1 + f' n.2 x_1) < ε
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
⊢ ∀ ε > 0,
    ∀ᶠ (n : ι × ι) in l ×ˢ l, ∀ x_1 ∈ Metric.ball x r, dist (0 x_1) (f n.1 x_1 - f n.2 x_1 - (f n.1 x - f n.2 x)) < ε
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f i

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ℕ) in atTop, F x ∈ Metric.closedBall f i
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ ‖F n - f‖ ≤ ε

Tactic:
]

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ ‖F n - f‖ ≤ ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case inr.right
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∃ pa,
    (∀ᶠ (x : ι) in l, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : ι) in l, pb y) ∧
          ∀ {x_1 : ι},
            pa x_1 → ∀ {y : ι}, pb y → ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f (x_1, y).1 x - f (x_1, y).2 x) < ε

Tactic:
]

Goal state after:
case inr.right
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
f' : ι → E → E →L[𝕜] G
x : E
r : ℝ
hf : ∀ (n : ι), ∀ y ∈ Metric.ball x r, HasFDerivAt (f n) (f' n y) y
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOn (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (Metric.ball x r)
this✝ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
this : l.NeBot
hr : 0 < r
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∃ pa,
    (∀ᶠ (x : ι) in l, pa x) ∧
      ∃ pb,
        (∀ᶠ (y : ι) in l, pb y) ∧
          ∀ {x_1 : ι},
            pa x_1 → ∀ {y : ι}, pb y → ∀ x_2 ∈ Metric.ball x r, dist (0 x_2) (f (x_1, y).1 x - f (x_1, y).2 x) < ε