mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
𝕜 : Type u_6
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
k : 𝕜
f : ↥(simpleFunc E p μ)
a✝ : α
⊢ (toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ →
    (toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → (toSimpleFunc (k • f)) a✝ = k • (toSimpleFunc f) a✝

Tactic:
repeat intro h; rw [h]

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Extend

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : NormedAddCommGroup Eₗ
inst✝⁶ : NormedSpace 𝕜 Eₗ
inst✝⁵ : CompleteSpace Eₗ
inst✝⁴ : NormedAddCommGroup Fₗ
inst✝³ : NormedSpace 𝕜₂ Fₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_dense₂ : DenseRange ⇑e₂
h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖
h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖
⊢ ∀ (x : Eₗ), ‖↑(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ ⋯) x‖ = ‖x‖

Tactic:
refine h_dense₁.induction ?_ (isClosed_eq (by
        simp only [ContinuousLinearEquiv.coe_toLinearEquiv]; fun_prop) continuous_norm)

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : NormedAddCommGroup Eₗ
inst✝⁶ : NormedSpace 𝕜 Eₗ
inst✝⁵ : CompleteSpace Eₗ
inst✝⁴ : NormedAddCommGroup Fₗ
inst✝³ : NormedSpace 𝕜₂ Fₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_dense₂ : DenseRange ⇑e₂
h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖
h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖
⊢ ∀ x ∈ Set.range ⇑e₁, ‖↑(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ ⋯) x‖ = ‖x‖
Module: Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

Goal state before:
pp: α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
hp_pos : p ≠ 0
hp_ne_top : p ≠ ∞
P : ↥(simpleFunc E p μ) → Prop
indicatorConst : ∀ (c : E) {s : Set α} (hs : MeasurableSet s) (hμs : μ s < ∞), P (simpleFunc.indicatorConst p hs ⋯ c)
add :
  ∀ ⦃f g : α →ₛ E⦄ (hf : MemLp (⇑f) p μ) (hg : MemLp (⇑g) p μ),
    Disjoint (support ⇑f) (support ⇑g) → P (f.toLp hf) → P (g.toLp hg) → P (f.toLp hf + g.toLp hg)
f : ↥(simpleFunc E p μ)
this : ∀ (f : α →ₛ E) (hf : MemLp (⇑f) p μ), P (f.toLp hf)
⊢ P ((toSimpleFunc f).toLp ⋯)

Tactic:
apply this

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

Goal state before:
pp: case inr
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
m : MeasurableSpace α
inst✝ : DecidablePred fun x ↦ x ≠ 0
T : Set α → F →L[ℝ] F'
hT : T ∅ = 0
f : α →ₛ F
s : Finset F
hs : {x ∈ f.range | x ≠ 0} ⊆ s
x : F
hx✝ : x ∉ f.range ∨ x = 0
hx : x ∉ Set.range ⇑f
⊢ (T (⇑f ⁻¹' {x})) x = 0

Tactic:
rw [preimage_eq_empty] <;> simp [Set.disjoint_singleton_left, hx, hT]

Goal state after:
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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 = setToSimpleFunc T (map Prod.snd (f.pair g))

Tactic:
rw [map_setToSimpleFunc T h_add h_pair Prod.snd_zero]

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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y ↦ T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 = ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc (posPart f))) -
      MeasureTheory.SimpleFunc.integral μ (SimpleFunc.map norm (toSimpleFunc (negPart f)))

Tactic:
← SimpleFunc.integral_sub

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ MeasureTheory.SimpleFunc.integral μ (toSimpleFunc f) =
    MeasureTheory.SimpleFunc.integral μ
      (SimpleFunc.map norm (toSimpleFunc (posPart f)) - SimpleFunc.map norm (toSimpleFunc (negPart f)))

case hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))) μ

case hg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
ae_eq₁ : ⇑(toSimpleFunc f).posPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (posPart f)))
ae_eq₂ : ⇑(toSimpleFunc f).negPart =ᵐ[μ] ⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))
⊢ Integrable (⇑(SimpleFunc.map norm (toSimpleFunc (negPart f)))) μ
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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2 =
    setToSimpleFunc T (map Prod.fst (f.pair g)) + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2

Tactic:
map_setToSimpleFunc T h_add hp_pair Prod.fst_zero

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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
hp_pair : Integrable (⇑(f.pair g)) μ
⊢ ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2 =
    ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.1 + ∑ x ∈ (f.pair g).range, (T (⇑(f.pair g) ⁻¹' {x})) x.2
Module: Mathlib.MeasureTheory.Integral.Bochner.L1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ‖integral f‖ = ‖integralCLM f‖

Tactic:
by simp only [integral]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ENNReal.ofReal ↑(f a) ∂μ).toReal

Tactic:
← ENNReal.coe_nnreal_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (fun x ↦ ↑(f x)) μ
⊢ ∫⁻ (a : α), ↑(f a) ∂μ = ENNReal.ofReal (∫⁻ (a : α), ↑(f a) ∂μ).toReal
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), 0 ≤ f' n x
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
this : Tendsto (fun n ↦ ∫ (x : α), f' n x ∂μ) atTop (𝓝 (∫ (x : α), (F - f 0) x ∂μ))
⊢ Tendsto (fun n ↦ ∫ (x : α), f n x ∂μ) atTop (𝓝 (∫ (x : α), F x ∂μ))

Tactic:
simp_rw [f', integral_sub (hf _) (hf _), integral_sub' hF (hf 0),
      tendsto_sub_const_iff] at this
    exact this

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

Goal state before:
pp: case e'_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
x✝ : ℕ
⊢ ∫ (x : α), - -f x✝ x ∂μ = -∫ (x : α), -f x✝ x ∂μ

Tactic:
rw [integral_neg]

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

Goal state before:
pp: case e'_5
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
this : Tendsto (fun n ↦ ∫ (x : α), -f n x ∂μ) atTop (𝓝 (∫ (x : α), -F x ∂μ))
⊢ ∫ (x : α), - -F x ∂μ = -∫ (x : α), -F x ∂μ

Tactic:
rw [integral_neg]

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

Goal state before:
pp: case mem
α : 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 α
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕜 F
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : IsBoundedSMul 𝕜 F
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
f : ↥(Lp E 1 μ)
h₁ : Dense (range ⇑(coeToLp α E ℝ))
⊢ ∀ x ∈ range ⇑(coeToLp α E ℝ), (setToL1 hT) x = (setToL1' 𝕜 hT h_smul) x

Tactic:
intro f ⟨f', hf⟩
    simp [← hf]

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

Goal state before:
pp: α : 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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
filter_upwards [this] with a ha_tendsto

Goal state after:
α : 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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha_tendsto : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case e'_3
α : 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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
x✝ : ℕ
⊢ ∫ (a : α), f' x✝ a ∂μ = -∫ (a : α), f x✝ a ∂μ

Tactic:
rw [integral_neg]

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

Goal state before:
pp: case e'_5
α : 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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ ∫ (a : α), F' a ∂μ = -∫ (a : α), F a ∂μ

Tactic:
rw [integral_neg]

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

Goal state before:
pp: case refine_1
α : 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 : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ Tendsto (fun i ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))

Tactic:
convert! hf_tendsto.neg
    · rw [integral_neg]
    · rw [integral_neg]

Goal state after:
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 = ∅

Goal state after:
case pos
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : s = ∅
⊢ Bornology.IsBounded ((fun x ↦ x ^ 0) '' s)

case neg
R : Type u_2
inst✝² : Bornology R
inst✝¹ : Monoid R
inst✝ : BoundedMul R
s : Set R
s_bdd : Bornology.IsBounded s
s_empty : ¬s = ∅
⊢ Bornology.IsBounded ((fun x ↦ x ^ 0) '' s)
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
x : R
s : Set R
hs : Bornology.IsBounded sᶜ
y : R
⊢ y ∈ (fun x_1 ↦ x_1 + x) ⁻¹' sᶜ ↔ y ∈ sᶜ - {x}

Tactic:
simp [sub_eq_iff_eq_add]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type w
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : CompleteSpace 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f.linear
x y : PE
⊢ ‖x -ᵥ y‖ ≤ ↑K * ‖f.linear (x -ᵥ y)‖

Tactic:
exact ZeroHomClass.bound_of_antilipschitz f.linear hK (x -ᵥ y)

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

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
hE : CompleteSpace E
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst✝ : Decidable (a ∈ s)
h✝ : a ∈ s
⊢ ∫ (x : α), f x ∂Measure.dirac a = f a

Tactic:
exact integral_dirac _ _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(zsmulRec (fun x1 x2 ↦ x1 • x2) (Int.ofNat n) f) = Int.ofNat n • ⇑f

Tactic:
rw [zsmulRec, Int.ofNat_eq_natCast, coe_nsmul, natCast_zsmul]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : LocallyCompactSpace E
r : ℝ
rpos : 0 < r
hr : IsCompact (closedBall 0 r)
c : 𝕜
hc : 1 < ‖c‖
n : ℕ
⊢ IsCompact (closedBall 0 (‖c‖ ^ n * r))

Tactic:
have : c ^ n ≠ 0 := pow_ne_zero _ <| fun h ↦ by simp [h, zero_le_one.not_gt] at hc
    simpa [_root_.smul_closedBall' this] using hr.smul (c ^ n)

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:
by simp only [← norm_mkOfCompact, mkOfCompact_one, norm_one]

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

Goal state before:
pp: case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖f‖ ≤ ‖⇑f‖

pp: case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖⇑f‖ ≤ ‖f‖

Tactic:
· rw [ContinuousMap.norm_le _ (by positivity)]
    exact norm_le_pi_norm _

Goal state after:
case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖⇑f‖ ≤ ‖f‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ c'.toReal * (ε / 2 / c'.toReal) = ε / 2

Tactic:
refine mul_div_cancel₀ (ε / 2) ?_

Goal state after:
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ c'.toReal ≠ 0
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ (thickenedIndicator δ_pos E) y ≤ (thickenedIndicator δ_pos E) x

Tactic:
simp only [thickenedIndicator_apply]
  gcongr
  · finiteness
  · exact thickenedIndicatorAux_mono_infEDist δ h

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
by
  by_cases x_mem_closure : x ∈ closure E
  · filter_upwards [univ_mem] with δ _
    have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
    rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
  · filter_upwards [eventually_notMem_cthickening_of_infEDist_pos x_mem_closure] with δ hδ
    simp only [hδ, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ

Tactic:
← integral_indicator (Finset.measurableSet_biUnion _ hs)

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X), (⋃ i ∈ t, s i).indicator f x ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x ↦ ↑‖f x‖₊) S < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun x ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ε

Tactic:
← ENNReal.coe_le_coe

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
S : Set X := ⋃ i, s i
hfi : IntegrableOn f S μ
hfi' : (μ.withDensity fun x ↦ ↑‖f x‖₊) S < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
ν : Measure X := μ.withDensity fun x ↦ ‖f x‖ₑ
hν : ν = μ.withDensity fun x ↦ ‖f x‖ₑ
ε : ℝ≥0
ε0 : 0 < ↑ε
this : ∀ᶠ (i : ι) in atTop, ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
i : ι
hi : ν (s i) ∈ Icc (ν S - ↑ε) (ν S + ↑ε)
⊢ ↑‖∫ (x : X) in S \ s i, f x ∂μ‖₊ ≤ ↑ε
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ ∑ i ∈ t, μ (L i) ≤ ∑' (i : ℕ), μ.innerContent (U i)

Tactic:
refine le_trans (Finset.sum_le_sum ?_) (ENNReal.sum_le_tsum t)

Goal state after:
case convert_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
t : Finset ℕ
ht : ↑K ⊆ ⋃ i ∈ t, ↑(U i)
K' : ℕ → Set G
h1K' : ∀ (i : ℕ), IsCompact (K' i)
h2K' : ∀ (i : ℕ), K' i ⊆ (SetLike.coe ∘ U) i
h3K' : ↑K = ⋃ i ∈ t, K' i
L : ℕ → Compacts G := fun n ↦ { carrier := K' n, isCompact' := ⋯ }
⊢ ∀ i ∈ t, μ (L i) ≤ μ.innerContent (U i)
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: 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
⊢ IntegrableOn f t μ

Tactic:
apply integrableOn_zero.congr_fun_ae

Goal state after:
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
⊢ (fun x ↦ 0) =ᵐ[μ.restrict t] f