mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁹ : RCLike 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : InnerProductSpace 𝕜 E
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : InnerProductSpace 𝕜 G
H : Type u_5
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace 𝕜 H
inst✝ : CompleteSpace H
u v : ↥(unitary (H →L[𝕜] H))
⊢ (let __src := ↑(u * v);
    { toLinearMap := ↑__src, invFun := ⇑↑↑(star (u * v)), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) =
    (let __src := ↑u;
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star u), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }) *
      let __src := ↑v;
      { toLinearMap := ↑__src, invFun := ⇑↑↑(star v), left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

Tactic:
ext; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : CharZero k
n : ℕ
inst✝ : NeZero n
s : Simplex k P n
i : Fin (n + 1)
⊢ Collinear k {s.points i, s.centroid, s.faceOppositeCentroid i}

Tactic:
apply collinear_insert_of_mem_affineSpan_pair
  have h : s.points i = (-n : k) • (s.faceOppositeCentroid i -ᵥ s.centroid) +ᵥ s.centroid := by
    rw [← neg_vsub_eq_vsub_rev, neg_smul_neg, ← point_vsub_centroid_eq_smul_vsub, vsub_vadd]
  rw [h]
  exact smul_vsub_vadd_mem_affineSpan_pair _ _ _

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (-f) 0

Tactic:
apply memℓp_zero
    simp [hf.finite_dsupport]

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}

Tactic:
simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_ofPred_eq]

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
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
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
f : α → E → F
f' : α → E → E →L[𝕜] F
s : Set E
x₀ x : E
hu : Summable u
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n
hx₀ : x₀ ∈ s
hf0 : Summable fun x ↦ f x x₀
hx : x ∈ s
⊢ Summable fun n ↦ f n x

Tactic:
have := Classical.decEq α
  rw [summable_iff_cauchySeq_finset] at hf0 ⊢
  have A : UniformCauchySeqOn (fun t : Finset α => fun x => ∑ i ∈ t, f' i x) atTop s :=
    (tendstoUniformlyOn_tsum hu hf').uniformCauchySeqOn
  refine cauchy_map_of_uniformCauchySeqOn_fderiv (f := fun t x ↦ ∑ i ∈ t, f i x)
    hs h's A (fun t y hy => ?_) hx₀ hx hf0
  exact HasFDerivAt.fun_sum fun i _ => hf i y hy

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)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal * p.toReal) = ∑' (i : α), ‖↑f i‖ ^ p.toReal

Tactic:
field_simp

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ 1 = ∑' (i : α), ‖↑f i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)

Tactic:
rw [norm_rpow_eq_tsum hp]
  exact ((lp.memℓp f).summable hp).hasSum

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E 0)
h : ‖f‖ = 0
⊢ f = 0

pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
⊢ f = 0

pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ f = 0

Tactic:
· ext i
    have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using! h
    have : ¬¬f i = 0 := Set.eq_empty_iff_forall_notMem.mp this i
    tauto

Goal state after:
case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
h : ‖f‖ = 0
⊢ f = 0

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
h : ‖f‖ = 0
hp : 0 < p.toReal
⊢ f = 0
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' : UniformCauchySeqOnFilter f' l (𝓝 x)
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 𝕜
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _

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
hf' : UniformCauchySeqOnFilter f' l (𝓝 x)
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 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniformCauchySeqOnFilter f l (𝓝 x)
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case 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
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 𝕜 := ⋯
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := ⋯
⊢ TendstoUniformlyOnFilter (fun n z ↦ f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0 (l ×ˢ l) (𝓝 x)

Tactic:
rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢

Goal state after:
case 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
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' : ∀ ε > 0, ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (-f' n.1.1 n.2 + f' n.1.2 n.2) < ε
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x, dist (0 n.2) (f n.1.1 n.2 - f n.1.2 n.2 - (f n.1.1 x - f n.1.2 x)) < ε
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
f : (i : α) → E i
hf : Memℓp f 0
⊢ Memℓp (star f) 0

Tactic:
apply memℓp_zero
    simp [hf.finite_dsupport]

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

Goal state before:
pp: case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ∞
j : α
hij : i ≠ j
⊢ ‖Pi.single i x j‖ ≤ ‖x‖

Tactic:
rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]

Goal state after:
case top.refine_1.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this : Nonempty α
hp : 0 < ∞
j : α
hij : i ≠ j
⊢ 0 ≤ ‖x‖
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))⁻¹ = 1

Tactic:
field_simp

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
x✝ : x ∈ univ
⊢ 1 / √((|√(1 + ‖x‖ ^ 2)| ^ 2 - ‖x‖ ^ 2) / |√(1 + ‖x‖ ^ 2)| ^ 2) = √(1 + ‖x‖ ^ 2)
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
this : 0 < 1 - ‖y‖ ^ 2
⊢ (√(1 + (|√(1 - ‖y‖ ^ 2)|⁻¹ * ‖y‖) ^ 2))⁻¹ * (√(1 - ‖y‖ ^ 2))⁻¹ = 1

Tactic:
field_simp

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
this : 0 < 1 - ‖y‖ ^ 2
⊢ 1 = √((|√(1 - ‖y‖ ^ 2)| ^ 2 + ‖y‖ ^ 2) / |√(1 - ‖y‖ ^ 2)| ^ 2) * √(1 - ‖y‖ ^ 2)
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' : UniformCauchySeqOn f' l (Metric.ball x 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 𝕜
⊢ UniformCauchySeqOn f l (Metric.ball x r)

Tactic:
let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _

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' : UniformCauchySeqOn f' l (Metric.ball x 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 𝕜
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
⊢ UniformCauchySeqOn f l (Metric.ball x r)
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)
p q r : ℝ≥0∞
h : p ≤ q
x✝¹ x✝ : ↥(lp E p)
⊢ ⟨↑(x✝¹ + x✝), ⋯⟩ = ⟨↑x✝¹, ⋯⟩ + ⟨↑x✝, ⋯⟩

Tactic:
ext; rfl

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)
p q r : ℝ≥0∞
h : p ≤ q
x✝¹ : 𝕜
x✝ : ↥(lp E p)
⊢ ⟨↑(x✝¹ • x✝), ⋯⟩ = (RingHom.id 𝕜) x✝¹ • ⟨↑x✝, ⋯⟩

Tactic:
ext; rfl

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)
p q : ℝ≥0∞
h : p ≤ q
f : ↥(lp E p)
⊢ ↑((linearMapOfLE 𝕜 E h) f) = ↑f

Tactic:
ext; rfl

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)
p q : ℝ≥0∞
h : p ≤ q
⊢ (linearMapOfLE 𝕜 E h).toAddMonoidHom = AddSubgroup.inclusion ⋯

Tactic:
ext; rfl

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)
p q r : ℝ≥0∞
hpq : p ≤ q
hqr : q ≤ r
⊢ linearMapOfLE 𝕜 E hqr ∘ₗ linearMapOfLE 𝕜 E hpq = linearMapOfLE 𝕜 E ⋯

Tactic:
ext; rfl

Goal state after:
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
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε

Tactic:
have mvt :=
      Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
        (fun z hz => ((hf n.1 z hz).sub (hf n.2 z hz)).hasFDerivWithinAt) (fun z hz => (hn z hz).le)
        (convex_ball x r) (Metric.mem_ball_self hr) hy

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
ε : ℝ
hε : ε > 0
q : ℝ
hqpos : 0 < q
hq : q * r < ε
n : ι × ι
y : E
hy : y ∈ Metric.ball x r
hn : ∀ x_1 ∈ Metric.ball x r, ‖f' n.1 x_1 - f' n.2 x_1‖ < q
mvt : ‖(f n.1 - f n.2) y - (f n.1 - f n.2) x‖ ≤ q * ‖y - x‖
⊢ ‖f n.1 y - f n.2 y - (f n.1 x - f n.2 x)‖ < ε
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)
ι : Type u_5
l : Filter ι
inst✝¹ : l.NeBot
_i : Fact (1 ≤ p)
inst✝ : ∀ (a : α), CompleteSpace (E a)
⊢ ∀ (u : ℕ → ↥(lp E p)), CauchySeq u → ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
by
    intro F hF
    -- A Cauchy sequence in `lp E p` is pointwise convergent; let `f` be the pointwise limit.
    obtain ⟨f, hf⟩ := cauchySeq_tendsto_of_complete
      ((uniformContinuous_coe (p := p)).comp_cauchySeq hF)
    -- Since the Cauchy sequence is bounded, its pointwise limit `f` is in `lp E p`.
    have hf' : Memℓp f p := memℓp_of_tendsto hF.isBounded_range hf
    -- And therefore `f` is its limit in the `lp E p` topology as well as pointwise.
    exact ⟨⟨f, hf'⟩, tendsto_lp_of_tendsto_pi hF hf⟩

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case refine_2
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 E'
inst✝² : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹ : AddGroup G
inst✝ : TopologicalSpace G
C : ℝ
hC : ∀ (i : G), ‖g i‖ ≤ C
x t✝ : G
s u : Set G
hx : x ∈ s
hu : -tsupport g + s ⊆ u
t : G
ht : t ∉ u
⊢ ‖(L (f t)) (g (x - t))‖ ≤ 0

Tactic:
have : x - t ∉ support g := by
      refine mt (fun hxt => hu ?_) ht
      refine ⟨_, Set.neg_mem_neg.mpr (subset_closure hxt), _, hx, ?_⟩
      simp only [neg_sub, sub_add_cancel]
    simp only [notMem_support.mp this, (L _).map_zero, norm_zero, le_rfl]

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: case inr.h_diff
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : SFinite μ
inst✝ : μ.IsAddLeftInvariant
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : ContDiff 𝕜 1 g
x₀ : G
fin_dim : FiniteDimensional 𝕜 G
this : ProperSpace G
L' : E →L[𝕜] (G →L[𝕜] E') →L[𝕜] G →L[𝕜] F := ⋯
h1 : ∀ᶠ (x : G) in 𝓝 x₀, AEStronglyMeasurable (fun t ↦ (L (f t)) (g (x - t))) μ
h2 : ∀ (x : G), AEStronglyMeasurable (fun t ↦ (L' (f t)) (fderiv 𝕜 g (x - t))) μ
h3 : ∀ (x t : G), HasFDerivAt (fun x ↦ g (x - t)) (fderiv 𝕜 g (x - t)) x
K' : Set G := ⋯
hK' : IsCompact K'
⊢ ∀ᵐ (a : G) ∂μ, ∀ x ∈ ball x₀ 1, HasFDerivAt (fun x ↦ (L (f a)) (g (x - a))) ((L' (f a)) (fderiv 𝕜 g (x - a))) x

Tactic:
exact Eventually.of_forall fun t x _ => (L _).hasFDerivAt.comp x (h3 x t)

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
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
inst✝ : l.NeBot
hf'✝ : TendstoUniformly f' g' l
hf✝ : ∀ (n : ι) (x : E), HasFDerivAt (f n) (f' n x) x
hfg✝ : ∀ (x : E), Tendsto (fun n ↦ f n x) l (𝓝 (g x))
x : E
hf : ∀ (n : ι), ∀ x ∈ Set.univ, HasFDerivAt (f n) (f' n x) x
hfg : ∀ x ∈ Set.univ, Tendsto (fun n ↦ f n x) l (𝓝 (g x))
hf' : TendstoUniformlyOn f' g' l Set.univ
⊢ HasFDerivAt g (g' x) x

Tactic:
exact hasFDerivAt_of_tendstoUniformlyOn isOpen_univ hf' hf hfg (Set.mem_univ x)

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
⊢ LipschitzOnWith (Real.nnabs (bound a)) (fun x ↦ F x a) (ball x₀ ε)

Tactic:
refine (convex_ball _ _).lipschitzOnWith_of_nnnorm_hasDerivWithin_le
      (fun x x_in ↦ (ha_deriv x (hε x_in)).hasDerivWithinAt) fun x x_in ↦ ?_

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 E
bound : α → ℝ
F : 𝕜 → α → E
x₀ : 𝕜
s : Set 𝕜
hs : s ∈ 𝓝 x₀
hF_meas : ∀ᶠ (x : 𝕜) in 𝓝 x₀, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
F' : 𝕜 → α → E
hF'_meas : AEStronglyMeasurable (F' x₀) μ
h_bound : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, ‖F' x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
diff_x₀ : ∀ᵐ (a : α) ∂μ, HasDerivAt (fun x ↦ F x a) (F' x₀ a) x₀
a : α
ha_deriv : ∀ x ∈ s, HasDerivAt (fun x ↦ F x a) (F' x a) x
ha_bound : ∀ x ∈ s, ‖F' x a‖ ≤ bound a
x : 𝕜
x_in : x ∈ ball x₀ ε
⊢ ‖F' x a‖₊ ≤ Real.nnabs (bound a)
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : SecondCountableTopology X
B : Set (Set X)
hBc : B.Countable
hB : IsTopologicalBasis B
s : Set (Set X × Set X) := {UV | UV ∈ B ×ˢ B ∧ closure[inst✝²] UV.1 ⊆ UV.2}
this✝¹ : Encodable ↑s
this✝ : TopologicalSpace ↑s := ⊥
this : DiscreteTopology ↑s
hd : ∀ (UV : ↑s), Disjoint (closure[inst✝²] (↑UV).1) (↑UV).2ᶜ
ε : ↑s → ℝ
ε01 : ∀ (UV : ↑s), ε UV ∈ Ioc 0 1
hε : Tendsto ε cofinite (𝓝 0)
UV : ↑s
f : C(X, ℝ)
hf₀ : EqOn (⇑f) 0 (closure[inst✝²] (↑UV).1)
hf₁ : EqOn (⇑f) 1 (↑UV).2ᶜ
hf01 : ∀ (x : X), f x ∈ Icc 0 1
x : X
hx : x ∈ (↑UV).1
⊢ (ε UV • f) x = 0 x

Tactic:
by simp [hf₀ (subset_closure hx)]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁰ : CompleteSpace F
inst✝⁹ : AddGroup G
inst✝⁸ : SFinite μ
inst✝⁷ : SFinite ν
inst✝⁶ : μ.IsAddRightInvariant
inst✝⁵ : MeasurableAdd₂ G
inst✝⁴ : MeasurableNeg G
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ ∫ (x : G), (f ⋆[L, ν] g) x ∂μ = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)

Tactic:
refine (integral_integral_swap (by apply hf.convolution_integrand L hg)).trans ?_

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁹ : NormedAddCommGroup E
inst✝¹⁸ : NormedAddCommGroup E'
inst✝¹⁷ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedSpace 𝕜 E'
inst✝¹³ : NormedSpace ℝ F
inst✝¹² : NormedSpace 𝕜 F
inst✝¹¹ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁰ : CompleteSpace F
inst✝⁹ : AddGroup G
inst✝⁸ : SFinite μ
inst✝⁷ : SFinite ν
inst✝⁶ : μ.IsAddRightInvariant
inst✝⁵ : MeasurableAdd₂ G
inst✝⁴ : MeasurableNeg G
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
hf : Integrable f ν
hg : Integrable g μ
⊢ ∫ (y : G), ∫ (x : G), (L (f y)) (g (x - y)) ∂μ ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
K : Set G
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
⊢ r < μ K → ∃ K_1 ⊆ K, (fun s ↦ ∃ f, Continuous[inst✝⁷, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧ r < μ K_1

Tactic:
hr

Goal state after:
G : Type u_2
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : LocallyCompactSpace G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
K : Set G
K_comp : IsCompact K
K_closed : IsClosed[inst✝⁷] K
r : ℝ≥0∞
hr : r < μ K
⊢ ∃ K_1 ⊆ K, (fun s ↦ ∃ f, Continuous[inst✝⁷, _] f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) K_1 ∧ r < μ K_1