mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] toPiNat

Tactic:
continuous_iff_continuous_dist

Goal state after:
ι : Type u_2
X : Type u_3
Y : ι → Type u_4
f : (i : ι) → X → Y i
inst✝² : Encodable ι
inst✝¹ : (i : ι) → PseudoMetricSpace (Y i)
inst✝ : TopologicalSpace X
continuous_f : ∀ (i : ι), Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ Continuous[instTopologicalSpaceProd, _] fun x ↦ dist { ofPiNat := x.1 } { ofPiNat := x.2 }
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)

Tactic:
filter_upwards [ihn, eventually_measure_le_doublingConstant_mul μ] with ε hεn hε x

Goal state after:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
C : ℝ≥0 := doublingConstant μ
n : ℕ
ihn : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
ε : ℝ
hεn : ∀ (x : α), μ (closedBall x (2 ^ n * (2 * ε))) ≤ ↑C ^ n * μ (closedBall x (2 * ε))
hε : ∀ (x : α), μ (closedBall x (2 * ε)) ≤ ↑(doublingConstant μ) * μ (closedBall x ε)
x : α
⊢ μ (closedBall x (2 ^ (n + 1) * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ (sum (sfiniteSeq ν)) (Prod.mk x ⁻¹' s)

Tactic:
Measure.sum_apply_of_countable

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
s : Set (α × β)
hs : MeasurableSet s
⊢ Measurable fun x ↦ ∑' (i : ℕ), (sfiniteSeq ν i) (Prod.mk x ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : M), f a ∂(μ ∗ₘ ν) ∗ₘ ρ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
lintegral_mconv (by fun_prop)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ρ ∂μ ∗ₘ ν = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
lintegral_mconv (by fun_prop)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (a : M), f a ∂μ ∗ₘ ν ∗ₘ ρ

Tactic:
lintegral_mconv (by fun_prop)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ

Tactic:
lintegral_mconv (by fun_prop)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : M), ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν ∂μ = ∫⁻ (x : M), ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ ∂μ
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (y : M), f (x * y) ∂ν ∗ₘ ρ

Tactic:
lintegral_mconv (by fun_prop)

Goal state after:
M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
f : M → ℝ≥0∞
hf : Measurable f
x : M
⊢ ∫⁻ (y : M), ∫⁻ (y_1 : M), f (x * y * y_1) ∂ρ ∂ν = ∫⁻ (x_1 : M), ∫⁻ (y : M), f (x * (x_1 * y)) ∂ρ ∂ν
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁴ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst✝ : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x)

Tactic:
nhds_prod_eq

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
inst✝⁵ : MeasurableSpace γ
μ✝ μ' : Measure α
ν✝ ν' : Measure β
τ : Measure γ
inst✝⁴ : SFinite ν✝
X : Type u_4
Y : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
m : MeasurableSpace X
μ : Measure X
inst✝¹ : IsLocallyFiniteMeasure μ
m' : MeasurableSpace Y
ν : Measure Y
inst✝ : IsLocallyFiniteMeasure ν
x : X × Y
⊢ (μ.prod ν).FiniteAtFilter (𝓝 x.1 ×ˢ 𝓝 x.2)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ (μ.prod ν) (s ×ˢ univ) ≤ 0

Tactic:
refine (prod_prod_le _ _).trans_eq ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set α
hs : MeasurableSet s
h2s : μ s = 0
⊢ μ s * ν univ = 0
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ (μ.prod ν) (univ ×ˢ s) ≤ 0

Tactic:
refine (prod_prod_le _ _).trans_eq ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
s : Set β
hs : MeasurableSet s
h2s : ν s = 0
⊢ μ univ * ν s = 0
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case hsc
X : Type u_3
Z : Type u_5
inst✝³ : MeasurableSpace X
inst✝² : StandardBorelSpace X
inst✝¹ : MeasurableSpace Z
inst✝ : CountablySeparated Z
f : X → Z
hf : Measurable f
hsurj : Surjective f
s : Set Z
h : MeasurableSet (f ⁻¹' s)
τ : TopologicalSpace Z
left✝¹ : SecondCountableTopology Z
left✝ : T4Space Z
right✝ : OpensMeasurableSpace Z
⊢ AnalyticSet sᶜ

Tactic:
rw [← image_preimage_eq sᶜ hsurj]
    exact h.compl.analyticSet_image hf

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement S ↑H''
⊢ Nat.card ↑(⇑H.subtype '' S) * Nat.card ↥(map H.subtype H'') = Nat.card ↑S * Nat.card ↑↑H''

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H' H : Subgroup G
h : H' ≤ H
H'' : Subgroup ↥H := comap H.subtype H'
this✝ : H' = map H.subtype H''
S : Set ↥H
cmem : IsComplement (↑H'') S
this : Nat.card ↥H'' * Nat.card ↑S = Nat.card ↥H
⊢ Nat.card ↥(map H.subtype H'') * Nat.card ↑(⇑H.subtype '' S) = Nat.card ↥H'' * Nat.card ↑S

Tactic:
refine congr_arg₂ (· * ·) ?_ ?_ <;>
      exact Nat.card_congr (Equiv.Set.image _ _ <| subtype_injective H).symm

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
⊢ x ∈ range f

Tactic:
have C1 : ∀ n, ∃ (s : b) (_ : IsBounded s.1 ∧ diam s.1 ≤ u n), x ∈ E s := fun n => by
      simpa only [F, mem_iUnion] using mem_iInter.1 hx n

Goal state after:
case h₂
γ : Type u_3
β : Type u_4
inst✝⁵ : TopologicalSpace γ
inst✝⁴ : PolishSpace γ
inst✝³ : TopologicalSpace β
inst✝² : T2Space β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
f : γ → β
f_cont : Continuous[inst✝⁵, inst✝³] f
f_inj : Injective f
this✝ : UpgradedIsCompletelyMetrizableSpace γ := upgradeIsCompletelyMetrizable γ
b : Set (Set γ)
b_count : b.Countable
b_nonempty : ∅ ∉ b
hb : IsTopologicalBasis b
this : Encodable ↑b
A : Type (max 0 u_3) := { p // Disjoint ↑p.1 ↑p.2 }
q : A → Set β
hq1 : ∀ (p : A), f '' ↑(↑p).1 ⊆ q p
hq2 : ∀ (p : A), Disjoint (f '' ↑(↑p).2) (q p)
q_meas : ∀ (p : A), MeasurableSet (q p)
E : ↑b → Set β := fun s ↦ closure[inst✝³] (f '' ↑s) ∩ ⋂ t, ⋂ (ht : Disjoint ↑s ↑t), q ⟨(s, t), ht⟩ \ q ⟨(t, s), ⋯⟩
u : ℕ → ℝ
u_anti : StrictAnti u
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
F : ℕ → Set β := fun n ↦ ⋃ s, ⋃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), E s
x : β
hx : x ∈ ⋂ n, F n
C1 : ∀ (n : ℕ), ∃ s, ∃ (_ : Bornology.IsBounded ↑s ∧ diam ↑s ≤ u n), x ∈ E s
⊢ x ∈ range f
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_3
inst✝² : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U → Bornology.IsBounded U → μ U = ν U
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
f : ℕ → Set α
hm : Monotone f
hu : ⋃ i, f i = U
hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ⨆ i, μ (f i) = ν (⋃ i, f i)

Tactic:
hm.measure_iUnion

Goal state after:
α : Type u_3
inst✝² : PseudoMetricSpace α
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.OuterRegular
inst✝ : ν.OuterRegular
hμν : ∀ (U : Set α), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U → Bornology.IsBounded U → μ U = ν U
U : Set α
hU : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
f : ℕ → Set α
hm : Monotone f
hu : ⋃ i, f i = U
hf : ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
⊢ ⨆ i, μ (f i) = ⨆ i, ν (f i)
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K

Tactic:
rcases hs.exists_isOpen_sdiff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
⊢ ∃ K ⊆ s, p K ∧ μ s - (ε + ε) < μ K
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝²] U
H : μ U ≤ μ s + (r' - μ s)
⊢ μ U < r

Tactic:
add_tsub_cancel_of_le hsr'.le

Goal state after:
α : Type u_1
inst✝³ : MeasurableSpace α
inst✝² : TopologicalSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
H✝ : μ.InnerRegularWRT IsClosed[inst✝²] IsOpen[inst✝²]
hfin : ∀ {s : Set α}, μ s ≠ ∞
this :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ε : ℝ≥0∞), ε ≠ 0 → ∃ F ⊆ s, ∃ U ⊇ s, IsClosed[inst✝²] F ∧ IsOpen[inst✝²] U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r > μ s
r' : ℝ≥0∞
hsr' : μ s < r'
hr'r : r' < r
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝²] U
H : μ U ≤ r'
⊢ μ U < r
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c | ∃ x y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')

Tactic:
apply MeasurableSet.union

Goal state after:
case h₁
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))

case h₂
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := ⋯
hu : u.Countable
t' : Set α := ⋯
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t')
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (map Prod.snd ρ) s = ρ (Prod.snd ⁻¹' s)

Tactic:
Measure.map_apply measurable_snd hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ρ (Prod.snd ⁻¹' s) = ρ (Prod.snd ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: case hcd
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
V : Set G
hV1 : V ∈ 𝓝 1
hVkU : V * k ⊆ U
g : G
hg : g ∈ V
⊢ g • k ⊆ U

Tactic:
exact (smul_set_subset_smul hg).trans hVkU

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

Goal state before:
pp: G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Goal state after:
case inl
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
s : Set G
hs : IsOpen[inst✝⁵] s
inst✝¹ : IsMulLeftInvariant 0
inst✝ : Regular 0
⊢ 0 s = 0 ↔ s = ∅ ∨ 0 = 0

case inr
G : Type u_1
inst✝⁶ : MeasurableSpace G
inst✝⁵ : TopologicalSpace G
inst✝⁴ : BorelSpace G
μ : Measure G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.Regular
s : Set G
hs : IsOpen[inst✝⁵] s
hμ : NeZero μ
⊢ μ s = 0 ↔ s = ∅ ∨ μ = 0
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
congr 1; exact restrict_toMeasurable_of_sFinite s

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ discrim a b c = (2 * a * x + b) ^ 2

Tactic:
rw [discrim]
  linear_combination -4 * a * h

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

Goal state before:

Tactic:
(∫⁻ a, ‖f a‖ₑ ∂μ) ≤ ∫⁻ a : α, ‖g a‖ₑ ∂μ := lintegral_mono_ae h
    _ < ∞ := hg

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

Goal state before:
pp: α : Type u_1
ε : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
c : ε
hc : ‖c‖ₑ ≠ 0
hc' : ‖c‖ₑ ≠ ∞
⊢ HasFiniteIntegral (fun x ↦ c) μ ↔ IsFiniteMeasure μ

Tactic:
simp [hasFiniteIntegral_const_iff_enorm hc', hc, isFiniteMeasure_iff]

Goal state after:
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 ι
inst✝ : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : μ s ≠ ∞
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
⊢ iUnionNotConvergentSeq hε hf hsm hs hfg ⊆ s

Tactic:
by
  rw [iUnionNotConvergentSeq, ← Set.inter_iUnion]
  exact Set.inter_subset_left

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal ‖F n a‖ + ENNReal.ofReal ‖f a‖

Tactic:
rw [← ENNReal.ofReal_add]
        · apply ofReal_le_ofReal
          apply norm_sub_le
        · exact norm_nonneg _
        · exact norm_nonneg _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : HasFiniteIntegral f μ
x : α
⊢ ‖max (f x) 0‖ ≤ ‖f x‖

Tactic:
by simp [abs_le, le_abs_self]

Goal state after:
Module: Mathlib.Data.Complex.Basic

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

Tactic:
ext <;> simp

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: a✝ : ℂ
⊢ 0 + a✝ = a✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ + 0 = a✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ -a✝ + a✝ = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
ext <;> simp

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

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

Goal state before:
pp: ⊢ ↑0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0

Tactic:
neg_re_eq_norm

Goal state after:
z : ℂ
⊢ z ≤ 0 ↔ z ≤ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ b✝ c✝ : ℂ
⊢ a✝ * b✝ * c✝ = a✝ * (b✝ * c✝)

Tactic:
ext <;> simp

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

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

Goal state before:
pp: a✝ : ℂ
⊢ 1 * a✝ = a✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ * 1 = a✝

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ 0 * a✝ = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a✝ : ℂ
⊢ a✝ * 0 = 0

Tactic:
ext <;> simp

Goal state after: