mathlib-initiative/mathlib-tactics huggingface dataset:
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 j : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.faceOppositeCentroid j = (↑n)⁻¹ • (s.points j -ᵥ s.points i)

Tactic:
by
  rw [faceOppositeCentroid_eq_sum_vsub_vadd s i, faceOppositeCentroid_eq_sum_vsub_vadd s j,
    vadd_vsub_vadd_comm _ _ (s.points i) (s.points j)]
  have h1 (i : Fin (n + 1)) : ∑ x, (s.points x -ᵥ s.points i) =
      ∑ x, (s.points x -ᵥ s.points 0 - (s.points i -ᵥ s.points 0)) := by
    apply sum_congr rfl
    simp
  simp_rw [h1 i, h1 j, sum_sub_distrib]
  rw [smul_sub, smul_sub, sub_sub_sub_cancel_left, ← smul_sub, ← sum_sub_distrib,
    vsub_sub_vsub_cancel_right, sum_const, card_univ, Fintype.card_fin]
  have : (s.points i -ᵥ s.points j) = -(s.points j -ᵥ s.points i) := by simp
  rw [this, ← sub_eq_add_neg, add_smul, sub_eq_iff_eq_add, one_smul, smul_add, add_comm]
  have : (n : k)⁻¹ • n • (s.points j -ᵥ s.points i) =
      (n : k)⁻¹ • (n : k) • (s.points j -ᵥ s.points i) := by
    norm_cast0
    congr 1
  rw [this, smul_smul, inv_eq_one_div, one_div_mul_cancel (NeZero.ne (n : k)), one_smul]

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)
⊢ -((↑n + 1) • (s.faceOppositeCentroid i -ᵥ s.centroid)) = (↑n + 1) • (s.centroid -ᵥ s.faceOppositeCentroid i)

Tactic:
← neg_smul,

Goal state after:
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)
⊢ -(↑n + 1) • (s.faceOppositeCentroid i -ᵥ s.centroid) = (↑n + 1) • (s.centroid -ᵥ s.faceOppositeCentroid i)
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)
⊢ -(-↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)) = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)

Tactic:
← neg_smul,

Goal state after:
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)
⊢ - -↑n • (s.faceOppositeCentroid i -ᵥ s.centroid) = ↑n • (s.faceOppositeCentroid i -ᵥ s.centroid)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr.inr.inr.inr.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i ↦ ‖f i‖ ^ q.toReal
⊢ {x | (fun i ↦ ‖‖f i‖ ^ p.toReal‖ ≤ ‖f i‖ ^ q.toReal) x}ᶜ ⊆ {i | 1 ≤ ‖f i‖}

Tactic:
change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
      intro i hi
      have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
      simp only [abs_of_nonneg, this] at hi
      contrapose! hi
      exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

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
k : ℕ
hk : ↑k ≤ N
⊢ (iteratedFDeriv 𝕜 k fun y ↦ ∑' (n : α), f n y) = fun x ↦ ∑' (n : α), iteratedFDeriv 𝕜 k (f n) x

Tactic:
induction k with

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:
eventually_all_finset

Goal state after:
α : 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 ∈ Finset.range (m + 1), ∀ᶠ (x : α) in cofinite, ∀ (x_1 : E), ‖iteratedFDeriv 𝕜 i (f x) x_1‖ ≤ v i 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)
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 ∞)
i : I
⊢ ‖↑f i‖ ≤ √‖star f * f‖

Tactic:
rw [Real.le_sqrt (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self]

Goal state after:
𝕜 : 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 ∞)
i : I
⊢ ‖star (↑f i) * ↑f i‖ ≤ ‖star f * f‖
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x : E
hx₀ : x₀ ∈ s
hx : x ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t ∩ s ⊆ t

Tactic:
rintro x ⟨xt, xs⟩

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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : IsPreconnected s
hf' : UniformCauchySeqOn f' l s
hf : ∀ (n : ι), ∀ y ∈ s, HasFDerivAt (f n) (f' n y) y
x₀ x✝ : E
hx₀ : x₀ ∈ s
hx : x✝ ∈ s
hfg : Cauchy (map (fun n ↦ f n x₀) l)
this : l.NeBot
t : Set E := {y | y ∈ s ∧ Cauchy (map (fun n ↦ f n y) l)}
A : ∀ (x : E) (ε : ℝ), x ∈ t → Metric.ball x ε ⊆ s → Metric.ball x ε ⊆ t
open_t : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
st_nonempty : (s ∩ t).Nonempty
x : E
xt : x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
xs : x ∈ s
⊢ x ∈ t
Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition

Goal state before:
pp: ⊢ ¬AnalyticAt ℝ expNegInvGlue 0

Tactic:
intro h
  obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
  suffices expNegInvGlue (r / 2) = 0 by simpa [hr, not_le_of_gt]
  exact h.eqOn_zero_of_preconnected_of_mem_closure (z₀ := 0)
    (Real.ball_eq_Ioo 0 r ▸ isPreconnected_Ioo)
    (by simp [hr]) (by simp [Set.Iic_def]) (by simp [abs_of_pos, hr])

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
⊢ ContinuousOn (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
apply (continuousOn_const (c := 0)).congr

Goal state after:
case pos
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : AddGroup G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalAddGroup G
inst✝¹ : BorelSpace G
inst✝ : TopologicalSpace P
g : P → G → E'
s : Set P
k : Set G
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContinuousOn (↿g) (s ×ˢ univ)
H : ∀ p ∈ s, ∀ (x : G), g p x = 0
⊢ EqOn (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (fun x ↦ 0) (s ×ˢ univ)
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case refine_2
ι : 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
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝¹ : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)))
        0 <
      ε

Tactic:
have := hn.self_of_nhds

Goal state after:
case refine_2
ι : 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
x : E
inst✝ : l.NeBot
hf' : TendstoUniformlyOnFilter f' g' l (𝓝 x)
hf : ∀ᶠ (n : ι × E) in l ×ˢ 𝓝 x, HasFDerivAt (f n.1) (f' n.1 n.2) n.2
hfg : ∀ᶠ (y : E) in 𝓝 x, Tendsto (fun n ↦ f n y) l (𝓝 (g y))
this✝² : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
this✝¹ :
  (fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (g' x) (a.2 - x))) =
    ((fun a ↦ (↑‖a.2 - x‖)⁻¹ • (g a.2 - g x - (f a.1 a.2 - f a.1 x))) + fun a ↦
        (↑‖a.2 - x‖)⁻¹ • (f a.1 a.2 - f a.1 x - ((f' a.1 x) a.2 - (f' a.1 x) x))) +
      fun a ↦ (↑‖a.2 - x‖)⁻¹ • (f' a.1 x - g' x) (a.2 - x)
this✝ : 𝓝 0 = 𝓝 (0 + 0 + 0)
ε : ℝ
hε : ε > 0
n : ι
hn : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt (f (n, y).1) (f' (n, y).1 (n, y).2) (n, y).2
this : HasFDerivAt (f (n, x).1) (f' (n, x).1 (n, x).2) (n, x).2
⊢ ∀ᶠ (y : E) in 𝓝 x,
    dist ((↑‖(n, y).2 - x‖)⁻¹ • (f (n, y).1 (n, y).2 - f (n, y).1 x - ((f' (n, y).1 x) (n, y).2 - (f' (n, y).1 x) x)))
        0 <
      ε
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
ε : ℝ
εpos : 0 < ε
hε : thickening ε ({q₀.1} ×ˢ k) ⊆ t
⊢ ∃ ε, 0 < ε ∧ thickening ε ({q₀.1} ×ˢ k) ⊆ t ∧ ball q₀.1 ε ⊆ s

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ, 0 < δ ∧ ball q₀.1 δ ⊆ s := Metric.isOpen_iff.1 hs _ hq₀

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
f : G → E
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 1 (↿g) (s ×ˢ univ)
q₀ : P × G
hq₀ : q₀.1 ∈ s
g' : P × G → P × G →L[𝕜] E' := fderiv 𝕜 ↿g
A✝ :
  ∀ p ∈ s,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
      (g p)
A' : ∀ (q : P × G), q.1 ∈ s → s ×ˢ univ ∈ 𝓝 q
g'_zero : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g' (p, x) = 0
A : IsCompact ({q₀.1} ×ˢ k)
t : Set (P × G)
kt : {q₀.1} ×ˢ k ⊆ t
t_open : IsOpen[instTopologicalSpaceProd] t
ht : Bornology.IsBounded (g' '' t)
ε : ℝ
εpos : 0 < ε
hε : thickening ε ({q₀.1} ×ˢ k) ⊆ t
δ : ℝ
δpos : 0 < δ
hδ : ball q₀.1 δ ⊆ s
⊢ ∃ ε, 0 < ε ∧ thickening ε ({q₀.1} ×ˢ k) ⊆ t ∧ ball q₀.1 ε ⊆ s
Module: Mathlib.MeasureTheory.Measure.Haar.NormedSpace

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
R : ℝ
s : Set E
hR : R ≠ 0
e : E ≃ᵐ E := (Homeomorph.smul (Units.mk0 R hR)).toMeasurableEquiv
⊢ ∫ (x : E) in s, f (R • x) ∂μ = ∫ (x : E) in ⇑e ⁻¹' ⇑e.symm ⁻¹' s, f (e x) ∂μ

Tactic:
by simp [← preimage_comp]; rfl

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✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
⊢ ∫ (x : G), ‖L (f x)‖ * ε ∂μ ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
rw [integral_mul_const]

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✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁶ : MeasurableSpace G
μ : Measure G
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : SecondCountableTopology G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : SFinite μ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hif : Integrable f μ
hf : support f ⊆ ball 0 R
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hfg : ConvolutionExistsAt f g x₀ L μ
h2 : ∀ (t : G), ‖(L (f t)) (g (x₀ - t)) - (L (f t)) z₀‖ ≤ ‖L (f t)‖ * ε
⊢ (∫ (a : G), ‖L (f a)‖ ∂μ) * ε ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: case hnhds
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s k : Set α
hk : IsCompact k
h'k : k ⊆ s \ μ.everywherePosSubset s
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, μ t = 0

Tactic:
· intro x hx
    obtain ⟨u, ux, hu⟩ : ∃ u ∈ 𝓝[s] x, μ u = 0 := by
      simpa [everywherePosSubset, (h'k hx).1] using (h'k hx).2
    exact ⟨u, nhdsWithin_mono x (h'k.trans sdiff_subset) ux, hu⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : p.c (p.index y) ∉ p.iUnionUpTo y
⊢ x = y

Tactic:
simp only [iUnionUpTo, not_exists, exists_prop, mem_iUnion, not_and,
    Subtype.exists] at A

Goal state after:
case inr
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x y : Ordinal.{u}
hxy : p.index x = p.index y
x_le_y : x ≤ y
H : x < y
h : ∃ x, p.c x ∉ p.iUnionUpTo y ∧ p.R y ≤ p.τ * p.r x
A : ∀ x < y, p.c (p.index y) ∉ ball (p.c (p.index x)) (p.r (p.index x))
⊢ x = y
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ (range fun b ↦ p.r ↑b).Nonempty

Tactic:
rw [← image_univ, image_nonempty]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : MetricSpace α
β : Type u
inst✝ : Nonempty β
p : TauPackage β α
x : β
A : ∀ (z : β), p.c z ∈ p.iUnionUpTo p.lastStep ∨ p.τ * p.r z < p.R p.lastStep
h : ¬p.c x ∈ p.iUnionUpTo p.lastStep
H : p.τ * p.r x < p.R p.lastStep
Rpos : 0 < p.R p.lastStep
B : p.τ⁻¹ * p.R p.lastStep < p.R p.lastStep
⊢ univ.Nonempty
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 ℕ :=
  ⋃ 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
n : ℕ
hn : n ≤ N
⊢ p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))

Tactic:
have :
      p.index (G n) =
        Classical.epsilon fun t => p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t := by
      rw [index]; rfl

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
n : ℕ
hn : n ≤ N
this : p.index (G n) = Classical.epsilon fun t ↦ p.c t ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r t
⊢ p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case refine_3.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ∀ x ∈ Ioo 0 1 ×ˢ univ, x.1 ≠ 0

Tactic:
intro x hx; exact ne_of_gt hx.1.1

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Finset E
hs : ∀ c ∈ s, ‖c‖ ≤ 2
h : ∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 ≤ ‖c - d‖
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
μ : Measure E := Measure.addHaar
δ : ℝ := 1 / 2
ρ : ℝ := 5 / 2
ρpos : 0 < ρ
A : Set E := ⋃ c ∈ s, ball c δ
hA : A = ⋃ c ∈ s, ball c δ
D : (↑s).Pairwise (Disjoint on fun c ↦ ball c δ)
x : E
hx : x ∈ s
⊢ δ + 2 = 5 / 2

Tactic:
by norm_num

Goal state after: