mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
f : ↥(Lp E 1 μ)
⊢ ∀ (f : ↥(α →₁ₛ[μ] E)), (setToL1SCLM α E μ ⋯) f = (setToL1 hT + setToL1 hT') ↑f

Tactic:
simp [setToL1_eq_setToL1SCLM, setToL1_eq_setToL1SCLM, setToL1SCLM_add_left hT hT']

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
x₀ : E
hx₀ : x₀ ∉ F
h : ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
⊢ x₀ ≠ 0

Tactic:
rintro rfl

Goal state after:
𝕜 : Type u_4
inst✝² : RCLike 𝕜
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
F : Subspace 𝕜 E
hFc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑F
hF : ∃ x, x ∉ F
r : ℝ
hr : r < 1
hx₀ : 0 ∉ F
h : ∀ y ∈ F, r * ‖0‖ ≤ ‖0 - y‖
⊢ False
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✝ : Fintype X
hf : Integrable f μ
⊢ ∫ (x : X), f x ∂μ = ∑ x, μ.real {x} • f x

Tactic:
by
  -- NB: Integrable f does not follow from Fintype, because the measure itself could be non-finite
  rw [← setIntegral_finset .univ, Finset.coe_univ, Measure.restrict_univ]
  simp [Finset.coe_univ, hf]

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

Goal state before:
pp: R : Type u_1
inst✝ : SeminormedAddCommGroup R
⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
by
  convert! LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
  norm_num

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

Goal state before:
pp: s t : Set ℝ≥0
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
Af : ℝ
hAf : s ⊆ closedBall 0 Af
Ag : ℝ
hAg : t ⊆ closedBall 0 Ag
key : IsCompact (closedBall 0 Af ×ˢ closedBall 0 Ag)
a✝ x : ℝ≥0
x_in_s : x ∈ s
y : ℝ≥0
y_in_t : y ∈ t
xy_eq : (fun x1 x2 ↦ x1 * x2) x y = a✝
⊢ a✝ ∈ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag

Tactic:
exact ⟨⟨x, y⟩, by simpa only [Set.mem_prod] using ⟨⟨hAf x_in_s, hAg y_in_t⟩, xy_eq⟩⟩

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

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type w
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : CompleteSpace 𝕜
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)

Tactic:
dist_eq_norm_vsub E,

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
⊢ ‖x -ᵥ y‖ ≤ ↑K * dist (f x) (f y)
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 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖ < (↑K)⁻¹
⊢ ↑(∑ i, ‖g i - f i‖₊) < ↑K⁻¹

Tactic:
push_cast

Goal state after:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖ < (↑K)⁻¹
⊢ ∑ i, ‖g i - f i‖ < (↑K)⁻¹
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case hbc
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : ((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i)).ker = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x ↦ 𝕜) ℕ) fun i ↦ LinearMap.id.smulRight (f i))
this : Tendsto (fun g ↦ ∑ i, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ ≤ ‖v - u‖

Tactic:
exact norm_le_pi_norm (v - u) i

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

Goal state before:
pp: case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
⊢ ε > 0 → ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a f < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑f ⋯) < ε

Tactic:
hε_pos

Goal state after:
case neg
α : Type u_1
G : Type u_5
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hc'0 : ¬c' = 0
f : ↥(Lp G 1 μ)
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ > 0, ∀ (a : ↥(Lp G 1 μ)), dist a f < δ → dist (Integrable.toL1 ↑↑a ⋯) (Integrable.toL1 ↑↑f ⋯) < ε
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: case inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [ENNReal.sub_le_sub_iff_left hle (by simp)]
    gcongr

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

Goal state before:
pp: δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
i' : δ
s : Finset δ
hi' : i' ∉ s
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
hi : i ∉ insert i' s
x : (i : δ) → X i
⊢ i = i' → i ∈ insert i' s

Tactic:
rintro rfl

Goal state after:
δ : Type u_1
X : δ → Type u_3
inst✝² : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝¹ : DecidableEq δ
s✝ : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
i : δ
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
y : X i
s : Finset δ
ih : i ∉ s → ∀ (x : (i : δ) → X i), (∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x ↦ update x i y ∂μ) x
x : (i : δ) → X i
hi' : i ∉ s
hi : i ∉ insert i s
⊢ i ∈ insert i s
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: case hst
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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ AEDisjoint μ (s \ t) t

pp: case ht
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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ NullMeasurableSet t μ

pp: case hfs
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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f (s \ t) μ

pp: case hft
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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f t μ

Tactic:
exacts [disjoint_sdiff_self_left.aedisjoint, ht, hfs.mono_set sdiff_subset, hfs.mono_set hts]

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

Goal state before:
pp: case refine_3
α : 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 : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x ↦ fs x a) s x

Tactic:
filter_upwards [h_cont] with a ha using ha x hx

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

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }

Tactic:
have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩

Goal state after:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  μ.innerContent (⨆ i, { carrier := U i, is_open' := ⋯ }) ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s

Tactic:
rw [ae_iff_measure_eq h_meas', ← iUnion_smul_eq_ofPred_exists]

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
s : Set α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : Countable G
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
h_measure_univ_le : μ univ ≤ ∑' (g : G), μ (g • s)
aedisjoint : Pairwise (AEDisjoint μ on fun g ↦ g • s)
h_meas : ∀ (g : G), NullMeasurableSet (g • s) μ
h_meas' : NullMeasurableSet {a | ∃ g, g • a ∈ s} μ
⊢ μ (⋃ g, g • s) = μ univ
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: 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 ∂μ =
    ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ

Tactic:
rw [← setIntegral_neg_eq_setIntegral_nonpos hfi.1, compl_ofPred]

Goal state after:
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 {a | ¬0 ≤ f a}, f x ∂μ =
    ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x < 0}, f x ∂μ
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
_s : ℕ → Set R
hs : ∀ (i : ℕ), MeasurableSet (_s i)
i : ℕ
⊢ MeasurableSet (_s i)

Tactic:
by
    borelize R
    exact hs i

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
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:
by
      rw [setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)]

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

Goal state before:
pp: case pos
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
a : R
ha : IsBot a
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)

Tactic:
have : leftLim f a = f a := by
      apply leftLim_eq_of_eq_bot
      simp [nhdsLT_eq_bot_iff, ha]

Goal state after:
case pos
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
a : R
ha : IsBot a
this : leftLim (↑f) a = ↑f a
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
a b : G
hab : a ≠ b
x : α
hx : x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
y : α
hy : y ∈ s ∧ ∀ (g : G), g ≠ 1 → y ∉ g • s
hxy : (fun x ↦ b • x) y = (fun x ↦ a • x) x
⊢ x ∈ (a⁻¹ * b) • s

Tactic:
· simpa [mul_smul, ← hxy, mem_inv_smul_set_iff] using hy.1

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

Goal state before:
pp: case pos
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

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:
· apply norm_setIntegral_le_of_norm_le_const_ae hs
    have A : ∀ᵐ x : X ∂μ, x ∈ s → ‖AEStronglyMeasurable.mk f hfm x‖ ≤ C := by
      filter_upwards [hC, hfm.ae_mem_imp_eq_mk] with _ h1 h2 h3
      rw [← h2 h3]
      exact h1 h3
    have B : MeasurableSet {x | ‖hfm.mk f x‖ ≤ C} :=
      hfm.stronglyMeasurable_mk.norm.measurable measurableSet_Iic
    filter_upwards [hfm.ae_eq_mk, (ae_restrict_iff B).2 A] with _ h1 _
    rwa [h1]

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)
⊢ ‖∫ (x : X) in s, f x ∂μ‖ ≤ 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✝¹ : PartialOrder X
x y : X
inst✝ : NullSingletonClass μ
⊢ ∫ (t : X) in Ico x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ

Tactic:
integral_Ico_eq_integral_Ioo

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✝¹ : PartialOrder X
x y : X
inst✝ : NullSingletonClass μ
⊢ ∫ (t : X) in Ioo x y, f t ∂μ = ∫ (t : X) in Ioo x y, f t ∂μ
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 : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this : Nonempty R
val✝ : OrderTop R
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)

Tactic:
have : Ici x = Icc x ⊤ := by simp

Goal state after:
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 : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this✝ : Nonempty R
val✝ : OrderTop R
this : Ici x = Icc x ⊤
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
g : G
V : Set G
hV : (interior V).Nonempty
⊢ index ((fun h ↦ g * h) '' K) V = index K V

Tactic:
refine le_antisymm (mul_left_index_le hK hV g) ?_
  convert! mul_left_index_le (hK.image <| continuous_const_mul g) hV g⁻¹
  rw [image_image]
  simp

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
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) / ↑(index (↑K₀) U) = (↑(index (↑K₁) U) + ↑(index (↑K₂) U)) / ↑(index (↑K₀) U)

Tactic:
refine congr_arg (fun x : ℝ => x / index K₀ U) ?_

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
K₁ K₂ : Compacts G
hU : (interior U).Nonempty
h : Disjoint (K₁.carrier * U⁻¹) (K₂.carrier * U⁻¹)
⊢ ↑(index (↑(K₁ ⊔ K₂)) U) = ↑(index (↑K₁) U) + ↑(index (↑K₂) U)
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
⊢ x = 0 → ⟪x, x⟫ = 0

Tactic:
rintro rfl

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
⊢ ⟪0, 0⟫ = 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
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ x = 0 → normSq x = 0

Tactic:
rintro rfl

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

Tactic:
ofReal_normSq_eq_inner_self

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
⊢ ⟪⟪x, y⟫ • x - ⟪x, x⟫ • y, ⟪x, y⟫ • x - ⟪x, x⟫ • y⟫ = ↑(normSq x * (normSq x * normSq y - ‖⟪x, y⟫‖ ^ 2))
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:
push_cast

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
⊢ ↑‖⟪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
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
⊢ normSq x * (t * t) = normSq (⟪x, y⟫ • x) * (t / ‖⟪x, y⟫‖) * (t / ‖⟪x, y⟫‖)

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
⊢ 2 * ‖⟪x, y⟫‖ * t = 2 * re ⟪⟪x, y⟫ • x, y⟫ * (t / ‖⟪x, y⟫‖)

Tactic:
· field_simp
      rw [normSq, normSq, inner_smul_right, inner_smul_left, ← mul_assoc _ _ ⟪x, x⟫,
        mul_conj]
      rw [← ofReal_pow, re_ofReal_mul]
      ring

Goal state after:
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
⊢ 2 * ‖⟪x, y⟫‖ * t = 2 * re ⟪⟪x, y⟫ • x, y⟫ * (t / ‖⟪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
cd : Core 𝕜 F
x : F
⊢ normSq x = 0 ↔ ⟪x, x⟫ = 0

Tactic:
by simp only [normSq, ext_iff, map_zero, inner_self_im, and_true]

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
⊢ 1 ≤ (haarContent K₀).outerMeasure ↑K₀

Tactic:
rw [Content.outerMeasure_eq_iInf]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
⊢ 1 ≤ ⨅ U, ⨅ (hU : IsOpen[inst✝¹] U), ⨅ (_ : ↑K₀ ⊆ U), (haarContent K₀).innerContent { carrier := U, is_open' := hU }
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 - y‖ * ‖x - y‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
push_cast

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖) / 4 +
      (↑‖x - I • y‖ * ↑‖x - I • y‖ - ↑‖x + I • y‖ * ↑‖x + I • y‖) / 4 * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4
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
⊢ LinearIndependent 𝕜 v

Tactic:
by
  rw [linearIndependent_iff]
  intro l hl
  ext i
  have key : ⟪v i, Finsupp.linearCombination 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]
  simpa only [hv.inner_right_finsupp, inner_zero_right] using! key

Goal state after: