mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

pp: case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t →
        MeasurableSet u →
          (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)

case refine_2
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure ((α × β) × γ)
inst✝ : IsFiniteMeasure μ
h_eq :
  ∀ (ν : Measure ((α × β) × γ)) {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s →
      MeasurableSet t → MeasurableSet u → (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
h :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ ((s ×ˢ t) ×ˢ u) = ν ((s ×ˢ t) ×ˢ u)
s : Set α
t : Set β
u : Set γ
hs : MeasurableSet s
ht : MeasurableSet t
hu : MeasurableSet u
⊢ (map (⇑MeasurableEquiv.prodAssoc) μ) (s ×ˢ t ×ˢ u) = (map (⇑MeasurableEquiv.prodAssoc) ν) (s ×ˢ t ×ˢ u)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ Measurable ↿fun a ↦ f x✝¹.down

pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ Measurable ↿fun a ↦ 1

Tactic:
<;>

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ Measurable ↿fun a ↦ f x✝¹.down

case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
f : ι → X → E
h : ∀ (i : ι), Measurable (f i)
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ Measurable ↿fun a ↦ 1
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ AEMeasurable (f x✝¹.down) μ

pp: case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ AEMeasurable 1 μ

Tactic:
<;>

Goal state after:
case pos
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∈ L.support
⊢ AEMeasurable (f x✝¹.down) μ

case neg
X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
hm : Multipliable (fun i ↦ f i) L
h✝² : L.HasSupport ∧ ((mulSupport fun i ↦ f i) ∩ L.support).Finite
h✝¹ : HasFiniteMulSupport ((L.support.mulIndicator fun i ↦ f i) ∘ PLift.down)
x✝¹ : PLift ι
x✝ : x✝¹ ∈ Finite.toFinset h✝¹
h✝ : x✝¹.down ∉ L.support
⊢ AEMeasurable 1 μ
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case pos.refine_1
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e

pp: case pos.refine_2
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e.symm

Tactic:
<;>

Goal state after:
case pos.refine_1
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e

case pos.refine_2
α✝ : Type u_1
ι : Type u_2
γ : Type u_3
α : Type u_4
β✝ : Type u_5
inst✝⁴ : MeasurableSpace β✝
β : Type u_6
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : StandardBorelSpace α
inst✝ : StandardBorelSpace β
e : α ≃ β
h : Countable α
this : Countable β := Countable.of_equiv α e
⊢ Measurable ⇑e.symm
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K ⊆ K ∪ K'

pp: case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K' ⊆ K ∪ K'

Tactic:
<;>

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K ⊆ K ∪ K'

case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ✝ : Measure α
inst✝² : TopologicalSpace α
μ ν : Measure α
inst✝¹ : μ.InnerRegular
inst✝ : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < μ s + ν s
h : μ s ≠ 0
h' : ν s ≠ 0
u : ℝ≥0∞
hu : u < μ s
v : ℝ≥0∞
hv : v < ν s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < μ K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < ν K'
⊢ K' ⊆ K ∪ K'
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ (μ.withDensity fun x ↦ ENNReal.ofReal (-f x)) Sᶜ = 0

Tactic:
withDensity_apply _ hS.compl,

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Measurable f
S : Set α := {x | f x < 0}
hS : MeasurableSet S
⊢ ∫⁻ (a : α) in Sᶜ, ENNReal.ofReal (-f a) ∂μ = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
⊢ (c • μ).InnerRegularCompactLTTop

Tactic:
by_cases hc : c = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : c = 0
⊢ (c • μ).InnerRegularCompactLTTop

case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
h : μ.InnerRegularCompactLTTop
c : ℝ≥0∞
hc : ¬c = 0
⊢ (c • μ).InnerRegularCompactLTTop
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t✝ : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t✝ ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ ∫⁻ (a : α) in {x | g x = 0}, g a ∂μ = 0

Tactic:
lintegral_eq_zero_iff hg

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t✝ : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t✝ ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ g =ᵐ[μ.restrict {x | g x = 0}] 0
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ 0

pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ ∞

Tactic:
<;>

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ 0

G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s t : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ∞
this : ∀ (s : Set G), ν' s ≠ 0 → ν' s ≠ ∞ → MeasurableSet s → μ' s * ν' t = ν' s * μ' t
hs : ¬MeasurableSet s
s' : Set G
hm : MeasurableSet s'
hμ : μ' s' = μ' s
hν : ν' s' = ν' s
⊢ ν' s' ≠ ∞
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝² : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst✝¹ : SemilatticeSup ι
inst✝ : Nonempty ι
n✝ : ℕ
hfg : μ {a | ¬(a ∈ s → ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (f n a) (g a) < ε)} = 0
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n✝)⁻¹ < edist (f k x) (g x)
N n : ι
hn₁ : n ≥ N
hn₂ : (↑n✝)⁻¹ < edist (f n x) (g x)
⊢ ∃ n ≥ N, (↑n✝)⁻¹ ≤ edist (f n x) (g x)

Tactic:
exact ⟨n, hn₁, hn₂.le⟩

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
hf : Measurable f
a : α
⊢ (dirac a).withDensity f = f a • dirac a

Tactic:
by
  ext s hs
  classical
  simp [withDensity_apply f hs, setLIntegral_dirac' hf hs, dirac_apply' _ hs,
    Set.indicator]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝¹ : α
x✝ : ℕ
⊢ ENNReal.ofReal ‖F x✝ x✝¹‖ = ‖F x✝ x✝¹‖ₑ

pp: case e'_5
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝ : α
⊢ ENNReal.ofReal ‖f x✝‖ = ‖f x✝‖ₑ

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝¹ : α
x✝ : ℕ
⊢ ENNReal.ofReal ‖F x✝ x✝¹‖ = ‖F x✝ x✝¹‖ₑ

case e'_5
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
x✝ : α
⊢ ENNReal.ofReal ‖f x✝‖ = ‖f x✝‖ₑ
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case h₁
x y : ℝ≥0
⊢ x ≤ max x y

pp: case h₂
x y : ℝ≥0
⊢ y ≤ max x y

Tactic:
<;>

Goal state after:
case h₁
x y : ℝ≥0
⊢ x ≤ max x y

case h₂
x y : ℝ≥0
⊢ y ≤ max x y
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case inl
x : ℝ
h✝ : x < 0
⊢ √x ^ 2 = max x 0

pp: case inr.inl
x : ℝ
h✝ : x = 0
⊢ √x ^ 2 = max x 0

pp: case inr.inr
x : ℝ
h✝ : 0 < x
⊢ √x ^ 2 = max x 0

Tactic:
<;>

Goal state after:
case inl
x : ℝ
h✝ : x < 0
⊢ √x ^ 2 = max x 0

case inr.inl
x : ℝ
h✝ : x = 0
⊢ √x ^ 2 = max x 0

case inr.inr
x : ℝ
h✝ : 0 < x
⊢ √x ^ 2 = max x 0
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ √2 < 3 / 2

Tactic:
← sq_lt_sq₀ (by positivity) (by positivity)

Goal state after:
⊢ √2 ^ 2 < (3 / 2) ^ 2
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
h : √x < y
⊢ x < y ^ 2

Tactic:
by
  have hy := x.sqrt_nonneg.trans_lt h
  rwa [← sqrt_lt_sqrt_iff_of_pos (sq_pos_of_pos hy), sqrt_sq hy.le]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: a : ℕ
⊢ ↑a < (↑a.sqrt + 1) ^ 2

pp: a : ℕ
⊢ 0 ≤ ↑a.sqrt + 1

Tactic:
<;>

Goal state after:
a : ℕ
⊢ ↑a < (↑a.sqrt + 1) ^ 2

a : ℕ
⊢ 0 ≤ ↑a.sqrt + 1
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case e'_2
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = ↑(NNReal.sqrtHom (∏ x_1 ∈ s, (toNNReal ∘ x) x_1))

pp: case e'_3
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ ∏ i ∈ s, √(x i) = ↑(∏ x_1 ∈ s, NNReal.sqrtHom ((toNNReal ∘ x) x_1))

Tactic:
<;>

Goal state after:
case e'_2
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ √(∏ i ∈ s, x i) = ↑(NNReal.sqrtHom (∏ x_1 ∈ s, (toNNReal ∘ x) x_1))

case e'_3
ι : Type u_1
s : Finset ι
x : ι → ℝ
hx : ∀ i ∈ s, 0 ≤ x i
⊢ ∏ i ∈ s, √(x i) = ↑(∏ x_1 ∈ s, NNReal.sqrtHom ((toNNReal ∘ x) x_1))
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: case h₁
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ x ^ 2 ≤ m ^ 2

pp: case h₂
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ y ^ 2 ≤ m ^ 2

Tactic:
<;>

Goal state after:
case h₁
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ x ^ 2 ≤ m ^ 2

case h₂
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ y ^ 2 ≤ m ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ m

pp: case hx
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ 2

Tactic:
<;>

Goal state after:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ m

case hx
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ 0 ≤ 2
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).re = (↑p.1 + ↑p.2 * I).re

pp: case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).im = (↑p.1 + ↑p.2 * I).im

Tactic:
<;>

Goal state after:
case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).re = (↑p.1 + ↑p.2 * I).re

case a
p : ℝ × ℝ
⊢ (equivRealProd.symm p).im = (↑p.1 + ↑p.2 * I).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).re = (a✝ + (b✝ + c✝)).re

case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝ + c✝).im = (a✝ + (b✝ + c✝)).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re + b✝.re + c✝.re = a✝.re + (b✝.re + c✝.re)

pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.im + b✝.im + c✝.im = a✝.im + (b✝.im + c✝.im)

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re + b✝.re + c✝.re = a✝.re + (b✝.re + c✝.re)

case a
a✝ b✝ c✝ : ℂ
⊢ a✝.im + b✝.im + c✝.im = a✝.im + (b✝.im + c✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 + a✝).re = a✝.re

pp: case a
a✝ : ℂ
⊢ (0 + a✝).im = a✝.im

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (0 + a✝).re = a✝.re

case a
a✝ : ℂ
⊢ (0 + a✝).im = a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ + 0).re = a✝.re

pp: case a
a✝ : ℂ
⊢ (a✝ + 0).im = a✝.im

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (a✝ + 0).re = a✝.re

case a
a✝ : ℂ
⊢ (a✝ + 0).im = a✝.im
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hf_ne_zero : μ {a | f a = 0} = 0
hμs : μ {a | a ∈ s ∧ ¬f a = 0} = 0
⊢ μ s = 0

Tactic:
have hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0} :=
    fun x hx ↦ or_iff_not_imp_right.mpr <| fun hnx ↦ ⟨hx, hnx⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
s : Set α
hs : MeasurableSet s
hf_ne_zero : μ {a | f a = 0} = 0
hμs : μ {a | a ∈ s ∧ ¬f a = 0} = 0
hle : s ⊆ {a | a ∈ s ∧ ¬f a = 0} ∪ {a | f a = 0}
⊢ μ s = 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
x✝ : ℂ
⊢ (0 • x✝).re = re 0

pp: case a
x✝ : ℂ
⊢ (0 • x✝).im = im 0

Tactic:
<;>

Goal state after:
case a
x✝ : ℂ
⊢ (0 • x✝).re = re 0

case a
x✝ : ℂ
⊢ (0 • x✝).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).re = (n✝ • x✝ + x✝).re

pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).im = (n✝ • x✝ + x✝).im

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).re = (n✝ • x✝ + x✝).re

case a
n✝ : ℕ
x✝ : ℂ
⊢ ((n✝ + 1) • x✝).im = (n✝ • x✝ + x✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.re = ↑n✝ * x✝.re + x✝.re

pp: case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.im = ↑n✝ * x✝.im + x✝.im

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.re = ↑n✝ * x✝.re + x✝.re

case a
n✝ : ℕ
x✝ : ℂ
⊢ (↑n✝ + 1) * x✝.im = ↑n✝ * x✝.im + x✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 • a✝).re = re 0

pp: case a
a✝ : ℂ
⊢ (0 • a✝).im = im 0

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (0 • a✝).re = re 0

case a
a✝ : ℂ
⊢ (0 • a✝).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).re = (↑n✝ • a✝ + a✝).re

pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).re = (↑n✝ • a✝ + a✝).re

case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.re = ↑n✝ * a✝.re + a✝.re

pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.im = ↑n✝ * a✝.im + a✝.im

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.re = ↑n✝ * a✝.re + a✝.re

case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝ + 1) * a✝.im = ↑n✝ * a✝.im + a✝.im