awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 ∂μ
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (RCLike.re : (a : 𝕜) → ℝ) ⟪f, f⟫
have rw₁ : ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ ≠ ∞
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)) _]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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
⊢ HPow.hPow (β := ℕ) (eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ) 2 =
    ∫⁻ (a : α), HPow.hPow (β := ℝ) (↑‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖₊ : ℝ≥0∞) 2 ∂μ
have rw : (∫⁻ (a : α), HPow.hPow (β := ℝ) ‖(↑(↑f : α →ₘ[μ] E) : α → E) a‖ₑ 2 ∂μ) ^ HMul.hMul (α := ℝ) 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 ∂μ ≠ ∞
have refine : eLpNorm' (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞
Tactic: refine (lintegral_rpow_enorm_lt_top_of_eLpNorm'_lt_top zero_lt_two (ε := E) ?_).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 μ < ∞
have rw : eLpNorm (↑(↑f : α →ₘ[μ] E) : α → E) 2 μ < ∞
Tactic: rw [← h_two, ← eLpNorm_eq_eLpNorm' two_ne_zero ENNReal.ofNat_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 μ)
⊢ Membership.mem (γ := AddSubgroup (α →ₘ[μ] 𝕜)) (Lp 𝕜 1 μ)
    (AEEqFun.mk (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) ⋯)
have simp_rw : eLpNorm.{u_1, u_4} (ε := 𝕜) (fun (x : α) ↦ ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫) 1 μ < ∞
Tactic: simp_rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_aeeqFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 μ)
⊢ ⟪f + f', g⟫ = ⟪f, g⟫ + ⟪f', g⟫
have 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⟫ ∂μ)
Tactic: simp_rw [inner_def, ← integral_add (integrable_inner (𝕜 := 𝕜) f g) (integrable_inner f' g),
    ← inner_add_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫ ∂μ)
have 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)
Tactic: refine integral_congr_ae ((coeFn_add f f').mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 : 𝕜
⊢ ⟪r • f, g⟫ = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) ⟪f, g⟫
have 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⟫ ∂μ)
Tactic: rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫ ∂μ)
have 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)
Tactic: refine integral_congr_ae ((coeFn_smul r f).mono fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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
⊢ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
have rw : ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
  HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
    ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
Tactic: rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫
⊢ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
have rw₁ : ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
  ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
Tactic: rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫
⊢ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
have rw₂ : ⟪(r • (↑(↑f : α →ₘ[μ] E) : α → E)) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
  ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
Tactic: rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫
⊢ ⟪(↑(↑(r • f) : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
    HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜)
      ⟪(↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
have rw₃ : ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫ =
  ⟪r • (↑(↑f : α →ₘ[μ] E) : α → E) x, (↑(↑g : α →ₘ[μ] E) : α → E) x⟫
Tactic: rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 μ)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x_1, x⟫ = ⟪x, x_1⟫
have 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⟫ ∂μ : 𝕜)
Tactic: simp_rw [inner_def, ← integral_conj, inner_conj_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫ ∂μ : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x_1, x⟫ = ⟪x, x_1⟫
have 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⟫ ∂μ)
Tactic: simp_rw [inner_def, ← integral_conj, inner_conj_symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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∞)
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ
have 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 ∂μ)
Tactic: rw [inner_def, ← integral_indicator hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 ∂μ)
have 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)
Tactic: refine integral_congr_ae ((@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs c).mono fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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
have 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
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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
⊢ ⟪(↑(↑(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
have 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
Tactic: by_cases hxs : x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 μ)
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ⟪c, ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E) : α → E) x ∂μ⟫
have rw : ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ∫ (x : α) in s, ⟪c, (↑(↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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⟫ ∂μ
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs c, f⟫ = ⟪c, ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] E) : α → E) x ∂μ⟫
have rw₁ : Eq.{u_4 + 1} (α := 𝕜) (∫ (x : α) in s, ⟪c, (↑(↑f : α →ₘ[μ] E) : α → E) x⟫ ∂μ)
  (∫ (x : α) in s, ⟪c, (↑(↑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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp 𝕜 2 μ)
⊢ ⟪indicatorConstLp (s := s) 2 hs hμs 1, f⟫ = ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ
have rw : inner 𝕜 (E := 𝕜) 1 (∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ) = ∫ (x : α) in s, (↑(↑f : α →ₘ[μ] 𝕜) : α → 𝕜) x ∂μ
Tactic: rw [L2.inner_indicatorConstLp_eq_inner_setIntegral 𝕜 hs hμs (1 : 𝕜) f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 t : Set α
inst_4 : CompleteSpace E
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∞)
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
⊢ inner 𝕜 (E := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs a) (indicatorConstLp (s := t) 2 ht hμt b) =
    μ.real (s ∩ t) • ⟪a, b⟫
have rw : ⟪a, ∫ (x : α) in s, (↑(↑(indicatorConstLp (s := t) 2 ht hμt b) : α →ₘ[μ] E) : α → E) x ∂μ⟫ = μ.real (s ∩ t) • ⟪a, b⟫
Tactic: rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
    inner_smul_right_eq_smul, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 t : Set α
inst_4 : CompleteSpace E
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∞)
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
rw :
  ⟪a, ∫ (x : α) in s, (↑(↑(indicatorConstLp (s := t) 2 ht hμt b) : α →ₘ[μ] E) : α → E) x ∂μ⟫ = μ.real (s ∩ t) • ⟪a, b⟫
⊢ inner 𝕜 (E := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs a) (indicatorConstLp (s := t) 2 ht hμt b) =
    μ.real (s ∩ t) • ⟪a, b⟫
have rw₁ : ⟪a, μ.real (t ∩ s) • b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
Tactic: rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
    inner_smul_right_eq_smul, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 t : Set α
inst_4 : CompleteSpace E
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∞)
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
rw :
  ⟪a, ∫ (x : α) in s, (↑(↑(indicatorConstLp (s := t) 2 ht hμt b) : α →ₘ[μ] E) : α → E) x ∂μ⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₁ : ⟪a, μ.real (t ∩ s) • b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
⊢ inner 𝕜 (E := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs a) (indicatorConstLp (s := t) 2 ht hμt b) =
    μ.real (s ∩ t) • ⟪a, b⟫
have rw₂ : μ.real (t ∩ s) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
Tactic: rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
    inner_smul_right_eq_smul, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
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 t : Set α
inst_4 : CompleteSpace E
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∞)
a b : E
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
rw :
  ⟪a, ∫ (x : α) in s, (↑(↑(indicatorConstLp (s := t) 2 ht hμt b) : α →ₘ[μ] E) : α → E) x ∂μ⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₁ : ⟪a, μ.real (t ∩ s) • b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
rw₂ : μ.real (t ∩ s) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
⊢ inner 𝕜 (E := ↥(Lp E 2 μ)) (indicatorConstLp (s := s) 2 hs hμs a) (indicatorConstLp (s := t) 2 ht hμt b) =
    μ.real (s ∩ t) • ⟪a, b⟫
have rw₃ : μ.real (s ∩ t) • ⟪a, b⟫ = μ.real (s ∩ t) • ⟪a, b⟫
Tactic: rw [inner_indicatorConstLp_eq_inner_setIntegral, setIntegral_indicatorConstLp hs,
    inner_smul_right_eq_smul, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (goal)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ inner 𝕜 (E := ↥(Lp 𝕜 2 μ)) ((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f : ↥(Lp 𝕜 2 μ))
      ((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g : ↥(Lp 𝕜 2 μ)) =
    ∫ (x : α),
      HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) x : 𝕜)
        ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) x : 𝕜) : 𝕜) ∂μ
have h : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (fun (a : α) ↦
    inner 𝕜 (E := 𝕜)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
      ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
  fun (a : α) ↦
  HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.L2Space (hypothesis)
Goal:
α : Type u_1
𝕜 : Type u_2
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : RCLike 𝕜
μ : Measure α
inst_4 : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
    (fun (a : α) ↦
      inner 𝕜 (E := 𝕜)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) a)
        ((↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) g) : α →ₘ[μ] 𝕜) : α → 𝕜) a))
    fun (a : α) ↦
    HMul.hMul (α := 𝕜) (β := 𝕜) ((g : (a : α) → 𝕜) a : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((f : (a : α) → 𝕜) a : 𝕜) : 𝕜)
have hf_ae : EventuallyEq.{u_1, u_2} (β := 𝕜) (ae μ)
  (↑(↑((BoundedContinuousFunction.toLp 2 μ 𝕜 : (a : α →ᵇ 𝕜) → ↥(Lp 𝕜 2 μ)) f) : α →ₘ[μ] 𝕜) : α → 𝕜) (⇑f : (a : α) → 𝕜)
Tactic: have hf_ae := f.coeFn_toLp 2 μ 𝕜