awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : 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 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hst : Disjoint s t
c : E
h :
  (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)
h₁ h₂ :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ)
    (fun (a : α) ↦ HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)) fun (a : α) ↦
    HAdd.hAdd (α := E) (s.indicator (fun (x : α) ↦ c) a) (t.indicator (fun (x : α) ↦ c) a)
⊢ ((s ∪ t).indicator fun (x : α) ↦ c) =ᶠ[ae μ]
    HAdd.hAdd (α := α → E) (s.indicator fun (x : α) ↦ c) (t.indicator fun (x : α) ↦ c)

Tactic:
rw [Set.indicator_union_of_disjoint hst, Pi.add_def]

Premises used: Pi.add_def, Set.indicator_union_of_disjoint
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ (↑(↑((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] Function.const α c

Tactic:
AEEqFun.coeFn_const α c

Premises used: MeasureTheory.AEEqFun.coeFn_const, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ Eq (α := α →ₘ[μ] E) (↑((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c) : α →ₘ[μ] E) (AEEqFun.const α c)

Tactic:
rfl

Premises used: rfl, MeasureTheory.AEEqFun.mk, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ Eq (α := ↥(Lp E p μ)) (toLp (fun (x : α) ↦ c) ⋯) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c)

Tactic:
rfl

Premises used: Set.Mem, MeasureTheory.MemLp.toLp, rfl, MeasureTheory.AEEqFun.const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ Eq (α := ↥(Lp E p μ)) (MemLp.toLp (Set.indicator Set.univ fun (x : α) ↦ c) ⋯) (MemLp.toLp (fun (x : α) ↦ c) ⋯)

Tactic:
simp only [Set.indicator_univ]

Premises used: Set.indicator_univ
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
⊢ μ ≠ 0

Tactic:
have := NeZero.ne μ
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
h0 : p ≠ 0
hμ : μ ≠ 0
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const]

Premises used: MeasureTheory.Lp.norm_toLp, MeasureTheory.eLpNorm_const, MeasureTheory.MemLp.toLp_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ p ≠ 0

Tactic:
try assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
⊢ μ ≠ 0

Tactic:
try assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
inst_2 : NeZero μ
hp_zero : p ≠ 0
this : μ ≠ 0
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₁ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₂ :
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₃ rw₄ :
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal) =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]

Premises used: toReal_enorm, ENNReal.toReal_mul, MeasureTheory.measureReal_def, ENNReal.toReal_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
h0 : p ≠ 0
h_top : p ≠ ∞
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const']

Premises used: MeasureTheory.Lp.norm_toLp, MeasureTheory.eLpNorm_const', MeasureTheory.MemLp.toLp_const
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ 0

Tactic:
try assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
⊢ p ≠ ∞

Tactic:
try assumption
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ∞
rw :
  (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₁ :
  ‖c‖ₑ.toReal * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₂ :
  ‖c‖ * (HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
rw₃ rw₄ :
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal) =
    ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]

Premises used: toReal_enorm, ENNReal.toReal_mul, MeasureTheory.measureReal_def, ENNReal.toReal_rpow
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
rw : norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := Set.univ) p ⋯ ⋯ c) ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
⊢ norm (E := ↥(Lp E p μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) ≤
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
rw [← indicatorConstLp_univ]

Premises used: MeasureTheory.indicatorConstLp_univ
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := Set.univ) p ⋯ ⋯ c) ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
norm_indicatorConstLp_le

Premises used: MeasureTheory.norm_indicatorConstLp_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
c : E
⊢ norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := Set.univ) p ⋯ ⋯ c) ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)

Tactic:
exact norm_indicatorConstLp_le

Premises used: MeasureTheory.norm_indicatorConstLp_le
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
𝕜 : Type u_3
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : Fact (1 ≤ p)
⊢ 0 ≤ μ.real Set.univ ^ (1 / p.toReal)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_3
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
s : Set β
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hf : MeasurePreserving f μ μb
rwa rwa₁ rwa₂ rwa₃ : Ne (α := ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rwa [hf.measure_preimage hs.nullMeasurableSet]

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.MeasurePreserving.measure_preimage
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst : NormedAddCommGroup E
β : Type u_3
inst_1 : MeasurableSpace β
μb : Measure β
f : α → β
s : Set β
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μb : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
hf : MeasurePreserving f μ μb
⊢ Eq (α := ↥(Lp E p μ))
    ((compMeasurePreserving f hf : (a : ↥(Lp E p μb)) → ↥(Lp E p μ)) (indicatorConstLp (s := s) p hs hμs c) :
      ↥(Lp E p μ))
    (indicatorConstLp (s := f ⁻¹' s) p ⋯ ⋯ c : ↥(Lp E p μ))

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, Set.indicator, MeasureTheory.indicatorConstLp, setOf, MeasureTheory.AEEqFun.compMeasurePreserving, Set.preimage, MeasureTheory.MemLp.toLp, MeasureTheory.AEEqFun.compQuasiMeasurePreserving, rfl, MeasureTheory.AEEqFun.mk, ite
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h :
  (↑(↑(indicatorConstLp (s := s) 2 hs hμs x) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)
⊢ Eq (α := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs x)
    (ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1))

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ (↑(↑(indicatorConstLp (s := s) 2 hs hμs x) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
indicatorConstLp_coeFn.trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h :
  (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)
⊢ (↑(↑(indicatorConstLp (s := s) 2 hs hμs x) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
refine indicatorConstLp_coeFn.trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
⊢ ∀ᵐ (a : α) ∂μ,
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              α →ₘ[μ] E) :
          α → E)
        a =
      (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
        ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)

Tactic:
have h_compLp :=
    (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  ∀ᵐ (a : α) ∂μ,
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              α →ₘ[μ] E) :
          α → E)
        a =
      (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
        ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
⊢ (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)

Tactic:
rw [← EventuallyEq] at h_compLp

Premises used: Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
⊢ (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
EventuallyEq.trans ?_ h_compLp.symm

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
h :
  EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x_1 : α) ↦ x) fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
⊢ (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)

Tactic:
refine EventuallyEq.trans ?_ h_compLp.symm

Premises used: Filter.EventuallyEq.trans, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x_1 : α) ↦ x) fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)

Tactic:
(@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
h :
  ∀ (y : α)
    (hy :
      Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y)
        (s.indicator (fun (x : α) ↦ 1) y)),
    Eq.{u_2 + 1} (α := E) (s.indicator (fun (x_1 : α) ↦ x) y)
      ((fun (a : α) ↦
          ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
              ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a) :
            E))
        y)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae μ) (s.indicator fun (x_1 : α) ↦ x) fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)

Tactic:
refine (@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => ?_

Premises used: Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
y : α
hy : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y) (s.indicator (fun (x : α) ↦ 1) y)
h :
  Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
    ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
        ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y) :
      E)
⊢ Eq.{u_2 + 1} (α := E) (s.indicator (fun (x_1 : α) ↦ x) y)
    ((fun (a : α) ↦
        ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
            ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a) :
          E))
      y)

Tactic:
dsimp only
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
y : α
hy : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y) (s.indicator (fun (x : α) ↦ 1) y)
h :
  Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
    ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E) (s.indicator (fun (x : α) ↦ 1) y) : E)
⊢ Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
    ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
        ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y) :
      E)

Tactic:
rw [hy]
-- Module: Mathlib.MeasureTheory.Function.LpSpace.Indicator
Goal:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
s : Set α
inst_1 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
h_compLp :
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    fun (a : α) ↦
    (ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E)
      ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) a)
y : α
hy : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) y) (s.indicator (fun (x : α) ↦ 1) y)
h : s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
⊢ Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
    ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E) (s.indicator (fun (x : α) ↦ 1) y) : E)

Tactic:
simp_rw [ContinuousLinearMap.toSpanSingleton_apply]

Premises used: ContinuousLinearMap.toSpanSingleton_apply