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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key :
  f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) ≤
    z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z

Tactic:
field_simp at key

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : ConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 ≤ (z - y) / (z - x)
hb : 0 ≤ (y - x) / (z - x)
key : (z - x) * f y ≤ f x * (z - y) + y * f z - x * f z
⊢ (z - x) * f y ≤ (z - y) * f x + (y - x) * f z
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≪ μ
⊢ eLpNormEssSup f ν ≤ eLpNormEssSup f μ

Tactic:
by
  simp_rw [eLpNormEssSup]
  exact essSup_mono_measure hμν

Goal state after:
Module: Mathlib.Analysis.Convex.Slope

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
key :
  f (z * y * (z - x)⁻¹ - y * x * (z - x)⁻¹) <
    z * (z - x)⁻¹ * f x - y * (z - x)⁻¹ * f x + y * (z - x)⁻¹ * f z - x * (z - x)⁻¹ * f z
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z

Tactic:
field_simp at key

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hf : StrictConvexOn 𝕜 s f
x y z : 𝕜
hx : x ∈ s
hz : z ∈ s
hxy : x < y
hyz : y < z
hxy' : 0 < y - x
hyz' : 0 < z - y
hxz' : 0 < z - x
ha : 0 < (z - y) / (z - x)
hb : 0 < (y - x) / (z - x)
key : (z - x) * f y < f x * (z - y) + y * f z - x * f z
⊢ (z - x) * f y < (z - y) * f x + (y - x) * f z
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p / ENNReal.ofReal p + g a ^ q / ENNReal.ofReal q ∂μ = 1

Tactic:
simp only [div_eq_mul_inv]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_norm : ∫⁻ (a : α), f a ^ p ∂μ = 1
hg_norm : ∫⁻ (a : α), g a ^ q ∂μ = 1
⊢ ∫⁻ (a : α), f a ^ p * (ENNReal.ofReal p)⁻¹ + g a ^ q * (ENNReal.ofReal q)⁻¹ ∂μ = 1
Module: Mathlib.MeasureTheory.Integral.MeanInequalities

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ∞
a : α
⊢ f a = funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)

Tactic:
simp [funMulInvSnorm, mul_assoc, ENNReal.inv_mul_cancel, hf_nonzero, hf_top]

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

Goal state before:

Tactic:
eLpNorm' (fun x => b (f x) (g x)) r μ
      ≤ eLpNorm' (fun x ↦ (c : ℝ) • ‖f x‖ * ‖g x‖) r μ := by
      simp only [eLpNorm']
      gcongr ?_ ^ _
      refine lintegral_mono_ae <| h.mono fun a ha ↦ ?_
      gcongr
      simp only [enorm_eq_nnnorm, ENNReal.coe_le_coe]
      simpa using! ha
    _ ≤ c * eLpNorm' f p μ * eLpNorm' g q μ := by
      simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm'_const_smul _ hro_lt]
      rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
      gcongr
      simpa only [eLpNorm', enorm_mul, enorm_norm] using!
        ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr hro_lt hrp hpqr μ hf.enorm hg.enorm

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

Goal state before:
pp: case e'_7
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_6
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
q : ℝ≥0∞
f : α → ε
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ₑ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
· rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

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

Goal state before:
pp: case e'_7
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
q : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
q_zero : q ≠ 0
q_top : q ≠ ∞
h : MemLp (fun x ↦ ‖f x‖ ^ q.toReal) (p / q) μ
⊢ p = p / q / q⁻¹

Tactic:
· rw [div_eq_mul_inv, inv_inv, div_eq_mul_inv, mul_assoc, ENNReal.inv_mul_cancel q_zero q_top,
      mul_one]

Goal state after:
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
⊢ IsStrictMap f ↔ IsHomeomorph ⇑(quotientKerEquivRange f)

Tactic:
by
  simp only [IsStrictMap, isHomeomorph_iff_isQuotientMap_injective, Equiv.injective, and_true]
  exact ⟨fun h => IsQuotientMap.of_comp_isQuotientMap isQuotientMap_quotient_mk' h,
         fun h ↦ h.comp isQuotientMap_quotient_mk'⟩

Goal state after:
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
⊢ IsStrictMap f ↔ IsEmbedding (kerLift f)

Tactic:
simp only [isStrictMap_iff_isHomeomorph_quotientKerEquivRange,
    isHomeomorph_iff_isEmbedding_surjective, Equiv.surjective, and_true]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsEmbedding ⇑(quotientKerEquivRange f) ↔ IsEmbedding (kerLift f)
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : μ s ≠ ∞
⊢ μ.real (s ∩ t) + μ.real (s \ t) = μ.real s

Tactic:
by
  simp only [Measure.real]
  rw [← ENNReal.toReal_add, measure_inter_add_sdiff _ ht]
  · exact measure_ne_top_of_subset inter_subset_left h
  · exact measure_ne_top_of_subset sdiff_subset h

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

Goal state before:
pp: case e'_5
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
hp : p ≠ ∞
c : E
ε : ℝ≥0∞
hε : ε ≠ 0
h'p : p ≠ 0
hp₀ : 0 < p
hp₀' : 0 ≤ 1 / p.toReal
hp₀'' : 0 < p.toReal
⊢ 0 = ‖c‖₊ * 0 ^ (1 / p.toReal)

Tactic:
simp [hp₀''.ne']

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 t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
c : E
⊢ ((s ∪ t).indicator fun x ↦ c) =ᵐ[μ] (s.indicator fun x ↦ c) + t.indicator fun x ↦ c

Tactic:
Set.indicator_union_of_disjoint hst,

Goal state after:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : μ s ≠ ∞
hμt : μ t ≠ ∞
hst : Disjoint s t
c : E
⊢ (fun a ↦ s.indicator (fun x ↦ c) a + t.indicator (fun x ↦ c) a) =ᵐ[μ] (s.indicator fun x ↦ c) + t.indicator fun x ↦ c
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:
by
  apply h.smul_measure
  simp

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

Goal state before:
pp: case inl
𝕜 : 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✝ : IsEmpty ι
⊢ ‖f 0‖ ≤ (‖f 0‖ + 1) * ∏ i, ‖0 i‖

Tactic:
simp [univ_eq_empty, zero_le_one]

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

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

Tactic:
by
  simp_rw [IntegrableOn, integrable_indicator_iff hs, IntegrableOn, Measure.restrict_restrict hs]

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
⊢ False

Tactic:
have : x ∈ interior (LinearMap.ker l : Set E)ᶜ := by
    rw [mem_interior_iff_mem_nhds]
    exact mem_of_superset (hs₁.mem_nhds hx) hs₃

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousSMul 𝕜 E
l : E →ₗ[𝕜] 𝕜
s : Set E
hs₁ : IsOpen[inst✝²] s
hs₃ : ∀ x ∈ s, l x ≠ 0
hl : Dense ↑l.ker
x : E
hx : x ∈ s
this : x ∈ interior (↑l.ker)ᶜ
⊢ False
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
⊢ IntegrableOn f t μ

Tactic:
by
  let u := { x ∈ s | f x ≠ 0 }
  have hu : IntegrableOn f u μ := hf.mono_set fun x hx => hx.1
  let v := toMeasurable μ u
  have A : IntegrableOn f v μ := by
    rw [IntegrableOn, hu.restrict_toMeasurable]
    · exact hu
    · intro x hx; simpa using hx.2
  have B : IntegrableOn f (t \ v) μ := by
    apply integrableOn_zero.congr
    filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt hx
    by_cases h'x : x ∈ s
    · by_contra H
      exact hx.2 (subset_toMeasurable μ u ⟨h'x, Ne.symm H⟩)
    · exact (hxt ⟨hx.1, h'x⟩).symm
  apply (A.union B).mono_set _
  rw [union_sdiff_self]
  exact subset_union_right

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

Goal state before:
pp: 𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝ : Fintype ι
this : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ Continuous[inst✝⁵, Pi.topologicalSpace] ⇑ξ.equivFun

Tactic:
let : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup

Goal state after:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module 𝕜 E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul 𝕜 E
inst✝² : CompleteSpace 𝕜
inst✝¹ : T2Space E
ι : Type v
inst✝ : Finite ι
ξ : Basis ι 𝕜 E
this✝¹ : Fintype ι
this✝ : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
⊢ Continuous[inst✝⁵, Pi.topologicalSpace] ⇑ξ.equivFun
Module: Mathlib.MeasureTheory.Integral.IntegrableOn

Goal state before:
pp: α : Type u_1
E : Type u_5
mα : MeasurableSpace α
inst✝² : NormedAddCommGroup E
μ : Measure α
l : Filter α
𝕜 : Type u_7
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → E
c : 𝕜
hc : c ≠ 0
⊢ IntegrableAtFilter (c • f) l μ ↔ IntegrableAtFilter f l μ

Tactic:
by
  refine ⟨fun hf ↦ ?_, fun h ↦ h.smul c⟩
  convert! hf.smul c⁻¹
  simp [← smul_assoc, inv_mul_cancel₀ hc]

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
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
⊢ ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = ↑↑((RingHom.id ℝ) r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x

Tactic:
RingHom.id_apply,

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
r : ℝ
u : ↥(Lp E 1 (μ.withDensity fun x ↦ ↑(f x)))
x : α
h : ↑(f x) ≠ 0 → ↑↑(r • u) x = (r • ↑↑u) x
h' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = f x • ↑↑(r • u) x
h'' : ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = (r • ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯)) x
h''' : ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x = f x • ↑↑u x
⊢ ↑↑(MemLp.toLp (fun x ↦ f x • ↑↑(r • u) x) ⋯) x = ↑↑(r • MemLp.toLp (fun x ↦ f x • ↑↑u x) ⋯) x
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

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

Tactic:
exact (norm_mkPiAlgebraFin_le_of_pos (Nat.zero_lt_succ _)).trans (le_max_left _ _)

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 (Iic b) μ ↔ IntegrableOn f (Iio b) μ

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

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: X : Type u_4
E : Type u_5
ι : Type u_6
inst✝⁷ : MeasurableSpace X
inst✝⁶ : CommMonoid E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : ContinuousMul E
L : SummationFilter ι
inst✝³ : L.NeBot
inst✝² : L.filter.IsCountablyGenerated
inst✝¹ : IsCompletelyPseudoMetrizableSpace E
inst✝ : Countable ι
f : ι → X → E
h : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable fun x ↦ ∏'[L] (i : ι), f i x

Tactic:
let E := { x | Multipliable (f · x) L }
  have hE : MeasurableSet E := StronglyMeasurable.measurableSet_exists_tendsto (by fun_prop)
  have h0 : (Eᶜ.domRestrict fun x => ∏'[L] i, f i x) = fun _ => 1 :=
    funext fun ⟨x, hx⟩ => tprod_eq_one_of_not_multipliable hx
  refine stronglyMeasurable_of_restrict_of_restrict_compl hE ?_ (h0 ▸ stronglyMeasurable_const)
  refine stronglyMeasurable_of_tendsto L.filter ?_ (tendsto_pi_nhds.mpr fun e => e.2.hasProd)
  fun_prop

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[U ∩ Z] x) μ

Tactic:
nhdsWithin_inter_of_mem (nhdsWithin_le_nhds <| hU.mem_nhds hx.1)

Goal state after:
X : Type u_1
ε : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝¹ : PseudoMetrizableSpace ε
inst✝ : LocallyCompactSpace X
x : X
U Z : Set X
hU : IsOpen[inst✝⁴] U
hZ : IsClosed[inst✝⁴] Z
hf : ∀ k ⊆ U ∩ Z, IsCompact k → IntegrableOn f k μ
hx : x ∈ U ∩ Z
K : Set X
hK : IsCompact K
hxK : x ∈ interior K
hKU : K ⊆ U
⊢ IntegrableAtFilter f (𝓝[Z] x) μ
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: case neg
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✝ : OpensMeasurableSpace X
hs : IsClosed[inst✝³] s
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)

Tactic:
rw [← isOpen_compl_iff] at hs

Goal state after:
case neg
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✝ : OpensMeasurableSpace X
hs : IsOpen[inst✝³] sᶜ
hf : LocallyIntegrableOn f s μ
x : X
h : x ∉ s
⊢ IntegrableAtFilter f (𝓝 x) (μ.restrict s)
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝⁵ : BorelSpace X
inst✝⁴ : ConditionallyCompleteLinearOrder X
inst✝³ : ConditionallyCompleteLinearOrder E
inst✝² : OrderTopology X
inst✝¹ : OrderTopology E
inst✝ : SecondCountableTopology E
f : X → E
hmono : MonotoneOn f s
a b : X
ha : IsLeast s a
hb : IsGreatest s b
h's : MeasurableSet s
⊢ MemLp f ∞ (μ.restrict s)

Tactic:
by
  borelize E
  have hbelow : BddBelow (f '' s) := ⟨f a, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono ha.1 hy (ha.2 hy)⟩
  have habove : BddAbove (f '' s) := ⟨f b, fun x ⟨y, hy, hyx⟩ => hyx ▸ hmono hy hb.1 (hb.2 hy)⟩
  have : IsBounded (f '' s) := Metric.isBounded_of_bddAbove_of_bddBelow habove hbelow
  rcases isBounded_iff_forall_norm_le.mp this with ⟨C, hC⟩
  have A : MemLp (fun _ => C) ⊤ (μ.restrict s) := memLp_top_const _
  apply MemLp.mono A (aemeasurable_restrict_of_monotoneOn h's hmono).aestronglyMeasurable
  apply (ae_restrict_iff' h's).mpr
  apply ae_of_all _ fun y hy ↦ ?_
  exact (hC _ (mem_image_of_mem f hy)).trans (le_abs_self _)

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

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
hp : Fact (1 ≤ p)
hp_ne_top : p ≠ ∞
μ : Measure β
fmeas : Measurable f
inst✝ : SeparableSpace ↑(Set.range f ∪ {0})
hf : MemLp f p μ
⊢ Tendsto (fun n ↦ MemLp.toLp ⇑(approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) ⋯) atTop (𝓝 (MemLp.toLp f hf))

Tactic:
by
  simpa only [Lp.tendsto_Lp_iff_tendsto_eLpNorm''] using
    tendsto_approxOn_range_Lp_eLpNorm hp_ne_top fmeas hf.2

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

Goal state before:
pp: case h_dense
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ DenseRange ⇑e.range.subtypeL

pp: case h_e
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ IsUniformInducing ⇑e.range.subtypeL

pp: case H
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e

Tactic:
· simpa using! h_dense

Goal state after:
case h_e
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ IsUniformInducing ⇑e.range.subtypeL

case H
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝¹⁰ : NormedDivisionRing 𝕜
inst✝⁹ : NormedDivisionRing 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁸ : AddCommGroup E
inst✝⁷ : SeminormedAddCommGroup Eₗ
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : Module 𝕜 E
inst✝⁴ : Module 𝕜₂ F
inst✝³ : IsBoundedSMul 𝕜₂ F
inst✝² : Module 𝕜 Eₗ
inst✝¹ : IsBoundedSMul 𝕜 Eₗ
inst✝ : CompleteSpace F
f : E →ₛₗ[σ₁₂] F
e : E →ₗ[𝕜] Eₗ
h_dense : DenseRange ⇑e
C : ℝ
h_norm : ∀ (x : E), ‖f x‖ ≤ C * ‖e x‖
g : Eₗ →SL[σ₁₂] F
H : ↑g ∘ₛₗ e = f
⊢ g ∘SL e.range.subtypeL = f.compLeftInverse e
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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
⊢ μ (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0

Tactic:
refine measure_mono_null (fun z => ?_) h

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_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
⊢ z ∈ ⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y} → z ∈ {a | ¬f a = g a}