awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.snd (borel β)) (borel (α × β))

Tactic:
comap_le_iff_le_map.mpr continuous_snd.borel_measurable

Premises used: Iff.mpr, continuous_snd, 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.snd (borel β)) (borel (α × β))

Tactic:
exact comap_le_iff_le_map.mpr continuous_snd.borel_measurable

Premises used: Iff.mpr, MeasurableSpace.comap_le_iff_le_map
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst_8 : Countable ι
inst_9 : (i : ι) → TopologicalSpace (X i)
inst_10 : (i : ι) → MeasurableSpace (X i)
inst_11 : ∀ (i : ι), SecondCountableTopology.{u_7} (X i)
inst_12 : ∀ (i : ι), BorelSpace.{u_7} (X i)
⊢ BorelSpace ((i : ι) → X i)

Tactic:
⟨le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le⟩

Premises used: OpensMeasurableSpace.borel_le, le_antisymm, pi_le_borel_pi, BorelSpace.mk
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
γ₂ : Type u_4
δ : Type u_5
ι_1 : Sort y
s t u : Set α
inst : TopologicalSpace α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
ι : Type u_6
X : ι → Type u_7
inst_8 : Subsingleton ι
inst_9 : (i : ι) → TopologicalSpace (X i)
inst_10 : (i : ι) → MeasurableSpace (X i)
inst_11 : ∀ (i : ι), BorelSpace.{u_7} (X i)
⊢ BorelSpace ((i : ι) → X i)

Tactic:
⟨le_antisymm pi_le_borel_pi OpensMeasurableSpace.borel_le⟩

Premises used: OpensMeasurableSpace.borel_le, le_antisymm, pi_le_borel_pi, BorelSpace.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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
inst_8 : SecondCountableTopologyEither α β
⊢ BorelSpace (α × β)

Tactic:
⟨le_antisymm prod_le_borel_prod OpensMeasurableSpace.borel_le⟩

Premises used: OpensMeasurableSpace.borel_le, le_antisymm, BorelSpace.mk, prod_le_borel_prod
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
measurable_eq : inst = borel α
⊢ BorelSpace α

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ MeasurableSpace.comap e (borel β) = inst

Tactic:
simpa [hβ.measurable_eq] using h'e.comap_eq

Premises used: BorelSpace.measurable_eq, MeasurableEmbedding.comap_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
⊢ MeasurableSpace.comap e (borel β) = inst

Tactic:
have : MeasurableSpace.comap e (borel β) = ‹_› := by simpa [hβ.measurable_eq] using h'e.comap_eq
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Goal:
α : Type u_6
β : Type u_7
inst : MeasurableSpace α
inst_1 : TopologicalSpace α
inst_2 : MeasurableSpace β
inst_3 : TopologicalSpace β
hβ : BorelSpace β
e : α → β
h'e : MeasurableEmbedding e
h''e : IsInducing e
this : MeasurableSpace.comap e (borel β) = inst
measurable_eq : MeasurableSpace.comap e (borel β) = borel α
measurable_eq₁ : borel α = borel α
measurable_eq₂ measurable_eq₃ : borel α = borel α
⊢ inst = borel α

Tactic:
rw [← this, ← borel_comap, h''e.eq_induced]

Premises used: Topology.IsInducing.eq_induced, borel_comap
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace (ULift.{u_6, u_1} α)

Tactic:
MeasurableEquiv.ulift.measurableEmbedding.borelSpace Homeomorph.ulift.isInducing

Premises used: Homeomorph.isInducing, MeasurableEquiv.measurableEmbedding, MeasurableEquiv.ulift, Homeomorph.ulift, MeasurableEmbedding.borelSpace
-- 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
mα : MeasurableSpace α_1
inst_1 : BorelSpace α_1
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
α : Type u_6
inst_8 : TopologicalSpace α
inst_9 : DiscreteTopology α
inst_10 : MeasurableSpace α
inst_11 : DiscreteMeasurableSpace α
measurable_eq : inst_10 = borel α
⊢ BorelSpace α

Tactic:
constructor
-- 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
mα : MeasurableSpace α_1
inst_1 : BorelSpace α_1
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
α : Type u_6
inst_8 : TopologicalSpace α
inst_9 : DiscreteTopology α
inst_10 : MeasurableSpace α
inst_11 : DiscreteMeasurableSpace α
measurable_eq : ∀ (s : Set α), MeasurableSet s ↔ MeasurableSet s
⊢ inst_10 = borel α

Tactic:
ext
-- 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
mα : MeasurableSpace α_1
inst_1 : BorelSpace α_1
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
α : Type u_6
inst_8 : TopologicalSpace α
inst_9 : DiscreteTopology α
inst_10 : MeasurableSpace α
inst_11 : DiscreteMeasurableSpace α
s_1 : Set α
⊢ MeasurableSet s_1 ↔ MeasurableSet s_1

Tactic:
simp [MeasurableSpace.measurableSet_generateFrom, MeasurableSet.of_discrete]

Premises used: MeasurableSet.of_discrete, MeasurableSpace.measurableSet_generateFrom
-- 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 β
f : α → β
h₁ : IsEmbedding f
h₂ : MeasurableSet (range f)
⊢ MeasurableEmbedding f

Tactic:
show MeasurableEmbedding
      (((↑) : range f → β) ∘ h₁.toHomeomorph.toMeasurableEquiv) from
    (MeasurableEmbedding.subtype_coe h₂).comp (MeasurableEquiv.measurableEmbedding _)

Premises used: MeasurableEquiv.measurableEmbedding, Homeomorph.toMeasurableEquiv, MeasurableEmbedding.comp, Topology.IsEmbedding.toHomeomorph, MeasurableEmbedding.subtype_coe
-- 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 β
f : α → β
h : IsClosedEmbedding f
⊢ MeasurableEmbedding f

Tactic:
h.isEmbedding.measurableEmbedding h.isClosed_range.measurableSet

Premises used: IsClosed.measurableSet, Topology.IsClosedEmbedding.isEmbedding, Topology.IsClosedEmbedding.isClosed_range, Topology.IsEmbedding.measurableEmbedding
-- 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 β
f : α → β
h : IsOpenEmbedding f
⊢ MeasurableEmbedding f

Tactic:
h.isEmbedding.measurableEmbedding h.isOpen_range.measurableSet

Premises used: Topology.IsOpenEmbedding.isEmbedding, IsOpen.measurableSet, Topology.IsOpenEmbedding.isOpen_range, Topology.IsEmbedding.measurableEmbedding
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace Empty

Tactic:
⟨borel_eq_top_of_discrete.symm⟩

Premises used: borel_eq_top_of_discrete, BorelSpace.mk, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace Unit

Tactic:
⟨borel_eq_top_of_discrete.symm⟩

Premises used: borel_eq_top_of_discrete, BorelSpace.mk, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace Bool

Tactic:
⟨borel_eq_top_of_discrete.symm⟩

Premises used: borel_eq_top_of_discrete, BorelSpace.mk, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℕ

Tactic:
⟨borel_eq_top_of_discrete.symm⟩

Premises used: borel_eq_top_of_discrete, BorelSpace.mk, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℤ

Tactic:
⟨borel_eq_top_of_discrete.symm⟩

Premises used: borel_eq_top_of_discrete, BorelSpace.mk, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℚ

Tactic:
⟨borel_eq_top_of_countable.symm⟩

Premises used: BorelSpace.mk, borel_eq_top_of_countable, Eq.symm
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℝ

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℝ≥0

Tactic:
inferInstanceAs <| BorelSpace (Subtype _)

Premises used: _private.0.NNReal.borelSpace._proof_1
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace ℝ≥0∞

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- 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 α
mα : MeasurableSpace α
inst_1 : BorelSpace α
mβ : TopologicalSpace β
inst_2 : MeasurableSpace β
inst_3 : BorelSpace β
inst_4 : TopologicalSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
inst_7 : MeasurableSpace δ
⊢ BorelSpace EReal

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- 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 β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_2) (map (⇑f : (a : α) → β) μ)

Tactic:
⟨fun K hK ↦ ?_⟩

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.mk
-- 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 β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
refine :
  ∀ (K : Set β) (hK : IsCompact K),
    LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasureOnCompacts.{u_2} (α := β) (m0 := inst_2) (map (⇑f : (a : α) → β) μ)

Tactic:
refine ⟨fun K hK ↦ ?_⟩
-- 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 β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f.toMeasurableEquiv : (a : α) → β) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((map (⇑f : (a : α) → β) μ : Measure β) : (a : Set β) → ℝ≥0∞) K : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← f.toMeasurableEquiv_coe, MeasurableEquiv.map_apply]

Premises used: MeasurableEquiv.map_apply, Homeomorph.toMeasurableEquiv_coe
-- 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 β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f.toMeasurableEquiv : (a : α) → β) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

Premises used: Iff.mpr, Homeomorph.isCompact_preimage, IsCompact.measure_lt_top
-- 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 β
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((⇑f.toMeasurableEquiv : (a : α) → β) ⁻¹' K) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact IsCompact.measure_lt_top (f.isCompact_preimage.2 hK)

Premises used: Iff.mpr, Homeomorph.isCompact_preimage, IsCompact.measure_lt_top
-- 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 β
μ : Measure β
inst_4 : IsFiniteMeasureOnCompacts μ
f : α ≃ₜ β
⊢ IsFiniteMeasureOnCompacts.{u_1} (α := α) (m0 := mα) (comap (⇑f : (a : α) → β) μ)

Tactic:
IsFiniteMeasureOnCompacts.comap' μ f.continuous f.measurableEmbedding

Premises used: Homeomorph.continuous, Homeomorph.measurableEmbedding, MeasureTheory.IsFiniteMeasureOnCompacts.comap'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
⊢ BorelSpace 𝕜

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
Goal:
⊢ BorelSpace ℂ

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
R : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring R
inst_1 : SeminormedAddCommGroup E
inst_2 : Module R E
inst_3 : MeasurableSpace E
inst_4 : OpensMeasurableSpace E
inst_5 : SeminormedAddCommGroup F
inst_6 : Module R F
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
L : E →L[R] F
⊢ Measurable.{u_3, u_4} (α := E) (β := F) (⇑L : (a : E) → F)

Tactic:
L.continuous.measurable

Premises used: ContinuousLinearMap.continuous, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
R : Type u_2
E : Type u_3
F : Type u_4
inst_1 : Semiring R
inst_2 : SeminormedAddCommGroup E
inst_3 : Module R E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
inst_6 : SeminormedAddCommGroup F
inst_7 : Module R F
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
L : E →L[R] F
φ : α → E
φ_meas : Measurable φ
⊢ Measurable.{u_1, u_4} (β := F) fun (a : α) ↦ (L : (a : E) → F) (φ a)

Tactic:
L.measurable.comp φ_meas

Premises used: ContinuousLinearMap.measurable, Measurable.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
F : Type u_4
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
⊢ BorelSpace (E →L[𝕜] F)

Tactic:
⟨rfl⟩

Premises used: BorelSpace.mk, rfl
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
x : E
⊢ Measurable (β := F) fun (f : E →L[𝕜] F) ↦ (f : (a : E) → F) x

Tactic:
(apply 𝕜 F x).continuous.measurable

Premises used: ContinuousLinearMap.continuous, ContinuousLinearMap.apply, Continuous.measurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : MeasurableSpace F
inst_8 : BorelSpace F
⊢ Measurable (β := (f : E →L[𝕜] F) → F) fun (x : E) (f : E →L[𝕜] F) ↦ (f : (a : E) → F) x

Tactic:
measurable_pi_lambda _ fun f => f.measurable

Premises used: ContinuousLinearMap.measurable, measurable_pi_lambda
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_4
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : MeasurableSpace F
inst_6 : BorelSpace F
⊢ Measurable (β := (x : E) → F) fun (f : E →L[𝕜] F) (x : E) ↦ (f : (a : E) → F) x

Tactic:
measurable_pi_lambda _ measurable_apply

Premises used: measurable_pi_lambda, ContinuousLinearMap.measurable_apply
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
F : Type u_4
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
φ : α → F →L[𝕜] E
hφ : Measurable φ
v : F
⊢ Measurable.{u_1, u_3} (β := E) fun (a : α) ↦ (φ a : (a : F) → E) v

Tactic:
(ContinuousLinearMap.apply 𝕜 E v).measurable.comp hφ

Premises used: ContinuousLinearMap.measurable, Measurable.comp, ContinuousLinearMap.apply, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
E : Type u_3
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
F : Type u_4
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
φ : α → F →L[𝕜] E
μ : Measure α
hφ : AEMeasurable φ μ
v : F
⊢ AEMeasurable.{u_1, u_3} (β := E) (fun (a : α) ↦ (φ a : (a : F) → E) v) μ

Tactic:
(ContinuousLinearMap.apply 𝕜 E v).measurable.comp_aemeasurable hφ

Premises used: ContinuousLinearMap.measurable, ContinuousLinearMap.apply, Measurable.comp_aemeasurable, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
E : Type u_3
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
f : α → 𝕜
c : E
hc : c ≠ 0
⊢ (Measurable.{u_1, u_3} (β := E) fun (x : α) ↦ f x • c) ↔ Measurable f

Tactic:
(isClosedEmbedding_smul_left hc).measurableEmbedding.measurable_comp_iff

Premises used: Topology.IsClosedEmbedding.measurableEmbedding, MeasurableEmbedding.measurable_comp_iff, isClosedEmbedding_smul_left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap
Goal:
α : Type u_1
inst : MeasurableSpace α
𝕜 : Type u_2
inst_1 : NontriviallyNormedField 𝕜
inst_2 : CompleteSpace 𝕜
inst_3 : MeasurableSpace 𝕜
inst_4 : BorelSpace 𝕜
E : Type u_3
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
inst_7 : MeasurableSpace E
inst_8 : BorelSpace E
f : α → 𝕜
μ : Measure α
c : E
hc : c ≠ 0
⊢ AEMeasurable.{u_1, u_3} (β := E) (fun (x : α) ↦ f x • c) μ ↔ AEMeasurable f μ

Tactic:
(isClosedEmbedding_smul_left hc).measurableEmbedding.aemeasurable_comp_iff

Premises used: MeasurableEmbedding.aemeasurable_comp_iff, Topology.IsClosedEmbedding.measurableEmbedding, isClosedEmbedding_smul_left