awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ {x, 0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have neg : ∀ (hx0 : ¬x = 0),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : x = 0
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have pos : Eq.{u_4 + 1} (α := F')
  (∑ x ∈ {0, 0},
      (T (Set.preimage (β := F) (⇑(piecewise s hs (const α 0) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x :
    F')
  ((T s : (a : F) → F') 0 : F')
Tactic: simp_rw [hx0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have neg : HAdd.hAdd (α := F') (β := F')
    ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
    (∑ x_1 ∈ {0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F') =
  (T s : (a : F) → F') x
Tactic: rw [sum_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
neg :
  HAdd.hAdd (α := F') (β := F')
      ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
      (∑ x_1 ∈ {0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F') =
    (T s : (a : F) → F') x
⊢ Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
have neg₁ : x ∉ {0}
Tactic: rw [sum_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ HAdd.hAdd (α := F') (β := F')
      ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
      (∑ x_1 ∈ {0},
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F') =
    (T s : (a : F) → F') x
have neg : Eq.{u_4 + 1} (α := F')
  ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
  ((T s : (a : F) → F') x : F')
Tactic: rw [sum_singleton, (T _).map_zero, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Eq.{u_4 + 1} (α := F')
    ((T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x}) : (a : F) → F') x : F')
    ((T s : (a : F) → F') x : F')
have neg : Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x} = s
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x} = s
have neg : s.indicator (Function.const α x) ⁻¹' {x} = s
Tactic: simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s
have neg : s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
Tactic: rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
neg : s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s
have neg₁ : Membership.mem (γ := Set F) {x} x
Tactic: rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
⊢ s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
have neg : s.ite Set.univ ∅ = s
Tactic: rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
hs_empty : s.Nonempty
hs_univ : s ≠ Set.univ
hx0 : ¬x = 0
neg : s.ite Set.univ ∅ = s
⊢ s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s
have neg₁ : 0 ∉ {x}
Tactic: rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inl : ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
  setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr : ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
inr inr₁ :
  ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr₂ : ∀ (hs_empty : s.Nonempty),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
inr inr₁ :
  ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
inr₂ :
  ∀ (hs_empty : s.Nonempty),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr₃ : ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
            (a : F) → F')
          x_1 :
      F')
    ((T Set.univ : (a : F) → F') x : F')
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
inr inr₁ :
  ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
inr₂ :
  ∀ (hs_empty : s.Nonempty),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
inr₃ :
  ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
              (a : F) → F')
            x_1 :
        F')
      ((T Set.univ : (a : F) → F') x : F')
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr₄ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
m : MeasurableSpace α
s : Set α
hs : MeasurableSet s
x : F
inl :
  ∀ (hs : MeasurableSet.{u_1} (α := α) ∅),
    setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x
inr inr₁ :
  ∀ (hs_empty : s.Nonempty), setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
inr₂ :
  ∀ (hs_empty : s.Nonempty),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
inr₃ :
  ∀ (hs : MeasurableSet.{u_1} (α := α) Set.univ) (hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise Set.univ hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise Set.univ hs (const α x) (const α 0)) : (a : α) → F) {x_1}) :
              (a : F) → F')
            x_1 :
        F')
      ((T Set.univ : (a : F) → F') x : F')
inr₄ inr₅ :
  ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ),
    Eq.{u_4 + 1} (α := F')
      (∑ x_1 ∈ (piecewise s hs (const α x) (const α 0)).range,
          (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F')
            x_1 :
        F')
      ((T s : (a : F) → F') x : F')
⊢ setToSimpleFunc T (piecewise s hs (const α x) (const α 0)) = (T s : (a : F) → F') x
have inr₆ : ∀ (hs_empty : s.Nonempty) (hs_univ : s ≠ Set.univ),
  Eq.{u_4 + 1} (α := F')
    (∑ x_1 ∈ {x, 0},
        (T (Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x_1}) : (a : F) → F') x_1 :
      F')
    ((T s : (a : F) → F') x : F')
Tactic: classical
  obtain rfl | hs_empty := s.eq_empty_or_nonempty
  · simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]
  simp_rw [setToSimpleFunc]
  obtain rfl | hs_univ := eq_or_ne s univ
  · haveI hα := hs_empty.to_type
    simp [← Function.const_def]
  rw [range_indicator hs hs_empty hs_univ]
  by_cases hx0 : x = 0
  · simp_rw [hx0]; simp
  rw [sum_insert]
  swap; · rw [Finset.mem_singleton]; exact hx0
  rw [sum_singleton, (T _).map_zero, add_zero]
  congr
  simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]
  rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]
  swap; · exact Set.mem_singleton x
  rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]
  swap; · rw [Set.mem_singleton_iff]; exact Ne.symm hx0
  simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
have inl : IsEmpty α → @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
inl : IsEmpty α → @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
have inr : Nonempty α → @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h : IsEmpty α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
have h_univ_empty : Eq.{u_1 + 1} (α := Set α) Set.univ ∅
Tactic: have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h : IsEmpty α
h_univ_empty : Eq.{u_1 + 1} (α := Set α) Set.univ ∅
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
have inl : @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (0 : (a : F) → F') x
Tactic: rw [h_univ_empty, hT_empty]