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

Tactic:
eq_vadd_iff_vsub_eq,

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)
⊢ s.centroid -ᵥ s.points i = (↑n * (1 / (↑n + 1))) • (s.faceOppositeCentroid i -ᵥ s.points i)
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case mp
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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ n + 1 = finrank k ↥⊤ + 1

Tactic:
← (vectorSpan_eq_top_of_affineSpan_eq_top k V P) h_tot,

Goal state after:
case mp
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✝¹ : FiniteDimensional k V
inst✝ : Fintype ι
p : ι → P
hi : AffineIndependent k p
h_tot : affineSpan k (Set.range p) = ⊤
n : ℕ := Fintype.card ι - 1
hn : Fintype.card ι = n + 1
⊢ n + 1 = finrank k ↥(vectorSpan k (Set.range p)) + 1
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
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut

Tactic:
closure_ball _ f.rOut_pos.ne'

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

Goal state before:
pp: case inr.inr.inr.inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖ ^ q.toReal)
⊢ BddAbove (Set.range fun i ↦ ‖f i‖)

Tactic:
use A ^ q.toReal⁻¹

Goal state after:
case h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : A ∈ upperBounds (Set.range fun i ↦ ‖f i‖ ^ q.toReal)
⊢ A ^ q.toReal⁻¹ ∈ upperBounds (Set.range fun i ↦ ‖f i‖)
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
x₀ : E
hu : Summable u
hf : ∀ (n : α) (x : E), HasFDerivAt (f n) (f' n x) x
hf' : ∀ (n : α) (x : E), ‖f' n x‖ ≤ u n
hf0 : Summable fun n ↦ f n x₀
x : E
⊢ Summable fun n ↦ f n x

Tactic:
by
  let : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
  let _ : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 _
  exact summable_of_summable_hasFDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hf n x) (fun n x _ => hf' n x) (mem_univ _) hf0 (mem_univ _)

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

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

Tactic:
rcases isEmpty_or_nonempty α with _i | _i
    · simp [eq_iff_true_of_subsingleton]
    have H : IsLUB (Set.range fun i => ‖f i‖) 0 := by simpa [h] using! lp.isLUB_norm f
    ext i
    have : ‖f i‖ = 0 := le_antisymm (H.1 ⟨i, rfl⟩) (norm_nonneg _)
    simpa using! this

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

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

Tactic:
simp only [lp.eq_zero' f, neg_zero, norm_zero]

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

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖

Tactic:
refine le_trans ?_ hC₂

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖↑f i‖
hg₁ : ∀ (i : α), 0 ≤ ‖↑g i‖
hf₂ : HasSum (fun i ↦ ‖↑f i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun i ↦ ‖↑g i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun i ↦ (‖↑f i‖ + ‖↑g i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ≤ C
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ (‖Pi.single i x i‖ ^ (↑p).toReal) ^ (↑p).toReal⁻¹ = ‖x‖

pp: case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0

Tactic:
Real.rpow_rpow_inv _ this.ne',

Goal state after:
case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ‖Pi.single i x i‖ = ‖x‖

α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ 0 ≤ ‖Pi.single i x i‖

case coe
α : Type u_3
E : α → Type u_4
p✝ : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : DecidableEq α
i : α
x : E i
this✝ : Nonempty α
p : ℝ≥0
hp : 0 < ↑p
this : 0 < (↑p).toReal
⊢ ∀ (b' : α), b' ≠ i → ‖↑(lp.single (↑p) i x) b'‖ ^ (↑p).toReal = 0
Module: Mathlib.Analysis.Calculus.UniformLimitsDeriv

Goal state before:
pp: case right
ι : 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 x_1 ↦ f n.1 x - f n.2 x) 0 (l ×ˢ l) (𝓝 x)

Tactic:
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.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : DecidableEq α
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f : ↥(lp E p)
hp₀ : 0 < p
hp' : 0 < p.toReal
this :
  ∀ ε > 0,
    ∀ᶠ (x : Finset α) in (SummationFilter.unconditional α).filter,
      dist (∑ b ∈ x, ‖↑f b‖ ^ p.toReal) (‖f‖ ^ p.toReal) < ε
ε : ℝ
hε : ε > 0
s : Finset α
hs : |‖f‖ ^ p.toReal - ∑ b ∈ s, ‖↑f b‖ ^ p.toReal| < ε ^ p.toReal
⊢ ‖∑ i ∈ s, lp.single p i (↑f i) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖↑f i‖ ^ p.toReal

Tactic:
simpa only [coeFn_neg, Pi.neg_apply, lp.single_neg, Finset.sum_neg_distrib, neg_sub_neg,
      norm_neg, _root_.norm_neg] using lp.norm_compl_sum_single hp' (-f) s

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝⁵ : (i : α) → NormedAddCommGroup (E i)
inst✝⁴ : DecidableEq α
F : Type u_5
inst✝³ : AddCommMonoid F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : Fact (1 ≤ p)
hp : p ≠ ∞
f g : ↥(lp E p) →ₜ+ F
h : ∀ (i : α), f.comp (singleContinuousAddMonoidHom E p i) = g.comp (singleContinuousAddMonoidHom E p i)
⊢ f = g

Tactic:
by
  ext x
  have := lp.hasSum_single hp x
  rw [← (this.map f f.continuous).tsum_eq, ← (this.map g g.continuous).tsum_eq]
  congr! 2 with i
  exact DFunLike.congr_fun (h i) (x i)

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < expNegInvGlue x

Tactic:
by
  simp [expNegInvGlue, not_le.2 hx, exp_pos]

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
    rintro ⟨p, x⟩ ⟨hp, -⟩
    apply integral_eq_zero_of_ae (Eventually.of_forall (fun y ↦ ?_))
    simp [H p hp _]

Goal state after:
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'

Tactic:
obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) :=
    this.exists_isMaxOn (β := α) (α := ℝ) hne (by fun_prop)

Goal state after:
case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hr : 0 < r
hs : IsClosed s
h : s ⊆ ball x r
hne : s.Nonempty
this : IsCompact s
y : α
hys : y ∈ s
hy : s ⊆ closedBall x (dist y x)
⊢ ∃ r' ∈ Ioo 0 r, s ⊆ ball x r'
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
rw [ball_eq_empty.2 hr, subset_empty_iff] at h

Goal state after:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'
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
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 ns with ⟨v, vx, hv⟩

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
⊢ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} ∈ 𝓝 x
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)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
⊢ ∃ f, IsInducing f

Tactic:
have hF : ∀ x UV, F x UV = f UV x := fun _ _ => rfl

Goal state after:
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)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
⊢ ∃ f, IsInducing f
Module: Mathlib.Topology.Metrizable.Urysohn

