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

Goal state before:
pp: case pos
α : 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 μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)

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 α⦄,
    MeasurableSet s → μ s < ∞ → setToFun μ T hT (s.indicator fun x ↦ c) = setToFun μ' T hT' (s.indicator fun x ↦ c)

case pos.h_add
α : 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 μ'
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f μ →
        Integrable g μ →
          setToFun μ T hT f = setToFun μ' T hT' f →
            setToFun μ T hT g = setToFun μ' T hT' g → setToFun μ T hT (f + g) = setToFun μ' T hT' (f + g)

case pos.h_closed
α : 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 μ'
⊢ IsClosed {f | setToFun μ T hT ↑↑f = setToFun μ' T hT' ↑↑f}

case pos.h_ae
α : 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 μ'
⊢ ∀ ⦃f g : α → E⦄,
    f =ᵐ[μ] g → Integrable f μ → setToFun μ T hT f = setToFun μ' T hT' f → setToFun μ T hT g = setToFun μ' T hT' g
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 < ∞
⊢ setToFun μ T hT (s.indicator fun x ↦ c) = setToFun μ' T hT' (s.indicator fun x ↦ c)

Tactic:
have hμ's : μ' s ≠ ∞ := by
      refine ((hμ'_le s).trans_lt ?_).ne
      rw [Measure.smul_apply, smul_eq_mul]
      exact ENNReal.mul_lt_top hc'.lt_top hμs

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 ≠ ∞
⊢ setToFun μ T hT (s.indicator fun x ↦ c) = setToFun μ' T hT' (s.indicator fun x ↦ c)
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: case neg
α : 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 c' : ℝ≥0∞
hc : c ≠ ∞
hc' : c' ≠ ∞
hμ_le : μ ≤ c • μ'
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hf : ¬Integrable f μ
h_int : ∀ (g : α → E), ¬Integrable g μ → ¬Integrable g μ'
⊢ setToFun μ T hT f = setToFun μ' T hT' f

Tactic:
simp_rw [setToFun_undef _ hf, setToFun_undef _ (h_int f hf)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f a = f a

Tactic:
apply leftLim_eq_of_eq_bot

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
ha : IsBot a
A : TopologicalSpace α := ⋯
this : OrderTopology α
⊢ 𝓝[<] a = ⊥
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
hf : ContinuousWithinAt f (Iic a) a
h' : (𝓝[<] a).NeBot
⊢ Tendsto f (𝓝[<] a) (𝓝 (f a))

Tactic:
exact hf.tendsto.mono_left (nhdsWithin_mono _ Iio_subset_Iic_self)

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ (f '' Iio x).Nonempty

pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ∀ b ∈ f '' Iio x, b ≤ f y

Tactic:
· simp only [image_nonempty]
    exact (forall_mem_nonempty_iff_neBot.2 h') _ self_mem_nhdsWithin

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] x).NeBot
⊢ ∀ b ∈ f '' Iio x, b ≤ f y
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: case inr.inl
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
⊢ f z < u

Tactic:
have : z ∈ Ioo x y := ⟨h''z, hz.2⟩

Goal state after:
case inr.inl
R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
f✝ : StieltjesFunction R
inst✝ : OrderTopology R
f : R → ℝ
hf : Monotone f
x : R
s : Set ℝ
hs : s ∈ 𝓝 (rightLim f x)
l u : ℝ
hlu : rightLim f x ∈ Ioo l u
lus : Ioo l u ⊆ s
y₀ : R
hy₀ : x < y₀
y : R
xy : x < y
h'y : Ioo x y ⊆ f ⁻¹' Ioo l u
z : R
hz : z ∈ Ico x y
h''z : x < z
h'z : 𝓝[>] z = ⊥
this : z ∈ Ioo x y
⊢ f z < u
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 ∈ Iotop (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:
replace bcd : b ∈ Ioc (c i) (d i) := Iotop_subset_Ioc bcd

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)) + ∑ x ∈ s.erase i, ofReal (↑f (d x) - ↑f (c x))
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : 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) < ↑δ
⊢ ContinuousWithinAt (fun r ↦ ↑f r - ↑f a) (Ioi a) a

Tactic:
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const

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) < ↑δ
⊢ ContinuousWithinAt (↑f) (Ioi a) a
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 α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : x ∈ (fun g ↦ g • s) a
hxb : x ∈ (fun g ↦ g • s) b
⊢ False

Tactic:
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb

Goal state after:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
s : Set α
μ : Measure α
h_meas : NullMeasurableSet s μ
h_exists : ∀ (x : α), ∃! g, g • x ∈ s
a b : G
hab : a ≠ b
x : α
hxa : a⁻¹ • x ∈ s
hxb : b⁻¹ • x ∈ s
⊢ False
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 := ⋯
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this✝ : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (fun r ↦ ↑f r - ↑f p) (Ioi q') q'

Tactic:
refine ContinuousWithinAt.sub ?_ continuousWithinAt_const

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) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this✝ : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
A : Icc a' b ∩ s i ⊆ Ioc p q'
htq' : ¬IsTop q'
this : (𝓝[>] q').NeBot
⊢ ContinuousWithinAt (↑f) (Ioi q') q'
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this : ↑U' \ U ⊆ ↑U' \ ↑L'
⊢ μ L' + ⨆ x, μ ↑x ≤ μ.outerMeasure ↑U'

Tactic:
have : Nonempty { M : Compacts G // (M : Set G) ⊆ ↑U' \ closure L } := ⟨⟨⊥, empty_subset _⟩⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
μ : Content G
inst✝¹ : R1Space G
S : MeasurableSpace G
inst✝ : BorelSpace G
U : Set G
hU : U ∈ {s | IsOpen s}
U' : Opens G
this✝¹ : Nonempty { L // ↑L ⊆ ↑U' ∩ U }
L : Compacts G
L' : Compacts G := { carrier := closure ↑L, isCompact' := ⋯ }
hL : ↑L ⊆ ↑U' ∧ ↑L ⊆ U
hL'U : ↑L' ⊆ U
hL'U' : ↑L' ⊆ ↑U'
this✝ : ↑U' \ U ⊆ ↑U' \ ↑L'
this : Nonempty { M // ↑M ⊆ ↑U' \ closure ↑L }
⊢ μ L' + ⨆ x, μ ↑x ≤ μ.outerMeasure ↑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 α μ
inst✝ : Countable G
h : IsFundamentalDomain G s μ
f : α → ℝ≥0∞
t : Set α
⊢ ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫⁻ (x : α) in t ∩ g • s, f x ∂μ

Tactic:
simp only [h.restrict_restrict, inter_comm]

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
⊢ ∑' (g : G), μ (t ∩ s) = Nat.card G • μ (t ∩ s)

Tactic:
tsum_fintype,

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
⊢ ∑ g, μ (t ∩ s) = Nat.card G • μ (t ∩ s)
Module: Mathlib.MeasureTheory.Group.FundamentalDomain

Goal state before:
pp: G : Type u_1
α : Type u_3
E : Type u_5
inst✝⁷ : Group G
inst✝⁶ : MulAction G α
inst✝⁵ : MeasurableSpace α
inst✝⁴ : NormedAddCommGroup E
s : Set α
μ : Measure α
inst✝³ : MeasurableConstSMul G α
inst✝² : SMulInvariantMeasure G α μ
inst✝¹ : Countable G
inst✝ : NormedSpace ℝ E
h : IsFundamentalDomain G s μ
f : α → E
t : Set α
hf : IntegrableOn f t μ
⊢ ∑' (g : G), ∫ (x : α) in g • s, f x ∂μ.restrict t = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ

Tactic:
simp only [h.restrict_restrict, inter_comm]

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✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
a : R
ha : IsBot a
⊢ leftLim (↑f) a = ↑f a

Tactic:
apply leftLim_eq_of_eq_bot

Goal state after:
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
⊢ 𝓝[<] a = ⊥
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
X : Type u_5
m m0 : MeasurableSpace X
μ : Measure X
hm : m ≤ m0
f : X → E
hf_meas : StronglyMeasurable f
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in s, f x ∂μ.trim hm

Tactic:
by
  rwa [integral_trim hm hf_meas, restrict_trim hm μ]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this : Nonempty R
val✝ : OrderTop R
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)

pp: case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this : Nonempty R
val✝ : NoTopOrder R
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)

Tactic:
· have : Ici x = Icc x ⊤ := by simp
    rw [atTop_eq_pure_of_isTop isTop_top] at hf
    rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]

Goal state after:
case inr
R : Type u_1
inst✝⁷ : LinearOrder R
inst✝⁶ : TopologicalSpace R
f : StieltjesFunction R
inst✝⁵ : OrderTopology R
inst✝⁴ : CompactIccSpace R
inst✝³ : MeasurableSpace R
inst✝² : BorelSpace R
inst✝¹ : SecondCountableTopology R
inst✝ : DenselyOrdered R
l : ℝ
hf : Tendsto (↑f) atTop (𝓝 l)
x : R
this : Nonempty R
val✝ : NoTopOrder R
⊢ f.measure (Ici x) = ofReal (l - leftLim (↑f) x)
Module: Mathlib.MeasureTheory.Measure.Haar.Basic

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) / ↑(index (↑K₀) U) ≤ ↑(index (↑K₂) U) / ↑(index (↑K₀) U)

Tactic:
rw [div_le_div_iff_of_pos_right]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ ↑(index (↑K₁) U) ≤ ↑(index (↑K₂) U)

G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
U : Set G
hU : (interior U).Nonempty
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ K₂.carrier
⊢ 0 < ↑(index (↑K₀) U)
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 α ν
𝓕 : Set α
h𝓕 : IsFundamentalDomain G 𝓕 ν
H : ν (Quotient.mk α_mod_G ⁻¹' univ ∩ 𝓕) < ∞
⊢ covolume G α ν < ∞

Tactic:
simpa [h𝓕.covolume_eq_volume ν] using H

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
V : OpenNhdsOf 1
this : ∀ (i : OpenNhdsOf 1), Classical.choose ⋯ ∈ clPrehaar (↑K₀) i
⊢ chaar K₀ ∈ clPrehaar (↑K₀) V

Tactic:
exact this V

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

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x ↦ 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Tactic:
apply lintegral_mono
    apply indicator_le_thickenedIndicatorAux

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

Goal state before:
pp: Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ ∀ᵐ (x_1 : Y) ∂μ, x_1 ∈ s → ‖f x x_1‖ ≤ ?bound x_1

pp: Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ MeasurableSet {x_1 | ‖f x x_1‖ ≤ ?bound x_1}

Tactic:
· filter_upwards with t t_in using hM (mem_image_of_mem _ <| mk_mem_prod x_in t_in)

Goal state after:
Y : Type u_2
E : Type u_3
X : Type u_5
inst✝⁹ : TopologicalSpace X
inst✝⁸ : TopologicalSpace Y
inst✝⁷ : MeasurableSpace Y
inst✝⁶ : OpensMeasurableSpace Y
μ : Measure Y
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FirstCountableTopology X
inst✝² : LocallyCompactSpace X
inst✝¹ : SecondCountableTopologyEither Y E
inst✝ : IsLocallyFiniteMeasure μ
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
s : Set Y
hs : IsCompact s
x₀ : X
U : Set X
U_cpct : IsCompact U
U_nhds : U ∈ 𝓝 x₀
M : ℝ
hM : M ∈ upperBounds ((fun x ↦ ‖uncurry f x‖) '' U ×ˢ s)
x : X
x_in : x ∈ U
⊢ MeasurableSet {x_1 | ‖f x x_1‖ ≤ M}
Module: Mathlib.Analysis.InnerProductSpace.Continuous

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖⟪(x, y).1, (x, y).2⟫‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
rw [one_mul]
        exact norm_inner_le_norm x y

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 * (w₂ x_1 * (‖v₁ x‖ * ‖v₁ x‖ / 2)) +
        ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * (‖v₂ x_1‖ * ‖v₂ x_1‖ / 2)) -
      ∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * (w₂ x_1 * (‖v₁ x - v₂ x_1‖ * ‖v₁ x - v₂ x_1‖ / 2)) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

Tactic:
← Finset.mul_sum,

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₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x‖ * ‖v₁ x‖ / 2) + ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₂ i‖ * ‖v₂ i‖ / 2) -
      ∑ x ∈ s₁, w₁ x * ∑ i ∈ s₂, w₂ i * (‖v₁ x - v₂ i‖ * ‖v₁ x - v₂ i‖ / 2) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2