mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : 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 : μ s = 0
⊢ C * μ.real s = 0

Tactic:
rw [measureReal_def, hs_zero, ENNReal.toReal_zero, mul_zero]

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

Goal state before:
pp: case refine_1.inr
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
inst✝⁹ : NontriviallyNormedField 𝕜
inst✝⁸ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup Eₗ
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 Eₗ
inst✝² : NormedSpace 𝕜₂ F
inst✝¹ : CompleteSpace F
f : E →SL[σ₁₂] F
e : E →L[𝕜] Eₗ
N : ℝ≥0
inst✝ : RingHomIsometric σ₁₂
h_dense : DenseRange ⇑e
h_e : ∀ (x : E), ‖x‖ ≤ ↑N * ‖e x‖
hN : N ≤ 0
⊢ 0 ≤ ↑N * ‖f‖

Tactic:
| inr hN =>

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

Goal state before:
pp: case add
α : 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 g : α →ₛ E
hfg : Disjoint (support ⇑f) (support ⇑g)
hf : ∀ (hf : MemLp (⇑f) p μ), P (f.toLp hf)
hg : ∀ (hf : MemLp (⇑g) p μ), P (g.toLp hf)
hfg' : MemLp (⇑(f + g)) p μ
hf' : MemLp (⇑f) p μ
hg' : MemLp (⇑g) p μ
⊢ P ((f + g).toLp hfg')

Tactic:
exact add hf' hg' hfg (hf hf') (hg hg')

Goal state after:
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✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
this : ν (⇑f ⁻¹' {f x}) = 0
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f x

Tactic:
have A : μ (f ⁻¹' {f x}) = 0 := by simpa using (hμν _ |>.trans_eq this)

Goal state after:
α : Type u_1
F : Type u_3
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝² : PartialOrder F
inst✝¹ : IsOrderedAddMonoid F
inst✝ : IsOrderedModule ℝ F
ν : Measure α
f : α →ₛ F
hf : 0 ≤ᵐ[ν] ⇑f
hμν : μ ≤ ν
hfν : Integrable (⇑f) ν
x : α
hx : ¬0 ≤ f x
this : ν (⇑f ⁻¹' {f x}) = 0
A : μ (⇑f ⁻¹' {f x}) = 0
⊢ μ.real (⇑f ⁻¹' {f x}) • f x ≤ ν.real (⇑f ⁻¹' {f x}) • f 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 : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ ((fun i ↦ -g i) ⁻¹' {x}) < ∞

Tactic:
← Function.comp_def,

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 : ∀ (y : E), y ≠ 0 → μ (⇑g ⁻¹' {y}) < ∞
x : E
hx_ne : x ≠ 0
⊢ μ (Neg.neg ∘ ⇑g ⁻¹' {x}) < ∞
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
· rw [← isEquivalent_const_iff_tendsto h] at hu ⊢
    exact huv.symm.trans hu

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 : α) ∂μ, 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)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
⊢ ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a

Tactic:
filter_upwards [hf_mono] with a ha_mono i j hij

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 : α) ∂μ, 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)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
a : α
ha_mono : Monotone fun i ↦ f i a
i j : ℕ
hij : i ≤ j
⊢ (fun i ↦ f' i a) i ≤ (fun i ↦ f' i a) j
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case refine_1
α : 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
s : Finset ι
f : ι → α → E
hf✝ : ∀ i ∈ ∅, Integrable (f i) μ
⊢ setToFun μ T hT (∑ i ∈ ∅, f i) = ∑ i ∈ ∅, setToFun μ T hT (f i)

Tactic:
simp only [setToFun_zero, Finset.sum_empty]

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

Goal state before:
pp: case refine_2
α : 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
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i + ∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

Tactic:
setToFun_add hT (hf i (Finset.mem_insert_self i s)) _

Goal state after:
case refine_2
α : 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
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i) + setToFun μ T hT (∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)

α : 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
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ Integrable (∑ i ∈ s, f i) μ
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
C : ℝ
C0 : 0 ≤ C
⊢ ‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C

Tactic:
by
  simpa using! @dist_le _ _ _ _ f 0 _ C0

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 C' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
⊢ c' * μ s < ∞

Tactic:
exact ENNReal.mul_lt_top hc'.lt_top hμs

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

Goal state before:
pp: α : 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)
d : α
⊢ d ∈ Ioo u a → f d ∈ s

Tactic:
hd

Goal state after:
α : 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)
d : α
hd : d ∈ Ioo u a
⊢ f d ∈ s
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : 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))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
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)
d : α
⊢ d ∈ Ioo u a → f d ∈ s

Tactic:
hd

Goal state after:
α : 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))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
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)
d : α
hd : d ∈ Ioo u a
⊢ f d ∈ s
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) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
⊢ ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ

Tactic:
apply Finset.sum_congr rfl (fun x hx ↦ ?_)

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) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
x : Finset ι
hx : x ∈ {x ∈ t.powerset | x.Nonempty}
⊢ ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) a ∂μ
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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
y : α
⊢ ‖(s' n x) y‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) y

Tactic:
simp_rw [s', SimpleFunc.coe_comp]

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
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
y : α
⊢ ‖(⇑(s n) ∘ Prod.mk x) y‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) y
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: case refine_2
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
t : Finset ℕ
K : ℕ → Compacts G
n : ℕ
s : Finset ℕ
hn : n ∉ s
ih : μ (s.sup K) ≤ ∑ i ∈ s, μ (K i)
⊢ μ ((insert n s).sup K) ≤ ∑ i ∈ insert n s, μ (K i)

Tactic:
grw [Finset.sup_insert, Finset.sum_insert hn, μ.sup_le, ih]

Goal state after:
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:
rw [integral_undef H, integral_undef]

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) μ
⊢ ¬Integrable f (μ.restrict s)
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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in s ∩ k, f x ∂μ + ∫ (x : X) in s \ k, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [integral_inter_add_sdiff hk (h'aux.mono hts le_rfl)]

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

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
ι : Type u_5
inst✝⁵ : Countable ι
μ : Measure X
inst✝⁴ : NormedAddCommGroup E
inst✝³ : TopologicalSpace X
inst✝² : BorelSpace X
inst✝¹ : T2Space X
inst✝ : IsLocallyFiniteMeasure μ
f : C(X, E)
s : ι → Compacts X
hf : Summable fun i ↦ ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)
hs : ⋃ i, ↑(s i) = univ
⊢ Integrable (⇑f) μ

Tactic:
simpa only [hs, integrableOn_univ] using integrableOn_iUnion_of_summable_norm_restrict hf

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

Goal state before:
pp: X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ Integrable (s.indicator (const X c) * f) μ

Tactic:
rw [this, integrable_indicator_iff hs]

Goal state after:
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
this : s.indicator (const X c) * f = s.indicator (c • f)
⊢ IntegrableOn (c • f) s μ
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: case h'
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀) ↑K₀ ≠ ∞

Tactic:
· simp only [haarMeasure_self, ne_eq, ENNReal.one_ne_top, not_false_eq_true]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst✝⁶] K
hKpos : 0 < μ K
⊢ E / E ∈ 𝓝 1

Tactic:
filter_upwards [eventually_nhds_one_measure_smul_sdiff_lt hK K_closed hKpos.ne' (μ := μ)]
    with g hg

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : LocallyCompactSpace G
E : Set G
hE : MeasurableSet E
hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K
K : Set G
hKE : K ⊆ E
hK : IsCompact K
K_closed : IsClosed[inst✝⁶] K
hKpos : 0 < μ K
g : G
hg : μ (g • K \ K) < μ K
⊢ g ∈ E / E
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
hx : x ≠ 0
hr : r < 0
⊢ r * (‖x‖ * ‖x‖) ≠ 0

Tactic:
exact mul_ne_zero hr.ne (mul_self_ne_zero.2 (norm_ne_zero_iff.2 hx))

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (x ≠ 0 ∧ ∃ r, r ≠ 0 ∧ y = r • x) → ‖⟪x, y⟫ / (↑‖x‖ * ↑‖y‖)‖ = 1

Tactic:
· rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
    simp only [norm_div, norm_mul, norm_ofReal, abs_norm]
    exact norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul hx hr

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ ‖v i‖ ^ 2 = 1 ^ 2

Tactic:
rw [@norm_sq_eq_re_inner 𝕜, h i i]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
⊢ re (if i = i then 1 else 0) = 1 ^ 2
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_4
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
⊢ ‖(toSesqForm f) v‖ ≤ ‖f‖ * ‖v‖

Tactic:
by
  refine opNorm_le_bound _ (by positivity) fun x ↦ ?_
  have h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
  have h₂ := @norm_inner_le_norm 𝕜 E' _ _ _ v (f x)
  calc
    ‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
    _ ≤ ‖v‖ * (‖f‖ * ‖x‖) := by gcongr
    _ = ‖f‖ * ‖v‖ * ‖x‖ := by ring

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Subspace

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
⊢ iSupIndep V

Tactic:
classical
  apply iSupIndep_of_dfinsupp_lsum_injective
  refine LinearMap.ker_eq_bot.mp ?_
  rw [Submodule.eq_bot_iff]
  intro v hv
  rw [LinearMap.mem_ker] at hv
  ext i
  suffices ⟪(v i : E), v i⟫ = 0 by simpa only [inner_self_eq_zero] using! this
  calc
    ⟪(v i : E), v i⟫ = ⟪(v i : E), DFinsupp.lsum ℕ (fun i => (V i).subtype) v⟫ := by
      simpa only [DFinsupp.sumAddHom_apply, DFinsupp.lsum_apply_apply] using!
        (hV.inner_right_dfinsupp v i (v i)).symm
    _ = 0 := by simp only [hv, inner_zero_right]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
a✝ b✝ : E
hx : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hy : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
u : E
hu : u ∈ K
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by rw [inner_add_right, hx u hu, hy u hu, add_zero]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : WithLp p (α × β)
⊢ edist f f = 0

Tactic:
rcases p.trichotomy with (rfl | rfl | h)
  · classical
    simp
  · simp [prod_edist_eq_sup]
  · simp [prod_edist_eq_add h, ENNReal.zero_rpow_of_pos h,
      ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
prod_edist_eq_add pos,

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ Pi.single i a i' = 0

Tactic:
Pi.single_eq_of_ne' h

Goal state after:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ 0 = 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a b : ℝ
⊢ volume (uIoo a b) = ofReal |b - a|

Tactic:
by
  simp [uIoo, volume_Ioo, max_sub_min_eq_abs]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: a : ℝ
⊢ volume (Ici a) = ∞

Tactic:
rw [← measure_congr Ioi_ae_eq_Ici]; simp

Goal state after: