mathlib-initiative/mathlib-tactics huggingface dataset:
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 T' T'' : Set α → E →L[ℝ] F
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ∞ → T'' s = T s + T' s
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T'' f = setToSimpleFunc T f + setToSimpleFunc T' f

Tactic:
simp_rw [setToSimpleFunc_eq_sum_filter]
  suffices ∀ x ∈ {x ∈ f.range | x ≠ 0}, T'' (f ⁻¹' {x}) = T (f ⁻¹' {x}) + T' (f ⁻¹' {x}) by
    rw [← sum_add_distrib]
    refine Finset.sum_congr rfl fun x hx => ?_
    rw [this x hx]
    push_cast
    rw [Pi.add_apply]
  intro x hx
  refine
    h_add (f ⁻¹' {x}) (measurableSet_preimage _ _) (measure_preimage_lt_top_of_integrable _ hf ?_)
  rw [mem_filter] at hx
  exact hx.2

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(α →₁ₛ[μ] ℝ)
⊢ ⇑(toSimpleFunc (negPart f)) =ᵐ[μ] ⇑(toSimpleFunc f).negPart

Tactic:
rw [SimpleFunc.negPart, MeasureTheory.SimpleFunc.negPart]
  filter_upwards [posPart_toSimpleFunc (-f), neg_toSimpleFunc f]
  intro a h₁ h₂
  rw [h₁]
  change max _ _ = max _ _
  rw [h₂]
  simp

Goal state after:
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 g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
⊢ setToSimpleFunc T (f - g) = setToSimpleFunc T f - setToSimpleFunc T g

Tactic:
by
  rw [sub_eq_add_neg, setToSimpleFunc_add T h_add hf, setToSimpleFunc_neg T h_add hg,
    sub_eq_add_neg]
  rw [integrable_iff] at hg ⊢
  intro x hx_ne
  rw [SimpleFunc.coe_neg, Pi.neg_def, ← Function.comp_def, preimage_comp, neg_preimage,
    Set.neg_singleton]
  refine hg (-x) ?_
  simp [hx_ne]

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

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous integral

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous fun x ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖

pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] ℝ)), integral ↑a = ‖Lp.posPart ↑a‖ - ‖Lp.negPart ↑a‖

Tactic:
· simp only [integral]
    exact cont _

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous fun x ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖

case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ ∀ (a : ↥(α →₁ₛ[μ] ℝ)), integral ↑a = ‖Lp.posPart ↑a‖ - ‖Lp.negPart ↑a‖
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, v t ≤ 0
⊢ ∀ᶠ (x : α) in l, u x ≤ 0

Tactic:
by
  obtain ⟨φ, hφ, h_eq⟩ := h.exists_pos_eq_mul
  exact (hφ.and (hv.and h_eq)).mono (fun x ⟨hφ, hv, h_eq⟩ ↦
    h_eq ▸ mul_nonpos_of_nonneg_of_nonpos hφ.le 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
x y z : P
⊢ ‖x -ᵥ y - (x -ᵥ z)‖ = dist y z

Tactic:
vsub_sub_vsub_cancel_left,

Goal state after:
V : Type u_2
P : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor V P
x y z : P
⊢ ‖z -ᵥ y‖ = dist y z
Module: Mathlib.Analysis.Normed.Affine.Isometry

Goal state before:
pp: V : Type u_2
P : Type u_10
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedSpace ℝ V
x y : P
⊢ dist ((pointReflection ℝ x) y) y = 2 * dist x y

Tactic:
dist_pointReflection_self,

Goal state after:
V : Type u_2
P : Type u_10
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NormedSpace ℝ V
x y : P
⊢ ‖2‖ * dist x y = 2 * dist x y
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✝ : ℝ≥0
⊢ a✝ ∈ s * t → a✝ ∈ (fun p ↦ p.1 * p.2) '' closedBall 0 Af ×ˢ closedBall 0 Ag

Tactic:
⟨x, x_in_s, y, y_in_t, xy_eq⟩

Goal state after:
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
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : 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:
rcases h with ⟨s, ⟨b⟩⟩

Goal state after:
case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun f ↦ LinearMap.det ↑f
Module: Mathlib.Analysis.Normed.Module.FiniteDimension

Goal state before:
pp: case pos
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
E : Type v
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace 𝕜
s : Finset E
b : Basis (↥s) 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ Continuous[_, instTopologicalSpaceMatrix] fun f ↦ (LinearMap.toMatrix b b) ↑f

Tactic:
exact
      ((LinearMap.toMatrix b b).toLinearMap.comp
          (ContinuousLinearMap.coeLM 𝕜)).continuous_of_finiteDimensional

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 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    ⇑(LinearMap.toContinuousLinearMap.symm ≪≫ₗ LinearEquiv.piRing 𝕜 E ι 𝕜).symm

Tactic:
LinearEquiv.trans_symm,

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 𝕜
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ Continuous[Pi.topologicalSpace, topologicalSpace]
    ⇑((LinearEquiv.piRing 𝕜 E ι 𝕜).symm ≪≫ₗ LinearMap.toContinuousLinearMap.symm.symm)
Module: Mathlib.Topology.ContinuousMap.Bounded.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
δ : Type u_2
inst✝¹ : TopologicalSpace δ
inst✝ : DiscreteTopology δ
f : α ↪ δ
g₁ g₂ : α →ᵇ β
h₁ h₂ : δ →ᵇ β
⊢ dist (extend f g₁ h₁) (extend f g₂ h₂) =
    max (dist g₁ g₂) (dist (h₁.domRestrict (range ⇑f)ᶜ) (h₂.domRestrict (range ⇑f)ᶜ))

Tactic:
refine le_antisymm ((dist_le <| le_max_iff.2 <| Or.inl dist_nonneg).2 fun x => ?_) (max_le ?_ ?_)
  · rcases em (∃ y, f y = x) with (⟨x, rfl⟩ | hx)
    · simp only [extend_apply]
      exact (dist_coe_le_dist x).trans (le_max_left _ _)
    · simp only [extend_apply' hx]
      lift x to ((range f)ᶜ : Set δ) using hx
      calc
        dist (h₁ x) (h₂ x) = dist (h₁.domRestrict (range f)ᶜ x) (h₂.domRestrict (range f)ᶜ x) := rfl
        _ ≤ dist (h₁.domRestrict (range f)ᶜ) (h₂.domRestrict (range f)ᶜ) := dist_coe_le_dist x
        _ ≤ _ := le_max_right _ _
  · refine (dist_le dist_nonneg).2 fun x => ?_
    rw [← extend_apply f g₁ h₁, ← extend_apply f g₂ h₂]
    exact dist_coe_le_dist _
  · refine (dist_le dist_nonneg).2 fun x => ?_
    calc
      dist (h₁ x) (h₂ x) = dist (extend f g₁ h₁ x) (extend f g₂ h₂ x) := by
        rw [extend_apply' x.coe_prop, extend_apply' x.coe_prop]
      _ ≤ _ := dist_coe_le_dist _

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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
⊢ Continuous[inst✝¹, _] f ↔
    ∀ (y : E), Continuous[inst✝¹, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ (f x) y

Tactic:
by
  simp_rw [← continuousOn_univ, continuousOn_clm_apply]

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

Goal state before:
pp: F : Type u_1
α : Type u
β : Type v
γ : Type w
𝕜 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : StarRing 𝕜
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SeminormedAddCommGroup β
inst✝³ : StarAddMonoid β
inst✝² : NormedStarGroup β
inst✝¹ : NormedSpace 𝕜 β
inst✝ : StarModule 𝕜 β
f : α →ᵇ β
⊢ ‖star f‖ ≤ ‖f‖

Tactic:
by simp only [norm_eq, star_apply, norm_star, le_of_eq]

Goal state after:
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' • μ) = c' * eLpNorm (↑↑g - ↑↑f) 1 μ

Tactic:
rw [eLpNorm_smul_measure_of_ne_zero hc'0, smul_eq_mul]

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 μ ≠ ∞
⊢ c' ^ (1 / 1).toReal * eLpNorm (↑↑g - ↑↑f) 1 μ = c' * eLpNorm (↑↑g - ↑↑f) 1 μ
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case pos.h_ind
α : 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' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hμ's : μ' s ≠ ∞
⊢ setToFun μ T hT (s.indicator fun x ↦ c) = setToFun μ' T hT' (s.indicator fun x ↦ c)

Tactic:
setToFun_indicator_const hT hs hμs.ne,

Goal state after:
case pos.h_ind
α : 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' : ℝ
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ∞
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f μ
hF : CompleteSpace F
h_int : ∀ (g : α → E), Integrable g μ → Integrable g μ'
c : E
s : Set α
hs : MeasurableSet s
hμs : μ s < ∞
hμ's : μ' s ≠ ∞
⊢ (T s) c = setToFun μ' T hT' (s.indicator fun x ↦ c)
Module: Mathlib.MeasureTheory.Integral.Bochner.Basic

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r

Tactic:
have hposbdd : ∫ ω, max (f ω) 0 ∂μ ≤ μ.real Set.univ • (r : ℝ) := by
    rw [← integral_const]
    refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_
    filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω

Goal state after:
case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ≥0
hfint : Integrable f μ
hfint' : ∫ (a : α), ↑(-f a).toNNReal ∂μ ≤ ∫ (a : α), ↑(f a).toNNReal ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r
hr : ¬r = 0
hμ this : IsFiniteMeasure μ
hposbdd : ∫ (ω : α), max (f ω) 0 ∂μ ≤ μ.real univ • ↑r
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ↑r
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
val✝ : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
this : rightLim f ⊤ = f ⊤
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 b)

Tactic:
rw [tendsto_nhds_unique h (tendsto_pure_nhds f ⊤), ← this]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
val✝ : OrderTop α
h : Tendsto f (pure ⊤) (𝓝 b)
this : rightLim f ⊤ = f ⊤
⊢ Tendsto (rightLim f) (pure ⊤) (𝓝 (rightLim f ⊤))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: f : StieltjesFunction ℝ
x y : ℝ
hy_mem : y ∈ Ioi x
⊢ ↑f x ≤ ↑f y

Tactic:
exact f.mono (le_of_lt hy_mem)

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 : Set X
μ : Measure X
hs : NullMeasurableSet s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by
  rw [← integral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    integral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]

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
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ MeasurableSet (⋂ i ∈ u, s i)

Tactic:
refine u.measurableSet_biInter fun i hi ↦ hs i ?_

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
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
i : ι
hi : i ∈ u
⊢ i ∈ t
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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
⊢ Integrable (⇑(s' n x)) μ

Tactic:
apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable

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 := ⋯
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := ⋯
s' : ℕ → β → SimpleFunc α E := ⋯
f' : ℕ → β → F := ⋯
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, ‖(s' n x) a‖ ≤ ((fun a ↦ ‖f x a‖) + fun a ↦ ‖f x a‖) a
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h3 : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun x ↦ g * x) ⋯ K) = μ K
K : Compacts G
hK : μ K ≠ 0
U : Opens G
hU : (↑U).Nonempty
this✝ : (interior ↑U).Nonempty
s : Finset G
hs : K.carrier ⊆ ⋃ g ∈ s, (fun x ↦ g * x) ⁻¹' ↑U
this : μ K ≤ ↑s.card * μ.innerContent U
⊢ 0 < μ.innerContent U

Tactic:
by
    exact (ENNReal.mul_pos_iff.mp <| hK.bot_lt.trans_le this).2

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 t : Set α
μ : Measure α
inst✝⁴ : MeasurableConstSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
g : G
he : MeasurableEmbedding fun x ↦ g⁻¹ • x
⊢ AEStronglyMeasurable (f ∘ fun x ↦ g⁻¹ • x) (μ.restrict (g • s ∩ t)) ↔ AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
simp only [Function.comp_def, hf]

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 t : Set α
μ : Measure α
inst✝⁴ : MeasurableConstSMul G α
inst✝³ : SMulInvariantMeasure G α μ
inst✝² : Countable G
β : Type u_6
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
hs : IsFundamentalDomain G s μ
ht : IsFundamentalDomain G t μ
f : α → β
hf : ∀ (g : G) (x : α), f (g • x) = f x
⊢ (∀ (g : G), AEStronglyMeasurable f (μ.restrict (g⁻¹ • (g • s ∩ t)))) ↔
    ∀ (g : G), AEStronglyMeasurable f (μ.restrict (g • s ∩ t))

Tactic:
by
      refine forall_congr' fun g => ?_
      have he : MeasurableEmbedding (g⁻¹ • · : α → α) := measurableEmbedding_const_smul _
      rw [← image_smul, ← ((measurePreserving_smul g⁻¹ μ).restrict_image_emb he
        _).aestronglyMeasurable_comp_iff he]
      simp only [Function.comp_def, hf]

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

Goal state before:
pp: G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ∞
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.measure (interior ↑K') ≤ μ K'

Tactic:
μ.measure_apply (IsOpen.measurableSet isOpen_interior)

Goal state after:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : MeasurableSpace G
inst✝¹ : R1Space G
inst✝ : BorelSpace G
H : μ.ContentRegular
K : Compacts G
ε : ℝ≥0
εpos : 0 < ε
a✝ : μ K < ∞
K' : Compacts G
K'_hyp : K.carrier ⊆ interior K'.carrier ∧ μ K' ≤ μ K + ↑ε
⊢ μ.outerMeasure (interior ↑K') ≤ μ K'
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}

Tactic:
rcases compact_covered_by_mul_left_translates hK hV with ⟨t, ht⟩

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ g ∈ t, (fun x ↦ g * x) ⁻¹' V
⊢ ∃ n, n ∈ Finset.card '' {t | K ⊆ ⋃ g ∈ t, (fun h ↦ g * h) ⁻¹' V}
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 α
μ : Measure (Quotient α_mod_G)
i : QuotientMeasureEqMeasurePreimage ν μ
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ (Measure.map (Quotient.mk α_mod_G) (ν.restrict t)) U = ν (Quotient.mk α_mod_G ⁻¹' U ∩ t)

Tactic:
measure_map_restrict_apply ν t meas_U

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
ν : Measure α
μ : Measure (Quotient α_mod_G)
i : QuotientMeasureEqMeasurePreimage ν μ
t : Set α
fund_dom_t : IsFundamentalDomain G t ν
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ ν (Quotient.mk α_mod_G ⁻¹' U ∩ t) = ν (Quotient.mk α_mod_G ⁻¹' U ∩ t)
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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)

Tactic:
obtain ⟨A, hA_meas, hA, hA'⟩ := Measure.toFiniteSpanningSetsIn (h := i)

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 α
i : SigmaFinite ν
i' : HasFundamentalDomain G α ν
μ : Measure (Quotient α_mod_G)
inst✝ : QuotientMeasureEqMeasurePreimage ν μ
A : ℕ → Set α
hA_meas : ∀ (i : ℕ), A i ∈ {s | MeasurableSet s}
hA : ∀ (i : ℕ), ν (A i) < ∞
hA' : ⋃ i, A i = univ
⊢ Nonempty (μ.FiniteSpanningSetsIn univ)
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
x : R
this : Nonempty R
val✝ : OrderBot R
hf : Tendsto (↑f) (pure ⊥) atBot
⊢ f.measure (Iio x) = ∞

Tactic:
simpa using (tendsto_pure_left.1 hf) _ (Iio_mem_atBot (f ⊥))

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

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

Tactic:
rw [← zero_smul 𝕜 (0 : F), inner_smul_left]

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x : F
⊢ (starRingEnd 𝕜) 0 * ⟪0, x⟫ = 0