mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = ∅
⊢ False

pp: case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = univ
⊢ False

Tactic:
· absurd hx
      simp [← mem_preimage, h']

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace β
inst✝¹ : Nonempty β
inst✝ : SeparatesPoints β
f : α → β
hf : Measurable f
a₁ a₂ : α
h : f a₁ ≠ f a₂
s : Set β
hs : MeasurableSet s
hx : f a₁ ∈ s
hy : f a₂ ∉ s
h' : f ⁻¹' s = univ
⊢ False
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : SeparatesPoints α
b : Set (Set α)
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y

Tactic:
hb

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
b : Set (Set α)
inst✝ : SeparatesPoints α
hbc : b.Countable
hb : inst✝¹ = generateFrom b
⊢ ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ b, x ∈ s ↔ y ∈ s) → x = y
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δ (⋂ i, {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U i)})

Tactic:
refine .iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_

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)
k : ℕ
x : X
⊢ x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} →
    {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} ∈ nhds x
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : r₁ ≤ 0
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))

Tactic:
· simp [thickening_of_nonpos h₁]

Goal state after:
case inr
α : Type u
inst✝ : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_5
inst✝⁴ : TopologicalSpace α
m : MeasurableSpace α
inst✝³ : SecondCountableTopology α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : BorelSpace α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a ≤ b → μ (Icc a b) = ν (Icc a b)
⊢ μ = ν

Tactic:
rcases exists_countable_dense_bot_top α with ⟨s, hsc, hsd, hsb, hst⟩
  have : (⋃ (l ∈ s) (u ∈ s) (_ : l ≤ u), {Icc l u} : Set (Set α)).Countable :=
    hsc.biUnion fun l _ => hsc.biUnion fun u _ => countable_iUnion fun _ => countable_singleton _
  simp only [← ofPred_eq_eq_singleton, ← ofPred_exists] at this
  refine
    Measure.ext_of_generateFrom_of_cover_subset
      (BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Icc α)) (isPiSystem_Icc id id) ?_ this
      ?_ ?_ ?_
  · rintro _ ⟨l, -, u, -, h, rfl⟩
    exact ⟨l, u, h, rfl⟩
  · refine sUnion_eq_univ_iff.2 fun x => ?_
    rcases hsd.exists_le' hsb x with ⟨l, hls, hlx⟩
    rcases hsd.exists_ge' hst x with ⟨u, hus, hxu⟩
    exact ⟨_, ⟨l, hls, u, hus, hlx.trans hxu, rfl⟩, hlx, hxu⟩
  · rintro _ ⟨l, -, u, -, hlt, rfl⟩
    exact hμ hlt
  · rintro _ ⟨l, u, hlt, rfl⟩
    exact h hlt

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u

Tactic:
have I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s :=
    hausdorffDist_triangle fin

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s t u : Set α
fin : hausdorffEDist u t ≠ ∞
I : hausdorffDist u s ≤ hausdorffDist u t + hausdorffDist t s
⊢ hausdorffDist s u ≤ hausdorffDist s t + hausdorffDist t u
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
⊢ (∀ (i : ℝ), 0 < i → ∀ᶠ (x : β) in l, f x ∈ thickening i s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, infDist (f x) s < ε

Tactic:
congrm (∀ ε hε, ?_)

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : PseudoMetricSpace α
l : Filter β
s : Set α
f : β → α
hs₁ : IsCompact s
hs₂ : s.Nonempty
ε : ℝ
hε : 0 < ε
⊢ (∀ᶠ (x : β) in l, f x ∈ thickening ε s) ↔ ∀ᶠ (x : β) in l, infDist (f x) s < ε
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
⊢ ∀ (b : ℕ), MeasurableSet (t b ×ˢ s)

Tactic:
rintro n

Goal state after:
case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hD : IsCountablySpanning D
s : Set β
hs : s ∈ D
t : ℕ → Set α
h1t : ∀ (n : ℕ), t n ∈ C
h2t : ⋃ n, t n = univ
n : ℕ
⊢ MeasurableSet (t n ×ˢ s)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
r : β
s : Set α
f : α →ₛ β
hr : r ∈ (f.restrict s).range
h0 : r ≠ 0
⊢ r ∈ ⇑f '' s

Tactic:
classical
  exact if hs : MeasurableSet s then by simpa [mem_restrict_range hs, h0, -mem_range] using hr
  else by
    rw [restrict_of_not_measurable hs] at hr
    exact (h0 <| eq_zero_of_mem_range_zero hr).elim

Goal state after:
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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
b : δ
⊢ b ∈ s → g b = g x

Tactic:
hb

Goal state after:
α : 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
b : δ
hb : b ∈ s
⊢ g b = g x
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inl.inr
α : 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
⊢ Measurable g

Tactic:
have : g = s.piecewise (fun _y ↦ g x) g' := by
        ext b
        by_cases hb : b ∈ s
        · simp [hb, B]
        · simp [hb, hg' hb]

Goal state after:
case inl.inr
α : 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
hι : IsEmpty ι
x : δ
hx : x ∈ s
A : ∀ b ∈ s, IsBot (g b)
B : ∀ b ∈ s, g b = g x
this : g = s.piecewise (fun _y ↦ g x) g'
⊢ Measurable g
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inr
α : 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
⊢ Measurable g

Tactic:
let f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'

Goal state after:
case inr
α : 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 : ι → δ → α
g g' : δ → α
hf : ∀ (i : ι), Measurable (f i)
s : Set δ
hs : MeasurableSet s
hg : ∀ b ∈ s, IsLUB {a | ∃ i, f i b = a} (g b)
hg' : EqOn g g' sᶜ
g'_meas : Measurable g'
i : ι
this : Nonempty ι
f' : ι → δ → α := fun i ↦ s.piecewise (f i) g'
⊢ Measurable g
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
⊢ b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b

Tactic:
hb

Goal state after:
case refine_3
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
b : ℝ≥0∞
a✝ : b ∈ s
hb : b * μ (⇑f ⁻¹' {b}) ≠ 0
⊢ ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
⊢ MeasurableSet s

Tactic:
by
  by_cases H : ∃ x ∈ s, IsTop x
  · rcases H with ⟨x₀, x₀s, h₀⟩
    have : s = { x₀ } ∪ s \ { x₀ } := by rw [union_sdiff_cancel (singleton_subset_iff.2 x₀s)]
    rw [this]
    refine (measurableSet_singleton _).union ?_
    have A : ∀ x ∈ s \ { x₀ }, x < x₀ := fun x hx => lt_of_le_of_ne (h₀ _) (by simpa using hx.2)
    refine .of_mem_nhdsGT_aux (fun x hx => ?_) fun x hx => ⟨x₀, A x hx⟩
    obtain ⟨u, hu, us⟩ : ∃ (u : α), u ∈ Ioi x ∧ Ioo x u ⊆ s :=
      (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).1 (h x hx.1)
    refine (mem_nhdsGT_iff_exists_Ioo_subset' (A x hx)).2 ⟨u, hu, fun y hy => ⟨us hy, ?_⟩⟩
    exact ne_of_lt (hy.2.trans_le (h₀ _))
  · refine .of_mem_nhdsGT_aux h ?_
    simp only [IsTop] at H
    push Not at H
    exact H

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

Goal state before:
pp: case pos
δ : Type u_4
mδ : MeasurableSpace δ
α : Type u_5
mα : MeasurableSpace α
inst✝ : ConditionallyCompleteLattice α
p : Prop
f : δ → α
hf : Measurable f
h : p
⊢ Measurable fun b ↦ f b

Tactic:
exact hf

Goal state after:
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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
⊢ b ∈ {b | BddAbove (range fun i ↦ f i b)} → IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)

Tactic:
hb

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i ↦ f i b)}
⊢ IsLUB {a | ∃ i, f i b = a} (⨆ i, f i b)
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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
⊢ b ∈ {b | BddAbove (range fun i ↦ f i b)}ᶜ → (fun b ↦ ⨆ i, f i b) b = (fun _b ↦ sSup ∅) b

Tactic:
hb

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), Measurable (f i)
hι : Nonempty ι
A : MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
this : Measurable fun _b ↦ sSup ∅
b : δ
hb : b ∈ {b | BddAbove (range fun i ↦ f i b)}ᶜ
⊢ (fun b ↦ ⨆ i, f i b) b = (fun _b ↦ sSup ∅) b
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✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
b : δ
⊢ (∀ (i : ι), f i b = mk (f i) ⋯ b) → ⨆ i, f i b = ⨆ i, mk (f i) ⋯ b

Tactic:
hb

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
b : δ
hb : ∀ (i : ι), f i b = mk (f i) ⋯ b
⊢ ⨆ i, f i b = ⨆ i, mk (f i) ⋯ b
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✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
this✝ : ∀ i ∈ s, Measurable (g i)
this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b
b : δ
⊢ (∀ i ∈ s, f i b = g i b) → ⨆ i ∈ s, f i b = ⨆ i ∈ s, g i b

Tactic:
hb

Goal state after:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
mδ : MeasurableSpace δ
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
ι : Type u_5
μ : Measure δ
s : Set ι
f : ι → δ → α
hs : s.Countable
hf : ∀ i ∈ s, AEMeasurable (f i) μ
g : ι → δ → α := fun i ↦ if hi : i ∈ s then mk (f i) ⋯ else fun _b ↦ sSup ∅
this✝ : ∀ i ∈ s, Measurable (g i)
this : ∀ i ∈ s, ∀ᵐ (b : δ) ∂μ, f i b = g i b
b : δ
hb : ∀ i ∈ s, f i b = g i b
⊢ ⨆ i ∈ s, f i b = ⨆ i ∈ s, g i b
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_5
γ : Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : AddZeroClass γ
motive : (α →ₛ γ) → Prop
const :
  ∀ (c : γ) {s : Set α} (hs : MeasurableSet s), motive (piecewise s hs (SimpleFunc.const α c) (SimpleFunc.const α 0))
add : ∀ ⦃f g : α →ₛ γ⦄, Disjoint (support ⇑f) (support ⇑g) → motive f → motive g → motive (f + g)
f : α →ₛ γ
s : Finset γ
h : range ⇑f \ {0} = ↑s
⊢ motive f

Tactic:
induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, sdiff_eq_empty, range_subset_singleton] at h
    convert! const 0 MeasurableSet.univ
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx 0 f
    have Pg : motive g := by
      apply ih
      simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
      rw [image_compl_preimage, union_sdiff_distrib, sdiff_sdiff_comm, h, Finset.coe_insert,
        insert_sdiff_self_of_notMem, sdiff_eq_empty.mpr, Set.empty_union]
      · rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)
      · rwa [Finset.mem_coe]
    convert! add _ Pg (const x mx)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]
    rw [disjoint_iff_inf_le]
    rintro y
    by_cases hy : y ∈ f ⁻¹' {x} <;> simp [g, hy]

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 ∞)
i j : ℤ
hij : i ≠ j
⊢ Function.onFun Disjoint (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j

Tactic:
wlog h : i < j generalizing i j

Goal state after:
case hn.inr
α : 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
this : ∀ ⦃i j : ℤ⦄, i ≠ j → i < j → Function.onFun Disjoint (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j
h : ¬i < j
⊢ Function.onFun Disjoint (fun n ↦ s ∩ f ⁻¹' Ico (↑t ^ n) (↑t ^ (n + 1))) i j

α : 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
h : 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 : Measurable f
⊢ ⨆ n, ∫⁻ (a : α), (eapprox f n) a ∂μ = ⨆ n, (eapprox f n).lintegral μ

Tactic:
by
      congr; ext n; rw [(eapprox f n).lintegral_eq_lintegral]

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

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

Tactic:
by_cases h : r = 0
  · simp [h]
  apply le_antisymm _ (lintegral_const_mul_le r f)
  have rinv : r * r⁻¹ = 1 := ENNReal.mul_inv_cancel h hr
  have rinv' : r⁻¹ * r = 1 := by
    rw [mul_comm]
    exact rinv
  have := lintegral_const_mul_le (μ := μ) r⁻¹ fun x => r * f x
  simp only [(mul_assoc _ _ _).symm, rinv'] at this
  simpa [(mul_assoc _ _ _).symm, rinv] using mul_le_mul_right this r

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : γ → β
mα : MeasurableSpace α
mγ : MeasurableSpace γ
inst✝ : TopologicalSpace β
hg : MeasurableEmbedding g
hf : StronglyMeasurable f
hg' : StronglyMeasurable g'
x : γ
hx : ¬∃ y, g y = x
⊢ Tendsto (fun n ↦ ((fun n ↦ (hf.approx n).extend g hg (hg'.approx n)) n) x) atTop (𝓝 (Function.extend g f g' x))

Tactic:
simpa only [hx, SimpleFunc.extend_apply', not_false_iff, extend_apply'] using
      hg'.tendsto_approx x

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

Goal state before:
pp: α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : MetrizableSpace ι
inst✝⁵ : MeasurableSpace ι
inst✝⁴ : SecondCountableTopology ι
inst✝³ : OpensMeasurableSpace ι
mβ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : PseudoMetrizableSpace β
inst✝ : BorelSpace β
m : MeasurableSpace α
u : ι → α → β
hu_cont : ∀ (x : α), Continuous[inst✝⁷, inst✝²] fun i ↦ u i x
h : ∀ (i : ι), Measurable (u i)
⊢ Measurable (uncurry u)

Tactic:
by
  obtain ⟨t_sf, ht_sf⟩ :
    ∃ t : ℕ → SimpleFunc ι ι, ∀ j x, Tendsto (fun n => u (t n j) x) atTop (𝓝 <| u j x) := by
    have h_str_meas : StronglyMeasurable (id : ι → ι) := stronglyMeasurable_id
    refine ⟨h_str_meas.approx, fun j x => ?_⟩
    exact ((hu_cont x).tendsto j).comp (h_str_meas.tendsto_approx j)
  let U (n : ℕ) (p : ι × α) := u (t_sf n p.fst) p.snd
  have h_tendsto : Tendsto U atTop (𝓝 fun p => u p.fst p.snd) := by
    rw [tendsto_pi_nhds]
    exact fun p => ht_sf p.fst p.snd
  refine measurable_of_tendsto_metrizable (fun n => ?_) h_tendsto
  have h_meas : Measurable fun p : (t_sf n).range × α => u (↑p.fst) p.snd := by
    have :
      (fun p : ↥(t_sf n).range × α => u (↑p.fst) p.snd) =
        (fun p : α × (t_sf n).range => u (↑p.snd) p.fst) ∘ Prod.swap :=
      rfl
    rw [this, @measurable_swap_iff α (↥(t_sf n).range) β m]
    exact measurable_from_prod_countable_left fun j => h j
  have :
    (fun p : ι × α => u (t_sf n p.fst) p.snd) =
      (fun p : ↥(t_sf n).range × α => u p.fst p.snd) ∘ fun p : ι × α =>
        (⟨t_sf n p.fst, SimpleFunc.mem_range_self _ _⟩, p.snd) :=
    rfl
  simp_rw [U, this]
  refine h_meas.comp (Measurable.prodMk ?_ measurable_snd)
  exact ((t_sf n).measurable.comp measurable_fst).subtype_mk

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
ε : ℝ
ε0 : 0 < ε
x y : X
h : glueDist Φ Ψ ε (Sum.inl x) (Sum.inl y) = 0
⊢ Sum.inl x = Sum.inl y

Tactic:
rw [eq_of_dist_eq_zero h]

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
ε : ℝ
ε0 : 0 < ε
x y : Y
h : glueDist Φ Ψ ε (Sum.inr x) (Sum.inr y) = 0
⊢ Sum.inr x = Sum.inr y

Tactic:
rw [eq_of_dist_eq_zero h]

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

Goal state before:
pp: case inl.inl
X : Type u
Y : Type v
Z : Type w
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
p q : X
h : Sum.dist (Sum.inl p) (Sum.inl q) = 0
⊢ Sum.inl p = Sum.inl q

Tactic:
rw [eq_of_dist_eq_zero h]

Goal state after: