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

Goal state before:
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 μ
g : X → ℝ := fun x ↦ max (f x) 0
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ μ s

Tactic:
apply this.trans

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 μ
g : X → ℝ := ⋯
g_int : Integrable g μ
this : ENNReal.ofReal (∫ (x : X), f x ∂μ) ≤ ENNReal.ofReal (∫ (x : X), g x ∂μ)
⊢ ENNReal.ofReal (∫ (x : X), g x ∂μ) ≤ μ s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
⊢ Continuous[inst✝⁹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ ∫ (y : Y) in s, f x y ∂μ

Tactic:
rw [continuous_iff_continuousAt]

Goal state after:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
⊢ ∀ (x : X), ContinuousAt (fun x ↦ ∫ (y : Y) in s, f x y ∂μ) x
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
g : G
hg : μ (g • K \ K) < μ K
⊢ g ∈ E / E

Tactic:
obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at 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
x : G
hxK : x ∈ K
hgxK : (fun x ↦ g • x) x ∈ K
⊢ g ∈ E / E
Module: Mathlib.Analysis.InnerProductSpace.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2 = (R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2

Tactic:
simp [field, sq, norm_sub_mul_self_real, norm_smul, real_inner_smul_left, inner_smul_right,
          Real.norm_of_nonneg (mul_self_nonneg _), -mul_eq_mul_left_iff]
        ring

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

Goal state before:
pp: case mpr
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ (x ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • x) → ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) = 1

Tactic:
· rintro ⟨hx, ⟨r, ⟨hr, rfl⟩⟩⟩
    exact real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul hx hr

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

Goal state before:
pp: G : Type u_4
inst✝¹ : SeminormedAddCommGroup G
inst✝ : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
⊢ ⟪x, y⟫_ℝ = (f y * (starRingEnd ℂ) (f x)).re

Tactic:
rw [← Complex.inner, f.inner_map_map]

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
x : E
⊢ x = 0 → ∀ u ∈ ⊤, ⟪u, x⟫ = 0

Tactic:
rintro rfl
      simp

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

Goal state before:
pp: case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ

Tactic:
← inner_conj_symm x (T y)

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = (starRingEnd ℂ) ⟪T y, x⟫_ℂ
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ ⟪x, T y⟫ = (⟪x, T x⟫ + ⟪x, T y⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) - (⟪x, T x⟫ - ⟪x, T y⟫ - (⟪T y, x⟫ - ⟪T y, y⟫))) / 4

Tactic:
← inner_conj_symm x (T y)

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
h : I = 0
⊢ (starRingEnd 𝕜) ⟪T y, x⟫ =
    (⟪x, T x⟫ + (starRingEnd 𝕜) ⟪T y, x⟫ + (⟪T y, x⟫ + ⟪T y, y⟫) -
        (⟪x, T x⟫ - (starRingEnd 𝕜) ⟪T y, x⟫ - (⟪T y, x⟫ - ⟪T y, y⟫))) /
      4
Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection

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.starProjection x + K.starProjection x = 2 • x ↔ K.starProjection x = x

Tactic:
← two_smul 𝕜

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
⊢ 2 • K.starProjection x = 2 • x ↔ K.starProjection x = x
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
⊢ Tendsto (fun i ↦ (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection x))

