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

Goal state before:
pp: case compl.refine_2.mpr
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
hx : ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1
⊢ ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2

Tactic:
·

Goal state after:
case compl.refine_2.mpr
α : Type u_1
𝒜 : Set (Set α)
s u : Set α
hs✝ : generateSetAlgebra 𝒜 u
A : Set (Set (Set α))
A_fin : A.Finite
mem_A : ∀ a ∈ A, a.Finite
hA : ∀ a ∈ A, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ A, ⋂ t ∈ a, t
this✝ : Finite ↑A
this : ∀ (a : ↑A), Finite ↑↑a
x : α
hx : ∃ i, ∀ (i_1 : Set α) (i_2 : Set (Set α)) (i_3 : i_2 ∈ A), (↑(i ⟨i_2, ⋯⟩))ᶜ = i_1 → x ∈ i_1
⊢ ∀ i ∈ A, ∃ i_2 ∈ i, x ∉ i_2
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2.«0».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case convert_2.«0».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case convert_2.«1».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case convert_2.«0».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2.«0».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case convert_2.«1».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case convert_2.«0».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_1
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ (⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z ⊆ Ioi ↑a

pp: case a.inl.coe.coe.refine_2
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)

Tactic:
·

Goal state after:
case a.inl.coe.coe.refine_1
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ (⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z ⊆ Ioi ↑a
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2.«1».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case convert_2.«1».«0»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case convert_2.«1».«1»
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ (Disjoint on ![s, t]) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case convert_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ⋃ i, ![s, t] i ∈ C

Tactic:
·

Goal state after:
case convert_3
α : Type u_1
C : Set (Set α)
s t : Set α
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
A : s ∪ t = ⋃ i, ![s, t] i
⊢ ⋃ i, ![s, t] i ∈ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, a.Finite

pp: case union.refine_2
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
·

Goal state after:
case union.refine_1
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, a.Finite
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_2
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)

Tactic:
·

Goal state after:
case a.inl.coe.coe.refine_2
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ x, Ioi x = ∅ then h.choose else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {↑x₁}
basis : Set (Set ι) := {s | ∃ f g, f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] ((⋂ z ∈ f, Ioi ↑z) ∩ ⋂ z ∈ g, Iio ↑z)
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union.refine_1.inl
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
⊢ a.Finite

pp: case union.refine_1.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
⊢ a.Finite

Tactic:
·

Goal state after:
case union.refine_1.inl
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Au
⊢ a.Finite
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

pp: case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

pp: case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
·

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_2.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi ↑z)

pp: case a.inl.coe.coe.refine_2.ht
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio ↑z)

Tactic:
·

Goal state after:
case a.inl.coe.coe.refine_2.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi ↑z)
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

pp: case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
·

Goal state after:
case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union.refine_1.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
⊢ a.Finite

Tactic:
·

Goal state after:
case union.refine_1.inr
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
a : Set (Set α)
ha : a ∈ Av
⊢ a.Finite
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
·

Goal state after:
case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_2.hs.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ f.Finite

pp: case a.inl.coe.coe.refine_2.hs.h
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ ∀ i ∈ f, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑i)

Tactic:
·

Goal state after:
case a.inl.coe.coe.refine_2.hs.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ f.Finite
Module: Mathlib.MeasureTheory.Measure.AddContent

Goal state before:
pp: case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
·

Goal state after:
case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
G : Type u_2
inst✝ : AddCommMonoid G
m : AddContent G C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C
Module: Mathlib.MeasureTheory.SetAlgebra

Goal state before:
pp: case union.refine_2
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜

Tactic:
·

Goal state after:
case union.refine_2
α : Type u_1
𝒜 : Set (Set α)
s u v : Set α
hs✝ : generateSetAlgebra 𝒜 u
ht✝ : generateSetAlgebra 𝒜 v
Au : Set (Set (Set α))
Au_fin : Au.Finite
mem_Au : ∀ a ∈ Au, a.Finite
hAu : ∀ a ∈ Au, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
u_eq : u = ⋃ a ∈ Au, ⋂ t ∈ a, t
Av : Set (Set (Set α))
Av_fin : Av.Finite
mem_Av : ∀ a ∈ Av, a.Finite
hAv : ∀ a ∈ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜
v_eq : v = ⋃ a ∈ Av, ⋂ t ∈ a, t
⊢ ∀ a ∈ Au ∪ Av, ∀ t ∈ a, t ∈ 𝒜 ∨ tᶜ ∈ 𝒜