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

Goal state before:
pp: α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
q : ℝ≥0∞
⊢ MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ

Tactic:
by
  refine ⟨(hf.1.norm.aemeasurable.pow_const q.toReal).aestronglyMeasurable, ?_⟩
  by_cases q_top : q = ∞
  · simp [q_top]
  by_cases q_zero : q = 0
  · simp only [q_zero, ENNReal.toReal_zero, Real.rpow_zero]
    by_cases p_zero : p = 0
    · simp [p_zero]
    rw [ENNReal.div_zero p_zero]
    exact (memLp_top_const (1 : ℝ)).2
  rw [eLpNorm_norm_rpow _ (ENNReal.toReal_pos q_zero q_top)]
  apply ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg
  rw [ENNReal.ofReal_toReal q_top, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
    mul_one]
  exact hf.2.ne

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
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') x‖ ≤ ↑c * ‖↑↑(f - f') x‖

Tactic:
filter_upwards [hg.coeFn_compLp g0 f, hg.coeFn_compLp g0 f',
    Lp.coeFn_sub (hg.compLp g0 f) (hg.compLp g0 f'), Lp.coeFn_sub f f'] with a ha1 ha2 ha3 ha4

Goal state after:
α : Type u_1
E : Type u_4
F : Type u_5
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
g : E → F
c : ℝ≥0
hg : LipschitzWith c g
g0 : g 0 = 0
f f' : ↥(Lp E p μ)
a : α
ha1 : ↑↑(hg.compLp g0 f) a = (g ∘ ↑↑f) a
ha2 : ↑↑(hg.compLp g0 f') a = (g ∘ ↑↑f') a
ha3 : ↑↑(hg.compLp g0 f - hg.compLp g0 f') a = (↑↑(hg.compLp g0 f) - ↑↑(hg.compLp g0 f')) a
ha4 : ↑↑(f - f') a = (↑↑f - ↑↑f') a
⊢ ‖↑↑(hg.compLp g0 f - hg.compLp g0 f') a‖ ≤ ↑c * ‖↑↑(f - f') a‖
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ∞)
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)

Tactic:
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp

Goal state after:
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : ¬((∑ i ∈ s, f i ^ p) ^ (1 / p) = ∞ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ∞)
pos : 0 < p
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) + (∑ i ∈ s, g i ^ p) ^ (1 / p)
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

Tactic:
simp only at f_eq

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ a₂ : α
f_eq : f a₁ = f a₂
⊢ Sum.inl a₁ = Sum.inl a₂
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

Tactic:
simp only at f_eq

Goal state after:
case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
a₁ : α
b₂ : β
f_eq : f a₁ = g b₂
⊢ Sum.inl a₁ = Sum.inr b₂
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

Tactic:
simp only at f_eq

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ : β
a₂ : α
f_eq : g b₁ = f a₂
⊢ Sum.inr b₁ = Sum.inl a₂
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq :
  (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₁) =
    (fun x ↦
        match x with
        | Sum.inl a => f a
        | Sum.inr b => g b)
      (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
simp only at f_eq

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
x✝ : { f // Disjoint (Set.range ⇑f.1) (Set.range ⇑f.2) }
f : α ↪ γ
g : β ↪ γ
disj : Disjoint (Set.range ⇑(f, g).1) (Set.range ⇑(f, g).2)
b₁ b₂ : β
f_eq : g b₁ = g b₂
⊢ Sum.inr b₁ = Sum.inr b₂
Module: Mathlib.Analysis.Normed.Operator.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ‖lsmul 𝕜 R‖₊ ≤ 1

Tactic:
← NNReal.coe_le_coe

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
R : Type u_3
inst✝⁴ : SeminormedRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : Module R E
inst✝¹ : IsBoundedSMul R E
inst✝ : IsScalarTower 𝕜 R E
⊢ ↑‖lsmul 𝕜 R‖₊ ≤ ↑1
Module: Mathlib.Analysis.Normed.Operator.NormedSpace

Goal state before:
pp: case h.calc_1
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 0 ≤ c

pp: case h.calc_2
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r

Tactic:
· exact le_trans (norm_nonneg _) (h 0 (by simp [r_pos]))

Goal state after:
case h.calc_2
𝕜 : Type u_1
E : Type u_5
Fₗ : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup Fₗ
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 Fₗ
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] Fₗ
h : ∀ z ∈ ball 0 r, ‖f z‖ ≤ c
k : 𝕜
hk : 1 < ‖k‖
z x : E
hko : r / ‖k‖ ≤ ‖x‖
hxo : ‖x‖ < r
⊢ 1 ≤ ‖x‖ * ‖k‖ / r
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
⊢ IsVonNBounded 𝕜 (image2 (fun f x ↦ f x) S s)

Tactic:
intro U

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
⊢ U ∈ 𝓝 0 → Absorbs 𝕜 U (image2 (fun f x ↦ f x) S s)
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
⊢ IsVonNBounded 𝕜 (image2 (fun f x ↦ f x) S s)

Tactic:
intro U hU
  filter_upwards [hS (eventually_nhds_zero_mapsTo hs hU)] with c hc
  rw [image2_subset_iff]
  intro f hf x hx
  rcases hc hf with ⟨g, hg, rfl⟩
  exact smul_mem_smul_set (hg hx)

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
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo ⇑f (U, V).1 (U, V).2}

Tactic:
set φ : (∀ i, E i) →L[𝕜] (∀ i, E₁ i) := .piMap f

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
E₁ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (E₁ i)
inst✝² : ContinuousConstSMul 𝕜 F
inst✝¹ : (i : ι) → AddCommGroup (E₁ i)
inst✝ : (i : ι) → Module 𝕜 (E₁ i)
f : (i : ι) → E i →L[𝕜] E₁ i
aux : ContinuousMultilinearMap 𝕜 E₁ F →ₗ[𝕜] ContinuousMultilinearMap 𝕜 E F :=
  { toFun := fun g ↦ g.compContinuousLinearMap f, map_add' := ⋯, map_smul' := ⋯ }
U : Set ((i : ι) → E i)
V : Set F
hU : IsVonNBounded 𝕜 (U, V).1
hV : (U, V).2 ∈ 𝓝 0
φ : ((i : ι) → E i) →L[𝕜] (i : ι) → E₁ i := ContinuousLinearMap.piMap f
⊢ ∃ ia,
    (IsVonNBounded 𝕜 ia.1 ∧ ia.2 ∈ 𝓝 0) ∧ ∀ x ∈ {f | MapsTo (⇑f) ia.1 ia.2}, aux x ∈ {f | MapsTo ⇑f (U, V).1 (U, V).2}
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ (μ (s₁ ∪ t₁)).toReal = (μ (s₂ ∪ t₂)).toReal

Tactic:
rw [measure_union_congr_of_subset hs _ ht]

Goal state after:
α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ t₂ ≤ μ t₁

α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : μ s₂ ≠ ∞
h₂ : μ t₂ ≠ ∞
⊢ μ s₂ ≤ μ s₁
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ (∑ i ∈ s, μ (t i)).toReal = ∑ i ∈ s, (μ (t i)).toReal

Tactic:
ENNReal.toReal_sum (by finiteness)

Goal state after:
α : Type u_1
ι : Type u_3
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (μ univ).toReal < ∑ i ∈ s, (μ (t i)).toReal
⊢ ∑ a ∈ s, (μ (t a)).toReal = ∑ i ∈ s, (μ (t i)).toReal
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ MemLp f 1 (μ + ν)

Tactic:
refine ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩

Goal state after:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
inst✝ : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 (μ + ν) < ∞
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hs : MeasurableSet s
⊢ IntegrableOn f s μ ↔ IntegrableOn f (range Subtype.val) μ

Tactic:
Subtype.range_val

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
hs : MeasurableSet s
⊢ IntegrableOn f s μ ↔ IntegrableOn f s μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : Nonempty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ 1

Tactic:
by
  refine opNorm_le_bound zero_le_one fun m => ?_
  simp only [ContinuousMultilinearMap.mkPiAlgebra_apply, one_mul]
  exact norm_prod_le' _ univ_nonempty _

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

Tactic:
by_cases hab : a < b
  · rw [← Ioo_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
  · rw [Ioo_eq_empty hab, Ioc_eq_empty hab]

Goal state after:
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 ι
f : ContinuousMultilinearMap 𝕜 E 𝕜
z : G
⊢ ‖({ toFun := fun f ↦ { toFun := fun z ↦ f.smulRight z, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
            map_smul' := ⋯ }
          f)
        z‖ ≤
    1 * ‖f‖ * ‖z‖

Tactic:
by simp [norm_smulRight]

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

Goal state before:
pp: case refine_1
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
⊢ IsOpen[inst✝³] (u n)

Tactic:
have : u n ∈ T' := by rw [hu]; exact mem_range_self n

Goal state after:
case refine_1
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
⊢ IsOpen[inst✝³] (u n)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case refine_3
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
⊢ IntegrableOn f (u n ∩ s) μ

Tactic:
have : u n ∈ T' := by rw [hu]; exact mem_range_self n

Goal state after:
case refine_3
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✝ : SecondCountableTopology X
hf : LocallyIntegrableOn f s μ
T : Set (Set X)
T_count : T.Countable
T_open : ∀ u ∈ T, IsOpen[inst✝³] u
sT : s ⊆ ⋃ u ∈ T, u
hT : ∀ u ∈ T, IntegrableOn f (u ∩ s) μ
T' : Set (Set X) := insert ∅ T
T'_count : T'.Countable
T'_ne : T'.Nonempty
u : ℕ → Set X
hu : T' = range u
n : ℕ
this : u n ∈ T'
⊢ IntegrableOn f (u n ∩ s) μ
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) ((↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun x) = x}

Tactic:
· exact isClosed_eq (by simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]; fun_prop) continuous_id

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹⁵ : NormedDivisionRing 𝕜
inst✝¹⁴ : NormedDivisionRing 𝕜₂
inst✝¹³ : AddCommGroup E
inst✝¹² : NormedAddCommGroup Eₗ
inst✝¹¹ : AddCommGroup F
inst✝¹⁰ : NormedAddCommGroup Fₗ
inst✝⁹ : Module 𝕜 E
inst✝⁸ : Module 𝕜 Eₗ
inst✝⁷ : IsBoundedSMul 𝕜 Eₗ
inst✝⁶ : Module 𝕜₂ F
inst✝⁵ : Module 𝕜₂ Fₗ
inst✝⁴ : IsBoundedSMul 𝕜₂ Fₗ
inst✝³ : CompleteSpace Eₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_norm₁ : ∃ C, ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖
h_dense₂ : DenseRange ⇑e₂
h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖
⊢ IsClosed {x | (↑((e₂ ∘ₛₗ ↑f).extendOfNorm e₁)).toFun (((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x) = x}

Tactic:
· exact isClosed_eq (by simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
      ContinuousLinearMap.coe_coe]; fun_prop) continuous_id

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
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : (μ + ν) s < ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s

Tactic:
lt_top_iff_ne_top,

Goal state after:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
ν : Measure α
f : α →ₛ E
hf : Integrable (⇑f) (μ + ν)
s : Set α
x✝ : MeasurableSet s
hμνs : (μ + ν) s ≠ ∞
⊢ weightedSMul (μ + ν) s = weightedSMul μ s + weightedSMul ν s
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᵐ[μ] g
⊢ setToFun μ (weightedSMul μ) ⋯ f = setToFun μ (weightedSMul μ) ⋯ g

Tactic:
exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬(True ∧ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ < ∞)
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal

Tactic:
lt_top_iff_ne_top,

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᵐ[μ] f
hfm : AEStronglyMeasurable f μ
hfi : ¬(True ∧ ∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ ≠ ∞)
⊢ 0 = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
φ : α → β
hφ : Tendsto φ l (𝓝 1)
h : u =ᶠ[l] φ * v
x✝ : α
⊢ ((φ - 1) * v) x✝ = (φ * v) x✝ - v x✝

Tactic:
simp [sub_mul]

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 : (a - b) =o[l] b
huv : (u - v) =o[l] v
φ : α → 𝕜
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
⊢ (fun x ↦ φ x • u x - v x) =o[l] v

Tactic:
rw [isLittleO_iff] at *

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 : IsBigOWith C l u v
⊢ ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖φ x • u x - v x‖ ≤ c * ‖v x‖