awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ (ENNReal.ofReal q).toReal) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal q ≠ 0

Tactic:
simp [hq]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ (ENNReal.ofReal q).toReal) μ
hp : 0 < p
hq : 0 < q
⊢ ENNReal.ofReal q ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
⊢ MemLp f (ENNReal.ofReal q) μ

Tactic:
rw [← ENNReal.toReal_ofReal hq.le, integrable_norm_rpow_iff hf (by simp [hq]) (by simp)] at hint

Premises used: MeasureTheory.integrable_norm_rpow_iff, LT.lt.le, ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
hint₁ : MemLp f (ENNReal.ofReal q) μ
⊢ 0 < p

Tactic:
rw [← ENNReal.toReal_ofReal hq.le, integrable_norm_rpow_iff hf (by simp [hq]) (by simp)] at hint

Premises used: MeasureTheory.integrable_norm_rpow_iff, LT.lt.le, ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
hp : 0 < p
hq : 0 < q
hint₁ : MemLp f (ENNReal.ofReal q) μ
hp₁ : 0 < p
⊢ 0 < q

Tactic:
rw [← ENNReal.toReal_ofReal hq.le, integrable_norm_rpow_iff hf (by simp [hq]) (by simp)] at hint

Premises used: MeasureTheory.integrable_norm_rpow_iff, LT.lt.le, ENNReal.toReal_ofReal
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : MemLp f (ENNReal.ofReal q) μ
hp : 0 < p
hq : 0 < q
⊢ MemLp f (ENNReal.ofReal p) μ

Tactic:
MemLp.mono_exponent hint (ENNReal.ofReal_le_ofReal hpq)

Premises used: ENNReal.ofReal_le_ofReal, MeasureTheory.MemLp.mono_exponent
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℝ
hp_1 : 0 ≤ p
hq_1 : 0 ≤ q
hpq : p ≤ q
hint : MemLp f (ENNReal.ofReal q) μ
hp : 0 < p
hq : 0 < q
⊢ MemLp f (ENNReal.ofReal p) μ

Tactic:
exact MemLp.mono_exponent hint (ENNReal.ofReal_le_ofReal hpq)

Premises used: ENNReal.ofReal_le_ofReal, MeasureTheory.MemLp.mono_exponent
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℕ
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ q) μ
simp_rw :
  ∀ (hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑q : ℝ)) μ),
    Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑p : ℝ)) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ ‖f x‖ ^ p) μ

Tactic:
simp_rw [← Real.rpow_natCast] at *

Premises used: Real.rpow_natCast
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℕ
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑q : ℝ)) μ
⊢ LE.le (α := ℝ) (↑p : ℝ) (↑q : ℝ)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
inst_1 : IsFiniteMeasure μ
f : α → β
hf : AEStronglyMeasurable f μ
p q : ℕ
hpq : p ≤ q
hint : Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑q : ℝ)) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ HPow.hPow (β := ℝ) ‖f x‖ (↑p : ℝ)) μ

Tactic:
exact integrable_norm_rpow_of_le hf p.cast_nonneg q.cast_nonneg (by simpa) hint

Premises used: Nat.cast_nonneg, MeasureTheory.integrable_norm_rpow_of_le
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : Integrable f ν
hμ : μ ≤ ν
⊢ Integrable f μ

Tactic:
⟨h.aestronglyMeasurable.mono_measure hμ, h.hasFiniteIntegral.mono_measure hμ⟩

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.HasFiniteIntegral.mono_measure, MeasureTheory.Integrable, MeasureTheory.AEStronglyMeasurable.mono_measure, And.intro, MeasureTheory.Integrable.hasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : Integrable f μ
rw : ∀ (hf : MemLp f 1 μ), MemLp f 1 μ'
⊢ Integrable f μ'

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f 1 μ
⊢ MemLp f 1 μ'

Tactic:
hf.of_measure_le_smul hc hμ'_le

Premises used: MeasureTheory.MemLp.of_measure_le_smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
μ' : Measure α
c : ℝ≥0∞
hc : c ≠ ∞
hμ'_le : μ' ≤ c • μ
f : α → ε
hf : MemLp f 1 μ
⊢ MemLp f 1 μ'

Tactic:
exact hf.of_measure_le_smul hc hμ'_le

Premises used: MeasureTheory.MemLp.of_measure_le_smul
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : Integrable f μ
hν : Integrable f ν
simp_rw : ∀ (hμ : MemLp f 1 μ) (hν : MemLp f 1 ν), MemLp f 1 (μ + ν)
⊢ Integrable f (μ + ν)

Tactic:
simp_rw [← memLp_one_iff_integrable] at hμ hν ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ MemLp f 1 (μ + ν)

Tactic:
⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.add_measure, MeasureTheory.MemLp, And.intro, MeasureTheory.MemLp.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
refine : eLpNorm f 1 (μ + ν) < ∞
⊢ MemLp f 1 (μ + ν)

Tactic:
refine ⟨hμ.aestronglyMeasurable.add_measure hν.aestronglyMeasurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
rw : eLpNorm f 1 μ < ∞ ∧ eLpNorm f 1 ν < ∞
⊢ eLpNorm f 1 (μ + ν) < ∞

Tactic:
rw [eLpNorm_one_add_measure, ENNReal.add_lt_top]

Premises used: ENNReal.add_lt_top, MeasureTheory.eLpNorm_one_add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 μ < ∞ ∧ eLpNorm f 1 ν < ∞

Tactic:
⟨hμ.eLpNorm_lt_top, hν.eLpNorm_lt_top⟩

Premises used: And.intro, MeasureTheory.MemLp.eLpNorm_lt_top
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
hμ : MemLp f 1 μ
hν : MemLp f 1 ν
⊢ eLpNorm f 1 μ < ∞ ∧ eLpNorm f 1 ν < ∞

Tactic:
exact ⟨hμ.eLpNorm_lt_top, hν.eLpNorm_lt_top⟩
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : Integrable f (μ + ν)
rw : ∀ (h : MemLp f 1 (μ + ν)), MemLp f 1 μ
⊢ Integrable f μ

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 μ

Tactic:
h.left_of_add_measure

Premises used: MeasureTheory.MemLp.left_of_add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 μ

Tactic:
exact h.left_of_add_measure

Premises used: MeasureTheory.MemLp.left_of_add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : Integrable f (μ + ν)
rw : ∀ (h : MemLp f 1 (μ + ν)), MemLp f 1 ν
⊢ Integrable f ν

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 ν

Tactic:
h.right_of_add_measure

Premises used: MeasureTheory.MemLp.right_of_add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
h : MemLp f 1 (μ + ν)
⊢ MemLp f 1 ν

Tactic:
exact h.right_of_add_measure

Premises used: MeasureTheory.MemLp.right_of_add_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ ν : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
f : α → ε
⊢ Integrable f (μ + ν) ↔ Integrable f μ ∧ Integrable f ν

Tactic:
⟨fun h => ⟨h.left_of_add_measure, h.right_of_add_measure⟩, fun h => h.1.add_measure h.2⟩

Premises used: MeasureTheory.Integrable.right_of_add_measure, MeasureTheory.Integrable.left_of_add_measure, MeasureTheory.Integrable.add_measure, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
left : AEStronglyMeasurable (m₀ := m) f 0
right : @HasFiniteIntegral _ _ _ m f 0
⊢ @Integrable _ _ _ _ m f 0

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
⊢ AEStronglyMeasurable (m₀ := m) f 0

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
f : α → ε
⊢ @HasFiniteIntegral _ _ _ m f 0

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : MeasurableSingletonClass α
a : α
f : α → ε
hfa : ‖f a‖ₑ < ∞
⊢ @HasFiniteIntegral _ _ _ m f (Measure.dirac a)

Tactic:
simpa [HasFiniteIntegral]

Premises used: MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
a : α
f : α → ε
hf : StronglyMeasurable f
hfa : ‖f a‖ₑ < ∞
⊢ @HasFiniteIntegral _ _ _ m f (Measure.dirac a)

Tactic:
simpa [HasFiniteIntegral, lintegral_dirac' _ hf.enorm]

Premises used: MeasureTheory.StronglyMeasurable.enorm, MeasureTheory.lintegral_dirac', MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
        (@Integrable _ _ _ _ m f (∑ i ∈ Insert.insert a s, μ i) ↔ ∀ i ∈ Insert.insert a s, Integrable f (μ i))
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Tactic:
induction s using Finset.induction_on
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
⊢ @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
h_1 : @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)
⊢ @Integrable _ _ _ _ m f (∑ i ∈ insert a s, μ i) ↔ ∀ i ∈ insert a s, Integrable f (μ i)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
inst_2 : PseudoMetrizableSpace ε
ι : Type u_8
m : MeasurableSpace α
f : α → ε
μ : ι → Measure α
s : Finset ι
empty : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
        (@Integrable _ _ _ _ m f (∑ i ∈ Insert.insert a s, μ i) ↔ ∀ i ∈ Insert.insert a s, Integrable f (μ i))
empty₁ : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
insert₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
        (@Integrable _ _ _ _ m f (∑ i ∈ Insert.insert a s, μ i) ↔ ∀ i ∈ Insert.insert a s, Integrable f (μ i))
empty₂ : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
insert₂ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
        (@Integrable _ _ _ _ m f (∑ i ∈ Insert.insert a s, μ i) ↔ ∀ i ∈ Insert.insert a s, Integrable f (μ i))
empty₃ : @Integrable _ _ _ _ m f (∑ i ∈ ∅, μ i) ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)
insert₃ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s →
      (@Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)) →
        (@Integrable _ _ _ _ m f (∑ i ∈ Insert.insert a s, μ i) ↔ ∀ i ∈ Insert.insert a s, Integrable f (μ i))
⊢ @Integrable _ _ _ _ m f (∑ i ∈ s, μ i) ↔ ∀ i ∈ s, Integrable f (μ i)

Tactic:
classical
  induction s using Finset.induction_on <;> simp [*]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0∞
hc : c ≠ ∞
rw : ∀ (h : MemLp f 1 μ) {c : ℝ≥0∞} (hc : c ≠ ∞), MemLp f 1 (c • μ)
⊢ Integrable f (c • μ)

Tactic:
rw [← memLp_one_iff_integrable] at h ⊢

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : MemLp f 1 μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ MemLp f 1 (c • μ)

Tactic:
h.smul_measure hc

Premises used: MeasureTheory.MemLp.smul_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : MemLp f 1 μ
c : ℝ≥0∞
hc : c ≠ ∞
⊢ MemLp f 1 (c • μ)

Tactic:
exact h.smul_measure hc

Premises used: MeasureTheory.MemLp.smul_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0
apply : (↑c : ℝ≥0∞) ≠ ∞
⊢ Integrable f (c • μ)

Tactic:
apply h.smul_measure

Premises used: MeasureTheory.Integrable.smul_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
c : ℝ≥0
⊢ (↑c : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
h : Integrable f (c • μ)
⊢ Integrable f μ

Tactic:
simpa only [smul_smul, ENNReal.inv_mul_cancel h₁ h₂, one_smul] using
      h.smul_measure (ENNReal.inv_ne_top.2 h₁)

Premises used: Iff.mpr, ENNReal.inv_ne_top, smul_smul, one_smul, MeasureTheory.Integrable.smul_measure, ENNReal.inv_mul_cancel
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simpa using h₂
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
c : ℝ≥0∞
h₁ : c ≠ 0
h₂ : c ≠ ∞
⊢ c⁻¹ ≠ ∞

Tactic:
simpa using h₁
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
inl :
  ∀ (h : @Integrable _ _ _ _ m f 0),
    Integrable f (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
inr : ∀ (hne : μ ≠ 0), Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
rcases eq_or_ne μ 0 with (rfl | hne)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h inl inl₁ inl₂ inl₃ : @Integrable _ _ _ _ m f 0
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)

Tactic:
rwa [smul_zero]

Premises used: smul_zero
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
inr : Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
apply h.smul_measure

Premises used: MeasureTheory.Integrable.smul_measure
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
f : α → ε
h : Integrable f μ
hne : μ ≠ 0
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : IsFiniteMeasure μ
f : α → ε
h : μ = 0
⊢ Integrable f (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ) ↔ Integrable f μ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
inst_2 : IsFiniteMeasure μ
f : α → ε
h : μ ≠ 0
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map f μ)
hf : AEMeasurable f μ
simp_rw : MemLp (m0 := inst_2) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ
⊢ @Integrable _ _ _ _ inst_2 g (Measure.map f μ) ↔ Integrable (g ∘ f) μ

Tactic:
simp_rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp (m0 := inst_2) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
memLp_map_measure_iff hg hf

Premises used: MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : AEStronglyMeasurable (m₀ := inst_2) g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ MemLp (m0 := inst_2) g 1 (Measure.map f μ) ↔ MemLp (g ∘ f) 1 μ

Tactic:
exact memLp_map_measure_iff hg hf

Premises used: MeasureTheory.memLp_map_measure_iff
-- Module: Mathlib.MeasureTheory.Function.L1Space.Integrable
Goal:
α : Type u_1
ε : Type u_5
m : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace ε
inst_1 : ContinuousENorm ε
α' : Type u_8
inst_2 : MeasurableSpace α'
f : α → α'
g : α' → ε
hg : @Integrable _ _ _ _ inst_2 g (Measure.map f μ)
hf : AEMeasurable f μ
⊢ Integrable (g ∘ f) μ

Tactic:
(integrable_map_measure hg.aestronglyMeasurable hf).mp hg

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, Iff.mp, MeasureTheory.integrable_map_measure