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

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ Tendsto (fun i ↦ (As i).indicator fun x ↦ b) L (𝓝 (A.indicator fun x ↦ b)) ↔
    Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))

Tactic:
tendsto_indicator_const_iff_forall_eventually' _ b nhds_b nhds_o,

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ Tendsto (fun i x ↦ x ∈ As i) L (pi fun x ↦ pure (x ∈ A))
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝¹ : Zero β
inst✝ : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
b : β
nhds_b : {0}ᶜ ∈ 𝓝 b
nhds_o : {b}ᶜ ∈ 𝓝 0
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), Tendsto (fun x ↦ i ∈ As x) L (pure (i ∈ A))

Tactic:
simp_rw [tendsto_pure]

Goal state after:
α : Type u_1
A : Set α
β : Type u_2
inst✝³ : Zero β
inst✝² : TopologicalSpace β
ι : Type u_3
L : Filter ι
As : ι → Set α
inst✝¹ : T1Space β
b : β
inst✝ : NeZero b
⊢ (∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A) ↔ ∀ (i : α), ∀ᶠ (x : ι) in L, (i ∈ As x) = (i ∈ A)
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 ↦ if r = 0 then 0 else ∞

Tactic:
exact measurable_const.piecewise (measurableSet_singleton _) measurable_const

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

Goal state before:
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 ↦ if r = 0 then 0 else ∞

Tactic:
exact measurable_const.piecewise (measurableSet_singleton _) measurable_const

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

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ≥0
hf : Measurable f
μ : Measure α
inst✝ : SigmaFinite μ
sigma_finite_sets : ℕ → Set α := spanningSets μ
norm_sets : ℕ → Set α := fun n ↦ {x | f x ≤ ↑n}
norm_sets_spanning : ⋃ n, norm_sets n = univ
sets : ℕ → Set α := fun n ↦ sigma_finite_sets n ∩ norm_sets n
h_meas : ∀ (n : ℕ), MeasurableSet (sets n)
h_finite : ∀ (n : ℕ), μ (sets n) < ∞
this : ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i
⊢ ⋃ i, sets i = univ

Tactic:
rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]

Goal state after:
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε

Tactic:
rw [edist_comm] at hN

Goal state after:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist (e N) x < ε
⊢ ∃ ia, True ∧ ∀ x_1 ∈ Ici ia, (nearestPt e x_1) x ∈ eball x ε
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx :
  f x ∈
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (Subtype.val '' closure[instTopologicalSpaceSubtype] (range (denseSeq ↑s)))
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (range (denseSeq ↑s)) ⊆
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (range fun k ↦ Nat.casesOn k y₀ (Subtype.val ∘ denseSeq ↑s))

Tactic:
simp -iota only [Nat.range_casesOn, closure_union, range_comp]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
this : Nonempty ↑s
hx :
  f x ∈
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (Subtype.val '' closure[instTopologicalSpaceSubtype] (range (denseSeq ↑s)))
⊢ Subtype.val '' closure[instTopologicalSpaceSubtype] (range (denseSeq ↑s)) ⊆
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {y₀} ∪
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (Subtype.val '' range (denseSeq ↑s))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (⨅ x ∈ s, f x) * μ s ≤ ∫⁻ (x : α) in s, f x ∂μ

Tactic:
calc (⨅ x ∈ s, f x) * μ s
  _ = ∫⁻ y in s, ⨅ x ∈ s, f x ∂μ := by simp
  _ ≤ ∫⁻ x in s, f x ∂μ := setLIntegral_mono' hs fun x hx ↦ iInf₂_le x hx

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), (⨅ n, aeSeq h_meas p n) a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
simp_rw [iInf_apply]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
h_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (a : α) ∂μ, Antitone fun i ↦ f i a
h_fin : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Antitone f'
hp : ∀ᵐ (x : α) ∂μ, p x fun i ↦ f i x
h_ae_seq_mono : Antitone (aeSeq h_meas p)
⊢ ∫⁻ (a : α), ⨅ i, aeSeq h_meas p i a ∂μ = ⨅ n, ∫⁻ (a : α), f n a ∂μ
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Sub

Goal state before:
pp: case intro.inr
α : 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 β
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ

Tactic:
have : ∀ a, ⨅ b, f b a = ⨅ n, f (h_directed.sequence f n) a := by
    refine fun a =>
      le_antisymm (le_iInf fun n => iInf_le _ _)
        (le_iInf fun b => iInf_le_of_le (Encodable.encode b + 1) ?_)
    exact h_directed.sequence_le b a

Goal state after:
case intro.inr
α : 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
⊢ ∫⁻ (a : α), ⨅ b, f b a ∂μ = ⨅ b, ∫⁻ (a : α), f b a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | g x ≠ 0}
h : g x = 0
⊢ Tendsto (fun n ↦ ((fun n ↦ hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}) n) x) atTop (𝓝 ((f / g) x))

Tactic:
simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_ofPred_eq,
      not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]

Goal state after:
case pos
α : Type u_1
β : Type u_2
f g : α → β
mα : MeasurableSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : GroupWithZero β
inst✝² : ContinuousMul β
inst✝¹ : ContinuousInv₀ β
inst✝ : MetrizableSpace β
hf : StronglyMeasurable f
hg : StronglyMeasurable g
this✝¹ : MeasurableSpace β := borel β
this✝ : BorelSpace β
x : α
this : MeasurableSet {x | ¬g x = 0}
h : g x = 0
⊢ Tendsto (fun n ↦ 0) atTop (𝓝 0)
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))
this : F' =ᵐ[μ] F
a : α
h_eq : F' a = F a
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) → Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
h_tendsto

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))
this : F' =ᵐ[μ] F
a : α
h_eq : F' a = F a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
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))
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) → F' a ≤ F a

Tactic:
h_tendsto

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))
a : α
h_le : ∀ (i : ℕ), f i a ≤ F a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F' a ≤ F a
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds 0)

Tactic:
← mul_zero (K : ℝ)

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds (↑K * 0))
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
apply (hf.dist_le_mul _ (A n) _ (A m)).trans

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ ↑K * dist (u n) (u m) ≤ (fun n ↦ ↑K * b n) N
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds 0)

Tactic:
← mul_zero (K : ℝ)

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (fun n ↦ ↑K * b n) atTop (nhds (↑K * 0))
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' : ℝ
hK' : K' ∈ upperBounds ((fun y ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ edist (f x) (f y) ≤ ↑(NNReal.mk (max K' 0) ⋯) * edist x y

Tactic:
simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]

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)))
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ ↑(σ 0) = ↑1

Tactic:
by simp [symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: ⊢ ↑(σ 1) = ↑0

Tactic:
by simp [symm]

Goal state after:
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: x : ↑I
⊢ ↑(σ (σ x)) = ↑x

Tactic:
by simp [symm]

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 ∂μ ≠ ∞
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))
this : F' =ᵐ[μ] F
a : α
h_eq : F' a = F a
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) → Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))

Tactic:
h_tendsto

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)
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))
this : F' =ᵐ[μ] F
a : α
h_eq : F' a = F a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F a))
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 ∂μ ≠ ∞
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))
a : α
h_le : ∀ (i : ℕ), F a ≤ f i a
⊢ Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) → F a ≤ F' a

Tactic:
h_tendsto

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)
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))
a : α
h_le : ∀ (i : ℕ), F a ≤ f i a
h_tendsto : Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a))
⊢ F a ≤ F' a
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
ht : ¬↑t = 1
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z

Tactic:
have : (1 - s * t : ℝ) ≠ 0 := by
        intro h
        have : 1 ≤ (t : ℝ) := by nlinarith [s.2.2, t.2.1]
        grind

Goal state after:
case neg
a b : ℝ
x y z : ↑(Icc a b)
s t : ↑unitInterval
hs : ¬↑s = 1
ht : ¬↑t = 1
this : 1 - ↑s * ↑t ≠ 0
⊢ (1 - ↑s) * ↑x + ↑s * ((1 - ↑t) * ↑y + ↑t * ↑z) =
    (1 - ↑s * ↑t) * ((1 - ↑s * (1 - ↑t) / (1 - ↑s * ↑t)) * ↑x + ↑s * (1 - ↑t) / (1 - ↑s * ↑t) * ↑y) + ↑s * ↑t * ↑z
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
h : x ∈ cylinder y i
this : firstDiff x y < i
⊢ False

Tactic:
exact apply_firstDiff_ne hne (h _ this)

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

Goal state before:
pp: case mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
hne : x ≠ y
i : ℕ
⊢ x ∈ cylinder y i → i ≤ firstDiff x y

Tactic:
intro h
    by_contra!
    exact apply_firstDiff_ne hne (h _ this)

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

Goal state before:
pp: case refine_4
α : Type u_1
β : Type u_2
inst✝ : MetricSpace α
s : Opens α
t : Set s.CompleteCopy
⊢ IsOpen t ↔ ∀ x ∈ t, ∃ ε > 0, ∀ (y : s.CompleteCopy), dist x y < ε → y ∈ t

Tactic:
· refine ⟨fun h x hx ↦ ?_, fun h ↦ isOpen_iff_mem_nhds.2 fun x hx ↦ ?_⟩
    · rcases (Metric.isOpen_iff (α := s)).1 h x hx with ⟨ε, ε0, hε⟩
      exact ⟨ε, ε0, fun y hy ↦ hε <| (dist_comm _ _).trans_lt <| (dist_val_le_dist _ _).trans_lt hy⟩
    · rcases h x hx with ⟨ε, ε0, hε⟩
      simp only [dist_eq, one_div] at hε
      have : Tendsto (fun y : s ↦ dist x.1 y.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist y.1 sᶜ)⁻¹|)
          (𝓝 x) (𝓝 (dist x.1 x.1 + |(infDist x.1 sᶜ)⁻¹ - (infDist x.1 sᶜ)⁻¹|)) := by
        refine (tendsto_const_nhds.dist continuous_subtype_val.continuousAt).add
          (tendsto_const_nhds.sub <| ?_).abs
        refine (continuousAt_inv_infDist_pt ?_).comp continuous_subtype_val.continuousAt
        rw [s.isOpen.isClosed_compl.closure_eq, mem_compl_iff, not_not]
        exact x.2
      simp only [dist_self, sub_self, abs_zero, zero_add] at this
      exact mem_of_superset (this <| gt_mem_nhds ε0) hε

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α

Tactic:
rw [← f.induced_symm]

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed[inst✝¹] s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map

Goal state before:
pp: case refine_2
α : 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 (g a)
⊢ f₀.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a), g_1.lintegral (Measure.map g μ)

Tactic:
← f₀.extend_comp_eq hg (const _ 0),

Goal state after:
case refine_2
α : 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 (g a)
⊢ ((f₀.extend g hg (const β 0)).comp g ⋯).lintegral μ ≤
    ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a ↦ f a), g_1.lintegral (Measure.map g μ)