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

Goal state before:
pp: α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
⊢ ↑↑|f| x ≤ ↑↑|g| x → ↑↑|f| x = |↑↑f x| → ↑↑|g| x = |↑↑g x| → ‖↑↑f x‖ ≤ ‖↑↑g x‖

Tactic:
hx

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Lattice E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : Fact (1 ≤ p)
f g : ↥(Lp E p μ)
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : ↑↑|f| x ≤ ↑↑|g| x
⊢ ↑↑|f| x = |↑↑f x| → ↑↑|g| x = |↑↑g x| → ‖↑↑f x‖ ≤ ‖↑↑g x‖
Module: Mathlib.Logic.Equiv.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
a : α ↪ γ
⊢ (fun b ↦ Disjoint (Set.range ⇑a) (Set.range ⇑b)) = fun f ↦ ∀ (a_1 : β), f a_1 ∈ (Set.range ⇑a)ᶜ

Tactic:
ext f
            rw [← Set.range_subset_iff, Set.subset_compl_iff_disjoint_right, disjoint_comm]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ ContinuousAt inverse ↑x

Tactic:
rw [ContinuousAt, tendsto_iff_norm_sub_tendsto_zero, inverse_unit]

Goal state after:
R : Type u_1
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : Rˣ
h_is_o : (fun t ↦ (↑x + t)⁻¹ʳ - ↑x⁻¹) =o[𝓝 0] fun x ↦ 1
h_lim : Tendsto (fun y ↦ y - ↑x) (𝓝 ↑x) (𝓝 0)
⊢ Tendsto (fun e ↦ ‖e⁻¹ʳ - ↑x⁻¹‖) (𝓝 ↑x) (𝓝 0)
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
M : Type u_5
inst✝³ : Monoid M
inst✝² : DistribMulAction M F
inst✝¹ : SMulCommClass 𝕜 M F
inst✝ : ContinuousConstSMul M F
⊢ ContinuousConstSMul M (ContinuousMultilinearMap 𝕜 E F)

Tactic:
by
  let := IsTopologicalAddGroup.rightUniformSpace F
  have := isUniformAddGroup_of_addCommGroup (G := F)
  infer_instance

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
x : (i : ι) → E i
⊢ x ∈ s → f x ∈ c • U

Tactic:
hx

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
hx : x ∈ s
⊢ f x ∈ c • U
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
⊢ x ∈ {x | f x ≠ 0}ᶜ → ↑(f x) • g x = ↑(f x) • g' x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f x ≠ 0}
x : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
⊢ ↑(f x) • g x = g' x → ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g g' : α → E
g'meas : StronglyMeasurable g'
hg' : (fun x ↦ ↑(f x) • g x) =ᵐ[μ] g'
x : α
hx : ↑(f x) • g x = g' x
⊢ ↑(f x) ≠ 0 → g x = (↑(f x))⁻¹ • g' x
Module: Mathlib.Topology.Algebra.Module.Complement

Goal state before:
pp: R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔
    Continuous[instTopologicalSpaceProd, inst✝³] ⇑(p.prodEquivOfIsCompl q h) ∧
      Continuous[inst✝³, instTopologicalSpaceProd] ⇑(p.prodEquivOfIsCompl q h).symm

Tactic:
isTopCompl_iff_continuous_symm_prodEquivOfIsCompl,

Goal state after:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ Continuous[inst✝³, instTopologicalSpaceProd] ⇑(p.prodEquivOfIsCompl q ?m.64).symm ↔
    Continuous[instTopologicalSpaceProd, inst✝³] ⇑(p.prodEquivOfIsCompl q h) ∧
      Continuous[inst✝³, instTopologicalSpaceProd] ⇑(p.prodEquivOfIsCompl q h).symm

R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p q : Submodule R M
inst✝ : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsCompl p q
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

Tactic:
by
  rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h
  · simp only [Measure.real, h, ENNReal.toReal_top]
    exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
  · have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
    have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
    simp only [Measure.real, ← ENNReal.toReal_add A B]
    exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)

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
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp (f + g) p μ ↔ MemLp f p μ ∧ MemLp g p μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Goal state after:
case refine_1
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp f p μ

case refine_2
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f g : α → E
h : Disjoint (support f) (support g)
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
hfg : MemLp (f + g) p μ
⊢ MemLp g p μ
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 g : α → ε'
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ Integrable (s.piecewise f g) μ

Tactic:
rw [IntegrableOn] at hf hg
  rw [← memLp_one_iff_integrable] at hf hg ⊢
  exact MemLp.piecewise hs hf hg

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 : α → β
he : MeasurableEmbedding e
f : β → ε
μ : Measure α
s : Set β
⊢ Integrable f (Measure.map e (μ.restrict (e ⁻¹' s))) ↔ Integrable (f ∘ e) (μ.restrict (e ⁻¹' s))

Tactic:
he.integrable_map_iff

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 : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ∞
x : α
⊢ x ∈ s → x ∈ ⋃ n, v n

Tactic:
hx

Goal state after:
α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : TopologicalSpace ε'
inst✝ : ESeminormedAddMonoid ε'
f : α → ε'
hf : IntegrableOn f s μ
h's : ∀ x ∈ s, ‖f x‖ₑ ≠ 0
u : ℕ → ℝ≥0∞
left✝ : StrictAnti u
u_pos : ∀ (n : ℕ), u n ∈ Ioo 0 ∞
u_lim : Tendsto u atTop (𝓝 0)
v : ℕ → Set α := fun n ↦ toMeasurable (μ.restrict s) {x | u n ≤ ‖f x‖ₑ}
A : ∀ (n : ℕ), μ (s ∩ v n) ≠ ∞
x : α
hx : x ∈ s
⊢ x ∈ ⋃ n, v n
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
⊢ ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ → ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
this : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
x : α
hx : ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖
⊢ ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖
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
x : α
⊢ x ∈ u → ‖f x‖ₑ ≠ 0

Tactic:
hx

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
x : α
hx : x ∈ u
⊢ ‖f x‖ₑ ≠ 0
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g₁ g₂ : α → ℝ
hf : AEStronglyMeasurable f μ
h_le₁ : g₁ ≤ᵐ[μ] f
h_le₂ : f ≤ᵐ[μ] g₂
h_int₁ : Integrable g₁ μ
h_int₂ : Integrable g₂ μ
⊢ Integrable f μ

Tactic:
have : ∀ᵐ x ∂μ, ‖f x‖ ≤ max ‖g₁ x‖ ‖g₂ x‖ := by
    filter_upwards [h_le₁, h_le₂] with x hx1 hx2
    simp only [Real.norm_eq_abs]
    exact abs_le_max_abs_abs hx1 hx2
  have h_le_add : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖‖g₁ x‖ + ‖g₂ x‖‖ := by
    filter_upwards [this] with x hx
    refine hx.trans ?_
    conv_rhs => rw [Real.norm_of_nonneg (by positivity)]
    exact max_le_add_of_nonneg (norm_nonneg _) (norm_nonneg _)
  exact Integrable.mono (by fun_prop) hf h_le_add

Goal state after:
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
A : IntegrableOn f v μ
x : α
hxt : x ∈ t \ s → f x = 0
⊢ x ∈ t \ v → 0 = f x

Tactic:
hx

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
A : IntegrableOn f v μ
x : α
hxt : x ∈ t \ s → f x = 0
hx : x ∈ t \ v
⊢ 0 = f x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

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

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
x : α
hx : f x < ∞
⊢ ENNReal.ofReal (f x).toReal = f x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
x : α
⊢ f x < ∞ → ↑(f x).toNNReal = f x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
x : α
hx : f x < ∞
⊢ ↑(f x).toNNReal = f x
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
x : α
⊢ (x ∉ s → f x = 0) → x ∈ univ \ s → f x = 0

Tactic:
hx

Goal state after:
α : Type u_1
mα : MeasurableSpace α
s : Set α
μ : Measure α
ε' : Type u_7
inst✝² : TopologicalSpace ε'
inst✝¹ : ENormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
hf : IntegrableOn f s μ
h't : ∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0
x : α
hx : x ∉ s → f x = 0
⊢ x ∈ univ \ s → f x = 0
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: case pos
𝕜 : 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‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

pp: case neg
𝕜 : 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‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖

Tactic:
· rw [h]
          simp

Goal state after:
case neg
𝕜 : 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‖
A : (insert i s).piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₂ i)
B : s.piecewise m₂ m₁ = update (s.piecewise m₂ m₁) i (m₁ i)
j : ι
a✝ : j ∈ univ
h : ¬j = i
⊢ ‖update (s.piecewise m₂ m₁) i (m₁ i - m₂ i) j‖ ≤ if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
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
x : α
⊢ f x = AEMeasurable.mk f hf x → ↑(f x) = ↑(AEMeasurable.mk f hf x)

Tactic:
hx

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
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf 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
x : α
⊢ f x = AEMeasurable.mk f hf x → ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x

Tactic:
hx

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
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(AEMeasurable.mk f hf x) • g x = ↑(f x) • g x
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
x : α
⊢ x ∈ u → (x ∈ t ↔ x ∈ t ∩ u)

Tactic:
hx

Goal state after:
α : Type u_1
ε : Type u_3
mα : MeasurableSpace α
f : α → ε
μ : Measure α
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
l : Filter α
t : Set α
ht : t ∈ l
u : Set α
hu : u ∈ ae μ
hf : IntegrableOn f (t ∩ u) μ
x : α
hx : x ∈ u
⊢ x ∈ t ↔ x ∈ t ∩ u
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : 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
⊢ Integrable (f + g) μ ↔ Integrable f μ ∧ Integrable g μ

Tactic:
refine ⟨fun hfg => ⟨?_, ?_⟩, fun h => h.1.add h.2⟩

Goal state after:
case refine_1
α : 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 f μ

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 μ
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:

Tactic:
‖f m' - f m‖ ≤ D * Fintype.card ι * max ‖m'‖ ‖m‖ ^ (Fintype.card ι - 1) * ‖m' - m‖ :=
      f.norm_image_sub_le_of_bound D_pos H m' m
    _ ≤ D * Fintype.card ι * (‖m‖ + 1) ^ (Fintype.card ι - 1) * ‖m' - m‖ := by gcongr

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

Goal state before:
pp: 𝕜 : Type u
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
n : ℕ
Ei : Fin n → Type u_1
inst✝¹ : (i : Fin n) → SeminormedAddCommGroup (Ei i)
inst✝ : (i : Fin n) → NormedSpace 𝕜 (Ei i)
f : ContinuousMultilinearMap 𝕜 Ei G
m : (i : Fin n) → Ei i
b : ℝ
hm : ‖m‖ ≤ b
⊢ ‖f m‖ ≤ ‖f‖ * b ^ n

Tactic:
simpa only [Fintype.card_fin] using f.le_opNorm_mul_pow_card_of_le hm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
⊢ ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x →
    ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x‖ₑ = ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) x

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hx : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
⊢ ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x‖ₑ = ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hx : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
⊢ ‖↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x‖ₑ = ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) x

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ε' : Type u_6
ε'' : Type u_7
m : MeasurableSpace α
μ ν : Measure α
inst✝⁹ : MeasurableSpace δ
inst✝⁸ : NormedAddCommGroup β
inst✝⁷ : NormedAddCommGroup γ
inst✝⁶ : TopologicalSpace ε
inst✝⁵ : ContinuousENorm ε
inst✝⁴ : TopologicalSpace ε'
inst✝³ : ContinuousENorm ε'
inst✝² : ENorm ε''
E : Type u_8
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
f_meas : Measurable f
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
hx : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
⊢ ‖f x • ↑↑u x‖ₑ = ((fun x ↦ ↑(f x)) * fun a ↦ ‖↑↑u a‖ₑ) x
Module: Mathlib.MeasureTheory.Function.L1Space.Integrable

Goal state before:
pp: G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun n ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (fun x ↦ ‖G n x‖ₑ) μ
x : ℝ
⊢ Tendsto (fun n ↦ G n x) atTop (𝓝 (f x)) → ?m.51 x = ?m.52 x

Tactic:
hx

Goal state after:
G : ℕ → ℝ → ℝ
f : ℝ → ℝ
μ : Measure ℝ
hGf : ∀ᵐ (x : ℝ) ∂μ, Tendsto (fun n ↦ G n x) atTop (𝓝 (f x))
hG : ∀ (n : ℕ), AEMeasurable (fun x ↦ ‖G n x‖ₑ) μ
x : ℝ
hx : Tendsto (fun n ↦ G n x) atTop (𝓝 (f x))
⊢ ?m.51 x = ?m.52 x