mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case pos
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst✝³] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ IntegrableOn f u (μ.restrict s)

Tactic:
IntegrableOn,

Goal state after:
case pos
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∈ s
t : Set X
ht_nhds : t ∈ 𝓝[s] x
ht_int : IntegrableOn f t μ
u : Set X
hu_o : IsOpen[inst✝³] u
hu_x : x ∈ u
hu_sub : u ∩ s ⊆ t
⊢ Integrable f ((μ.restrict s).restrict u)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableOn f sᶜ (μ.restrict s)

Tactic:
IntegrableOn,

Goal state after:
case neg
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ Integrable f ((μ.restrict s).restrict sᶜ)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ IntegrableOn f U μ

Tactic:
IntegrableOn,

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
p : ℝ≥0∞
hf : MemLp f p μ
hp : 1 ≤ p
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : μ U < ∞
this : Fact (μ U < ∞)
⊢ Integrable f (μ.restrict U)
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹⁰ : Fintype ι'
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ ‖{ toFun := fun f ↦ g.compContinuousLinearMap f, map_update_add' := ⋯, map_update_smul' := ⋯ } f‖ ≤ ‖g‖ * ∏ i, ‖f i‖

Tactic:
simp [norm_compContinuousLinearMap_le]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ

Tactic:
by
  refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩
  obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc
  rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]
  exact ⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
⊢ integral 0 = 0

Tactic:
by
  simp only [integral]
  exact map_zero integralCLM

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ↥(Lp E 1 μ)
⊢ integral (f - g) = integral f - integral g

Tactic:
simp only [integral]
  exact map_sub integralCLM f g

