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

Goal state before:
pp: case refine_1
α : 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✝⁴ : CompleteSpace 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g : { g // 0 ≤ g }
⊢ IsClosed {x | 0 ≤ (setToL1 hT) ↑x}

pp: case refine_2
α : 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✝⁴ : CompleteSpace 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g : { g // 0 ≤ g }
⊢ ∀ (a : { g // 0 ≤ g }), 0 ≤ (setToL1 hT) ↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' a)

Tactic:
· exact (isClosed_Ici (a := 0)).preimage ((setToL1 hT).continuous.comp continuous_induced_dom)

Goal state after:
case refine_2
α : 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✝⁴ : CompleteSpace 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 : ↥(Lp G' 1 μ)
hf : 0 ≤ f
g : { g // 0 ≤ g }
⊢ ∀ (a : { g // 0 ≤ g }), 0 ≤ (setToL1 hT) ↑(coeSimpleFuncNonnegToLpNonneg 1 μ G' a)
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ LinearMap.det ↑f

Tactic:
rw [LinearMap.det]

Goal state after:
case neg
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
h : ¬∃ s, Nonempty (Basis (↥s) 𝕜 E)
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦
    (if H : ∃ s, Nonempty (Basis (↥s) 𝕜 E) then LinearMap.detAux (Trunc.mk ⋯.some) else 1) ↑f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s

Tactic:
have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz

Goal state after:
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * (‖↑A‖₊ * K) ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K

Tactic:
← mul_assoc

Goal state after:
case refine_1
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
LA : LipschitzWith ‖↑A‖₊ ⇑A
L : LipschitzOnWith (‖↑A‖₊ * K) (⇑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (⇑A ∘ f) g s
LAsymm : LipschitzWith ‖↑A.symm‖₊ ⇑A.symm
⊢ ‖↑A.symm‖₊ * ‖↑A‖₊ * K ≤
    (have A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
      max (‖↑A.symm‖₊ * ‖↑A‖₊) 1) *
      K
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist (g₁ x) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)

Tactic:
← extend_apply f g₁ h₁,

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
x : α
⊢ dist ((extend f g₁ h₁) (f x)) (g₂ x) ≤ dist (extend f g₁ h₁) (extend f g₂ h₂)
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁶ : PseudoMetricSpace 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : PseudoMetricSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMul 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : α →ᵇ β
b : ℝ
hb : ∀ (x y : α), dist (f x) (f y) ≤ b
x y : α
⊢ dist ((c • f.toContinuousMap).toFun x) ((c • f.toContinuousMap).toFun y) ≤ dist c 0 * b

Tactic:
by
          refine (dist_smul_pair c (f x) (f y)).trans ?_
          gcongr
          apply hb

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
g : β → E := AEStronglyMeasurable.mk f hfm
A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)
⊢ setToFun μ' T' hT' f = setToFun μ T hT (f ∘ φ)

Tactic:
rw [A, B]

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 C' : ℝ
hT : DominatedFinMeasAdditive μ T C
β : Type u_7
x✝ : MeasurableSpace β
μ' : Measure β
φ : α → β
T' : Set β → E →L[ℝ] F
hT' : DominatedFinMeasAdditive μ' T' C'
f : β → E
hf : Integrable (f ∘ φ) μ
hfm : AEStronglyMeasurable f (Measure.map φ μ)
hφ : Measurable φ
hμ' : μ' ≤ Measure.map φ μ
h : ∀ (s : Set β) (x : E), MeasurableSet s → (T' s) x = (T (φ ⁻¹' s)) x
g : β → E := AEStronglyMeasurable.mk f hfm
A : setToFun μ' T' hT' f = setToFun μ' T' hT' g
B : setToFun μ T hT (f ∘ φ) = setToFun μ T hT (g ∘ φ)
⊢ setToFun μ' T' hT' g = setToFun μ T hT (g ∘ φ)
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
⊢ c' • μ ≤ 0

Tactic:
simp [hc'0]

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

Goal state before:
pp: case insert
δ : 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
⊢ (∫⋯∫⁻_insert i' s, f ∂μ) (update x i y) = (∫⋯∫⁻_insert i' s, f ∘ fun x ↦ update x i y ∂μ) x

Tactic:
| insert i' s hi' ih =>

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = rightLim f x

Tactic:
have A : leftLim f x = f x :=
      hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ leftLim f x = rightLim f x
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.convert_5
α : 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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
⊢ ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ f n a) (∑' (i : ι), f i a)

Tactic:
filter_upwards [hhh] with x hx

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 : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
x : α
hx : Summable fun n ↦ ↑‖f n x‖₊
⊢ HasSum (fun n ↦ f n x) (∑' (i : ι), f i x)
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))

Tactic:
grw [← IH _ (Finset.erase_ssubset is) (c i), ← ENNReal.ofReal_add_le]

Goal state after:
case inr
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ofReal (↑f (d i) - ↑f (c i) + (↑f (c i) - ↑f a))

case a
R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
ab : a ≤ b
i : ℕ
cv : Icc a b ⊆ Iotop (c i) (d i) ∪ ⋃ x ∈ ↑(s.erase i), Iotop (c x) (d x)
is : i ∈ s
bcd : b ∈ Ioc (c i) (d i)
⊢ Icc a (c i) ⊆ ⋃ i_1 ∈ ↑(s.erase i), Iotop (c i_1) (d i_1)
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) μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s

Tactic:
have h_meas' : NullMeasurableSet {a | ∃ g : G, g • a ∈ s} μ := by
        rw [← iUnion_smul_eq_ofPred_exists]; exact .iUnion h_meas

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} μ
⊢ ∀ᵐ (x : α) ∂μ, ∃ g, g • x ∈ s
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
hx : x ∉ {x | 0 ≤ f x}
⊢ f x ≤ 0

Tactic:
Set.notMem_ofPred_iff

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
hx : ¬0 ≤ f x
⊢ f x ≤ 0
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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * (g₁ * g₂) ∈ V
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V

Tactic:
← mul_assoc

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : ↑K ⊆ ⋃ g ∈ s, (fun h ↦ g * h) ⁻¹' ↑K₀
h2s : s.card = index ↑K ↑K₀
t : Finset G
h1t : ↑K₀ ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V
h2t : t.card = index (↑K₀) V
g₁ : G
hg₁ : g₁ ∈ s
g₂ : G
hg₂ : g₁ * g₂ ∈ ↑K₀
g₃ : G
hg₃ : g₃ ∈ t
h2V : g₃ * g₁ * g₂ ∈ V
⊢ g₂ ∈ ⋃ g ∈ t * s, (fun h ↦ g * h) ⁻¹' V
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
K : Compacts G
V : Set G
hV : (interior V).Nonempty
⊢ index (↑K) V ≤ index ↑K ↑K₀ * index (↑K₀) V

Tactic:
by
  classical
  obtain ⟨s, h1s, h2s⟩ := index_elim K.isCompact K₀.interior_nonempty
  obtain ⟨t, h1t, h2t⟩ := index_elim K₀.isCompact hV
  rw [← h2s, ← h2t, mul_comm]
  refine le_trans ?_ Finset.card_mul_le
  apply Nat.sInf_le; refine ⟨_, ?_, rfl⟩; rw [mem_ofPred_eq]; refine Subset.trans h1s ?_
  apply iUnion₂_subset; intro g₁ hg₁; rw [preimage_subset_iff]; intro g₂ hg₂
  have := h1t hg₂
  rcases this with ⟨_, ⟨g₃, rfl⟩, A, ⟨hg₃, rfl⟩, h2V⟩; rw [mem_preimage, ← mul_assoc] at h2V
  exact mem_biUnion (Finset.mul_mem_mul hg₃ hg₁) h2V

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

Tactic:
obtain ⟨b, hb⟩ : ∃ b, b < a := by simpa only [IsBot, not_forall, not_le] using ha

Goal state after:
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
a : R
ha : ¬IsBot a
b : R
hb : b < a
⊢ f.measure {a} = ofReal (↑f a - leftLim (↑f) a)
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:
by
  classical
  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.Group.FundamentalDomain

Goal state before:
pp: case refine_1
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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
⊢ μ (Quotient.mk α_mod_G '' A n) < ∞

Tactic:
have : π ⁻¹' π '' (A n) = _ := MulAction.quotient_preimage_image_eq_union_mul (A n) (G := G)

Goal state after:
case refine_1
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 α
i : SigmaFinite ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), MeasurableSet (A i)
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
n : ℕ
s : Set α
fund_dom_s : IsFundamentalDomain G s ν
this : Quotient.mk α_mod_G ⁻¹' Quotient.mk α_mod_G '' A n = ⋃ g, (fun x ↦ g • x) '' A n
⊢ μ (Quotient.mk α_mod_G '' A n) < ∞
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: case pos
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 ν μ
inst✝ : IsFiniteMeasure μ
hasFun : HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞

pp: case neg
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 ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞

Tactic:
· obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
    have H : μ univ < ∞ := IsFiniteMeasure.measure_univ_lt_top
    rw [h𝓕.projection_respects_measure_apply (μ := μ) MeasurableSet.univ] at H
    simpa [h𝓕.covolume_eq_volume ν] using H

Goal state after:
case neg
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 ν μ
inst✝ : IsFiniteMeasure μ
hasFun : ¬HasFundamentalDomain G α ν
⊢ covolume G α ν < ∞
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
hf : Tendsto (↑f) atBot atBot
x : R
⊢ f.measure (Iio x) = ∞

Tactic:
by
  have : Nonempty R := ⟨x⟩
  cases botOrderOrNoBotOrder R
  · rw [atBot_eq_pure_of_isBot isBot_bot] at hf
    simpa using (tendsto_pure_left.1 hf) _ (Iio_mem_atBot (f ⊥))
  have : NoMinOrder R := NoBotOrder.to_noMinOrder R
  obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
  rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf y]
  exact measure_mono <| Set.Iic_subset_Iio.mpr <| hy

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
K₁ K₂ : Compacts G
⊢ chaar K₀ (K₁ ⊔ K₂) ≤ chaar K₀ K₁ + chaar K₀ K₂

Tactic:
let eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
  have : Continuous eval := by
    exact ((continuous_apply K₁).add (continuous_apply K₂)).sub (continuous_apply (K₁ ⊔ K₂))
  rw [← sub_nonneg]; change chaar K₀ ∈ eval ⁻¹' Ici (0 : ℝ)
  apply mem_of_subset_of_mem _ (chaar_mem_clPrehaar K₀ ⊤)
  unfold clPrehaar; rw [IsClosed.closure_subset_iff]
  · rintro _ ⟨U, ⟨_, h2U, h3U⟩, rfl⟩; simp only [eval, mem_preimage, mem_Ici, sub_nonneg]
    apply prehaar_sup_le; rw [h2U.interior_eq]; exact ⟨1, h3U⟩
  · apply continuous_iff_isClosed.mp this; exact isClosed_Ici

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

Goal state before:
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_notMem, not_false_iff, zero_mul]

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✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
← mul_assoc

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
r : 𝕜
x : F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
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
⊢ p.ball 0 1 = {v | re ⟪v, v⟫ < 1}

Tactic:
ext v

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
v : F
⊢ v ∈ p.ball 0 1 ↔ v ∈ {v | re ⟪v, v⟫ < 1}