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

Goal state before:
pp: α : Type u_1
ε' : Type u_4
mα : MeasurableSpace α
inst✝⁴ : PartialOrder α
inst✝³ : MeasurableSingletonClass α
inst✝² : TopologicalSpace ε'
inst✝¹ : ESeminormedAddMonoid ε'
inst✝ : PseudoMetrizableSpace ε'
f : α → ε'
μ : Measure α
a b : α
hb : μ {b} ≠ ∞
hb' : ‖f b‖ₑ ≠ ∞
⊢ IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ

Tactic:
by
  by_cases hab : a ≤ b
  · rw [← Ico_union_right hab, integrableOn_union, eq_true (integrableOn_singleton hb'), and_true]
  · rw [Icc_eq_empty hab, Ico_eq_empty]
    contrapose hab
    exact hab.le

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

Goal state before:
pp: X : Type u_1
ε : Type u_3
inst✝⁴ : MeasurableSpace X
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace ε
inst✝¹ : ContinuousENorm ε
f : X → ε
μ : Measure X
inst✝ : SecondCountableTopology X
hf : LocallyIntegrable f μ
⊢ ∃ u, (∀ (n : ℕ), IsOpen[inst✝³] (u n)) ∧ ⋃ n, u n = univ ∧ ∀ (n : ℕ), IntegrableOn f (u n) μ

Tactic:
rcases (hf.locallyIntegrableOn univ).exists_nat_integrableOn with ⟨u, u_open, u_union, hu⟩
  refine ⟨u, u_open, eq_univ_of_univ_subset u_union, fun n ↦ ?_⟩
  simpa only [inter_univ] using hu n

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

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
Eₗ : Type u_4
F : Type u_5
Fₗ : Type u_6
inst✝¹³ : NormedField 𝕜
inst✝¹² : NormedField 𝕜₂
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : Module 𝕜 E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₂ F
inst✝⁷ : NormedAddCommGroup Eₗ
inst✝⁶ : NormedSpace 𝕜 Eₗ
inst✝⁵ : CompleteSpace Eₗ
inst✝⁴ : NormedAddCommGroup Fₗ
inst✝³ : NormedSpace 𝕜₂ Fₗ
inst✝² : CompleteSpace Fₗ
σ₁₂ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ₁₂
f : E ≃ₛₗ[σ₁₂] F
e₁ : E →ₗ[𝕜] Eₗ
e₂ : F →ₗ[𝕜₂] Fₗ
h_dense₁ : DenseRange ⇑e₁
h_dense₂ : DenseRange ⇑e₂
h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖
h_norm₂ : ∀ (x : F), ‖e₁ (f.symm x)‖ = ‖e₂ x‖
y : E
⊢ ∃ C, ∀ (x : E), ‖(e₂ ∘ₛₗ ↑f) x‖ ≤ C * ‖e₁ x‖

Tactic:
by use 1; simp [h_norm]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
G : Type u_7
inst✝¹ : NormedAddCommGroup G
inst✝ : PartialOrder G
f g : ↥(simpleFunc G p μ)
⊢ ↑↑↑f ≤ᵐ[μ] ↑↑↑g ↔ f ≤ g

Tactic:
by
  rw [← Subtype.coe_le_coe, ← Lp.coeFn_le]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
⊢ map (fun b ↦ max b 0) f - map (fun b ↦ max b 0) (-f) = f

Tactic:
ext a

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α →ₛ ℝ
a : α
⊢ (map (fun b ↦ max b 0) f - map (fun b ↦ max b 0) (-f)) a = f a
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_zero : ∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
h✝ : μ {a | ¬f a = g a} = 0
x y : E
hxy : x ≠ y
z : α
h : f z = x ∧ g z = y
⊢ ¬f z = g z

Tactic:
rwa [h.1, h.2]

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

Goal state before:
pp: α : Type u_1
E : Type u_2
𝕜 : Type u_4
inst✝⁶ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedRing 𝕜
inst✝³ : Module 𝕜 E
inst✝² : IsBoundedSMul 𝕜 E
inst✝¹ : SMulCommClass ℝ 𝕜 E
inst✝ : CompleteSpace E
f : ↥(α →₁ₛ[μ] E)
⊢ (L1.integralCLM' 𝕜) ↑f = integral f

Tactic:
by
  apply ContinuousLinearMap.extend_eq _ _ simpleFunc.isUniformInducing
  exact simpleFunc.denseRange one_ne_top

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

Goal state before:
pp: case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = (T ∅) x

Tactic:
hT_empty

Goal state after:
case inl
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
T : Set α → F →L[ℝ] F'
hT_empty : T ∅ = 0
x : F
m : MeasurableSpace α
h✝ : IsEmpty α
h_univ_empty : Set.univ = ∅
⊢ setToSimpleFunc T (const α x) = 0 x
Module: Mathlib.Analysis.Normed.Group.AddTorsor

Goal state before:
pp: V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y z : P
⊢ dist (x -ᵥ y) (x -ᵥ z) = dist y z

Tactic:
by
  rw [dist_eq_norm, vsub_sub_vsub_cancel_left, dist_comm, dist_eq_norm_vsub V]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
a : α
ha : Monotone fun n ↦ f n a
⊢ ∀ (n : ℕ), 0 ≤ f' n a

Tactic:
n

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
a : α
ha : Monotone fun n ↦ f n a
n : ℕ
⊢ 0 ≤ f' n a
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Monotone fun n ↦ f n x
⊢ Monotone fun n ↦ ENNReal.ofReal (f' n x)

Tactic:
n

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Monotone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
f' : ℕ → α → ℝ := fun n x ↦ f n x - f 0 x
hf'_nonneg : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, 0 ≤ f' i a
hf'_meas : ∀ (n : ℕ), Integrable (f' n) μ
hF_ge : 0 ≤ᵐ[μ] fun x ↦ (F - f 0) x
h_cont : ContinuousAt ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal ((F - f 0) a) ∂μ)
x : α
hx : Monotone fun n ↦ f n x
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → (fun n ↦ ENNReal.ofReal (f' n x)) n ≤ (fun n ↦ ENNReal.ofReal (f' n x)) b
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 g : P →ᴬ[R] Q
h : ↑f = ↑g
⊢ f = g

Tactic:
ext a

Goal state after:
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 g : P →ᴬ[R] Q
h : ↑f = ↑g
a : P
⊢ f a = g a
Module: Mathlib.Topology.Algebra.ContinuousAffineMap

Goal state before:
pp: case refine_1
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
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : f = const R P q
p✝ : P
⊢ ↑f p✝ = (AffineMap.const R P q) p✝

pp: case refine_2
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
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ f x✝ = (const R P q) x✝

Tactic:
· rw [h]; rfl

Goal state after:
case refine_2
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
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddTorsor P
inst✝¹ : TopologicalSpace W
inst✝ : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : f.contLinear = 0 ↔ (↑f).linear = 0
q : Q
h : ↑f = AffineMap.const R P q
x✝ : P
⊢ f x✝ = (const R P q) x✝
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
x : α
hx : Antitone fun n ↦ f n x
⊢ Monotone fun n ↦ -f n x

Tactic:
n

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf : ∀ (n : ℕ), Integrable (f n) μ
hF : Integrable F μ
h_mono : ∀ᵐ (x : α) ∂μ, Antitone fun n ↦ f n x
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))
x : α
hx : Antitone fun n ↦ f n x
n : ℕ
⊢ ∀ ⦃b : ℕ⦄, n ≤ b → (fun n ↦ -f n x) n ≤ (fun n ↦ -f n x) b
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:

Tactic:
r * ‖x - y₀‖ ≤ r' * ‖x - y₀‖ := by gcongr; apply le_max_left
    _ < d := by
      rw [← dist_eq_norm]
      exact (lt_div_iff₀' hlt).1 hxy₀
    _ ≤ dist x (y₀ + y) := Metric.infDist_le_dist_of_mem hy₀y
    _ = ‖x - y₀ - y‖ := by rw [sub_sub, dist_eq_norm]

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

Goal state before:
pp: case isClosed
α : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
G'' : Type u_8
inst✝⁵ : NormedAddCommGroup G''
inst✝⁴ : PartialOrder G''
inst✝³ : IsOrderedAddMonoid G''
inst✝² : NormedSpace ℝ G''
inst✝¹ : CompleteSpace G''
inst✝ : OrderClosedTopology G''
T T' : Set α → E →L[ℝ] G''
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
⊢ IsClosed {f | (setToL1 hT) f ≤ (setToL1 hT') f}

Tactic:
exact isClosed_le (setToL1 hT).continuous (setToL1 hT').continuous

Goal state after:
Module: Mathlib.Topology.Instances.Matrix

Goal state before:
pp: X : Type u_1
n : Type u_5
R : Type u_8
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace R
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : IsTopologicalRing R
A : X → Matrix n n R
hA : Continuous A
⊢ Continuous fun x ↦ (A x).det

Tactic:
simp_rw [Matrix.det_apply]
  refine continuous_finsetSum _ fun l _ => Continuous.const_smul ?_ _
  exact continuous_finsetProd _ fun l _ => hA.matrix_elem _ _

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

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ (∫ (x : X), f x ∂Measure.sum fun i ↦ c i • Measure.dirac (x i)) = ∑' (i : ι), (c i).toReal • f (x i)

Tactic:
rw [integral_sum_measure hf]

Goal state after:
case pos
ι : Type u_1
X : Type u_2
E : Type u_3
inst✝⁴ : Countable ι
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSingletonClass X
x : ι → X
c : ι → ℝ≥0∞
inst✝ : FiniteDimensional ℝ E
hc : ∀ (i : ι), c i ≠ ∞
hf : Integrable f (Measure.sum fun i ↦ c i • Measure.dirac (x i))
⊢ ∑' (i : ι), ∫ (x : X), f x ∂c i • Measure.dirac (x i) = ∑' (i : ι), (c i).toReal • f (x i)
Module: Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Goal state before:
pp: X : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝⁴ : NormedAddCommGroup E
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSingletonClass X
μ : Measure X
inst✝ : Countable X
hf : Integrable f μ
⊢ ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x

Tactic:
by
  rw [← Measure.sum_smul_dirac μ] at hf
  rw [← Measure.sum_smul_dirac μ, integral_sum_measure hf]
  congr 1 with a : 1
  rw [integral_smul_measure, integral_dirac, Measure.sum_smul_dirac, measureReal_def]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
f : α → β
s : Set α
inst✝ : One β
hs : ∀ a ∈ frontier s, f a = 1
hf : Continuous[inst✝², inst✝¹] f
⊢ Continuous[inst✝², inst✝¹] (s.mulIndicator f)

Tactic:
exact hf.piecewise hs continuous_const

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

Goal state before:
pp: case intro
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
hf : LinearIndependent 𝕜 f
val✝ : Fintype ι
⊢ ∀ᶠ (g : ι → E) in 𝓝 f, LinearIndependent 𝕜 g

Tactic:
simp only [Fintype.linearIndependent_iff'] at hf ⊢
  rcases LinearMap.exists_antilipschitzWith _ hf with ⟨K, K0, hK⟩
  have : Tendsto (fun g : ι → E => ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 <| ∑ i, ‖f i - f i‖) :=
    tendsto_finsetSum _ fun i _ =>
      Tendsto.norm <| ((continuous_apply i).tendsto _).sub tendsto_const_nhds
  simp only [sub_self, norm_zero, Finset.sum_const_zero] at this
  refine (this.eventually (gt_mem_nhds <| inv_pos.2 K0)).mono fun g hg => ?_
  replace hg : ∑ i, ‖g i - f i‖₊ < K⁻¹ := by
    rw [← NNReal.coe_lt_coe]
    push_cast
    exact hg
  rw [LinearMap.ker_eq_bot]
  refine (hK.add_sub_lipschitzWith (LipschitzWith.of_dist_le_mul fun v u => ?_) hg).injective
  simp only [dist_eq_norm, LinearMap.lsum_apply, Pi.sub_apply, LinearMap.sum_apply,
    LinearMap.comp_apply, LinearMap.proj_apply, LinearMap.smulRight_apply, LinearMap.id_apply, ←
    Finset.sum_sub_distrib, ← smul_sub, ← sub_smul, NNReal.coe_sum, coe_nnnorm, Finset.sum_mul]
  refine norm_sum_le_of_le _ fun i _ => ?_
  rw [norm_smul, mul_comm]
  gcongr
  exact norm_le_pi_norm (v - u) i

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
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
h : ∀ (x : E), x ∈ F
⊢ FiniteDimensional 𝕜 E

Tactic:
have : (⊤ : Submodule 𝕜 E) = F := by
      ext x
      simp [h]

Goal state after:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
s : Finset E
F : Submodule 𝕜 E := Submodule.span 𝕜 ↑s
hF : F.FG
this✝ : FiniteDimensional 𝕜 ↥F
Fclosed : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
h : ∀ (x : E), x ∈ F
this : ⊤ = F
⊢ FiniteDimensional 𝕜 E
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), f x ∂μ = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x

Tactic:
simp_rw [← f.coe_toLargerSpace_eq hm]

Goal state after:
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
β : Type u_6
m m0 : MeasurableSpace β
μ : Measure β
hm : m ≤ m0
f : β →ₛ F
hf_int : Integrable (⇑f) μ
⊢ ∫ (x : β), (SimpleFunc.toLargerSpace hm f) x ∂μ = ∑ x ∈ f.range, μ.real (⇑(SimpleFunc.toLargerSpace hm f) ⁻¹' {x}) • x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hr : r = 0
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ 0
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
exact le_antisymm (integral_nonpos_of_ae hf) hfint'

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ∀ b ∈ f '' Iio x, b ≤ f y

Tactic:
simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
    intro z hz
    exact hf (hz.le.trans h)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length (t ∩ Ioi c) + f.length (t \ Ioi c) ≤ ofReal (↑f b - ↑f a)

Tactic:
← length_sdiff_botSet,

Goal state after:
R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
c : R
t : Set R
this : Nonempty R
a b : R
h : t \ botSet ⊆ Ioc a b
⊢ f.length ((t ∩ Ioi c) \ botSet) + f.length (t \ Ioi c) ≤ ofReal (↑f b - ↑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
f : X → E
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
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.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
hr : ∃ i, ∃ (h : IsOpen i) (_ : A ⊆ i), μ.innerContent { carrier := i, is_open' := ⋯ } < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r

Tactic:
rcases hr with ⟨U, hUo, hAU, hr⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
A : Set G
hA : MeasurableSet A
r : ℝ≥0∞
U : Set G
hUo : IsOpen U
hAU : A ⊆ U
hr : μ.innerContent { carrier := U, is_open' := ⋯ } < r
⊢ ∃ U ⊇ A, IsOpen U ∧ μ.measure U < r
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ i, ∃ (_ : i ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}), g ∈ (fun h ↦ i * h) ⁻¹' V

Tactic:
use g₀

Goal state after:
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
h : Disjoint (K₁.carrier * V⁻¹) (K₂.carrier * V⁻¹)
s : Finset G
h1s : K₁.carrier ∪ K₂.carrier ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' V
h2s : s.card = index (K₁.carrier ∪ K₂.carrier) V
K : Set G
hK : K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V
g : G
hg : g ∈ K
g₀ : G
h1g₀ : g₀ ∈ s
h2g₀ : g₀ * g ∈ V
⊢ ∃ (_ : g₀ ∈ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}), g ∈ (fun h ↦ g₀ * h) ⁻¹' V
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
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
μ : Measure X
f : X → E
s : Set X
inst✝¹ : ClosedIciTopology E
inst✝ : CompleteSpace E
c : E
hs : MeasurableSet s
hμs : μ s ≠ ∞
hf : ∀ x ∈ s, c ≤ f x
hfint : IntegrableOn (fun x ↦ f x) s μ
⊢ ∫ (x : X) in s, c ∂μ ≤ ∫ (x : X) in s, f x ∂μ

Tactic:
exact setIntegral_mono_on (integrableOn_const hμs) hfint hs hf

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

Goal state before:
pp: case inl
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 u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
h✝ : IsEmpty R
⊢ f.measure univ < ∞

pp: case inr
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 u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
h✝ : Nonempty R
⊢ f.measure univ < ∞

Tactic:
· simp [eq_empty_of_isEmpty]

Goal state after:
case inr
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 u : ℝ
hfl : Tendsto (↑f) atBot (𝓝 l)
hfu : Tendsto (↑f) atTop (𝓝 u)
h✝ : Nonempty R
⊢ f.measure univ < ∞
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
r : 𝕜
⊢ ⟪x, r • y⟫ = r * ⟪x, y⟫

Tactic:
rw [← inner_conj_symm, inner_smul_left]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
r : 𝕜
⊢ (starRingEnd 𝕜) ((starRingEnd 𝕜) r * ⟪y, x⟫) = r * ⟪x, y⟫
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 : ℝ
⊢ ⟪x, ↑t • y⟫ = ⟪x, y⟫ * ↑t

Tactic:
by
  rw [inner_smul_right, mul_comm]

Goal state after: