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

Goal state before:
pp: case pos
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : g (f a) = 0
⊢ (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)

pp: case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
⊢ (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)

Tactic:
· simp_rw [h0]
    rw [map_zero, Finset.sum_eq_zero fun x hx => ?_]
    rw [mem_filter] at hx
    rw [hx.2, map_zero]

Goal state after:
case neg
α : Type u_1
F : Type u_3
F' : Type u_4
G : Type u_5
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup F'
inst✝¹ : NormedSpace ℝ F'
inst✝ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
T : Set α → F →L[ℝ] F'
h_add : FinMeasAdditive μ T
f : α →ₛ G
hf : Integrable (⇑f) μ
g : G → F
hg : g 0 = 0
T_empty : T ∅ = 0
hfp : ∀ x ∈ f.range, x ≠ 0 → μ (⇑f ⁻¹' {x}) ≠ ∞
a : α
hb : f a ∈ f.range
h0 : ¬g (f a) = 0
⊢ (T (⇑(map g f) ⁻¹' {g (f a)})) (g (f a)) = ∑ j ∈ f.range with g j = g (f a), (T (⇑f ⁻¹' {j})) (g j)
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ setToSimpleFunc (T + T') f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
setToSimpleFunc,

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T T' : Set α → F →L[ℝ] F'
f : α →ₛ F
⊢ ∑ x ∈ f.range, ((T + T') (⇑f ⁻¹' {x})) x = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x + ∑ x ∈ f.range, (T' (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.FinMeasAdditive

Goal state before:
pp: α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
⊢ setToSimpleFunc (fun s ↦ c • T s) f = c • setToSimpleFunc T f

Tactic:
setToSimpleFunc,

Goal state after:
α : Type u_1
F : Type u_3
F' : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace ℝ F'
m : MeasurableSpace α
T : Set α → F →L[ℝ] F'
c : ℝ
f : α →ₛ F
⊢ ∑ x ∈ f.range, (c • T (⇑f ⁻¹' {x})) x = c • ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x
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_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = -setToSimpleFunc T f

Tactic:
setToSimpleFunc,

Goal state after:
α : 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_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = -∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) x
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
⊢ setToFun μ (weightedSMul μ) ⋯ f = 0

Tactic:
exact setToFun_undef (dominatedFinMeasAdditive_weightedSMul μ) h

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

Goal state before:
pp: α : 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''
T T' : Set α → E →L[ℝ] G''
hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → ∀ (x : E), (T s) x ≤ (T' s) x
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T f ≤ setToSimpleFunc T' f

Tactic:
by
  unfold setToSimpleFunc
  gcongr with i _
  by_cases h0 : i = 0
  · simp [h0]
  · exact hTT' _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hf h0) i

Goal state after:
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : Tendsto u l (𝓝 c)
h : ¬c = 0
⊢ Tendsto v l (𝓝 c)

Tactic:
← isEquivalent_const_iff_tendsto h

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝ : NormedAddCommGroup β
u v : α → β
l : Filter α
c : β
huv : u ~[l] v
hu : u ~[l] const α c
h : ¬c = 0
⊢ v ~[l] const α c
Module: Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
u v : α → β
l : Filter α
inst✝ : ClosedIicTopology β
h : u ~[l] v
hv : ∀ᶠ (t : α) in l, 0 < v t
φ : α → β
hφ : ∀ᶠ (x : α) in l, 0 < φ x
h_eq : u =ᶠ[l] φ * v
⊢ ∀ᶠ (x : α) in l, 0 < u x

Tactic:
exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦ h_eq ▸ mul_pos hφ hv)

Goal state after:
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
v : V
x : P
⊢ dist (v +ᵥ x) x = ‖v‖

Tactic:
by
  simp [dist_eq_norm_vsub V _ x]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal + f 0 a) atTop (𝓝 ((F' a).toReal + f 0 a))

Tactic:
refine Filter.Tendsto.add ?_ tendsto_const_nhds

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
f' : ℕ → α → ℝ≥0∞ := fun n a ↦ ENNReal.ofReal (f n a - f 0 a)
F' : α → ℝ≥0∞ := fun a ↦ ENNReal.ofReal (F a - f 0 a)
hf'_int_eq : ∀ (i : ℕ), ∫⁻ (a : α), f' i a ∂μ = ENNReal.ofReal (∫ (a : α), f i a ∂μ - ∫ (a : α), f 0 a ∂μ)
hF'_int_eq : ∫⁻ (a : α), F' a ∂μ = ENNReal.ofReal (∫ (a : α), F a ∂μ - ∫ (a : α), f 0 a ∂μ)
h_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f' i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
h_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
a : α
ha : Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))
ha_mono : Monotone fun i ↦ f i a
ha_bound : ∀ (i : ℕ), f i a ≤ F a
h1 : (fun i ↦ f i a) = fun i ↦ (f' i a).toReal + f 0 a
h2 : F a = (F' a).toReal + f 0 a
⊢ Tendsto (fun i ↦ (f' i a).toReal) atTop (𝓝 (F' a).toReal)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f' i a) atTop (𝓝 (F' a))

Tactic:
refine tendsto_of_integral_tendsto_of_monotone (fun n ↦ (hf_int n).neg) hF_int.neg ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ Tendsto (fun i ↦ ∫ (a : α), f' i a ∂μ) atTop (𝓝 (∫ (a : α), F' a ∂μ))

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f' i a

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ
F : α → ℝ
hf_int : ∀ (n : ℕ), Integrable (f n) μ
hF_int : Integrable F μ
hf_tendsto : Tendsto (fun i ↦ ∫ (a : α), f i a ∂μ) atTop (𝓝 (∫ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
hf_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
f' : ℕ → α → ℝ := fun i a ↦ -f i a
F' : α → ℝ := fun a ↦ -F a
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f' i a ≤ F' a
Module: Mathlib.MeasureTheory.Integral.SetToL1

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

Tactic:
· simp_rw [setToFun_undef _ hfi, le_rfl]

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ⇑(npowRec 0 f) = ⇑f ^ 0

Tactic:
npowRec,

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ⇑1 = ⇑f ^ 0
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
⊢ ⇑(npowRec 0 f) = ⇑f ^ 0

Tactic:
rw [npowRec, pow_zero, coe_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ⇑(npowRec (n + 1) f) = ⇑f ^ (n + 1)

Tactic:
npowRec,

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
R : Type u_1
inst✝ : SeminormedRing R
f : α →ᵇ R
n : ℕ
⊢ ⇑(npowRec n f * f) = ⇑f ^ (n + 1)
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (thickenedIndicator δ_pos E) x ≤ 1

Tactic:
by
  rw [thickenedIndicator.coeFn_eq_comp]
  simpa using (toNNReal_le_toNNReal (by finiteness) one_ne_top).mpr
    (thickenedIndicatorAux_le_one δ E x)

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 δ
f : ((i : δ) → X i) → ℝ≥0∞
x : (i : δ) → X i
⊢ Measurable fun a ↦ f (updateFinset x ∅ a)

Tactic:
exact Subsingleton.measurable

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 t : Finset δ
inst✝ : ∀ (i : δ), SigmaFinite (μ i)
f : ((i : δ) → X i) → ℝ≥0∞
hf : Measurable f
hst : Disjoint s t
x : (i : δ) → X i
e : ((i : ↥s) → X ↑i) × ((i : ↥t) → X ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → X ↑i) := MeasurableEquiv.piFinsetUnion X hst
⊢ (∫⋯∫⁻_s ∪ t, f ∂μ) x = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x

Tactic:
calc (∫⋯∫⁻_s ∪ t, f ∂μ) x
      = ∫⁻ (y : (i : ↥(s ∪ t)) → X i), f (updateFinset x (s ∪ t) y)
          ∂.pi fun i' : ↥(s ∪ t) ↦ μ i' := rfl
    _ = ∫⁻ (y : ((i : s) → X i) × ((j : t) → X j)), f (updateFinset x (s ∪ t) _)
          ∂(Measure.pi fun i : s ↦ μ i).prod (.pi fun j : t ↦ μ j) := by
        rw [measurePreserving_piFinsetUnion hst μ |>.lintegral_map_equiv]
    _ = ∫⁻ (y : (i : s) → X i), ∫⁻ (z : (j : t) → X j), f (updateFinset x (s ∪ t) (e (y, z)))
          ∂.pi fun j : t ↦ μ j ∂.pi fun i : s ↦ μ i := by
        apply lintegral_prod
        apply Measurable.aemeasurable
        exact hf.comp <| measurable_updateFinset.comp e.measurable
    _ = (∫⋯∫⁻_s, ∫⋯∫⁻_t, f ∂μ ∂μ) x := by
        simp_rw [lmarginal, updateFinset_updateFinset hst]
        rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ ContinuousWithinAt (leftLim f) (Iic a) a

Tactic:
by
  have : 𝓝[≤] a = 𝓝[<] a ⊔ pure a := by
    rw [← Iio_union_Icc_eq_Iic le_rfl, nhdsWithin_union]
    simp
  rw [ContinuousWithinAt, this, tendsto_sup]
  simp only [tendsto_pure_nhds, and_true]
  apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2
  rintro s ⟨s_mem, s_closed⟩
  rcases eq_or_neBot (𝓝[<] a) with h' | h'
  · simp [h']
  obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a))
  obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by
    have := (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.1 h s ⟨s_mem, s_closed⟩
    simpa using (mem_nhdsLT_iff_exists_Ioo_subset' hb).1 this
  filter_upwards [Ioo_mem_nhdsLT au] with c hc
  rcases eq_or_neBot (𝓝[<] c) with h'c | h'c
  · simpa [h'c, leftLim_eq_of_eq_bot] using hu hc
  by_cases! h''c : ¬ ∃ y, Tendsto f (𝓝[<] c) (𝓝 y)
  · simpa [leftLim_eq_of_not_tendsto _ h''c] using hu hc
  apply s_closed.mem_of_tendsto (tendsto_leftLim_of_tendsto h''c)
  filter_upwards [Ioo_mem_nhdsLT_of_mem ⟨hc.1, hc.2.le⟩] with d hd using hu hd

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ rightLim (↑f) x = ⨅ r, ↑f ↑r

Tactic:
rw [f.mono.rightLim_eq_sInf, sInf_image']

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
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε

Tactic:
rcases ENNReal.exists_pos_sum_of_countable δpos.ne' ℕ with ⟨ε', ε'0, hε⟩

Goal state after:
R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), f.length (s i) + ↑ε
Module: Mathlib.MeasureTheory.Measure.Content

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

Tactic:
by
  rw [μ.outerMeasure_opens] at hU ⊢
  rcases μ.innerContent_exists_compact hU hε with ⟨K, h1K, h2K⟩
  exact ⟨K, h1K, by grw [h2K, μ.le_outerMeasure_compacts K]⟩

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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := ⋯
hk : MeasurableSet k
⊢ t \ k =ᵐ[μ] s \ k

Tactic:
filter_upwards [h't] with x hx

Goal state after:
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
hx : x ∈ t \ s → f x = 0
⊢ (t \ k) x = (s \ k) 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₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
⊢ index (K₁.carrier ∪ K₂.carrier) V ≤ index K₁.carrier V + index K₂.carrier V

Tactic:
rcases index_elim K₁.2 hV with ⟨s, h1s, h2s⟩
  rcases index_elim K₂.2 hV with ⟨t, h1t, h2t⟩
  rw [← h2s, ← h2t]
  refine le_trans (Nat.sInf_le ⟨_, ?_, rfl⟩) (Finset.card_union_le _ _)
  rw [mem_ofPred_eq, Finset.set_biUnion_union]
  gcongr

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

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (support f) (μ.restrict s)

Tactic:
support_eq_preimage

Goal state after:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᵐ[μ.restrict s] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
ν : Measure α
inst✝² : SMulInvariantMeasure G α ν
inst✝¹ : Countable G
inst✝ : MeasurableConstSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
⊢ QuotientMeasureEqMeasurePreimage ν 0

Tactic:
apply fund_dom_s.quotientMeasureEqMeasurePreimage

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Group G
inst✝⁴ : MulAction G α
inst✝³ : MeasurableSpace α
ν : Measure α
inst✝² : SMulInvariantMeasure G α ν
inst✝¹ : Countable G
inst✝ : MeasurableConstSMul G α
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
vol_s : ν s = 0
⊢ 0 = Measure.map (Quotient.mk α_mod_G) (ν.restrict s)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
ν : Measure α
inst✝³ : SMulInvariantMeasure G α ν
inst✝² : Countable G
inst✝¹ : MeasurableConstSMul G α
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
hasFun : HasFundamentalDomain G α ν
h : covolume G α ν ≠ ∞
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
⊢ ν 𝓕 = covolume G α ν

Tactic:
exact (h𝓕.covolume_eq_volume ν).symm

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : NormedAddCommGroup E
c : InnerProductSpace 𝕜 E
x : E
hx : ⟪x, x⟫_𝕜 = 0
⊢ ‖x‖ ^ 2 = 0

Tactic:
rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero]

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

Goal state before:
pp: case h.refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed[inst✝¹] K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen[inst✝¹] U₁
h1U₂ : IsOpen[inst✝¹] U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen[inst✝¹] V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen[inst✝¹] V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f ↦ f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen[inst✝¹] U
h3U : 1 ∈ U
⊢ K₂.carrier * U⁻¹ ⊆ U₂

Tactic:
refine Subset.trans (mul_subset_mul Subset.rfl ?_) h2L₂
        exact Subset.trans (inv_subset.mpr h1U) inter_subset_right

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‖ ^ 2 = ‖x‖ ^ 2 - 2 * re ⟪x, y⟫ + ‖y‖ ^ 2

Tactic:
exact norm_sub_sq _ _

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

Goal state before:
pp: F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * ⟪v₁ x, w₂ x_1 • v₂ x_1⟫_ℝ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
real_inner_smul_right,

Goal state after:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
ι₁ : Type u_4
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_5
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * ⟪v₁ x, v₂ x_1⟫_ℝ) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
s : Set E
hs : Orthonormal 𝕜 Subtype.val
⊢ ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Tactic:
have := zorn_subset_nonempty { b | Orthonormal 𝕜 (Subtype.val : b → E) } ?_ _ hs
  · obtain ⟨b, hb⟩ := this
    exact ⟨b, hb.1, hb.2.1, fun u hus hu => hb.2.eq_of_ge hu hus⟩
  · refine fun c hc cc _c0 => ⟨⋃₀ c, ?_, ?_⟩
    · exact orthonormal_sUnion_of_directed cc.directedOn fun x xc => hc xc
    · exact fun _ => Set.subset_sUnion_of_mem

Goal state after: