mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
⊢ (Measure.pi μ).FiniteAtFilter (𝓝 x)

Tactic:
choose s hxs ho hμ using fun i => (μ i).exists_isOpen_measure_lt_top (x i)

Goal state after:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
inst✝⁴ : Fintype ι
m : (i : ι) → OuterMeasure (α i)
inst✝³ : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
inst✝² : ∀ (i : ι), SigmaFinite (μ i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), IsLocallyFiniteMeasure (μ i)
x : (i : ι) → α i
s : (i : ι) → Set (α i)
hxs : ∀ (i : ι), x i ∈ s i
ho : ∀ (i : ι), IsOpen[inst✝¹ i] (s i)
hμ : ∀ (i : ι), (μ i) (s i) < ∞
⊢ (Measure.pi μ).FiniteAtFilter (𝓝 x)
Module: Mathlib.MeasureTheory.Constructions.Pi

Goal state before:
pp: case refine_1.refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})

pp: case refine_1.refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})

Tactic:
· exact (FiniteSpanningSetsIn.pi (fun i ↦ (μ i).toFiniteSpanningSetsIn)).isCountablySpanning

Goal state after:
case refine_1.refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : Fintype γ
μ : γ → Measure α
ν : γ → Measure β
inst✝¹ : ∀ (i : γ), SigmaFinite (μ i)
inst✝ : ∀ (i : γ), SigmaFinite (ν i)
⊢ IsCountablySpanning (univ.pi '' univ.pi fun i ↦ {s | MeasurableSet s})
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
h_top

Goal state after:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_5
ε' : Type u_6
inst✝³ : TopologicalSpace ε
inst✝² : ContinuousENorm ε
inst✝¹ : TopologicalSpace ε'
inst✝ : ContinuousENorm ε'
f : α → ε
g : α → ε'
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f p μ ≤ c • eLpNorm g p μ

Tactic:
h_top

Goal state after:
case pos
α : Type u_1
F : Type u_3
G : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : α → F
g : α → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊
p : ℝ≥0∞
h0 : ¬p = 0
h_top : p = ∞
⊢ eLpNorm f ∞ μ ≤ c • eLpNorm g ∞ μ
Module: Mathlib.Data.ENNReal.Holder

Goal state before:
pp: p q : ℝ≥0∞
inst✝ : p.HolderConjugate q
⊢ p ≠ ∞ ↔ q ≠ 1

Tactic:
by
  rw [not_iff_not, eq_top_iff_eq_one p q]

Goal state after:
Module: Mathlib.Analysis.Convex.SpecificFunctions.Basic

Goal state before:
pp: ⊢ StrictConcaveOn ℝ (Ioi 0) log

Tactic:
by
  apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
  intro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
  have hy : 0 < y := hx.trans hxy
  trans y⁻¹
  · have h : 0 < z - y := by linarith
    rw [div_lt_iff₀ h]
    have hyz' : 0 < z / y := by positivity
    have hyz'' : z / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
    calc
      log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
      _ < z / y - 1 := log_lt_sub_one_of_pos hyz' hyz''
      _ = y⁻¹ * (z - y) := by field
  · have h : 0 < y - x := by linarith
    rw [lt_div_iff₀ h]
    have hxy' : 0 < x / y := by positivity
    have hxy'' : x / y ≠ 1 := by
      contrapose! h
      rw [div_eq_one_iff_eq hy.ne'] at h
      simp [h]
    calc
      y⁻¹ * (y - x) = 1 - x / y := by field
      _ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
      _ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
      _ = log y - log x := by ring

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

Goal state before:
pp: case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm f p ν ≤ eLpNorm f p μ

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ ν : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hμν : ν ≤ μ
hp0 : ¬p = 0
hp_top : ¬p = ∞
⊢ eLpNorm' f p.toReal ν ≤ eLpNorm' f p.toReal μ
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
h : MemLp f p μ
⊢ eLpNorm (fun x ↦ ‖f x‖ₑ) p μ < ∞

Tactic:
MeasureTheory.eLpNorm_enorm,

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
h : MemLp f p μ
⊢ eLpNorm f p μ < ∞
Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ContinuousENorm ε
f : α → ε
hf : AEStronglyMeasurable f μ
h : MemLp (fun x ↦ ‖f x‖ₑ) p μ
⊢ eLpNorm f p μ < ∞

Tactic:
by rw [← eLpNorm_enorm]; exact h.2

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

Goal state before:
pp: α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑(g.compMeasurePreserving f hf)) p μ = eLpNorm (↑g) p ν

Tactic:
eLpNorm_congr_ae (g.coeFn_compMeasurePreserving _)

Goal state after:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
β : Type u_8
mβ : MeasurableSpace β
f : α → β
ν : Measure β
g : β →ₘ[ν] E
hf : MeasurePreserving f μ ν
⊢ eLpNorm (↑g ∘ f) p μ = eLpNorm (↑g) p ν
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) → ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x

Tactic:
intro h j hj

Goal state after:
case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x) → ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
intro h j hj

Goal state after:
case e'_2.mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x

Tactic:
← arith_mean_weighted_of_constant s w _ (log (z j)) hw' fun i _ => congrFun rfl

Goal state after:
case e'_2.mp
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ i ∈ s, z i = 0 → w i = 0
hz' : ∀ i ∈ s, 0 < z i
this : ∏ x ∈ s, rexp (log (z x) * w x) = ∑ x ∈ s, w x * rexp (log (z x)) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ ∑ i ∈ s, w i * log (z j) = ∑ x ∈ s, log (z x) * w x
Module: Mathlib.Analysis.MeanInequalitiesPow

Goal state before:
pp: case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p

Tactic:
h_top

Goal state after:
case pos
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
⊢ a ^ p + b ^ p ≤ ∞
Module: Mathlib.Analysis.Convex.Mul

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
inst✝¹¹ : CommRing 𝕜
inst✝¹⁰ : LinearOrder 𝕜
inst✝⁹ : IsStrictOrderedRing 𝕜
inst✝⁸ : CommRing E
inst✝⁷ : LinearOrder E
inst✝⁶ : IsStrictOrderedRing E
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module 𝕜 G
inst✝³ : Module 𝕜 E
s : Set G
inst✝² : IsOrderedModule 𝕜 E
inst✝¹ : IsScalarTower 𝕜 E E
inst✝ : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
⊢ ConvexOn 𝕜 s (f ^ 0)

Tactic:
by simpa using! convexOn_const 1 hf.1

Goal state after:
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
intro j hjs

Goal state after:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i
Module: Mathlib.Analysis.MeanInequalities

Goal state before:
pp: ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal

Tactic:
rw [sum_add_distrib, sum_div, sum_div]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ↑c * eLpNorm g ∞ μ * eLpNorm f p μ = ↑c * eLpNorm f p μ * eLpNorm g ∞ μ

Tactic:
simp only [mul_assoc]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
hf : AEStronglyMeasurable f μ
g : α → F
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ ↑c * (eLpNorm g ∞ μ * eLpNorm f p μ) = ↑c * (eLpNorm f p μ * eLpNorm g ∞ μ)
Module: Mathlib.MeasureTheory.Function.LpSpace.Complete

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm f_lim p μ ≤ liminf (fun n ↦ eLpNorm (f n) p μ) atTop

Tactic:
simp_rw [eLpNorm_eq_eLpNorm' hp0 hp_top]

Goal state after:
case neg
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : SeminormedAddGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ∞
⊢ eLpNorm' f_lim p.toReal μ ≤ liminf (fun n ↦ eLpNorm' (f n) p.toReal μ) atTop
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 : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0
⊢ f = 0

Tactic:
eq_zero_iff_ae_eq_zero,

Goal state after:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : ↥(Lp E p μ)
hp : 0 < p
hf : eLpNorm (↑↑f) p μ = 0
⊢ ↑↑f =ᵐ[μ] 0
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
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ ↑↑((L + L').compLp f) =ᵐ[μ] ↑↑(L.compLp f + L'.compLp f)

Tactic:
grw [Lp.coeFn_add, coeFn_compLp', coeFn_compLp', coeFn_compLp']

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
𝕜 : Type u_6
𝕜' : Type u_7
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' F
σ : 𝕜 →+* 𝕜'
inst✝ : RingHomIsometric σ
L L' : E →SL[σ] F
f : ↥(Lp E p μ)
⊢ (fun a ↦ (L + L') (↑↑f a)) =ᵐ[μ] (fun a ↦ L (↑↑f a)) + fun a ↦ L' (↑↑f a)
Module: Mathlib.Data.Fintype.CardEmbedding

Goal state before:
pp: case refine_1
β : Type u_2
inst✝ : Fintype β
α₁ α₂ : Type u_1
h₂ : Fintype α₂
e : α₁ ≃ α₂
ih : ‖α₁ ↪ β‖ = ‖β‖.descFactorial ‖α₁‖
⊢ ‖α₂ ↪ β‖ = ‖β‖.descFactorial ‖α₂‖

Tactic:
let := Fintype.ofEquiv _ e.symm
    rw [← card_congr (Equiv.embeddingCongr e (Equiv.refl β)), ih, card_congr e]

Goal state after:
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 : α
hx : x ∈ {x | f x ≠ 0}ᶜ
⊢ ↑(f x) • g x = ↑(f x) • g' x

Tactic:
simp only [Classical.not_not, mem_ofPred_eq, mem_compl_iff] at 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 : f x = 0
⊢ ↑(f x) • g x = ↑(f x) • g' x
Module: Mathlib.MeasureTheory.Measure.Real

Goal state before:
pp: α : Type u_1
x✝ : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : μ s ≠ ∞
h₂ : μ t ≠ ∞
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ∞
⊢ ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖ * μ.real s ^ 0

Tactic:
Real.rpow_zero,

Goal state after:
case pos
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
c : E
hp_pos : p ≠ 0
hμs_pos : μ s ≠ 0
hp_top : p = ∞
⊢ ‖indicatorConstLp ∞ hs hμs c‖ = ‖c‖ * 1
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 α := ⋯
hu : IntegrableOn f u μ
v : Set α := ⋯
A : IntegrableOn f v μ
⊢ (fun x ↦ 0) =ᵐ[μ.restrict (t \ v)] f

Tactic:
filter_upwards [ae_restrict_of_ae h't,
      ae_restrict_mem₀ (ht.diff (measurableSet_toMeasurable μ u).nullMeasurableSet)] with x hxt 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.Topology.Algebra.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
⊢ FiniteDimensional 𝕜 Eᵤ

Tactic:
obtain ⟨c, hc0, hc1⟩ : ∃ c : 𝕜, 0 < ‖c‖ ∧ ‖c‖ < 1 := NormedField.exists_norm_lt 𝕜 zero_lt_one

Goal state after:
𝕜 : Type u_4
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : CompleteSpace 𝕜
Eᵤ : Type u_6
inst✝⁵ : AddCommGroup Eᵤ
inst✝⁴ : Module 𝕜 Eᵤ
inst✝³ : UniformSpace Eᵤ
inst✝² : T2Space Eᵤ
inst✝¹ : IsUniformAddGroup Eᵤ
inst✝ : ContinuousSMul 𝕜 Eᵤ
U : Set Eᵤ
hU_nhds : U ∈ 𝓝 0
hU_tb : TotallyBounded U
c : 𝕜
hc0 : 0 < ‖c‖
hc1 : ‖c‖ < 1
⊢ FiniteDimensional 𝕜 Eᵤ
Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable

Goal state before:
pp: case neg
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace E
inst✝² : Countable ι
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst✝ : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x | ∃ c, Tendsto (fun x_1 ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x
x : X
hx : x ∉ conv
⊢ (l.limUnder fun x_1 ↦ f x_1 x) = Function.extend Subtype.val (fun x ↦ l.limUnder fun x_1 ↦ f x_1 ↑x) (fun x ↦ e) x

Tactic:
rw [Function.extend_val_apply' hx, limUnder_of_not_tendsto hx]

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
ε'' : Type u_5
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace ε''
inst✝² : ESeminormedAddMonoid ε''
inst✝¹ : BorelSpace X
inst✝ : BorelSpace Y
e : X ≃ₜ Y
f : Y → ε''
μ : Measure X
h : LocallyIntegrable (f ∘ ⇑e) μ
x : Y
⊢ IntegrableAtFilter f (𝓝 x) (Measure.map (⇑e) μ)

Tactic:
rcases h (e.symm x) with ⟨U, hU, h'U⟩
    refine ⟨e.symm ⁻¹' U, e.symm.continuous.continuousAt.preimage_mem_nhds hU, ?_⟩
    apply (integrableOn_map_equiv e.toMeasurableEquiv).2
    simp only [Homeomorph.toMeasurableEquiv_coe]
    convert! h'U
    ext x
    simp only [mem_preimage, Homeomorph.symm_apply_apply]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : FinMeasAdditive μ T
h_empty : μ ∅ ≠ ∞
⊢ T ∅ = 0

Tactic:
specialize hT ∅ ∅ MeasurableSet.empty MeasurableSet.empty h_empty h_empty (disjoint_empty _)

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst✝ : AddCancelMonoid β
T : Set α → β
hT : T (∅ ∪ ∅) = T ∅ + T ∅
h_empty : μ ∅ ≠ ∞
⊢ T ∅ = 0
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ i ∈ sι, μ (S i) ≠ ∞) → (∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

Tactic:
refine Finset.induction_on sι ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ (∀ i ∈ ∅, μ (S i) ≠ ∞) → (∀ i ∈ ∅, ∀ j ∈ ∅, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ ∅, S i) = ∑ i ∈ ∅, T (S i)

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
⊢ ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      ((∀ i ∈ s, μ (S i) ≠ ∞) →
          (∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i)) →
        (∀ i ∈ insert a s, μ (S i) ≠ ∞) →
          (∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)) →
            T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑↑↑(-f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(-↑f) a✝ = (-↑↑↑f) a✝ → (toSimpleFunc (-f)) a✝ = (-⇑(toSimpleFunc f)) a✝

Tactic:
simp only [Pi.neg_apply, AddSubgroup.coe_neg]

Goal state after:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (-f)) a✝ = ↑(-↑↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑(-↑↑f) a✝ = -↑↑↑f a✝ → (toSimpleFunc (-f)) a✝ = -(toSimpleFunc f) a✝
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
⊢ ⇑g =ᵐ[μ] ⇑(SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g)

Tactic:
filter_upwards [hf] with x (hx : 0 ≤ g x)

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
g : α →ₛ G
hp : AEEqFun.mk ⇑g ⋯ ∈ Lp G p μ
hf : 0 ≤ᵐ[μ] ⇑g
x : α
hx : 0 ≤ g x
⊢ g x = (SimpleFunc.map ({x | 0 ≤ x}.piecewise id 0) g) x