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

Goal state before:
pp: case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : CompleteSpace G''
hfi : Integrable f μ
⊢ 0 ≤ setToFun μ T hT f

pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : CompleteSpace G''
hfi : ¬Integrable f μ
⊢ 0 ≤ setToFun μ T hT f

Tactic:
· simp_rw [setToFun_eq _ hfi]
    exact L1.setToL1_nonneg hT hT_nonneg hf

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
G' : Type u_7
G'' : Type u_8
inst✝⁷ : NormedAddCommGroup G''
inst✝⁶ : PartialOrder G''
inst✝⁵ : IsOrderedAddMonoid G''
inst✝⁴ : NormedSpace ℝ G''
inst✝³ : NormedAddCommGroup G'
inst✝² : PartialOrder G'
inst✝¹ : NormedSpace ℝ G'
inst✝ : ClosedIciTopology G''
T : Set α → G' →L[ℝ] G''
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x
f : α → G'
hf : 0 ≤ᵐ[μ] f
hG'' : CompleteSpace G''
hfi : ¬Integrable f μ
⊢ 0 ≤ setToFun μ T hT f
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_2
F✝ : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : PseudoMetricSpace γ
f✝ g : α →ᵇ β
x✝ : α
C✝ : ℝ
inst✝ : CompleteSpace β
f : ℕ → α →ᵇ β
hf : CauchySeq f
b : ℕ → ℝ
b0 : ∀ (n : ℕ), 0 ≤ b n
b_bound : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (f n) (f m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
f_bdd : ∀ (x : α) (n m N : ℕ), N ≤ n → N ≤ m → dist ((f n) x) ((f m) x) ≤ b N
fx_cau : ∀ (x : α), CauchySeq fun n ↦ (f n) x
F : α → β
hF : ∀ (x : α), Tendsto (fun n ↦ (f n) x) atTop (𝓝 (F x))
fF_bdd : ∀ (x : α) (N : ℕ), dist ((f N) x) (F x) ≤ b N
C : ℝ
hC : ∀ (x y : α), dist ((f 0) x) ((f 0) y) ≤ C
x y : α
⊢ dist ({ toFun := F, continuous_toFun := ⋯ }.toFun x) ({ toFun := F, continuous_toFun := ⋯ }.toFun y) ≤ C + (b 0 + b 0)

Tactic:
calc
        dist (F x) (F y) ≤ dist (f 0 x) (f 0 y) + (dist (f 0 x) (F x) + dist (f 0 y) (F y)) :=
          dist_triangle4_left _ _ _ _
        _ ≤ C + (b 0 + b 0) := add_le_add (hC x y) (add_le_add (fF_bdd x 0) (fF_bdd y 0))

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝¹ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g✝ : β →L[𝕜] γ
f g : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g✝ ∘ ⇑(f + g)) ⋯ (‖g✝‖ * ‖f + g‖) ⋯ =
    ofNormedAddCommGroup (⇑g✝ ∘ ⇑f) ⋯ (‖g✝‖ * ‖f‖) ⋯ + ofNormedAddCommGroup (⇑g✝ ∘ ⇑g) ⋯ (‖g✝‖ * ‖g‖) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
𝕜 : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
f✝ g✝ : α →ᵇ β
x : α
C : ℝ
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 β
inst✝¹ : SeminormedAddCommGroup γ
inst✝ : NormedSpace 𝕜 γ
g : β →L[𝕜] γ
c : 𝕜
f : α →ᵇ β
⊢ ofNormedAddCommGroup (⇑g ∘ ⇑(c • f)) ⋯ (‖g‖ * ‖c • f‖) ⋯ =
    (RingHom.id 𝕜) c • ofNormedAddCommGroup (⇑g ∘ ⇑f) ⋯ (‖g‖ * ‖f‖) ⋯

Tactic:
ext; simp

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

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y

Tactic:
have : FiniteDimensional ℝ E :=
      .of_isCompact_closedBall ℝ hr₀
        (hK.of_isClosed_subset Metric.isClosed_closedBall hrK)

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
K : Set E
hK : IsCompact K
hx : x ∈ K
r : ℝ
hr₀ : 0 < r
hrK : closedBall x r ⊆ K
this : FiniteDimensional ℝ E
⊢ ∃ y ∈ frontier K, infDist x Kᶜ = dist x y
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
by
  simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ
hf_nonneg : 0 ≤ᵐ[μ] f
hg_nonneg : 0 ≤ᵐ[μ] g
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫ (a : α), f a * g a ∂μ = ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ
h_right_f : ∫ (a : α), f a ^ p ∂μ = ∫ (a : α), ‖f a‖ ^ p ∂μ
h_right_g : ∫ (a : α), g a ^ q ∂μ = ∫ (a : α), ‖g a‖ ^ q ∂μ
⊢ ∫ (a : α), ‖f a‖ * ‖g a‖ ∂μ ≤ (∫ (a : α), ‖f a‖ ^ p ∂μ) ^ (1 / p) * (∫ (a : α), ‖g a‖ ^ q ∂μ) ^ (1 / q)

Tactic:
exact integral_mul_norm_le_Lp_mul_Lq hpq hf hg

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

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
⊢ ⨅ a, ⨅ b, ⨅ (_ : s₁ \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a) ≤
    ⨅ a, ⨅ b, ⨅ (_ : s₂ \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f a)

Tactic:
exact iInf_mono fun a => biInf_mono fun b => by gcongr

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
inst✝ : WeaklyLocallyCompactSpace G
K : Set G
hK : IsCompact K
⊢ μ.outerMeasure K < ∞

Tactic:
by
  rcases exists_compact_superset hK with ⟨F, h1F, h2F⟩
  calc
    μ.outerMeasure K ≤ μ.outerMeasure (interior F) := measure_mono h2F
    _ ≤ μ ⟨F, h1F⟩ := by
      apply μ.outerMeasure_le ⟨interior F, isOpen_interior⟩ ⟨F, h1F⟩ interior_subset
    _ < ⊤ := μ.lt_top _

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
μ : Measure X
inst✝ : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ {x | f x < 0 ∨ f x = 0} = {x | f x < 0} ∪ {x | f x = 0}

Tactic:
ofPred_or

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

Goal state before:
pp: case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
⊢ ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ = -∫ (x : X) in {x | 0 ≤ f x}ᶜ, f x ∂μ

Tactic:
← integral_neg

Goal state after:
case e_a
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x | 0 ≤ f x} μ
⊢ ∫ (x : X) in {x | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ = ∫ (a : X) in {x | 0 ≤ f x}ᶜ, -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
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ ∫ (x : X) in s, ↑↑(indicatorConstLp p ht hμt e) x ∂μ = ∫ (x : X) in s, t.indicator (fun x ↦ e) x ∂μ

Tactic:
setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Set X
μ : Measure X
inst✝ : CompleteSpace E
p : ℝ≥0∞
hs : MeasurableSet s
ht : MeasurableSet t
hμt : μ t ≠ ∞
e : E
⊢ ∫ (x : X) in s, t.indicator (fun x ↦ e) x ∂μ = ∫ (x : X) in s, t.indicator (fun x ↦ e) 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
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ ‖∫ (x : X) in sᶜ, f x ∂μ‖ ≤ μ.real sᶜ * C

Tactic:
← h2

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
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
h0 : ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ
h1 : ∫ (x : X) in sᶜ, ‖f x‖ ∂μ ≤ ∫ (x : X) in sᶜ, C ∂μ
h2 : ∫ (x : X) in sᶜ, C ∂μ = μ.real sᶜ * C
⊢ ‖∫ (x : X) in sᶜ, f x ∂μ‖ ≤ ∫ (x : X) in sᶜ, C ∂μ
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
⊢ f.measure (Ioi x) = ofReal (l - ↑f x)

Tactic:
← Ici_sdiff_left,

Goal state after:
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
⊢ f.measure (Ici x \ {x}) = ofReal (l - ↑f x)
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 : F
⊢ im ⟪x, x⟫ = 0

Tactic:
by
  rw [← @ofReal_inj 𝕜, im_eq_conj_sub]
  simp [inner_conj_symm]

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
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ prehaar ↑K₀ '' {U | U ⊆ ↑⊤.toOpens ∧ IsOpen[inst✝¹] U ∧ 1 ∈ U} ⊆ eval ⁻¹' Ici 0

pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)

Tactic:
· rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
    apply prehaar_mono _ h; rw [h2U.interior_eq]; exact ⟨1, h3U⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₂ - f K₁
this : Continuous eval
⊢ IsClosed (eval ⁻¹' Ici 0)
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
⊢ tF = PseudoMetricSpace.toUniformSpace.toTopologicalSpace

Tactic:
let p : Seminorm 𝕜 F := @normSeminorm 𝕜 F _ cd.toNormedAddCommGroup.toSeminormedAddCommGroup
    InnerProductSpace.Core.toNormedSpace

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ tF = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ (δ : ℝ), 0 < δ ∧ ∫ x in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε := by
    simpa [integral_mul_const] using exists_pos_mul_lt εpos _

Goal state after:
Y : Type u_2
E : Type u_3
F : Type u_4
X : Type u_5
G : Type u_6
𝕜 : Type u_7
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : MeasurableSpace Y
inst✝⁸ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : NormedSpace 𝕜 E
L : F →L[𝕜] G →L[𝕜] E
f : X → Y → G
s : Set X
k : Set Y
g : Y → F
hk : IsCompact k
hf : ContinuousOn (uncurry f) (s ×ˢ univ)
hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0
hg : IntegrableOn g k μ
A : ∀ p ∈ s, Continuous[inst✝¹⁰, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f p)
q : X
hq : q ∈ s
ε : ℝ
εpos : ε > 0
δ : ℝ
δpos : 0 < δ
hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε
⊢ ∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε
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
g : G
K : Compacts G
⊢ (haarContent K₀) (Compacts.map (fun x ↦ g * x) ⋯ K) = (haarContent K₀) K

Tactic:
by
  simpa only [ENNReal.coe_inj, ← NNReal.coe_inj, haarContent_apply] using!
    is_left_invariant_chaar g K

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
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
i : ι
⊢ ⟪v i, (linearCombination 𝕜 v) l⟫ = l i

Tactic:
simp [linearCombination_apply, Finsupp.inner_sum, orthonormal_iff_ite.mp hv, inner_smul_right,
    eq_comm]

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

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : ↑K
this : ⟪u - v, ↑w - v⟫_ℝ ≤ 0
⊢ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, ↑w - v⟫_ℝ ≤ ‖u - v‖ * ‖u - v‖ - 2 * ⟪u - v, ↑w - v⟫_ℝ + ‖↑w - v‖ ^ 2

Tactic:
refine le_add_of_nonneg_right ?_

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
h✝ : Convex ℝ K
u v : F
hv : v ∈ K
this✝ : Nonempty ↑K := Nonempty.intro ⟨v, hv⟩
h : ∀ w ∈ K, ⟪u - v, w - v⟫_ℝ ≤ 0
w : ↑K
this : ⟪u - v, ↑w - v⟫_ℝ ≤ 0
⊢ 0 ≤ ‖↑w - v‖ ^ 2
Module: Mathlib.Analysis.InnerProductSpace.LinearMap

Goal state before:
pp: 𝕜 : Type u_4
F : Type u_6
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
⊢ ((rankOne 𝕜) x) 1 = toSpanSingleton 𝕜 x

Tactic:
ext; simp

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

Goal state before:
pp: 𝕜 : Type u_4
F : Type u_6
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x : F
⊢ ((rankOne 𝕜) 1) x = (innerSL 𝕜) x

Tactic:
ext; simp

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : TopologicalSpace M
inst✝² : Module R M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousConstSMul R M
s : Submodule R M
hs : IsClosed s.carrier
⊢ s.closure = { toSubmodule := s, isClosed' := hs }

Tactic:
ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
⊢ ‖(K.projection Kᗮ ⋯) x‖ ≤ ‖x‖

Tactic:
conv_rhs => rw [← projection_add_projection_eq_self K.isCompl_orthogonal x]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
⊢ ‖(K.projection Kᗮ ⋯) x‖ ≤ ‖(K.projection Kᗮ ⋯) x + (Kᗮ.projection K ⋯) x‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x : E
⊢ ‖(K.projection Kᗮ ⋯) x‖ ≤ ‖x‖

Tactic:
by
  conv_rhs => rw [← projection_add_projection_eq_self K.isCompl_orthogonal x]
  simp [← sq_le_sq₀ (norm_nonneg _), sq, mul_nonneg,
    norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ (K.mem_orthogonal _ |>.mp _ _ _)]

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

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
    ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal + (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^
      (1 / p.toReal)

Tactic:
by
          gcongr <;> apply edist_triangle

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

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f h ≤ edist f g + edist g h

Tactic:
simp only [prod_edist_eq_add (zero_lt_one.trans_le hp)]
      calc
        (edist f.fst h.fst ^ p.toReal + edist f.snd h.snd ^ p.toReal) ^ (1 / p.toReal) ≤
            ((edist f.fst g.fst + edist g.fst h.fst) ^ p.toReal +
              (edist f.snd g.snd + edist g.snd h.snd) ^ p.toReal) ^ (1 / p.toReal) := by
          gcongr <;> apply edist_triangle
        _ ≤
            (edist f.fst g.fst ^ p.toReal + edist f.snd g.snd ^ p.toReal) ^ (1 / p.toReal) +
              (edist g.fst h.fst ^ p.toReal + edist g.snd h.snd ^ p.toReal) ^ (1 / p.toReal) := by
          have := ENNReal.Lp_add_le {0, 1}
            (if · = 0 then edist f.fst g.fst else edist f.snd g.snd)
            (if · = 0 then edist g.fst h.fst else edist g.snd h.snd) hp
          simp only [Finset.mem_singleton, not_false_eq_true, Finset.sum_insert,
            Finset.sum_singleton, reduceCtorEq] at this
          exact this

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
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v

Tactic:
let e := (‖x‖⁻¹ : 𝕜) • x

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
⊢ ∃ u ⊇ v, Orthonormal 𝕜 Subtype.val ∧ u ≠ v
Module: Mathlib.Analysis.Normed.Lp.Matrix

Goal state before:
pp: n : Type u_2
R : Type u_4
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing R
p : ℝ≥0∞
⊢ (toLpLin p p) 1 = LinearMap.id

Tactic:
ext; simp

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

Goal state before:
pp: m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
p q r : ℝ≥0∞
inst✝¹ : Fintype o
inst✝ : DecidableEq o
A : Matrix m n R
B : Matrix n o R
⊢ (toLpLin p r) (A * B) = (toLpLin q r) A ∘ₗ (toLpLin p q) B

Tactic:
ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (map_star U)⁻¹ = transpose U

Tactic:
ext; simp

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

Goal state before:
pp: case mpr
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ ∃ t ∈ Icc 0 1, x = ∑ i, t i • (v.prod w) i

Tactic:
use Sum.elim t s

Goal state after:
case h
ι : 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ Sum.elim t s ∈ Icc 0 1 ∧ x = ∑ i, Sum.elim t s i • (v.prod w) i
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
⊢ μ s = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
u : ℕ → E
hu : Bornology.IsBounded (range u)
hs : Pairwise (Disjoint on fun n ↦ {u n} + s)
h's : MeasurableSet s
H : ∀ (R : ℝ), μ (s ∩ closedBall 0 R) = 0
⊢ μ s ≤ 0
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ↑⊥ = 0

Tactic:
AffineSubspace.bot_coe,

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : ⊥ ≠ ⊤
⊢ μ ∅ = 0
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
⊢ fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x ↦ Set.Ico 0 1

Tactic:
ext; simp

Goal state after: