awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
pos : ∀ (hy_mem : y ∈ s), s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x
neg : ∀ (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

Tactic:
by_cases hy_mem : y ∈ s
-- 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)
hy_mem : y ∈ s
⊢ s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x

Tactic:
simp [hy_mem]
-- 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)
hy_mem : y ∉ s
⊢ s.indicator (fun (x_1 : α) ↦ x) y = HSMul.hSMul (α := ℝ) (s.indicator (fun (x : α) ↦ 1) y) x

Tactic:
simp [hy_mem]
-- Module: Mathlib.MeasureTheory.Function.Piecewise
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
s : ι → Set α
f : ι → α → β
inst_1 : MeasurableSpace β
inst_2 : Countable ι
hs : IndexedPartition s
hm : ∀ (i : ι), MeasurableSet (s i)
hf : ∀ (i : ι), Measurable (f i)
t : Set β
ht : MeasurableSet t
⊢ MeasurableSet (hs.piecewise (s := s) f ⁻¹' t)

Tactic:
simpa [piecewise_preimage] using .iUnion (fun i => (hm i).inter ((hf i) ht))

Premises used: IndexedPartition.piecewise_preimage
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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) μ
choose :
  ∀ (p : (i : ι) → α → β) (hp : ∀ (i : ι), Measurable (p i)) (hq : ∀ (i : ι), f i =ᶠ[ae μ] p i),
    AEMeasurable (hs.piecewise (s := s) f) μ
⊢ AEMeasurable (hs.piecewise (s := s) f) μ

Tactic:
choose p hp hq using hf
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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) μ

Tactic:
⟨hs.piecewise p, hs.measurable_piecewise hm hp, ?_⟩

Premises used: AEMeasurable, IndexedPartition.measurable_piecewise, IndexedPartition.piecewise, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
refine : hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p
⊢ AEMeasurable (hs.piecewise (s := s) f) μ

Tactic:
refine ⟨hs.piecewise p, hs.measurable_piecewise hm hp, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
x : α
hx : ∀ (i : ι), f i x = p i x
⊢ hs.piecewise (s := s) f x = hs.piecewise (s := s) p x

Tactic:
hx (hs.index x)

Premises used: IndexedPartition.piecewise, IndexedPartition.index
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
h₁ h₂ : ∀ (x : α) (hx : ∀ (i : ι), f i x = p i x), hs.piecewise (s := s) f x = hs.piecewise (s := s) p x
⊢ hs.piecewise (s := s) f =ᶠ[ae μ] hs.piecewise (s := s) p

Tactic:
filter_upwards [ae_all_iff.2 hq] with x hx using hx (hs.index x)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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)
neg : ∀ (Fi : ¬Finite ι), StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
by_cases Fi : Finite ι

Premises used: Finite
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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)

Tactic:
⟨fun n => simpleFunc_piecewise hs hm (fun i => (hf i).approx n), fun x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, IndexedPartition.simpleFunc_piecewise, Exists.intro, MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 ι
pos :
  ∀ (x : α),
    Tendsto
      (fun (n : ℕ) ↦
        ((fun (n : ℕ) ↦ (hs.simpleFunc_piecewise (s := s) hm fun (i : ι) ↦ ⋯.approx n : SimpleFunc α β)) n :
            (a : α) → β)
          x)
      atTop (nhds (hs.piecewise (s := s) f x))
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
refine ⟨fun n => simpleFunc_piecewise hs hm (fun i => (hf i).approx n), fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 ι
x : α
⊢ Tendsto
    (fun (n : ℕ) ↦
      ((fun (n : ℕ) ↦ (hs.simpleFunc_piecewise (s := s) hm fun (i : ι) ↦ ⋯.approx n : SimpleFunc α β)) n : (a : α) → β)
        x)
    atTop (nhds (hs.piecewise (s := s) f x))

Tactic:
simp [simpleFunc_piecewise, piecewise_apply, StronglyMeasurable.tendsto_approx]

Premises used: IndexedPartition.simpleFunc_piecewise, MeasureTheory.StronglyMeasurable.tendsto_approx, IndexedPartition.piecewise_apply
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 ι
⊢ Infinite ι

Tactic:
simp only [not_finite_iff_infinite] at Fi

Premises used: not_finite_iff_infinite
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 ι
neg : ∀ (e : ℕ ≃ ι), StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
obtain ⟨e, -⟩ := exists_true_iff_nonempty.mpr (nonempty_equiv_of_countable (α := ℕ) (β := ι))

Premises used: Iff.mpr, exists_true_iff_nonempty, nonempty_equiv_of_countable
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 : ℕ ≃ ι
n : ℕ
i : ι
hi : ∃ m < n, i = (e : (a : ℕ) → ι) m
⊢ hi.choose (p := fun (m : ℕ) ↦ m < n ∧ i = (e : (a : ℕ) → ι) m) < n + 1

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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)
unfold :
  ∃ (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
⊢ ∃ (a : ι), g n a = b

Tactic:
unfold g
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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

Tactic:
⟨e b, ?_⟩

Premises used: Fin.val, Exists.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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)
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 : ι)), ⋯⟩
    else Fin.last n) =
    b
⊢ ∃ (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

Tactic:
refine ⟨e b, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
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 : ι)),
          ⋯⟩
      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

Tactic:
by_cases hb : b < n
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
⊢ ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)

Tactic:
have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
this : ∃ m < n, Eq (α := ι) ((e : (a : ℕ) → ι) (↑b : ℕ) : ι) ((e : (a : ℕ) → ι) m : ι)
⊢ (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

Tactic:
simpa only [this, Fin.ext_iff] using e.injective this.choose_spec.2.symm

Premises used: Exists.choose_spec, Fin.ext_iff, And.right, Equiv.injective, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
neg : 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

Tactic:
simp [hb]
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
⊢ Fin.last n = b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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 : ℕ), Function.Surjective (g n)

Tactic:
have sg (n : ℕ) : (g n).Surjective := by
    intro b
    unfold g
    refine ⟨e b, ?_⟩
    by_cases hb : b < n
    · have : ∃ m < n, e b = e m := ⟨b, ⟨hb, rfl⟩⟩
      simpa only [this, Fin.ext_iff] using e.injective this.choose_spec.2.symm
    · simp [hb]
      grind
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
sg : ∀ (n : ℕ), Function.Surjective (g n)
neg :
  ∀ (G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i),
    StronglyMeasurable (hs.piecewise (s := s) f)
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
have G (n : ℕ) := hs.coarserPartition (g n) (sg n)
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, IndexedPartition.simpleFunc_piecewise, Fin.val, Exists.intro, MeasureTheory.StronglyMeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
neg : ∀ (n : ℕ) (i : Fin (n + 1)), MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)
neg₁ :
  ∀ (x : α),
    Tendsto
      (fun (n : ℕ) ↦
        ((fun (n : ℕ) ↦
                ((G n).simpleFunc_piecewise (s := fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i) ⋯
                    fun (i : Fin (n + 1)) ↦ StronglyMeasurable.approx (f := f ((e : (a : ℕ) → ι) (↑i : ℕ))) ⋯ n :
                  SimpleFunc α β))
              n :
            (a : α) → β)
          x)
      atTop (nhds (hs.piecewise (s := s) f x))
⊢ StronglyMeasurable (hs.piecewise (s := s) f)

Tactic:
refine ⟨fun n => (G n).simpleFunc_piecewise (fun i => ?_) (fun i => (hf (e i)).approx n),
    fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
n : ℕ
i : Fin (n + 1)
⊢ MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)

Tactic:
.biUnion (to_countable _) fun _ _ ↦ hm _

Premises used: Set.to_countable, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Function.Piecewise
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
sg : ∀ (n : ℕ), Function.Surjective (g n)
G : (n : ℕ) → IndexedPartition (α := α) fun (k : Fin (n + 1)) ↦ ⋃ i ∈ g n ⁻¹' {k}, s i
n : ℕ
i : Fin (n + 1)
⊢ MeasurableSet.{u_2} (α := α) (⋃ i_1 ∈ g n ⁻¹' {i}, s i_1)

Tactic:
exact .biUnion (to_countable _) fun _ _ ↦ hm _