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

Goal state before:
pp: ι : Type u_1
X : Type u_2
E : Type u_3
inst✝¹ : Countable ι
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
μ : ι → Measure X
f : X → E
hf : ∀ (i : ι), Integrable f (μ i)
h : Summable fun i ↦ ∫ (x : X), ‖f x‖ ∂μ i
⊢ HasFiniteIntegral f (Measure.sum μ)

Tactic:
· rw [HasFiniteIntegral, lintegral_sum_measure]
    convert! h.tsum_ofReal_lt_top with i
    rw [ofReal_integral_eq_lintegral_ofReal (hf i).norm]
    · simp_rw [ofReal_norm]
    · exact ae_of_all _ fun _ ↦ by positivity

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

Goal state before:
pp: R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
⊢ Bornology.IsBounded (s * t)

Tactic:
convert! mul_lip.isBounded_image bdd

Goal state after:
R : Type u_1
inst✝² : PseudoMetricSpace R
inst✝¹ : Monoid R
inst✝ : LipschitzMul R
s t : Set R
s_bdd : Bornology.IsBounded s
t_bdd : Bornology.IsBounded t
bdd : Bornology.IsBounded (s ×ˢ t)
C : ℝ≥0
mul_lip : LipschitzWith C fun p ↦ p.1 * p.2
⊢ s * t = (fun p ↦ p.1 * p.2) '' s ×ˢ t
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : 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 μ
hr : c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

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 μ
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f

Tactic:
· rw [hr]; simp

Goal state after:
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 μ
hr : ¬c = 0
⊢ setToFun μ T hT (c • f) = c • setToFun μ T hT f
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 α
f : α → G
⊢ setToFun 0 (weightedSMul 0) ⋯ f = 0

Tactic:
exact setToFun_measure_zero (dominatedFinMeasAdditive_weightedSMul _) rfl

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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) ↔ ∀ (y : E), ∀ x ∈ s, ContinuousWithinAt (fun x ↦ (f x) y) s x

Tactic:
continuousWithinAt_clm_apply,

Goal state after:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ (∀ x ∈ s, ∀ (y : E), ContinuousWithinAt (fun q ↦ (f q) y) s x) ↔
    ∀ (y : E), ∀ x ∈ s, ContinuousWithinAt (fun x ↦ (f x) y) s 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
⊢ ∫ (x : X) in ∅, f x ∂μ = 0

Tactic:
by
  rw [Measure.restrict_empty, integral_zero_measure]

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

Goal state before:
pp: case hf
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)
this :
  ∑ 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 ∂μ
u : Finset ι
⊢ u ∈ {x ∈ t.powerset | x.Nonempty} → Integrable ((⋂ i ∈ u, s i).indicator fun a ↦ (-1) ^ (#u + 1) • f a) μ

Tactic:
hu

Goal state after:
case hf
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)
this :
  ∑ 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 ∂μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ Integrable ((⋂ i ∈ u, s i).indicator fun a ↦ (-1) ^ (#u + 1) • f 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)
n : ℕ
⊢ StronglyMeasurable fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)

Tactic:
have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩

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
⊢ StronglyMeasurable fun x ↦ SimpleFunc.setToSimpleFunc T (s' n 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' : ∫⁻ (x : X) in S, ↑‖f x‖₊ ∂μ < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))

Tactic:
rw [← withDensity_apply₀ _ hSm] at hfi'

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
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ↑K = ↑⊥

Tactic:
subset_empty_iff.mp hK,

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ ∅ = ↑⊥
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)
g : G
⊢ NullMeasurableSet (g • s) μ

Tactic:
← inv_inv g,

Goal state after:
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)
g : G
⊢ NullMeasurableSet (g⁻¹⁻¹ • 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 μ
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
let k := f ⁻¹' {0}
  have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
  calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_sdiff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, Set.mem_sdiff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_sdiff hk (h'aux.mono hts le_rfl)]

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
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ 0 < sInf (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V})

Tactic:
Nat.sInf_def,

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ 0 < Nat.find ?m.21

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : PositiveCompacts G
V : Set G
hV : (interior V).Nonempty
⊢ (Finset.card '' {t | ↑K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}).Nonempty
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case refine_3
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ MeasurableSet (toMeasurable μ s)

pp: case refine_4
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x

Tactic:
· exact measurableSet_toMeasurable μ s

Goal state after:
case refine_4
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : PartialOrder E
inst✝² : IsOrderedAddMonoid E
inst✝¹ : IsOrderedModule ℝ E
μ : Measure X
f g : X → E
s : Set X
inst✝ : ClosedIciTopology E
hf : IntegrableOn f s μ
hg : IntegrableOn g s μ
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x ≤ g x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ toMeasurable μ s → f x ≤ g x
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X) in {y | f y ≤ 0}, f x ∂μ ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← integral_indicator hs, ←
    integral_indicator (hf.measurableSet_le stronglyMeasurable_const)]

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
s : Set X
hs : MeasurableSet s
hf : StronglyMeasurable f
hfi : Integrable f μ
⊢ ∫ (x : X), {a | f a ≤ 0}.indicator f x ∂μ ≤ ∫ (x : X), s.indicator f x ∂μ
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
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) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ

Tactic:
rw [integral_non_aestronglyMeasurable h'f]
    apply integral_nonneg_of_ae
    apply (ae_restrict_iff₀ ?_).2
    · filter_upwards with x hx using (hf x hx).trans (h x hx)
    · exact nullMeasurableSet_le aemeasurable_const hg.aemeasurable

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

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

Tactic:
hu

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪x, ↑v⟫ = ⟪y, ↑v⟫
u : E
hu : u ∈ K
⊢ ⟪x - y, u⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

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

Tactic:
hu

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
h : ∀ (v : ↥K), ⟪↑v, x⟫ = ⟪↑v, y⟫
u : E
hu : u ∈ K
⊢ ⟪u, x - y⟫ = 0
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
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
u : E
⊢ ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → ⟪f u, f v⟫ = 0

Tactic:
hu

Goal state after:
𝕜 : 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
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ u ∈ U, ∀ v ∈ V, ⟪u, v⟫ = 0
u : E
hu : ↑f u ∈ U
⊢ ∀ (v : E), ↑f v ∈ V → ⟪f u, f v⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : U ⟂ V
x y : E
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV) x, y⟫ = ⟪x, (U.subtype ∘ₗ U.projectionOnto V hUV) y⟫

Tactic:
← projection_add_projection_eq_self hUV x

Goal state after:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
hUV : IsCompl U V
h : U ⟂ V
x y : E
⊢ ⟪(U.subtype ∘ₗ U.projectionOnto V hUV) x, y⟫ =
    ⟪(U.projection V hUV) x + (V.projection U ⋯) x, (U.subtype ∘ₗ U.projectionOnto V hUV) y⟫
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
this : FiniteDimensional 𝕜 E
⊢ finrank 𝕜 ↥(𝕜 ∙ v) + n = finrank 𝕜 E

Tactic:
by
    simp [finrank_span_singleton hv, _i.elim, add_comm]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v

Tactic:
have he' : e ∈ (span 𝕜 v)ᗮ := smul_mem' _ _ hx'

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A B : ↥(unitaryGroup n α)
⊢ ↑(toGL (A * B)) = ↑(toGL A * toGL B)

Tactic:
simp only [coe_toGL, toLin'_mul]
  rfl

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : WithLp ∞ ((i : ι) → β i)
⊢ edist x.ofLp y.ofLp ≤ edist x y

Tactic:
by simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_ofLp ∞ β x y

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

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = √(∑ i, ‖x.ofLp i‖ ^ 2)

Tactic:
exact norm_eq_of_L2 x

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

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0
⊢ ↑(r + r) = 2 * ↑r

Tactic:
ENNReal.coe_add,

Goal state after:
case inr
a : ℝ
r : ℝ≥0
⊢ ↑r + ↑r = 2 * ↑r
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case inr
a : ℝ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ volume (closedEBall a r) = 2 * r

Tactic:
lift r to ℝ≥0 using hr
    rw [Metric.closedEBall_coe, volume_closedBall, two_mul, ← NNReal.coe_add,
      ENNReal.ofReal_coe_nnreal, ENNReal.coe_add, two_mul]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
⊢ ofReal |∏ i, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x, volume (s x)

Tactic:
have B : ∀ i, ofReal (abs (D i)) * volume ((D i * ·) ⁻¹' s i) = volume (s i) := by
    intro i
    have A : D i ≠ 0 := by
      simp only [det_diagonal, Ne] at h
      exact Finset.prod_ne_zero_iff.1 h i (Finset.mem_univ i)
    rw [volume_preimage_mul_left A, ← mul_assoc, ← ENNReal.ofReal_mul (abs_nonneg _), ← abs_mul,
      mul_inv_cancel₀ A, abs_one, ENNReal.ofReal_one, one_mul]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
D : ι → ℝ
h : (Matrix.diagonal D).det ≠ 0
s : ι → Set ℝ
hs : ∀ (i : ι), MeasurableSet (s i)
this : (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi fun i ↦ s i) = univ.pi fun i ↦ (fun x ↦ D i * x) ⁻¹' s i
B : ∀ (i : ι), ofReal |D i| * volume ((fun x ↦ D i * x) ⁻¹' s i) = volume (s i)
⊢ ofReal |∏ i, D i| * volume (⇑(toLin' (Matrix.diagonal D)) ⁻¹' univ.pi s) = ∏ x, volume (s x)
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
⊢ ∀ (D : ι → ℝ),
    (Matrix.diagonal D).det ≠ 0 →
      Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = ofReal |(Matrix.diagonal D).det⁻¹| • volume

Tactic:
intro D hD

Goal state after:
case hdiag
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
M : Matrix ι ι ℝ
hM : M.det ≠ 0
D : ι → ℝ
hD : (Matrix.diagonal D).det ≠ 0
⊢ Measure.map (⇑(toLin' (Matrix.diagonal D))) volume = ofReal |(Matrix.diagonal D).det⁻¹| • volume
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this : FiniteDimensional ℝ E
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar

Tactic:
have : FiniteDimensional ℝ F := w.finiteDimensional_of_finite

Goal state after:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fintype ι'
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this✝ : FiniteDimensional ℝ E
this : FiniteDimensional ℝ F
⊢ (v.prod w).addHaar = v.addHaar.prod w.addHaar