mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.Multilinear.Basic

Goal state before:
pp: 𝕜 : Type u
ι : Type v
ι' : Type v'
E : ι → Type wE
E₁ : ι → Type wE₁
E' : ι' → Type wE'
G : Type wG
G' : Type wG'
inst✝¹¹ : Fintype ι'
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
inst✝³ : SeminormedAddCommGroup G'
inst✝² : NormedSpace 𝕜 G'
inst✝¹ : Fintype ι
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
inst✝ : DecidableEq ι
m : (i : ι) → E i
i : ι
c : 𝕜
x : E i
x✝ : G
⊢ ({ toFun := fun x_1 ↦ (f x_1) (update m i (c • x)), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
        (‖f‖ * ∏ i_1, ‖update m i (c • x) i_1‖) ⋯)
      x✝ =
    (c •
        { toFun := fun x_1 ↦ (f x_1) (update m i x), map_add' := ⋯, map_smul' := ⋯ }.mkContinuous
          (‖f‖ * ∏ i_1, ‖update m i x i_1‖) ⋯)
      x✝

Tactic:
simp only [FunLike.coe_smul, ContinuousMultilinearMap.map_update_smul, LinearMap.coe_mk,
          LinearMap.mkContinuous_apply, Pi.smul_apply, AddHom.coe_mk]

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : PseudoMetrizableSpace ε
⊢ Integrable f μ ↔ IntegrableAtFilter f (cocompact X) μ ∧ LocallyIntegrable f μ

Tactic:
refine ⟨fun hf ↦ ⟨hf.integrableAtFilter _, hf.locallyIntegrable⟩, fun ⟨⟨s, hsc, hs⟩, hloc⟩ ↦ ?_⟩
  obtain ⟨t, htc, ht⟩ := mem_cocompact'.mp hsc
  rewrite [← integrableOn_univ, ← compl_union_self s, integrableOn_union]
  exact ⟨(hloc.integrableOn_isCompact htc).mono ht le_rfl, hs⟩

Goal state after:
Module: Mathlib.MeasureTheory.Function.LocallyIntegrable

Goal state before:
pp: X : Type u_1
E : Type u_6
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
μ : Measure X
s : Set X
inst✝ : OpensMeasurableSpace X
K : Set X
f : X → E
hf : ContinuousOn f K
hK : IsCompact K
hs : MeasurableSet s
h's : s ⊆ K
mus : μ s ≠ ∞
⊢ IntegrableOn f s μ

Tactic:
by
  refine ⟨hf.aestronglyMeasurable_of_subset_isCompact hK hs h's, ?_⟩
  have : Fact (μ s < ∞) := ⟨mus.lt_top⟩
  obtain ⟨C, hC⟩ : ∃ C, ∀ x ∈ f '' K, ‖x‖ ≤ C :=
    IsBounded.exists_norm_le (hK.image_of_continuousOn hf).isBounded
  apply HasFiniteIntegral.of_bounded (C := C)
  filter_upwards [ae_restrict_mem hs] with a ha using hC _ (mem_image_of_mem f (h's ha))

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
⊢ MemLp (fun x ↦ ‖f x - y₀‖) p μ

Tactic:
have h_meas : Measurable fun x => ‖f x - y₀‖ := by
      simp only [← dist_eq_norm]
      fun_prop

Goal state after:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
p : ℝ≥0∞
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f p μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x ↦ y₀) p μ
n : ℕ
h_meas : Measurable fun x ↦ ‖f x - y₀‖
⊢ MemLp (fun x ↦ ‖f x - y₀‖) p μ
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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 : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ ‖T s + T' s‖ ≤ max C C' * (μ.real s + ν.real s)

Tactic:
mul_add

Goal state after:
α : 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 : (μ + ν) s < ∞
hμs : μ s < ∞
hνs : ν s < ∞
⊢ ‖T s + T' s‖ ≤ max C C' * μ.real s + max C C' * ν.real s
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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 → c • μ s = ∞ → μ s = ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hcμs : c * μ s ≠ ∞
⊢ C * (c • μ).real s = c.toReal * C * μ.real s

Tactic:
simp only [measureReal_ennreal_smul_apply]

Goal state after:
α : 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 → c • μ s = ∞ → μ s = ∞
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hcμs : c * μ s ≠ ∞
⊢ C * (c.toReal * μ.real s) = c.toReal * C * μ.real s
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (μ + ν).real s • x = μ.real s • x + ν.real s • x

Tactic:
measureReal_add_apply,

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hμs : μ s ≠ ∞
hνs : ν s ≠ ∞
x : F
⊢ (μ.real s + ν.real s) • x = μ.real s • x + ν.real s • x
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PartialOrder F
inst✝ : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ (weightedSMul μ s) x

Tactic:
simp only [weightedSMul, _root_.id, coe_id', smul_apply]

Goal state after:
α : Type u_1
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝¹ : PartialOrder F
inst✝ : IsOrderedModule ℝ F
s : Set α
x : F
hx : 0 ≤ x
⊢ 0 ≤ μ.real s • x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range with x ≠ 0, (T'' (⇑f ⁻¹' {x})) x =
    ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T' f = c • setToSimpleFunc T f

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]

Goal state after:
α : Type u_1
E : Type u_2
F' : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range with x ≠ 0, (T' (⇑f ⁻¹' {x})) x = c • ∑ x ∈ f.range with x ≠ 0, (T (⇑f ⁻¹' {x})) x
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a b : α → 𝕜
u v : α → E
l : Filter α
hab : a ~[l] b
huv : u ~[l] v
⊢ (fun x ↦ a x • u x) ~[l] fun x ↦ b x • v x

Tactic:
by
  rcases hab.exists_eq_mul with ⟨φ, hφ, habφ⟩
  have : ((fun x ↦ a x • u x) - (fun x ↦ b x • v x)) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x) := by
    convert!
      (habφ.comp₂ (· • ·) <| EventuallyEq.refl _ u).fun_sub
        (EventuallyEq.refl _ fun x ↦ b x • v x) using 1
    ext
    rw [Pi.mul_apply, mul_comm, mul_smul, ← smul_sub]
  refine (isLittleO_congr this.symm <| EventuallyEq.rfl).mp ((isBigO_refl b l).smul_isLittleO ?_)
  rcases huv.isBigO.exists_pos with ⟨C, hC, hCuv⟩
  rw [IsEquivalent] at *
  rw [isLittleO_iff] at *
  rw [IsBigOWith] at hCuv
  simp only [Metric.tendsto_nhds, dist_eq_norm] at hφ
  intro c hc
  specialize hφ (c / 2 / C) (div_pos (div_pos hc zero_lt_two) hC)
  specialize huv (div_pos hc zero_lt_two)
  refine hφ.mp (huv.mp <| hCuv.mono fun x hCuvx huvx hφx ↦ ?_)
  have key :=
    calc
      ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 / C * ‖u x‖ := by gcongr
      _ ≤ c / 2 / C * (C * ‖v x‖) := by gcongr
      _ = c / 2 * ‖v x‖ := by field
  calc
    ‖((fun x : α ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖ := by
      simp [sub_smul, sub_add]
    _ ≤ ‖(φ x - 1) • u x‖ + ‖u x - v x‖ := norm_add_le _ _
    _ = ‖φ x - 1‖ * ‖u x‖ + ‖u x - v x‖ := by rw [norm_smul]
    _ ≤ c / 2 * ‖v x‖ + ‖u x - v x‖ := by gcongr
    _ ≤ c / 2 * ‖v x‖ + c / 2 * ‖v x‖ := by gcongr; exact huvx
    _ = c * ‖v x‖ := by ring

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| (fun x ↦ (u - v) x + (t - w) x) =o[l] fun x ↦ v x + w x

Tactic:
enter [

Goal state after:
α : Type u_1
u v t w : α → ℝ
l : Filter α
hu : 0 ≤ v
hw : 0 ≤ w
htu : u ~[l] v
hvw : t ~[l] w
| (fun x ↦ (u - v) x + (t - w) x) =o[l] fun x ↦ v x + w x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hfi
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ Integrable (fun a ↦ f i a - f 0 a) μ

pp: case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a

Tactic:
· exact (hf_int i).sub (hf_int 0)

Goal state after:
case f_nn
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
i : ℕ
⊢ 0 ≤ᵐ[μ] fun a ↦ f i a - f 0 a
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f

Tactic:
· simp_rw [setToFun_eq _ hf, L1.setToL1_smul_left' hT hT' c h_smul]

Goal state after:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T' hT' f = c • setToFun μ T hT f
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: case zero
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
⊢ Bornology.IsBounded ((fun x ↦ x ^ 0) '' s)

Tactic:
by_cases s_empty : s = ∅
    · simp [s_empty]
    simp_rw [← nonempty_iff_ne_empty] at s_empty
    simp [s_empty]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
le_ae : ∀ᵐ (a : α) ∂μ, 0 ≤ ‖f a‖
h : AEStronglyMeasurable f μ
⊢ ‖∫ (a : α), f a ∂μ‖ ≤ ∫ (a : α), ‖f a‖ ∂μ

Tactic:
calc
      ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) :=
        norm_integral_le_lintegral_norm _
      _ = ∫ a, ‖f a‖ ∂μ := (integral_eq_lintegral_of_nonneg_ae le_ae <| h.norm).symm

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_6
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝⁴ : NormedDivisionRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : NormSMulClass 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : NormSMulClass 𝕜 F
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
· by_cases hr : c = 0
    · rw [hr]; simp
    · have hf' : ¬Integrable (c • f) μ := by rwa [integrable_smul_iff hr f]
      rw [setToFun_undef hT hf, setToFun_undef hT hf', smul_zero]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
classical
  rcases eq_or_neBot l with rfl | hl
  · simp
  have hfi : Integrable f μ := by
    obtain ⟨i, hi, h'i⟩ : ∃ i, ∫⁻ x, ‖fs i x - f x‖ₑ ∂μ < 1 ∧ Integrable (fs i) μ :=
      (((tendsto_order.1 hfs).2 _ zero_lt_one).and hfsi).exists
    have : Integrable (fs i - f) μ := ⟨h'i.aestronglyMeasurable.sub hf, hi.trans one_lt_top⟩
    convert h'i.sub this
    abel
  let f_lp := hfi.toL1 f
  let F_lp i := if hFi : Integrable (fs i) μ then hFi.toL1 (fs i) else 0
  have tendsto_L1 : Tendsto F_lp l (𝓝 f_lp) := by
    rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
    simp_rw [eLpNorm_one_eq_lintegral_enorm, Pi.sub_apply]
    refine (tendsto_congr' ?_).mp hfs
    filter_upwards [hfsi] with i hi
    refine lintegral_congr_ae ?_
    filter_upwards [hi.coeFn_toL1, hfi.coeFn_toL1] with x hxi hxf
    simp_rw [F_lp, dif_pos hi, hxi, f_lp, hxf]
  suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f)) by
    refine (tendsto_congr' ?_).mp this
    filter_upwards [hfsi] with i hi
    suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
    simp_rw [F_lp, dif_pos hi]
    exact hi.coeFn_toL1
  rw [setToFun_congr_ae hT hfi.coeFn_toL1.symm]
  exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : CompactSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : SeminormedAddCommGroup E
inst✝² : Nonempty α
inst✝¹ : One E
inst✝ : NormOneClass E
⊢ ‖1‖ = 1

Tactic:
simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm

Tactic:
have : SeparableSpace (range f ∪ {0} : Set G) := hf.separableSpace_range_union_singleton

Goal state after:
case pos
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β → G
hf : StronglyMeasurable f
hG : CompleteSpace G
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
hf_int : Integrable f μ
this : SeparableSpace ↑(range f ∪ {0})
⊢ ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
by_cases hF : CompleteSpace F; swap
  · simp [setToFun, hF]
  -- integrability for `μ` implies integrability for `μ'`.
  have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg =>
    Integrable.of_measure_le_smul hc' hμ'_le hg
  -- We use `Integrable.induction`
  apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
  · intro c s hs hμs
    have hμ's : μ' s ≠ ∞ := by
      refine ((hμ'_le s).trans_lt ?_).ne
      rw [Measure.smul_apply, smul_eq_mul]
      exact ENNReal.mul_lt_top hc'.lt_top hμs
    rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
  · intro f₂ g₂ _ hf₂ hg₂ h_eq_f h_eq_g
    rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]
  · refine isClosed_eq (continuous_setToFun hT) ?_
    have :
      (fun f : α →₁[μ] E => setToFun μ' T hT' f) = fun f : α →₁[μ] E =>
        setToFun μ' T hT' ((h_int f (L1.integrable_coeFn f)).toL1 f) := by
      ext1 f; exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
    rw [this]
    exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)
  · intro f₂ g₂ hfg _ hf_eq
    have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
    rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case insert
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → X i
hii' : i ≠ i'
⊢ ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∂μ) (update (update x i y) i' xᵢ) ∂μ i' =
    ∫⁻ (xᵢ : X i'), (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) (update x i' xᵢ) ∂μ i'

Tactic:
simp_rw [update_comm hii', ih (mt Finset.mem_insert_of_mem hi)]

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ¬∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s

Tactic:
· simpa [leftLim_eq_of_not_tendsto _ h''c] using hu hc

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
u : α
au : u < a
hu : Ioo u a ⊆ {x | f x ∈ s}
c : α
hc : c ∈ Ioo u a
h'c : (𝓝[<] c).NeBot
h''c : ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
⊢ leftLim f c ∈ id s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : ¬IntegrableOn f (s ∪ t) μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
integral_undef H,

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : ¬IntegrableOn f (s ∪ t) μ
⊢ 0 = ∫ (x : X) in s, f x ∂μ
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_meas : NullMeasurableSet s μ
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s

Tactic:
replace h_meas : ∀ g : G, NullMeasurableSet (g • s) μ := fun g => by
        rw [← inv_inv g, ← preimage_smul]; exact h_meas.preimage (h_qmp g⁻¹)
      have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by
        rw [← iUnion_smul_eq_ofPred_exists]; exact .iUnion h_meas
      rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_ofPred_exists]
      refine le_antisymm (measure_mono <| subset_univ _) ?_
      rw [measure_iUnion₀ aedisjoint h_meas]
      exact h_measure_univ_le

Goal state after: