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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i ↦ μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
convert! h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε) with i a

Goal state after:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
⊢ ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤ (∑ i ∈ s, f i ^ p) ^ (r / p) * (∑ i ∈ s, g i ^ q) ^ (r / q)

Tactic:
convert Lr_rpow_le_Lp_mul_Lq s f g hpqr with i hi
  · rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))]
  all_goals
    exact Eq.symm (abs_of_nonneg (by grind))

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ (∑ i ∈ s, w i * f i) / ↑(#s) ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ / ↑(#s)

Tactic:
gcongr

Goal state after:
case hab
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ExistsSeqTendstoAe.seqTendstoAeSeq hfg
S : ℕ → Set α := fun k ↦ {x | 2⁻¹ ^ k ≤ edist (f (ns k) x) (g x)}
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := limsup S atTop
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 2 ^ k ≤ 2 ^ (n + 1)

Tactic:
gcongr

Goal state after:
case ha
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ⋯
S : ℕ → Set α := ⋯
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := ⋯
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ 1 ≤ 2

case hmn
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
hfg : TendstoInMeasure μ f atTop g
h_lt_ε_real : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ k, 2 * 2⁻¹ ^ k < ε
ns : ℕ → ℕ := ⋯
S : ℕ → Set α := ⋯
hμS_le : ∀ (k : ℕ), μ (S k) ≤ 2⁻¹ ^ k
s : Set α := ⋯
hs : s = limsup S atTop
hμs : μ s = 0
x : α
ε : ℝ≥0∞
hε : ε > 0
N k : ℕ
hk_lt_ε : 2 * 2⁻¹ ^ k < ε
n : ℕ
hNx : edist (f (ns n) x) (g x) < 2⁻¹ ^ n
hn_ge : n ≥ max N (k - 1)
⊢ k ≤ n + 1
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 μ)
⊢ ↑↑((compLpₗ p μ (B (g + h))) f) =ᵐ[μ] ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f)

Tactic:
filter_upwards [(B (g + h)).coeFn_compLp f, (B g).coeFn_compLp f, (B h).coeFn_compLp f,
      Lp.coeFn_add ((B g).compLp f) ((B h).compLp f)] with x hx hg hh 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
⊢ ↑↑((compLpₗ p μ (B (g + h))) f) x = ↑↑((compLpₗ p μ (B g) + compLpₗ p μ (B h)) f) x
Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst✝² : SeminormedAddGroup E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
l : ℕ → ι
hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun i ↦ f (l i) x) atTop (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C

Tactic:
exact Lp.eLpNorm_le_of_ae_tendsto (hl.1.eventually bound) (fun n => hf (l n)) hl.2

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖ ≤ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖

Tactic:
gcongr

Goal state after:
case hab
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖a‖ ≤ ‖∏ i ∈ I, c i‖
Module: Mathlib.Topology.Algebra.Module.Multilinear.Bounded

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := { toNormedField := inst✝⁷, non_trivial := ⋯ }
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := I.piecewise (fun i ↦ c i • x i) x
i : ι
hi : i ∈ ↑I
⊢ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ * ‖c i‖ ≤ 1 * ‖c i‖

Tactic:
gcongr

Goal state after:
case hbc
ι : Type u_1
𝕜 : Type u_2
F : Type u_3
E : ι → Type u_4
inst✝⁷ : NormedField 𝕜
inst✝⁶ : (i : ι) → AddCommGroup (E i)
inst✝⁵ : (i : ι) → Module 𝕜 (E i)
inst✝⁴ : (i : ι) → TopologicalSpace (E i)
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace F
inst✝ : Nonempty ι
s : Set ((i : ι) → E i)
hs : IsVonNBounded 𝕜 s
f : ContinuousMultilinearMap 𝕜 E F
V : Set F
hV : V ∈ 𝓝 0
h₁ : ¬∀ (c : 𝕜), ‖c‖ ≤ 1
x✝ : NontriviallyNormedField 𝕜 := ⋯
I : Finset ι
t : (i : ι) → Set (E i)
ht₀ : ∀ (i : ι), t i ∈ 𝓝 0
hft : (↑I).pi t ⊆ ⇑f ⁻¹' V
c : ι → 𝕜
hc₀ : ∀ (i : ι), c i ≠ 0
hc : ∀ (i : ι) (c' : 𝕜), ‖c'‖ ≤ ‖c i‖ → ∀ x ∈ s, c' • x i ∈ t i
hc₀' : ∏ i ∈ I, c i ≠ 0
a : 𝕜
ha : a ∈ {y | ‖y‖ < ‖∏ i ∈ I, c i‖}
x : (i : ι) → E i
hx : x ∈ s
y : (i : ι) → E i := ⋯
i : ι
hi : i ∈ ↑I
⊢ ‖∏ i ∈ I, c i‖ / ‖∏ i ∈ I, c i‖ ≤ 1
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n‖⁻¹ * ‖c ^ n • x‖ ≤ ‖c ^ n‖⁻¹ * 1

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
𝕜₂ : Type u_3
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NontriviallyNormedField 𝕜₂
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
h : RingHomIsometric σ₁₂
f : E →ₛₗ[σ₁₂] F
hf : Filter.comap (⇑f) (𝓝 0) ≤ 𝓝 0
ε : ℝ≥0
ε0 : 0 < ↑ε
hε : ∀ (x : E), ‖f x‖ < ↑ε → ‖x‖ < 1
c : 𝕜
hc : 1 < ‖σ₁₂ c‖
x : E
hx : ¬f x = 0
hc₀ : c ≠ 0
n : ℤ
hlt : ‖f (c ^ n • x)‖ < ↑ε
hle : ‖c ^ n‖⁻¹ ≤ (↑ε)⁻¹ * ‖c‖ * ‖f x‖
⊢ ‖c ^ n • x‖ ≤ 1
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:
gcongr

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ * ‖x‖ * ‖y‖ ≤ max ‖f‖ 1 * ‖x‖ * ‖y‖

Tactic:
gcongr

Goal state after:
case hbc
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : SeminormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E
y : F
⊢ ‖f‖ ≤ max ‖f‖ 1
Module: Mathlib.Topology.Maps.Strict.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding f ↔ IsStrictMap f ∧ Injective f

Tactic:
refine ⟨fun H ↦ ⟨H.isStrictMap, H.injective⟩, fun ⟨f_strict, f_inj⟩ ↦ ?_⟩
  rw [isStrictMap_iff_isEmbedding_kerLift] at f_strict
  set Φ : Quotient (ker f) ≃ₜ X :=
    (Homeomorph.Quotient.congrRight <| by simp [f_inj.eq_iff]).trans Homeomorph.quotientBot
  exact f_strict.comp Φ.symm.isEmbedding

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: case mp
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x)) → AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ

pp: case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
· rintro ⟨g', g'meas, hg'⟩
    have A : MeasurableSet { x : α | f x ≠ 0 } := (hf (measurableSet_singleton 0)).compl
    refine ⟨fun x => (f x : ℝ) • g' x, hf.coe_nnreal_real.stronglyMeasurable.smul g'meas, ?_⟩
    apply @ae_of_ae_restrict_of_ae_restrict_compl _ _ _ { x | f x ≠ 0 }
    · rw [EventuallyEq, ae_withDensity_iff hf.coe_nnreal_ennreal] at hg'
      rw [ae_restrict_iff' A]
      filter_upwards [hg'] with a ha h'a
      have : (f a : ℝ≥0∞) ≠ 0 := by simpa only [Ne, ENNReal.coe_eq_zero] using h'a
      rw [ha this]
    · filter_upwards [ae_restrict_mem A.compl] with x hx
      simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at hx
      simp [hx]

Goal state after:
case mpr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x) • g x) μ → AEStronglyMeasurable g (μ.withDensity fun x ↦ ↑(f x))
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:
gcongr

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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c c' : E
⊢ indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')

Tactic:
by
  simp_rw [indicatorConstLp, ← MemLp.toLp_add, indicator_add]
  rfl

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:
rw [← inseparable_zero_iff_norm] at hi ⊢

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.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 : Inseparable (m i) 0
⊢ Inseparable (f m) 0

Tactic:
have : Inseparable (update m i 0) m := inseparable_pi.2 <|
    (forall_update_iff m fun i a ↦ Inseparable a (m i)).2 ⟨hi.symm, fun _ _ ↦ rfl⟩

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
this : Inseparable (update m i 0) m
⊢ Inseparable (f m) 0
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:
rwa [IntegrableOn, μ.restrict_restrict_of_subset inter_subset_right] at this

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0
⊢ Integrable f (c • μ)

Tactic:
apply h.smul_measure

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0
⊢ ↑c ≠ ∞
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
⊢ Integrable f ((μ univ)⁻¹ • μ)

Tactic:
apply h.smul_measure

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
⊢ (μ univ)⁻¹ ≠ ∞
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 ∘ e) (e ⁻¹' s) (Measure.comap e μ)

Tactic:
by
  simp_rw [← he.integrableOn_map_iff, he.map_comap, IntegrableOn,
    Measure.restrict_restrict_of_subset hs]

Goal state after:
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 : α ≃ᵐ β
f : β → ε
μ : Measure α
s : Set β
⊢ IntegrableOn f s (Measure.map (⇑e) μ) ↔ IntegrableOn (f ∘ ⇑e) (⇑e ⁻¹' s) μ

Tactic:
by
  simp only [IntegrableOn, e.restrict_map, integrable_map_equiv e]

Goal state after:
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:
gcongr

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

Goal state before:
pp: case inr
𝕜 : 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
⊢ ∏ _x, ε / ‖c‖ ≤ ∏ i, ‖m i‖

Tactic:
gcongr

Goal state after:
case h1
𝕜 : 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
hf : Continuous[Pi.topologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ⇑f
h✝ : Nonempty ι
ε : ℝ
ε0 : 0 < ε
hε : ∀ (m : (i : ι) → E i), ‖m‖ < ε → ‖f m‖ < 1
c : 𝕜
hc : 1 < ‖c‖
this : 0 < (‖c‖ / ε) ^ Fintype.card ι
m : (i : ι) → E i
hcm : ∀ (i : ι), ε / ‖c‖ ≤ ‖m i‖
hm : ∀ (i : ι), ‖m i‖ < ε
_x : ι
a✝ : _x ∈ univ
⊢ ε / ‖c‖ ≤ ‖m _x‖
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable (fun x ↦ (f x).toNNReal • g x) μ ↔ Integrable (fun x ↦ (f x).toReal • g x) μ

Tactic:
NNReal.smul_def,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
hf : Measurable f
hflt : ∀ᵐ (x : α) ∂μ, f x < ∞
g : α → E
⊢ Integrable (fun x ↦ ↑(f x).toNNReal • g x) μ ↔ Integrable (fun x ↦ (f x).toReal • g x) μ
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ Integrable g (μ.withDensity fun x ↦ ↑(f x)) ↔ Integrable g (μ.withDensity fun x ↦ ↑(AEMeasurable.mk f hf x))

Tactic:
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by
        rw [withDensity_congr_ae this]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → E
⊢ (fun x ↦ ↑(f x)) =ᵐ[μ] fun x ↦ ↑(AEMeasurable.mk f hf x)
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 : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)
⊢ (C * ∑ i, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤
    C * ∑ _i, ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)

Tactic:
gcongr

Goal state after:
case h
𝕜 : 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 : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
A :
  ∀ (i : ι),
    (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)
i : ι
a✝ : i ∈ univ
⊢ (∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) ≤ ‖m₁ - m₂‖ * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1)