mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜' (E i)
c : 𝕜
f : PreLp E
hf : f ∈ (lp E p).carrier
⊢ c • f ∈ (lp E p).carrier

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
c : 𝕜
hp : ∞ ≠ 0
f : ↥(lp E ∞)
h✝ : Nonempty α
hfc : IsLUB (Set.range fun x ↦ ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ 0 ≤ ‖c‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp✝ : p ≠ 0
c : 𝕜
f : ↥(lp E p)
hp : 0 < p.toReal
inst : NNNorm ↥(lp E p) := { nnnorm := fun f ↦ ⟨‖f‖, ⋯⟩ }
coe_nnnorm : ∀ (f : ↥(lp E p)), ↑‖f‖₊ = ‖f‖
this : ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖‖↑f a‖‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ↥(lp (fun x ↦ E) 1)
⊢ ∑' (i : α), ‖↑f i‖ = ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f g : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m < N
⊢ ↑(m + 1) ≤ N

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f g : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑g a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f g : ↥(lp (fun x ↦ E) 1)
⊢ ∑' (i : α), ↑(f + g) i = ∑' (i : α), ↑f i + ∑' (i : α), ↑g i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(lp (fun x ↦ E) 1)
⊢ Summable fun a ↦ ‖↑f a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(lp (fun x ↦ E) 1)
⊢ ∑' (i : α), ↑(c • f) i = (RingHom.id 𝕜) c • ∑' (i : α), ↑f i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E✝ : α → Type u_4
p q : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E✝ i)
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedRing 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 E
inst✝ : CompleteSpace E
f : ↥(lp (fun x ↦ E) 1)
⊢ ‖{ toFun := fun f ↦ ∑' (i : α), ↑f i, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ = ‖c‖ * ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ) (i : α) (x : E), ↑k ≤ N → ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 ↑N fun x ↦ ∑' (i : α), f i x

Tactic:
by

Goal state after:
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✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
f : (i : α) → E i
hf : Memℓp f p
⊢ Memℓp (star f) p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
x : ↥(lp E p)
⊢ star (star x) = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
hp : Fact (1 ≤ p)
f : ↥(lp E p)
⊢ ‖star f‖ = ‖f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ Memℓp (f * g) ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : ↥(lp B ∞)
⊢ 0 ≤ ‖f‖ * ‖g‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
⊢ ∀ᶠ (i : α) in cofinite, ∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝³ : (i : I) → NonUnitalNormedRing (B i)
inst✝² : (i : I) → StarRing (B i)
inst✝¹ : ∀ (i : I), NormedStarGroup (B i)
inst✝ : ∀ (i : I), CStarRing (B i)
f : ↥(lp B ∞)
⊢ ‖f‖ * ‖f‖ ≤ ‖star f * f‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝¹ : (i : I) → NormedRing (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
⊢ 1 ∈ upperBounds (Set.range fun i ↦ ‖1 i‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
I : Type u_5
B : I → Type u_6
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : ∀ (i : I), NormOneClass (B i)
inst✝ : Nonempty I
⊢ ‖1‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
I : Type u_5
B : I → Type u_6
inst✝³ : NormedField 𝕜
inst✝² : (i : I) → NormedRing (B i)
inst✝¹ : (i : I) → NormedAlgebra 𝕜 (B i)
inst✝ : ∀ (i : I), NormOneClass (B i)
k : 𝕜
⊢ Memℓp ((algebraMap 𝕜 ((i : I) → B i)) k) ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
m : ℕ
hm : ↑m ≤ N
t : Set α := {i | ¬∀ k ∈ Finset.range (m + 1), ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i}
ht : t.Finite
T : Finset α := ht.toFinset
⊢ (fun x ↦ ∑' (i : α), f i x) = (fun x ↦ ∑ i ∈ T, f i x) + fun x ↦ ∑' (i : { i // i ∉ T }), f (↑i) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p✝ q : ℝ≥0∞
inst✝⁴ : (i : α) → NormedAddCommGroup (E i)
inst✝³ : NormedRing 𝕜
inst✝² : (i : α) → Module 𝕜 (E i)
inst✝¹ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
inst✝ : DecidableEq α
p : ℝ≥0∞
i : α
a : E i
⊢ Pi.single i a ∈ lp E p

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_3
inst✝¹ : NormedRing 𝕜
inst✝ : DecidableEq α
i : α
⊢ zeroBasis i = lp.single 0 i 1

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
i : α
hi : i ∉ s
⊢ ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
h : ∀ i ∉ s, ‖if i ∈ s then f i else 0‖ ^ p.toReal = 0
⊢ ∀ i ∈ s, ‖f i‖ ^ p.toReal = ‖if i ∈ s then f i else 0‖ ^ p.toReal

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : (i : α) → E i
s : Finset α
⊢ ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : IsRCLikeNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace 𝕜 F
f : α → E → F
v : ℕ → α → ℝ
N : ℕ∞
hf : ∀ (i : α), ContDiff 𝕜 (↑N) (f i)
hv : ∀ (k : ℕ), ↑k ≤ N → Summable (v k)
h'f : ∀ (k : ℕ), ↑k ≤ N → ∀ᶠ (i : α) in cofinite, ∀ (x : E), ‖iteratedFDeriv 𝕜 k (f i) x‖ ≤ v k i
⊢ ContDiff 𝕜 ↑N fun x ↦ ∑' (i : α), f i x

Tactic:
by

Goal state after:
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 α
i : α
x : E i
this : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
⊢ 0 < (↑p).toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
hx : 0 < x
⊢ 2 * √x ^ (2 - 1) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (fun x ↦ √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x ↦ √x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun y ↦ √(f y)) (f' / (2 * √(f x))) s x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun y ↦ √(f y)) (f' / (2 * √(f x))) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

Goal state before:
pp: f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun t ↦ √(f t)) (f' / (2 * √(f x))) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (√(1 + ‖x‖ ^ 2))⁻¹ • x ∈ ball 0 1

Tactic:
by

Goal state after:
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 α
hp : 0 < p
i : α
x : E i
⊢ ‖lp.single p i x‖ = ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ (√(1 - ‖(√(1 + ‖x‖ ^ 2))⁻¹ • x‖ ^ 2))⁻¹ • (√(1 + ‖x‖ ^ 2))⁻¹ • x = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ 0 < 1 - ‖y‖ ^ 2

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
i : α
hi : i ∉ s
this : ‖↑f i‖ ^ p.toReal - ‖↑f i - if i ∈ s then ↑f i else 0‖ ^ p.toReal = 0
⊢ F i = 0

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
⊢ ∀ i ∉ s, F i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ (√(1 + ‖(√(1 - ‖y‖ ^ 2))⁻¹ • y‖ ^ 2))⁻¹ • (√(1 - ‖y‖ ^ 2))⁻¹ • y = y

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
F : α → ℝ := fun i ↦ ‖↑f i‖ ^ p.toReal - ‖↑(f - ∑ i ∈ s, lp.single p i (↑f i)) i‖ ^ p.toReal
hF : ∀ i ∉ s, F i = 0
⊢ ∀ i ∈ s, F i = ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
this : Continuous fun x ↦ (√(1 + ‖x‖ ^ 2))⁻¹
⊢ ContinuousOn (fun x ↦ (√(1 + ‖x‖ ^ 2))⁻¹ • x) univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Continuous fun x ↦ √(1 + ‖x‖ ^ 2)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn (fun x ↦ (√(1 + ‖x‖ ^ 2))⁻¹ • x) univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ √(1 - ‖y‖ ^ 2) ≠ 0

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f‖ ^ p.toReal - ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ContinuousOn (fun y ↦ (√(1 - ‖y‖ ^ 2))⁻¹ • y) (ball 0 1)

Tactic:
by

Goal state after:
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 α
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ ‖f - ∑ i ∈ s, lp.single p i (↑f i)‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ↑univUnitBall.symm 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ ⇑((Homeomorph.smulOfNeZero r ⋯).trans (IsometryEquiv.vaddConst c).toHomeomorph) '' ball 0 1 = ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (univBall c r).source = univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
hr : 0 < r
⊢ (univBall c r).target = ball c r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ball c r ⊆ (univBall c r).target

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r) 0 = c

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (univBall c r).source

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r).symm c = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ Continuous ↑(univBall c r)

Tactic:
by

Goal state after:
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
⊢ ContDiffWithinAt 𝕜 n f t y ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x ↦ (f x).ofLp i) t y

Tactic:
by

Goal state after:
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
⊢ ContDiffAt 𝕜 n f y ↔ ∀ (i : ι), ContDiffAt 𝕜 n (fun x ↦ (f x).ofLp i) y

Tactic:
by

Goal state after:
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
⊢ ContDiffOn 𝕜 n f t ↔ ∀ (i : ι), ContDiffOn 𝕜 n (fun x ↦ (f x).ofLp i) t

Tactic:
by

Goal state after:
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
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : Cauchy (map (fun n ↦ f n x) l)
this✝ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∀ᶠ (y : E) in 𝓝 x, (fun x ↦ True) y

Tactic:
by

Goal state after: