mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ (m.toMeasure h) s = m s

Tactic:
refine le_antisymm ?_ (le_toMeasure_apply _ _ _)
  rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩
  calc
    m.toMeasure h s = m.toMeasure h t := measure_congr heq.symm
    _ = m t := toMeasure_apply m h htm
    _ ≤ m s := m.mono hts

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ (x ∈ t') = (x ∈ t)

Tactic:
simp only [eq_iff_iff]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : t ⊆ s
h : NullMeasurableSet t (μ.restrict s)
t' : Set α
t'_subs : t' ⊆ t
ht' : MeasurableSet t'
t't : t' =ᵐ[μ.restrict s] t
this : ∀ᵐ (x : α) ∂μ, x ∈ s → (x ∈ t' ↔ x ∈ t)
x : α
hx : x ∈ s → (x ∈ t' ↔ x ∈ t)
⊢ x ∈ t' ↔ x ∈ t
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
h : NeZero (Measure.map f μ)
⊢ AEMeasurable f μ

Tactic:
by
  by_contra h'
  simp [h'] at h

Goal state after:
Module: Mathlib.Topology.GDelta.MetrizableSpace

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
this✝ : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left✝ : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun i ↦ id (U i)
⊢ IsGδ {x | Filter.Tendsto (fun x ↦ (f x.1, f x.2)) (nhds x ×ˢ nhds x) (uniformity Y)}

Tactic:
simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis,
    forall_prop_of_true, ofPred_forall]

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : PseudoMetrizableSpace Y
f : X → Y
this✝ : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left✝ : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun i ↦ id (U i)
⊢ IsGδ (⋂ i, {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U i)})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: case sUnion
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
⊢ MeasurableSet (⋃₀ f)

Tactic:
rw [← vu]

Goal state after:
case sUnion
α : Type u_1
s : Set (Set α)
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
hs : t = TopologicalSpace.generateFrom s
u : Set α
f : Set (Set α)
hf : ∀ s_1 ∈ f, GenerateOpen s s_1
ih : ∀ s_1 ∈ f, MeasurableSet s_1
v : Set (Set α)
hv : v.Countable
vf : v ⊆ f
vu : ⋃₀ v = ⋃₀ f
⊢ MeasurableSet (⋃₀ v)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ ⋃ n, F n = U

pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F

Tactic:
· show ⋃ n, F n = U
    refine Subset.antisymm (by simp only [iUnion_subset_iff, F_subset, forall_const]) fun x hx => ?_
    have : x ∉ Uᶜ := by simpa using hx
    rw [mem_iff_infEDist_zero_of_closed hU.isClosed_compl] at this
    have B : 0 < infEDist x Uᶜ := by simpa [pos_iff_ne_zero] using this
    have : Filter.Tendsto (fun n => a ^ n) atTop (𝓝 0) :=
      ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one a_lt_one
    rcases ((tendsto_order.1 this).2 _ B).exists with ⟨n, hn⟩
    simp only [mem_iUnion]
    exact ⟨n, hn.le⟩

Goal state after:
case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
U : Set α
hU : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
a : ℝ≥0∞
a_pos : 0 < a
a_lt_one : a < 1
F : ℕ → Set α := fun n ↦ (fun x ↦ infEDist x Uᶜ) ⁻¹' Ici (a ^ n)
F_subset : ∀ (n : ℕ), F n ⊆ U
⊢ Monotone F
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
r : ℝ≥0∞
H1 : ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ r
H2 : ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ r
x : α
xs : x ∈ s
y : α
yt : y ∈ t
hy : edist x y ≤ r
⊢ infEDist x t ≤ r

Tactic:
exact le_trans (infEDist_le_edist_of_mem yt) hy

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

Goal state before:
pp: case right
α : Type u
inst✝ : PseudoEMetricSpace α
s t u : Set α
⊢ ∀ i ∈ u, infEDist i s ≤ hausdorffEDist s t + hausdorffEDist t u

Tactic:
change ∀ x ∈ u, infEDist x s ≤ hausdorffEDist s t + hausdorffEDist t u
    exact fun x xu =>
      calc
        infEDist x s ≤ infEDist x t + hausdorffEDist t s :=
          infEDist_le_infEDist_add_hausdorffEDist
        _ ≤ hausdorffEDist u t + hausdorffEDist t s := by grw [infEDist_le_hausdorffEDist_of_mem xu]
        _ = hausdorffEDist s t + hausdorffEDist t u := by simp [hausdorffEDist_comm, add_comm]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ hausdorffEDist s (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = 0

Tactic:
hausdorffEDist_zero_iff_closure_eq_closure,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
    closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ hausdorffEDist s t = 0 ↔ s = t

Tactic:
hausdorffEDist_zero_iff_closure_eq_closure,

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s =
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t ↔
    s = t
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case right
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
i : ι
x : α
hx : x ∈ t i
⊢ infEDist x (s i) ≤ max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

Tactic:
· exact le_max_of_le_right <| le_iSup₂_of_le x hx le_rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam (cthickening (↑ε) s) ≤ ediam s + 2 * ↑ε

Tactic:
by
  refine ediam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => ?_
  rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy
  have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
  replace hx := hx.trans_lt hε
  obtain ⟨x', hx', hxx'⟩ := infEDist_lt_iff.mp hx
  calc
    edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
    _ ≤ ε + δ + (infEDist y s + ediam s) :=
      add_le_add hxx'.le (edist_le_infEDist_add_ediam hx')
    _ ≤ ε + δ + (ε + ediam s) := by grw [hy]
    _ = _ := by rw [two_mul]; ac_rfl

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ infDist x {y} = dist x y

Tactic:
simp [infDist, dist_edist]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
⊢ ∃ y ∈ t, dist x y < r

Tactic:
have : hausdorffEDist s t < ENNReal.ofReal r := by
    rwa [hausdorffDist, ← ENNReal.toReal_ofReal (le_of_lt r0),
      ENNReal.toReal_lt_toReal fin ENNReal.ofReal_ne_top] at H

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
x : α
r : ℝ
h : x ∈ s
H : hausdorffDist s t < r
fin : hausdorffEDist s t ≠ ∞
r0 : 0 < r
this : hausdorffEDist s t < ENNReal.ofReal r
⊢ ∃ y ∈ t, dist x y < r
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
⊢ c < ⨆ i, f i x ↔ ∃ i, ∃ (_ : i ∈ J), c < f i x

Tactic:
lt_iSup_iff

Goal state after:
β : Type u_2
δ : Type u_4
inst✝⁶ : TopologicalSpace β
mβ : MeasurableSpace β
inst✝⁵ : BorelSpace β
mδ : MeasurableSpace δ
inst✝⁴ : CompleteLinearOrder β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
ι : Type u_5
inst✝¹ : TopologicalSpace ι
inst✝ : SeparableSpace ι
f : ι → δ → β
mf : ∀ (t : ι), Measurable (f t)
cf : ∀ (x : δ), LowerSemicontinuous fun x_1 ↦ f x_1 x
c : β
J : Set ι
cJ : J.Countable
dJ : Dense J
x : δ
⊢ (∃ i, c < f i x) ↔ ∃ i, ∃ (_ : i ∈ J), c < f i x
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet ((fun x1 x2 ↦ x1 ×ˢ x2) s t)

Tactic:
dsimp only

Goal state after:
case a
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
s : Set α
hs : s ∈ C
t : Set β
ht : t ∈ D
⊢ MeasurableSet (s ×ˢ t)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_3
γ : Type u_4
inst✝ : MeasurableSingletonClass α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : α
f : γ → β
hf : MeasurableEmbedding f
⊢ ∀ ⦃s : Set γ⦄, MeasurableSet s → MeasurableSet ((fun y ↦ (x, f y)) '' s)

Tactic:
by
    intro s hs
    convert! (MeasurableSet.singleton x).prod (hf.measurableSet_image.mpr hs)
    ext x
    simp [Prod.ext_iff, eq_comm, ← exists_and_left, and_left_comm]

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : i k ≤ f a
⊢ i k ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k

pp: case neg
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k

Tactic:
· exact le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : CompleteLattice β
inst✝³ : OrderClosedTopology β
inst✝² : Zero β
inst✝¹ : MeasurableSpace β
inst✝ : OpensMeasurableSpace β
i : ℕ → β
f : α → β
a : α
hf : Measurable f
h_zero : 0 = ⊥
n k : ℕ
x✝ : k ∈ Finset.range n
h : ¬i k ≤ f a
⊢ ⊥ ≤ ⨆ k, ⨆ (_ : i k ≤ f a), i k
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ ∑ x ∈ (const α c).range, x * μ (⇑(const α c) ⁻¹' {x}) = c * μ univ

Tactic:
simp only [range_const, coe_const, Finset.sum_singleton]

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
h✝ : Nonempty α
⊢ c * μ (Function.const α c ⁻¹' {c}) = c * μ univ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet ((fun a ↦ Ioi ↑a) q)

Tactic:
dsimp only

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Ioi ↑q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Iic ↑a) q)

Tactic:
dsimp only

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Iic ↑q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet ((fun a ↦ Iio ↑a) q)

Tactic:
dsimp only

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Iio ↑q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Ici ↑a) q)

Tactic:
dsimp only

Goal state after:
case refine_2
q : ℚ
⊢ MeasurableSet (Ici ↑q)
Module: Mathlib.MeasureTheory.Function.SimpleFuncDense

Goal state before:
pp: case succ
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : PseudoEMetricSpace α
inst✝ : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ}, k ≤ N → edist ((nearestPt e N) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
⊢ edist ((nearestPt e (N + 1)) x) x ≤ edist (e k) x

Tactic:
simp only [nearestPt, nearestPtInd_succ, map_apply]
    split_ifs with h
    · rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
    · push Not at h
      rcases h with ⟨l, hlN, hxl⟩
      rcases hk.eq_or_lt with (rfl | hk)
      exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]

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

Goal state before:
pp: case zero
α : 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
n : ℕ
x : β
this : Nonempty ↑s
⊢ Nat.casesOn 0 y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s

pp: case succ
α : 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
n✝ : ℕ
x : β
this : Nonempty ↑s
n : ℕ
⊢ Nat.casesOn (n + 1) y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s

Tactic:
exacts [h₀, Subtype.mem _]

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ ∫⁻ (x : α), 1 ∂μ = μ univ

Tactic:
rw [lintegral_const, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
| ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))

Tactic:
x,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Nonempty β
inst✝ : T2Space β
hα : Nonempty α
hf : StronglyMeasurable f
fs : ℕ → α →ₛ β := hf.approx
h_fs_tendsto : ∀ (x : α), Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
this : ∀ (n : ℕ), ∃ c, ∀ (x : α), (fs n) x = c
cs : ℕ → β := fun n ↦ ⋯.choose
h_cs_eq : ∀ (n : ℕ), ⇑(fs n) = fun x ↦ cs n
x : α
| Tendsto (fun n ↦ (fs n) x) atTop (𝓝 (f x))
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᵐ[μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ (fun a ↦ g (f a)) a = (fun a ↦ g (f' a)) a

Tactic:
dsimp only

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
f f' : α → β
h✝ : f =ᵐ[μ] f'
g : β → ℝ≥0∞
a : α
h : f a = f' a
⊢ g (f a) = g (f' a)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᵐ[μ] f₁'
h₂✝ : f₂ =ᵐ[μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ (fun a ↦ g (f₁ a) (f₂ a)) x✝ = (fun a ↦ g (f₁' a) (f₂' a)) x✝

Tactic:
dsimp only

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
μ : Measure α
f₁ f₁' : α → β
f₂ f₂' : α → γ
h₁✝ : f₁ =ᵐ[μ] f₁'
h₂✝ : f₂ =ᵐ[μ] f₂'
g : β → γ → ℝ≥0∞
x✝ : α
h₂ : f₂ x✝ = f₂' x✝
h₁ : f₁ x✝ = f₁' x✝
⊢ g (f₁ x✝) (f₂ x✝) = g (f₁' x✝) (f₂' x✝)
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
hm : ∀ (i : β), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ = ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
by
  simp only [Measure.restrict_iUnion_ae hd hm, lintegral_sum_measure]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable β
s : β → Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in ⋃ i, s i, f a ∂μ ≤ ∑' (i : β), ∫⁻ (a : α) in s i, f a ∂μ

Tactic:
rw [← lintegral_sum_measure]
  exact lintegral_mono' restrict_iUnion_le le_rfl

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ∞
f : α → ℝ≥0∞
hbdd : ∃ y, ∀ x ∈ s, f x ≤ ↑y
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞

Tactic:
obtain ⟨M, hM⟩ := hbdd

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ ∞
f : α → ℝ≥0∞
M : ℝ≥0
hM : ∀ x ∈ s, f x ≤ ↑M
⊢ ∫⁻ (x : α) in s, f x ∂μ < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (a : α), ⨆ n, (const α r * eapprox f n) a ∂μ = ⨆ n, r * (eapprox f n).lintegral μ

Tactic:
by
      rw [lintegral_iSup]
      · congr
        funext n
        rw [← SimpleFunc.const_mul_lintegral, ← SimpleFunc.lintegral_eq_lintegral]
      · intro n
        exact SimpleFunc.measurable _
      · intro i j h a
        dsimp
        gcongr
        exact monotone_eapprox _ h _

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ

Tactic:
lintegral_const_mul _ hf.measurable_mk

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
r : ℝ≥0∞
f : α → ℝ≥0∞
hf : AEMeasurable f μ
A : ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
B : ∫⁻ (a : α), r * f a ∂μ = ∫⁻ (a : α), r * AEMeasurable.mk f hf a ∂μ
⊢ r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = r * ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
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 : ℕ
⊢ ∫⁻ (x : α), f n x ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ

Tactic:
hg n

Goal state after:
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∞ := 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
n : ℕ
⊢ ∫⁻ (a : α), g n a ∂μ ≤ ∫⁻ (x : α), g' n x ∂μ
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 ≤ n, N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N

Tactic:
N

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 : ℕ
⊢ N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun n ↦ ↑K * b n) N
Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
replace hf : ∀ x ∈ s, ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s) := fun x hx ↦ by
    let ⟨K, t, ht, hf⟩ := hf hx
    let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
    exact ⟨ε, hε, K, hf.mono hε'⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
hf : ∀ x ∈ s, ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s)
⊢ ∃ K, LipschitzOnWith K f s
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: α : Type u_2
x : ℕ → α
n : ℕ
⊢ (res x n).length = n

Tactic:
induction n

Goal state after:
case zero
α : Type u_2
x : ℕ → α
⊢ (res x 0).length = 0

case succ
α : Type u_2
x : ℕ → α
n✝ : ℕ
a✝ : (res x n✝).length = n✝
⊢ (res x (n✝ + 1)).length = n✝ + 1