awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_8
inst : NormedAddCommGroup β
T : Set α → β
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : C * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) = 0
rw₁ : C * ENNReal.toReal 0 = 0
rw₂ : C * 0 = 0
⊢ C * μ.real s = 0
have rw₃ : Eq (α := ℝ) 0 0
Tactic: rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
⊢ DominatedFinMeasAdditive μ (T + T') (C + C')
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖(T + T') s‖ ≤ (C + C') * μ.real s
Tactic: refine ⟨hT.1.add hT'.1, fun s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T T' : Set α → β
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖(T + T') s‖ ≤ (C + C') * μ.real s
have rw : ‖T s + T' s‖ ≤ C * μ.real s + C' * μ.real s
Tactic: rw [Pi.add_apply, add_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst_1 : SeminormedAddGroup 𝕜
inst_2 : DistribSMul 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
⊢ DominatedFinMeasAdditive.{u_1, u_7} (β := β) μ (fun (s : Set α) ↦ c • T s) (‖c‖ * C)
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖c‖ * ‖T s‖ ≤ ‖c‖ * C * μ.real s
Tactic: refine ⟨hT.1.smul c, fun s hs hμs => (norm_smul_le _ _).trans ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
𝕜 : Type u_6
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
inst_1 : SeminormedAddGroup 𝕜
inst_2 : DistribSMul 𝕜 β
inst_3 : IsBoundedSMul 𝕜 β
hT : DominatedFinMeasAdditive μ T C
c : 𝕜
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖c‖ * ‖T s‖ ≤ ‖c‖ * C * μ.real s
have rw : ‖c‖ * ‖T s‖ ≤ ‖c‖ * (C * μ.real s)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
⊢ DominatedFinMeasAdditive μ' T C
have h' : ∀ (s : Set α),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h' : ∀ s, μ s = ∞ → μ' s = ∞ := fun s hs ↦ top_unique <| hs.symm.trans_le (h _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ DominatedFinMeasAdditive μ' T C
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμ's : LT.lt (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖T s‖ ≤ C * μ'.real s
Tactic: refine ⟨hT.1.of_eq_top_imp_eq_top fun s _ ↦ h' s, fun s hs hμ's ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥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∞)
⊢ ‖T s‖ ≤ C * μ'.real s
have hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμs : μ s < ∞ := (h s).trans_lt hμ's
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥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∞)
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ C * ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ C * ENNReal.toReal ((μ' : (a : Set α) → ℝ≥0∞) s)
have hbc : Ne (α := ℝ≥0∞) ((μ' : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : SeminormedAddCommGroup β
T : Set α → β
C : ℝ
μ' : Measure α
h : μ ≤ μ'
hT : DominatedFinMeasAdditive μ T C
hC : 0 ≤ C
h' :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥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∞)
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖T s‖ ≤ C * μ'.real s
have C₁ : C * μ.real s ≤ C * μ'.real s
Tactic: calc
    ‖T s‖ ≤ C * μ.real s := hT.2 s hs hμs
    _ ≤ C * μ'.real s := by
      simp only [measureReal_def]
      gcongr
      exact hμ's.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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')
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hsf : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖(T + T') s‖ ≤ max C C' * (μ + ν).real s
Tactic: refine ⟨hT.1.add_measure hT'.1, fun s hs hsf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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∞)
⊢ ‖(T + T') s‖ ≤ max C C' * (μ + ν).real s
have hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hμs : μ s < ∞ := (Measure.le_add_right le_rfl s).trans_lt hsf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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∞)
⊢ ‖(T + T') s‖ ≤ max C C' * (μ + ν).real s
have hνs : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hνs : ν s < ∞ := (Measure.le_add_left le_rfl s).trans_lt hsf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
⊢ ‖(T + T') s‖ ≤ max C C' * (μ + ν).real s
have rw : ‖T s + T' s‖ ≤ max C C' * μ.real s + max C C' * ν.real s
Tactic: rw [Pi.add_apply, measureReal_add_apply hμs.ne hνs.ne, mul_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
⊢ C * μ.real s + C' * ν.real s ≤ max C C' * μ.real s + max C C' * ν.real s
have h₁ : C ≤ max C C'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
h₁ : C ≤ max C C'
⊢ C * μ.real s + C' * ν.real s ≤ max C C' * μ.real s + max C C' * ν.real s
have h₂ : C' ≤ max C C'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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∞)
⊢ ‖T s + T' s‖ ≤ max C C' * μ.real s + max C C' * ν.real s
have s₁ : C * μ.real s + C' * ν.real 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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)
⊢ @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C)
have singleton : ∀ (i : ι), @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ {i}, μ i) (∑ i ∈ {i}, T i) (sup' {i} sorry 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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)
⊢ @DominatedFinMeasAdditive.{u_1, u_7} α β _ m (∑ i ∈ s, μ i) (∑ i ∈ s, T i) (s.sup' hs C)
have 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 ∈ cons i s his, μ i) (∑ i ∈ cons i s his, T i)
    ((cons i s his).sup' sorry 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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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∞) = ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have hcμs₁ : ¬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
Cleared hypotheses: hcμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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
⊢ DominatedFinMeasAdditive μ T (c.toReal * C)
have h : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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)
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  ‖T s‖ ≤ c.toReal * C * μ.real s
Tactic: refine ⟨hT.1.of_eq_top_imp_eq_top (μ := c • μ) h, fun s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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∞)
⊢ ‖T s‖ ≤ c.toReal * C * μ.real s
have hcμs : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
Tactic: have hcμs : c • μ s ≠ ∞ := mt (h s hs) hμs.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (hypothesis)
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∞) ≠ ∞
⊢ ‖T s‖ ≤ c.toReal * C * μ.real s
have hcμs₁ : HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ≠ ∞
Tactic: rw [smul_eq_mul] at hcμs
Cleared hypotheses: hcμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
have refine : C * (c • μ).real s = c.toReal * C * μ.real s
Tactic: refine (hT.2 s hs hcμs.lt_top).trans (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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 • μ).real s = c.toReal * C * μ.real s
have simp : C * (c.toReal * μ.real s) = c.toReal * C * μ.real s
Tactic: simp only [measureReal_ennreal_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
have refine : ∀ x ∈ f.range,
  Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
Tactic: refine sum_eq_zero fun x _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
have pos : ∀ (hx0 : x = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
have neg : ∀ (hx0 : ¬x = 0),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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')
have neg : Eq.{u_4 + 1} (α := F') ((0 : (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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
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')
⊢ Eq.{u_4 + 1} (α := F') ((T (Set.preimage (β := E) (⇑f : (a : α) → E) {x}) : (a : E) → F') x : F') (0 : F')
have neg₁ : Eq.{u_4 + 1} (α := F') 0 0
Tactic: rw [h_zero (f ⁻¹' ({x} : Set E)) (measurableSet_fiber _ _)
      (measure_preimage_lt_top_of_integrable f hf hx0),
    ContinuousLinearMap.zero_apply]
-- 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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
have inl : IsEmpty α → @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
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'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
inl : IsEmpty α → @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
⊢ @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
have inr : Nonempty α → @setToSimpleFunc _ _ _ _ _ _ _ m T 0 = 0
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'
inst_4 : DecidablePred fun (x : F) ↦ x ≠ 0
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc T f = ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x
have symm : ∑ x ∈ f.range with x ≠ 0, (T (Set.preimage (β := F) (⇑f : (a : α) → F) {x}) : (a : F) → F') x = setToSimpleFunc T f
Tactic: symm