mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case hnhds
X : Type u_3
Y : Type u_4
α : Type u_5
inst✝⁷ : Zero α
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace X
inst✝³ : MeasurableSpace Y
inst✝² : OpensMeasurableSpace X
inst✝¹ : OpensMeasurableSpace Y
inst✝ : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ g s, MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε

Tactic:
· rintro ⟨x, y⟩ -
      obtain ⟨u, v, hu, xu, hv, yv, huv⟩ : ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧
        u ×ˢ v ⊆ {z | dist (f z) (f (x, y)) < ε} :=
          mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε
      refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
      exact ⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
        Subset.rfl, fun z hz ↦ huv hz⟩

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

Goal state before:
pp: α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} =ᵐ[μ] {x | f x = g x}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Goal state after:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝¹ : TopologicalSpace E
inst✝ : MetrizableSpace E
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a = AEStronglyMeasurable.mk g hg a} x = {x | f x = g x} x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} =ᵐ[μ] {a | f a < g a}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a < AEStronglyMeasurable.mk g hg a} x = {a | f a < g a} x
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
⊢ {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} =ᵐ[μ] {a | f a ≤ g a}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst✝² : Preorder β
inst✝¹ : OrderClosedTopology β
inst✝ : PseudoMetrizableSpace β
f g : α → β
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
x : α
hfx : f x = AEStronglyMeasurable.mk f hf x
hgx : g x = AEStronglyMeasurable.mk g hg x
⊢ {a | AEStronglyMeasurable.mk f hf a ≤ AEStronglyMeasurable.mk g hg a} x = {a | f a ≤ g a} x
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
⊢ ∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε

Tactic:
use (ε₂ - ε₁) / C, ENNReal.div_pos_iff.2 ⟨(tsub_pos_iff_lt.2 hε₁₂).ne', ENNReal.coe_ne_top⟩

Goal state after:
case right
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h : ∫⁻ (x : α), f x ∂μ ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
ε₂ : ℝ≥0∞
hε₂0 : 0 < ε₂
hε₂ε : ε₂ < ε
ε₁ : ℝ≥0∞
hε₁0 : 0 < ε₁
hε₁₂ : ε₁ < ε₂
φ : α →ₛ ℝ≥0
left✝ : ∀ (x : α), ↑(φ x) ≤ f x
hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁
C : ℝ≥0
hC : ∀ (x : α), φ x ≤ C
⊢ ∀ (s : Set α), μ s < (ε₂ - ε₁) / ↑C → ∫⁻ (x : α) in s, f x ∂μ < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Markov

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
⊢ s.indicator f a ≤ 1

Tactic:
by_cases has : a ∈ s

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∈ s
⊢ s.indicator f a ≤ 1

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
hf : ∀ a ∈ s, a ∈ t → f a ≤ 1
hf' : ∀ a ∈ s, a ∉ t → f a = 0
a : α
has : a ∉ s
⊢ s.indicator f a ≤ 1
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddCancelMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n ↦ (φ n) x) atTop (𝓝 (f x))
⊢ Measurable (g + f)

Tactic:
have : Tendsto (fun n x ↦ g x + φ n x) atTop (𝓝 (g + f)) :=
    tendsto_pi_nhds.2 (fun x ↦ tendsto_const_nhds.add (hφ x))

Goal state after:
α : Type u_5
E : Type u_6
x✝ : MeasurableSpace α
inst✝⁵ : AddCancelMonoid E
inst✝⁴ : TopologicalSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : ContinuousAdd E
inst✝ : PseudoMetrizableSpace E
g f : α → E
hg : Measurable g
φ : ℕ → α →ₛ E
hφ : ∀ (x : α), Tendsto (fun n ↦ (φ n) x) atTop (𝓝 (f x))
this : Tendsto (fun n x ↦ g x + (φ n) x) atTop (𝓝 (g + f))
⊢ Measurable (g + f)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f✝ : α → ℝ≥0∞
hf✝ : Measurable f✝
f g : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support f) (Function.support g)
hf : Measurable f
a✝ : Measurable g
hf_prop : ∫⁻ (a : α), f a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ
hg_prop : ∫⁻ (a : α), g a ∂μ.trim hm = ∫⁻ (a : α), g a ∂μ
h_m : ∫⁻ (a : α), f a + g a ∂μ.trim hm = ∫⁻ (a : α), f a ∂μ.trim hm + ∫⁻ (a : α), g a ∂μ.trim hm
h_m0 : ∫⁻ (a : α), f a + g a ∂μ = ∫⁻ (a : α), f a ∂μ + ∫⁻ (a : α), g a ∂μ
⊢ ∫⁻ (a : α), (f + g) a ∂μ.trim hm = ∫⁻ (a : α), (f + g) a ∂μ

Tactic:
rwa [hf_prop, hg_prop, ← h_m0] at h_m

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
by_contra h0

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ False
Module: Mathlib.Topology.Perfect

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ U ∩ C ⊆ E ∩ D ∪ V ∩ C

pp: case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ (E ∩ D ∪ V ∩ C).Countable

Tactic:
· rintro y ⟨yU, yC⟩
          by_cases h : y ∈ V
          · exact mem_union_right _ (mem_inter h yC)
          · exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)

Goal state after:
case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed[inst✝¹] C
b : Set (Set α)
bct : b.Countable
left✝ : ∅ ∉ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := ⋯
V : Set α := ⋯
D : Set α := ⋯
Vct : (V ∩ C).Countable
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : (E ∩ D).Countable
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ (E ∩ D ∪ V ∩ C).Countable
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: case neg
ι : Type u_1
E : Type u_3
inst✝ : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

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

Goal state before:
pp: case a
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
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 ∂μ ≠ ∞
g : ℕ → α → ℝ≥0∞
gmeas : ∀ (n : ℕ), Measurable (g n)
gf : ∀ (n : ℕ), g n ≤ f n
hg : ∀ (n : ℕ), ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g n a ∂μ
g' : ℕ → α → ℝ≥0∞ := ⋯
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, g' n a ≤ f n a

Tactic:
filter_upwards [I'] with x hx using hx n

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_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
have h_exists : ∀ᵐ a ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l) := by
    filter_upwards [hf_mono] with a h_mono
    rcases _root_.tendsto_atTop_of_antitone h_mono with h | h
    · refine ⟨0, h.mono_right ?_⟩
      rw [OrderBot.atBot_eq]
      exact pure_le_nhds _
    · exact h

Goal state after:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ l, Tendsto (fun i ↦ f i a) atTop (𝓝 l)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i ↦ Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}
i : ι
⊢ IsComplete (s i)

Tactic:
simp only [s, ← range_sigmaMk]

Goal state after:
ι : Type u_1
E : ι → Type u_2
inst✝¹ : (i : ι) → MetricSpace (E i)
inst✝ : ∀ (i : ι), CompleteSpace (E i)
s : ι → Set ((i : ι) × E i) := fun i ↦ Sigma.fst ⁻¹' {i}
U : Set (((k : ι) × E k) × (k : ι) × E k) := {p | dist p.1 p.2 < 1}
i : ι
⊢ IsComplete (range (Sigma.mk i))
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
ε_pos : 0 < ε
x : α
xC : x ∈ C
⊢ ε ≠ 0 ∧ 2 ≠ ∞

Tactic:
exact ⟨ne_of_gt ε_pos, by simp⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
x : (n : ℕ) → E n
hx : x ∉ s
⊢ 0 < shortestPrefixDiff x s

Tactic:
rcases hne with ⟨y, hy⟩

Goal state after:
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x : (n : ℕ) → E n
hx : x ∉ s
y : (n : ℕ) → E n
hy : y ∈ s
⊢ 0 < shortestPrefixDiff x s
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist (toInductiveLimit I n x) (toInductiveLimit I n y) = dist x y

Tactic:
change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y

Goal state after:
X : ℕ → Type u
inst✝ : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
x : ℕ → Bool
⊢ x ∈ (inducedMap D).fst

Tactic:
rw [hanti.map_of_vanishingDiam hdiam fun l => (DP l).property.2]

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
C : Set α
hC : Perfect C
hnonempty : C.Nonempty
inst✝ : CompleteSpace α
u : ℕ → ℝ≥0∞
upos' : ∀ (n : ℕ), u n ∈ Ioo 0 1
hu : Tendsto u atTop (nhds 0)
upos : ∀ (n : ℕ), 0 < u n
P : Type (max 0 u_1) := { E // Perfect E ∧ E.Nonempty }
C0 C1 : {C : Set α} → Perfect C → C.Nonempty → {ε : ℝ≥0∞} → 0 < ε → Set α
h0 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C0 hC hnonempty hε) ∧
      (C0 hC hnonempty hε).Nonempty ∧ C0 hC hnonempty hε ⊆ C ∧ ediam (C0 hC hnonempty hε) ≤ ε
h1 :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Perfect (C1 hC hnonempty hε) ∧
      (C1 hC hnonempty hε).Nonempty ∧ C1 hC hnonempty hε ⊆ C ∧ ediam (C1 hC hnonempty hε) ≤ ε
hdisj :
  ∀ {C : Set α} (hC : Perfect C) (hnonempty : C.Nonempty) {ε : ℝ≥0∞} (hε : 0 < ε),
    Disjoint (C0 hC hnonempty hε) (C1 hC hnonempty hε)
DP : List Bool → P :=
  fun l ↦
    List.rec ⟨C, ⋯⟩
      (fun a l ih ↦ Bool.casesOn (motive := fun t ↦ a = t → P) a (fun h ↦ ⟨C0 ⋯ ⋯ ⋯, ⋯⟩) (fun h ↦ ⟨C1 ⋯ ⋯ ⋯, ⋯⟩) ⋯) l
D : List Bool → Set α := fun l ↦ ↑(DP l)
hanti : ClosureAntitone D
hdiam : VanishingDiam D
hdisj' : CantorScheme.Disjoint D
x : ℕ → Bool
⊢ x ∈ univ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
a✝ : MeasurableSet s
this : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ (map f μ) s = (sum fun b ↦ μ (f ⁻¹' {b}) • dirac b) s

Tactic:
simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
    tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]

Goal state after:
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
hfxfy : Ax.some ≠ f y
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
fy

Goal state after:
case pos
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
hfxfy : Ax.some ≠ Ay.some
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y ∨ longestPrefix y s < firstDiff x y
this : cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
t : TopologicalSpace α
inst✝⁵ : PolishSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
tβ : TopologicalSpace β
inst✝² : MeasurableSpace β
inst✝¹ : OpensMeasurableSpace β
f : α → β
inst✝ : SecondCountableTopology ↑(range f)
hf : Measurable f
b : Set (Set ↑(range f))
b_count : b.Countable
hb : IsTopologicalBasis b
this✝ : Countable ↑b
T : ↑b → TopologicalSpace α
Tt : ∀ (s : ↑b), T s ≤ t
Tpolish : ∀ (s : ↑b), PolishSpace α
h✝ : ∀ (s : ↑b), IsClosed[T s] (rangeFactorization f ⁻¹' ↑s)
Topen : ∀ (s : ↑b), IsOpen[T s] (rangeFactorization f ⁻¹' ↑s)
t' : TopologicalSpace α
t'T : ∀ (i : ↑b), t' ≤ T i
t't : t' ≤ t
t'_polish : PolishSpace α
this : Continuous[t', instTopologicalSpaceSubtype] (rangeFactorization f)
⊢ Continuous[t', tβ] f

Tactic:
exact continuous_subtype_val.comp this

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

Goal state before:
pp: α : 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 ε)

Tactic:
pow_succ,

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 * 2 * ε)) ≤ ↑C ^ (n + 1) * μ (closedBall x ε)
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
⊢ MeasurableSpace.map f inst✝⁶ = borel Y

Tactic:
have d := hf.mono le_rfl OpensMeasurableSpace.borel_le

Goal state after:
X : Type u_3
Y : Type u_4
inst✝⁶ : MeasurableSpace X
inst✝⁵ : StandardBorelSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : T0Space Y
inst✝² : MeasurableSpace Y
inst✝¹ : OpensMeasurableSpace Y
inst✝ : SecondCountableTopology Y
f : X → Y
hf : Measurable f
hsurj : Surjective f
d : Measurable f
⊢ MeasurableSpace.map f inst✝⁶ = borel Y
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: γ : 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
⊢ MeasurableSet (range f)

Tactic:
let := TopologicalSpace.upgradeIsCompletelyMetrizable γ

Goal state after:
γ : 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 γ
⊢ MeasurableSet (range f)
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
⊢ H.IsComplement' K

Tactic:
by
  refine ⟨mul_injective_of_disjoint h1, fun g => ?_⟩
  obtain ⟨h, hh, k, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g
  exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩

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✝ : SMulInvariantMeasure G α μ
c : G
s t : Set α
⊢ c • s ≤ᵐ[μ] c • t ↔ s ≤ᵐ[μ] t

Tactic:
by
  simp only [ae_le_set, ← smul_set_sdiff, measure_smul_eq_zero_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν).snd s = ν s

Tactic:
rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]

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

Goal state before:
pp: G : Type u_1
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : InvolutiveInv G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsInvInvariant
f : G → ℝ≥0∞
⊢ ∫⁻ (x : G), f x⁻¹ ∂μ = ∫⁻ (x : G), f x ∂μ

Tactic:
by
  simpa using (lintegral_map_equiv f (μ := μ) <| MeasurableEquiv.inv G).symm

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: case hf
G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : SFinite μ
f g k : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hk : AEMeasurable k μ
x : G
⊢ AEMeasurable (Function.uncurry fun y x_1 ↦ f y * (g (y⁻¹ * x_1) * k ((y⁻¹ * x_1)⁻¹ * (y⁻¹ * x)))) (μ.prod μ)

Tactic:
simpa [mul_assoc] using by fun_prop

Goal state after: