mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case mpr
𝕜 : 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
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
⊢ ∃ p,
    Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] ⇑p ∧
      ∀ (k : ι), (normSeminorm 𝕜₂ F).comp ↑(f k) ≤ p

Tactic:
refine ⟨C.toNNReal • normSeminorm 𝕜 E,
        ((norm_withSeminorms 𝕜 E).continuous_seminorm 0).const_smul C.toNNReal, fun i x ↦ ?_⟩

Goal state after:
case mpr
𝕜 : 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
tfae_4_iff_5 : (∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
tfae_5_iff_7 : (∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖) ↔ ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C
tfae_7_iff_8 : (∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_6_iff_8 : (∃ C, ∀ (i : ι), ‖f i‖ ≤ C) ↔ BddAbove (Set.range fun x ↦ ‖f x‖)
tfae_8_iff_9 : BddAbove (Set.range fun x ↦ ‖f x‖) ↔ ⨆ i, ↑‖f i‖₊ < ⊤
C : ℝ
hC : ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖
i : ι
x : E
⊢ ((normSeminorm 𝕜₂ F).comp ↑(f i)) x ≤ (C.toNNReal • normSeminorm 𝕜 E) x
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✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝¹⁴, non_trivial := ⋯ }
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]

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✝⁸ : UniformSpace F
inst✝⁷ : IsUniformAddGroup F
𝕜' : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜'
inst✝⁵ : NormedAlgebra 𝕜' 𝕜
inst✝⁴ : (i : ι) → Module 𝕜' (E i)
inst✝³ : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)
inst✝² : Module 𝕜' F
inst✝¹ : IsScalarTower 𝕜' 𝕜 F
inst✝ : ∀ (i : ι), ContinuousSMul 𝕜 (E i)
this : NontriviallyNormedField 𝕜 := { toNormedField := inst✝¹⁴, non_trivial := ⋯ }
⊢ IsUniformEmbedding (toUniformOnFun ∘ restrictScalars 𝕜')
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h : μ s ≠ ∞
⊢ μ.real s = 0 ↔ μ s = 0

Tactic:
rw [Measure.real, ENNReal.toReal_eq_zero_iff]
  exact or_iff_left h

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

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s : Set α
μ : Measure α
C : ℝ
hs : μ s < ∞
hf : ∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
⊢ (μ.restrict s) univ < ∞

Tactic:
by rwa [Measure.restrict_apply_univ]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᵐ[μ] f
hg : 0 ≤ᵐ[μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
⊢ 0 a ≤ g a → ‖f a‖ ≤ (f + g) a

Tactic:
hag

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h_meas : AEStronglyMeasurable f μ
hf : 0 ≤ᵐ[μ] f
hg : 0 ≤ᵐ[μ] g
h_int : Integrable (f + g) μ
a : α
haf : 0 a ≤ f a
hag : 0 a ≤ g a
⊢ ‖f a‖ ≤ (f + g) a
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case insert
𝕜 : 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 ι
inst✝ : DecidableEq ι
f : MultilinearMap 𝕜 E G
C : ℝ
hC : 0 ≤ C
H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i, ‖m i‖
m₁ m₂ : (i : ι) → E i
i : ι
s : Finset ι
his : i ∉ s
Hrec : ‖f m₁ - f (s.piecewise m₂ m₁)‖ ≤ C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
⊢ ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
    C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
have I :
        ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ ≤
          C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
        have A : (insert i s).piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₂ i) :=
          s.piecewise_insert _ _ _
        have B : s.piecewise m₂ m₁ = Function.update (s.piecewise m₂ m₁) i (m₁ i) := by
          simp [his]
        rw [B, A, ← f.map_update_sub]
        apply le_trans (H _)
        gcongr with j
        by_cases h : j = i
        · rw [h]
          simp
        · by_cases h' : j ∈ s <;> simp [h', h]
      calc
        ‖f m₁ - f ((insert i s).piecewise m₂ m₁)‖ ≤
            ‖f m₁ - f (s.piecewise m₂ m₁)‖ +
              ‖f (s.piecewise m₂ m₁) - f ((insert i s).piecewise m₂ m₁)‖ := by
          rw [← dist_eq_norm, ← dist_eq_norm, ← dist_eq_norm]
          exact dist_triangle _ _ _
        _ ≤ (C * ∑ i ∈ s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖) +
              C * ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ :=
          (add_le_add Hrec I)
        _ = C * ∑ i ∈ insert i s, ∏ j, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖ := by
          simp [his, add_comm, left_distrib]

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 α
b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Ici b) μ ↔ IntegrableOn f (Ioi b) μ

Tactic:
by
  rw [← Ioi_union_left, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : Module 𝕜 E
inst✝¹ : ContinuousSMul 𝕜 E
p q : Submodule 𝕜 E
h : IsCompl p q
hp : IsClosed[inst✝⁴] ↑p
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
φ : E ⧸ p →L[𝕜] ↥q := LinearMap.toContinuousLinearMap ↑(p.quotientEquivOfIsCompl q h)
x : ↥q
⊢ (φ ∘SL p.mkQL) ↑x = x

Tactic:
by simp [φ]

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

Goal state before:
pp: case pos
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hp_ne_top : p ≠ ∞
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hi : eLpNorm (fun x ↦ f x - y₀) p μ < ∞
hp_zero : p = 0
⊢ Tendsto (fun n ↦ eLpNorm (⇑(approxOn f hf s y₀ h₀ n) - f) p μ) atTop (𝓝 0)

Tactic:
simpa only [hp_zero, eLpNorm_exponent_zero] using tendsto_const_nhds

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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
h_left_eq : (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a))
⊢ (T (⇑f ⁻¹' ↑({b ∈ f.range | g b = g (f a)}))) (g (f a)) =
    (T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, ⇑f ⁻¹' {y})) (g (f a))

Tactic:
rw [← Finset.set_biUnion_preimage_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ (map norm f.posPart) a✝ = f.posPart a✝

Tactic:
rw [map_apply, Real.norm_eq_abs, abs_of_nonneg]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a✝ : α
⊢ 0 ≤ f.posPart a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)

Tactic:
let x n := SimpleFunc.approxOn (g : α → G) g_meas
    ((range (g : α → G) ∪ {0}) ∩ { y | 0 ≤ y }) 0 zero_mem n

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
g : { g // 0 ≤ g }
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hg_memLp : MemLp (↑↑↑g) p μ
zero_mem : 0 ∈ (Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}
this : SeparableSpace ↑((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y})
g_meas : Measurable ↑↑↑g
x : ℕ → α →ₛ G := fun n ↦ approxOn (↑↑↑g) g_meas ((Set.range ↑↑↑g ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
⊢ ∃ x, (∀ (n : ℕ), x n ∈ Set.range (coeSimpleFuncNonnegToLpNonneg p μ G)) ∧ Tendsto x atTop (𝓝 g)
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ integral μ (piecewise s hs f 0) = integral (μ.restrict s) f

Tactic:
refine (integral_eq_sum_of_subset ?_).trans
      ((sum_congr rfl fun y hy => ?_).trans (integral_eq_sum_filter _ _).symm)

Goal state after:
case refine_1
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ {x ∈ (piecewise s hs f 0).range | x ≠ 0} ⊆ {x ∈ f.range | x ≠ 0}

case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
s : Set α
hs : MeasurableSet s
y : F
hy : y ∈ {x ∈ f.range | x ≠ 0}
⊢ μ.real (⇑(piecewise s hs f 0) ⁻¹' {y}) • y = (μ.restrict s).real (⇑f ⁻¹' {y}) • y
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

Tactic:
have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
  have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
  simp only [setToSimpleFunc, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  by_cases h0 : g (f a) = 0
  · simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]
  have h_left_eq :
    T (map g f ⁻¹' {g (f a)}) (g (f a))
      = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
    rw [map_preimage_singleton]
  rw [h_left_eq]
  have h_left_eq' :
    T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a))
      = T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' {y}) (g (f a)) := by
    rw [← Finset.set_biUnion_preimage_singleton]
  rw [h_left_eq']
  rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
  · simp only [_root_.sum_apply]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [mem_filter] at hx
    rw [hx.2]
  · exact fun i => measurableSet_fiber _ _
  · grind
  · grind [Set.disjoint_iff]

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

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
p : E × E
hp : p ∈ (f.pair g).range
⊢ (T (⇑(f.pair g) ⁻¹' {p})) p.1 = (T (⇑(f.pair g) ⁻¹' {p})) p.2

Tactic:
rcases mem_range.1 hp with ⟨a, rfl⟩

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
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
a : α
hp : (f.pair g) a ∈ (f.pair g).range
⊢ (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).1 = (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).2
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ integral (c • f) = c • (integralCLM' 𝕜) f

Tactic:
integral_eq' 𝕜 (c • f),

Goal state after:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
c : 𝕜
f : ↥(Lp E 1 μ)
⊢ (integralCLM' 𝕜) (c • f) = c • (integralCLM' 𝕜) f
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ u =ᶠ[l] 0

Tactic:
eventuallyEq_iff_exists_mem

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u : α → β
l : Filter α
h : u =O[l] 0
⊢ ∃ s ∈ l, Set.EqOn u 0 s
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case cons
α : Type u_1
ι : Type u_2
β : Type u_3
inst✝ : NormedField β
l : Filter α
f g : ι → α → β
i : ι
L : List ι
ihL :
  (∀ i ∈ L, f i ~[l] g i) →
    (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod
h : ∀ i_1 ∈ i :: L, f i_1 ~[l] g i_1
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) (i :: L)).prod) ~[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) (i :: L)).prod

Tactic:
| cons i L ihL =>

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 : α → E
hf : f ≤ᵐ[μ] 0
⊢ ∫ (x : α), f x ∂μ ≤ 0

Tactic:
rw [← neg_nonneg, ← integral_neg]
  refine integral_nonneg_of_ae ?_
  filter_upwards [hf] with x hx
  simpa

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫ (a : α), ↑(f a) ∂μ)

Tactic:
integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg)
      hfi.aestronglyMeasurable,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b
hf : ¬Integrable (fun a ↦ ↑(f a)) μ
⊢ ∫ (a : α), ↑(f a) ∂μ ≤ ↑b

Tactic:
rw [integral_undef hf]; exact b.2

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑‖x‖)⁻¹ • x‖ = 1
Module: Mathlib.Analysis.Normed.Module.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r

Tactic:
have : ‖x‖ ≠ 0 := by simp [hx]

Goal state after:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
r : ℝ
r_nonneg : 0 ≤ r
x : E
hx : x ≠ 0
this : ‖x‖ ≠ 0
⊢ ‖(↑r * (↑‖x‖)⁻¹) • x‖ = r
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
G'' : Type u_7
G' : Type u_8
inst✝⁶ : NormedAddCommGroup G'
inst✝⁵ : PartialOrder G'
inst✝⁴ : IsOrderedAddMonoid G'
inst✝³ : NormedSpace ℝ G'
inst✝² : NormedAddCommGroup G''
inst✝¹ : PartialOrder G''
inst✝ : NormedSpace ℝ G''
T : Set α → G'' →L[ℝ] G'
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G''), 0 ≤ x → 0 ≤ (T s) x
f : ↥(α →₁ₛ[μ] G'')
hf : 0 ≤ f
⊢ 0 ≤ setToL1S T f

Tactic:
simp_rw [setToL1S]
  obtain ⟨f', hf', hff'⟩ := exists_simpleFunc_nonneg_ae_eq hf
  replace hff' : simpleFunc.toSimpleFunc f =ᵐ[μ] f' :=
    (Lp.simpleFunc.toSimpleFunc_eq_toFun f).trans hff'
  rw [SimpleFunc.setToSimpleFunc_congr _ h_zero h_add (SimpleFunc.integrable _) hff']
  exact
    SimpleFunc.setToSimpleFunc_nonneg' T hT_nonneg _ hf' ((SimpleFunc.integrable f).congr hff')

Goal state after:
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'
⊢ ‖d‖ * (‖c‖ / R * ‖x‖) ≤ ‖d‖ * ‖x - y'‖

Tactic:
by gcongr; exact hx y' (by simp [y', Submodule.smul_mem _ _ hy])

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 : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ENNReal.ofReal (∫ (x : X), ‖f x‖ ∂μ i)

Tactic:
ofReal_integral_eq_lintegral_ofReal (hf i).norm

Goal state after:
ι : 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 : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

ι : 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‖
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 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
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  by_cases hf : Integrable f μ
  · simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]
  · simp_rw [setToFun_undef _ hf]

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

Goal state before:
pp: case neg
α : 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 φ μ)
⊢ ¬Integrable (fun x ↦ f (φ x)) μ

Tactic:
exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)

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 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    ⇑((LinearEquiv.piRing 𝕜 E ι 𝕜).symm ≪≫ₗ LinearMap.toContinuousLinearMap.symm.symm)

Tactic:
LinearEquiv.symm_symm

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    ⇑((LinearEquiv.piRing 𝕜 E ι 𝕜).symm ≪≫ₗ LinearMap.toContinuousLinearMap)