awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
hb_1 : b ∈ f.range
hb : b ≠ 0
inr : ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ ≤ C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b})
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ * ‖b‖ ≤
    C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b}) * ‖b‖

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
hb_1 : b ∈ f.range
hb : b ≠ 0
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ ≤ C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b})

Tactic:
hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
        SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
b : E
hb_1 : b ∈ f.range
hb : b ≠ 0
⊢ ‖T (Set.preimage (β := E) (⇑f : (a : α) → E) {b})‖ ≤ C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {b})

Tactic:
exact hT_norm _ (SimpleFunc.measurableSet_fiber _ _) <|
        SimpleFunc.measure_preimage_lt_top_of_integrable _ hf hb

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, MeasureTheory.SimpleFunc.measurableSet_fiber
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
simp_rw :
  LE.le (α := ℝ) (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)
⊢ ∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖ ≤
    C * ∑ x ∈ f.range, μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖

Tactic:
simp_rw [mul_sum, ← mul_assoc]

Premises used: Finset.mul_sum, mul_assoc
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
E : Type u_2
F' : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F'
C : ℝ
hT_norm :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ‖T s‖ ≤ C * μ.real s
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ LE.le (α := ℝ) (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)
    (∑ x ∈ f.range, C * μ.real (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) * ‖x‖)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : ∀ (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

Tactic:
obtain rfl | hs_empty := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 α
x : F
hs : MeasurableSet.{u_1} (α := α) ∅
⊢ setToSimpleFunc T (piecewise ∅ hs (const α x) (const α 0)) = (T ∅ : (a : F) → F') x

Tactic:
simp only [hT_empty, ContinuousLinearMap.zero_apply, piecewise_empty, const_zero,
      setToSimpleFunc_zero_apply]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_zero_apply, MeasureTheory.SimpleFunc.piecewise_empty, MeasureTheory.SimpleFunc.const_zero, ContinuousLinearMap.zero_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
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₁ :
  ∀ (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')
⊢ 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:
obtain rfl | hs_univ := eq_or_ne s univ

Premises used: Set.univ, eq_or_ne, rfl
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 α
x : F
hs : MeasurableSet.{u_1} (α := α) Set.univ
hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ
⊢ Nonempty α

Tactic:
haveI hα := hs_empty.to_type
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 α
x : F
hs : MeasurableSet.{u_1} (α := α) Set.univ
hs_empty : Set.Nonempty.{u_1} (α := α) Set.univ
hα : Nonempty α
⊢ 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:
simp [← Function.const_def]

Premises used: Function.const_def
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
inr :
  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 ∈ (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:
rw [range_indicator hs hs_empty hs_univ]

Premises used: MeasureTheory.SimpleFunc.range_indicator
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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')
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')
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
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')
⊢ 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:
simp_rw [hx0]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∈ {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
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
neg₁ : 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:
rw [sum_insert]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 neg : ¬x = 0
⊢ x ∉ {0}

Tactic:
rw [Finset.mem_singleton]

Premises used: Finset.mem_singleton
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ ¬x = 0

Tactic:
hx0
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ ¬x = 0

Tactic:
exact hx0
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 :
  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')
⊢ 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_singleton, (T _).map_zero, add_zero]

Premises used: ContinuousLinearMap.map_zero, Finset.sum_singleton, add_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x} = s
⊢ 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:
congr
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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.indicator (Function.const α x) ⁻¹' {x} = s
⊢ Set.preimage (β := F) (⇑(piecewise s hs (const α x) (const α 0)) : (a : α) → F) {x} = s

Tactic:
simp only [coe_piecewise, piecewise_eq_indicator, coe_const, Function.const_zero,
    piecewise_eq_indicator]

Premises used: MeasureTheory.SimpleFunc.coe_piecewise, Function.const_zero, Set.piecewise_eq_indicator, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
neg₁ : Membership.mem (γ := Set F) {x} x
⊢ s.indicator (Function.const α x) ⁻¹' {x} = s

Tactic:
rw [indicator_preimage, ← Function.const_def, preimage_const_of_mem]

Premises used: Function.const_def, Set.indicator_preimage, Set.preimage_const_of_mem
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ Membership.mem (γ := Set F) {x} x

Tactic:
Set.mem_singleton x

Premises used: Set.mem_singleton
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ Membership.mem (γ := Set F) {x} x

Tactic:
exact Set.mem_singleton x

Premises used: Set.mem_singleton
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
neg₁ : 0 ∉ {x}
⊢ s.ite Set.univ (Set.preimage (β := F) 0 {x}) = s

Tactic:
rw [← Function.const_zero, ← Function.const_def, preimage_const_of_notMem]

Premises used: Set.preimage_const_of_notMem, Function.const_def, Function.const_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ ¬0 = x

Tactic:
Ne.symm hx0

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
⊢ ¬0 = x

Tactic:
exact Ne.symm hx0

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∅ = s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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'
inst_4 : Nonempty α
T : Set α → F →L[ℝ] F'
x : F
m : MeasurableSpace α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x

Tactic:
simp only [setToSimpleFunc, range_const, Set.mem_singleton, preimage_const_of_mem,
    sum_singleton, ← Function.const_def, coe_const]

Premises used: Set.mem_singleton, Finset.sum_singleton, Function.const_def, MeasureTheory.SimpleFunc.setToSimpleFunc, MeasureTheory.SimpleFunc.range_const, Set.preimage_const_of_mem, MeasureTheory.SimpleFunc.coe_const
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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
inr : Nonempty α → @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 α
⊢ Eq.{u_1 + 1} (α := Set α) Set.univ ∅

Tactic:
have h_univ_empty : (univ : Set α) = ∅ := Subsingleton.elim _ _
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 ∅
inl : @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (0 : (a : F) → F') x
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x

Tactic:
rw [h_univ_empty, hT_empty]
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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) = (0 : (a : F) → F') x

Tactic:
simp only [setToSimpleFunc, ContinuousLinearMap.zero_apply, sum_empty,
      range_eq_empty_of_isEmpty]

Premises used: MeasureTheory.SimpleFunc.range_eq_empty_of_isEmpty, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum_empty, ContinuousLinearMap.zero_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : Nonempty α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x

Tactic:
setToSimpleFunc_const' T x

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_const'
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
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 : Nonempty α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T (const α x) = (T Set.univ : (a : F) → F') x

Tactic:
exact setToSimpleFunc_const' T x

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc_const'