awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : Eq (α := ℝ) 2 (↑2 : ℝ)
e_a :
  HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
⊢ ENNReal.ofReal (HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ 2) =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)

Tactic:
rw [← Real.rpow_natCast _ 2, ← h_two, ←
    ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two, ofReal_norm]

Premises used: ENNReal.ofReal_rpow_of_nonneg, zero_le_two, ofReal_norm, OfNat.ofNat, norm_nonneg, Real.rpow_natCast
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
x : α
h_two : Eq (α := ℝ) 2 (↑2 : ℝ)
e_a e_a₁ e_a₂ e_a₃ :
  HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)
⊢ HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖ₑ 2 =
    (↑(HPow.hPow (β := ℕ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) x‖₊ 2) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ENNReal.toReal 2 = 2

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
⊢ ENNReal.toReal 2 = 2

Tactic:
have h_two : (2 : ℝ≥0∞).toReal = 2 := by simp
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
rw :
  HPow.hPow (β := ℕ) (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ) 2 =
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ
rw₁ : ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ ≠ ∞
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (RCLike.re : (a : 𝕜) → ℝ) ⟪f, f⟫

Tactic:
rw [inner_def, integral_inner_eq_sq_eLpNorm, norm_def, ← ENNReal.toReal_pow, RCLike.ofReal_re,
    ENNReal.toReal_eq_toReal_iff' (ENNReal.pow_ne_top (Lp.eLpNorm_ne_top f)) _]

Premises used: ENNReal.toReal_eq_toReal_iff', RCLike.ofReal_re, MeasureTheory.L2.inner_def, ENNReal.pow_ne_top, MeasureTheory.L2.integral_inner_eq_sq_eLpNorm, ENNReal.toReal_pow, MeasureTheory.Lp.eLpNorm_ne_top, MeasureTheory.Lp.norm_def
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
rw :
  (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ₑ 2 ∂μ) ^ HMul.hMul (α := ℝ) 2⁻¹ (↑2 : ℝ) =
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ
⊢ HPow.hPow (β := ℕ) (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ) 2 =
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ

Tactic:
rw [← ENNReal.rpow_natCast, eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top, eLpNorm', ←
      ENNReal.rpow_mul, one_div, h_two]

Premises used: ENNReal.rpow_mul, ENNReal.ofNat_ne_top, MeasureTheory.eLpNorm', ENNReal.rpow_natCast, MeasureTheory.eLpNorm_eq_eLpNorm', two_ne_zero, one_div
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ₑ 2 ∂μ) ^ HMul.hMul (α := ℝ) 2⁻¹ (↑2 : ℝ) =
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ

Tactic:
simp [enorm_eq_nnnorm]

Premises used: enorm_eq_nnnorm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ ≠ ∞

Tactic:
(lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top zero_lt_two (ε := E) ?_).ne

Premises used: MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top, zero_lt_two, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
refine : eLpNorm' (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞
⊢ ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ ≠ ∞

Tactic:
refine (lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top zero_lt_two (ε := E) ?_).ne

Premises used: MeasureTheory.lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top, zero_lt_two, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
rw : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞
⊢ eLpNorm' (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞

Tactic:
rw [← h_two, ← eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, MeasureTheory.eLpNorm_eq_eLpNorm', two_ne_zero
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f : ↥(Lp E 2 μ)
h_two : ENNReal.toReal 2 = 2
⊢ eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
simp_rw :
  eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] 𝕜)) (Lp 𝕜 1 μ)
    (AEEqFun.mk (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) ⋯)

Tactic:
simp_rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_aeeqFun]

Premises used: MeasureTheory.Lp.mem_Lp_iff_eLpNorm_lt_top, MeasureTheory.eLpNorm_aeeqFun
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞

Tactic:
eLpNorm_inner_lt_top f g

Premises used: MeasureTheory.L2.eLpNorm_inner_lt_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞

Tactic:
exact eLpNorm_inner_lt_top f g

Premises used: MeasureTheory.L2.eLpNorm_inner_lt_top
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
⊢ Integrable.{u_4, u_1} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) μ

Tactic:
(integrable_congr
        (AEEqFun.coeFn_mk (fun x => ⟪f x, g x⟫)
          ((Lp.aestronglyMeasurable f).inner (Lp.aestronglyMeasurable g)))).mp
    (AEEqFun.integrable_iff_mem_L1.mpr (mem_L1_inner f g))

Premises used: Iff.mpr, MeasureTheory.integrable_congr, MeasureTheory.Lp.aestronglyMeasurable, Inner.inner, MeasureTheory.AEEqFun.integrable_iff_mem_L1, MeasureTheory.AEEqFun.cast, MeasureTheory.AEEqFun.coeFn_mk, MeasureTheory.AEStronglyMeasurable.inner, MeasureTheory.L2.mem_L1_inner, Iff.mp, Subtype.val
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
simp_rw :
  Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(f + f') : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑f' : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
⊢ ⟪f + f', g⟫ = ⟪f, g⟫ + ⟪f', g⟫

Tactic:
simp_rw [inner_def, ← integral_add (integrable_inner (𝕜 := 𝕜) f g) (integrable_inner f' g),
    ← inner_add_left]

Premises used: MeasureTheory.L2.inner_def, inner_add_left, MeasureTheory.L2.integrable_inner, MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(f + f') : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑f' : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)

Tactic:
integral_congr_ae ((coeFn_add f f').mono fun x hx => ?_)

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.integral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
refine :
  ∀ (x : α)
    (hx : (↑(↑(f + f') : α →ₘ[μ] E) : α → E) x = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑f' : α →ₘ[μ] E) : α → E)) x),
    Eq.{u_4 + 1} (α := 𝕜) ((fun (a : α) ↦ ⟪(↑(↑(f + f') : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫) x)
      ((fun (a : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑f' : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫)
        x)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(f + f') : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α), ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑f' : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)

Tactic:
refine integral_congr_ae ((coeFn_add f f').mono fun x hx => ?_)

Premises used: MeasureTheory.Lp.coeFn_add, MeasureTheory.integral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f f' g : ↥(Lp E 2 μ)
x : α
hx : (↑(↑(f + f') : α →ₘ[μ] E) : α → E) x = ((↑(↑f : α →ₘ[μ] E) : α → E) + (↑(↑f' : α →ₘ[μ] E) : α → E)) x
⊢ Eq.{u_4 + 1} (α := 𝕜) ((fun (a : α) ↦ ⟪(↑(↑(f + f') : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫) x)
    ((fun (a : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a + (↑(↑f' : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫) x)

Tactic:
simp only [hx, Pi.add_apply]

Premises used: Pi.add_apply
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
rw :
  Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α),
      HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
        ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
⊢ ⟪r • f, g⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪f, g⟫

Tactic:
rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]

Premises used: MeasureTheory.L2.inner_def, MeasureTheory.integral_smul, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α),
      HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
        ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)

Tactic:
integral_congr_ae ((coeFn_smul r f).mono fun x hx => ?_)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.Lp.coeFn_smul, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
refine :
  ∀ (x : α) (hx : (↑(↑(r • f) : α →ₘ[μ] E) : α → E) x = (r • (↑(↑f : α →ₘ[μ] E) : α → E)) x),
    Eq.{u_4 + 1} (α := 𝕜) ((fun (a : α) ↦ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫) x)
      ((fun (a : α) ↦
          HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
            ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫)
        x)
⊢ Eq.{u_4 + 1} (α := 𝕜) (∫ (a : α), ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (a : α),
      HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
        ⟪(↑(↑f : α →ₘ[μ] E) : α → E) a, (↑(↑g : α →ₘ[μ] E) : α → E) a⟫ ∂μ)

Tactic:
refine integral_congr_ae ((coeFn_smul r f).mono fun x hx => ?_)

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.Lp.coeFn_smul, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
f g : ↥(Lp E 2 μ)
r : 𝕜
x : α
hx : (↑(↑(r • f) : α →ₘ[μ] E) : α → E) x = (r • (↑(↑f : α →ₘ[μ] E) : α → E)) x
rw :
  ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
rw₁ :
  ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
rw₂ :
  ⟪(r • (↑(↑f : α →ₘ[μ] E) : α → E)) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
rw₃ rw₄ :
  ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
⊢ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫

Tactic:
rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]

Premises used: smul_eq_mul, inner_smul_left, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
inst_4 : NormedAddCommGroup F
x x_1 : ↥(Lp E 2 μ)
simp_rw :
  Eq (α := 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (∫ (a : α), ⟪(↑(↑x_1 : α →ₘ[μ] E) : α → E) a, (↑(↑x : α →ₘ[μ] E) : α → E) a⟫ ∂μ) : 𝕜)
    (∫ (a : α), ⟪(↑(↑x : α →ₘ[μ] E) : α → E) a, (↑(↑x_1 : α →ₘ[μ] E) : α → E) a⟫ ∂μ : 𝕜)
simp_rw₁ :
  Eq.{u_4 + 1} (α := 𝕜)
    (∫ (x_2 : α), (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑(↑x_1 : α →ₘ[μ] E) : α → E) x_2, (↑(↑x : α →ₘ[μ] E) : α → E) x_2⟫ ∂μ)
    (∫ (a : α), ⟪(↑(↑x : α →ₘ[μ] E) : α → E) a, (↑(↑x_1 : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x_1, x⟫ = ⟪x, x_1⟫

Tactic:
simp_rw [inner_def, ← integral_conj, inner_conj_symm]

Premises used: MeasureTheory.L2.inner_def, integral_conj, inner_conj_symm
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  Eq.{u_4 + 1} (α := 𝕜)
    (∫ (a : α), ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (x : α), s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x ∂μ)
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ

Tactic:
rw [inner_def, ← integral_indicator hs]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.L2.inner_def
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_4 + 1} (α := 𝕜)
    (∫ (a : α), ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (x : α), s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x ∂μ)

Tactic:
integral_congr_ae ((@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs c).mono fun x hx ↦ ?_)

Premises used: MeasureTheory.integral_congr_ae, Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∀ (x : α) (hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x),
    Eq.{u_4 + 1} (α := 𝕜)
      ((fun (a : α) ↦
          ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫)
        x)
      (s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x)
⊢ Eq.{u_4 + 1} (α := 𝕜)
    (∫ (a : α), ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫ ∂μ)
    (∫ (x : α), s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x ∂μ)

Tactic:
refine integral_congr_ae ((@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs c).mono fun x hx ↦ ?_)

Premises used: MeasureTheory.integral_congr_ae, Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x
pos :
  ∀ (hxs : x ∈ s),
    ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
      s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x
neg :
  ∀ (hxs : x ∉ s),
    ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
      s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x
⊢ ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
    s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x

Tactic:
by_cases hxs : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x
hxs : x ∈ s
⊢ ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
    s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x

Tactic:
simp [hx, hxs]
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x
hxs : x ∉ s
⊢ ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
    s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x

Tactic:
simp [hx, hxs]
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x
⊢ ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
    s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x

Tactic:
have : ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = s.indicator (fun x ↦ ⟪c, f x⟫) x := by
    by_cases hxs : x ∈ s <;> simp [hx, hxs]
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
f : ↥(Lp E 2 μ)
hs : MeasurableSet s
c : E
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : (↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x = s.indicator (fun (x : α) ↦ c) x
this :
  ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) x, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ =
    s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x
⊢ Eq.{u_4 + 1} (α := 𝕜)
    ((fun (a : α) ↦ ⟪(↑(↑(indicatorConstLp (s := s) 2 hs hμs c) : α →ₘ[μ] E) : α → E) a, (↑(↑f : α →ₘ[μ] E) : α → E) a⟫)
      x)
    (s.indicator (fun (x : α) ↦ ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫) x)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.L2Space
Goal:
α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
s : Set α
inst_4 : CompleteSpace E
inst_5 : NormedSpace ℝ E
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : E
f : ↥(Lp E 2 μ)
rw : ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := 𝕜) (∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ)
    (∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ)
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ⟪c, ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E) : α → E) x ∂μ⟫

Tactic:
rw [← integral_inner (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
    L2.inner_indicatorConstLp_eq_setIntegral_inner]

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, integral_inner, MeasureTheory.L2.inner_indicatorConstLp_eq_setIntegral_inner, Fact.elim