mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Module.RieszLemma

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
⊢ ‖c‖ / R < 1

Tactic:
rw [div_lt_iff₀ Rpos]

Goal state after:
𝕜 : Type u_1
inst✝² : NormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
c : 𝕜
hc : 1 < ‖c‖
R : ℝ
hR : ‖c‖ < R
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
Rpos : 0 < R
⊢ ‖c‖ < 1 * R
Module: Mathlib.Analysis.Normed.Module.RieszLemma

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

Tactic:
ring

Goal state after:
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
i : ι
⊢ ∫⁻ (a : X), ‖f a‖ₑ ∂μ i = ∫⁻ (x : X), ENNReal.ofReal ‖f x‖ ∂μ i

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
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖

Tactic:
· simp_rw [ofReal_norm]

Goal state after:
ι : 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
i : ι
⊢ 0 ≤ᵐ[μ i] fun a ↦ ‖f a‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
c : ℝ
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ 0 = c • 0

Tactic:
smul_zero

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

Goal state before:
pp: case neg
α : 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 T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
c : ℝ
h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T' s = c • T s
f : α → E
hF : CompleteSpace F
hf : ¬Integrable f μ
⊢ 0 = c • 0

Tactic:
smul_zero

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

Goal state before:
pp: case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (∑ i ∈ insert i s, f i) = ∑ i ∈ insert i s, setToFun μ T hT (f i)

Tactic:
simp only [his, Finset.sum_insert, not_false_iff]

Goal state after:
case refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
s✝ : Finset ι
f : ι → α → E
i : ι
s : Finset ι
his : i ∉ s
ih : (∀ i ∈ s, Integrable (f i) μ) → setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i)
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ setToFun μ T hT (f i + ∑ i ∈ s, f i) = setToFun μ T hT (f i) + ∑ i ∈ s, setToFun μ T hT (f i)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
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
hf' : ¬Integrable (c • f) μ
⊢ 0 = c • 0

Tactic:
smul_zero

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
hf' : ¬Integrable (c • f) μ
⊢ 0 = 0
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 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f.linear
⊢ ∃ K, AntilipschitzWith K ⇑f

Tactic:
refine ⟨K, AntilipschitzWith.of_le_mul_dist fun x y ↦ ?_⟩

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 𝕜
PE : Type u_1
PF : Type u_2
inst✝⁴ : MetricSpace PE
inst✝³ : NormedAddTorsor E PE
inst✝² : MetricSpace PF
inst✝¹ : NormedAddTorsor F PF
inst✝ : FiniteDimensional 𝕜 E
f : PE →ᵃ[𝕜] PF
hf : Function.Injective ⇑f
K : ℝ≥0
hK : AntilipschitzWith K ⇑f.linear
x y : PE
⊢ dist x y ≤ ↑K * dist (f x) (f y)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
hF : CompleteSpace F
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ (L1.setToL1 hT) f

Tactic:
exact ContinuousLinearMap.continuous _

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

Goal state before:
pp: case inr
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun i ↦ setToFun μ T hT (fs i)) l (𝓝 (setToFun μ T hT f))

Tactic:
suffices Tendsto (fun i => setToFun μ T hT (F_lp i)) l (𝓝 (setToFun μ T hT f)) by
    refine (tendsto_congr' ?_).mp this
    filter_upwards [hfsi] with i hi
    suffices h_ae_eq : F_lp i =ᵐ[μ] fs i from setToFun_congr_ae hT h_ae_eq
    simp_rw [F_lp, dif_pos hi]
    exact hi.coeFn_toL1

Goal state after:
case inr
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
f : α → E
hf : AEStronglyMeasurable f μ
fs : ι → α → E
l : Filter ι
hfsi : ∀ᶠ (i : ι) in l, Integrable (fs i) μ
hfs : Tendsto (fun i ↦ ∫⁻ (x : α), ‖fs i x - f x‖ₑ ∂μ) l (𝓝 0)
hl : l.NeBot
hfi : Integrable f μ
f_lp : ↥(Lp E 1 μ) := Integrable.toL1 f hfi
F_lp : ι → ↥(Lp E 1 μ) := fun i ↦ if hFi : Integrable (fs i) μ then Integrable.toL1 (fs i) hFi else 0
tendsto_L1 : Tendsto F_lp l (𝓝 f_lp)
⊢ Tendsto (fun i ↦ setToFun μ T hT ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT f))
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ⇑1 = 1

Tactic:
coe_one

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ 1 = 1
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : FiniteDimensional ℝ E
inst✝ : FiniteDimensional ℝ F
f : ℕ → E
g : ℕ → F
h : f =Θ[atTop] g
⊢ f =Θ[cofinite] g

Tactic:
simpa [← Nat.cofinite_eq_atTop] using h

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

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hC : 0 ≤ C
⊢ ‖setToFun μ T hT f‖ ≤ C * ‖Integrable.toL1 f hf‖

Tactic:
by
  by_cases hF : CompleteSpace F; swap
  · simp only [setToFun, hF, ↓reduceDIte, norm_zero]
    positivity
  rw [setToFun_eq hT hf]
  exact L1.norm_setToL1_le_mul_norm hT hC _

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
f : X → E
s t : Set X
μ : Measure X
hst : s =ᵐ[μ] t
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, f x ∂μ

Tactic:
by
  rw [Measure.restrict_congr_set hst]

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
K : Compacts G
h1K : ↑K ⊆ ↑U
h2K : μ.innerContent U ≤ μ K + ↑ε
⊢ μ.innerContent U ≤ μ.outerMeasure ↑K + ↑ε

Tactic:
grw [h2K, μ.le_outerMeasure_compacts K]

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

Goal state before:
pp: case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ C * μ.real s

Tactic:
rw [integral_non_aestronglyMeasurable hfm]

Goal state after:
case neg
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
C : ℝ
hs : μ s < ∞
hC : ∀ᵐ (x : X) ∂μ, x ∈ s → ‖f x‖ ≤ C
hfm : ¬AEStronglyMeasurable f (μ.restrict s)
⊢ ‖0‖ ≤ C * μ.real 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
μ : Measure X
inst✝ : IsFiniteMeasure μ
C : ℝ
hf : ∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C
s : Set X
hs : MeasurableSet s
hf1 : Integrable f μ
⊢ ∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in sᶜ, f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add, add_comm, integral_add_compl hs hf1]

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

Goal state before:
pp: case left.refine_1
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
this : ∀ K ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' V, index K V ≤ {g ∈ s | ((fun x ↦ g * x) ⁻¹' V ∩ K).Nonempty}.card
g₁ : G
a✝ : g₁ ∈ s
g₂ : G
h2g₂ : g₂ ∈ K₁.carrier
g₃ : G
h2g₃ : g₃ ∈ K₂.carrier
h1g₃ : g₁ * g₃ ∈ V
h1g₂ : g₁ * g₂ ∈ V
⊢ (g₁ * g₂)⁻¹⁻¹ ∈ V

Tactic:
simp only [inv_inv, h1g₂]

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

Goal state before:
pp: case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ 0 ≤ᵐ[μ.restrict {x | R < f x}] fun a ↦ f a - R

Tactic:
rw [Pi.zero_def, EventuallyLE, ae_restrict_iff₀]

Goal state after:
case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ ∀ᵐ (x : X) ∂μ, x ∈ {x | R < f x} → 0 ≤ f x - R

case hf
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
R : ℝ
f : X → ℝ
hR : 0 ≤ R
hfint : IntegrableOn f {x | R < f x} μ
hμ : μ {x | R < f x} ≠ 0
this : IntegrableOn (fun x ↦ R) {x | R < f x} μ
⊢ NullMeasurableSet {x | 0 ≤ f x - R} (μ.restrict {x | R < f x})
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case neg
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
hx : ∀ (x : R), ¬IsBot x
⊢ f.measure botSet = 0

Tactic:
simp [botSet, hx]

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
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
hx : x ∈ toMeasurable μ s ↔ x ∈ s
h : x ∈ s → f x ≤ g x
⊢ x ∈ toMeasurable μ s → f x ≤ g x

Tactic:
rwa [hx]

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

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

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring

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

Goal state before:
pp: case inl.hq
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
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
hxy : x ≤ y
hf : ofReal (↑g y - ↑g x) = ofReal (↑f y - ↑f x)
⊢ ↑f x ≤ ↑f y

Tactic:
exact f.mono hxy

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

Goal state before:
pp: case inr.hq
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
g : StieltjesFunction R
y : R
hfg : f.measure = g.measure
hy : ↑f y = ↑g y
x : R
hxy : y ≤ x
hf : ofReal (↑g x - ↑g y) = ofReal (↑f x - ↑f y)
⊢ ↑f y ≤ ↑f x

Tactic:
exact f.mono hxy

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

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

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ↑‖⟪x, y⟫‖ ^ 2 * ↑(normSq x) - ↑(normSq x) * ↑‖⟪x, y⟫‖ ^ 2 - ↑(normSq x) * ↑‖⟪x, y⟫‖ ^ 2 +
      ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) =
    ↑(normSq x) * (↑(normSq x) * ↑(normSq y)) - ↑(normSq x) * ↑‖⟪x, y⟫‖ ^ 2

Tactic:
ring

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
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑(MemLp.toLp ↑↑f ⋯)) p (μ.restrict s)).toReal ≤ (eLpNorm (↑↑f) p μ).toReal

Tactic:
eLpNorm_congr_ae (MemLp.coeFn_toLp _)

Goal state after:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure X
s : Set X
f : ↥(Lp E p μ)
⊢ (eLpNorm (↑↑f) p (μ.restrict s)).toReal ≤ (eLpNorm (↑↑f) p μ).toReal
Module: Mathlib.Analysis.InnerProductSpace.Defs

Goal state before:
pp: case e'_4.e'_5
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ re ⟪x, x⟫ * t ^ 2 * ‖⟪x, y⟫‖ ^ 2 = t ^ 2 * (‖⟪x, y⟫‖ ^ 2 * re ⟪x, x⟫)

Tactic:
ring

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

Goal state before:
pp: case e'_4.e'_6
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
t : ℝ
hzero : ¬⟪x, y⟫ = 0
hzero' : ‖⟪x, y⟫‖ ≠ 0
⊢ ‖⟪x, y⟫‖ ^ 2 * t = t * ‖⟪x, y⟫‖ ^ 2

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) = ‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫ + ⟪y, x⟫ + (⟪x, y⟫ + ⟪y, y⟫) = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ + ⟪x, y⟫_ℝ + ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫ - ⟪y, x⟫ - (⟪x, y⟫ - ⟪y, y⟫) = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫

Tactic:
ring

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
this : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, x⟫_ℝ - ⟪x, y⟫_ℝ - ⟪x, y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ + (⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫) = 2 * (⟪x, x⟫ + ⟪y, y⟫)

Tactic:
ring

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
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
⊢ CauchySeq fun n ↦ ↑(w n)

Tactic:
rw [cauchySeq_iff_le_tendsto_0]

Goal state after:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Module: Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Goal state before:
pp: F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
K : Set F
ne : K.Nonempty
h₁ : IsComplete K
h₂ : Convex ℝ K
u : F
δ : ℝ := ⨅ w, ‖u - ↑w‖
this : Nonempty ↑K := Set.Nonempty.to_subtype ne
zero_le_δ : 0 ≤ δ
δ_le : ∀ (w : ↑K), δ ≤ ‖u - ↑w‖
δ_le' : ∀ w ∈ K, δ ≤ ‖u - w‖
w : ℕ → ↑K
hw : ∀ (n : ℕ), ‖u - ↑(w n)‖ < δ + 1 / (↑n + 1)
norm_tendsto : Tendsto (fun n ↦ ‖u - ↑(w n)‖) atTop (𝓝 δ)
b✝ : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
p q N : ℕ
hp : N ≤ p
hq : N ≤ q
wp : F := ↑(w p)
wq : F := ↑(w q)
a : F := u - wq
b : F := u - wp
half : ℝ := 1 / 2
div : ℝ := 1 / (↑N + 1)
⊢ 4 * ‖u - half • (wq + wp)‖ * ‖u - half • (wq + wp)‖ + ‖wp - wq‖ * ‖wp - wq‖ =
    2 * ‖u - half • (wq + wp)‖ * (2 * ‖u - half • (wq + wp)‖) + ‖wp - wq‖ * ‖wp - wq‖

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖

Tactic:
by
  repeat' rw [← sq (M := ℝ)]
  exact norm_add_sq _ _

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫ = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖)) / 2

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫ = (‖x‖ * ‖x‖ + 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫ + ‖y‖ * ‖y‖)) / 4

Tactic:
ring

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ im ⟪x, y⟫ = (‖x‖ * ‖x‖ - 2 * -im ⟪x, y⟫ + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -im ⟪x, y⟫ + ‖I • y‖ * ‖I • y‖)) / 4

Tactic:
ring

Goal state after: