awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : T0Space α
x y : α
⊢ x ≠ y → ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
fun a => exists_measurableSet_of_ne a

Premises used: MeasurableSpace.exists_measurableSet_of_ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : T0Space α
x y : α
⊢ x ≠ y → ∃ (s : Set α), MeasurableSet s ∧ x ∈ s ∧ y ∉ s

Tactic:
exact fun a => exists_measurableSet_of_ne a

Premises used: MeasurableSpace.exists_measurableSet_of_ne
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f : α → γ
hf : Continuous[inst, inst_3] f
⊢ Measurable f

Tactic:
hf.borel_measurable.mono OpensMeasurableSpace.borel_le (le_of_eq <| BorelSpace.measurable_eq)

Premises used: OpensMeasurableSpace.borel_le, BorelSpace.measurable_eq, Continuous.borel_measurable, le_of_eq, Measurable.mono
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f : α → γ
h : Continuous[inst, inst_3] f
μ : Measure α
⊢ AEMeasurable f μ

Tactic:
h.measurable.aemeasurable

Premises used: Measurable.aemeasurable, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f : α → γ
hf : IsClosedEmbedding f
⊢ Measurable f

Tactic:
hf.continuous.measurable

Premises used: Topology.IsClosedEmbedding.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
⊢ Measurable (s.piecewise (β := fun (a : α) ↦ γ) f g)

Tactic:
measurable_of_isOpen fun t ht => ?_

Premises used: measurable_of_isOpen
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
refine : ∀ (t : Set γ) (ht : IsOpen[inst_3] t), MeasurableSet (s.piecewise (β := fun (a : α) ↦ γ) f g ⁻¹' t)
⊢ Measurable (s.piecewise (β := fun (a : α) ↦ γ) f g)

Tactic:
refine measurable_of_isOpen fun t ht => ?_

Premises used: measurable_of_isOpen
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
rw : MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
⊢ MeasurableSet (s.piecewise (β := fun (a : α) ↦ γ) f g ⁻¹' t)

Tactic:
rw [piecewise_preimage, Set.ite]

Premises used: Set.ite, Set.piecewise_preimage
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
h₁ : MeasurableSet (f ⁻¹' t ∩ s)
h₂ : MeasurableSet (g ⁻¹' t \ s)
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)

Tactic:
apply MeasurableSet.union

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
h₁ : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : f ⁻¹' t ∩ s = u ∩ s), MeasurableSet (f ⁻¹' t ∩ s)
⊢ MeasurableSet (f ⁻¹' t ∩ s)

Tactic:
rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
h₁ : MeasurableSet (u ∩ s)
⊢ MeasurableSet (f ⁻¹' t ∩ s)

Tactic:
rw [hu]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s)

Tactic:
u_open.measurableSet.inter hs

Premises used: IsOpen.measurableSet, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s)

Tactic:
exact u_open.measurableSet.inter hs

Premises used: IsOpen.measurableSet, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
h₂ : ∀ (u : Set α) (u_open : IsOpen[inst] u) (hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ), MeasurableSet (g ⁻¹' t \ s)
⊢ MeasurableSet (g ⁻¹' t \ s)

Tactic:
rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩

Premises used: Iff.mp, continuousOn_iff'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
h₂ : MeasurableSet (u ∩ sᶜ)
⊢ MeasurableSet (g ⁻¹' t \ s)

Tactic:
rw [diff_eq_compl_inter, inter_comm, hu]

Premises used: Set.diff_eq_compl_inter, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (u ∩ sᶜ)

Tactic:
u_open.measurableSet.inter hs.compl

Premises used: IsOpen.measurableSet, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f g : α → γ
s : Set α
inst_6 : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g sᶜ
hs : MeasurableSet s
t : Set γ
ht : IsOpen[inst_3] t
u : Set α
u_open : IsOpen[inst] u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (u ∩ sᶜ)

Tactic:
exact u_open.measurableSet.inter hs.compl

Premises used: IsOpen.measurableSet, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : Inv γ
inst_16 : ContinuousInv γ
⊢ MeasurableInv γ

Tactic:
⟨continuous_inv.measurable⟩

Premises used: MeasurableInv.mk, Continuous.measurable, ContinuousInv.continuous_inv
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
h : α ≃ₜ γ
⊢ Measurable.{u_1, u_3} (α := α) (β := γ) (⇑h : (a : α) → γ)

Tactic:
h.continuous.measurable

Premises used: Homeomorph.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
γ₂ : Type u_4
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : TopologicalSpace γ₂
inst_4 : MeasurableSpace γ₂
inst_5 : BorelSpace γ₂
h : γ ≃ₜ γ₂
⊢ MeasurableEmbedding.{u_3, u_4} (α := γ) (β := γ₂) (⇑h : (a : γ) → γ₂)

Tactic:
h.toMeasurableEquiv.measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, Homeomorph.toMeasurableEquiv
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
γ₂ : Type u_4
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : TopologicalSpace γ₂
inst_4 : MeasurableSpace γ₂
inst_5 : BorelSpace γ₂
h : γ ≃ₜ γ₂
⊢ Eq (α := (a : γ) → γ₂) (⇑h.toMeasurableEquiv : (a : γ) → γ₂) (⇑h : (a : γ) → γ₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
γ : Type u_3
γ₂ : Type u_4
inst : TopologicalSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
inst_3 : TopologicalSpace γ₂
inst_4 : MeasurableSpace γ₂
inst_5 : BorelSpace γ₂
h : γ ≃ₜ γ₂
⊢ Eq (α := (a : γ₂) → γ) (⇑(MeasurableEquiv.symm h.toMeasurableEquiv) : (a : γ₂) → γ) (⇑h.symm : (a : γ₂) → γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
f : C(α, γ)
⊢ Measurable.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)

Tactic:
f.continuous.measurable

Premises used: ContinuousMap.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
γ : Type u_3
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
inst_6 : T1Space α
f : α → γ
a : α
hf : ContinuousOn f {a}ᶜ
⊢ Measurable f

Tactic:
measurable_of_measurable_on_compl_singleton a
    (continuousOn_iff_continuous_restrict.1 hf).measurable

Premises used: continuousOn_iff_continuous_restrict, measurable_of_measurable_on_compl_singleton, Continuous.measurable, Iff.mp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : MeasurableSpace δ
inst_10 : SecondCountableTopologyEither α β
f : δ → α
g : δ → β
c : α → β → γ
h : Continuous[instTopologicalSpaceProd, inst_6] fun (p : α × β) ↦ c p.1 p.2
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_5, u_3} (β := γ) fun (a : δ) ↦ c (f a) (g a)

Tactic:
h.measurable.comp (hf.prodMk hg)

Premises used: Measurable.comp, Measurable.prodMk, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_5
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : MeasurableSpace δ
inst_10 : SecondCountableTopologyEither α β
f : δ → α
g : δ → β
c : α → β → γ
μ : Measure δ
h : Continuous[instTopologicalSpaceProd, inst_6] fun (p : α × β) ↦ c p.1 p.2
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_5, u_3} (β := γ) (fun (a : δ) ↦ c (f a) (g a)) μ

Tactic:
h.measurable.comp_aemeasurable (hf.prodMk hg)

Premises used: AEMeasurable.prodMk, Continuous.measurable, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : GroupWithZero γ
inst_16 : T1Space γ
inst_17 : ContinuousInv₀ γ
⊢ MeasurableInv γ

Tactic:
⟨measurable_of_continuousOn_compl_singleton 0 continuousOn_inv₀⟩

Premises used: MeasurableInv.mk, continuousOn_inv₀, measurable_of_continuousOn_compl_singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : SecondCountableTopology γ
inst_16 : Mul γ
inst_17 : ContinuousMul γ
⊢ MeasurableMul₂ γ

Tactic:
⟨continuous_mul.measurable⟩

Premises used: ContinuousMul.continuous_mul, Continuous.measurable, MeasurableMul₂.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : SecondCountableTopology γ
inst_16 : Sub γ
inst_17 : ContinuousSub γ
⊢ MeasurableSub₂ γ

Tactic:
⟨continuous_sub.measurable⟩

Premises used: ContinuousSub.continuous_sub, MeasurableSub₂.mk, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α_1
inst : TopologicalSpace α_1
inst_1 : MeasurableSpace α_1
inst_2 : OpensMeasurableSpace α_1
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
M : Type u_7
α : Type u_8
inst_15 : TopologicalSpace M
inst_16 : MeasurableSpace M
inst_17 : OpensMeasurableSpace M
inst_18 : TopologicalSpace α
inst_19 : SecondCountableTopologyEither M α
inst_20 : MeasurableSpace α
inst_21 : BorelSpace α
inst_22 : SMul M α
inst_23 : ContinuousSMul M α
⊢ MeasurableSMul₂ M α

Tactic:
⟨continuous_smul.measurable⟩

Premises used: Continuous.measurable, ContinuousSMul.continuous_smul, MeasurableSMul₂.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι : Sort y
s t u : Set α
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
inst_6 : TopologicalSpace γ
inst_7 : MeasurableSpace γ
inst_8 : BorelSpace γ
inst_9 : TopologicalSpace γ₂
inst_10 : MeasurableSpace γ₂
inst_11 : BorelSpace γ₂
inst_12 : MeasurableSpace δ
α' : Type u_6
inst_13 : TopologicalSpace α'
inst_14 : MeasurableSpace α'
inst_15 : SecondCountableTopology α
inst_16 : T2Space α
⊢ MeasurableEq α

Tactic:
⟨isClosed_diagonal.measurableSet⟩

Premises used: IsClosed.measurableSet, isClosed_diagonal, MeasurableEq.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
⊢ inst_1 = fun (i : ι) ↦ borel (X i)

Tactic:
have : ‹∀ i, MeasurableSpace (X i)› = fun i => borel (X i) :=
    funext fun i => BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
this : inst_1 = fun (i : ι) ↦ borel (X i)
rw : LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))
⊢ LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
this : inst_1 = fun (i : ι) ↦ borel (X i)
⊢ LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))

Tactic:
iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable

Premises used: Iff.mpr, Continuous.borel_measurable, MeasurableSpace.comap_le_iff_le_map, iSup_le, continuous_apply
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
ι : Type u_6
X : ι → Type u_7
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : (i : ι) → MeasurableSpace (X i)
inst_2 : ∀ (i : ι), BorelSpace.{u_7} (X i)
this : inst_1 = fun (i : ι) ↦ borel (X i)
⊢ LE.le (α := MeasurableSpace ((a : ι) → X a)) (MeasurableSpace.pi (X := X)) (borel ((i : ι) → X i))

Tactic:
exact iSup_le fun i => comap_le_iff_le_map.2 <| (continuous_apply i).borel_measurable

Premises used: Iff.mpr, MeasurableSpace.comap_le_iff_le_map, iSup_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
rw : LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))

Tactic:
rw [‹BorelSpace α›.measurable_eq, ‹BorelSpace β›.measurable_eq]

Premises used: BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))

Tactic:
sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
refine_1 : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (borel α)) (borel (α × β))
refine_2 : LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.snd (borel β)) (borel (α × β))
⊢ LE.le (α := MeasurableSpace (α × β)) Prod.instMeasurableSpace (borel (α × β))

Tactic:
refine sup_le ?_ ?_

Premises used: sup_le
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (borel α)) (borel (α × β))

Tactic:
comap_le_iff_le_map.mpr continuous_fst.borel_measurable

Premises used: Iff.mpr, continuous_fst, Continuous.borel_measurable, MeasurableSpace.comap_le_iff_le_map
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
⊢ LE.le (α := MeasurableSpace (α × β)) (MeasurableSpace.comap Prod.fst (borel α)) (borel (α × β))

Tactic:
exact comap_le_iff_le_map.mpr continuous_fst.borel_measurable

Premises used: Iff.mpr, MeasurableSpace.comap_le_iff_le_map