Tactic:
have proj_x : ∀ i, (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y := fun i =>
    (orthogonalProjectionOnto_starProjection_of_le
        ((le_iSup U i).trans (iSup U).le_topologicalClosure) _).symm

Goal state after:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝² : Preorder ι
U : ι → Submodule 𝕜 E
inst✝¹ : ∀ (i : ι), (U i).HasOrthogonalProjection
inst✝ : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection
hU : Monotone U
x : E
h : atTop.NeBot
left✝ : Nonempty ι
right✝ : IsDirectedOrder ι
y : E := (⨆ i, U i).topologicalClosure.starProjection x
proj_x : ∀ (i : ι), (U i).orthogonalProjectionOnto x = (U i).orthogonalProjectionOnto y
⊢ Tendsto (fun i ↦ (U i).starProjection x) atTop (𝓝 ((⨆ i, U i).topologicalClosure.starProjection 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
U V : Submodule 𝕜 E
inst✝¹ : U.HasOrthogonalProjection
inst✝ : V.HasOrthogonalProjection
h : U ⟂ V
⊢ U.subtypeL ∘SL (U.orthogonalProjectionOnto ∘SL V.subtypeL) ∘SL V.orthogonalProjectionOnto = 0

Tactic:
by simp [h.orthogonalProjectionOnto_comp_subtypeL]

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
⊢ ∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖

Tactic:
obtain ⟨C, C0, hC⟩ := exists_approx_preimage_norm_le f surj

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
C : ℝ
C0 : C ≥ 0
hC : ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖
⊢ ∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
f g h : WithLp ∞ (α × β)
⊢ max (edist f.fst h.fst) (edist f.snd h.snd) ≤
    max (edist f.fst g.fst) (edist f.snd g.snd) + max (edist g.fst h.fst) (edist g.snd h.snd)

Tactic:
exact sup_le ((edist_triangle _ g.fst _).trans <| add_le_add le_sup_left le_sup_left)
        ((edist_triangle _ g.snd _).trans <| add_le_add le_sup_right le_sup_right)

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:
gcongr <;> apply edist_triangle

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

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : Fact (1 ≤ ∞)
f g : WithLp ∞ (α × β)
r : ℝ≥0
⊢ edist f g ≤ ↑r ↔ ENNReal.ofReal (dist f g) ≤ ↑r

Tactic:
simp [prod_edist_eq_sup, prod_dist_eq_sup]

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

Goal state before:
pp: case mp.refine_2.inr.inr
𝕜 : 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)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
this : ⟨a, ha⟩ ≠ ⟨b, hb⟩
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

Tactic:
exact hv.2 this

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
simp only [Exists, FinVec.exists_iff, exists_iff]

Goal state after:
α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ (∃ r A, P (of (vecCons r A))) ↔ ∃ x, P x
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e.symm

Tactic:
rw [continuous_def]

Goal state after:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
⊢ ∀ (s : Set E),
    IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s →
      IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑e.symm ⁻¹' s)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_le_iff hp0,
        NNReal.mul_rpow, ← NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one,
        Finset.mul_sum]

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
hp✝ : Fact (1 ≤ p)
inst✝⁴ : Fintype ι
inst✝³ : SeminormedRing 𝕜
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → Module 𝕜 (β i)
inst✝ : ∀ (i : ι), IsBoundedSMul 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ∑ i, ‖(c • f).ofLp i‖₊ ^ p.toReal ≤ ∑ i, ‖c‖₊ ^ p.toReal * ‖f.ofLp i‖₊ ^ p.toReal
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (univ.pi fun i ↦ Ioo (a i) (b i))).toReal = ∏ i, (b i - a i)

Tactic:
by
  simp only [volume_pi_Ioo, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
a : ι → ℝ
r : ℝ
hr : 0 < r
⊢ volume (ball a r) = ofReal ((2 * r) ^ Fintype.card ι)

Tactic:
by
  simp only [MeasureTheory.volume_pi_ball a hr, volume_ball, Finset.prod_const]
  exact (ENNReal.ofReal_pow (mul_nonneg zero_le_two hr.le) _).symm

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

Goal state after:
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
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ nndist (single p i b₁) (single p i b₂) = nndist b₁ b₂

Tactic:
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← single_sub, nnnorm_single]

Goal state after:
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
b : Basis ι ℝ E
⊢ b.addHaar.IsAddHaarMeasure

Tactic:
Basis.addHaar

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
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped).IsAddHaarMeasure
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ b.addHaar (_root_.parallelepiped ⇑b) = 1

Tactic:
Basis.addHaar

Goal state after:
ι : Type u_1
E : Type u_3
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ (addHaarMeasure b.parallelepiped) (_root_.parallelepiped ⇑b) = 1
Module: Mathlib.MeasureTheory.Measure.Lebesgue.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
f : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hf : LinearMap.det f ≠ 0
M : Matrix ι ι ℝ := LinearMap.toMatrix' f
A : LinearMap.det f = M.det
⊢ f = toLin' M

Tactic:
simp only [M, toLin'_toMatrix']

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
hf : Measurable f
hg : Measurable g
hs : MeasurableSet s
⊢ (μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ

Tactic:
classical
    rw [Measure.prod_apply]
    · have h :
        (fun x => volume { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) }) =
          s.indicator fun x => ENNReal.ofReal (g x - f x) := by
        funext x
        rw [indicator_apply]
        split_ifs with h
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = Ioo (f x) (g x) := by simp [h, Ioo]
          simp only [hx, Real.volume_Ioo]
        · have hx : { a | x ∈ s ∧ a ∈ Ioo (f x) (g x) } = ∅ := by simp [h]
          simp only [hx, measure_empty]
      dsimp only [regionBetween, preimage_ofPred_eq]
      rw [h, lintegral_indicator] <;> simp only [hs, Pi.sub_apply]
    · exact measurableSet_regionBetween hf hg hs

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝ : Finite ι
⊢ DiscreteTopology ↥(span ℤ (Set.range ⇑b))

Tactic:
by
  have h : Set.MapsTo b.equivFun (span ℤ (Set.range b)) (span ℤ (Set.range (Pi.basisFun ℝ ι))) := by
    intro _ hx
    rwa [SetLike.mem_coe, Basis.mem_span_iff_repr_mem] at hx ⊢
  convert! DiscreteTopology.of_continuous_injective ((continuous_equivFun_basis b).restrict h) ?_
  · exact discreteTopology_pi_basisFun
  · refine Subtype.map_injective _ (Basis.equivFun b).injective

Goal state after:
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
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ μ (closedBall x r) = μ (ball x r)

Tactic:
by_cases! h : r < 0
  · rw [Metric.closedBall_eq_empty.mpr h, Metric.ball_eq_empty.mpr h.le]
  rw [addHaar_closedBall μ x h, addHaar_ball μ x h]

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (span ℤ s).mkQ L)).Finite

Tactic:
rw [show span ℤ s = span ℤ (Set.range b) by simp [b, Basis.coe_mk, Subtype.range_coe_subtype]]

Goal state after:
case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
s : Set E
h_incl : s ⊆ ↑L
h_span : span K s = span K ↑L
h_lind : LinearIndependent K Subtype.val
b : Basis { x // x ∈ s } K E := Basis.mk h_lind ⋯
⊢ (↑(Submodule.map (span ℤ (Set.range ⇑b)).mkQ L)).Finite
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
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] (R * 0))
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)

Tactic:
rw [mul_zero] at B

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
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t u : Set E
h'u : μ u ≠ 0
R : ℝ
Rpos : 0 < R
t_bound : t ⊆ closedBall 0 R
t' : Set E := R⁻¹ • t
ht' : t' = R⁻¹ • t
u' : Set E := R⁻¹ • u
hu' : u' = R⁻¹ • u
A : Tendsto (fun r ↦ μ (s ∩ ({x} + r • t')) / μ ({x} + r • u')) (𝓝[>] 0) (𝓝 0)
B : Tendsto (fun r ↦ R * r) (𝓝[>] 0) (𝓝[>] 0)
⊢ Tendsto (fun r ↦ μ (s ∩ ({x} + r • t)) / μ ({x} + r • u)) (𝓝[>] 0) (𝓝 0)
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'

Tactic:
rcases Hi J hJ this with ⟨Ji, hJi, hlei⟩

Goal state after:
case refine_2
ι : Type u_1
I : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
π' : Prepartition I
H : π' ≤ π
Hi : ∀ J ∈ π, π'.restrict J ≤ πi J
J' : Box ι
hJ' : J' ∈ π'
J : Box ι
hJ : J ∈ π
hle : J' ≤ J
this : J' ∈ π'.restrict J
Ji : Box ι
hJi : Ji ∈ πi J
hlei : J' ≤ Ji
⊢ ∃ I' ∈ π.biUnion πi, J' ≤ I'
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
w : PiLp 2 fun i ↦ ↥(V i)
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this : ∀ (v : ⨁ (i : ι), ↥(V i)), e₂ v = ∑ i, ↑(e₁ v i)
⊢ (hV.isometryL2OfOrthogonalFamily hV').symm w = ∑ i, ↑(w.ofLp i)

Tactic:
exact this (e₁.symm w)

Goal state after: