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

Goal state before:
pp: case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')

Tactic:
[

Goal state after:
case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ n, (|a| + y n + ε') * (μ.real (E n) + ε' / ↑N) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ x, ((|a| + y x + ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')

Tactic:
this

Goal state after:
case calc_5
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
this : ∀ (n : Fin N), (|a| + y n + ε') * μ.real (E n) = (|a| + 2 * ε') * μ.real (E n) + (y n - ε') * μ.real (E n)
⊢ ∑ x, ((|a| + 2 * ε') * μ.real (E x) + (y x - ε') * μ.real (E x) + (|a| + y x + ε') * (ε' / ↑N)) - |a| * μ.real K =
    ∑ n, (y n - ε') * μ.real (E n) + 2 * ε' * μ.real K + ε' / ↑N * ∑ n, (|a| + y n + ε')
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε

Tactic:
[

Goal state after:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
⊢ s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
Module: Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic

Goal state before:
pp: E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ charFunDual (μ ∗ ν) L = charFunDual μ L * charFunDual ν L

Tactic:
[

Goal state after:
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
mE : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
L : StrongDual ℝ E
⊢ charFunDual (μ ∗ ν) L = charFunDual μ L * charFunDual ν L
Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), (μ i) (frontier (s i)) = 0
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), (μ i) (frontier (s' i)) = 0
i : ι
⊢ (μ i) (frontier (s i ∩ s' i)) = 0

Tactic:
[

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → MeasurableSpace (α i)
inst✝³ : (i : ι) → TopologicalSpace (α i)
inst✝² : ∀ (i : ι), SecondCountableTopology (α i)
inst✝¹ : ∀ (i : ι), PseudoMetrizableSpace (α i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t | ∃ s, t = univ.pi s ∧ (∀ (i : ι), MeasurableSet (s i)) ∧ ∀ (i : ι), (μ i) (frontier (s i)) = 0}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), (μ i) (frontier (s i)) = 0
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), (μ i) (frontier (s' i)) = 0
i : ι
⊢ (μ i) (frontier (s i ∩ s' i)) = 0
Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Goal state before:
pp: case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ μ B ≤
      κ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε ∧
    κ B ≤
      μ (thickening (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal B) +
          (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ) +
        ε

Tactic:
rw [← hs_add_r', add_assoc, ← hs_add_r, add_assoc _ _ ε, ← hs_add_r]

Goal state after:
case neg
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
⊢ μ B ≤ κ (thickening (s.toReal + r.toReal) B) + (s + r) ∧ κ B ≤ μ (thickening (s.toReal + r.toReal) B) + (s + r)
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, f x ∂μ
⊢ ∫ (x : X) in ⋃ n, E n, f x ∂μ = ∫ (x : X) in tsupport ⇑f, f x ∂μ

Tactic:
[

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst✝ : LocallyCompactSpace X
f : X →C_c ℝ
μ : Measure X := rieszMeasure Λ
K : Set X := tsupport ⇑f
ε : ℝ
hε : 0 < ε
a b : ℝ
hab : a < b ∧ range ⇑f ⊆ Ioo a b
N : ℕ
hN : 0 < N
ε' : ℝ := (b - a) / ↑N
hε' : 0 < ε' ∧ ε' * (2 * μ.real K + |a| + b + ε') ≤ ε
E : Fin N → Set X
hE :
  tsupport ⇑f = ⋃ j, E j ∧
    univ.PairwiseDisjoint E ∧
      (∀ (n : Fin N), ∀ x ∈ E n, a + ε' * ↑↑n < f x ∧ f x ≤ a + ε' * (↑↑n + 1)) ∧ ∀ (n : Fin N), MeasurableSet (E n)
y : Fin N → ℝ := fun n ↦ a + ε' * (↑↑n + 1)
hE' : ∀ (n : Fin N), μ (E n) ≠ ∞
V : Fin N → Opens X
hV : ∀ (n : Fin N), E n ⊆ ↑(V n) ∧ (∀ x ∈ V n, f x < y n + ε') ∧ μ ↑(V n) ≤ μ (E n) + ENNReal.ofReal (ε' / ↑N)
g : Fin N → X →C_c ℝ
hg :
  (∀ (n : Fin N), tsupport ⇑(g n) ⊆ (V n).carrier) ∧
    EqOn (∑ n, ⇑(g n)) 1 (tsupport f.toFun) ∧
      (∀ (n : Fin N) (x : X), (g n) x ∈ Icc 0 1) ∧ ∀ (n : Fin N), HasCompactSupport ⇑(g n)
h : ∀ (n : Fin N), (y n - ε') * μ.real (E n) ≤ ∫ (x : X) in E n, f x ∂μ
⊢ ∫ (x : X) in ⋃ n, E n, f x ∂μ = ∫ (x : X) in tsupport ⇑f, f x ∂μ
Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real

Goal state before:
pp: case refine_1
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ (Measure.map Subtype.val ν') Kᶜ = 0

Tactic:
Measure.map_apply (by fun_prop) hK.measurableSet.compl

Goal state after:
case refine_1
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : T2Space X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
K : Set X
hK : IsCompact K
h : μ Kᶜ = 0
μ' : Measure ↑K := Measure.comap Subtype.val μ
ν' : Measure ↑K
ν'_reg : ν'.Regular
ν'_fin : IsFiniteMeasure ν'
hν' : ∀ (g : ↑K →ᵇ ℝ), ∫ (x : ↑K), g x ∂μ' = ∫ (x : ↑K), g x ∂ν'
⊢ ν' (Subtype.val ⁻¹' Kᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (DomMulAct.mk (g * g') • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar

Tactic:
[

Goal state after:
G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ (DomMulAct.mk (g * g') • addHaar).addHaarScalarFactor addHaar =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar * (DomMulAct.mk g' • addHaar).addHaarScalarFactor addHaar
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: case e_a
G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ ((DomMulAct.mk g' * DomMulAct.mk g) • addHaar).addHaarScalarFactor (DomMulAct.mk g' • addHaar) =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar

Tactic:
[

Goal state after:
case e_a
G : Type u_1
A : Type u_2
inst✝⁶ : Group G
inst✝⁵ : AddCommGroup A
inst✝⁴ : DistribMulAction G A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalAddGroup A
inst✝¹ : LocallyCompactSpace A
inst✝ : ContinuousConstSMul G A
g✝ : G
this✝ : MeasurableSpace A := borel A
this : BorelSpace A
g g' : G
⊢ ((DomMulAct.mk g' * DomMulAct.mk g) • addHaar).addHaarScalarFactor (DomMulAct.mk g' • addHaar) =
    (DomMulAct.mk g • addHaar).addHaarScalarFactor addHaar
Module: Mathlib.MeasureTheory.Measure.Haar.DistribChar

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝⁹ : Group G
inst✝⁸ : AddCommGroup A
inst✝⁷ : DistribMulAction G A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalAddGroup A
inst✝⁴ : LocallyCompactSpace A
inst✝³ : ContinuousConstSMul G A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
g : G
⊢ (DomMulAct.mk g • μ).addHaarScalarFactor (DomMulAct.mk g • (DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g

Tactic:
[

Goal state after:
G : Type u_1
A : Type u_2
inst✝⁹ : Group G
inst✝⁸ : AddCommGroup A
inst✝⁷ : DistribMulAction G A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : IsTopologicalAddGroup A
inst✝⁴ : LocallyCompactSpace A
inst✝³ : ContinuousConstSMul G A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
g : G
⊢ (DomMulAct.mk g • μ).addHaarScalarFactor (DomMulAct.mk g • (DomMulAct.mk g)⁻¹ • μ) = (distribHaarChar A) g
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA

Tactic:
[

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹³ : Group A
inst✝¹² : Group B
inst✝¹¹ : Group C
inst✝¹⁰ : TopologicalSpace A
inst✝⁹ : TopologicalSpace B
inst✝⁸ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝⁷ : IsTopologicalGroup A
inst✝⁶ : IsTopologicalGroup B
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace A
inst✝³ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝² : NormedSpace ℝ E
inst✝¹ : IsTopologicalGroup C
inst✝ : LocallyCompactSpace B
f : CompactlySupportedContinuousMap B E
this : UniformSpace B := IsTopologicalGroup.rightUniformSpace B
⊢ Continuous fun c ↦ ∫ (a : A), (H.pullback f (Function.invFun (⇑ψ) c)) a ∂μA
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
⊢ (haar.haarScalarFactor μ • μ).haarScalarFactor (map (⇑φ) (haar.haarScalarFactor μ • μ)) =
    μ.haarScalarFactor (map (⇑φ) μ)

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁷ : Group G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
μ : Measure G
inst✝¹ : μ.IsHaarMeasure
inst✝ : μ.Regular
φ : G ≃ₜ* G
smul : haar = haar.haarScalarFactor μ • μ
⊢ (haar.haarScalarFactor μ • μ).haarScalarFactor (map (⇑φ) (haar.haarScalarFactor μ • μ)) =
    μ.haarScalarFactor (map (⇑φ) μ)
Module: Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable ⇑φ
hψ : Measurable ⇑ψ
⊢ haar.haarScalarFactor (map (⇑(ψ.trans φ)) haar) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ

Tactic:
[

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : LocallyCompactSpace G
φ ψ : G ≃ₜ* G
hφ : Measurable ⇑φ
hψ : Measurable ⇑ψ
⊢ haar.haarScalarFactor (map (⇑(ψ.trans φ)) haar) = haar.haarScalarFactor (map (⇑ψ) haar) * mulEquivHaarChar φ
Module: Mathlib.MeasureTheory.Measure.Haar.Extension

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC

Tactic:
[

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
E : Type u_4
inst✝¹⁸ : Group A
inst✝¹⁷ : Group B
inst✝¹⁶ : Group C
inst✝¹⁵ : TopologicalSpace A
inst✝¹⁴ : TopologicalSpace B
inst✝¹³ : TopologicalSpace C
φ : A →* B
ψ : B →* C
H : IsSES φ ψ
inst✝¹² : IsTopologicalGroup A
inst✝¹¹ : IsTopologicalGroup B
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : MeasurableSpace A
inst✝⁸ : BorelSpace A
μA : Measure A
hμA : μA.IsHaarMeasure
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : IsTopologicalGroup C
inst✝⁵ : LocallyCompactSpace B
inst✝⁴ : MeasurableSpace C
inst✝³ : BorelSpace C
μC : Measure C
hμC : μC.IsHaarMeasure
inst✝² : T2Space B
inst✝¹ : MeasurableSpace B
inst✝ : BorelSpace B
b : B
this : (map (fun x ↦ b * x) (H.inducedMeasure μA μC)).Regular
f : CompactlySupportedContinuousMap B ℝ
h : ∀ (x : B), f (b * x) = (f.comp (Homeomorph.mulLeft b).toCocompactMap) x
⊢ ∫ (x : B), f (b * x) ∂H.inducedMeasure μA μC = ∫ (x : B), f x ∂H.inducedMeasure μA μC
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
this : (fun a ↦ ‖Function.uncurry (fun x y ↦ cexp (↑x * ↑y * I)) a‖) = fun x ↦ 1
⊢ Integrable (fun a ↦ ‖Function.uncurry (fun x y ↦ cexp (↑x * ↑y * I)) a‖) ((volume.restrict (Set.Ioc (-r) r)).prod μ)

Tactic:
this

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
this : (fun a ↦ ‖Function.uncurry (fun x y ↦ cexp (↑x * ↑y * I)) a‖) = fun x ↦ 1
⊢ Integrable (fun x ↦ 1) ((volume.restrict (Set.Ioc (-r) r)).prod μ)
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (t : ℝ) in -r..r, charFun μ t = ∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp (↑x * ↑y * I) ∂μ

Tactic:
[

Goal state after:
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
⊢ ∫ (t : ℝ) in -r..r, charFun μ t = ∫ (x : ℝ) in -r..r, ∫ (y : ℝ), cexp (↑x * ↑y * I) ∂μ
Module: Mathlib.MeasureTheory.Measure.IntegralCharFun

Goal state before:
pp: case neg.refine_1
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
x : ℝ
hx : x ∈ Set.uIcc (-r) r
⊢ HasDerivAt (fun x ↦ y * x) y x

Tactic:
[

Goal state after:
case neg.refine_1
μ : Measure ℝ
r : ℝ
inst✝ : IsFiniteMeasure μ
hr : 0 < r
h_int : Integrable (Function.uncurry fun x y ↦ cexp (↑x * ↑y * I)) ((volume.restrict (Set.uIoc (-r) r)).prod μ)
y : ℝ
hy : ¬y = 0
x : ℝ
hx : x ∈ Set.uIcc (-r) r
⊢ HasDerivAt (fun x ↦ y * x) y x