mathlib-initiative/mathlib-tactics huggingface dataset:
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 ↑↑(F_lp i)) l (𝓝 (setToFun μ T hT ↑↑(Integrable.toL1 f hfi)))

Tactic:
exact ((continuous_setToFun hT).tendsto f_lp).comp tendsto_L1

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

Goal state before:
pp: case hp_ne_zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ ¬p ≤ 0

Tactic:
not_le

Goal state after:
case hp_ne_zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ 0 < p
Module: Mathlib.Topology.ContinuousMap.Bounded.Normed

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ ⇑(-(n.succ • f)) = -((n + 1) • ⇑f)

Tactic:
coe_neg,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
n : ℕ
⊢ -⇑(n.succ • f) = -((n + 1) • ⇑f)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case hp_ne_zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ ¬q ≤ 0

Tactic:
not_le

Goal state after:
case hp_ne_zero
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝ : NormedAddCommGroup E
f g : α → E
p q : ℝ
hpq : p.HolderConjugate q
hf : MemLp f (ENNReal.ofReal p) μ
hg : MemLp g (ENNReal.ofReal q) μ
h_left : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ * ‖g a‖) ∂μ = ∫⁻ (a : α), ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖g x‖ₑ) a ∂μ
h_right_f : ∫⁻ (a : α), ENNReal.ofReal (‖f a‖ ^ p) ∂μ = ∫⁻ (a : α), ‖f a‖ₑ ^ p ∂μ
h_right_g : ∫⁻ (a : α), ENNReal.ofReal (‖g a‖ ^ q) ∂μ = ∫⁻ (a : α), ‖g a‖ₑ ^ q ∂μ
⊢ 0 < q
Module: Mathlib.Topology.ContinuousMap.Compact

Goal state before:
pp: α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖f‖ = ‖⇑f‖

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖f‖ ≤ ‖⇑f‖

case a
α : Type u_1
E : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : SeminormedAddCommGroup E
f : C(α, E)
inst✝ : Fintype α
⊢ ‖⇑f‖ ≤ ‖f‖
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : 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
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ eLpNorm (↑↑g - ↑↑f) 1 μ' ≤ c' * eLpNorm (↑↑g - ↑↑f) 1 μ

Tactic:
refine (eLpNorm_mono_measure (⇑g - ⇑f) hμ'_le).trans_eq ?_

Goal state after:
α : 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
g : ↥(Lp G 1 μ)
hfg : (eLpNorm (↑↑g - ↑↑f) 1 μ).toReal < ε / 2 / c'.toReal
h_int : ∀ (f' : ↥(Lp G 1 μ)), Integrable (↑↑f') μ' :=
  fun f' ↦ Integrable.of_measure_le_smul hc' hμ'_le (L1.integrable_coeFn f')
this : eLpNorm (↑↑(Integrable.toL1 ↑↑g ⋯) - ↑↑(Integrable.toL1 ↑↑f ⋯)) 1 μ' = eLpNorm (↑↑g - ↑↑f) 1 μ'
h_eLpNorm_ne_top : eLpNorm (↑↑g - ↑↑f) 1 μ ≠ ∞
⊢ eLpNorm (↑↑g - ↑↑f) 1 (c' • μ) = c' * eLpNorm (↑↑g - ↑↑f) 1 μ
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: X : Type u_2
inst✝ : PseudoEMetricSpace X
δ : ℝ
δ_pos : 0 < δ
F : Set X
x : X
hxF : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
⊢ 1 ≤ (thickenedIndicator δ_pos F) x

Tactic:
rw [thickenedIndicator_one_of_mem_closure δ_pos F hxF]

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 T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f : α → E
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T' C'
hT'' : DominatedFinMeasAdditive μ'' T'' C''
h : ∀ (s : Set α), MeasurableSet s → (μ + μ') s < ∞ → T'' s = T s + T' s
hf : Integrable f μ
hf' : Integrable f μ'
hμ : μ'' ≤ μ + μ'
hC : 0 ≤ C
hC' : 0 ≤ C'
hC'' : 0 ≤ C''
⊢ setToFun μ'' T'' hT'' f = setToFun μ T hT f + setToFun μ' T' hT' f

Tactic:
have I : DominatedFinMeasAdditive (μ + μ') T C := .add_measure_right _ _ hT hC
  have A : setToFun (μ + μ') T I f = setToFun μ T hT f :=
    setToFun_congr_measure_of_add_right _ _ _ (hf.add_measure hf')
  have I' : DominatedFinMeasAdditive (μ + μ') T' C' := .add_measure_left _ _ hT' hC'
  have A' : setToFun (μ + μ') T' I' f = setToFun μ' T' hT' f :=
    setToFun_congr_measure_of_add_left _ _ _ (hf.add_measure hf')
  have I'' : DominatedFinMeasAdditive (μ + μ') T'' C'' := .of_measure_le hμ hT'' hC''
  have A'' : setToFun (μ + μ') T'' I'' f = setToFun μ'' T'' hT'' f := by
    apply setToFun_congr_measure_of_integrable (c' := 1) (by simp) (by simpa using hμ)
    apply hf.add_measure hf'
  rw [← A, ← A', ← A'']
  apply setToFun_add_left' _ _ _ h

Goal state after:
Module: Mathlib.Topology.MetricSpace.ThickenedIndicator

Goal state before:
pp: α : Type u_1
inst✝² : PseudoEMetricSpace α
β : Type u_2
inst✝¹ : One β
inst✝ : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun δ ↦ (cthickening δ E).mulIndicator f) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))

Tactic:
rw [tendsto_pi_nhds]
  intro x
  rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
  apply tendsto_const_nhds

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

Goal state before:
pp: case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ (∫⋯∫⁻_Finset.image e (insert a✝ s✝), f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)

Tactic:
image_insert,

Goal state after:
case insert
δ : Type u_1
δ' : Type u_2
X : δ → Type u_3
inst✝³ : (i : δ) → MeasurableSpace (X i)
μ : (i : δ) → Measure (X i)
inst✝² : DecidableEq δ
inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)
inst✝ : DecidableEq δ'
e : δ' → δ
he : Injective e
f : ((i : δ') → X (e i)) → ℝ≥0∞
hf : Measurable f
h : Measurable fun x ↦ (fun {x_1} ↦ x) ∘' e
a✝ : δ'
s✝ : Finset δ'
hi : a✝ ∉ s✝
ih :
  ∀ (x : (i : δ) → X i),
    (∫⋯∫⁻_Finset.image e s✝, f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
      (∫⋯∫⁻_s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
x : (i : δ) → X i
⊢ (∫⋯∫⁻_insert (e a✝) (Finset.image e s✝), f ∘ fun x ↦ (fun {x_1} ↦ x) ∘' e ∂μ) x =
    (∫⋯∫⁻_insert a✝ s✝, f ∂(fun {x} ↦ μ) ∘' e) ((fun {x_1} ↦ x) ∘' e)
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 : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
x : β
y : E
⊢ y ∈ (s' n x).range → y ∈ (s n).range

Tactic:
SimpleFunc.mem_range

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
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
x : β
y : E
⊢ y ∈ range ⇑(s' n x) → y ∈ range ⇑(s n)
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono'✝¹ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
sup_disjoint'✝¹ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le'✝¹ : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'✝ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → v K₁ ≤ v K₂
sup_disjoint'✝ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'✝ : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  (fun μ s ↦ ↑(μ.toFun s)) { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    (fun μ s ↦ ↑(μ.toFun s)) { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }
⊢ { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }

Tactic:
congr!

Goal state after:
G : Type w
inst✝ : TopologicalSpace G
μ : Compacts G → ℝ≥0
mono'✝¹ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → μ K₁ ≤ μ K₂
sup_disjoint'✝¹ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → μ (K₁ ⊔ K₂) = μ K₁ + μ K₂
sup_le'✝¹ : ∀ (K₁ K₂ : Compacts G), μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂
v : Compacts G → ℝ≥0
mono'✝ : ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → v K₁ ≤ v K₂
sup_disjoint'✝ : ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → v (K₁ ⊔ K₂) = v K₁ + v K₂
sup_le'✝ : ∀ (K₁ K₂ : Compacts G), v (K₁ ⊔ K₂) ≤ v K₁ + v K₂
h :
  (fun μ s ↦ ↑(μ.toFun s)) { toFun := μ, mono' := mono'✝¹, sup_disjoint' := sup_disjoint'✝¹, sup_le' := sup_le'✝¹ } =
    (fun μ s ↦ ↑(μ.toFun s)) { toFun := v, mono' := mono'✝, sup_disjoint' := sup_disjoint'✝, sup_le' := sup_le'✝ }
⊢ μ = 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
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ ∀ (i : ι), MeasurableSet (s i₀ \ s i)

Tactic:
measurability

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

Goal state before:
pp: case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : μ.innerContent U✝ ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : μ.innerContent U✝ - ↑ε < μ U
⊢ ∃ K, ↑K ⊆ ↑U✝ ∧ μ.innerContent U✝ ≤ μ K + ↑ε

Tactic:
refine ⟨U, h1U, ?_⟩

Goal state after:
case inr
G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U✝ : Opens G
hU : μ.innerContent U✝ ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
h'ε : ↑ε ≠ 0
h : ↑ε < μ.innerContent U✝
U : Compacts G
h1U : ↑U ⊆ ↑U✝
h2U : μ.innerContent U✝ - ↑ε < μ U
⊢ μ.innerContent U✝ ≤ μ U + ↑ε
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✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
h : IsFundamentalDomain G s μ
g g' : G
x : α
⊢ (MulAction.toPerm g)
      ((fun x ↦
          { toFun := fun g' ↦ g⁻¹ * g' * g, invFun := fun g' ↦ g * g' * g⁻¹, left_inv := ⋯, right_inv := ⋯ } g' • x)
        x) =
    (fun x ↦ g' • x) ((MulAction.toPerm g) x)

Tactic:
simp [smul_smul, mul_assoc]

Goal state after:
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✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᵐ[μ] t ∩ s
⊢ Finset.univ.card • μ (t ∩ s) = Nat.card G • μ (t ∩ s)

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
inst✝⁴ : MeasurableSpace α
s : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : Finite G
h : IsFundamentalDomain G s μ
t : Set α
this : Fintype G
ht : ∀ (g : G), g • t ∩ s =ᵐ[μ] t ∩ s
⊢ Finset.univ.card • μ (t ∩ s) = Fintype.card G • μ (t ∩ 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 α
s : Set α
μ : Measure α
inst✝² : MeasurableConstSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
hs : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
hf : ∀ (γ : G) (x : α), f (γ • x) = f x
a : ℝ≥0∞
ha : μ ({x | a < f x} ∩ s) = 0
γ : G
x : α
⊢ γ⁻¹ • x ∈ {x | a < f x} ↔ x ∈ {x | a < f x}

Tactic:
simp only [mem_ofPred_eq, hf γ⁻¹ x]

Goal state after:
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ {a | ¬∃ g, g • a ∈ fundamentalInterior G s} = 0

Tactic:
not_exists,

Goal state after:
G : Type u_1
α : Type u_3
inst✝⁵ : Countable G
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MeasurableSpace α
μ : Measure α
s : Set α
hs : IsFundamentalDomain G s μ
inst✝¹ : MeasurableConstSMul G α
inst✝ : SMulInvariantMeasure G α μ
⊢ μ {a | ∀ (x : G), x • a ∉ fundamentalInterior G s} = 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
t : ℝ
⊢ normSq x * t * t + re (⟪x, y⟫ * ↑t) + re (⟪y, x⟫ * ↑t) + re ⟪y, y⟫ =
    normSq x * t * t + re ⟪x, y⟫ * t + re ⟪y, x⟫ * t + re ⟪y, y⟫

Tactic:
rw [mul_comm ⟪x, y⟫ _,
    RCLike.re_ofReal_mul, mul_comm t _, mul_comm ⟪y, x⟫ _, RCLike.re_ofReal_mul, mul_comm t _]

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

Goal state before:
pp: case pos
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∈ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

pp: case neg
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∉ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x

Tactic:
· simp only [hx, Pi.mul_apply, Set.indicator_of_mem, Pi.smul_apply, smul_eq_mul,
        ← Function.const_def]

Goal state after:
case neg
X : Type u_6
f : X → ℝ
m0 : MeasurableSpace X
μ : Measure X
g : SimpleFunc X ℝ
hf : Integrable f μ
c : ℝ
s : Set X
hs : MeasurableSet s
x : X
hx : x ∉ s
⊢ (s.indicator (const X c) * f) x = s.indicator (c • f) x
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
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ WithSeminorms fun i ↦ p

Tactic:
have : p.ball 0 1 = {v | re (cd.inner v v) < 1} := by
    ext v
    simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_ofPred_eq, p]
    change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1
    conv_lhs => rw [show (1 : ℝ) = √1 by simp]
    rw [sqrt_lt_sqrt_iff]
    exact InnerProductSpace.Core.inner_self_nonneg

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
h : ContinuousAt (fun v ↦ ⟪v, v⟫) 0
h' : IsVonNBounded 𝕜 {v | re ⟪v, v⟫ < 1}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v | re ⟪v, v⟫ < 1}
⊢ WithSeminorms fun i ↦ p
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, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ↑(w n) ↑(w m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
let b := fun n : ℕ => 8 * δ * (1 / (n + 1)) + 4 * (1 / (n + 1)) * (1 / (n + 1))

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 : ℕ → ℝ := fun n ↦ 8 * δ * (1 / (↑n + 1)) + 4 * (1 / (↑n + 1)) * (1 / (↑n + 1))
⊢ ∃ 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.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀) ↑K₀ = 1

Tactic:
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarMeasure K₀) ↑K₀ = 1
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀) ↑K₀ = 1

Tactic:
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group
  simp only [haarMeasure, coe_smul, Pi.smul_apply, smul_eq_mul]
  rw [← K₀.isCompact.measure_closure,
    Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]
  · exact (haarContent_outerMeasure_closure_pos K₀).ne'
  · exact (Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact.closure).ne

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
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀).Regular

Tactic:
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group

Goal state after:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarMeasure K₀).Regular
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : SecondCountableTopology G
K₀ : PositiveCompacts G
⊢ SigmaFinite (haarMeasure K₀)

Tactic:
have : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : BorelSpace G
inst✝ : SecondCountableTopology G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ SigmaFinite (haarMeasure K₀)
Module: Mathlib.Analysis.InnerProductSpace.Orthonormal

Goal state before:
pp: case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
⊢ ‖v i‖ = 1

Tactic:
have h₁ : 0 ≤ ‖v i‖ := norm_nonneg _

Goal state after:
case mpr.left
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝ : DecidableEq ι
v : ι → E
h : ∀ (i j : ι), ⟪v i, v j⟫ = if i = j then 1 else 0
i : ι
h' : ‖v i‖ ^ 2 = 1 ^ 2
h₁ : 0 ≤ ‖v i‖
⊢ ‖v i‖ = 1