case intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb : inst✝¹ = generateFrom b
⊢ ∃ f, Measurable f ∧ Injective f
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
⊢ ∃ f, Measurable f ∧ Injective f
obtain ⟨b, bct, hb⟩ := h.IsCountablyGenerated
case intro.intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb : inst✝¹ = generateFrom b
e : ℕ → Set α
he : insert ∅ b = range e
⊢ ∃ f, Measurable f ∧ Injective f
case intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb : inst✝¹ = generateFrom b
⊢ ∃ f, Measurable f ∧ Injective f
obtain ⟨e, he⟩ := Set.Countable.exists_eq_range (bct.insert ∅) (insert_nonempty _ _)
case intro.intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ ∃ f, Measurable f ∧ Injective f
case intro.intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb : inst✝¹ = generateFrom b
e : ℕ → Set α
he : insert ∅ b = range e
⊢ ∃ f, Measurable f ∧ Injective f
rw [← generateFrom_insert_empty, he] at hb
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Measurable fun x n => decide (x ∈ e n)

case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Injective fun x n => decide (x ∈ e n)
case intro.intro.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ ∃ f, Measurable f ∧ Injective f
refine' ⟨fun x n => x ∈ e n, _, _⟩
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Injective fun x n => decide (x ∈ e n)
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Measurable fun x n => decide (x ∈ e n)

case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Injective fun x n => decide (x ∈ e n)
. rw [measurable_pi_iff]
  intro n
  apply measurable_to_bool
  simp only [preimage, mem_singleton_iff, Bool.decide_iff]
  rw [hb]
  apply measurableSet_generateFrom
  exact ⟨n, rfl⟩
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
⊢ x = y
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Injective fun x n => decide (x ∈ e n)
intro x y hxy
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
this : x ∈ {y} ↔ y ∈ {y}
⊢ x = y
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
this : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y
specialize this {y} measurableSet_eq
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
this : x ∈ {y}
⊢ x = y
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
this : x ∈ {y} ↔ y ∈ {y}
⊢ x = y
simp only [mem_singleton, iff_true_iff] at this
no goals
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
this : x ∈ {y}
⊢ x = y
exact this
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ ∀ (a : ℕ), Measurable fun x => decide (x ∈ e a)
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ Measurable fun x n => decide (x ∈ e n)
rw [measurable_pi_iff]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ Measurable fun x => decide (x ∈ e n)
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
⊢ ∀ (a : ℕ), Measurable fun x => decide (x ∈ e a)
intro n
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet ((fun x => decide (x ∈ e n)) ⁻¹' {true})
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ Measurable fun x => decide (x ∈ e n)
apply measurable_to_bool
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet {x | x ∈ e n}
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet ((fun x => decide (x ∈ e n)) ⁻¹' {true})
simp only [preimage, mem_singleton_iff, Bool.decide_iff]
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet {x | x ∈ e n}
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet {x | x ∈ e n}
rw [hb]
case intro.intro.intro.refine'_1.h.ht
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ {x | x ∈ e n} ∈ range e
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ MeasurableSet {x | x ∈ e n}
apply measurableSet_generateFrom
no goals
case intro.intro.intro.refine'_1.h.ht
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
n : ℕ
⊢ {x | x ∈ e n} ∈ range e
exact ⟨n, rfl⟩
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
rw [hb]
case hC
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (t : Set α), t ∈ range e → (x ∈ t ↔ y ∈ t)

case h_empty
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅

case h_compl
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (t : Set α), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)

case h_Union
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (f : ℕ → Set α), (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → ((x ∈ ⋃ (i : ℕ), f i) ↔ y ∈ ⋃ (i : ℕ), f i)
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ MeasurableSet s → (x ∈ s ↔ y ∈ s)
apply generateFrom_induction
case h_Union
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t✝ u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
t : ℕ → Set α
ht : ∀ (n : ℕ), x ∈ t n ↔ y ∈ t n
⊢ (x ∈ ⋃ (i : ℕ), t i) ↔ y ∈ ⋃ (i : ℕ), t i
case h_Union
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (f : ℕ → Set α), (∀ (n : ℕ), x ∈ f n ↔ y ∈ f n) → ((x ∈ ⋃ (i : ℕ), f i) ↔ y ∈ ⋃ (i : ℕ), f i)
intro t ht
no goals
case h_Union
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t✝ u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
t : ℕ → Set α
ht : ∀ (n : ℕ), x ∈ t n ↔ y ∈ t n
⊢ (x ∈ ⋃ (i : ℕ), t i) ↔ y ∈ ⋃ (i : ℕ), t i
simp_rw [mem_iUnion, ht]
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
n : ℕ
⊢ x ∈ e n ↔ y ∈ e n
case hC
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (t : Set α), t ∈ range e → (x ∈ t ↔ y ∈ t)
rintro - ⟨n, rfl⟩
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
n : ℕ
⊢ decide (x ∈ e n) = decide (y ∈ e n)
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
n : ℕ
⊢ x ∈ e n ↔ y ∈ e n
rw [← decide_eq_decide]
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : ∀ (a : ℕ), (fun x n => decide (x ∈ e n)) x a = (fun x n => decide (x ∈ e n)) y a
s : Set α
n : ℕ
⊢ decide (x ∈ e n) = decide (y ∈ e n)
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
n : ℕ
⊢ decide (x ∈ e n) = decide (y ∈ e n)
rw [funext_iff] at hxy
no goals
case hC.intro
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : ∀ (a : ℕ), (fun x n => decide (x ∈ e n)) x a = (fun x n => decide (x ∈ e n)) y a
s : Set α
n : ℕ
⊢ decide (x ∈ e n) = decide (y ∈ e n)
exact hxy n
no goals
case h_empty
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ x ∈ ∅ ↔ y ∈ ∅
tauto
case h_compl
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t✝ u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s t : Set α
⊢ (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
case h_compl
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s : Set α
⊢ ∀ (t : Set α), (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
intro t
no goals
case h_compl
α : Type u_1
β : Type ?u.887190
γ : Type ?u.887193
δ : Type ?u.887196
δ' : Type ?u.887199
ι : Sort uι
s✝ t✝ u : Set α
inst✝¹ : MeasurableSpace α
h : CountablyGenerated α
inst✝ : MeasurableSingletonClass α
b : Set (Set α)
bct : Set.Countable b
hb✝ : inst✝¹ = generateFrom b
e : ℕ → Set α
hb : inst✝¹ = generateFrom (range e)
he : insert ∅ b = range e
x y : α
hxy : (fun x n => decide (x ∈ e n)) x = (fun x n => decide (x ∈ e n)) y
s t : Set α
⊢ (x ∈ t ↔ y ∈ t) → (x ∈ tᶜ ↔ y ∈ tᶜ)
tauto