mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) ≠ ∞

pp: case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) = ν (Ico a b)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) ≠ ∞

case refine_2
α : Type u_5
inst✝⁵ : TopologicalSpace α
m : MeasurableSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : BorelSpace α
inst✝ : NoMinOrder α
μ ν : Measure α
hμ : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) ≠ ∞
h : ∀ ⦃a b : α⦄, a < b → μ (Ioc a b) = ν (Ioc a b)
a b : αᵒᵈ
hab : a < b
⊢ μ (Ico a b) = ν (Ico a b)
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : DecidableEq γ
g : β → γ
f : α →ₛ β
⊢ ↑(map g f).range = ↑(Finset.image g f.range)

Tactic:
simp only [coe_range, coe_map, Finset.coe_image, range_comp]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ MeasurableSpace.comap Prod.fst (generateFrom C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ MeasurableSpace.comap Prod.snd (generateFrom D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
<;>

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ MeasurableSpace.comap Prod.fst (generateFrom C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ MeasurableSpace.comap Prod.snd (generateFrom D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

Tactic:
<;>

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.fst '' C) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)

case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ generateFrom (preimage Prod.snd '' D) ≤ generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D)
Module: Mathlib.MeasureTheory.MeasurableSpace.Prod

Goal state before:
pp: case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ preimage Prod.fst '' C, MeasurableSet t

pp: case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ preimage Prod.snd '' D, MeasurableSet t

Tactic:
<;>

Goal state after:
case a.refine_1
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ preimage Prod.fst '' C, MeasurableSet t

case a.refine_2
α : Type u_3
β : Type u_4
C : Set (Set α)
D : Set (Set β)
hC : IsCountablySpanning C
hD : IsCountablySpanning D
⊢ ∀ t ∈ preimage Prod.snd '' D, MeasurableSet t
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case hle
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₁

pp: case hle
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₂

Tactic:
<;>

Goal state after:
case hle
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₁

case hle
α : Type u
inst✝¹ : PseudoEMetricSpace α
β : Type u_2
inst✝ : PseudoEMetricSpace β
f : α → β
K : Set α
U : Set β
hK : IsCompact K
ho : IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] U
hf : ∀ x ∈ K, ContinuousAt f x
hKU : MapsTo f K U
s t : Set α
ε₁ : ℝ
hε₁ : ε₁ > 0
V₁ : Set α
hV₁ : V₁ ∈ 𝓝ˢ s
hV₁thickening : thickening ε₁ (f '' V₁) ⊆ U
ε₂ : ℝ
hε₂ : ε₂ > 0
V₂ : Set α
hV₂ : V₂ ∈ 𝓝ˢ t
hV₂thickening : thickening ε₂ (f '' V₂) ⊆ U
⊢ min ε₁ ε₂ ≤ ε₂
Module: Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst✝ : NullSingletonClass μ
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s

Tactic:
by
  simpa only [ae_iff, Classical.not_not] using! h.measure_zero μ

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∀ a < b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)

Tactic:
by
  simp_rw [lt_add_iff_lt_right_or_exists_lt]
  aesop

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
P : α → Prop
b c : α
inst✝³ : AddCommMagma α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : AddLeftReflectLT α
inst✝ : IsLeftCancelAdd α
⊢ (∃ a < b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)

Tactic:
by
  simp_rw [lt_add_iff_lt_right_or_exists_lt]
  aesop

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ f.lintegral μ = ∑ x ∈ s, x * μ (⇑f ⁻¹' {x})

Tactic:
refine Finset.sum_bij_ne_zero (fun r _ _ => r) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ a ∈ f.range, a * μ (⇑f ⁻¹' {a}) ≠ 0 → a ∈ s

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
s : Finset ℝ≥0∞
hs : ∀ (x : α), f x ≠ 0 → μ (⇑f ⁻¹' {f x}) ≠ 0 → f x ∈ s
⊢ ∀ a₁ ∈ f.range, a₁ * μ (⇑f ⁻¹' {a₁}) ≠ 0 → ∀ a₂ ∈ f.range, a₂ * μ (⇑f ⁻¹' {a₂}) ≠ 0 → a₁ = a₂ → a₁ = a₂

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 ∈ s, b * μ (⇑f ⁻¹' {b}) ≠ 0 → ∃ a, ∃ (_ : a ∈ f.range) (_ : a * μ (⇑f ⁻¹' {a}) ≠ 0), a = b

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

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

Tactic:
rcases H with ⟨x₀, x₀s, h₀⟩

Goal state after:
case pos
α : Type u_1
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : BorelSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
h : ∀ x ∈ s, s ∈ 𝓝[>] x
x₀ : α
x₀s : x₀ ∈ s
h₀ : IsTop x₀
⊢ MeasurableSet s
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case inl
α : 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)
hα : IsEmpty α
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}

Tactic:
have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _

Goal state after:
case inl
α : 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)
hα : IsEmpty α
this : ∀ (b : δ), (range fun i ↦ f i b) = ∅
⊢ MeasurableSet {b | BddAbove (range fun i ↦ f i b)}
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case left
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s i)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

pp: case right
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

Tactic:
<;>

Goal state after:
case left
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s i)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})

case right
α : Type u_1
m : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : α →ₛ ℝ≥0∞
s : ι → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
μ : Measure α
i j k : ι
x✝ : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k) ∧ (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
hik : (fun x1 x2 ↦ x1 ⊆ x2) (s i) (s k)
hjk : (fun x1 x2 ↦ x1 ⊆ x2) (s j) (s k)
a : ℝ≥0∞
⊢ a * (μ.restrict (s j)) (⇑f ⁻¹' {a}) ≤ a * (μ.restrict (s k)) (⇑f ⁻¹' {a})
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case mp
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
⊢ Tendsto (fun i ↦ if p i then a else b) L (if q then F else G) → ∀ᶠ (i : ι) in L, p i ↔ q

pp: case mpr
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) → Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)

Tactic:
<;>

Goal state after:
case mp
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
⊢ Tendsto (fun i ↦ if p i then a else b) L (if q then F else G) → ∀ᶠ (i : ι) in L, p i ↔ q

case mpr
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
⊢ (∀ᶠ (i : ι) in L, p i ↔ q) → Tendsto (fun i ↦ if p i then a else b) L (if q then F else G)
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case neg
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : (fun x ↦ if q then a else b) =ᶠ[L] fun i ↦ if p i then a else b
hq : ¬q
⊢ Tendsto (fun x ↦ if q then a else b) L (if q then F else G)

Tactic:
simp only [hq, ite_false]

Goal state after:
case neg
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst✝¹ : DecidablePred p
q : Prop
inst✝ : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
obs : (fun x ↦ if q then a else b) =ᶠ[L] fun i ↦ if p i then a else b
hq : ¬q
⊢ Tendsto (fun x ↦ b) L G
Module: Mathlib.Topology.IndicatorConstPointwise

Goal state before:
pp: case pos
α : 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 : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
hxA : x ∈ A
⊢ 𝓝 (A.indicator (fun x ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

pp: case neg
α : 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 : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
hxA : x ∉ A
⊢ 𝓝 (A.indicator (fun x ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

Tactic:
<;>

Goal state after:
case pos
α : 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 : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
hxA : x ∈ A
⊢ 𝓝 (A.indicator (fun x ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0

case neg
α : 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 : α
heart : Tendsto (fun i ↦ if x ∈ As i then b else 0) L (if x ∈ A then 𝓝 b else 𝓝 0) ↔ ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
hxA : x ∉ A
⊢ 𝓝 (A.indicator (fun x ↦ b) x) = if x ∈ A then 𝓝 b else 𝓝 0
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
⊢ ∀ t ∈ range fun a ↦ Ioi ↑a, MeasurableSet t

pp: case refine_2
⊢ ∀ t ∈ range fun a ↦ Iic ↑a, MeasurableSet t

Tactic:
<;>

Goal state after:
case refine_1
⊢ ∀ t ∈ range fun a ↦ Ioi ↑a, MeasurableSet t

case refine_2
⊢ ∀ t ∈ range fun a ↦ Iic ↑a, MeasurableSet t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

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

Tactic:
<;>

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

case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Iic ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet (Iic ↑q)ᶜ

pp: case refine_2
q : ℚ
⊢ MeasurableSet (Ioi ↑q)ᶜ

Tactic:
<;>

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Iic ↑q)ᶜ

case refine_2
q : ℚ
⊢ MeasurableSet (Ioi ↑q)ᶜ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
⊢ ∀ t ∈ range fun a ↦ Iio ↑a, MeasurableSet t

pp: case refine_2
⊢ ∀ t ∈ range fun a ↦ Ici ↑a, MeasurableSet t

Tactic:
<;>

Goal state after:
case refine_1
⊢ ∀ t ∈ range fun a ↦ Iio ↑a, MeasurableSet t

case refine_2
⊢ ∀ t ∈ range fun a ↦ Ici ↑a, MeasurableSet t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

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

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

Tactic:
<;>

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

case refine_2
q : ℚ
⊢ MeasurableSet ((fun a ↦ Ici ↑a) q)
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: case refine_1
q : ℚ
⊢ MeasurableSet (Ici ↑q)ᶜ

pp: case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ

Tactic:
<;>

Goal state after:
case refine_1
q : ℚ
⊢ MeasurableSet (Ici ↑q)ᶜ

case refine_2
q : ℚ
⊢ MeasurableSet (Iio ↑q)ᶜ
Module: Mathlib.MeasureTheory.Function.SimpleFunc

Goal state before:
pp: case pos
α : 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)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥

pp: case neg
α : 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)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥

Tactic:
<;>

Goal state after:
case pos
α : 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)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∈ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥

case neg
α : 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)
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ), range ⇑f \ {0} = ↑s → motive f
f : α →ₛ γ
h : range ⇑f \ {0} = ↑(insert x s)
mx : MeasurableSet (⇑f ⁻¹' {x})
g : α →ₛ γ := piecewise (⇑f ⁻¹' {x}) mx 0 f
Pg : motive g
y : α
hy : y ∉ ⇑f ⁻¹' {x}
⊢ y ∈ support ⇑g ⊓ support ⇑(piecewise (⇑f ⁻¹' {x}) mx (SimpleFunc.const α x) (SimpleFunc.const α 0)) → y ∈ ⊥
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Real

Goal state before:
pp: μ : Measure ℝ
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : NullSingletonClass μ
b : ℝ
⊢ Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝 0) (𝓝 0)

Tactic:
by
  rw [← nhdsLT_sup_nhdsGE, tendsto_sup]
  constructor
  · apply tendsto_const_nhds.congr'
    filter_upwards [self_mem_nhdsWithin] with r (hr : r < 0)
    rw [Icc_eq_empty (by linarith), measure_empty]
  · simpa only [measure_singleton] using tendsto_measure_Icc_nhdsWithin_right μ b

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

Goal state before:
pp: case e_a
α : 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)
x : α
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞

Tactic:
obtain (H | H) : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top

Goal state after:
case e_a.inl
α : 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)
x : α
H : f x = ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞

case e_a.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)
x : α
H : f x < ∞
⊢ 0 < f x ↔ f x = ∞ ∨ 0 < f x ∧ f x < ∞
Module: Mathlib.MeasureTheory.Integral.Lebesgue.Basic

Goal state before:
pp: case inl
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ = 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

pp: case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ

Tactic:
· exact ⟨0, measurable_zero, zero_le, h₀.trans lintegral_zero.symm⟩

Goal state after:
case inr
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h₀ : ∫⁻ (a : α), f a ∂μ ≠ 0
⊢ ∃ g, Measurable g ∧ g ≤ f ∧ ∫⁻ (a : α), f a ∂μ = ∫⁻ (a : α), g a ∂μ
Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst✝ : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n = g m
⊢ (simpleFuncAux f g n.succ) (g m) = f (g m)

pp: case inr
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst✝ : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n ≠ g m
⊢ (simpleFuncAux f g n.succ) (g m) = f (g m)

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst✝ : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n = g m
⊢ (simpleFuncAux f g n.succ) (g m) = f (g m)

case inr
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
f : α → β
g : ℕ → α
m : ℕ
inst✝ : MeasurableSingletonClass α
n : ℕ
hmn : m.succ.le n
hnm : g n ≠ g m
⊢ (simpleFuncAux f g n.succ) (g m) = f (g m)