Goal state after:
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inr.inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.univ.Nonempty
⊢ ∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
      (T (⇑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T Set.univ) x

Tactic:
have hα := hs_empty.to_type

Goal state after:
case inr.inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
x : F
hs : MeasurableSet Set.univ
hs_empty : Set.univ.Nonempty
hα : Nonempty α
⊢ ∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
      (T (⇑(piecewise Set.univ hs (const α x) (const α 0)) ⁻¹' {x_1})) x_1 =
    (T Set.univ) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x

Tactic:
have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _

Goal state after:
case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = (T Set.univ) x
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (x : α) in l, v x = 0 ∧ u x ≠ 0
⊢ False

Tactic:
replace h : ∃ᶠ t in l, (u / v) t = 0 := h.mono fun x ⟨hv, hu⟩ ↦ by simp [hv]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
huv : Tendsto (u / v) l (𝓝 1)
h : ∃ᶠ (t : α) in l, (u / v) t = 0
⊢ False
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : IsBigOWith C l u v
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖

Tactic:
rw [IsBigOWith] at hCuv

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
huv : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c * ‖v x‖
φ : α → 𝕜
hφ : Tendsto φ l (𝓝 1)
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
⊢ c / 2 / C * ‖u x‖ ≤ c / 2 / C * (C * ‖v x‖)

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : ClosedIciTopology E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᵐ[μ] g
⊢ ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

Tactic:
by
  rw [← sub_nonneg, ← integral_sub hg hf]
  refine integral_nonneg_of_ae ?_
  filter_upwards [h] with x hx
  simpa

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| fun x ↦ v x + w x

Tactic:
x

Goal state after:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
x : α
| v x + w x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_toReal.aestronglyMeasurable,
    lintegral_congr_ae (ofReal_toReal_ae_eq hf)]
  exact Eventually.of_forall fun x => ENNReal.toReal_nonneg

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_2
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝¹² : Ring R
inst✝¹¹ : AddCommGroup V
inst✝¹⁰ : Module R V
inst✝⁹ : TopologicalSpace P
inst✝⁸ : AddTorsor V P
inst✝⁷ : AddCommGroup W
inst✝⁶ : Module R W
inst✝⁵ : TopologicalSpace Q
inst✝⁴ : AddTorsor W Q
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ f x✝ = (const R P q) x✝

Tactic:
· rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ (eLpNorm (⇑(toSimpleFunc f)) 1 μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖

Tactic:
eLpNorm_one_eq_lintegral_enorm

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] G)
⊢ (∫⁻ (x : α), ‖(toSimpleFunc f) x‖ₑ ∂μ).toReal = ∑ x ∈ (toSimpleFunc f).range, μ.real (⇑(toSimpleFunc f) ⁻¹' {x}) * ‖x‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : f z = ↑‖z‖ / ↑r * f z₁
⊢ ‖↑‖z‖ / ↑r‖ * ‖f z₁‖ ≤ c / r * ‖z‖

Tactic:
norm_div,

Goal state after:
case neg
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ z ∈ sphere 0 r, ‖f z‖ ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := (↑r * (↑‖z‖)⁻¹) • z
hz₁ : z₁ = (↑r * (↑‖z‖)⁻¹) • z
norm_f_z₁ : ‖f z₁‖ ≤ c
r_ne_zero : ↑r ≠ 0
eq : f z = ↑‖z‖ / ↑r * f z₁
⊢ ‖↑‖z‖‖ / ‖↑r‖ * ‖f z₁‖ ≤ c / r * ‖z‖
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
y' : E := d⁻¹ • y
yy' : y = d • y'
⊢ ‖c‖ / R * (R / ‖c‖) ≤ ‖c‖ / R * ‖d • x‖

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
· simp_rw [setToFun_undef _ hf]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖

Tactic:
exact ae_of_all _ fun _ ↦ by positivity

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T s = T' s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
· simp_rw [setToFun_undef _ hf]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : IntegrableOn f s μ
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)

Tactic:
IntegrableOn,

Goal state after:
X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
μ : Measure X
f : X → E
s : Set X
hs : s.Countable
hf : Integrable f (μ.restrict s)
hi : Countable { x // x ∈ s }
⊢ Integrable (fun x ↦ f ↑x) (Measure.comap Subtype.val μ)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ∫ (a : α), ‖↑↑(Integrable.toL1 f hf) a‖ ∂μ = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
exact integral_congr_ae <| hf.coeFn_toL1.fun_comp _

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type w
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
fL : E →L[𝕜] F := LinearMap.toContinuousLinearMap f.linear
x y : PE
⊢ ‖f.linear (x -ᵥ y)‖ ≤ ↑‖fL‖₊ * ‖x -ᵥ y‖

Tactic:
exact fL.le_opNorm _

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : Integrable f (Measure.map φ μ)
s : Set β
⊢ ∀ (x : G), MeasurableSet s → (weightedSMul (Measure.map φ μ) s) x = (weightedSMul μ (φ ⁻¹' s)) x

Tactic:
x

Goal state after:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : Integrable f (Measure.map φ μ)
s : Set β
x : G
⊢ MeasurableSet s → (weightedSMul (Measure.map φ μ) s) x = (weightedSMul μ (φ ⁻¹' s)) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
⊢ ∫ (x : α) in s, f x ∂Measure.dirac a = if a ∈ s then f a else 0

Tactic:
by
  rw [restrict_dirac' hs]
  split_ifs
  · exact integral_dirac' _ _ hf
  · exact integral_zero_measure _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
⊢ ∀ (x : α), dist (f x) (g x) < C

Tactic:
x

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝ : CompactSpace α
C0 : 0 < C
w : dist f g < C
x : α
⊢ dist (f x) (g x) < C
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ setToFun μ T hT ↑↑f

Tactic:
simp_rw [L1.setToFun_eq_setToL1 hT]

Goal state after:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ (L1.setToL1 hT) f
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
⊢ Integrable f μ

Tactic:
have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
i : ι
hi : ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ < 1
h'i : Integrable (fs i) μ
this : Integrable (fs i - f) μ
⊢ Integrable f μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty α
f : α →ᵇ β
M : ℝ
⊢ ‖f‖ ≤ M ↔ ∀ (x : α), ‖f x‖ ≤ M

Tactic:
simp_rw [norm_def, ← dist_zero_right]
  exact dist_le_iff_of_nonempty

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(n • f) = Int.ofNat n • ⇑f

Tactic:
Int.ofNat_eq_natCast,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(n • f) = ↑n • ⇑f
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SeminormedAddCommGroup β
f✝ g : α →ᵇ β
x : α
C : ℝ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
c : 𝕜
f : α →ᵇ β
⊢ ∀ (x : α), ‖(c • ⇑f.toContinuousMap) x‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact fun x =>
      norm_smul c (f x) ▸ mul_le_mul_of_nonneg_left (f.norm_coe_le_norm _) (norm_nonneg _)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
⊢ ∀ (x y : α →ᵇ β), (x + y).compContinuous g = x.compContinuous g + y.compContinuous g

Tactic:
by intros; ext; simp

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜✝ : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SeminormedAddCommGroup β
f g✝ : α →ᵇ β
x : α
C : ℝ
inst✝⁴ : NontriviallyNormedField 𝕜✝
inst✝³ : NormedSpace 𝕜✝ β
𝕜 : Type u_2
inst✝² : TopologicalSpace γ
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 β
g : C(γ, α)
⊢ ∀ (m : 𝕜) (x : α →ᵇ β), (m • x).compContinuous g = (RingHom.id 𝕜) m • x.compContinuous g

Tactic:
by intros; ext; simp

Goal state after: