mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.Real.Lemmas

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) x

Tactic:
tendsto_nhds_unique h_tto (tendsto_atTop_ciInf h_ant h_bdd)

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 ↦ x1 ≤ x2
f : ι → ℝ
x : ℝ
h_tto : Tendsto f atTop (𝓝 x)
h_ant : Antitone f
h_bdd : BddBelow (range f)
⊢ IsGLB (range f) (⨅ i, f i)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable fun r ↦ (∞, ↑r).1 * (∞, ↑r).2

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable fun r ↦ (↑r, ∞).1 * (↑r, ∞).2

Tactic:
· simp only [ENNReal.top_mul', ENNReal.coe_eq_zero]
    exact measurable_const.piecewise (measurableSet_singleton _) measurable_const

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort y
s t u : Set α
mα : MeasurableSpace α
⊢ Measurable fun r ↦ (↑r, ∞).1 * (↑r, ∞).2
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
h : ∀ (i : ι), Measurable (f i)
⊢ Measurable (∑' (i : ι), f i)

Tactic:
by
  convert! Measurable.ennreal_tsum h with x
  exact tsum_apply (Pi.summable.2 fun _ => ENNReal.summable)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
have A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0) := by
    rw [← measure_union]
    · rw [← inter_union_distrib_left, ← preimage_union, singleton_union, Ioi_insert,
        ← _root_.bot_eq_zero, Ici_bot, preimage_univ, inter_univ]
    · exact disjoint_singleton_left.mpr self_notMem_Ioi
        |>.preimage f |>.inter_right' s |>.inter_left' s
    · exact hs.inter (hf measurableSet_Ioi)

Goal state after:
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
⊢ μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g : α → β
g₁ : γ → β
hgm₁ : StronglyMeasurable g₁
heq : g ∘ f =ᵐ[μ] g₁
⊢ AEStronglyMeasurable g (Measure.map f μ)

Tactic:
rcases hf.exists_stronglyMeasurable_extend hgm₁ fun x => ⟨g x⟩ with ⟨g₂, hgm₂, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
γ : Type u_5
mγ : MeasurableSpace γ
mα : MeasurableSpace α
f : γ → α
μ : Measure γ
hf : MeasurableEmbedding f
g g₂ : α → β
hgm₂ : StronglyMeasurable g₂
hgm₁ : StronglyMeasurable (g₂ ∘ f)
heq : g ∘ f =ᵐ[μ] g₂ ∘ f
⊢ AEStronglyMeasurable g (Measure.map f μ)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
have eq : ∀ p, rs.map c ⁻¹' {p} = ⋃ n, rs.map c ⁻¹' {p} ∩ { a | p ≤ f n a } := by
    intro p
    rw [← inter_iUnion]; nth_rw 1 [← inter_univ (map c rs ⁻¹' {p})]
    refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_
    by_cases p_eq : p = 0
    · simp [p_eq]
    simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx
    subst hx
    have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
    have : s x ≠ 0 := right_ne_zero_of_mul this
    have : (rs.map c) x < ⨆ n : ℕ, f n x := by
      refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
      suffices r * s x < 1 * s x by simpa
      gcongr
    rcases lt_iSup_iff.1 this with ⟨i, hi⟩
    exact mem_iUnion.2 ⟨i, le_of_lt hi⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : α → ℝ≥0∞ := fun a ↦ ⨆ n, f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), ↑(s x) ≤ ⨆ n, f n x
r : ℝ≥0
right✝ ha✝ : ↑r < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun a ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α ↑r * SimpleFunc.map c s
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
⊢ ↑r * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := spanningSets (μ.restrict t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := hf_meas.approx
fs : ℕ → α →ₛ β := fun n ↦ (f_approx n).restrict (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : x ∈ S n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m

pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := ⋯
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := ⋯
fs : ℕ → α →ₛ β := ⋯
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, x ∈ S n

Tactic:
· exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ this : SigmaFinite (μ.restrict t)
S : ℕ → Set α := ⋯
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := ⋯
fs : ℕ → α →ₛ β := ⋯
h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, (fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n ↦ (f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, x ∈ S n
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
g : α → ℝ≥0∞
hf_meas : ∀ (n : ℕ), Measurable (f n)
h_bound : ∀ (n : ℕ), f n ≤ᵐ[μ] g
h_fin : ∫⁻ (a : α), g a ∂μ ≠ ∞
⊢ Antitone fun n a ↦ ⨆ i, ⨆ (_ : i ≥ n), f i a

Tactic:
intro n m hnm a
        exact iSup_le_iSup_of_subset fun i hi => le_trans hnm hi

Goal state after:
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : MeasurableSpace α
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSingletonClass α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoMetrizableSpace β
h : SecondCountableTopologyEither α β
f : α → β
s : Set α
hf : ContinuousOn f s
hs : sᶜ.Countable
h's : MeasurableSet s
this✝ : f = fun x ↦ if hx : x ∈ s then f ↑⟨x, hx⟩ else f ↑⟨x, hx⟩
this : SecondCountableTopologyEither (↑s) β
⊢ StronglyMeasurable fun x ↦ f ↑x

Tactic:
exact (continuousOn_iff_continuous_domRestrict.1 hf).stronglyMeasurable

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ μ s = ∞

Tactic:
by
  rw [measure_eq_iInf]
  simp_rw [iInf_eq_top]
  suffices ∀ t, t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → s ⊆ t → MeasurableSet t → μ t = ∞ by
    intro t hts ht
    suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
      measure_mono_top Set.inter_subset_left this
    have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
    exact this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)
  intro t ht_subset hst ht
  refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_
  exact fun hνt ↦ hνs (measure_mono_null hst hνt)

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᵐ[μ] F
⊢ F' =ᵐ[μ] F

Tactic:
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ from
    ae_eq_of_ae_le_of_lintegral_le hF'_le (this ▸ h_int_finite) hF_meas this.symm.le

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hF_meas : AEMeasurable F μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Monotone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), f i a ≤ F a
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_bound_finite : ∀ᵐ (a : α) ∂μ, F a ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ := fun a ↦ if h : ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) then h.choose else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F' ≤ᵐ[μ] F
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → ‖∑ i ∈ t, g i‖ < ε
t : Finset ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ a ∈ {x | ‖f x‖ ≤ g x}
⊢ ‖f i‖ ≤ g i

Tactic:
exact (ht hi).2

Goal state after:
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
⊢ ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
by
    let ⟨K, t, ht, hf⟩ := hf hx
    let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
    exact ⟨ε, hε, K, hf.mono hε'⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
⊢ AnalyticSet (f '' s)

Tactic:
have : f '' s = range (f ∘ g) := by rw [range_comp, gs]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
s : Set α
hs : AnalyticSet s
f : α → β
hf : ContinuousOn f s
γ : Type
γtop : TopologicalSpace γ
γpolish : PolishSpace γ
g : γ → α
g_cont : Continuous[γtop, inst✝¹] g
gs : range g = s
this : f '' s = range (f ∘ g)
⊢ AnalyticSet (f '' s)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ univ = 0

Tactic:
rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν

Tactic:
simp_rw [Filter.disjoint_iff, mem_ae_iff] at h

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ∃ s, μ sᶜ = 0 ∧ ∃ t, ν tᶜ = 0 ∧ Disjoint s t
⊢ Disjoint μ ν
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
⊢ Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)

Tactic:
have : Tendsto (fun n : ℕ => (2 : ℝ) * (1 / 2) ^ n) atTop (𝓝 (2 * 0)) :=
        (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).const_mul _

Goal state after:
α : Type u_2
inst✝³ : MetricSpace α
inst✝² : CompleteSpace α
inst✝¹ : SecondCountableTopology α
inst✝ : Nonempty α
this✝ : MetricSpace (ℕ → ℕ) := metricSpaceNatNat
I0 : 0 < 1 / 2
I1 : 1 / 2 < 1
u : ℕ → α
hu : DenseRange u
s : Set (ℕ → ℕ) := {x | (⋂ n, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty}
g : ↑s → α := fun x ↦ Set.Nonempty.some ⋯
A : ∀ (x : ↑s) (n : ℕ), dist (g x) (u (↑x n)) ≤ (1 / 2) ^ n
g_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
g_surj : Surjective g
x : ℕ → ℕ
hx : ClusterPt x (𝓟 s)
this : Tendsto (fun n ↦ 2 * (1 / 2) ^ n) atTop (𝓝 (2 * 0))
⊢ Tendsto (fun n ↦ diam (closedBall (u (x n)) ((1 / 2) ^ n))) atTop (𝓝 0)
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : Fᶜ = ∅
⊢ F = univ

Tactic:
compl_empty_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝ : μ.IsOpenPosMeasure
F : Set X
hF : IsClosed[inst✝¹] F
h : F = univ
⊢ F = univ
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoMetricSpace (F i)
x y : (i : ι) → F i
i : ι
h : dist x y < 2⁻¹ ^ encode i
⊢ dist (x i) (y i) ≤ dist x y

Tactic:
by
  simpa only [not_le.2 h, false_or] using min_le_iff.1 (min_dist_le_dist_pi x y i)

Goal state after:
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✝ : NullSingletonClass μ
x : α
y : β
⊢ (μ.prod ν) {(x, y)} = (μ.prod ν) ({x} ×ˢ {y})

Tactic:
rw [singleton_prod_singleton]

Goal state after:
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✝ : NullSingletonClass ν
x : α
y : β
⊢ (μ.prod ν) {(x, y)} = (μ.prod ν) ({x} ×ˢ {y})

Tactic:
rw [singleton_prod_singleton]

Goal state after:
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 ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (μ.prod ν) univ < ∞

Tactic:
rw [← univ_prod_univ, prod_prod]

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ
μ✝ μ' : Measure α✝
ν✝ ν' : Measure β✝
τ : Measure γ
inst✝² : SFinite ν✝
α : Type u_4
β : Type u_5
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ μ univ * ν univ < ∞
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 ν✝
α : Type u_4
β : Type u_5
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝¹ : SFinite μ
x✝ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
⊢ SFinite (μ.prod ν)

Tactic:
have : μ.prod ν =
      Measure.sum (fun (p : ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod (sfiniteSeq ν p.2)) := by
    conv_lhs => rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν]
    apply prod_sum
  rw [this]
  infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (hST.equiv g).1 = ⟨1, h1⟩

Tactic:
ext
  rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]

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

Goal state before:
pp: M : Type v
α : Type w
m : MeasurableSpace α
inst✝² : SMul M α
inst✝¹ : MeasurableConstSMul M α
c : M
μ : Measure α
inst✝ : SMulInvariantMeasure M α μ
⊢ Measure.map (fun x ↦ c • x) μ = μ

Tactic:
ext1 s hs
      rw [map_apply (measurable_const_smul c) hs]
      exact SMulInvariantMeasure.measure_preimage_smul c hs

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

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
tfae_5_to_3 : (∀ (c : G) (s : Set α), μ (c • s) = μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
⊢ [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ].TFAE

Tactic:
tfae_have 3 → 2
  | H, c, s, hs => by
    rw [preimage_smul]
    exact H c⁻¹ s hs

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : MeasurableConstSMul G α
tfae_1_iff_2 : SMulInvariantMeasure G α μ ↔ ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_1_to_6 : SMulInvariantMeasure G α μ → ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ
tfae_6_to_7 : (∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ) → ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ
tfae_7_to_4 :
  (∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ) → ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s
tfae_4_to_5 : (∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s) → ∀ (c : G) (s : Set α), μ (c • s) = μ s
tfae_5_to_3 : (∀ (c : G) (s : Set α), μ (c • s) = μ s) → ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s
tfae_3_to_2 :
  (∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s) →
    ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s
⊢ [SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x ↦ c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), Measure.map (fun x ↦ c • x) μ = μ,
      ∀ (c : G), MeasurePreserving (fun x ↦ c • x) μ μ].TFAE
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
⊢ (∑ i ∈ a, μ i).InnerRegular

Tactic:
induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : ι → Measure α
f : α → ℝ≥0∞
⊢ (sum μ).withDensity f = sum fun n ↦ (μ n).withDensity f

Tactic:
ext1 s hs
  simp_rw [sum_apply _ hs, withDensity_apply f hs, restrict_sum μ hs, lintegral_sum_measure]

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

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
⊢ (μ.withDensity f) s = 0

Tactic:
have A : s ⊆ t ∪ { x | f x = 0 } := by
      intro x hx
      rcases eq_or_ne (f x) 0 with (fx | fx)
      · simp only [fx, mem_union, mem_ofPred_eq, or_true]
      · left
        apply subset_toMeasurable _ _
        exact ⟨fx, hx⟩

Goal state after:
case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
⊢ (μ.withDensity f) s = 0
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
μ✝ : Measure α
inst✝⁶ : TopologicalSpace α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SecondCountableTopology X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
U : Set X
hU : U ∈ {K | IsOpen[inst✝⁵] K} ∩ {s | μ s < ∞}
⊢ U ∈ {U | IsOpen[inst✝⁵] U ∧ (μ.restrict U).OuterRegular}

Tactic:
have : Fact (μ U < ∞) := ⟨hU.2⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
μ✝ : Measure α
inst✝⁶ : TopologicalSpace α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SecondCountableTopology X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
U : Set X
hU : U ∈ {K | IsOpen[inst✝⁵] K} ∩ {s | μ s < ∞}
this : Fact (μ U < ∞)
⊢ U ∈ {U | IsOpen[inst✝⁵] U ∧ (μ.restrict U).OuterRegular}
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
⊢ (μ.restrict A).InnerRegularWRT IsCompact IsOpen[inst✝³]

Tactic:
intro V hV r hr

Goal state after:
α : Type u_1
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : TopologicalSpace α
inst✝² : R1Space α
inst✝¹ : BorelSpace α
inst✝ : μ.Regular
A : Set α
h'A : μ A ≠ ∞
this : (μ.restrict A).WeaklyRegular
V : Set α
hV : IsOpen[inst✝³] V
r : ℝ≥0∞
hr : r < (μ.restrict A) V
⊢ ∃ K ⊆ V, IsCompact K ∧ r < (μ.restrict A) K