mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ p₁ ^ w₁ * p₂ ^ w₂ = w₁ * p₁ + w₂ * p₂ ↔ w₁ = 0 ∨ w₂ = 0 ∨ p₁ = p₂

Tactic:
have := geom_mean_eq_arith_mean_weighted_iff_of_nonneg univ ![w₁, w₂] ![p₁, p₂]
  simp at this
  grind

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Goal state before:
pp: α : Type u_1
ε : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
μ : Measure α
p δ : ℝ≥0∞
hδ : δ ≠ 0
this : Tendsto (fun η ↦ p.LpAddConst * (η + η)) (𝓝[>] 0) (𝓝 0)
η : ℝ≥0∞
hη : p.LpAddConst * (η + η) < δ
ηpos : 0 < η
f g : α → ε
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
Hf : eLpNorm f p μ ≤ η
Hg : eLpNorm g p μ ≤ η
⊢ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ) ≤ p.LpAddConst * (η + η)

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: α : Type u_1
ε : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → ε
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ
hq_pos : 0 < q
h_nnnorm_le_eLpNorm_ess_sup : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
x : α
hx : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ‖f x‖ₑ ^ q ≤ eLpNormEssSup f μ ^ q

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ (∑ x ∈ s, w x / n / z x)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
convert! this

Goal state after:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : (∑ i ∈ s, w i / n / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (w i / n)
⊢ (∏ i ∈ s, z i ^ w i) ^ n⁻¹ = ∏ i ∈ s, z i ^ (w i / n)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp

Goal state before:
pp: case cons
ι : Type u_1
α : Type u_2
𝕜 : Type u_3
x✝ : MeasurableSpace α
inst✝ : NormedCommRing 𝕜
μ : Measure α
f : ι → α → 𝕜
p : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : (∀ i ∈ s, MemLp (f i) (p i) μ) → MemLp (∏ i ∈ s, f i) (∑ i ∈ s, (p i)⁻¹)⁻¹ μ
hf : ∀ i_1 ∈ cons i s hi, MemLp (f i_1) (p i_1) μ
⊢ MemLp (∏ i ∈ cons i s hi, f i) (∑ i ∈ cons i s hi, (p i)⁻¹)⁻¹ μ

Tactic:
rw [prod_cons]
    exact (ih <| forall_of_forall_cons hf).mul (hf i <| mem_cons_self ..) (hpqr := ⟨by simp⟩)

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : ↥(Lp E p μ)
g : ↥(Lp F p μ)
h : ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
⊢ (eLpNorm (↑↑f) p μ).toReal ≤ (eLpNorm (↑↑g) p μ).toReal

Tactic:
exact ENNReal.toReal_mono (by finiteness) (eLpNorm_mono_ae h)

Goal state after:
Module: Mathlib.MeasureTheory.Function.LpSpace.Basic

Goal state before:
pp: α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hh : ↑↑((B h).compLp f) x = (B h) (↑↑f x)
hadd : ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x
⊢ ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) x

Tactic:
simp only [compLpₗ_apply, LinearMap.add_apply, hx, hadd]

Goal state after:
α : Type u_1
𝕜✝ : Type u_2
𝕜'✝ : Type u_3
E : Type u_4
F✝ : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup F✝
g✝ : E → F✝
c : ℝ≥0
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NontriviallyNormedField 𝕜'
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' F✝
σ : 𝕜 →+* 𝕜'
inst✝⁴ : RingHomIsometric σ
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
B : G →L[𝕜] E →L[𝕜] F
g h : G
f : ↥(Lp E p μ)
x : α
hx : ↑↑((B (g + h)).compLp f) x = (B (g + h)) (↑↑f x)
hg : ↑↑((B g).compLp f) x = (B g) (↑↑f x)
hh : ↑↑((B h).compLp f) x = (B h) (↑↑f x)
hadd : ↑↑((B g).compLp f + (B h).compLp f) x = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x
⊢ (B (g + h)) (↑↑f x) = (↑↑((B g).compLp f) + ↑↑((B h).compLp f)) x
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_3
inst✝ : NormedAddCommGroup E
hp : 1 ≤ p
f : ℕ → α → E
hf : ∀ (n : ℕ), MemLp (f n) p μ
f_lim : α → E
h_lim_meas : AEStronglyMeasurable f_lim μ
h_tendsto : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - f_lim) p μ ≤ ε
N : ℕ
h_tendsto_1 : eLpNorm (f N - f_lim) p μ ≤ 1
h_add : f_lim = f_lim - f N + f N
⊢ eLpNorm (f_lim - f N) p μ < ∞

Tactic:
refine lt_of_le_of_lt ?_ ENNReal.one_lt_top
    have h_neg : f_lim - f N = -(f N - f_lim) := by simp
    rwa [h_neg, eLpNorm_neg]

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.Units

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
I : Ideal R
hI : I ≠ ⊤
⊢ I.closure ≠ ⊤

Tactic:
have h := closure_minimal (coe_subset_nonunits hI) nonunits.isClosed
  simpa only [I.closure.eq_top_iff_one, Ne] using! mt (@h 1) one_notMem_nonunits

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
ι : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁴ : RingHomIsometric σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
f : ι → E →SL[σ₁₂] F
tfae_1_to_3 : EquicontinuousAt (DFunLike.coe ∘ f) 0 → UniformEquicontinuous (DFunLike.coe ∘ f)
tfae_3_to_2 : UniformEquicontinuous (DFunLike.coe ∘ f) → Equicontinuous (DFunLike.coe ∘ f)
tfae_2_to_1 : Equicontinuous (DFunLike.coe ∘ f) → EquicontinuousAt (DFunLike.coe ∘ f) 0
C₁ C₂ : ℝ
hC : C₁ ≤ C₂
i : ι
x : E
⊢ C₁ * ‖x‖ ≤ C₂ * ‖x‖

Tactic:
by gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : U ∈ 𝓝 0
c : 𝕜
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : ContinuousMultilinearMap 𝕜 E F
hf : f ∈ S
⊢ ∀ y ∈ s, f y ∈ c • U

Tactic:
x

Goal state after:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝⁸ : NormedField 𝕜
inst✝⁷ : (i : ι) → TopologicalSpace (E i)
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : AddCommGroup F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
S : Set (ContinuousMultilinearMap 𝕜 E F)
hS : IsVonNBounded 𝕜 S
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
U : Set F
hU : U ∈ 𝓝 0
c : 𝕜
hc : S ⊆ c • {x | MapsTo (⇑x) s U}
f : ContinuousMultilinearMap 𝕜 E F
hf : f ∈ S
x : (i : ι) → E i
⊢ x ∈ s → f x ∈ c • U
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
g : Y → Z
f_quot : IsQuotientMap f
Φ : ↑(range (g ∘ f)) ≃ₜ ↑(range g) := Homeomorph.setCongr ⋯
key : rangeFactorization g ∘ f = ⇑Φ ∘ rangeFactorization (g ∘ f)
⊢ IsQuotientMap (⇑Φ ∘ rangeFactorization (g ∘ f)) ↔ IsQuotientMap (rangeFactorization (g ∘ f))

Tactic:
exact ⟨fun H ↦ by simpa using! Φ.symm.isQuotientMap.comp H, fun H ↦ Φ.isQuotientMap.comp H⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
μ : Measure α
f : β → Set α
a✝ : β
s✝ : Finset β
hx : a✝ ∉ s✝
IH : μ.real (⋃ b ∈ s✝, f b) ≤ ∑ p ∈ s✝, μ.real (f p)
⊢ μ.real (f a✝) + μ.real (⋃ x ∈ s✝, f x) ≤ μ.real (f a✝) + ∑ p ∈ s✝, μ.real (f p)

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable f μ ∧ eLpNorm f 1 μ < ∞ ↔ AEStronglyMeasurable f μ ∧ ∫⁻ (a : α), ‖f a‖ₑ ∂μ < ∞

Tactic:
eLpNorm_one_eq_lintegral_enorm

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
m : (i : ι) → E i
i : ι
hi : ‖m i‖ = 0
⊢ ‖f m‖ = 0

Tactic:
← inseparable_zero_iff_norm

Goal state after:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝² : (i : ι) → NormedSpace 𝕜 (E i)
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : MultilinearMap 𝕜 E G
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
m : (i : ι) → E i
i : ι
hi : Inseparable (m i) 0
⊢ Inseparable (f m) 0
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
⊢ IntegrableOn f univ μ ↔ Integrable f μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
⊢ Integrable f (μ.restrict univ) ↔ Integrable f μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
⊢ IntegrableOn (fun x ↦ C) s μ ↔ ‖C‖ₑ = 0 ∨ μ s < ∞

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
C : ε'
hC : ‖C‖ₑ ≠ ∞
⊢ Integrable (fun x ↦ C) (μ.restrict s) ↔ ‖C‖ₑ = 0 ∨ μ s < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
this : IntegrableOn f (s ∩ t) (μ.restrict t)
⊢ IntegrableOn f (s ∩ t) μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
h : IntegrableOn f s (μ.restrict t)
this : Integrable f ((μ.restrict t).restrict (s ∩ t))
⊢ IntegrableOn f (s ∩ t) μ
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
f : α → ε'
x : α
inst✝ : MeasurableSingletonClass α
hfx : ‖f x‖ₑ ≠ ∞
this : f =ᵐ[μ.restrict {x}] fun x_1 ↦ f x
⊢ Integrable f (μ.restrict {x}) ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
⊢ IntegrableOn f s (Measure.map e μ) ↔ IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
⊢ Integrable f ((Measure.map e μ).restrict s) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ⊆ range e
⊢ IntegrableOn f s μ ↔ IntegrableOn f s (μ.restrict (range e))

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
β : Type u_2
ε : Type u_3
mα : MeasurableSpace α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure β
s : Set β
hs : s ⊆ range e
⊢ Integrable f (μ.restrict s) ↔ Integrable f ((μ.restrict (range e)).restrict s)
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
⊢ Integrable (g + f) μ ↔ Integrable g μ

Tactic:
by
  rw [add_comm, integrable_add_iff_integrable_right hf]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ ↔ IntegrableOn f s μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ Integrable (s.indicator f) μ ↔ Integrable f (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ IntegrableOn (fun x ↦ c) s μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
⊢ Integrable (fun x ↦ c) (μ.restrict s)
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ IntegrableOn (s.indicator f) t μ ↔ IntegrableOn f (s ∩ t) μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ Integrable (s.indicator f) (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ IntegrableOn f s (μ.restrict t) ↔ Integrable f (μ.restrict (s ∩ t))

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s t : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hs : MeasurableSet s
⊢ Integrable f ((μ.restrict t).restrict s) ↔ Integrable f (μ.restrict (s ∩ t))
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ IntegrableOn f v μ

Tactic:
IntegrableOn,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s t : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
ht : NullMeasurableSet t μ
h't : ∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0
u : Set α := {x | x ∈ s ∧ f x ≠ 0}
hu : IntegrableOn f u μ
v : Set α := toMeasurable μ u
⊢ Integrable f (μ.restrict v)
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f₀ f₁ : α → β
g : α → ℝ
hf₁_m : AEStronglyMeasurable f₁ μ
hf₀_i : Integrable f₀ μ
hg_i : Integrable g μ
h : ∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a
a : α
ha : ‖f₀ a - f₁ a‖ ≤ g a
⊢ ‖f₀ a‖ + ‖f₀ a - f₁ a‖ ≤ ‖f₀ a‖ + g a

Tactic:
by gcongr

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable g μ

Tactic:
← indicator_add_eq_right h

Goal state after:
case refine_2
α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
hfg : Integrable (f + g) μ
⊢ Integrable ((support g).indicator (f + g)) μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : MultilinearMap 𝕜 E G
C : ℝ
D : ℝ := max C 1
D_pos : 0 ≤ D
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ D * ∏ i, ‖m i‖
m m' : (i : ι) → E i
h' : dist m' m < 1
this : max ‖m'‖ ‖m‖ ≤ ‖m‖ + 1
⊢ D * ↑(Fintype.card ι) * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ ≤
    D * ↑(Fintype.card ι) * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ AEStronglyMeasurable (fun x ↦ (f x).toReal) μ ∧ eLpNorm (fun x ↦ (f x).toReal) 1 μ < ∞

Tactic:
eLpNorm_one_eq_lintegral_enorm

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ AEStronglyMeasurable (fun x ↦ (f x).toReal) μ ∧ ∫⁻ (x : α), ‖(f x).toReal‖ₑ ∂μ < ∞
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
n : ℕ
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1

Tactic:
refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebraFin_apply, one_mul, List.ofFn_eq_map,
    Fin.prod_univ_def]
  refine (List.norm_prod_le' ?_).trans_eq ?_
  · rw [Ne, List.map_eq_nil_iff, List.finRange_eq_nil_iff]
    exact Nat.succ_ne_zero _
  rw [List.map_map, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
ha : ‖f a‖ₑ ≠ ∞
⊢ μ {a} ≠ ∞

Tactic:
rw [measure_singleton]

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
ha : ‖f a‖ₑ ≠ ∞
⊢ 0 ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ μ {b} ≠ ∞

Tactic:
rw [measure_singleton]

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ 0 ≠ ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ μ {b} ≠ ∞

Tactic:
rw [measure_singleton]

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁵ : PartialOrder α
inst✝⁴ : MeasurableSingletonClass α
inst✝³ : TopologicalSpace ε'
inst✝² : ESeminormedAddMonoid ε'
inst✝¹ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
b : α
inst✝ : NullSingletonClass μ
hb : ‖f b‖ₑ ≠ ∞
⊢ 0 ≠ ∞
Module: Mathlib.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
hc_ne : c ≠ 0
F : Set Eᵤ
hF_finite : F.Finite
hF_cover : U ⊆ ⋃ y ∈ F, y +ᵥ c • U
M : Submodule 𝕜 Eᵤ := Submodule.span 𝕜 F
this : FiniteDimensional 𝕜 ↥M := Finite.span_of_finite 𝕜 hF_finite
h_cover : U ⊆ ↑M + c • U
n : ℕ
ih : U ⊆ ↑M + c ^ n • U
⊢ ↑M + c ^ n • U ⊆ ↑M + c ^ n • (↑M + c • U)

Tactic:
by gcongr

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.AEEqFun

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : ↥(Lp β 1 μ)
⊢ dist f g = (∫⁻ (a : α), edist (↑↑f a) (↑↑g a) ∂μ).toReal

Tactic:
simp_rw [dist_edist, edist_def]

Goal state after: