mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case pos
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∈ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)

pp: case neg
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∉ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∈ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a ∩ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a ∩ f n = memPartitionSet f n a \ f n)

case neg
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : memPartitionSet f n a ∈ memPartition f n
h✝ : a ∉ f n
⊢ memPartitionSet f n a ∈ memPartition f n ∧
    (memPartitionSet f n a \ f n = memPartitionSet f n a ∩ f n ∨
      memPartitionSet f n a \ f n = memPartitionSet f n a \ f n)
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case pos
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∈ f n
⊢ a ∈ memPartitionSet f n a ∩ f n

pp: case neg
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∉ f n
⊢ a ∈ memPartitionSet f n a \ f n

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∈ f n
⊢ a ∈ memPartitionSet f n a ∩ f n

case neg
α : Type u_1
f : ℕ → Set α
a : α
n : ℕ
ih : a ∈ memPartitionSet f n a
h : a ∉ f n
⊢ a ∈ memPartitionSet f n a \ f n
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ False

Tactic:
refine absurd h_disj ?_

Goal state after:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ ¬Disjoint s (memPartitionSet f n a)
Module: Mathlib.Order.Filter.CountableSeparatingOn

Goal state before:
pp: case mp
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ → HasCountableSeparatingOn α p t

pp: case mpr
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn α p t → HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ → HasCountableSeparatingOn α p t

case mpr
α : Type u_1
p : Set α → Prop
t : Set α
⊢ HasCountableSeparatingOn α p t → HasCountableSeparatingOn (↑t) (fun u ↦ ∃ v, p v ∧ Subtype.val ⁻¹' v = u) univ
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
p : α → Prop
h : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → p x

Tactic:
simp only [ae_iff] at h ⊢
  simpa [ofPred_and, inter_comm] using measure_inter_eq_zero_of_restrict h

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

Goal state before:
pp: case empty
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
⊢ (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ i ∈ ∅, ∀ᵐ (x : α) ∂μ i, p x

pp: case cons
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : (∀ᵐ (x : α) ∂∑ i ∈ s✝, μ i, p x) ↔ ∀ i ∈ s✝, ∀ᵐ (x : α) ∂μ i, p x
⊢ (∀ᵐ (x : α) ∂∑ i ∈ Finset.cons a✝¹ s✝ h✝, μ i, p x) ↔ ∀ i ∈ Finset.cons a✝¹ s✝ h✝, ∀ᵐ (x : α) ∂μ i, p x

Tactic:
<;>

Goal state after:
case empty
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
⊢ (∀ᵐ (x : α) ∂∑ i ∈ ∅, μ i, p x) ↔ ∀ i ∈ ∅, ∀ᵐ (x : α) ∂μ i, p x

case cons
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
p : α → Prop
μ : ι → Measure α
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : (∀ᵐ (x : α) ∂∑ i ∈ s✝, μ i, p x) ↔ ∀ i ∈ s✝, ∀ᵐ (x : α) ∂μ i, p x
⊢ (∀ᵐ (x : α) ∂∑ i ∈ Finset.cons a✝¹ s✝ h✝, μ i, p x) ↔ ∀ i ∈ Finset.cons a✝¹ s✝ h✝, ∀ᵐ (x : α) ∂μ i, p x
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ s.indicator f =ᵐ[μ] s.indicator g

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ s.indicator f =ᵐ[μ] s.indicator g

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
s : Set α
f : α → β
inst✝ : Zero β
g : α → β
hs : MeasurableSet s
h : s.indicator f =ᵐ[μ] s.indicator g
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: α : Type u_1
m m' : MeasurableSpace α
h : m ≤ m'
S : Set (Set α)
Sct : S.Countable
Smeas : ∀ s ∈ S, MeasurableSet s
hS : ∀ x ∈ univ, ∀ y ∈ univ, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y
⊢ HasCountableSeparatingOn α MeasurableSet univ

Tactic:
use S, Sct, (fun s hs ↦ h _ <| Smeas _ hs), hS

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (bif false then μ else ν)

pp: case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (bif true then μ else ν)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (bif false then μ else ν)

case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
μ✝ ν✝ : Measure α
s t : Set α
a : α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ SigmaFinite (bif true then μ else ν)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ ν : Measure α
s t : Set α
a : α
μ : Measure α
inst✝ : SigmaFinite μ
c : ℝ≥0
i : ℕ
⊢ ↑c * μ (spanningSets μ i) < ∞

Tactic:
exact ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_spanningSets_lt_top μ i)

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

Goal state before:
pp: case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n)

pp: case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s \ t n)

case refine_2
α : Type u_1
t : ℕ → Set α
n : ℕ
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet (s ∩ t n)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ Measurable ((⋂ i, s i).domRestrict g)

Tactic:
rw [domRestrict_piecewise]
    simp only [s]
    exact measurable_const

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

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
⊢ CountableOrCountablyGenerated (α × β) γ

pp: case inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
<;>

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : Countable α
⊢ CountableOrCountablyGenerated (α × β) γ

case inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hβ : CountableOrCountablyGenerated β γ
hα : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ
Module: Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

pp: case inl.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

pp: case inr.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountablyGenerated γ
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

pp: case inr.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

Tactic:
<;>

Goal state after:
case inl.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

case inl.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : Countable α
hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ

case inr.inl
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα : CountablyGenerated γ
hβ : Countable β
⊢ CountableOrCountablyGenerated (α × β) γ

case inr.inr
α✝ : Type u_1
β : Type u_2
m : MeasurableSpace α✝
h : CountablyGenerated α✝
α : Type u_3
γ : Type u_4
inst✝ : MeasurableSpace γ
hα hβ : CountablyGenerated γ
⊢ CountableOrCountablyGenerated (α × β) γ
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
⊢ AEMeasurable f (sum μ)

Tactic:
classical
  nontriviality β
  inhabit β
  set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x }
  have hsμ : ∀ i, μ i (s i) = 0 := by
    intro i
    rw [measure_toMeasurable]
    exact (h i).ae_eq_mk
  have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
  have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
    intro i x hx
    contrapose! hx
    exact subset_toMeasurable _ _ hx
  set g : α → β := (⋂ i, s i).piecewise (const α default) f
  refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
  · rw [domRestrict_piecewise]
    simp only [s]
    exact measurable_const
  · rw [domRestrict_piecewise_compl, compl_iInter]
    intro t ht
    refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
    ext ⟨x, hx⟩
    simp only [mem_preimage, mem_iUnion, Set.domRestrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢
    constructor
    · rintro ⟨i, hxt, hxs⟩
      rwa [hs _ _ hxs]
    · rcases hx with ⟨i, hi⟩
      rw [hs _ _ hi]
      exact fun h => ⟨i, h, hi⟩
  · refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)
    contrapose hx
    refine (piecewise_eq_of_notMem _ _ _ ?_).symm
    exact fun h => hx (mem_iInter.1 h i)

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

Goal state before:
pp: case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ AEMeasurable (s.indicator fun x ↦ b) μ → NullMeasurableSet s μ

pp: case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ NullMeasurableSet s μ → AEMeasurable (s.indicator fun x ↦ b) μ

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ AEMeasurable (s.indicator fun x ↦ b) μ → NullMeasurableSet s μ

case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
μ : Measure α
inst✝² : Zero β
s : Set α
inst✝¹ : MeasurableSingletonClass β
b : β
inst✝ : NeZero b
⊢ NullMeasurableSet s μ → AEMeasurable (s.indicator fun x ↦ b) μ
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
s : Set α
hs : MeasurableSet s
⊢ (sum (Function.extend f m 0)) s = (sum m) s

Tactic:
simp [*, Function.apply_extend (fun μ : Measure α ↦ μ s)]

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

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hf'm : NullMeasurable (fun i ↦ ↑(f' i)) μ
hff' : f =ᵐ[μ] fun i ↦ ↑(f' i)
⊢ AEMeasurable f μ

Tactic:
replace hf'm : NullMeasurable f' μ := hf'm.measurable'.subtype_mk

Goal state after:
case inr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ : Measure α
f : α → β
t : Set β
inst✝ : MeasurableSpace.CountablyGenerated ↑t
h : NullMeasurable f μ
hft : ∀ᵐ (x : α) ∂μ.completion, f x ∈ t
hne : t.Nonempty
f' : α → ↑t
hff' : f =ᵐ[μ] fun i ↦ ↑(f' i)
hf'm : NullMeasurable f' μ
⊢ AEMeasurable f μ
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι✝ : Sort y
s t u : Set α
inst✝¹⁶ : TopologicalSpace α
inst✝¹⁵ : MeasurableSpace α
inst✝¹⁴ : OpensMeasurableSpace α
inst✝¹³ : TopologicalSpace β
inst✝¹² : MeasurableSpace β
inst✝¹¹ : OpensMeasurableSpace β
inst✝¹⁰ : TopologicalSpace γ
inst✝⁹ : MeasurableSpace γ
inst✝⁸ : BorelSpace γ
inst✝⁷ : TopologicalSpace γ₂
inst✝⁶ : MeasurableSpace γ₂
inst✝⁵ : BorelSpace γ₂
inst✝⁴ : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst✝³ : Countable ι
t' : (i : ι) → TopologicalSpace (X i)
inst✝² : (i : ι) → MeasurableSpace (X i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (X i)
inst✝ : ∀ (i : ι), OpensMeasurableSpace (X i)
⊢ OpensMeasurableSpace ((i : ι) → X i)

Tactic:
constructor
  have : Pi.topologicalSpace = .generateFrom { t | ∃ (s : ∀ a, Set (X a)) (i : Finset ι),
      (∀ a ∈ i, s a ∈ countableBasis (X a)) ∧ t = pi (↑i) s } := by
    simp +instances only [funext fun a => @eq_generateFrom_countableBasis (X a) _ _,
      pi_generateFrom_eq]
  rw [borel_eq_generateFrom_of_subbasis this]
  apply generateFrom_le
  rintro _ ⟨s, i, hi, rfl⟩
  refine MeasurableSet.pi i.countable_toSet fun a ha => IsOpen.measurableSet ?_
  rw [eq_generateFrom_countableBasis (X a)]
  exact .basic _ (hi a ha)

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ x ∈ s ↔ infEDist x s = 0

Tactic:
by
  rw [← mem_closure_iff_infEDist_zero, h.closure_eq]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl.inr
α : Type u
inst✝ : PseudoEMetricSpace α
t : Set α
fin : hausdorffEDist t ∅ ≠ ∞
ht : t.Nonempty
⊢ ∅ = ∅ ∧ t = ∅ ∨ ∅.Nonempty ∧ t.Nonempty

Tactic:
exact Or.inr ⟨nonempty_of_hausdorffEDist_ne_top ht fin, ht⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : δ ≤ 0
⊢ cthickening (max 0 δ) E = cthickening δ E

pp: case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : 0 ≤ δ
⊢ cthickening (max 0 δ) E = cthickening δ E

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : δ ≤ 0
⊢ cthickening (max 0 δ) E = cthickening δ E

case inr
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
E : Set α
h✝ : 0 ≤ δ
⊢ cthickening (max 0 δ) E = cthickening δ E
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case left
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι), ∀ i_1 ∈ s i, ⨅ i, infEDist i_1 (t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

pp: case right
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι), ∀ i_1 ∈ t i, ⨅ i, infEDist i_1 (s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

Tactic:
<;>

Goal state after:
case left
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι), ∀ i_1 ∈ s i, ⨅ i, infEDist i_1 (t i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))

case right
α : Type u
inst✝ : PseudoEMetricSpace α
ι : Sort u_2
s t : ι → Set α
⊢ ∀ (i : ι), ∀ i_1 ∈ t i, ⨅ i, infEDist i_1 (s i) ≤ ⨆ i, max (⨆ x ∈ s i, infEDist x (t i)) (⨆ y ∈ t i, infEDist y (s i))
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

Goal state before:
pp: case e'_3.e'_2.mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} →
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

pp: case e'_3.e'_2.mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S} →
    s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S}

Tactic:
<;>

Goal state after:
case e'_3.e'_2.mp
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S} →
    s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S}

case e'_3.e'_2.mpr
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s✝ : Set α
hd : Dense s✝
hbot : ∀ (x : α), IsTop x → x ∈ s✝
hIoo : ∀ (x y : α), x < y → Ioo x y = ∅ → x ∈ s✝
e_1✝¹ : MeasurableSpace α = MeasurableSpace αᵒᵈ
e_1✝ : α = αᵒᵈ
s : Set α
⊢ s ∈ {S | ∃ l ∈ ⇑OrderDual.ofDual ⁻¹' s✝, ∃ u ∈ ⇑OrderDual.ofDual ⁻¹' s✝, l < u ∧ Ico l u = S} →
    s ∈ {S | ∃ l ∈ s✝, ∃ u ∈ s✝, l < u ∧ Ioc l u = S}
Module: Mathlib.Topology.MetricSpace.HausdorffDistance

Goal state before:
pp: case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ infEDist x ∅ = ∞ ↔ ∅ = ∅

pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ infEDist x s = ∞ ↔ s = ∅

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : PseudoMetricSpace α
x : α
⊢ infEDist x ∅ = ∞ ↔ ∅ = ∅

case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
hs : s.Nonempty
⊢ infEDist x s = ∞ ↔ s = ∅
Module: Mathlib.Topology.MetricSpace.Thickening

Goal state before:
pp: case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ⊆ thickening δ s

pp: case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ⊆ thickening δ t

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) s ⊆ thickening δ s

case refine_2
α : Type u
inst✝ : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
δ : ℝ
hδ : 0 < δ
h : Disjoint (thickening δ s) (thickening δ t)
⊢ cthickening (δ / 2) t ⊆ thickening δ t
Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Order

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

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

Tactic:
<;>

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

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