mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
p : P
hp : p ∈ s
⊢ ∃ a, a • v = p -ᵥ p₀

Tactic:
rcases hp₀v p hp with ⟨r, rfl⟩

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
s : Set P
p₀ : P
h : p₀ ∈ s
v : V
hp₀v : ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀
w : V
hw : w ∈ vectorSpan k s
r : k
hp : r • v +ᵥ p₀ ∈ s
⊢ ∃ a, a • v = (r • v +ᵥ p₀) -ᵥ p₀
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ tsupport ↑f = closedBall c f.rOut

Tactic:
simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']

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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) = 0

Tactic:
← finrank_bot k V

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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) = finrank k ↥⊥
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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
⊢ finrank k ↥(vectorSpan k (insert p ∅)) = finrank k ↥⊥

Tactic:
convert! rfl

Goal state after:
case e'_3.e'_2
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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
x✝ : V
⊢ ⊥ = vectorSpan k (insert p ∅)

case e'_3.e'_4.e'_6
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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
e_2✝ : ↥⊥ = ↥(vectorSpan k (insert p ∅))
e_3✝ : DivisionRing.toDivisionSemiring.toSemiring = inst✝³.toSemiring
e_5✝ : inst✝¹ ≍ inst✝¹
⊢ ⊥ = vectorSpan k (insert p ∅)

case e'_3.e'_5.e'_6
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
s : AffineSubspace k P
p : P
hf : FiniteDimensional k ↥s.direction
hs : s = ⊥
e_2✝ : ↥⊥ = ↥(vectorSpan k (insert p ∅))
e_4✝ : ⊥.addCommMonoid ≍ (vectorSpan k (insert p ∅)).addCommMonoid
e_3✝ : DivisionRing.toDivisionSemiring.toSemiring = inst✝³.toSemiring
e_5✝ : inst✝¹ ≍ inst✝¹
⊢ ⊥ = vectorSpan k (insert p ∅)
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (fun x ↦ ‖f x‖) p ↔ Memℓp f p

Tactic:
by
  obtain (rfl | rfl | hp) := p.trichotomy
  · simp [memℓp_zero_iff]
  · simp [memℓp_infty_iff]
  · simp [memℓp_gen_iff hp]

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
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 n ↦ f n x₀
hx : x ∈ s
⊢ ∀ x ∈ s, Tendsto (fun t ↦ ∑ n ∈ t, f n x) atTop (𝓝 (∑' (n : α), f n x))

Tactic:
intro y

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
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 n ↦ f n x₀
hx : x ∈ s
y : E
⊢ y ∈ s → Tendsto (fun t ↦ ∑ n ∈ t, f n y) atTop (𝓝 (∑' (n : α), f n y))
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)
h : ‖f‖ = 0
hp : 0 < p.toReal
hf : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0

Tactic:
rw [hasSum_zero_iff_of_nonneg this] at hf

Goal state after:
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
hf : (fun i ↦ ‖↑f i‖ ^ p.toReal) = 0
this : ∀ (i : α), 0 ≤ ‖↑f i‖ ^ p.toReal
⊢ f = 0
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
⊢ (deriv fun y ↦ ∑' (n : α), g n y) = fun y ↦ ∑' (n : α), deriv (g n) y

Tactic:
ext1 x
  exact deriv_tsum_apply hu hg hg' hg0 x

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:
refine contDiff_iff_forall_nat_le.2 fun m hm => ?_

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
⊢ ContDiff 𝕜 ↑m fun x ↦ ∑' (i : α), f i x
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)
⊢ UniformCauchySeqOnFilter f l (𝓝 x)

Tactic:
let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
  rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hf' ⊢
  suffices
    TendstoUniformlyOnFilter (fun (n : ι × ι) (z : E) => f n.1 z - f n.2 z - (f n.1 x - f n.2 x)) 0
        (l ×ˢ l) (𝓝 x) ∧
      TendstoUniformlyOnFilter (fun (n : ι × ι) (_ : E) => f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x) by
    have := this.1.neg.add this.2.neg
    rw [neg_zero, add_zero] at this
    apply this.congr (.of_forall (fun x ↦ by simp; abel))
  constructor
  · -- This inequality follows from the mean value theorem. To apply it, we will need to shrink our
    -- neighborhood to small enough ball
    rw [Metric.tendstoUniformlyOnFilter_iff] at hf' ⊢
    intro ε hε
    have := (tendsto_swap4_prod.eventually (hf.prod_mk hf)).diag_of_prod_right
    obtain ⟨a, b, c, d, e⟩ := eventually_prod_iff.1 ((hf' ε hε).and this)
    obtain ⟨R, hR, hR'⟩ := Metric.nhds_basis_ball.eventually_iff.mp d
    let r := min 1 R
    have hr : 0 < r := by simp [r, hR]
    have hr' : ∀ ⦃y : E⦄, y ∈ Metric.ball x r → c y := fun y hy =>
      hR' (lt_of_lt_of_le (Metric.mem_ball.mp hy) (min_le_right _ _))
    have hxy : ∀ y : E, y ∈ Metric.ball x r → ‖y - x‖ < 1 := by
      intro y hy
      rw [Metric.mem_ball, dist_eq_norm] at hy
      exact lt_of_lt_of_le hy (min_le_left _ _)
    have hxyε : ∀ y : E, y ∈ Metric.ball x r → ε * ‖y - x‖ < ε := by
      intro y hy
      exact (mul_lt_iff_lt_one_right hε.lt).mpr (hxy y hy)
    -- With a small ball in hand, apply the mean value theorem
    refine
      eventually_prod_iff.mpr
        ⟨_, b, (· ∈ Metric.ball x r),
          eventually_mem_set.mpr (Metric.nhds_basis_ball.mem_of_mem hr), fun {n} hn {y} hy => ?_⟩
    simp only [Pi.zero_apply, dist_zero_left, norm_neg_add] at e ⊢
    refine lt_of_le_of_lt ?_ (hxyε y hy)
    exact
      Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le
        (fun y hy => ((e hn (hr' hy)).2.1.sub (e hn (hr' hy)).2.2).hasFDerivWithinAt)
        (fun y hy => (e hn (hr' hy)).1.le) (convex_ball x r) (Metric.mem_ball_self hr) hy
  · -- This is just `hfg` run through `eventually_prod_iff`
    refine Metric.tendstoUniformlyOnFilter_iff.mpr fun ε hε => ?_
    obtain ⟨t, ht, ht'⟩ := (Metric.cauchy_iff.mp hfg).2 ε hε
    exact
      eventually_prod_iff.mpr
        ⟨fun n : ι × ι => f n.1 x ∈ t ∧ f n.2 x ∈ t,
          eventually_prod_iff.mpr ⟨_, ht, _, ht, fun {n} hn {n'} hn' => ⟨hn, hn'⟩⟩,
          fun _ => True,
          by simp,
          fun {n} hn {y} _ => by simpa [norm_sub_rev, dist_eq_norm] using ht' _ hn.1 _ hn.2⟩

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
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 := ⋯
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
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist y x ≤ ε

Tactic:
rw [dist_comm]

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
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ s
y : E
yt : y ∈ t
hxy : dist x y < ε / 2
⊢ ε / 2 + dist x y ≤ ε
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
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))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : UniformCauchySeqOnFilter f' l (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε

Tactic:
rw [SeminormedAddGroup.uniformCauchySeqOnFilter_iff_tendstoUniformlyOnFilter_zero] at hfg'

Goal state after:
ι : Type u_1
l : Filter ι
E : Type u_5
inst✝⁴ : NormedAddCommGroup E
𝕜 : Type u_6
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
x : E
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))
A : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
hfg' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
⊢ ∀ ε > 0,
    ∀ᶠ (n : (ι × ι) × E) in (l ×ˢ l) ×ˢ 𝓝 x,
      dist (0 n.2) (-((↑‖n.2 - x‖)⁻¹ • (f n.1.1 n.2 - f n.1.1 x)) + (↑‖n.2 - x‖)⁻¹ • (f n.1.2 n.2 - f n.1.2 x)) < ε
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case inr
𝕜 : 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)
p : P
hp : p ∈ s
x : G
hx : g p x ≠ 0
A : support (g p) ⊆ k
B : Continuous[inst✝³, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (g p)
H : LocallyCompactSpace G
⊢ LocallyCompactSpace G

Tactic:
· exact H

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
⊢ w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}

Tactic:
intro y

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
x : α
n : Set α
ns : n ∈ 𝓝[s] x
hx : μ n = 0
v : Set α
vx : v ∈ 𝓝 x
hv : v ∩ s ⊆ n
w : Set α
wv : w ⊆ v
w_open : IsOpen[inst✝¹] w
xw : x ∈ w
y : α
⊢ y ∈ w → y ∈ {x | ∃ n ∈ 𝓝[s] x, μ n = 0}
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegular
hs : MeasurableSet s
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Tactic:
exact measure_eq_zero_of_subset_sdiff_everywherePosSubset h'k hk

Goal state after:
Module: Mathlib.MeasureTheory.Measure.EverywherePos

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : OpensMeasurableSpace α
inst✝ : μ.InnerRegularCompactLTTop
hs : MeasurableSet s
h's : μ s ≠ ∞
A : μ (s \ μ.everywherePosSubset s) ≠ ∞
k : Set α
hk : k ⊆ s \ μ.everywherePosSubset s
h'k : IsCompact k
⊢ μ k = 0

Tactic:
exact measure_eq_zero_of_subset_sdiff_everywherePosSubset h'k hk

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case e_f
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst✝²⁶ : NormedAddCommGroup E
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 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
t : G
⊢ ∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ =
    ∫ (u : G), (L₃ (f t)) ((L₄ (g u)) (k (x₀ - t - u))) ∂μ

Tactic:
rw [eq_comm, ← integral_sub_right_eq_self _ t]

Goal state after:
case e_f
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
E'' : Type uE''
F : Type uF
F' : Type uF'
F'' : Type uF''
inst✝²⁶ : NormedAddCommGroup E
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 𝕜 E''
inst✝¹⁸ : NormedSpace ℝ F
inst✝¹⁷ : NormedSpace 𝕜 F
inst✝¹⁶ : MeasurableSpace G
μ ν : Measure G
L : E →L[𝕜] E' →L[𝕜] F
inst✝¹⁵ : CompleteSpace F
inst✝¹⁴ : NormedAddCommGroup F'
inst✝¹³ : NormedSpace ℝ F'
inst✝¹² : NormedSpace 𝕜 F'
inst✝¹¹ : CompleteSpace F'
inst✝¹⁰ : NormedAddCommGroup F''
inst✝⁹ : NormedSpace ℝ F''
inst✝⁸ : NormedSpace 𝕜 F''
inst✝⁷ : CompleteSpace F''
k : G → E''
L₂ : F →L[𝕜] E'' →L[𝕜] F'
L₃ : E →L[𝕜] F'' →L[𝕜] F'
L₄ : E' →L[𝕜] E'' →L[𝕜] F''
inst✝⁶ : AddGroup G
inst✝⁵ : SFinite μ
inst✝⁴ : SFinite ν
inst✝³ : μ.IsAddRightInvariant
inst✝² : MeasurableAdd₂ G
inst✝¹ : ν.IsAddRightInvariant
inst✝ : MeasurableNeg G
hL : ∀ (x : E) (y : E') (z : E''), (L₂ ((L x) y)) z = (L₃ x) ((L₄ y) z)
x₀ : G
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt g k x L₄ μ
hi : Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
t : G
⊢ ∫ (x : G), (L₃ (f t)) ((L₄ (g (x - t))) (k (x₀ - t - (x - t)))) ∂μ =
    ∫ (t_1 : G), (L₃ (f t)) ((L₄ (g (t_1 - t))) (k (x₀ - t_1))) ∂μ
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
⊢ support f ⊆ Euclidean.ball x d

Tactic:
intro y

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (toEuclidean x) := { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ := ↑c ∘ ⇑toEuclidean
y : E
⊢ y ∈ support f → y ∈ Euclidean.ball x d
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:

Tactic:
∫ x, f x ∂μ = ∫ x in closedBall c f.rOut, f x ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    apply f.zero_of_le_dist (le_of_lt _)
    simpa using hx
  _ ≤ ∫ x in closedBall c f.rOut, 1 ∂μ := by
    apply setIntegral_mono f.integrable.integrableOn _ (fun x ↦ f.le_one)
    simp [measure_closedBall_lt_top]
  _ = μ.real (closedBall c f.rOut) := by simp

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case neg
G : Type u_1
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
H : ¬LocallyCompactSpace G
⊢ ∃ c, ∀ (f : G → ℝ), Continuous[inst✝⁷, _] f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ

Tactic:
refine ⟨0, fun f f_cont f_comp ↦ ?_⟩
    rcases f_comp.eq_zero_or_locallyCompactSpace_of_group f_cont with hf | hf
    · simp [hf]
    · exact (H hf).elim

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

Goal state before:
pp: case inl
α : 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
this : sInf (univ \ A) ≠ N
H : sInf (univ \ A) < N
⊢ sInf (univ \ A) < N

pp: case inr
α : 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
this : sInf (univ \ A) ≠ N
H : sInf (univ \ A) = N
⊢ sInf (univ \ A) < N

Tactic:
· exact H

Goal state after:
case inr
α : 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
this : sInf (univ \ A) ≠ N
H : sInf (univ \ A) = N
⊢ sInf (univ \ A) < N
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
⊢ HasCompactSupport u

Tactic:
by
  rw [hasCompactSupport_def, u_support, closure_ball (0 : E) one_ne_zero]
  exact isCompact_closedBall _ _

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
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
Dpos : 0 < D
⊢ support (w D) = ball 0 D

Tactic:
have B : D • ball (0 : E) 1 = ball 0 D := by
    rw [smul_unitBall Dpos.ne', Real.norm_of_nonneg Dpos.le]
  have C : D ^ finrank ℝ E ≠ 0 := by
    norm_cast
    exact pow_ne_zero _ Dpos.ne'
  simp only [w_def, smul_eq_mul, support_mul, support_inv, univ_inter,
    support_comp_inv_smul₀ Dpos.ne', u_support, B, support_const (u_int_pos E).ne', support_const C,
    abs_of_nonneg Dpos.le]

Goal state after: