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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₂ ∈ {p₂, p₃, p}

Tactic:
by simp

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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p ∈ {p₂, p₃, p}

Tactic:
by simp

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
p₁ p₂ p₃ p : P
ha : AffineIndependent k ![p₁, p₂, p₃]
hcol : Collinear k {p₂, p₃, p}
hne : p₂ ≠ p
h : Collinear k {p₁, p₂, p}
⊢ p₃ ∈ {p₂, p₃, p}

Tactic:
by simp

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
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ Module.rank k ↥(vectorSpan k s) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2

Tactic:
rw [← finrank_eq_rank] at h

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
inst✝ : FiniteDimensional k ↥(vectorSpan k s)
h : Coplanar k s ↔ ↑(finrank k ↥(vectorSpan k s)) ≤ 2
⊢ Coplanar k s ↔ finrank k ↥(vectorSpan k s) ≤ 2
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ENNReal.toReal 0
H : Summable fun x ↦ 1
⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable fun i ↦ ‖f i‖ ^ ∞.toReal
H : Summable fun x ↦ 1
⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: α : 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
⊢ 0 < 1

Tactic:
by simp

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

Goal state before:
pp: I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ Memℓp (f * g) ∞

Tactic:
rw [memℓp_infty_iff]

Goal state after:
I : Type u_5
B : I → Type u_6
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ∞
hg : Memℓp g ∞
⊢ BddAbove (Set.range fun i ↦ ‖(f * g) i‖)
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
y : E
hy : y ∈ ball 0 1
⊢ √(1 - ‖y‖ ^ 2) ≠ 0

Tactic:
by
      rw [Real.sqrt_ne_zero']
      nlinarith [norm_nonneg y, mem_ball_zero_iff.1 hy]

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
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 𝕜 := IsRCLikeNormedField.rclike 𝕜
hf' : TendstoUniformlyOnFilter (fun n z ↦ -f' n.1 z + f' n.2 z) 0 (l ×ˢ l) (𝓝 x)
this : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
ε : ℝ
hε : ε > 0
t : Set G
ht : t ∈ map (fun n ↦ f n x) l
ht' : ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
⊢ ∀ᶠ (y : E) in 𝓝 x, (fun x ↦ True) y

Tactic:
by simp

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)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
⊢ ∀ (x : ℕ), (∀ᶠ (l : ℕ) in atTop, (F x, F l) ∈ {p_1 | ‖p_1.1 - p_1.2‖ < ε}) → F x ∈ Metric.closedBall f ε

Tactic:
rintro n (hn : ∀ᶠ l in atTop, ‖(fun f => F n - f) (F l)‖ < ε)

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
ε : ℝ
hε : 0 < ε
hε' : {p_1 | ‖p_1.1 - p_1.2‖ < ε} ∈ uniformity ↥(lp E p)
n : ℕ
hn : ∀ᶠ (l : ℕ) in atTop, ‖(fun f ↦ F n - f) (F l)‖ < ε
⊢ F n ∈ Metric.closedBall f ε
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
ι : Type u_5
inst✝ : PseudoMetricSpace α
g : α → ι → ℝ
K : ℝ≥0
hg : ∀ (i : ι), LipschitzWith K fun x ↦ g x i
a₀ a : α
M : ℝ
hM : M ∈ upperBounds (Set.range fun i ↦ ‖g a₀ i‖)
i : ι
⊢ |g a i| = |g a i - g a₀ i + g a₀ i|

Tactic:
by simp

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

Goal state before:
pp: n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ ↑m fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ↑m = ⊤ → AnalyticOn ℝ (fun x ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) univ

Tactic:
by simp

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
R : ℝ
hR : 0 < R - 1
A : ContinuousAt (fun p ↦ (p.1 - ‖p.2‖) / (p.1 - 1)) (R, 0)
⊢ ‖(R, 0).2‖ < 1

Tactic:
by simp

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
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 p x ≠ 0
this : LocallyCompactSpace G
q₀ : P
x₀ : G
hq₀ : (q₀, x₀).1 ∈ s
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := -k +ᵥ t
k'_comp : IsCompact k'
g' : P × G → G → E' := fun p x ↦ g p.1 (p.2 - x)
s' : Set (P × G) := s ×ˢ t
A : ContinuousOn (uncurry g') (s' ×ˢ univ)
p : P
x y : G
hp : (p, x).1 ∈ s
hx : (p, x).2 ∈ t
hy : (p, x).2 - y ∈ k
⊢ (fun x1 x2 ↦ x1 + x2) (y - x) x = y

Tactic:
by simp

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₀ ≤ ε
⊢ dist ((f ⋆[L, μ] g) x₀) (∫ (t : G), (L (f t)) z₀ ∂μ) ≤ (‖L‖ * ∫ (x : G), ‖f x‖ ∂μ) * ε

Tactic:
have hfg : ConvolutionExistsAt f g x₀ L μ := by
    refine BddAbove.convolutionExistsAt L ?_ Metric.isOpen_ball.measurableSet (Subset.trans ?_ hf)
      hif.integrableOn hmg
    swap; · refine fun t => mt fun ht : f t = 0 => ?_; simp_rw [ht, L.map_zero₂]
    rw [bddAbove_def]
    refine ⟨‖z₀‖ + ε, ?_⟩
    rintro _ ⟨x, hx, rfl⟩
    refine norm_le_norm_add_const_of_dist_le (hg x ?_)
    rwa [mem_ball_iff_norm, norm_sub_rev, ← mem_ball_zero_iff]
  have h2 : ∀ t, dist (L (f t) (g (x₀ - t))) (L (f t) z₀) ≤ ‖L (f t)‖ * ε := by
    intro t; by_cases ht : t ∈ support f
    · have h2t := hf ht
      rw [mem_ball_zero_iff] at h2t
      specialize hg (x₀ - t)
      rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
      refine ((L (f t)).dist_le_opNorm _ _).trans ?_
      gcongr
      exact hg h2t
    · rw [notMem_support] at ht
      simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
      rfl
  simp_rw [convolution_def]
  simp_rw [dist_eq_norm] at h2 ⊢
  rw [← integral_sub hfg.integrable]; swap; · exact (L.flip z₀).integrable_comp hif
  refine (norm_integral_le_of_norm_le ((L.integrable_comp hif).norm.mul_const ε)
    (Eventually.of_forall h2)).trans ?_
  rw [integral_mul_const]
  gcongr
  have h3 : ∀ t, ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖ := by
    intro t
    exact L.le_opNorm (f t)
  refine (integral_mono (L.integrable_comp hif).norm (hif.norm.const_mul _) h3).trans_eq ?_
  rw [integral_const_mul]

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: G : Type uG
E' : Type uE'
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : MeasurableSpace G
μ : Measure G
inst✝⁶ : SeminormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : SecondCountableTopology G
inst✝³ : μ.IsAddLeftInvariant
inst✝² : SFinite μ
inst✝¹ : NormedSpace ℝ E'
inst✝ : CompleteSpace E'
ι : Type u_1
g : ι → G → E'
l : Filter ι
x₀ : G
z₀ : E'
φ : ι → G → ℝ
k : ι → G
hnφ : ∀ᶠ (i : ι) in l, ∀ (x : G), 0 ≤ φ i x
hiφ : ∀ᶠ (i : ι) in l, ∫ (x : G), φ i x ∂μ = 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ t ∈ 𝓝 0, ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ pa,
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
⊢ 0 < 3

Tactic:
by simp

Goal state after:
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
⊢ comap F (𝓝 (F x)) ≤ 𝓝 x

Tactic:
refine ((nhds_basis_ball.comap _).le_basis_iff hB.nhds_hasBasis).2 ?_
    rintro V ⟨hVB, hxV⟩
    rcases hB.exists_closure_subset (hB.mem_nhds hVB hxV) with ⟨U, hUB, hxU, hUV⟩
    set UV : ↥s := ⟨(U, V), ⟨hUB, hVB⟩, hUV⟩
    refine ⟨ε UV, (ε01 UV).1, fun y (hy : dist (F y) (F x) < ε UV) => ?_⟩
    replace hy : dist (F y UV) (F x UV) < ε UV :=
      (BoundedContinuousFunction.dist_coe_le_dist _).trans_lt hy
    contrapose! hy
    rw [hF, hF, hfε UV hy, hf0 UV hxU, Pi.zero_apply, dist_zero_right]
    exact le_abs_self _

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: 𝕜 : 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
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x ↦ ‖g x‖) (fun x ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk : ConvolutionExistsAt (fun x ↦ ‖f x‖) ((fun x ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
⊢ ((f ⋆[L, ν] g) ⋆[L₂, μ] k) x₀ = (f ⋆[L₃, ν] g ⋆[L₄, μ] k) x₀

Tactic:
refine convolution_assoc' L L₂ L₃ L₄ hL hfg (hgk.mono fun x hx => hx.of_norm L₄ hg hk) ?_

Goal state after:
𝕜 : 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
hf : AEStronglyMeasurable f ν
hg : AEStronglyMeasurable g μ
hk : AEStronglyMeasurable k μ
hfg : ∀ᵐ (y : G) ∂μ, ConvolutionExistsAt f g y L ν
hgk : ∀ᵐ (x : G) ∂ν, ConvolutionExistsAt (fun x ↦ ‖g x‖) (fun x ↦ ‖k x‖) x (mul ℝ ℝ) μ
hfgk : ConvolutionExistsAt (fun x ↦ ‖f x‖) ((fun x ↦ ‖g x‖) ⋆[mul ℝ ℝ, μ] fun x ↦ ‖k x‖) x₀ (mul ℝ ℝ) ν
⊢ Integrable (uncurry fun x y ↦ (L₃ (f y)) ((L₄ (g (x - y))) (k (x₀ - x)))) (μ.prod ν)
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : LocallyCompactSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasureOnCompacts μ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : G → E
hg : Continuous[inst✝⁸, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
h'g : HasCompactSupport g
k : Set G := tsupport g
k_comp : IsCompact k
x₀ : G
t : Set G
t_comp : IsCompact t
ht : t ∈ 𝓝 x₀
k' : Set G := t • k⁻¹
k'_comp : IsCompact k'
p x : G
hp : p ∈ t
hx : g (x⁻¹ * p) ≠ 0
⊢ (fun x1 x2 ↦ x1 * x2) p (p⁻¹ * x) = x

Tactic:
by simp

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
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
hy : y ∈ support f
⊢ toEuclidean y ∈ support ↑c

Tactic:
simpa only [Function.mem_support, Function.comp_apply, Ne] using! hy

Goal state after:
Module: Mathlib.Analysis.Convolution

Goal state before:
pp: case pos.e_f.inr.inl
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : t ∈ Ioo 0 x
⊢ (Ioo 0 x).indicator (fun t ↦ (L (f t)) (g (x - t))) t = (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t))

Tactic:
indicator_of_mem ht,

Goal state after:
case pos.e_f.inr.inl
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ E'
inst✝¹ : NormedSpace ℝ F
f : ℝ → E
g : ℝ → E'
L : E →L[ℝ] E' →L[ℝ] F
ν : Measure ℝ
inst✝ : NullSingletonClass ν
x : ℝ
h : x ∈ Ioi 0
t : ℝ
ht : t ∈ Ioo 0 x
⊢ (L (f t)) (g (x - t)) = (L ((Ioi 0).indicator f t)) ((Ioi 0).indicator g (x - t))
Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
n✝ : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support ↑f = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun n ↦ ↑(g0 n)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n : ℕ
R : ℕ → ℝ
hR : ∀ (i : ℕ) (x : E), ‖iteratedFDeriv ℝ i (fun x ↦ g n x) x‖ ≤ R i
⊢ (Finset.image R (Finset.range (n + 1))).Nonempty

Tactic:
by simp

Goal state after:
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 μ
⊢ μ.real (closedBall c f.rIn) = ∫ (x : E) in closedBall c f.rIn, 1 ∂μ

Tactic:
by simp

Goal state after:
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 μ
⊢ ∫ (x : E) in closedBall c f.rOut, 1 ∂μ = μ.real (closedBall c f.rOut)

Tactic:
by simp

Goal state after:
Module: Mathlib.Analysis.Calculus.ContDiff.Convolution

Goal state before:
pp: 𝕜 : Type u𝕜
E : Type uE
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
G P : Type uP
inst✝¹⁰ : MeasurableSpace G
μ : Measure G
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : BorelSpace G
inst✝⁷ : NormedSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup P
inst✝⁵ : NormedSpace 𝕜 P
f : G → E
s : Set P
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hf : LocallyIntegrable f μ
n : ℕ
ih :
  ∀ {E' F : Type uP} [inst : NormedAddCommGroup E'] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 E']
    [inst_3 : NormedSpace ℝ F] [inst_4 : NormedSpace 𝕜 F] (L : E →L[𝕜] E' →L[𝕜] F) {g : P → G → E'},
    (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
      ContDiffOn 𝕜 (↑↑n) (↿g) (s ×ˢ univ) → ContDiffOn 𝕜 (↑↑n) (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)
E' F : Type uP
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
g : P → G → E'
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hg :
  DifferentiableOn 𝕜 (↿g) (s ×ˢ univ) ∧
    (↑n = ⊤ → AnalyticOn 𝕜 (↿g) (s ×ˢ univ)) ∧ ContDiffOn 𝕜 (↑n) (fderiv 𝕜 ↿g) (s ×ˢ univ)
f' : P → G → P × G →L[𝕜] F := fun p a ↦ (f ⋆[precompR (P × G) L, μ] fun x ↦ fderiv 𝕜 (uncurry g) (p, x)) a
A : ∀ (q₀ : P × G), q₀.1 ∈ s → HasFDerivAt (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (f' q₀.1 q₀.2) q₀
⊢ ↑n = ⊤ → AnalyticOn 𝕜 (fun q ↦ (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ)

Tactic:
by simp

Goal state after:
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
g : C(G, ℝ)
hg : HasCompactSupport ⇑g ∧ 0 ≤ ⇑g ∧ g 1 ≠ 0
⊢ (∫ (x : G), g x ∂c • μ') / ∫ (x : G), g x ∂μ = (c • ∫ (x : G), g x ∂μ') / ∫ (x : G), g x ∂μ

Tactic:
by simp

Goal state after:
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
this : (c • μ).IsHaarMeasure
g : C(G, ℝ)
hg : HasCompactSupport ⇑g ∧ 0 ≤ ⇑g ∧ g 1 ≠ 0
⊢ ↑c * ((∫ (x : G), g x ∂μ') / ∫ (x : G), g x ∂c • μ) = ↑c * ((∫ (x : G), g x ∂μ') / c • ∫ (x : G), g x ∂μ)

Tactic:
by simp

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

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

Tactic:
· apply le_trans _ (fGn a ha).2
      have B : p.c (p.index (G b)) ∉ p.iUnionUpTo (G a) := by
        intro H; exact (fGn b hb).1 (p.monotone_iUnionUpTo G_lt.le H)
      let b' : { t // p.c t ∉ p.iUnionUpTo (G a) } := ⟨p.index (G b), B⟩
      apply @le_ciSup _ _ _ (fun t : { t // p.c t ∉ p.iUnionUpTo (G a) } => p.r t) _ b'
      refine ⟨p.r_bound, fun t ht => ?_⟩
      simp only [exists_prop, mem_range, Subtype.exists] at ht
      rcases ht with ⟨u, hu⟩
      rw [← hu.2]
      exact p.r_le _

Goal state after: