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

Goal state before:
pp: case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

pp: case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

Tactic:
·

Goal state after:
case inl
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix x s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)

Tactic:
·

Goal state after:
case inr
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : longestPrefix y s < firstDiff x y
⊢ cylinder x (longestPrefix x s) = cylinder y (longestPrefix y s)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ ξ (s ∩ h.nullSet) = 0 ∧ ξ (s ∩ h.nullSetᶜ) = 0

pp: case hd
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)

pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
·

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ ξ (s ∩ h.nullSet) = 0 ∧ ξ (s ∩ h.nullSetᶜ) = 0
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case hd
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)

pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
·

Goal state after:
case hd
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
·

Goal state after:
case h
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) =
    μ (measurableAtom ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩) *
      (measurableAtom x).indicator 1 ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩

pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ∀ (b' : ↑(range points)),
    b' ≠ ⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ → μ (measurableAtom ↑b') * (measurableAtom x).indicator 1 ↑b' = 0

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) =
    μ (measurableAtom ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩) *
      (measurableAtom x).indicator 1 ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSetᶜ ∈ ae μ

pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν

pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSetᶜ ∈ ae μ
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = μ (measurableAtom ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩) * 1 ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩

pp: case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ ∈ measurableAtom x

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ μ (measurableAtom x) = μ (measurableAtom ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩) * 1 ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν

pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s ∪ h.nullSet ∈ ae ν
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
a✝ : s ∈ ⊥
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ ∈ measurableAtom x

Tactic:
·

Goal state after:
case h
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ↑⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ ∈ measurableAtom x
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ∀ (b' : ↑(range points)),
    b' ≠ ⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ → μ (measurableAtom ↑b') * (measurableAtom x).indicator 1 ↑b' = 0

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ : Measure α
measurableAtoms : Set (Set α) := measurableAtom '' univ
h_nonempty : ∀ (s : ↑measurableAtoms), (↑s).Nonempty
points : ↑measurableAtoms → α := fun s ↦ ⋯.some
h_points_mem : ∀ (s : ↑measurableAtoms), points s ∈ ↑s
x : α
⊢ ∀ (b' : ↑(range points)),
    b' ≠ ⟨points ⟨measurableAtom x, ⋯⟩, ⋯⟩ → μ (measurableAtom ↑b') * (measurableAtom x).indicator 1 ↑b' = 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)

Tactic:
·

Goal state after:
case neg
E : ℕ → Type u_1
inst✝¹ : (n : ℕ) → TopologicalSpace (E n)
inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)
s : Set ((n : ℕ) → E n)
hs : IsClosed[Pi.topologicalSpace] s
hne : s.Nonempty
f : ((n : ℕ) → E n) → (n : ℕ) → E n := fun x ↦ if x ∈ s then x else ⋯.some
fs : ∀ x ∈ s, f x = x
x y : (n : ℕ) → E n
hxy : x ≠ y
hfxfy : f x ≠ f y
I2 : cylinder x (firstDiff x y) = cylinder y (firstDiff x y)
xs : x ∉ s
ys : y ∉ s
Ax : (s ∩ cylinder x (longestPrefix x s)).Nonempty
fx : f x = Ax.some
Ay : (s ∩ cylinder y (longestPrefix y s)).Nonempty
fy : f y = Ay.some
H : firstDiff x y ≤ longestPrefix x s ∧ firstDiff x y ≤ longestPrefix y s
⊢ firstDiff x y ≤ firstDiff (f x) (f y)
Module: Mathlib.MeasureTheory.Measure.MutuallySingular

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : μ ⟂ₘ ν → Disjoint μ ν
tfae_2_to_1 : Disjoint μ ν → μ ⟂ₘ ν
tfae_1_to_3 : μ ⟂ₘ ν → Disjoint (ae μ) (ae ν)
tfae_3_to_2 : Disjoint (ae μ) (ae ν) → Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_finish

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENNReal

Goal state before:
pp: α : Type u_1
⊢ (↑(ENat.card α)).toReal = ↑(Nat.card α)

Tactic:
cases finite_or_infinite α <;> simp [ENat.card_eq_coe_natCard]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case isOpen
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (U : Set α), IsOpen[inst✝³] U → IsClopenable U

pp: case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

pp: case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
·

Goal state after:
case isOpen
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (U : Set α), IsOpen[inst✝³] U → IsClopenable U
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ

pp: case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
·

Goal state after:
case compl
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (t : Set α), MeasurableSet t → IsClopenable t → IsClopenable tᶜ
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite

pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : s.Finite
⊢ count s = ∞ ↔ s.Infinite
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ count s = ∞ ↔ s.Infinite
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)

Tactic:
·

Goal state after:
case iUnion
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), IsClopenable (f i)) → IsClopenable (⋃ i, f i)
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ count (f '' s) = count s

pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ count (f '' s) = count s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
⊢ s ∈ ae (dirac a) ↔ s ∈ pure a

Tactic:
simp [mem_ae_iff, imp_false]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ count (f '' s) = count s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a
Module: Mathlib.MeasureTheory.Measure.Count

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ count (f '' s) = count s

pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ count (f '' s) = count s

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : s.Finite
⊢ count (f '' s) = count s
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
s : Set α
a : α
hs : MeasurableSet s
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a

pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∈ s
⊢ (dirac a).restrict s = dirac a
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝² : MeasurableSpace α
s : Set α
a : α
inst✝¹ : MeasurableSingletonClass α
inst✝ : Decidable (a ∈ s)
has : a ∉ s
⊢ (dirac a).restrict s = 0
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x = dirac y → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)

pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → dirac x = dirac y

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ dirac x = dirac y → ∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∈ A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
h : dirac x = dirac y
A : Set α
A_mble : MeasurableSet A
obs : A.indicator 1 x = A.indicator 1 y
x_in_A : x ∉ A
⊢ x ∈ A ↔ y ∈ A
Module: Mathlib.MeasureTheory.Measure.Dirac

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → dirac x = dirac y

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝ : MeasurableSpace α
x y : α
⊢ (∀ (A : Set α), MeasurableSet A → (x ∈ A ↔ y ∈ A)) → dirac x = dirac y