mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α), g x ∂μ - ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α), g x - f x ∂μ

Tactic:
by
  rw [tsub_le_iff_right]
  by_cases hfi : ∫⁻ x, f x ∂μ = ∞
  · rw [hfi, add_top]
    exact le_top
  · rw [← lintegral_add_right' _ hf]
    gcongr
    exact le_tsub_add

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), Measurable (f n)
h_mono✝ : ∀ (n : ℕ), f n.succ ≤ᵐ[μ] f n
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
fn_le_f0 : ∫⁻ (a : α), ⨅ n, f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
fn_le_f0' : ⨅ n, ∫⁻ (a : α), f n a ∂μ ≤ ∫⁻ (a : α), f 0 a ∂μ
h_mono : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), f n.succ a ≤ f n a
a : α
h : ∀ (n : ℕ), f n.succ a ≤ f n a
n : ℕ
ih : f n a ≤ f 0 a
⊢ f (n + 1) a ≤ f 0 a

Tactic:
exact (h n).trans ih

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
⊢ ∫⁻ (a : α) in t, s.indicator f a ∂μ = ∫⁻ (a : α) in s ∩ t, f a ∂μ

Tactic:
lintegral_indicator₀ hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s t : Set α
hs : NullMeasurableSet s (μ.restrict t)
⊢ ∫⁻ (a : α) in s, f a ∂μ.restrict t = ∫⁻ (a : α) in s ∩ t, f a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ = c * μ s

Tactic:
lintegral_indicator₀ hs,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ ∫⁻ (a : α) in s, c ∂μ = c * μ s
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ ∫⁻ (a : α), f b a ∂μ = ∫⁻ (a : α), aeSeq hf p b a ∂μ

Tactic:
rw [lintegral_congr_ae]

Goal state after:
case e'_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
f : β → α → ℝ≥0∞
hf : ∀ (b : β), AEMeasurable (f b) μ
h_directed : Directed (fun x1 x2 ↦ x1 ≤ x2) f
p : α → (β → ℝ≥0∞) → Prop := fun x f' ↦ Directed LE.le f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_directed : Directed LE.le (aeSeq hf p)
b : β
⊢ f b =ᵐ[μ] aeSeq hf p b
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_3
f : ι → α → ℝ≥0∞
u : Filter ι
inst✝ : u.IsCountablyGenerated
h_meas : ∀ (i : ι), AEMeasurable (f i) μ
hu : u.NeBot
⊢ ∫⁻ (a : α), liminf (fun i ↦ f i a) u ∂μ ≤ liminf (fun i ↦ ∫⁻ (a : α), f i a ∂μ) u

Tactic:
obtain ⟨g, hg⟩ : ∃ g : ℕ → ι,
        Tendsto (fun n => ∫⁻ a, f (g n) a ∂μ) atTop (𝓝 (liminf (fun i => ∫⁻ a, f i a ∂μ) u)) ∧
        Tendsto g atTop u :=
      exists_seq_tendsto_liminf
    calc
    _ ≤ ∫⁻ a, liminf (fun n => f (g n) a) atTop ∂μ :=
      lintegral_mono fun a => hg.2.liminf_le_liminf_comp
    _ ≤ liminf (fun n => ∫⁻ a, f (g n) a ∂μ) atTop :=
      lintegral_liminf_nat_le' (fun n => h_meas (g n))
    _ = _ := hg.1.liminf_eq

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

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
ht :
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), ν t
ht_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
⊢ ∃ t,
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t

Tactic:
refine ⟨t, ht_meas, ht_mem, ?_⟩

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
n : ℕ
hC_lt : 1 / ↑n < ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s
h_lt_top : ⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s < ∞
t : Set α
ht :
  (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), ν t
ht_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
⊢ (⨆ s, ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / ↑n ≤ ν t
Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
⊢ Tendsto (fun i ↦ (↑i)⁻¹) atTop (𝓝 0)

Tactic:
exact ENNReal.tendsto_inv_nat_nhds_zero

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ¬ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ∞ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)
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 ν)ᶜ = ∞
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ False

Tactic:
refine ENNReal.top_ne_zero ?_

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite (μ.restrict μ.sigmaFiniteSet)

Tactic:
rw [Measure.sigmaFiniteSet]
  infer_instance

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 : 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∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
have I : ∀ n x, g n x ≤ g' n x := by
    intro n x
    cases n with | zero | succ => simp [g']

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 ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
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' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
⊢ ∃ K', ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑K' * edist x y

Tactic:
let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.sdiff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
⊢ ∃ K', ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑K' * edist x y
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' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
have (x) (hx : x ∈ s) : ∃ K' : ℝ≥0, ∀ y ∈ s.diff (ball x (ε x hx)),
      edist (f x) (f y) ≤ K' * edist x y := by
    let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.sdiff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
    refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
    simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
    refine (div_le_iff₀ ?_).1 ?_
    · exact NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)
    · simp [← NNReal.coe_le_coe, (mem_upperBounds.1 hK') _ <| mem_image_of_mem _ hy]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
this : ∀ (x : α) (hx : x ∈ s), ∃ K', ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ ↑K' * edist x y
⊢ ∃ K, LipschitzOnWith K f s
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 ∂μ ≠ ∞
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∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
have : ∀ᵐ a ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a)) := by
    apply tendsto_of_lintegral_tendsto_of_monotone_aux _ hF_meas _ _ _ h_int_finite
    · exact fun n ↦ (M n).aemeasurable
    · simp_rw [Int_eq]
      exact hf_tendsto
    · exact Eventually.of_forall (fun x ↦ monotone_nat_of_le_succ (fun n ↦ le_max_right _ _))
    · filter_upwards [h_bound, I'] with x h'x hx n using (hx n).trans (h'x n)

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 ∂μ
g' : ℕ → α → ℝ≥0∞ := fun t ↦ Nat.rec (motive := fun x ↦ α → ℝ≥0∞) (g 0) (fun n I x ↦ max (g (n + 1) x) (I x)) t
M : ∀ (n : ℕ), Measurable (g' n)
I : ∀ (n : ℕ) (x : α), g n x ≤ g' n x
I' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), g' n x ≤ f n x
Int_eq : ∀ (n : ℕ), ∫⁻ (x : α), g' n x ∂μ = ∫⁻ (x : α), f n x ∂μ
this : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ g' i a) atTop (𝓝 (F a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
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
⊢ glueDist Φ Ψ ε (Sum.inl x) (Sum.inl z) ≤
    glueDist Φ Ψ ε (Sum.inl x) (Sum.inr y) + glueDist Φ Ψ ε (Sum.inr y) (Sum.inl z)

Tactic:
simp_rw [glueDist, add_add_add_comm _ ε, add_assoc]

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
⊢ dist x z ≤ (⨅ p, dist x (Φ p) + dist y (Ψ p)) + ((⨅ p, dist z (Φ p) + dist y (Ψ p)) + (ε + ε))
Module: Mathlib.Topology.MetricSpace.CantorScheme

Goal state before:
pp: case refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : y ∈ Subtype.val ⁻¹' cylinder (↑x) n
⊢ dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε

Tactic:
mem_preimage,

Goal state after:
case refine_1
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝² : PseudoMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
hA : VanishingDiam A
x : ↑(inducedMap A).fst
ε : ℝ
ε_pos : ε > 0
n : ℕ
hn : ∀ y ∈ A (res (↑x) n), ∀ z ∈ A (res (↑x) n), dist y z < ε
y : ↑(inducedMap A).fst
hyx : ↑y ∈ cylinder (↑x) n
⊢ dist ((inducedMap A).snd y) ((inducedMap A).snd x) < ε
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)
⊢ ClosureAntitone D

Tactic:
refine Antitone.closureAntitone ?_ fun l => (DP l).property.1.closed

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)
⊢ CantorScheme.Antitone D
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ ∫⁻ (a : β), s.indicator (fun x ↦ c) a ∂Measure.map f μ = c * μ (f ⁻¹' s)

Tactic:
lintegral_indicator_const hs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
s : Set β
hf : Measurable f
hs : MeasurableSet s
c : ℝ≥0∞
⊢ c * (Measure.map f μ) s = c * μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f a
⊢ f₀.lintegral (Measure.map g μ) ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f (g a)), g_1.lintegral μ

Tactic:
SimpleFunc.lintegral_map _ hg.measurable

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
g : α → β
hg : MeasurableEmbedding g
f : β → ℝ≥0∞
f₀ : SimpleFunc β ℝ≥0∞
hf₀ : ⇑f₀ ≤ fun a ↦ f a
⊢ (f₀.comp g ⋯).lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f (g a)), g_1.lintegral μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
a : α
h : a ∈ s
⊢ (dirac a) s = 1

Tactic:
by
  have : ∀ t : Set α, a ∈ t → t.indicator (1 : α → ℝ≥0∞) a = 1 := fun t ht => indicator_of_mem ht 1
  refine le_antisymm (this univ trivial ▸ ?_) (this s h ▸ le_dirac_apply)
  rw [← dirac_apply' a MeasurableSet.univ]
  exact measure_mono (subset_univ s)

Goal state after:
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
y : α
⊢ ∃ a, g a = y

Tactic:
by
    have : ∀ n : ℕ, ∃ j, y ∈ closedBall (u j) ((1 / 2) ^ n) := fun n ↦ by
      rcases hu.exists_dist_lt y (by simp : (0 : ℝ) < (1 / 2) ^ n) with ⟨j, hj⟩
      exact ⟨j, hj.le⟩
    choose x hx using this
    have I : (⋂ n : ℕ, closedBall (u (x n)) ((1 / 2) ^ n)).Nonempty := ⟨y, mem_iInter.2 hx⟩
    refine ⟨⟨x, I⟩, ?_⟩
    refine dist_le_zero.1 ?_
    have J : ∀ n : ℕ, dist (g ⟨x, I⟩) y ≤ (1 / 2) ^ n + (1 / 2) ^ n := fun n =>
      calc
        dist (g ⟨x, I⟩) y ≤ dist (g ⟨x, I⟩) (u (x n)) + dist y (u (x n)) :=
          dist_triangle_right _ _ _
        _ ≤ (1 / 2) ^ n + (1 / 2) ^ n := add_le_add (A ⟨x, I⟩ n) (hx n)
    have L : Tendsto (fun n : ℕ => (1 / 2 : ℝ) ^ n + (1 / 2) ^ n) atTop (𝓝 (0 + 0)) :=
      (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1).add
        (tendsto_pow_atTop_nhds_zero_of_lt_one I0.le I1)
    rw [add_zero] at L
    exact ge_of_tendsto' L J

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

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

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

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
ι : Type u_3
m : ι → Measure α
f : α → Measure β
h : AEMeasurable f (sum fun i ↦ m i)
⊢ (sum fun i ↦ m i).bind f = sum fun i ↦ (m i).bind f

Tactic:
by
  simp_rw [bind, map_sum h, join_sum]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
μ : Measure (Measure α)
⊢ (map (map f) μ).join = map f μ.join

Tactic:
by
  ext1 s hs
  rw [join_apply hs, map_apply hf hs, join_apply (hf hs),
    lintegral_map (measurable_coe hs) (measurable_map f hf)]
  simp_rw [map_apply hf hs]

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

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

Tactic:
cases isEmpty_or_nonempty X
  · exact continuous_of_discreteTopology
  refine continuous_projIcc.comp <| Continuous.dist continuous_id' ?_
  convert! continuous_const (y := denseSeq X n)

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 ν
s : Set α
t : Set β
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)

Tactic:
set ST := toMeasurable (μ.prod ν) (s ×ˢ t)

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝ : SFinite ν
s : Set α
t : Set β
ST : Set (α × β) := toMeasurable (μ.prod ν) (s ×ˢ t)
⊢ μ s * ν t ≤ (μ.prod ν) (s ×ˢ t)
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
⊢ μ.prod ν ≪ μ'.prod ν'

Tactic:
refine AbsolutelyContinuous.mk fun s hs h2s => ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ μ' : Measure α
ν ν' : Measure β
inst✝ : SFinite ν'
h1 : μ ≪ μ'
h2 : ν ≪ ν'
s : Set (α × β)
hs : MeasurableSet s
h2s : (μ'.prod ν') s = 0
⊢ (μ.prod ν) s = 0
Module: Mathlib.MeasureTheory.Group.MeasurableEquiv

Goal state before:
pp: 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
⊢ map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) (μ + ν) =
    map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) μ + map (fun x ↦ DomMulAct.mk.symm g⁻¹ • x) ν

Tactic:
rw [Measure.map_add]

Goal state after:
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