awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
g : G → E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : CompleteSpace E'
f : G → ℝ
x₀ : G
R ε : ℝ
z₀ : E'
hε : 0 ≤ ε
hf : support f ⊆ ball 0 R
hnf : ∀ (x : G), 0 ≤ f x
hintf : Eq (α := ℝ) (∫ (x : G), f x ∂μ) 1
hmg : AEStronglyMeasurable g μ
hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε
hif : Integrable f μ
⊢ norm.{uE'} (E := ℝ →L[ℝ] E' →L[ℝ] E') (lsmul ℝ ℝ) * ε ≤ ε

Tactic:
exact (mul_le_mul_of_nonneg_right opNorm_lsmul_le hε).trans_eq (one_mul ε)

Premises used: LE.le.trans_eq, mul_le_mul_of_nonneg_right, ContinuousLinearMap.opNorm_lsmul_le, one_mul
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hφ : Tendsto.{u_1, uG} (β := Set G) (fun (n : ι) ↦ support (φ n)) l (smallSets (𝓝 0))
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)
hk : Tendsto k l (𝓝 x₀)
⊢ ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t

Tactic:
simp_rw [tendsto_smallSets_iff] at hφ

Premises used: Filter.tendsto_smallSets_iff
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : Tendsto (uncurry g) (l ×ˢ 𝓝 x₀) (𝓝 z₀)
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
rw :
  ∀ (hcg : ∀ ε > 0, ∀ᶠ (x : ι × G) in l ×ˢ 𝓝 x₀, dist (uncurry g x) z₀ < ε) (hk : Tendsto k l (𝓝 x₀))
    (hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t),
    ∀ ε > 0, ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
⊢ Tendsto (fun (i : ι) ↦ (φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) l (𝓝 z₀)

Tactic:
rw [Metric.tendsto_nhds] at hcg ⊢

Premises used: Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hcg : ∀ ε > 0, ∀ᶠ (x : ι × G) in l ×ˢ 𝓝 x₀, dist (uncurry g x) z₀ < ε
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
⊢ ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε

Tactic:
simp_rw [Metric.eventually_prod_nhds_iff] at hcg

Premises used: Metric.eventually_prod_nhds_iff
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (i : ι) in l, pa i) ∧ ∃ ε_1 > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : G⦄, dist x x₀ < ε_1 → dist (uncurry g (i, x)) z₀ < ε
ε : ℝ
hε : ε > 0
⊢ LT.lt (α := ℝ) 0 3

Tactic:
simp
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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:
have h2ε : 0 < ε / 3 := div_pos hε (by simp)
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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
obtain :
  ∀ (p : ι → Prop) (hp : ∀ᶠ (i : ι) in l, p i) (δ : ℝ) (hδ : δ > 0)
    (hgδ : ∀ ⦃i : ι⦄, p i → ∀ ⦃x : G⦄, dist x x₀ < δ → dist (uncurry g (i, x)) z₀ < ε / 3),
    ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε
⊢ ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε

Tactic:
obtain ⟨p, hp, δ, hδ, hgδ⟩ := hcg _ h2ε
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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
⊢ ∀ᶠ (x : ι) in l, dist (k x) x₀ < δ / 2

Tactic:
have h2k := hk.eventually (ball_mem_nhds x₀ <| half_pos hδ)
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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
⊢ ∀ᶠ (x : ι) in l, support (φ x) ⊆ ball 0 (δ / 2)

Tactic:
have h2φ := hφ (ball (0 : G) _) <| ball_mem_nhds _ (half_pos hδ)
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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)
h :
  ∀ (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 : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1) (hmgi : AEStronglyMeasurable (g i) μ),
    dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) z₀ < ε
⊢ ∀ᶠ (x : ι) in l, dist ((φ x ⋆[lsmul ℝ ℝ, μ] g x) (k x)) z₀ < ε

Tactic:
filter_upwards [hp, h2k, h2φ, hnφ, hiφ, hmg] with i hpi hki hφi hnφi hiφi hmgi
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
⊢ dist (g i (k i)) z₀ < ε / 3

Tactic:
have hgi : dist (g i (k i)) z₀ < ε / 3 := hgδ hpi (hki.trans <| half_lt_self hδ)
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (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)
⊢ dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3

Tactic:
(dist_triangle_right _ _ _).trans (add_le_add (hgδ hpi ?_).le hgi.le)

Premises used: add_le_add, dist_triangle_right, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (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)
refine : dist x' x₀ < δ
⊢ dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3

Tactic:
refine (dist_triangle_right _ _ _).trans (add_le_add (hgδ hpi ?_).le hgi.le)

Premises used: add_le_add, dist_triangle_right, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (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)
⊢ dist x' x₀ < δ

Tactic:
((dist_triangle _ _ _).trans_lt (add_lt_add hx'.out hki)).trans_eq (add_halves δ)

Premises used: dist_triangle, Membership.mem.out, add_halves, LT.lt.trans_eq, add_lt_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (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)
⊢ dist x' x₀ < δ

Tactic:
exact ((dist_triangle _ _ _).trans_lt (add_lt_add hx'.out hki)).trans_eq (add_halves δ)

Premises used: dist_triangle, Membership.mem.out, add_halves, LT.lt.trans_eq, add_lt_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
⊢ ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3

Tactic:
have h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3 := by
    intro x' hx'
    refine (dist_triangle_right _ _ _).trans (add_le_add (hgδ hpi ?_).le hgi.le)
    exact ((dist_triangle _ _ _).trans_lt (add_lt_add hx'.out hki)).trans_eq (add_halves δ)
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3
⊢ dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) (g i (k i)) ≤ ε / 3 + ε / 3

Tactic:
have := dist_convolution_le (add_pos h2ε h2ε).le hφi hnφi hiφi hmgi h1
-- Module: Mathlib.Analysis.Convolution
Goal:
G : Type uG
E' : Type uE'
inst : NormedAddCommGroup E'
inst_1 : MeasurableSpace G
μ : Measure G
inst_2 : SeminormedAddCommGroup G
inst_3 : BorelSpace G
inst_4 : SecondCountableTopology G
inst_5 : μ.IsAddLeftInvariant
inst_6 : SFinite μ
inst_7 : NormedSpace ℝ E'
inst_8 : 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, Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmg : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (g i) μ
hk : Tendsto k l (𝓝 x₀)
hφ : ∀ (t : Set G), Membership.mem (γ := Filter G) (𝓝 0) t → ∀ᶠ (x : ι) in l, support (φ x) ⊆ t
hcg :
  ∀ ε > 0,
    ∃ (pa : ι → Prop),
      (∀ᶠ (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 : Eq (α := ℝ) (∫ (x : G), φ i x ∂μ) 1
hmgi : AEStronglyMeasurable (g i) μ
hgi : dist (g i (k i)) z₀ < ε / 3
h1 : ∀ x' ∈ ball (k i) (δ / 2), dist (g i x') (g i (k i)) ≤ ε / 3 + ε / 3
this : dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) (g i (k i)) ≤ ε / 3 + ε / 3
⊢ dist ((φ i ⋆[lsmul ℝ ℝ, μ] g i) (k i)) z₀ < ε

Tactic:
((dist_triangle _ _ _).trans_lt (add_lt_add_of_le_of_lt this hgi)).trans_eq ?_

Premises used: dist_triangle, add_lt_add_of_le_of_lt, LT.lt.trans_eq, LE.le.trans_lt