awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
h :
  ∀ (x : α) (hx : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) x) (0 x)),
    HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) x = 0 x
⊢ HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
filter_upwards [Lp.coeFn_zero E q μ] with x hx

Premises used: MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
x : α
hx : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) x) (0 x)
h : HSMul.hSMul (β := E) ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x) = 0 x
⊢ HSMul.hSMul (β := α → E) (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑0 : α →ₘ[μ] E) : α → E) x = 0 x

Tactic:
rw [Pi.smul_apply', hx]

Premises used: Pi.smul_apply'
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
x : α
hx : Eq.{u_4 + 1} (α := E) ((↑(↑0 : α →ₘ[μ] E) : α → E) x) (0 x)
⊢ HSMul.hSMul (β := E) ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x) = 0 x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
MemLp.zero (ε := E) |>.toLp_zero

Premises used: MeasureTheory.MemLp.zero, MeasureTheory.MemLp.toLp_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ HSMul.hSMul (α := ↥(Lp 𝕜 p μ)) 0 f = 0

Tactic:
convert! MemLp.zero (ε := E) |>.toLp_zero

Premises used: MeasureTheory.MemLp.zero, MeasureTheory.MemLp.toLp_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
apply : HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply MemLp.toLp_congr _ _ ?_

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
h :
  ∀ (x : α) (hx : Eq.{u_3 + 1} (α := 𝕜) ((↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x)),
    HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x
⊢ HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] 0

Tactic:
filter_upwards [Lp.coeFn_zero 𝕜 p μ] with x hx

Premises used: MeasureTheory.Lp.coeFn_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
x : α
hx : Eq.{u_3 + 1} (α := 𝕜) ((↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x)
h : HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (0 x) ((↑(↑f : α →ₘ[μ] E) : α → E) x) = 0 x
⊢ HSMul.hSMul (α := α → 𝕜) (↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) (↑(↑f : α →ₘ[μ] E) : α → E) x = 0 x

Tactic:
rw [Pi.smul_apply', hx]

Premises used: Pi.smul_apply'
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp E q μ)
x : α
hx : Eq.{u_3 + 1} (α := 𝕜) ((↑(↑0 : α →ₘ[μ] 𝕜) : α → 𝕜) x) (0 x)
⊢ HSMul.hSMul.{u_3, u_4, u_4} (α := 𝕜) (0 x) ((↑(↑f : α →ₘ[μ] E) : α → E) x) = 0 x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ f • -g = -(f • g)

Tactic:
simp [eq_neg_iff_add_eq_zero, ← Lp.add_smul]

Premises used: MeasureTheory.Lp.add_smul, eq_neg_iff_add_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ -f • g = -(f • g)

Tactic:
simp [eq_neg_iff_add_eq_zero, ← Lp.smul_add]

Premises used: MeasureTheory.Lp.smul_add, eq_neg_iff_add_eq_zero
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
⊢ -f • -g = f • g

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ c • f • g = f • c • g

Tactic:
simp only [smul_def, ← MemLp.toLp_const_smul]

Premises used: MeasureTheory.Lp.smul_def, MeasureTheory.MemLp.toLp_const_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
hfg :
  c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply MemLp.toLp_congr

Premises used: MeasureTheory.MemLp.toLp_congr
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
h :
  ∀ (x : α) (hfx : (↑(↑(c • f) : α →ₘ[μ] 𝕜) : α → 𝕜) x = (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜)) x)
    (hgx : (↑(↑(c • g) : α →ₘ[μ] E) : α → E) x = (c • (↑(↑g : α →ₘ[μ] E) : α → E)) x),
    (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
      ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)) x
⊢ c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)

Tactic:
filter_upwards [Lp.coeFn_smul c f, Lp.coeFn_smul c g] with x hfx hgx

Premises used: MeasureTheory.Lp.coeFn_smul
-- Module: Mathlib.MeasureTheory.Function.Holder
Goal:
α : Type u_1
𝕜' : Type u_2
𝕜 : Type u_3
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p q r : ℝ≥0∞
hpqr : p.HolderTriple q r
inst : NormedRing 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
inst_4 : NormedRing 𝕜'
inst_5 : Module 𝕜' E
inst_6 : Module 𝕜' 𝕜
inst_7 : IsBoundedSMul 𝕜' E
inst_8 : IsBoundedSMul 𝕜' 𝕜
inst_9 : SMulCommClass 𝕜' 𝕜 E
c : 𝕜'
f : ↥(Lp 𝕜 p μ)
g : ↥(Lp E q μ)
x : α
hfx : (↑(↑(c • f) : α →ₘ[μ] 𝕜) : α → 𝕜) x = (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜)) x
hgx : (↑(↑(c • g) : α →ₘ[μ] E) : α → E) x = (c • (↑(↑g : α →ₘ[μ] E) : α → E)) x
⊢ (c • (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑g : α →ₘ[μ] E) : α → E)) x =
    ((↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) • (↑(↑(c • g) : α →ₘ[μ] E) : α → E)) x

Tactic:
simp [smul_comm, hgx]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have hN₀ : μ N = 0 := measure_iUnion_null fun u ↦ meas_eLpNormEssSup_lt
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
simp_rw : ((⋂ n ∈ u, s n) \ N).Nonempty → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)

Tactic:
simp_rw [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
hx.2 (mem_iUnion.2 ⟨u, ?_⟩)

Premises used: Iff.mpr, Set.mem_iUnion, And.right, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
refine : x ∈ M (indicator (⋂ n ∈ u, s n) 1)
⊢ False

Tactic:
refine hx.2 (mem_iUnion.2 ⟨u, ?_⟩)

Premises used: Iff.mpr, Set.mem_iUnion, And.right, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : 0 < (↑(nnnorm (E := ℝ) (1 x)) : ℝ≥0∞)
rw₁ : (ae μ).EventuallyEq (β := ℝ) (indicator (⋂ n ∈ u, s n) 1) 0
⊢ x ∈ M (indicator (⋂ n ∈ u, s n) 1)

Tactic:
rw [mem_setOf, indicator_of_mem hx.1, eLpNormEssSup_eq_zero_iff.2]

Premises used: Iff.mpr, Set.mem_setOf, Set.indicator_of_mem, And.left, MeasureTheory.eLpNormEssSup_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 < (↑(nnnorm (E := ℝ) (1 x)) : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
u : Finset ℕ
x : α
hx : x ∈ (⋂ n ∈ u, s n) \ N
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋂ n ∈ u, s n) ∩ support (M := ℝ) 1) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⋂ n ∈ u, s n) ∩ univ) : ℝ≥0∞) (0 : ℝ≥0∞)
rwa₂ rwa₃ rwa₄ rwa₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ) (indicator (⋂ n ∈ u, s n) 1) 0

Tactic:
rwa [indicator_ae_eq_zero, Function.support_one, inter_univ]

Premises used: Set.inter_univ, Set.indicator_ae_eq_zero, Function.support_one
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)

Tactic:
have hN₁ (u : Finset ℕ) : ((⋂ n ∈ u, s n) \ N).Nonempty → 0 < μ (⋂ n ∈ u, s n) := by
    simp_rw [pos_iff_ne_zero]
    rintro ⟨x, hx⟩ hu
    refine hx.2 (mem_iUnion.2 ⟨u, ?_⟩)
    rw [mem_setOf, indicator_of_mem hx.1, eLpNormEssSup_eq_zero_iff.2]
    · simp
    · rwa [indicator_ae_eq_zero, Function.support_one, inter_univ]
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
⊢ ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)

Tactic:
simp only [f, Pi.smul_apply, Finset.sum_apply,
    forall_const, imp_true_iff, smul_eq_mul]

Premises used: Finset.sum_apply, imp_true_iff, forall_const, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
⊢ ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)

Tactic:
have hfapp : ∀ n a, f n a = (↑(n + 1))⁻¹ * ∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a := by
    simp only [f, Pi.smul_apply, Finset.sum_apply,
    forall_const, imp_true_iff, smul_eq_mul]
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
n i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ MeasurableSet (s i)

Tactic:
hs _
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
n i : ℕ
h : i ∈ Finset.range (n + 1)
⊢ MeasurableSet (s i)

Tactic:
exact hs _
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
n : ℕ
funProp : ∀ i ∈ Finset.range (n + 1), MeasurableSet (s i)
⊢ Measurable (f n)

Tactic:
fun_prop (disch := exact hs _)
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
⊢ ∀ (n : ℕ), Measurable (f n)

Tactic:
have hf n : Measurable (f n) := by fun_prop (disch := exact hs _)
-- Module: Mathlib.MeasureTheory.Function.Intersectivity
Goal:
α : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
r : ℝ≥0∞
s : ℕ → Set α
hs : ∀ (n : ℕ), MeasurableSet (s n)
hr₀ : r ≠ 0
hr : ∀ (n : ℕ), r ≤ (μ : (a : Set α) → ℝ≥0∞) (s n)
M : (f : α → ℝ) → Set α := fun (f : α → ℝ) ↦ {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
N : Set α := ⋃ (u : Finset ℕ), M (indicator (⋂ n ∈ u, s n) 1)
hN₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
hN₁ :
  ∀ (u : Finset ℕ),
    ((⋂ n ∈ u, s n) \ N).Nonempty → LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ n ∈ u, s n) : ℝ≥0∞)
f : (n : ℕ) → α → ℝ≥0∞ :=
  fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ≥0∞) (β := (x : α) → ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1)
hfapp :
  ∀ (n : ℕ) (a : α), f n a = HMul.hMul (α := ℝ≥0∞) (↑(n + 1) : ℝ≥0∞)⁻¹ (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a)
hf : ∀ (n : ℕ), Measurable (f n)
n : ℕ
a : α
rw : HDiv.hDiv (α := ℝ≥0∞) (∑ k ∈ Finset.range (n + 1), (s k).indicator 1 a) (↑(n + 1) : ℝ≥0∞) ≤ 1 a
⊢ f n a ≤ 1 a

Tactic:
rw [hfapp, ← ENNReal.div_eq_inv_mul]

Premises used: ENNReal.div_eq_inv_mul