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

Goal state before:
pp: 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 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
⊢ ∃ g, ∀ (x : X × Y), dist (f x) (g x) < ε

Tactic:
refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩

Goal state after:
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 < ε
M : ∀ (K : Set (X × Y)), IsCompact K → ∃ g s, MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) (g x) < ε
p : X × Y
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0) p) < ε
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ∞
h_meas : μ (⇑φ ⁻¹' {∞}) ≠ 0
b : ℝ≥0∞
hb : b < ∞
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb)

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a ↦ f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ∞
h_meas : μ (⇑φ ⁻¹' {∞}) ≠ 0
b : ℝ≥0∞
hb : b < ∞
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {∞})
⊢ ∃ i, b < ⨆ (_ : ∀ (x : α), ↑(i x) ≤ f x), (SimpleFunc.map ofNNReal i).lintegral μ
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
eq : ∀ (p : ℝ≥0∞), ⇑(SimpleFunc.map c rs) ⁻¹' {p} = ⋃ n, ⇑(SimpleFunc.map c rs) ⁻¹' {p} ∩ {a | p ≤ f n a}
mono : ∀ (r : ℝ≥0∞), Monotone fun n ↦ ⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet {a | (SimpleFunc.map c rs) a ≤ f n a}
⊢ ∑ r ∈ (SimpleFunc.map c rs).range, ⨆ n, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a}) =
    ⨆ n, ∑ r ∈ (SimpleFunc.map c rs).range, r * μ (⇑(SimpleFunc.map c rs) ⁻¹' {r} ∩ {a | r ≤ f n a})

Tactic:
refine ENNReal.finsetSum_iSup_of_monotone fun p i j h ↦ ?_
      gcongr _ * μ ?_
      exact mono p h

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
⊢ μ = ν

Tactic:
ext s hs

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ∀ (f : α → ℝ≥0∞), Measurable f → ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), f a ∂ν
s : Set α
hs : MeasurableSet s
⊢ μ s = ν s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
b : β
⊢ ⨅ n, ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ ≤ ∫⁻ (a : α), f b a ∂μ

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ⨅ b, ∫⁻ (a : α), f b a ∂μ ≤ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
· exact iInf_le_of_le (Encodable.encode b + 1) (lintegral_mono <| h_directed.sequence_le b)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Countable β
f : β → α → ℝ≥0∞
μ : Measure α
hμ : μ ≠ 0
hf : ∀ (b : β), Measurable (f b)
hf_int : ∀ (b : β), ∫⁻ (a : α), f b a ∂μ ≠ ∞
h_directed : Directed (fun x1 x2 ↦ x1 ≥ x2) f
val✝ : Encodable β
h✝ : Nonempty β
inhabited_h : Inhabited β
this : ∀ (a : α), ⨅ b, f b a = ⨅ n, f (Directed.sequence f h_directed n) a
n : ℕ
⊢ ⨅ b, ∫⁻ (a : α), f b a ∂μ ≤ ∫⁻ (a : α), (f ∘ Directed.sequence f h_directed) n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ

Tactic:
have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hr : r ≠ ∞
h : ¬r = 0
rinv : r * r⁻¹ = 1
rinv' : r⁻¹ * r = 1
this : r⁻¹ * ∫⁻ (a : α), r * f a ∂μ ≤ ∫⁻ (a : α), r⁻¹ * (r * f a) ∂μ
⊢ ∫⁻ (a : α), r * f a ∂μ ≤ r * ∫⁻ (a : α), f a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : SeminormedAddCommGroup β
m m0 : MeasurableSpace α
hm : m ≤ m0
hf : StronglyMeasurable f
μ : Measure α
inst✝ : SigmaFinite (μ.trim hm)
⊢ ∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = univ

Tactic:
obtain ⟨s, hs, hs_univ⟩ :=
    @exists_spanning_measurableSet_le _ m _ hf.nnnorm.measurable (μ.trim hm) _
  refine ⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩
  have hx_nnnorm : ‖f x‖₊ ≤ n := (hs n).2.2 x hx
  rw [← coe_nnnorm]
  norm_cast

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

Goal state before:
pp: case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ ν ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) ≠ 0

pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ∞
⊢ False

Tactic:
· exact fun h ↦ h_ne_zero (hμν h)

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ∞
⊢ False
Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence

Goal state before:
pp: α : 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 ∂μ ≠ ∞
this : ∀ (n : ℕ), ∃ g, Measurable g ∧ g ≤ f n ∧ ∫⁻ (a : α), f n a ∂μ = ∫⁻ (a : α), g a ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
choose g gmeas gf hg using this

Goal state after:
α : 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 ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
Module: Mathlib.Topology.Perfect

Goal state before:
pp: α : 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 α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
⊢ ∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D

Tactic:
let D := C \ V

Goal state after:
α : 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 α) := {U | U ∈ b ∧ (U ∩ C).Countable}
V : Set α := ⋃ U ∈ v, U
D : Set α := C \ V
⊢ ∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
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 ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
⊢ ‖∑ i ∈ t, f i‖ < ε

Tactic:
have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2

Goal state after:
ι : 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 ι
ht : Disjoint t (s ∪ Set.Finite.toFinset h)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ ‖∑ i ∈ t, f i‖ < ε
Module: Mathlib.Analysis.Normed.Group.InfiniteSum

Goal state before:
pp: ι : Type u_1
ε : Type u_5
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ε
b : ℝ≥0∞
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
⊢ ‖a‖ₑ ≤ b

Tactic:
exact le_of_tendsto_of_tendsto' hf.enorm hg fun _s ↦ enorm_sum_le_of_le _ fun i _hi ↦ h i

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

Goal state before:
pp: case refine_1
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), StronglyMeasurable (u i)
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
t_sf : ℕ → ι →ₛ ι
ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n ↦ u ((t_sf n) j) x) atTop (𝓝 (u j x))
U : ℕ → ι × α → β := fun n p ↦ u ((t_sf n) p.1) p.2
h_tendsto : Tendsto U atTop (𝓝 fun p ↦ u p.1 p.2)
n : ℕ
this : (fun p ↦ u (↑p.1) p.2) = (fun p ↦ u (↑p.2) p.1) ∘ Prod.swap
⊢ Measurable fun p ↦ u (↑p.2) p.1

Tactic:
exact measurable_from_prod_countable_left fun j => (h j).measurable

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
⊢ dist x z ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))

Tactic:
refine le_ciInf_add fun p => ?_

Goal state after:
X : Type u
Y : Type v
Z : Type w
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Z
Φ : Z → X
Ψ : Z → Y
ε : ℝ
H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε
x : X
y : Y
z : X
p : Z
⊢ dist x z ≤ dist x (Φ p) + dist y (Ψ p) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
Module: Mathlib.Topology.MetricSpace.Gluing

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ (∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s) →
    (∃ ε > 0, ∀ ⦃a b : X⦄, dist a b < ε → Prod.map Sum.inl Sum.inl (a, b) ∈ s) ∧
      ∃ ε > 0, ∀ ⦃a b : Y⦄, dist a b < ε → Prod.map Sum.inr Sum.inr (a, b) ∈ s

Tactic:
rintro ⟨ε, ε0, H⟩
    constructor <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
x : X
y : Y
⊢ 1 ≤ Sum.dist (Sum.inr y) (Sum.inl x)

Tactic:
by
  rw [Sum.dist_comm]; exact Sum.one_le_dist_inl_inr

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

Goal state before:
pp: β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
⊢ x = y

Tactic:
ext1

Goal state after:
β : Type u_1
α : Type u_2
A : List β → Set α
hA : CantorScheme.Disjoint A
x y : ↑(inducedMap A).fst
hxy : (inducedMap A).snd x = (inducedMap A).snd y
⊢ ↑x = ↑y
Module: Mathlib.Topology.MetricSpace.Perfect

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
C : Set α
ε : ℝ≥0∞
hC : Perfect C
hnonempty : C.Nonempty
ε_pos : 0 < ε
D₀ D₁ : Set α
perf0 : Perfect D₀
sub0 : D₀ ⊆ C
hdisj : Disjoint D₀ D₁
perf1 : Perfect D₁
sub1 : D₁ ⊆ C
x₀ : α
hx₀ : x₀ ∈ D₀
x₁ : α
hx₁ : x₁ ∈ D₁
perf0' : Perfect (closure (eball x₀ (ε / 2) ∩ D₀))
non0' : (closure (eball x₀ (ε / 2) ∩ D₀)).Nonempty
sub0' : closure (eball x₀ (ε / 2) ∩ D₀) ⊆ D₀
diam0 : ediam (closure (eball x₀ (ε / 2) ∩ D₀)) ≤ ε
perf1' : Perfect (closure (eball x₁ (ε / 2) ∩ D₁))
non1' : (closure (eball x₁ (ε / 2) ∩ D₁)).Nonempty
sub1' : closure (eball x₁ (ε / 2) ∩ D₁) ⊆ D₁
diam1 : ediam (closure (eball x₁ (ε / 2) ∩ D₁)) ≤ ε
⊢ Disjoint (closure (eball x₀ (ε / 2) ∩ D₀)) (closure (eball x₁ (ε / 2) ∩ D₁))

Tactic:
apply Disjoint.mono _ _ hdisj <;> assumption

Goal state after:
Module: Mathlib.Dynamics.Ergodic.MeasurePreserving

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μa : Measure α
μb : Measure β
f : α → β
hf : MeasurePreserving f μa μb
s : Set β
⊢ μa (f ⁻¹' s) ≤ μb s

Tactic:
rw [← hf.map_eq]
  exact le_map_apply hf.aemeasurable _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f

Tactic:
obtain ⟨f, hfD, hf⟩ := hD.exists_nat_bool_injection Dnonempty

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
C : Set α
hC : IsClosed C
hunc : ¬C.Countable
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace α := TopologicalSpace.upgradeIsCompletelyMetrizable α
D : Set α
hD : Perfect D
Dnonempty : D.Nonempty
hDC : D ⊆ C
f : (ℕ → Bool) → α
hfD : range f ⊆ D
hf : Continuous f ∧ Injective f
⊢ ∃ f, range f ⊆ C ∧ Continuous f ∧ Injective f
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
⊢ map (fun x ↦ c) μ = μ univ • dirac c

Tactic:
ext s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
c : β
s : Set β
hs : MeasurableSet s
⊢ (map (fun x ↦ c) μ) s = (μ univ • dirac c) s
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
⊢ ξ = 0

Tactic:
ext s hs

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ ξ s = 0 s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
⊢ map f (dirac a) = dirac (f a)

Tactic:
ext s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : α → β
a : α
s : Set β
hs : MeasurableSet s
⊢ (map f (dirac a)) s = (dirac (f a)) s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i ∈ s, t ∩ {i}) = (∑ a ∈ s, μ {a} • dirac a) t

Tactic:
measure_biUnion_finset (fun i hi j hj hij ↦ .inter_left' _ <| .inter_right' _ ?_)
      (by measurability)

Goal state after:
α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
⊢ ∑ p ∈ s, μ (t ∩ {p}) = (∑ a ∈ s, μ {a} • dirac a) t

α : Type u_4
mα : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
μ : Measure α
s : Finset α
hμ : ∀ᵐ (a : α) ∂μ, a ∈ s
t : Set α
ht : MeasurableSet t
i : α
hi : i ∈ ↑s
j : α
hj : j ∈ ↑s
hij : i ≠ j
⊢ Disjoint {i} {j}
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
⊢ (c • m).join = c • m.join

Tactic:
ext s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
m : Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (c • m).join s = (c • m.join) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
⊢ (sum m).join = sum fun i ↦ (m i).join

Tactic:
ext s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_3
m : ι → Measure (Measure α)
s : Set α
hs : MeasurableSet s
⊢ (sum m).join s = (sum fun i ↦ (m i).join) s
Module: Mathlib.MeasureTheory.Measure.GiryMonad

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ (dirac μ).join = μ

Tactic:
ext s hs

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ (dirac μ).join s = μ s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case h₁
E : ℕ → Type u_1
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → PseudoEMetricSpace (F i)
ε : ℝ≥0∞
hε : 0 < ε
K : Finset ι
hK : ∑' (i : { j // j ∉ K }), 2⁻¹ ^ encode ↑i < ε / 2
δ : ℝ≥0∞
δpos : 0 < δ
hδ : δ * ↑K.card < ε / 2
x y : (i : ι) → F i
hxy : ∀ (x_1 : ι) (h : x_1 ∈ K), edist (x x_1) (y x_1) < δ
⊢ ∑ _i ∈ K, δ ≤ ε / 2

Tactic:
simpa [mul_comm] using hδ.le

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

Goal state before:
pp: case inl
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : IsEmpty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

pp: case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)

Tactic:
· exact continuous_of_discreteTopology

Goal state after:
case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] (distDenseSeq X n)
Module: Mathlib.MeasureTheory.Measure.Doubling

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ μ (closedBall x 0) ≤ ↑(scalingConstantOf μ K) * μ (closedBall x 0)

Tactic:
refine le_mul_of_one_le_of_le ?_ le_rfl

Goal state after:
case inr.inl
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
h : ∀ᶠ (ε : ℝ) in 𝓝[>] 0, ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)
R : ℝ
Rpos : R ∈ Ioi 0
hR :
  Ioc 0 R ⊆ {x | (fun ε ↦ ∀ (x : α), ∀ t ≤ K, μ (closedBall x (t * ε)) ≤ ↑(Classical.choose ⋯) * μ (closedBall x ε)) x}
x : α
t : ℝ
ht : t ∈ Ioc 0 K
hr : 0 ≤ R
⊢ 1 ≤ ↑(scalingConstantOf μ K)
Module: Mathlib.MeasureTheory.Group.Convolution

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
inst✝² : MeasurableSpace M
μ ν : Measure M
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ (map (fun x ↦ x.1 * x.2) (μ.prod ν)) Set.univ < ∞

Tactic:
exact IsFiniteMeasure.measure_univ_lt_top

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 ν
⊢ map Prod.fst (μ.prod ν) = ν univ • μ

Tactic:
ext s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
hs : MeasurableSet s
⊢ (map Prod.fst (μ.prod ν)) s = (ν univ • μ) s
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
⊢ map Prod.snd (μ.prod ν) = μ univ • ν

Tactic:
ext s hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set β
hs : MeasurableSet s
⊢ (map Prod.snd (μ.prod ν)) s = (μ univ • ν) s
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: case hg
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

Tactic:
exact measurable_const_smul ..

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

Goal state before:
pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν : Measure A
g✝ : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g'⁻¹ • x

Tactic:
exact measurable_const_smul ..

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

Goal state before:
pp: case hf
G : Type u_1
A : Type u_2
inst✝³ : Group G
inst✝² : MulAction G A
inst✝¹ : MeasurableSpace A
inst✝ : MeasurableConstSMul G A
μ✝ ν✝ : Measure A
g✝ : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable fun x ↦ DomMulAct.mk.symm g⁻¹ • x

Tactic:
exact measurable_const_smul ..

Goal state after: