mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Covering.Quotient

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
⊢ IsCoveringMapOn f (f '' {e | MulAction.stabilizer G e = ⊥})

Tactic:
let : TopologicalSpace G := ⊥; have : DiscreteTopology G := ⟨rfl⟩
  suffices ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t : Trivialization G f, x ∈ t.baseSet by
    choose t ht using this; exact IsCoveringMapOn.mk _ _ _ _ fun x ↦ ht x x.2
  rintro x ⟨e, he, rfl⟩
  have ⟨U, heU, hU⟩ := disjoint e
  refine ⟨hf.trivializationOfSMulDisjoint hfG (interior U) isOpen_interior
    fun g hg ↦ ?_, e, mem_interior_iff_mem_nhds.mpr heU, rfl⟩
  rw [← Subgroup.mem_bot, ← he]
  exact hU _ (hg.mono (by grw [interior_subset]))

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
δ : ℝ
hδ₀ : 0 < δ
hδ₂ : δ < 2
⊢ IsPathConnected (ball u δ)

Tactic:
suffices IsPathConnected (ball (1 : unitary A) δ) by
    convert! this |>.image (f := (u * ·)) (by fun_prop)
    ext v
    rw [← inv_mul_cancel u]
    simp [-inv_mul_cancel, Subtype.dist_eq, dist_eq_norm, ← mul_sub]
  refine ⟨1, by simpa, fun {u} hu ↦ ?_⟩
  have hu : ‖(u - 1 : A)‖ < δ := by simpa [Subtype.dist_eq, dist_eq_norm] using hu
  refine ⟨path 1 u (hu.trans hδ₂), fun t ↦ ?_⟩
  simpa [Subtype.dist_eq, dist_eq_norm] using
    norm_expUnitary_smul_argSelfAdjoint_sub_one_le u t.2 (hu.trans hδ₂) |>.trans_lt hu

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mp
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : p = s.centroid
⊢ ∑ i, (s.points i -ᵥ s.centroid) = 0

Tactic:
centroid_weighted_vsub_eq_zero

Goal state after:
case mp
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : p = s.centroid
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: case mpr
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : ∑ x, (s.points x -ᵥ s.centroid) - ∑ x, (p -ᵥ s.centroid) = 0
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
⊢ p -ᵥ s.centroid = 0

Tactic:
centroid_weighted_vsub_eq_zero

Goal state after:
case mpr
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
n : ℕ
inst✝ : CharZero k
s : Simplex k P n
p : P
h : 0 - ∑ x, (p -ᵥ s.centroid) = 0
this : ∑ i, (s.points i -ᵥ p) = ∑ i, (s.points i -ᵥ s.centroid - (p -ᵥ s.centroid))
⊢ p -ᵥ s.centroid = 0
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑((fun p ↦ p -ᵥ p₁) '' ↑((Finset.image p s).erase p₁))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n

Tactic:
← Finset.coe_image

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : DecidableEq P
p : ι → P
hi : AffineIndependent k p
s : Finset ι
n : ℕ
hc : #s = n + 1
hc' : #(Finset.image p s) = n + 1
p₁ : P
hi' : LinearIndependent k fun (v : ↑↑(Finset.image (fun p ↦ p -ᵥ p₁) ((Finset.image p s).erase p₁))) ↦ ↑v
hp₁ : p₁ ∈ Finset.image p s
hp₁' : p₁ ∈ p '' ↑s
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k (p '' ↑Finset.univ)) = n

Tactic:
← Finset.coe_image

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) = n
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (p '' ↑Finset.univ)) ≤ n

Tactic:
← Finset.coe_image

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) ≤ n
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.points i -ᵥ s.faceOppositeCentroid i = (↑n + 1) • (s.centroid -ᵥ s.faceOppositeCentroid i)

Tactic:
rw [← neg_vsub_eq_vsub_rev, faceOppositeCentroid_vsub_point_eq_smul_vsub, ← neg_smul,
    ← neg_smul_neg, neg_vsub_eq_vsub_rev, neg_neg]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ AffineIndependent k p ↔ n ≤ finrank k ↥(vectorSpan k (Set.range p))

Tactic:
rw [affineIndependent_iff_finrank_vectorSpan_eq k p hc]
  constructor
  · rintro rfl
    rfl
  · exact fun hle => le_antisymm (finrank_vectorSpan_range_le k p hc) hle

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

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
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.centroid -ᵥ s.faceOppositeCentroid i = (↑n)⁻¹ • (s.points i -ᵥ s.centroid)

Tactic:
by
  rw [point_vsub_centroid_eq_smul_vsub, smul_smul, inv_mul_cancel₀ (NeZero.ne (n : k)), one_smul]

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

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k (p '' ↑Finset.univ) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k (p '' ↑Finset.univ) = sp

Tactic:
← Finset.coe_image

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : Fintype ι
p : ι → P
hi : AffineIndependent k p
sp : AffineSubspace k P
inst✝ : FiniteDimensional k ↥sp.direction
hle : affineSpan k ↑(Finset.image p Finset.univ) ≤ sp
hc : #Finset.univ = finrank k ↥sp.direction + 1
⊢ affineSpan k ↑(Finset.image p Finset.univ) = sp
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case h
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
p₁ p₂ p : P
hp : p ∈ {p₁, p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁

Tactic:
Set.mem_insert_iff,

Goal state after:
case h
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
p₁ p₂ p : P
hp : p = p₁ ∨ p ∈ {p₂}
⊢ ∃ r, p = r • (p₂ -ᵥ p₁) +ᵥ p₁
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: case refine_1
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ Ioi 1 ×ˢ univ ∈ 𝓝 ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))

pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x

Tactic:
· exact prod_mem_nhds (Ioi_mem_nhds (f x).one_lt_rOut_div_rIn) univ_mem

Goal state after:
case refine_2
E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
s : Set X
f : (x : X) → ContDiffBump (c x)
x : X
hc : ContDiffWithinAt ℝ (↑n) c s x
hr : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rIn) s x
hR : ContDiffWithinAt ℝ (↑n) (fun x ↦ (f x).rOut) s x
hg : ContDiffWithinAt ℝ (↑n) g s x
⊢ ContDiffWithinAt ℝ (↑n) (fun x ↦ ((f x).rOut / (f x).rIn, (f x).rIn⁻¹ • (g x - c x))) s x
Module: Mathlib.MeasureTheory.Group.Integral

Goal state before:
pp: G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
hf' : ∀ (x : G), f (x * g) = -f x
this : IsAddTorsionFree E
⊢ ∫ (x : G), f x ∂μ = ∫ (a : G), f (a * g) ∂μ

Tactic:
integral_mul_right_eq_self

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

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

Tactic:
lp.norm_eq_tsum_rpow hp f

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ 0 ≤ (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: case succ
α : 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
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘
      fderiv 𝕜 fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x) =
    fun x ↦
    ∑' (n : α), (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x

Tactic:
fderiv_tsum (hv _ hk) (fun n => (hf n).differentiable_iteratedFDeriv
        (mod_cast h'k)) _ A

Goal state after:
case succ
α : 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
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fun x ↦
      ∑' (n : α), fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 k (f n) x) x) =
    fun x ↦
    ∑' (n : α), (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x ↦ E) F).symm ∘ fderiv 𝕜 (iteratedFDeriv 𝕜 k (f n))) x

α : 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
k : ℕ
IH : ↑k ≤ N → (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x
hk : ↑(k + 1) ≤ N
h'k : ↑k < N
A : Summable fun n ↦ iteratedFDeriv 𝕜 k (f n) 0
⊢ ∀ (n : α) (x : E), ‖fderiv 𝕜 (fun x ↦ iteratedFDeriv 𝕜 k (f n) x) x‖ ≤ v (k + 1) n
Module: Mathlib.Analysis.SpecialFunctions.Sqrt

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

Tactic:
· have : ↑2 * √x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
    constructor
    · simpa using! sqPartialHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)
    · exact fun n => sqPartialHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (√x))
        (contDiffAt_id.pow 2)

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
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_contDiffOn_iff, contDiffOn_pi]
  rfl

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)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ∞)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

Tactic:
apply norm_le_of_forall_le hC

Goal state after:
case inl
α : Type u_3
E : α → Type u_4
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ∞)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ ↑n fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
apply contDiff_all_iff_nat.2 (fun m => ?_) n
  induction m generalizing p with
  | zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
  | succ m ihm =>
    rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
    refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
    convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
    exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv

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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
⊢ HasFDerivAt (fun x ↦ ∫ (a : α), F x a ∂μ) (∫ (a : α), F' a ∂μ) x₀

Tactic:
rw [hasFDerivAt_iff_tendsto, tendsto_congr' this, ← tendsto_zero_iff_norm_tendsto_zero, ←
    show (∫ a : α, ‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ) = 0 by simp]

Goal state after:
case pos
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
H : Type u_4
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
F : H → α → E
x₀ : H
bound : α → ℝ
s : Set H
F' : α → H →L[𝕜] E
hs : s ∈ 𝓝 x₀
hF_meas : ∀ x ∈ s, AEStronglyMeasurable (F x) μ
hF_int : Integrable (F x₀) μ
hF'_meas : AEStronglyMeasurable F' μ
bound_integrable : Integrable bound μ
h_diff : ∀ᵐ (a : α) ∂μ, HasFDerivAt (fun x ↦ F x a) (F' a) x₀
ε : ℝ
ε_pos : ε > 0
hε : ball x₀ ε ⊆ s
x₀_in : x₀ ∈ ball x₀ ε
nneg : ∀ (x : H), 0 ≤ ‖x - x₀‖⁻¹
b : α → ℝ := fun a ↦ |bound a|
b_int : Integrable b μ
b_nonneg : ∀ (a : α), 0 ≤ b a
h_lipsch : ∀ᵐ (a : α) ∂μ, ∀ x ∈ ball x₀ ε, ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
hF_int' : ∀ x ∈ ball x₀ ε, Integrable (F x) μ
hF'_int : Integrable F' μ
hE : CompleteSpace E
h_ball : ball x₀ ε ∈ 𝓝 x₀
this :
  ∀ᶠ (x : H) in 𝓝 x₀,
    ‖x - x₀‖⁻¹ * ‖∫ (a : α), F x a ∂μ - ∫ (a : α), F x₀ a ∂μ - (∫ (a : α), F' a ∂μ) (x - x₀)‖ =
      ‖∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ‖
⊢ Tendsto (fun x ↦ ∫ (a : α), ‖x - x₀‖⁻¹ • (F x a - F x₀ a - (F' a) (x - x₀)) ∂μ) (𝓝 x₀)
    (𝓝 (∫ (a : α), ‖x₀ - x₀‖⁻¹ • (F x₀ a - F x₀ a - (F' a) (x₀ - x₀)) ∂μ))
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
g : G → E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : ∫ (x : G), f x ∂μ = 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
⊢ dist ((f ⋆[lsmul ℝ ℝ, μ] g) x₀) z₀ ≤ ε

Tactic:
have hif : Integrable f μ := integrable_of_integral_eq_one hintf
  convert! (dist_convolution_le' (lsmul ℝ ℝ) hε hif hf hmg hg).trans _
  · simp_rw [lsmul_apply, integral_smul_const, hintf, one_smul]
  · simp_rw [Real.norm_of_nonneg (hnf _), hintf, mul_one]
    exact (mul_le_mul_of_nonneg_right opNorm_lsmul_le hε).trans_eq (one_mul ε)

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ (range fun x ↦ 0) ⊆ Icc 0 1

Tactic:
by
        simp only [range_const, singleton_subset_iff, left_mem_Icc, zero_le_one]

Goal state after:
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case inr.refine_1.h₂
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := ⋯
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := ⋯
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : ℕ → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr : ∀ (n i : ℕ), i ≤ n → ∀ (x : E), ‖iteratedFDeriv ℝ i (r n • g n) x‖ ≤ ↑(δ n)
S : ∀ (x : E), Summable fun n ↦ (r n • g n) x
⊢ s ⊆ support fun x ↦ ∑' (n : ℕ), (r n • g n) x

Tactic:
intro x hx
      obtain ⟨n, hn⟩ : ∃ n, x ∈ support (g n) := s_g x hx
      have I : 0 < r n * g n x := mul_pos (rpos n) (lt_of_le_of_ne (g_nonneg n x) (Ne.symm hn))
      exact ne_of_gt ((S x).tsum_pos (fun i => mul_nonneg (rpos i).le (g_nonneg i x)) n I)

Goal state after:
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ := ⋯
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := ⋯
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
⊢ p.r (p.index (G ↑b)) ≤ p.R (G ↑a)

Tactic:
have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by
        intro H; exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
N : ℕ
hN : IsEmpty (SatelliteConfig α N p.τ)
i : Ordinal.{u}
IH : ∀ y < i, y < p.lastStep → p.color y < N
hi : i < p.lastStep
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty),
      {p.color ↑j}
color_i : p.color i = sInf (univ \ A)
N_mem : N ∈ univ \ A
Inf_eq_N : sInf (univ \ A) = N
g : ℕ → Ordinal.{u}
hg :
  ∀ k < N,
    g k < i ∧
      (closedBall (p.c (p.index (g k))) (p.r (p.index (g k))) ∩
            closedBall (p.c (p.index i)) (p.r (p.index i))).Nonempty ∧
        k = p.color (g k)
G : ℕ → Ordinal.{u} := fun n ↦ if n = N then i else g n
color_G : ∀ n ≤ N, p.color (G n) = n
G_lt_last : ∀ n ≤ N, G n < p.lastStep
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
a b : Fin N.succ
G_lt : G ↑a < G ↑b
ha : ↑a ≤ N
hb : ↑b ≤ N
B : p.c (p.index (G ↑b)) ∉ p.iUnionUpTo (G ↑a)
⊢ p.r (p.index (G ↑b)) ≤ p.R (G ↑a)