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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ map f (sum fun i ↦ m ↑i) = sum fun i ↦ map f (m ↑i)

Tactic:
Measure.map_sum

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ (sum fun i ↦ map f (m ↑i)) = sum fun i ↦ map f (m ↑i)

α : Type u_2
m0 : MeasurableSpace α
ι : Type u_7
β : Type u_8
mβ : MeasurableSpace β
m : ι → Measure α
f : α → β
s : Finset ι
hf : AEMeasurable f (∑ i ∈ s, m i)
⊢ AEMeasurable f (sum fun i ↦ m ↑i)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
a : α
⊢ (⨅ x, 𝓟 ↑x).IsMeasurablyGenerated

Tactic:
refine @Filter.iInf_isMeasurablyGenerated α _ _ _ fun i => ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst✝¹² : TopologicalSpace α
inst✝¹¹ : MeasurableSpace α
inst✝¹⁰ : OpensMeasurableSpace α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : MeasurableSpace β
inst✝⁷ : OpensMeasurableSpace β
inst✝⁶ : TopologicalSpace γ
inst✝⁵ : MeasurableSpace γ
inst✝⁴ : BorelSpace γ
inst✝³ : TopologicalSpace γ₂
inst✝² : MeasurableSpace γ₂
inst✝¹ : BorelSpace γ₂
inst✝ : MeasurableSpace δ
a : α
i : Subtype (Membership.mem {s | a ∈ s ∧ IsOpen[inst✝¹²] s})
⊢ (𝓟 ↑i).IsMeasurablyGenerated
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

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

Tactic:
exact infEDist_zero_of_mem h

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ↔ infEDist x s = 0

Tactic:
rw [← mem_closure_iff_infEDist_zero, h.closure_eq]

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

Goal state before:
pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
x : α
xs : x ∈ s
y : α
yt : y ∈ t
z : α
hz : z ∈ t
⊢ ∃ y ∈ s, edist z y ≤ ediam (s ∪ t)

Tactic:
exact ⟨x, xs, Metric.edist_le_ediam_of_mem (subset_union_right hz) (subset_union_left xs)⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + ediam s) = ediam s + 2 * ↑ε + ↑δ

Tactic:
rw [two_mul]

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : ediam s + 2 * ↑ε < ∞
hε : ↑ε < ↑ε + ↑δ
hx : infEDist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + ediam s) = ediam s + (↑ε + ↑ε) + ↑δ
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ infDist x s ≠ 0

Tactic:
Ne,

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs : s.Nonempty
⊢ ¬infDist x s = 0
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case H1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ s, ∃ y ∈ t, edist x y ≤ ENNReal.ofReal (max rs rt)

pp: case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)

Tactic:
· intro x xs
      exists ct, hct
      have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _)
      rwa [edist_dist, ENNReal.ofReal_le_ofReal_iff]
      exact le_trans dist_nonneg this

Goal state after:
case H2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
cs : α
hcs : cs ∈ s
ct : α
hct : ct ∈ t
rs : ℝ
hrs : s ⊆ closedBall ct rs
rt : ℝ
hrt : t ⊆ closedBall cs rt
⊢ ∀ x ∈ t, ∃ y ∈ s, edist x y ≤ ENNReal.ofReal (max rs rt)
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
⊢ cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ'

Tactic:
refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
E : Set α
δ δ' : ℝ
hδ₀ : 0 < δ'
hδδ' : δ < δ'
x : α
hx : x ∈ thickening δ' E
⊢ x ∈ ⋃ x ∈ E, closedBall x δ'
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ hausdorffDist ∅ s = 0

Tactic:
simp [hausdorffDist_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : s.Nonempty
hs_ne_univ : s ≠ univ
x y : β
⊢ (piecewise s hs (const α x) (const α y)).range = {x, y}

Tactic:
simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const,
    Finset.coe_insert, Finset.coe_singleton, hs_nonempty.image_const,
    (nonempty_compl.2 hs_ne_univ).image_const, singleton_union, Function.const]

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

Goal state before:
pp: α : 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, (approx i f n) a = ⨆ k, ⨆ (_ : i k ≤ f a), i k

Tactic:
refine le_antisymm (iSup_le fun n => ?_) (iSup_le fun k => iSup_le fun hk => ?_)
  · rw [approx_apply a hf, h_zero]
    refine Finset.sup_le fun k _ => ?_
    split_ifs with h
    · exact le_iSup_of_le k (le_iSup (fun _ : i k ≤ f a => i k) h)
    · exact bot_le
  · refine le_iSup_of_le (k + 1) ?_
    rw [approx_apply a hf]
    have : k ∈ Finset.range (k + 1) := Finset.mem_range.2 (Nat.lt_succ_self _)
    refine le_trans (le_of_eq ?_) (Finset.le_sup this)
    rw [if_pos hk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∑ i ∈ f.range with g i = g (f a), g (f a) * μ (⇑f ⁻¹' {i}) = ∑ j ∈ f.range with g j = g (f a), g j * μ (⇑f ⁻¹' {j})

Tactic:
refine Finset.sum_congr ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ {b ∈ f.range | g b = g (f a)} = {j ∈ f.range | g j = g (f a)}

case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
g : β → ℝ≥0∞
f : α →ₛ β
a : α
hb : f a ∈ f.range
⊢ ∀ x ∈ {j ∈ f.range | g j = g (f a)}, g (f a) * μ (⇑f ⁻¹' {x}) = g x * μ (⇑f ⁻¹' {x})
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}

Tactic:
by
  rcases isEmpty_or_nonempty α with hα | hα
  · have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _
    simp [this]
  have A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c} := by
    intro i c
    exact measurableSet_le (hf i) measurable_const
  have B : ∀ (c : α), MeasurableSet {x | ∀ i, f i x ≤ c} := by
    intro c
    rw [ofPred_forall]
    exact MeasurableSet.iInter (fun i ↦ A i c)
  obtain ⟨u, hu⟩ : ∃ (u : ℕ → α), Tendsto u atTop atTop := exists_seq_tendsto (atTop : Filter α)
  have : {b | BddAbove (range (fun i ↦ f i b))} = {x | ∃ n, ∀ i, f i x ≤ u n} := by
    apply Subset.antisymm
    · rintro x ⟨c, hc⟩
      obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
      exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
    · rintro x ⟨n, hn⟩
      refine ⟨u n, ?_⟩
      rintro - ⟨i, rfl⟩
      exact hn i
  rw [this, ofPred_exists]
  exact MeasurableSet.iUnion (fun n ↦ B (u n))

Goal state after:
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 : α
⊢ Tendsto (fun i ↦ (As i).indicator (fun x ↦ b) x) L (𝓝 (A.indicator (fun x ↦ b) x)) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A

Tactic:
classical
  have heart := @tendsto_ite ι L β (fun i ↦ x ∈ As i) _ (x ∈ A) _ b 0 (𝓝 b) (𝓝 (0 : β))
                nhds_o nhds_b ?_ ?_
  · convert! heart
    by_cases hxA : x ∈ A <;> simp [hxA]
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds
  · simp only [principal_singleton, le_def, mem_pure]
    exact fun s s_nhds ↦ mem_of_mem_nhds s_nhds

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable g

Tactic:
apply measurable_of_isClosed'

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := ⋯
⊢ ∀ (s : Set β), IsClosed[inst✝⁵] s → s.Nonempty → s ≠ Set.univ → MeasurableSet (g ⁻¹' s)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
μ : Measure α
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), AEMeasurable (f i) μ
hlim : ∀ᵐ (a : α) ∂μ, Tendsto (fun i ↦ f i a) u (𝓝 (g a))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → ℝ≥0∞) → Prop := fun x f' ↦ Tendsto f' atTop (𝓝 (g x))
hp : ∀ᵐ (x : α) ∂μ, p x fun n ↦ f (v n) x
aeSeqLim : α → ℝ≥0∞ := fun x ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun i ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))

Tactic:
simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact aeSeq.fun_prop_of_mem_aeSeqSet h'f hx

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

Goal state before:
pp: α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
As_mble : ∀ (i : ι), MeasurableSet (As i)
h_lim : ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ MeasurableSet A

Tactic:
simp_rw [← measurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢
  exact ENNReal.measurable_of_tendsto' L As_mble
    ((tendsto_indicator_const_iff_forall_eventually L (1 : ℝ≥0∞)).mpr h_lim)

Goal state after:
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
n : ℕ
x : β
⊢ (approxOn f hf s y₀ h₀ n) x ∈ s

Tactic:
have : Nonempty s := ⟨⟨y₀, h₀⟩⟩
  suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
  rintro (_ | n)
  exacts [h₀, Subtype.mem _]

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

Goal state before:
pp: case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
⊢ Pairwise (Function.onFun Disjoint fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1)))

Tactic:
intro i j hij

Goal state after:
case hn
α : Type u_5
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
t : ℝ≥0
ht : 1 < t
A : μ s = μ (s ∩ f ⁻¹' {0}) + μ (s ∩ f ⁻¹' Ioi 0)
B : μ (s ∩ f ⁻¹' Ioi 0) = μ (s ∩ f ⁻¹' {∞}) + μ (s ∩ f ⁻¹' Ioo 0 ∞)
i j : ℤ
hij : i ≠ j
⊢ Function.onFun Disjoint (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j
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
x : α
p_eq : ¬c (rs x) = 0
⊢ r * s x ≠ 0

Tactic:
Ne,

Goal state after:
α : 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
x : α
p_eq : ¬c (rs x) = 0
⊢ ¬r * s x = 0
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ (∀ (i : Bool), AEStronglyMeasurable f (bif i then μ else ν)) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν

Tactic:
Bool.forall_bool,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : PseudoMetrizableSpace β
ν : Measure α
⊢ AEStronglyMeasurable f (bif false then μ else ν) ∧ AEStronglyMeasurable f (bif true then μ else ν) ↔
    AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add

Goal state before:
pp: α : 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'
x : α
i j z : β
hz₁ : f i ≤ f z
hz₂ : f j ≤ f z
⊢ ∃ z, (fun i ↦ f i x) i ≤ (fun i ↦ f i x) z ∧ (fun i ↦ f i x) j ≤ (fun i ↦ f i x) z

Tactic:
exact ⟨z, hz₁ x, hz₂ x⟩

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : μ ≠ 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ

Tactic:
Ne,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hμ : ¬μ = 0
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ᵐ (x : α) ∂μ, f x < g x
⊢ ∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ FinStronglyMeasurable f μ

Tactic:
by
  have : SigmaFinite (μ.restrict t) := htμ
  let S := spanningSets (μ.restrict t)
  have hS_meas : ∀ n, MeasurableSet (S n) := measurableSet_spanningSets (μ.restrict t)
  let f_approx := hf_meas.approx
  let fs n := SimpleFunc.restrict (f_approx n) (S n ∩ t)
  have h_fs_t_compl : ∀ n, ∀ x, x ∉ t → fs n x = 0 := by
    intro n x hxt
    rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]
    refine Set.indicator_of_notMem ?_ _
    simp [hxt]
  refine ⟨fs, ?_, fun x => ?_⟩
  · simp_rw [SimpleFunc.support_eq, ← Finset.mem_coe]
    classical
    refine fun n => measure_biUnion_lt_top {y ∈ (fs n).range | y ≠ 0}.finite_toSet fun y hy => ?_
    rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
    swap
    · let : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _
      rw [Finset.mem_coe, Finset.mem_filter] at hy
      exact hy.2
    refine (measure_mono Set.inter_subset_left).trans_lt ?_
    have h_lt_top := measure_spanningSets_lt_top (μ.restrict t) n
    rwa [Measure.restrict_apply' ht] at h_lt_top
  · by_cases hxt : x ∈ t
    swap
    · rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]
      exact tendsto_const_nhds
    have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x
    obtain ⟨n₁, hn₁⟩ : ∃ n, ∀ m, n ≤ m → fs m x = f_approx m x := by
      obtain ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m ∩ t := by
        rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
        · exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
        rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
        · exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩
        rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
        trivial
      refine ⟨n, fun m hnm => ?_⟩
      simp_rw [fs, SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
        Set.indicator_of_mem (hn m hnm)]
    rw [tendsto_atTop'] at h ⊢
    intro s hs
    obtain ⟨n₂, hn₂⟩ := h s hs
    refine ⟨max n₁ n₂, fun m hm => ?_⟩
    rw [hn₁ m ((le_max_left _ _).trans hm)]
    exact hn₂ m ((le_max_right _ _).trans hm)

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

Goal state before:
pp: α : 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 ∂μ = ∫⁻ (a : α), ⨅ n, (f ∘ Directed.sequence f h_directed) n a ∂μ

Tactic:
by simp only [this, Function.comp_apply]

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
⊢ ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ.trim hm = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ

Tactic:
lintegral_trim hm hf.measurable_mk

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : AEMeasurable f (μ.trim hm)
⊢ ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ = ∫⁻ (a : α), AEMeasurable.mk f hf a ∂μ
Module: Mathlib.Topology.UnitInterval

Goal state before:
pp: i j : ↑I
⊢ σ i ≤ σ j ↔ j ≤ i

Tactic:
by
  simp only [symm, Subtype.mk_le_mk, sub_le_sub_iff, add_le_add_iff_left, Subtype.coe_le_coe]

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))
hF'_le : F ≤ᵐ[μ] F'
⊢ Tendsto (fun i ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))

Tactic:
exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto

Goal state after:
Module: Mathlib.Topology.Metrizable.CompletelyMetrizable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : IsCompletelyMetrizableSpace X
⊢ TopologicalSpace.MetrizableSpace X

Tactic:
let := upgradeIsCompletelyMetrizable X
  infer_instance

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
Φ : Z → X
Ψ : Z → Y
ε : ℝ
hε : 0 < ε
s : Set ((X ⊕ Y) × (X ⊕ Y))
⊢ s ∈ 𝓤 (X ⊕ Y) ↔ ∃ δ > 0, ∀ (a b : X ⊕ Y), glueDist Φ Ψ ε a b < δ → (a, b) ∈ s

Tactic:
by
  simp only [Sum.uniformity, Filter.mem_sup, Filter.mem_map, mem_uniformity_dist, mem_preimage]
  constructor
  · rintro ⟨⟨δX, δX0, hX⟩, δY, δY0, hY⟩
    refine ⟨min (min δX δY) ε, lt_min (lt_min δX0 δY0) hε, ?_⟩
    rintro (a | a) (b | b) h <;> simp only [lt_min_iff] at h
    · exact hX h.1.1
    · exact absurd h.2 (le_glueDist_inl_inr _ _ _ _ _).not_gt
    · exact absurd h.2 (le_glueDist_inr_inl _ _ _ _ _).not_gt
    · exact hY h.1.2
  · rintro ⟨ε, ε0, H⟩
    constructor <;> exact ⟨ε, ε0, fun _ _ h => H _ _ h⟩

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

Goal state before:
pp: E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
x y : (n : ℕ) → E n
hx : x ∉ s
hy : y ∈ s
A : ∃ n, Disjoint s (cylinder x n)
⊢ firstDiff x y < Nat.find A

Tactic:
classical
  have B := Nat.find_spec A
  contrapose! B
  rw [not_disjoint_iff_nonempty_inter]
  refine ⟨y, hy, ?_⟩
  rw [mem_cylinder_comm]
  exact cylinder_anti y B (mem_cylinder_firstDiff x y)

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

Goal state before:
pp: case false
α : 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)
l : List Bool
⊢ D (false :: l) ⊆ D l

Tactic:
exact (h0 _ _ _).2.2.1

Goal state after: