awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
s : Set α
hs : MeasurableSet s
hsf : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s₁ : C * μ.real s + C' * ν.real s ≤ max C C' * μ.real s + max C C' * ν.real s
⊢ ‖T s + T' s‖ ≤ max C C' * μ.real s + max C C' * ν.real s

Tactic:
calc
    ‖T s + T' s‖ ≤ ‖T s‖ + ‖T' s‖ := norm_add_le _ _
    _ ≤ C * μ.real s + C' * ν.real s := add_le_add (hT.2 s hs hμs) (hT'.2 s hs hνs)
    _ ≤ max C C' * μ.real s + max C C' * ν.real s := by
      gcongr
      · exact le_max_left C C'
      · exact le_max_right C C'

Premises used: add_le_add, MeasureTheory.Measure.real, norm_add_le, And.right, Max.max
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive ν T' C'
⊢ DominatedFinMeasAdditive (μ + ν) (T - T') (max C C')

Tactic:
sub_eq_add_neg T T' ▸ hT.add_measure μ ν hT'.neg

Premises used: MeasureTheory.DominatedFinMeasAdditive.neg, sub_eq_add_neg, Eq.rec, MeasureTheory.DominatedFinMeasAdditive.add_measure, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
x : MeasurableSpace α
μ ν : Measure α
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive (μ + ν) T C

Tactic:
of_measure_le (Measure.le_add_right le_rfl) hT hC

Premises used: le_rfl, MeasureTheory.DominatedFinMeasAdditive.of_measure_le, MeasureTheory.Measure.le_add_right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
x : MeasurableSpace α
μ ν : Measure α
hT : DominatedFinMeasAdditive ν T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive (μ + ν) T C

Tactic:
of_measure_le (Measure.le_add_left le_rfl) hT hC

Premises used: le_rfl, MeasureTheory.DominatedFinMeasAdditive.of_measure_le, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst : SeminormedAddCommGroup β
ι : Type u_8
s : Finset ι
μ : ι → Measure α
T : ι → Set α → β
C : ι → ℝ
hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
⊢ @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) (sup' {i} ⋯ C)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst : SeminormedAddCommGroup β
ι : Type u_8
s_1 : Finset ι
μ : ι → Measure α
T : ι → Set α → β
C : ι → ℝ
hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
i : ι
s : Finset ι
his : i ∉ s
hs' : s.Nonempty
ih : @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs' C)
⊢ @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ cons i s his, μ i) (∑ i ∈ cons i s his, T i)
    ((cons i s his).sup' ⋯ C)

Tactic:
simpa [his, Finset.sup'_cons hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih

Premises used: MeasureTheory.DominatedFinMeasAdditive.add_measure, Finset.sup'_cons, Finset.sum
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
β : Type u_7
inst : SeminormedAddCommGroup β
ι : Type u_8
s : Finset ι
hs : s.Nonempty
μ : ι → Measure α
T : ι → Set α → β
C : ι → ℝ
hT : ∀ (i : ι), DominatedFinMeasAdditive (μ i) (T i) (C i)
singleton : ∀ (i : ι), @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) (sup' {i} ⋯ C)
cons :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s) (hs' : s.Nonempty)
    (ih : @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs' C)),
    @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ Finset.cons i s his, μ i) (∑ i ∈ Finset.cons i s his, T i)
      ((Finset.cons i s his).sup' ⋯ C)
⊢ @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C)

Tactic:
induction hs using Finset.Nonempty.cons_induction with
  | singleton i => simp_all
  | @cons i s his hs' ih =>
    simpa [his, Finset.sup'_cons hs' C] using (hT i).add_measure (μ i) (∑ j ∈ s, μ j) ih

Premises used: Finset.cons, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
_ :
  MeasurableSet s →
    HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ MeasurableSet s →
    HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
h : MeasurableSet s
hcμs : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞
⊢ ¬c = 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [hc_ne_top, smul_eq_mul, ENNReal.mul_eq_top, or_false, Ne,
      false_and] at hcμs

Premises used: false_and, Ne, ENNReal.mul_eq_top, or_false, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
h : MeasurableSet s
hcμs : ¬c = 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
hcμs.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
s : Set α
h : MeasurableSet s
hcμs : ¬c = 0 ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact hcμs.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
⊢ ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have h : ∀ s, MeasurableSet s → c • μ s = ∞ → μ s = ∞ := by
    intro s _ hcμs
    simp only [hc_ne_top, smul_eq_mul, ENNReal.mul_eq_top, or_false, Ne,
      false_and] at hcμs
    exact hcμs.2
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ DominatedFinMeasAdditive μ T (c.toReal * C)

Tactic:
⟨hT.1.of_eq_top_imp_eq_top (μ := c • μ) h, fun s hs hμs => ?_⟩

Premises used: MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top, And.left, MeasureTheory.DominatedFinMeasAdditive, And.intro
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ‖T s‖ ≤ c.toReal * C * μ.real s
⊢ DominatedFinMeasAdditive μ T (c.toReal * C)

Tactic:
refine ⟨hT.1.of_eq_top_imp_eq_top (μ := c • μ) h, fun s hs hμs => ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞

Tactic:
have hcμs : c • μ s ≠ ∞ := mt (h s hs) hμs.ne
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hcμs : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞

Tactic:
rw [smul_eq_mul] at hcμs

Premises used: smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hcμs : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
⊢ ‖T s‖ ≤ c.toReal * C * μ.real s

Tactic:
(hT.2 s hs hcμs.lt_top).trans (le_of_eq ?_)

Premises used: And.right, Ne.lt_top, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hcμs : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
refine : C * (c • μ).real s = c.toReal * C * μ.real s
⊢ ‖T s‖ ≤ c.toReal * C * μ.real s

Tactic:
refine (hT.2 s hs hcμs.lt_top).trans (le_of_eq ?_)

Premises used: And.right, Ne.lt_top, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hcμs : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
simp : C * (c.toReal * μ.real s) = c.toReal * C * μ.real s
⊢ C * (c • μ).real s = c.toReal * C * μ.real s

Tactic:
simp only [measureReal_ennreal_smul_apply]

Premises used: MeasureTheory.measureReal_ennreal_smul_apply
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
c : ℝ≥0∞
hc_ne_top : c ≠ ∞
hT : DominatedFinMeasAdditive (c • μ) T C
h :
  ∀ (s : Set α),
    MeasurableSet s →
      HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = ∞ →
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hcμs : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
⊢ C * (c.toReal * μ.real s) = c.toReal * C * μ.real s

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
h : μ ≤ c • μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ' T (c.toReal * C)

Tactic:
(hT.of_measure_le h hC).of_smul_measure hc

Premises used: MeasureTheory.DominatedFinMeasAdditive.of_smul_measure, MeasureTheory.DominatedFinMeasAdditive.of_measure_le
-- 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'
m : MeasurableSpace α
f : α →ₛ F
⊢ Eq.{u_4 + 1} (α := F') (setToSimpleFunc 0 f) 0

Tactic:
simp [setToSimpleFunc]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc
-- 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'
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
⊢ Eq.{u_4 + 1} (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x) 0

Tactic:
sum_eq_zero fun x _ => ?_

Premises used: Finset.sum_eq_zero
-- 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'
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
refine :
  ∀ x ∈ f.range,
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
⊢ Eq.{u_4 + 1} (α := F') (∑ x ∈ f.range, (T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x) 0

Tactic:
refine sum_eq_zero fun x _ => ?_

Premises used: Finset.sum_eq_zero
-- 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'
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h : x ∈ f.range
pos :
  ∀ (hx0 : x = 0),
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
neg :
  ∀ (hx0 : ¬x = 0),
    Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')

Tactic:
by_cases hx0 : x = 0
-- 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'
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h : x ∈ f.range
hx0 : x = 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')

Tactic:
simp [hx0]
-- 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'
h_zero : ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → T s = 0
f : α →ₛ E
hf : Integrable.{u_2, u_1} (ε := E) (⇑f : (a : α) → E) μ
x : E
h : x ∈ f.range
hx0 : ¬x = 0
neg : Eq.{u_4 + 1} (α := F') ((0 : (a : E) → F') x : F') (0 : F')
neg₁ neg₂ : Eq.{u_4 + 1} (α := F') 0 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')

Tactic:
rw [h_zero (f ⁻¹' ({x} : Set E)) (measurableSet_fiber _ _)
      (measure_preimage_lt_top_of_integrable f hf hx0),
    ContinuousLinearMap.zero_apply]

Premises used: MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_integrable, Set.preimage, MeasureTheory.SimpleFunc.measurableSet_fiber, Singleton.singleton, DFunLike.coe, 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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
inl : IsEmpty α → @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
inr : Nonempty α → @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0

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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
h : IsEmpty α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0

Tactic:
simp [setToSimpleFunc]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc
-- 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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
h : Nonempty α
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0

Tactic:
simp [setToSimpleFunc]

Premises used: MeasureTheory.SimpleFunc.setToSimpleFunc
-- 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 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
symm :
  ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x = setToSimpleFunc T f
⊢ setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x

Tactic:
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'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x = setToSimpleFunc T f

Tactic:
sum_filter_of_ne fun x _ => mt fun hx0 => ?_

Premises used: mt, MeasureTheory.SimpleFunc.setToSimpleFunc, Finset.sum_filter_of_ne
-- 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 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
refine :
  ∀ x ∈ f.range,
    ∀ (hx0 : x = 0),
      Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') (0 : F')
⊢ ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x = setToSimpleFunc T f

Tactic:
refine sum_filter_of_ne fun x _ => mt fun hx0 => ?_

Premises used: mt, Finset.sum_filter_of_ne
-- 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 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
h : x ∈ f.range
hx0 : x = 0
rw : Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {0}) : (a : F) → F') 0 : F') (0 : F')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x : F') (0 : F')

Tactic:
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'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
h : x ∈ f.range
hx0 : x = 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {0}) : (a : F) → F') 0 : F') (0 : F')

Tactic:
map_zero _

Premises used: map_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'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
x : F
h : x ∈ f.range
hx0 : x = 0
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := F) (⇑f : (a : α) → F) {0}) : (a : F) → F') 0 : F') (0 : F')

Tactic:
exact map_zero _

Premises used: map_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable.{u_5, u_1} (ε := G) (⇑f : (a : α) → G) μ
g : G → F
hg : g 0 = 0
⊢ T ∅ = 0

Tactic:
have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive
Goal:
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedAddCommGroup F'
inst_3 : NormedSpace ℝ F'
inst_4 : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable.{u_5, u_1} (ε := G) (⇑f : (a : α) → G) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
⊢ ∀ x ∈ f.range,
    x ≠ 0 → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Set.preimage (β := G) (⇑f : (a : α) → G) {x}) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne