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

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
⊢ setToSimpleFunc T (map g f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (g x)

Tactic:
by
  classical
  have T_empty : T ∅ = 0 := h_add.map_empty_eq_zero
  have hfp : ∀ x ∈ f.range, x ≠ 0 → μ (f ⁻¹' {x}) ≠ ∞ := fun x _ hx0 =>
    (measure_preimage_lt_top_of_integrable f hf hx0).ne
  simp only [setToSimpleFunc, range_map]
  refine Finset.sum_image' _ fun b hb => ?_
  rcases mem_range.1 hb with ⟨a, rfl⟩
  by_cases h0 : g (f a) = 0
  · simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]
  have h_left_eq :
    T (map g f ⁻¹' {g (f a)}) (g (f a))
      = T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a)) := by
    rw [map_preimage_singleton]
  rw [h_left_eq]
  have h_left_eq' :
    T (f ⁻¹' ({b ∈ f.range | g b = g (f a)} : Finset _)) (g (f a))
      = T (⋃ y ∈ {b ∈ f.range | g b = g (f a)}, f ⁻¹' {y}) (g (f a)) := by
    rw [← Finset.set_biUnion_preimage_singleton]
  rw [h_left_eq']
  rw [h_add.map_iUnion_fin_meas_set_eq_sum T T_empty]
  · simp only [_root_.sum_apply]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [mem_filter] at hx
    rw [hx.2]
  · exact fun i => measurableSet_fiber _ _
  · grind
  · grind [Set.disjoint_iff]

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

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ ↑(AEEqFun.mk f ⋯) = setToFun μ (weightedSMul μ) ⋯ f

Tactic:
exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf

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

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace E
f : α →ₛ E
hfi : Integrable (⇑f) μ
⊢ ∫ (x : α), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
by
  rw [← f.integral_eq_integral hfi, SimpleFunc.integral, ← SimpleFunc.integral_eq]; rfl

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : NormedField β
u v : α → β
l : Filter α
hz : ∀ᶠ (x : α) in l, v x ≠ 0
⊢ u ~[l] v → Tendsto (u / v) l (𝓝 1)

Tactic:
intro hequiv
    have := hequiv.isLittleO.tendsto_div_nhds_zero
    simp only [Pi.sub_apply, sub_div] at this
    have key : Tendsto (fun x ↦ v x / v x) l (𝓝 1) :=
      (tendsto_congr' <| hz.mono fun x hnz ↦ @div_self _ _ (v x) hnz).mpr tendsto_const_nhds
    convert! this.add key
    · simp
    · simp

Goal state after:
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 : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖(a - b) x‖ ≤ c * ‖b x‖
φ : α → 𝕜
habφ : a =ᶠ[l] φ * b
this : ((fun x ↦ a x • u x) - fun x ↦ b x • v x) =ᶠ[l] fun x ↦ b x • (φ x • u x - v x)
C : ℝ
hC : C > 0
hCuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ C * ‖v x‖
c : ℝ
huv : ∀ᶠ (x : α) in l, ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφ : ∀ᶠ (x : α) in l, ‖φ x - 1‖ < c / 2 / C
hc : 0 < c
x : α
hCuvx : ‖u x‖ ≤ C * ‖v x‖
huvx : ‖(u - v) x‖ ≤ c / 2 * ‖v x‖
hφx : ‖φ x - 1‖ < c / 2 / C
key : ‖φ x - 1‖ * ‖u x‖ ≤ c / 2 * ‖v x‖
⊢ ‖((fun x ↦ φ x • u x) - v) x‖ = ‖(φ x - 1) • u x + (u x - v x)‖

Tactic:
simp [sub_smul, sub_add]

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module R W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
⊢ f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c

Tactic:
rw [← ContinuousAffineMap.coe_toAffineMap, AffineMap.apply_lineMap]

Goal state after:
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: R : Type u_1
S : Type u_2
V : Type u_3
W : Type u_4
inst✝¹² : Ring S
inst✝¹¹ : Ring R
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : AddCommGroup W
inst✝⁵ : Module R W
inst✝⁴ : TopologicalSpace W
inst✝³ : Module S W
inst✝² : SMulCommClass R S W
inst✝¹ : ContinuousConstSMul S W
inst✝ : IsTopologicalAddGroup W
p : W × (V →L[R] W)
⊢ ((decompLinearEquiv R S V W).symm p).contLinear = p.2

Tactic:
ext; simp [decompLinearEquiv]

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

Goal state before:
pp: case isClosed
α : 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 ℝ))
⊢ IsClosed {x | (setToL1 hT) x = (setToL1' 𝕜 hT h_smul) x}

Tactic:
exact isClosed_eq (setToL1 hT).continuous (setToL1' 𝕜 hT h_smul).continuous

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
⊢ ∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖

Tactic:
refine ⟨d • x, dxlt.le, fun y hy => ?_⟩

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
this : ‖c‖ / R < 1
x : E
xF : x ∉ F
hx : ∀ y ∈ F, ‖c‖ / R * ‖x‖ ≤ ‖x - y‖
x0 : x ≠ 0
d : 𝕜
d0 : d ≠ 0
dxlt : ‖d • x‖ < R
ledx : R / ‖c‖ ≤ ‖d • x‖
y : E
hy : y ∈ F
⊢ 1 ≤ ‖d • x - y‖
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 : ℝ
f : α → E
hF : CompleteSpace F
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
⊢ setToFun μ T hT f = (L1.setToL1 hT) (Integrable.toL1 f hf)

Tactic:
simp [setToFun, hF, hf]

Goal state after:
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 : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : ¬Integrable f μ
hF : CompleteSpace F
⊢ setToFun μ T hT f = 0

Tactic:
simp [setToFun, hF, hf]

Goal state after:
Module: Mathlib.Topology.Bornology.BoundedOperation

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
convert! LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
  norm_num

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ =
    ENNReal.ofReal (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹

Tactic:
ofReal_toReal

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ (∫⁻ (x : α), ‖f x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ = (∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹

α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_6
inst✝ : NormedAddCommGroup H
f : α → H
p : ℝ≥0∞
hp1 : p ≠ 0
hp2 : p ≠ ∞
hf : MemLp f p μ
A : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p.toReal) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ ≠ ∞
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ ⨆ x, dist (f x) (g x) = ↑(⨆ x, nndist (f x) (g x))

Tactic:
simp_rw [val_eq_coe, coe_iSup, coe_nndist]

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ⇑(npowRec n f * f) = ⇑f ^ (n + 1)

Tactic:
pow_succ,

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ⇑(npowRec n f * f) = ⇑f ^ n * ⇑f
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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
by_cases hf : Integrable f μ
  · exact setToFun_congr_measure_of_integrable c' hc' hμ'_le hT hT' f hf
  · -- if `f` is not integrable, both `setToFun` are 0.
    have h_int : ∀ g : α → E, ¬Integrable g μ → ¬Integrable g μ' := fun g =>
      mt fun h => h.of_measure_le_smul hc hμ_le
    simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]

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 : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
⊢ x ∉ cthickening δ E →
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
hδ

Goal state after:
α : Type u_1
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
hδ : x ∉ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Module: Mathlib.MeasureTheory.Integral.Marginal

Goal state before:
pp: case inr
δ : Type u_1
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : Fintype δ
s : Finset δ
f g : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hfg : ∫⋯∫⁻_s, f ∂μ = ∫⋯∫⁻_s, g ∂μ
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.univ, f ∂μ) x = (∫⋯∫⁻_Finset.univ, g ∂μ) x

Tactic:
lmarginal_eq_of_subset (Finset.subset_univ s) hf hg hfg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a

Tactic:
rw [h'α.topology_eq_generate_intervals] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[<] a = ⊥
⊢ leftLim f a = f a
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = f a

Tactic:
rw [h'α.topology_eq_generate_intervals] at h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y)
⊢ leftLim f a = f a
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
l : Filter ι
inst✝ : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s
h✝ : {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈ l
k : ℕ
h : ∀ b ≥ k, x b ∈ {x | (fun n ↦ AEStronglyMeasurable (fs n) μ) x} ∩ {x | (fun n ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x}
⊢ ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ

Tactic:
exact fun n => (h _ (self_le_add_left _ _)).1

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 : ℝ
β : 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)
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun x_1 ↦ (T (⇑(s' n x_1) ⁻¹' {x})) x

Tactic:
simp only [s', SimpleFunc.coe_comp, preimage_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)
n : ℕ
this : ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun x_1 ↦ (T (Prod.mk x_1 ⁻¹' ⇑(s n) ⁻¹' {x})) x
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 i, f x ∂μ ∈ Metric.closedBall (∫ (x : X) in S, f x ∂μ) ↑ε

Tactic:
rw [mem_closedBall_iff_norm', ← setIntegral_sdiff₀ (hsm i) hfi hsub, ← coe_nnnorm,
    NNReal.coe_le_coe, ← 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 m_mono
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
K : Compacts G
⊢ ∀ ⦃s₁ s₂ : Set G⦄ (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂),
    s₁ ⊆ s₂ → μ.innerContent { carrier := s₁, is_open' := hs₁ } ≤ μ.innerContent { carrier := s₂, is_open' := hs₂ }

Tactic:
· exact μ.innerContent_mono

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
this : ↑(L' ⊔ M') ⊆ ↑U'
⊢ μ L' + μ M' ≤ μ.outerMeasure ↑U'

Tactic:
rw [μ.outerMeasure_of_isOpen (↑U') U'.2]

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝² : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝¹ : ↑U' \ U ⊆ ↑U' \ ↑L'
this✝ : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
M : Compacts G
hM : ↑M ⊆ ↑U' \ ↑L'
M' : Compacts G := { carrier := closure ↑M, isCompact' := ⋯ }
hM' : ↑M' ⊆ ↑U' \ ↑L'
this : ↑(L' ⊔ M') ⊆ ↑U'
⊢ μ L' + μ M' ≤ μ.innerContent { carrier := ↑U', is_open' := ⋯ }
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ (haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty

Tactic:
have : IsCompact (haarProduct (K₀ : Set G)) := by
    apply isCompact_univ_pi; intro K; apply isCompact_Icc

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
this : IsCompact (haarProduct ↑K₀)
⊢ (haarProduct ↑K₀ ∩ ⋂ V, clPrehaar (↑K₀) V).Nonempty
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case neg
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : ¬Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

pp: case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

Tactic:
· simp [integral_undef H]

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : ∀ x ∈ s, f x ≤ 1
h's : ∀ x ∈ sᶜ, f x ≤ 0
H : Integrable f μ
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case pos.refine_1
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
g : X → ℝ
hf : ∀ x ∈ s, 0 ≤ f x
h : ∀ x ∈ s, f x ≤ g x
hg : IntegrableOn g s μ
h'f : AEStronglyMeasurable f (μ.restrict s)
⊢ ∀ᵐ (x : X) ∂μ, x ∈ s → 0 x ≤ f x

Tactic:
filter_upwards with x hx using hf x hx

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
⊢ normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + normSq y =
    normSq x * t * t + re ⟪x, y⟫ * t + re ⟪x, y⟫ * t + normSq y

Tactic:
by rw [inner_re_symm]

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

Goal state before:
pp: case neg
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
⊢ 0 ≤ normSq x * (t * t) + 2 * ‖⟪x, y⟫‖ * t + normSq y

Tactic:
have hzero' : ‖⟪x, y⟫‖ ≠ 0 := norm_ne_zero_iff.2 hzero
    convert! cauchy_schwarz_aux' (𝕜 := 𝕜) (⟪x, y⟫ • x) y (t / ‖⟪x, y⟫‖) using 3
    · field_simp
      rw [normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫,
        mul_conj]
      rw [← ofReal_pow, re_ofReal_mul]
      ring
    · field_simp
      rw [inner_smul_left, mul_comm _ ⟪x, y⟫_𝕜, mul_conj, ← ofReal_pow, ofReal_re]
      ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖w‖ ^ 2 ↔ ⟪v - w, w⟫ = 0

Tactic:
inner_sub_left,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
⊢ ⟪v, w⟫ = ↑‖w‖ ^ 2 ↔ ⟪v, w⟫ - ⟪w, w⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ ⟪x - y, x - y⟫ = 0

Tactic:
inner_sub_left,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
h : ∀ (v : E), ⟪x, v⟫ = ⟪y, v⟫
⊢ ⟪x, x - y⟫ - ⟪y, x - y⟫ = 0
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
K : Set G
hKE : K ⊆ E
hK_comp : IsCompact K
hK_meas : 0 < μ K
⊢ 0 < μ (closure[inst✝⁶] K)

Tactic:
rwa [hK_comp.measure_closure]

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

Goal state before:
pp: V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪S x - T x, x⟫_ℂ = 0

Tactic:
inner_sub_left,

Goal state after:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
S T : V →ₗ[ℂ] V
x : V
⊢ ⟪S x, x⟫_ℂ = ⟪T x, x⟫_ℂ ↔ ⟪S x, x⟫_ℂ - ⟪T x, x⟫_ℂ = 0