mathlib-initiative/mathlib-tactics huggingface dataset:
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✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ : G
⊢ (support fun t ↦ (L (f t)) (g (x₀ - t))) ⊆ support (g ∘ ⇑(Homeomorph.subLeft x₀))

Tactic:
refine fun t => mt fun ht : g (x₀ - t) = 0 => ?_

Goal state after:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedAddCommGroup E'
inst✝⁹ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : NormedSpace 𝕜 E'
inst✝⁵ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝⁴ : MeasurableSpace G
μ : Measure G
inst✝³ : AddGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalAddGroup G
inst✝ : BorelSpace G
hcg : HasCompactSupport g
hf : LocallyIntegrable f μ
hg : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
x₀ t : G
ht : g (x₀ - t) = 0
⊢ (fun t ↦ (L (f t)) (g (x₀ - t))) t = 0
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
s : Set P
v : P → G
hv : ContinuousOn v s
g : P → G → E'
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)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ

Tactic:
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ ∃ u, IsOpen[inst✝¹] u ∧ μ.everywherePosSubset s = s \ u

Tactic:
refine ⟨{x | ∃ n ∈ 𝓝[s] x, μ n = 0}, ?_, by ext x; simp [everywherePosSubset, pos_iff_ne_zero]⟩
  rw [isOpen_iff_mem_nhds]
  intro x ⟨n, ns, hx⟩
  rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 ns with ⟨v, vx, hv⟩
  rcases mem_nhds_iff.1 vx with ⟨w, wv, w_open, xw⟩
  have A : w ⊆ {x | ∃ n ∈ 𝓝[s] x, μ n = 0} := by
    intro y yw
    refine ⟨s ∩ w, inter_mem_nhdsWithin _ (w_open.mem_nhds yw), measure_mono_null ?_ hx⟩
    rw [inter_comm]
    exact (inter_subset_inter_left _ wv).trans hv
  have B : w ∈ 𝓝 x := w_open.mem_nhds xw
  exact mem_of_superset B A

Goal state after:
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, IsInducing f

Tactic:
have : ∀ UV : s, ∃ f : C(X, ℝ),
      EqOn f 0 UV.1.1 ∧ EqOn f (fun _ => ε UV) UV.1.2ᶜ ∧ ∀ x, f x ∈ Icc 0 (ε UV) := by
    intro UV
    rcases exists_continuous_zero_one_of_isClosed isClosed_closure
        (hB.isOpen UV.2.1.2).isClosed_compl (hd UV) with
      ⟨f, hf₀, hf₁, hf01⟩
    exact ⟨ε UV • f, fun x hx => by simp [hf₀ (subset_closure hx)], fun x hx => by simp [hf₁ hx],
      fun x => ⟨mul_nonneg (ε01 _).1.le (hf01 _).1, mul_le_of_le_one_right (ε01 _).1.le (hf01 _).2⟩⟩

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)
this : ∀ (UV : ↑s), ∃ f, EqOn (⇑f) 0 (↑UV).1 ∧ EqOn (⇑f) (fun x ↦ ε UV) (↑UV).2ᶜ ∧ ∀ (x : X), f x ∈ Icc 0 (ε UV)
⊢ ∃ f, IsInducing f
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
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
⊢ dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) z₀ < ε

Tactic:
have hgi : dist (g i (k i)) z₀ < ε / 3 := hgδ hpi (hki.trans <| half_lt_self hδ)

Goal state after:
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
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
⊢ dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) z₀ < ε
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
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
x' : G
hx' : x' ∈ ball (k i) (δ / 2)
⊢ δ / 2 + δ / 2 ≤ δ

Tactic:
add_halves

Goal state after:
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
h2ε : 0 < ε / 3
p : ι → Prop
hp : ∀ᶠ (i : ι) in l, p i
δ : ℝ
hδ : δ > 0
hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (g i x) z₀ < ε / 3
h2k : ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2
h2φ : ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)
i : ι
hpi : p i
hki : dist (k i) x₀ < δ / 2
hφi : support (φ i) ⊆ ball 0 (δ / 2)
hnφi : ∀ (x : G), 0 ≤ φ i x
hiφi : ∫ (x : G), φ i x ∂μ = 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
x' : G
hx' : x' ∈ ball (k i) (δ / 2)
⊢ δ ≤ δ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case inl
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 : f = 0
⊢ ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ

pp: case inr
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
⊢ ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ

Tactic:
· simp [Hf]

Goal state after:
case inr
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
⊢ ∫ (x : G), f x ∂μ = (∫ (y : G), f y * (∫ (z : G), g (z⁻¹ * y) ∂ν)⁻¹ ∂ν) * ∫ (x : G), g x ∂μ
Module: Mathlib.MeasureTheory.Measure.Haar.Unique

Goal state before:
pp: case inl
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
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
Hf : f = 0
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ

pp: case inr
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
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ

Tactic:
· simp [Hf]

Goal state after:
case inr
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
f : G → ℝ
hf : Continuous[inst✝⁷, _] f
h'f : HasCompactSupport f
Hf : LocallyCompactSpace G
⊢ ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂μ'.haarScalarFactor μ • μ
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 ∂μ') / c • ∫ (x : G), g x ∂μ) = (∫ (x : G), g x ∂μ') / ∫ (x : G), g x ∂μ

Tactic:
by
      rw [NNReal.smul_def, smul_eq_mul, ← mul_div_assoc]
      exact mul_div_mul_left (∫ (x : G), g x ∂μ') (∫ (x : G), g x ∂μ) (by simp [hc])

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

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedAddCommGroup E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : RCLike 𝕜
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : NormedSpace 𝕜 E'
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup G
inst✝³ : BorelSpace G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : NormedAddCommGroup P
inst✝ : NormedSpace 𝕜 P
μ : Measure G
n : ℕ∞
L : E →L[𝕜] E' →L[𝕜] F
s : Set P
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ

Tactic:
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]

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

Goal state before:
pp: 𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
P : Type uP
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : NormedAddCommGroup E'
inst✝¹³ : NormedAddCommGroup F
inst✝¹² : RCLike 𝕜
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : NormedSpace 𝕜 E'
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : BorelSpace G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : NormedAddCommGroup P
inst✝² : NormedSpace 𝕜 P
μ : Measure G
inst✝¹ : μ.IsAddLeftInvariant
inst✝ : μ.IsNegInvariant
L : E' →L[𝕜] E →L[𝕜] F
s : Set P
n : ℕ∞
v : P → G
hv : ContDiffOn 𝕜 (↑n) v s
f : G → E
g : P → G → E'
k : Set G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hk : IsCompact k
hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0
hf : LocallyIntegrable f μ
hg : ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ univ)
x : P
hx : x ∈ s
⊢ (fun x ↦ (id x, v x)) x ∈ s ×ˢ univ

Tactic:
simp only [hx, prodMk_mem_set_prod_eq, mem_univ, and_self_iff, _root_.id]

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

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
h :
  ∀ (δ : ℝ),
    0 < δ → δ < 1 → ∃ s, (∀ c ∈ s, ‖c‖ ≤ 2) ∧ (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - δ ≤ ‖c - d‖) ∧ multiplicity E < s.card
N : ℕ := multiplicity E + 1
hN : N = multiplicity E + 1
δ : ℝ
hδ : 0 < δ
hδ' : 1 ≤ δ
⊢ ∃ f, (∀ (i : Fin N), ‖f i‖ ≤ 2) ∧ Pairwise fun i j ↦ 1 - δ ≤ ‖f i - f j‖

Tactic:
· exact
        ⟨fun _ => 0, by simp, fun i j _ => by
          simpa only [norm_zero, sub_nonpos, sub_self]⟩

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Conformal

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : NormedField R
inst✝⁴ : SeminormedAddCommGroup M
inst✝³ : SeminormedAddCommGroup N
inst✝² : NormedSpace R M
inst✝¹ : NormedSpace R N
inst✝ : Subsingleton M
f' : M →L[R] N
x : M
⊢ ‖0 x‖ = ‖x‖

Tactic:
by simp [Subsingleton.elim x 0]

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

Goal state before:
pp: case refine_1
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✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
c : Set (Set G)
cA : c ⊆ A
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
a : Set G
ac : a ∈ c
x : G
hx : x ∈ a
⊢ x ∈ s

Tactic:
simp only [A, subset_def, mem_ofPred_eq] at cA

Goal state after:
case refine_1
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✝ : μ'.IsHaarMeasure
s : Set G
hs : MeasurableSet s
h's : μ.IsEverywherePos s
ν : Measure G := μ'.haarScalarFactor μ • μ
k : Set G
k_comp : IsCompact k
k_closed : IsClosed[inst✝⁷] k
k_mem : k ∈ 𝓝 1
one_k : 1 ∈ k
A : Set (Set G) := {t | t ⊆ s ∧ t.PairwiseDisjoint fun x ↦ x • k}
c : Set (Set G)
cA : ∀ x ∈ c, (∀ x_1 ∈ x, x_1 ∈ s) ∧ x.PairwiseDisjoint fun x ↦ x • k
hc : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
a : Set G
ac : a ∈ c
x : G
hx : x ∈ a
⊢ x ∈ s
Module: Mathlib.MeasureTheory.Covering.Besicovitch

Goal state before:
pp: α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
x : α
hx : x ∈ s
i : Fin N
y : ↑s
hxy : y ∈ u i
h' : x ∈ ball (↑y) (r ↑y)
⊢ x ∈ ⋃ i, s ∩ v i

Tactic:
refine mem_iUnion.2 ⟨i, ⟨hx, ?_⟩⟩

Goal state after:
α : Type u_1
inst✝⁴ : MetricSpace α
inst✝³ : SecondCountableTopology α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
s : Set α
r : α → ℝ
rpos : ∀ x ∈ s, 0 < r x
rle : ∀ x ∈ s, r x ≤ 1
hμs : 0 < μ s
h✝ : Nonempty α
Npos : N ≠ 0
o : Set α
so : s ⊆ o
omeas : MeasurableSet o
μo : μ o = μ s
a : BallPackage (↑s) α := { c := fun x ↦ ↑x, r := fun x ↦ r ↑x, rpos := ⋯, r_bound := 1, r_le := ⋯ }
u : Fin N → Set ↑s
hu : ∀ (i : Fin N), (u i).PairwiseDisjoint fun j ↦ closedBall (a.c j) (a.r j)
hu' : range a.c ⊆ ⋃ i, ⋃ j ∈ u i, ball (a.c j) (a.r j)
u_count : ∀ (i : Fin N), (u i).Countable
v : Fin N → Set α := fun i ↦ ⋃ x ∈ u i, closedBall (↑x) (r ↑x)
x : α
hx : x ∈ s
i : Fin N
y : ↑s
hxy : y ∈ u i
h' : x ∈ ball (↑y) (r ↑y)
⊢ x ∈ v i
Module: Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
hi : 2 < ‖a.c i‖
hij : ‖a.c i‖ ≤ ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
⊢ i ≠ ⊤

Tactic:
intro iN

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
N : ℕ
τ : ℝ
a : SatelliteConfig E N τ
lastc : a.c (last N) = 0
lastr : a.r (last N) = 1
hτ : 1 ≤ τ
δ : ℝ
hδ1 : τ ≤ 1 + δ / 4
i j : Fin N.succ
inej : i ≠ j
hi : 2 < ‖a.c i‖
hij : ‖a.c i‖ ≤ ‖a.c j‖
ah : Pairwise fun i j ↦ a.r i ≤ ‖a.c i - a.c j‖ ∧ a.r j ≤ τ * a.r i ∨ a.r j ≤ ‖a.c j - a.c i‖ ∧ a.r i ≤ τ * a.r j
δnonneg : 0 ≤ δ
hcrj : ‖a.c j‖ ≤ a.r j + 1
iN : i = ⊤
⊢ False
Module: Mathlib.Analysis.Calculus.ContDiff.Bounds

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
Bu_eq : (fun y ↦ (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y ↦ (B (f y)) (g y)) ∘ ⇑isoD
⊢ ‖Bu‖ ≤ ‖B‖

Tactic:
refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg B) fun y => ?_

Goal state after:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace 𝕜 D
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : ↑n ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := ⇑isoE.symm ∘ f ∘ ⇑isoD
gu : Du → Fu := ⇑isoF.symm ∘ g ∘ ⇑isoD
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G := ((B ∘SL ↑↑isoE).flip ∘SL ↑↑isoF).flip
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu := ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
hBu : Bu = ((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu)) ((compL 𝕜 Fu G Gu) ↑↑isoG.symm)) Bu₀
Bu_eq : (fun y ↦ (Bu (fu y)) (gu y)) = ⇑isoG.symm ∘ (fun y ↦ (B (f y)) (g y)) ∘ ⇑isoD
y : Eu
⊢ ‖Bu y‖ ≤ ‖B‖ * ‖y‖