Goal state before:
pp: case refine_2
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)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
⊢ ∃ i, 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V

Tactic:
rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩

Goal state after:
case refine_2
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)
f : ↑s → C(X, ℝ)
hf0 : ∀ (UV : ↑s), EqOn (⇑(f UV)) 0 (↑UV).1
hfε : ∀ (UV : ↑s), EqOn (⇑(f UV)) (fun x ↦ ε UV) (↑UV).2ᶜ
hf0ε : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 (ε UV)
hf01 : ∀ (UV : ↑s) (x : X), (f UV) x ∈ Icc 0 1
F : X → ↑s →ᵇ ℝ := fun x ↦ { toFun := fun UV ↦ (f UV) x, continuous_toFun := ⋯, map_bounded' := ⋯ }
hF : ∀ (x : X) (UV : ↑s), (F x) UV = (f UV) x
x : X
V : Set X
hVB : V ∈ B
hxV : x ∈ V
U : Set X
hUB : U ∈ B
hxU : x ∈ U
hUV : closure[inst✝²] U ⊆ V
⊢ ∃ i, 0 < i ∧ F ⁻¹' ball (F x) i ⊆ V
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
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
v : ℕ → G
hv : ∀ (i : ℕ), v i ∈ V i
y : ℕ → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun x1 x2 ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
⊢ x ∈ k

Tactic:
have A n : μ (((x * z⁻¹) • k) \ k) ≤ u n := by
    apply le_of_lt (hW _ _ ?_)
    have : W n * {z} ∈ 𝓝 z := (IsOpen.mul_right (W_open n)).mem_nhds (by simp [mem_W])
    obtain ⟨i, hi, ni⟩ : ∃ i, y i ∈ W n * {z} ∧ n < i :=
      ((hz.frequently this).and_eventually (eventually_gt_atTop n)).exists
    refine ⟨x * (y i) ⁻¹, ?_, y i * z⁻¹, by simpa using hi, by group⟩
    have I : V i ⊆ W n := iInter₂_subset n (by simp [ni])
    have J : x * (y i)⁻¹ ∈ V i := by simpa [← hvy i] using hv i
    exact I J

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
h : μ.IsEverywherePos k
hk : IsCompact k
h'k : IsClosed[inst✝⁷] k
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1
u_lim : Tendsto u atTop (𝓝 0)
W : ℕ → Set G
W_open : ∀ (n : ℕ), IsOpen[inst✝⁷] (W n)
mem_W : ∀ (n : ℕ), 1 ∈ W n
hW : ∀ (n : ℕ), ∀ g ∈ W n * W n, μ (g • k \ k) < u n
V : ℕ → Set G := fun n ↦ ⋂ i ∈ Finset.range n, W i
x : G
hx : x ∈ ⋂ n, V n * k
v : ℕ → G
hv : ∀ (i : ℕ), v i ∈ V i
y : ℕ → G
hy : ∀ (i : ℕ), y i ∈ k
hvy : ∀ (i : ℕ), (fun x1 x2 ↦ x1 * x2) (v i) (y i) = x
z : G
zk : z ∈ k
hz : MapClusterPt z atTop y
A : ∀ (n : ℕ), μ ((x * z⁻¹) • k \ k) ≤ u n
⊢ x ∈ k
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✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∉ K
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0

pp: case pos
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∈ K
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0

Tactic:
· simp [image_eq_zero_of_notMem_tsupport H]

Goal state after:
case pos
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := fun x ↦ ∫ (y : G), g (y⁻¹ * x) ∂ν
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
K : Set G := tsupport f
K_comp : IsCompact K
L : Set G := tsupport g
L_comp : IsCompact L
M : Set G := (fun p ↦ p.1 * p.2⁻¹) '' K ×ˢ L
M_comp : IsCompact M
M'_comp : IsCompact (closure[inst✝⁹] M)
x y : G
hxy : (x, y) ∉ K ×ˢ closure[inst✝⁹] M
H : x ∈ K
⊢ f (x, y).1 * (D (x, y).1)⁻¹ * g ((x, y).2⁻¹ * (x, y).1) = 0
Module: Mathlib.Analysis.Calculus.BumpFunction.Normed

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball c f.rOut) = closedBall c f.rOut

Tactic:
closure_ball _ f.rOut_pos.ne'

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : HasContDiffBump E
inst✝⁴ : MeasurableSpace E
c : E
f : ContDiffBump c
μ : Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : μ.IsOpenPosMeasure
⊢ closedBall c f.rOut = closedBall c f.rOut
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case h'f
G : Type u_1
inst✝⁹ : TopologicalSpace G
inst✝⁸ : Group G
inst✝⁷ : IsTopologicalGroup G
inst✝⁶ : MeasurableSpace G
inst✝⁵ : BorelSpace G
μ ν : Measure G
inst✝⁴ : IsFiniteMeasureOnCompacts μ
inst✝³ : IsFiniteMeasureOnCompacts ν
inst✝² : μ.IsMulLeftInvariant
inst✝¹ : ν.IsMulRightInvariant
inst✝ : ν.IsOpenPosMeasure
f g : G → ℝ
hf : Continuous[inst✝⁹, _] f
h'f : HasCompactSupport f
hg : Continuous[inst✝⁹, _] g
h'g : HasCompactSupport g
g_nonneg : 0 ≤ g
x₀ : G
g_pos : g x₀ ≠ 0
Hf : LocallyCompactSpace G
D : G → ℝ := ⋯
D_cont : Continuous[inst✝⁹, _] D
D_pos : ∀ (x : G), 0 < D x
⊢ HasCompactSupport (uncurry fun x y ↦ f x * (D x)⁻¹ * g (y⁻¹ * x))

Tactic:
let K := tsupport f
        have K_comp : IsCompact K := h'f
        let L := tsupport g
        have L_comp : IsCompact L := h'g
        let M := (fun (p : G × G) ↦ p.1 * p.2⁻¹) '' (K ×ˢ L)
        have M_comp : IsCompact M :=
          (K_comp.prod L_comp).image (continuous_fst.mul continuous_snd.inv)
        have M'_comp : IsCompact (closure M) := M_comp.closure
        have : ∀ (p : G × G), p ∉ K ×ˢ closure M → f p.1 * (D p.1)⁻¹ * g (p.2⁻¹ * p.1) = 0 := by
          rintro ⟨x, y⟩ hxy
          by_cases H : x ∈ K; swap
          · simp [image_eq_zero_of_notMem_tsupport H]
          have : g (y⁻¹ * x) = 0 := by
            apply image_eq_zero_of_notMem_tsupport
            contrapose hxy
            simp only [mem_prod, H, true_and]
            apply subset_closure
            simp only [M, mem_image, mem_prod, Prod.exists]
            exact ⟨x, y⁻¹ * x, ⟨H, hxy⟩, by group⟩
          simp [this]
        apply HasCompactSupport.intro' (K_comp.prod M'_comp) ?_ this
        exact (isClosed_tsupport f).prod isClosed_closure

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : MetricSpace α
N : ℕ
τ : ℝ
a : SatelliteConfig α N τ
i : Fin N.succ
H : i < last N
⊢ dist (a.c i) (a.c (last N)) ≤ a.r i + a.r (last N)

Tactic:
exact a.inter i H

Goal state after: