mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤

Tactic:
rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx)
    (singleton_nonempty _) (affineIndependent_of_subsingleton _ _) with ⟨s, -, hsu, hs⟩

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
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
S : AffineSubspace k P
hS : affineSpan k (Set.range s.points) ≤ S
⊢ (s.restrict S hS).medial = s.medial.restrict S ⋯

Tactic:
have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  ext i
  simp [medial_points]

Goal state after:
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:
by
  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 : Set P
p : P
⊢ finrank k ↥(vectorSpan k (insert p s)) ≤ finrank k ↥(vectorSpan k s) + 1

Tactic:
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan,
    ← direction_affineSpan _ s]

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
⊢ finrank k ↥(vectorSpan k (insert p ↑(affineSpan k s))) ≤ finrank k ↥(affineSpan k s).direction + 1
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
C : ℝ
hC : 0 ≤ C
f : ↥(lp E p)
hf : ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal
⊢ ∑' (i : α), ‖↑f i‖ ^ p.toReal ≤ C ^ p.toReal

Tactic:
exact hf

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

Goal state before:
pp: ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
f' : ι → E → E →L[𝕜] G
g' : E → E →L[𝕜] G
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 : ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x), dist (‖x_1.2 - x‖⁻¹ * ‖g x_1.2 - g x - (g' x) (x_1.2 - x)‖) 0 < ε
hε : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝 x, dist (‖x_1 - x‖⁻¹ * ‖g x_1 - g x - (g' x) (x_1 - x)‖) 0 < ε

Tactic:
eventually_curry_iff

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
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 :
  ∀ᶠ (x_1 : ι) in l, ∀ᶠ (y : E) in 𝓝 x, dist (‖(x_1, y).2 - x‖⁻¹ * ‖g (x_1, y).2 - g x - (g' x) ((x_1, y).2 - x)‖) 0 < ε
hε : ε > 0
⊢ ∀ᶠ (x_1 : E) in 𝓝 x, dist (‖x_1 - x‖⁻¹ * ‖g x_1 - g x - (g' x) (x_1 - x)‖) 0 < ε
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case pos.hF_meas
α : 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 : α → ℝ := ⋯
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₀)) ∂μ‖
⊢ ∀ᶠ (n : H) in 𝓝 x₀, AEStronglyMeasurable (fun a ↦ ‖n - x₀‖⁻¹ • (F n a - F x₀ a - (F' a) (n - x₀))) μ

Tactic:
filter_upwards [h_ball] with _ x_in

Goal state after:
α : Type u_1
inst✝⁶ : MeasurableSpace α
μ : Measure α
𝕜 : Type u_2
inst✝⁵ : RCLike 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace 𝕜 E
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₀)) ∂μ‖
a✝ : H
x_in : a✝ ∈ ball x₀ ε
⊢ AEStronglyMeasurable (fun a ↦ ‖a✝ - x₀‖⁻¹ • (F a✝ a - F x₀ a - (F' a) (a✝ - x₀))) μ
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
⊢ ∀ᶠ (x_1 : ι × E) in l.curry (𝓝 x),
    dist ((↑‖x_1.2 - x‖)⁻¹ • (f x_1.1 x_1.2 - f x_1.1 x - ((f' x_1.1 x) x_1.2 - (f' x_1.1 x) x))) 0 < ε

Tactic:
eventually_curry_iff

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
⊢ ∀ᶠ (x_1 : ι) in l,
    ∀ᶠ (y : E) in 𝓝 x,
      dist
          ((↑‖(x_1, y).2 - x‖)⁻¹ •
            (f (x_1, y).1 (x_1, y).2 - f (x_1, y).1 x - ((f' (x_1, y).1 x) (x_1, y).2 - (f' (x_1, y).1 x) x)))
          0 <
        ε
Module: Mathlib.Analysis.Calculus.ParametricIntegral

Goal state before:
pp: case pos.h_bound
α : 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₀)) ∂μ‖
x : H
hx : x ∈ ball x₀ ε
a : α
ha_bound : ‖F x a - F x₀ a‖ ≤ b a * ‖x - x₀‖
⊢ b a * ‖x - x₀‖ / ‖x - x₀‖ + ‖F' a‖ * ‖x - x₀‖ / ‖x - x₀‖ ≤ b a + ‖F' a‖

Tactic:
apply_rules [add_le_add, div_le_of_le_mul₀] <;> first | rfl | positivity

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'
x : G
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✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
t : G
ht : f (-t) = f t
⊢ g (-(x + t)) = g (x + t) → (L (f t)) (g (-x - t)) = (L (f (-t))) (g (x + t))

Tactic:
h't

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'
x : G
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✝⁴ : AddCommGroup G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : μ.IsNegInvariant
inst✝¹ : MeasurableNeg G
inst✝ : MeasurableAdd G
h1 : ∀ᵐ (x : G) ∂μ, f (-x) = f x
h2 : ∀ᵐ (x : G) ∂μ, g (-x) = g x
t : G
ht : f (-t) = f t
h't : g (-(x + t)) = g (x + t)
⊢ (L (f t)) (g (-x - t)) = (L (f (-t))) (g (x + t))
Module: Mathlib.Topology.MetricSpace.ProperSpace.Lemmas

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

Tactic:
exact ⟨r / 2, ⟨half_pos hr, half_lt_self hr⟩, empty_subset _⟩

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

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

Tactic:
rcases le_or_gt r 0 with hr | hr
  · rw [ball_eq_empty.2 hr, subset_empty_iff] at h
    subst s
    exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩
  · exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩

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 ℕ :=
  ⋃ 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}
⊢ p.color i = sInf (univ \ A)

Tactic:
color

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}
⊢ sInf
      (univ \
        ⋃ 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}) =
    sInf (univ \ A)
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : LocallyCompactSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : IsFiniteMeasureOnCompacts μ'
inst✝ : μ'.IsMulLeftInvariant
c : ℝ≥0
hc : c ≠ 0
⊢ (c • μ').haarScalarFactor (c • μ) = μ'.haarScalarFactor μ

Tactic:
rw [haarScalarFactor_smul, smul_eq_mul, mul_haarScalarFactor_smul _ _ hc]

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✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
R : ℝ
⊢ 1 < R → 0 < (R - 1) / (R + 1)

Tactic:
hR

Goal state after:
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
R : ℝ
hR : 1 < R
⊢ 0 < (R - 1) / (R + 1)
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: case hf.hf
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffOn ℝ ∞ (fun x ↦ (x.1 - 1) / (x.1 + 1)) (Ioi 1 ×ˢ univ)

pp: case hf.hg
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffOn ℝ ∞ (fun x ↦ ((x.1 + 1) / 2)⁻¹ • x.2) (Ioi 1 ×ˢ univ)

Tactic:
· refine
              (contDiffOn_fst.sub contDiffOn_const).div (contDiffOn_fst.add contDiffOn_const) ?_
            rintro ⟨R, x⟩ ⟨hR : 1 < R, _⟩
            apply ne_of_gt
            dsimp only
            linarith

Goal state after:
case hf.hg
E✝ : Type u_1
inst✝⁵ : NormedAddCommGroup E✝
inst✝⁴ : NormedSpace ℝ E✝
inst✝³ : FiniteDimensional ℝ E✝
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
this✝¹ : MeasurableSpace E := ⋯
this✝ : BorelSpace E
IR : ∀ (R : ℝ), 1 < R → 0 < (R - 1) / (R + 1)
⊢ ContDiffOn ℝ ∞ (fun x ↦ ((x.1 + 1) / 2)⁻¹ • x.2) (Ioi 1 ×ˢ univ)
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
⊢ s.card ≤ 5 ^ finrank ℝ E

Tactic:
have ρpos : 0 < ρ := by norm_num

Goal state after:
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 < ρ
⊢ s.card ≤ 5 ^ finrank ℝ E
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
fGn : ∀ n ≤ N, p.c (p.index (G n)) ∉ p.iUnionUpTo (G n) ∧ p.R (G n) ≤ p.τ * p.r (p.index (G n))
Gab :
  ∀ (a b : Fin N.succ),
    G ↑a < G ↑b →
      p.r (p.index (G ↑a)) ≤ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑b))) ∧
        p.r (p.index (G ↑b)) ≤ p.τ * p.r (p.index (G ↑a))
a : Fin (N + 1)
ha : a < last N
I : ↑a < N
J : G ↑(last N) = i
K : G ↑a = g ↑a
⊢ dist (p.c (p.index (G ↑a))) (p.c (p.index (G ↑(last N)))) ≤ p.r (p.index (G ↑a)) + p.r (p.index (G ↑(last N)))

Tactic:
convert! dist_le_add_of_nonempty_closedBall_inter_closedBall (hg _ I).2.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 δ)
A_subset : A ⊆ ball 0 ρ
I : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1)
⊢ s.card ≤ 5 ^ finrank ℝ E

Tactic:
have J : (s.card : ℝ≥0∞) * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) :=
    (ENNReal.mul_le_mul_iff_left (measure_ball_pos _ _ zero_lt_one).ne' measure_ball_lt_top.ne).1 I

Goal state after:
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 δ)
A_subset : A ⊆ ball 0 ρ
I : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1)
J : ↑s.card * ENNReal.ofReal (δ ^ finrank ℝ E) ≤ ENNReal.ofReal (ρ ^ finrank ℝ E)
⊢ s.card ≤ 5 ^ finrank ℝ E
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i ↦ ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx < jy
A : Set ℕ :=
  ⋃ j,
    ⋃ (_ :
      (closedBall (p.c (p.index ↑j)) (p.r (p.index ↑j)) ∩ closedBall (p.c (p.index jy)) (p.r (p.index jy))).Nonempty),
      {p.color ↑j}
color_j : p.color jy = sInf (univ \ A)
⊢ sInf (univ \ A) ∈ univ \ A

Tactic:
apply csInf_mem

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := ⋯
s : Fin N → Set β := ⋯
i : Fin N
jx : Ordinal.{u}
jx_lt : jx < p.lastStep
jxi : p.color jx = ↑i
hx : p.index jx ∈ s i
jy : Ordinal.{u}
jy_lt : jy < p.lastStep
jyi : p.color jy = ↑i
hy : p.index jy ∈ s i
x_ne_y : p.index jx ≠ p.index jy
jxy : jx < jy
A : Set ℕ := ⋯
color_j : p.color jy = sInf (univ \ A)
⊢ (univ \ A).Nonempty
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝¹² : TopologicalSpace G
inst✝¹¹ : Group G
inst✝¹⁰ : IsTopologicalGroup G
inst✝⁹ : MeasurableSpace G
inst✝⁸ : BorelSpace G
H : Type u_2
inst✝⁷ : Group H
inst✝⁶ : TopologicalSpace H
inst✝⁵ : IsTopologicalGroup H
inst✝⁴ : CompactSpace H
inst✝³ : MeasurableSpace H
inst✝² : BorelSpace H
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
ν : Measure H
inst✝ : ν.IsHaarMeasure
f : G →* H
hcont : Continuous[inst✝¹², inst✝⁶] ⇑f
hsurj : Surjective ⇑f
huniv : μ univ = ν univ
⊢ μ univ < ∞

Tactic:
by rw [huniv]; apply measure_lt_top

Goal state after:
Module: Mathlib.Analysis.Convex.NNReal

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x✝ : M
hx : x✝ ∈ s
y✝ : M
hy : y✝ ∈ s
a b : ℝ
ha : 0 ≤ a
⊢ 0 ≤ b → a + b = 1 → a • x✝ + b • y✝ ∈ s

Tactic:
hb

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x✝ : M
hx : x✝ ∈ s
y✝ : M
hy : y✝ ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
⊢ a + b = 1 → a • x✝ + b • y✝ ∈ s
Module: Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise

Goal state before:
pp: E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
k : ℕ
α : ↑I
f : E → F
a : E
g : E → G
hf : ContDiffPointwiseHolderAt k α f a
hg : ContDiffPointwiseHolderAt k α g a
⊢ (fun x ↦
      (iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a).prod (iteratedFDeriv ℝ k g x - iteratedFDeriv ℝ k g a)) =O[𝓝 a]
    fun x ↦ ‖x - a‖ ^ ↑α

Tactic:
by
      refine .of_norm_left ?_
      simp only [ContinuousMultilinearMap.opNorm_prod, ← Prod.norm_mk]
      exact (hf.isBigO.prod_left hg.isBigO).norm_left

Goal state after: