awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have 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)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
⊢ (‖c‖ₑ * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 / p.toReal)).toReal =
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw₃ : ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal) =
  ‖c‖ * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) Set.univ) ^ (1 / p.toReal)
Tactic: rw [measureReal_def, ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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 μ)) ((Lp.const p μ : (a : E) → ↥(Lp E p μ)) c : ↥(Lp E p μ)) ≤
    ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
have rw : norm (E := ↥(Lp E p μ)) (indicatorConstLp (s := Set.univ) p sorry sorry c) ≤ ‖c‖ * μ.real Set.univ ^ (1 / p.toReal)
Tactic: rw [← indicatorConstLp_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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
⊢ 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))
have 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)
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
have h : (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
  (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
        α →ₘ[μ] E) :
    α → E)
Tactic: refine indicatorConstLp_coeFn.trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
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
⊢ (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)
have 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)
Tactic: have h_compLp :=
    (ContinuousLinearMap.toSpanSingleton ℝ x).coeFn_compLp (indicatorConstLp 2 hs hμs (1 : ℝ))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (hypothesis)
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)
⊢ (s.indicator fun (x_1 : α) ↦ x) =ᶠ[ae μ]
    (↑(↑(ContinuousLinearMap.compLp (ContinuousLinearMap.toSpanSingleton ℝ x) (indicatorConstLp (s := s) 2 hs hμs 1)) :
          α →ₘ[μ] E) :
      α → E)
have 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)
Tactic: rw [← EventuallyEq] at h_compLp
Cleared hypotheses: h_compLp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
have 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)
Tactic: refine EventuallyEq.trans ?_ h_compLp.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
have 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)
Tactic: refine (@indicatorConstLp_coeFn _ _ _ 2 μ _ s hs hμs (1 : ℝ)).mono fun y hy => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
⊢ 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)
have h : Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
  ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E) (s.indicator (fun (x : α) ↦ 1) y) : E)
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
⊢ Eq (α := E) (s.indicator (fun (x_1 : α) ↦ x) y : E)
    ((ContinuousLinearMap.toSpanSingleton ℝ x : (a : ℝ) → E) (s.indicator (fun (x : α) ↦ 1) y) : E)
have h : s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
Tactic: simp_rw [ContinuousLinearMap.toSpanSingleton_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
⊢ s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
have pos : ∀ (hy_mem : y ∈ s), s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
Tactic: by_cases hy_mem : y ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.LpSpace.Indicator (goal)
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)
pos : ∀ (hy_mem : y ∈ s), s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
⊢ s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
have neg : ∀ (hy_mem : y ∉ s), s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
Tactic: by_cases hy_mem : y ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : MeasurableSpace β
inst_2 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (hs.piecewise (s := s) f) μ
have choose : ∀ (p : (i : ι) → α → β) (hp : ∀ (i : ι), Measurable (p i)) (hq : ∀ (i : ι), f i =ᶠ[ae μ] p i),
  AEMeasurable (hs.piecewise (s := s) f) μ
Tactic: choose p hp hq using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : MeasurableSpace β
inst_2 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
p : (i : ι) → α → β
hp : ∀ (i : ι), Measurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
⊢ AEMeasurable (hs.piecewise (s := s) f) μ
have refine : hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
Tactic: refine ⟨hs.piecewise p, hs.measurable_piecewise hm hp, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : MeasurableSpace β
inst_2 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
p : (i : ι) → α → β
hp : ∀ (i : ι), Measurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), f i a = p i a) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x) x} x}
    a
Tactic: filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
μ : Measure α
inst_1 : MeasurableSpace β
inst_2 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
p : (i : ι) → α → β
hp : ∀ (i : ι), Measurable (p i)
hq : ∀ (i : ι), f i =ᶠ[ae μ] p i
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ι), f i a = p i a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x) x}
            x}
      a
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
have h₁ : ∀ (a : α), (∀ (i : ι), f i a = p i a) → hs.piecewise (s := s) f a = hs.piecewise (s := s) p a
Tactic: filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have pos : ∀ (Fi : Finite ι), StronglyMeasurable (hs.piecewise (s := s) f)
Tactic: by_cases Fi : Finite ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
pos : ∀ (Fi : Finite ι), StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg : ∀ (Fi : ¬Finite ι), StronglyMeasurable (hs.piecewise (s := s) f)
Tactic: by_cases Fi : Finite ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Finite ι
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have pos : ∀ (x : α),
  Tendsto
    (fun (n : ℕ) ↦
      ((fun (n : ℕ) ↦ (hs.simpleFunc_piecewise (s := s) hm fun (i : ι) ↦ sorry.approx n : SimpleFunc α β)) n : (a : α) → β)
        x)
    atTop (nhds (hs.piecewise (s := s) f x))
Tactic: refine ⟨fun n => simpleFunc_piecewise hs hm (fun i => (hf i).approx n), fun x => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : ¬Finite ι
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have Fi₁ : Infinite ι
Tactic: simp only [not_finite_iff_infinite] at Fi
Cleared hypotheses: Fi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
⊢ StronglyMeasurable (hs.piecewise (s := s) f)
have neg : ∀ (e : ℕ ≃ ι), StronglyMeasurable (hs.piecewise (s := s) f)
Tactic: obtain ⟨e, -⟩ := exists_true_iff_nonempty.mpr (nonempty_equiv_of_countable (α := ℕ) (β := ι))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → (i : ι) → Fin (n + 1) :=
  fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n
n : ℕ
b : Fin (n + 1)
⊢ ∃ (a : ι),
    (if hi : ∃ m < n, a = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ a = (e : (a : ℕ) → ι) m), ⋯⟩
      else Fin.last n) =
      b
have refine : (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
    ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), sorry⟩
  else Fin.last n) =
  b
Tactic: refine ⟨e b, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → (i : ι) → Fin (n + 1) :=
  fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n
n : ℕ
b : Fin (n + 1)
⊢ (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), ⋯⟩
    else Fin.last n) =
    b
have pos : ∀ (hb : (↑b : ℕ) < n),
  (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), sorry⟩
    else Fin.last n) =
    b
Tactic: by_cases hb : b < n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → (i : ι) → Fin (n + 1) :=
  fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n
n : ℕ
b : Fin (n + 1)
pos :
  ∀ (hb : (↑b : ℕ) < n),
    (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
        ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)),
          ⋯⟩
      else Fin.last n) =
      b
⊢ (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), ⋯⟩
    else Fin.last n) =
    b
have neg : ∀ (hb : ¬(↑b : ℕ) < n),
  (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), sorry⟩
    else Fin.last n) =
    b
Tactic: by_cases hb : b < n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → (i : ι) → Fin (n + 1) :=
  fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n
n : ℕ
b : Fin (n + 1)
hb : (↑b : ℕ) < n
⊢ (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), ⋯⟩
    else Fin.last n) =
    b
have this : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)
Tactic: have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Piecewise (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
inst_2 : TopologicalSpace β
hf : ∀ (i : ι), StronglyMeasurable (f i)
Fi : Infinite ι
e : ℕ ≃ ι
g : (n : ℕ) → (i : ι) → Fin (n + 1) :=
  fun (n : ℕ) (i : ι) ↦
    if hi : ∃ m < n, i = (e : (a : ℕ) → ι) m then ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m), ⋯⟩
    else Fin.last n
n : ℕ
b : Fin (n + 1)
hb : ¬(↑b : ℕ) < n
⊢ (if hi : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι) then
      ⟨hi.choose (p := fun (m : ℕ) ↦ m < n ∧ Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)), ⋯⟩
    else Fin.last n) =
    b
have neg : Fin.last n = b
Tactic: simp [hb]