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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable (_root_.id ∘ f)
⊢ Measurable f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable (_root_.id ∘ f)
⊢ Measurable f
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
t : Set α
⊢ ⇑e.symm '' s = t ↔ ⇑e.symm '' s = t

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set β
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ m (⋂ n, t n) = ms

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
this✝ : ∀ r > ms, ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r
t : ℕ → Set α
hsub : ∀ (n : ℕ), s ⊆ t n
hm : ∀ (n : ℕ), MeasurableSet (t n)
hm' : ∀ (n : ℕ), m (t n) < ms + (↑n)⁻¹
this : Tendsto (fun n ↦ ms + (↑n)⁻¹) atTop (𝓝 ms)
⊢ m (⋂ n, t n) = ms
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
s : Set α
⊢ s = s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
e : α ≃ᵐ β
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
this : Measurable (f ∘ ⇑(refl β))
⊢ Measurable f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
this : Measurable (f ∘ ⇑(refl β))
⊢ Measurable f
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝¹ : (x : δ') → MeasurableSpace (π x)
inst✝ : (x : δ') → MeasurableSpace (π' x)
f : δ ≃ δ'
⊢ ∀ (a : δ), Measurable fun x ↦ (Equiv.piCongrLeft π f).symm x a

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝¹ : (x : δ') → MeasurableSpace (π x)
inst✝ : (x : δ') → MeasurableSpace (π' x)
f : δ ≃ δ'
⊢ ∀ (a : δ), Measurable fun x ↦ (Equiv.piCongrLeft π f).symm x a
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: ι : Type u_8
ι' : Type u_9
e : ι ≃ ι'
β : ι' → Type u_10
inst✝ : (i' : ι') → MeasurableSpace (β i')
x : (i : ι) → β (e i)
i : ι
⊢ x i = x i

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m₁ m₂ m₃ : OuterMeasure α
op : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞
h : ∀ (s : Set α), m₁ s = op (m₂ s) (m₃ s)
s t : Set α
_hst : s ⊆ t
_ht : MeasurableSet t
htm : m₁ t = m₁.trim s ∧ m₂ t = m₂.trim s ∧ m₃ t = m₃.trim s ∧ ∀ (i : Fin 0), (![] i) t = (![] i).trim s
⊢ op (m₂ t) (m₃ t) = op (m₂ t) (m₃ t)

Tactic:
]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ∀ (a : δ ⊕ δ'), Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x a

Tactic:
]

Goal state after:
α✝ : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝² : (x : δ') → MeasurableSpace (π x)
inst✝¹ : (x : δ') → MeasurableSpace (π' x)
α : δ ⊕ δ' → Type u_8
inst✝ : (i : δ ⊕ δ') → MeasurableSpace (α i)
⊢ ∀ (a : δ ⊕ δ'), Measurable fun x ↦ (Equiv.sumPiEquivProdPi α).symm x a
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ Measurable f

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ Measurable f
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : Injective f ∧ MeasurableSpace.comap f inst✝ = inst✝¹ ∧ MeasurableSet (range f)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → MeasurableSet (f '' s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ μ.trim (t ∩ s)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
⊢ ((restrict s) μ).trim t ≤ μ.trim (t ∩ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ∩ s ⊆ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding f
⊢ ↑(range f) = ↑(range f)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → α
hf : MeasurableEmbedding f
⊢ Subtype.instMeasurableSpace ≍ Subtype.instMeasurableSpace

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ ((restrict s) μ).trim t ≤ μ t'
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ μ (t' ∩ s) ≤ μ t'

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t t' : Set α
htt' : t ⊆ sᶜ ∪ t'
ht' : MeasurableSet t'
hμt' : μ t' = μ.trim (t ∩ s)
⊢ μ (t' ∩ s) ≤ μ t'
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ (F A)ᶜᶜ = (g '' Bᶜ)ᶜ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
⊢ (F A)ᶜᶜ = (g '' Bᶜ)ᶜ
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : OuterMeasure α
s : Set α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ s) ≤ μ (t ∩ s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ ↑(g '' Bᶜ) ≃ᵐ ↑Bᶜ

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
A : Set α
Ameas : MeasurableSet A
Afp : F A = A
B : Set β := f '' A
Bmeas : MeasurableSet B
this : Aᶜ = g '' Bᶜ
⊢ ↑(g '' Bᶜ) ≃ᵐ ↑Bᶜ
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ μ (s ∩ t) = 0

Tactic:
]

Goal state after:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : AEDisjoint μ s t
⊢ μ (s ∩ t) = 0
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : Disjoint s t
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ k
hk : IsMax k
⊢ m ≤ φ m

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ k
hk : IsMax k
⊢ m ≤ φ m
Module: Mathlib.Order.Interval.Set.Monotone

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : k ≤ φ k
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ (φ k) ≤ φ (succ k)

Tactic:
]

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : OrderBot α
n : α
φ : α → α
k : α
ih : k ≤ φ k
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ (φ k) ≤ φ (succ k)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F (F^[n] univ))

Tactic:
]

Goal state after:
case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F (F^[n] univ))
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F (F^[n✝] univ)

Tactic:
]

Goal state after:
case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F (F^[n✝] univ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ False

Tactic:
]

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ False
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ ⋂ i, f '' F^[i] univ

Tactic:
]

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ y ∈ ⋂ i, f '' F^[i] univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ ∀ (i : ℕ), y ∈ f '' F^[i] univ

Tactic:
]

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
hx : ∀ (i : ℕ), g y ∈ F^[i] univ
⊢ ∀ (i : ℕ), y ∈ f '' F^[i] univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
⊢ y ∈ f '' F^[n] univ

Tactic:
]

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F (F^[n] univ)
⊢ y ∈ f '' F^[n] univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = hf.equivRange.symm (hf.equivRange x)

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = hf.equivRange.symm (hf.equivRange x)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ hf.equivRange.symm ⟨f x, ⋯⟩ = hf.equivRange.symm ⟨f x, ⋯⟩

Tactic:
]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst✝ : BooleanAlgebra β
h : Measurable compl
f : α → β
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᵐ[μ] t
⊢ EventuallyMeasurableSet m0 (ae μ) t

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᵐ[μ] t
⊢ EventuallyMeasurableSet m0 (ae μ) t
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᵐ[μ] s

pp: case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s

Tactic:
]

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ Exists.choose ?hc =ᵐ[μ] s

case hc
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s