awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
⊢ MeasurePreserving (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ) (Measure.dirac ())

Tactic:
⟨e.measurable, ?_⟩

Premises used: MeasureTheory.MeasurePreserving.mk, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
refine :
  Eq (α := Measure Unit) (Measure.map (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ)) (Measure.dirac ())
⊢ MeasurePreserving (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ) (Measure.dirac ())

Tactic:
refine ⟨e.measurable, ?_⟩
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
m : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → Measure (α i)
e : ((i : ι) → α i) ≃ᵐ Unit := MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit
rw :
  Eq (α := Measure Unit)
    (Measure.map (α := (i : ι) → α i) (⇑e : (a : (i : ι) → α i) → Unit)
      (Measure.dirac fun (a : ι) ↦ isEmptyElim (p := fun (x : ι) ↦ α x) a))
    (Measure.dirac ())
rw₁ rw₂ :
  Eq (α := Measure Unit)
    (Measure.dirac ((e : (a : (i : ι) → α i) → Unit) fun (a : ι) ↦ isEmptyElim (p := fun (x : ι) ↦ α x) a) :
      Measure Unit)
    (Measure.dirac () : Measure Unit)
⊢ Eq (α := Measure Unit) (Measure.map (⇑e : (a : (i : ι) → α i) → Unit) (Measure.pi (α := α) μ)) (Measure.dirac ())

Tactic:
rw [Measure.pi_of_empty, Measure.map_dirac' e.measurable]

Premises used: MeasureTheory.Measure.pi_of_empty, isEmptyElim, MeasureTheory.Measure.map_dirac', MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u
α : ι → Type v
inst : Fintype ι
inst_1 : IsEmpty ι
inst_2 : (i : ι) → MeasureSpace (α i)
⊢ MeasurePreserving (α := (i : ι) → α i) (β := Unit)
    (⇑(MeasurableEquiv.ofUniqueOfUnique ((i : ι) → α i) Unit) : (a : (i : ι) → α i) → Unit) volume volume

Tactic:
measurePreserving_pi_empty fun _ => volume

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_pi_empty
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
α : ι → Type u_5
x : (i : ι) → MeasurableSpace (α i)
inst : DecidableEq ι
s t : Finset ι
h : Disjoint s t
μ : (i : ι) → Measure (α i)
inst_1 : ∀ (i : ι), SigmaFinite (μ i)
⊢ MeasurePreserving (α := ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) (β := (i : ↥(s ∪ t)) → α (↑i : ι))
    (⇑(MeasurableEquiv.piFinsetUnion α h) :
      (a : ((i : ↥s) → α (↑i : ι)) × ((i : ↥t) → α (↑i : ι))) → (i : ↥(s ∪ t)) → α (↑i : ι))
    (Measure.prod (Measure.pi (α := fun (i : ↥s) ↦ α (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
      (Measure.pi (α := fun (i : ↥t) ↦ α (↑i : ι)) fun (i : ↥t) ↦ μ (↑i : ι)))
    (Measure.pi (α := fun (i : ↥(s ∪ t)) ↦ α (↑i : ι)) fun (i : ↥(s ∪ t)) ↦ μ (↑i : ι))

Tactic:
let e := Equiv.Finset.union s t h
  measurePreserving_piCongrLeft (fun i : ↥(s ∪ t) ↦ μ i) e |>.comp <|
    measurePreserving_sumPiEquivProdPi_symm fun b ↦ μ (e b)

Premises used: MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasurePreserving.comp, MeasureTheory.measurePreserving_sumPiEquivProdPi_symm, Subtype.val, DFunLike.coe, Equiv.Finset.union
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : DecidableEq ι
α : ι → Type u_5
s t : Finset ι
h : Disjoint s t
inst_1 : (i : ι) → MeasureSpace (α i)
inst_2 : ∀ (i : ι), SigmaFinite.{u_5} (α := α i) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
measurePreserving_piFinsetUnion h (fun _ ↦ volume)

Premises used: MeasureTheory.MeasureSpace.volume, MeasureTheory.measurePreserving_piFinsetUnion
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
⊢ ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))

Tactic:
have (i : ι) : SigmaFinite ((μ i).map (f i)) := (hf i).map_eq ▸ hν i
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))
rw : (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (μ i)) = Measure.pi (α := β) ν
⊢ Measure.map (fun (a : (i : ι) → α i) (i : ι) ↦ f i (a i)) (Measure.pi (α := α) μ) = Measure.pi (α := β) ν

Tactic:
rw [pi_map_pi (fun i ↦ (hf i).aemeasurable)]

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.Measure.pi_map_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))
⊢ (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (μ i)) = Measure.pi (α := β) ν

Tactic:
congrArg _ <| funext fun i ↦ (hf i).map_eq

Premises used: congrArg, MeasureTheory.MeasurePreserving.map_eq, funext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_4
inst : Fintype ι
α : ι → Type v
β : ι → Type u_5
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → MeasurableSpace (β i)
μ : (i : ι) → Measure (α i)
ν : (i : ι) → Measure (β i)
f : (i : ι) → α i → β i
hν : ∀ (i : ι), SigmaFinite (ν i)
hf : ∀ (i : ι), MeasurePreserving (f i) (μ i) (ν i)
this : ∀ (i : ι), SigmaFinite (m0 := inst_2 i) (Measure.map (f i) (μ i))
⊢ (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (μ i)) = Measure.pi (α := β) ν

Tactic:
exact congrArg _ <| funext fun i ↦ (hf i).map_eq

Premises used: congrArg, MeasureTheory.MeasurePreserving.map_eq, funext
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
ι : Type u_1
inst : Fintype ι
α' : ι → Type u_4
β' : ι → Type u_5
inst_1 : (i : ι) → MeasureSpace (α' i)
inst_2 : (i : ι) → MeasureSpace (β' i)
inst_3 : ∀ (i : ι), SigmaFinite.{u_5} (α := β' i) (m0 := MeasureSpace.toMeasurableSpace) volume
f : (i : ι) → α' i → β' i
hf : ∀ (i : ι), MeasurePreserving (f i) volume volume
⊢ MeasurePreserving (β := (i : ι) → β' i) (fun (a : (i : ι) → α' i) (i : ι) ↦ f i (a i))
    (volume : Measure ((i : ι) → α' i)) (volume : Measure ((i : ι) → β' i))

Tactic:
measurePreserving_pi _ _ hf

Premises used: MeasureTheory.measurePreserving_pi
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
⊢ MeasurePreserving (β := (a : α₂) → β₂)
    (comp (β := (b : α₁) → β₂)
      (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
        (a : (b : α₁) → β₂) → (a : α₂) → β₂)
      fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))
    (Measure.pi (α := fun (i : α₁) ↦ β₁) μ) (Measure.pi (α := fun (i : α₂) ↦ β₂) fun (i : α₂) ↦ ν i)

Tactic:
(measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)

Premises used: MeasureTheory.measurePreserving_pi, MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasurePreserving.comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
h :
  Eq (α := (α₁ → β₁) → α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (comp (β := (b : α₁) → β₂)
      (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
        (a : (b : α₁) → β₂) → (a : α₂) → β₂)
      fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))
⊢ MeasurePreserving (α := α₁ → β₁) (β := α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (Measure.pi (α := fun (a : α₁) ↦ β₁) fun (i : α₁) ↦ μ i) (Measure.pi (α := fun (a : α₂) ↦ β₂) fun (i : α₂) ↦ ν i)

Tactic:
convert!
    (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)

Premises used: MeasureTheory.measurePreserving_pi, MeasureTheory.measurePreserving_piCongrLeft, MeasureTheory.MeasurePreserving.comp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
⊢ Eq (α := (α₁ → β₁) → α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (comp (β := (b : α₁) → β₂)
      (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
        (a : (b : α₁) → β₂) → (a : α₂) → β₂)
      fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))

Tactic:
simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
    comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
    Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, MeasurableEquiv.arrowCongr', Equiv.arrowCongr, MeasurableEquiv.piCongrLeft, Equiv.symm_symm, MeasurableEquiv.coe_mk, Equiv.piCongrLeft, Equiv.arrowCongr', Function.comp_def, Equiv.piCongrLeft', Equiv.coe_fn_mk, eq_rec_constant, EquivLike.coe_coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasurableSpace β₁
inst_3 : MeasurableSpace β₂
μ : α₁ → Measure β₁
ν : α₂ → Measure β₂
inst_4 : ∀ (i : α₂), SigmaFinite (ν i)
eα : α₁ ≃ α₂
eβ : β₁ ≃ᵐ β₂
hm : ∀ (i : α₁), MeasurePreserving (⇑eβ : (a : β₁) → β₂) (μ i) (ν ((eα : (a : α₁) → α₂) i))
h :
  Eq (α := (α₁ → β₁) → α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (comp (β := (b : α₁) → β₂)
      (⇑(MeasurableEquiv.piCongrLeft.{u_4, u_6, u_7} (fun (i : α₂) ↦ β₂) eα : ((b : α₁) → β₂) ≃ᵐ ((a : α₂) → β₂)) :
        (a : (b : α₁) → β₂) → (a : α₂) → β₂)
      fun (a : (i : α₁) → β₁) (i : α₁) ↦ (eβ : (a : β₁) → β₂) (a i))
⊢ MeasurePreserving (α := α₁ → β₁) (β := α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' eα eβ) : (a : α₁ → β₁) → α₂ → β₂)
    (Measure.pi (α := fun (a : α₁) ↦ β₁) fun (i : α₁) ↦ μ i) (Measure.pi (α := fun (a : α₂) ↦ β₂) fun (i : α₂) ↦ ν i)

Tactic:
classical
  convert!
    (measurePreserving_piCongrLeft (fun i : α₂ ↦ ν i) eα).comp
      (measurePreserving_pi μ (fun i : α₁ ↦ ν (eα i)) hm)
  simp only [MeasurableEquiv.arrowCongr', Equiv.arrowCongr', Equiv.arrowCongr, EquivLike.coe_coe,
    comp_def, MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, MeasurableEquiv.piCongrLeft,
    Equiv.piCongrLeft, Equiv.symm_symm, Equiv.piCongrLeft', eq_rec_constant, Equiv.coe_fn_symm_mk]

Premises used: Equiv.coe_fn_symm_mk, MeasureTheory.measurePreserving_pi, MeasurableEquiv.arrowCongr', Equiv.arrowCongr, MeasureTheory.measurePreserving_piCongrLeft, MeasurableEquiv.piCongrLeft, Equiv.symm_symm, MeasurableEquiv.coe_mk, Equiv.piCongrLeft, Equiv.arrowCongr', Function.comp_def, Equiv.piCongrLeft', Equiv.coe_fn_mk, eq_rec_constant, MeasureTheory.MeasurePreserving.comp, DFunLike.coe, EquivLike.coe_coe
-- Module: Mathlib.MeasureTheory.Constructions.Pi
Goal:
α₁ : Type u_4
β₁ : Type u_5
α₂ : Type u_6
β₂ : Type u_7
inst : Fintype α₁
inst_1 : Fintype α₂
inst_2 : MeasureSpace β₁
inst_3 : MeasureSpace β₂
inst_4 : SigmaFinite.{u_7} (α := β₂) (m0 := MeasureSpace.toMeasurableSpace) volume
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
hm : MeasurePreserving.{u_5, u_7} (α := β₁) (β := β₂) (⇑hβ : (a : β₁) → β₂) volume volume
⊢ MeasurePreserving (α := α₁ → β₁) (β := α₂ → β₂) (⇑(MeasurableEquiv.arrowCongr' hα hβ) : (a : α₁ → β₁) → α₂ → β₂)
    (volume : Measure (α₁ → β₁)) (volume : Measure (α₂ → β₂))

Tactic:
measurePreserving_arrowCongr' (fun _ ↦ volume) (fun _ ↦ volume) hα hβ (fun _ ↦ hm)

Premises used: MeasureTheory.measurePreserving_arrowCongr', MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
h : StandardBorelSpace α
choose : (τ : TopologicalSpace α) → (hb : BorelSpace α) → (hp : PolishSpace α) → UpgradedStandardBorel α
⊢ UpgradedStandardBorel α

Tactic:
choose τ hb hp using h.polish

Premises used: StandardBorelSpace.polish
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
h : StandardBorelSpace α
τ : TopologicalSpace α
hb : BorelSpace α
hp : PolishSpace α
⊢ UpgradedStandardBorel α

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ inst = borel α

Tactic:
@BorelSpace.measurable_eq _ (upgradeStandardBorel α).toTopologicalSpace _
    (upgradeStandardBorel α).toBorelSpace

Premises used: BorelSpace.measurable_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
τ : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : PolishSpace α
exists exists₁ : BorelSpace α ∧ PolishSpace α
⊢ StandardBorelSpace α

Tactic:
exists τ
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : DiscreteMeasurableSpace α
inst_2 : Countable α
⊢ StandardBorelSpace α

Tactic:
let _ : TopologicalSpace α := ⊥
  have : DiscreteTopology α := ⟨rfl⟩
  inferInstance

Premises used: inferInstance, Bot.bot, DiscreteTopology.mk, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ MeasurableSpace.CountablyGenerated α

Tactic:
letI := upgradeStandardBorel α
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ MeasurableSingletonClass α

Tactic:
letI := upgradeStandardBorel α
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : StandardBorelSpace α
inst_3 : StandardBorelSpace β
⊢ StandardBorelSpace (α × β)

Tactic:
letI := upgradeStandardBorel α
  letI := upgradeStandardBorel β
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α_1 : Type u_1
inst : MeasurableSpace α_1
β : Type u_2
inst_1 : MeasurableSpace β
ι : Type u_3
inst_2 : Countable ι
α : ι → Type u_4
inst_3 : (n : ι) → MeasurableSpace (α n)
inst_4 : ∀ (n : ι), StandardBorelSpace.{u_4} (α n)
⊢ StandardBorelSpace ((n : ι) → α n)

Tactic:
letI := fun n => upgradeStandardBorel (α n)
  inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
inst_2 : StandardBorelSpace α
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ MeasurableEq α

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = ∅
⊢ AnalyticSet.{u_1} (α := α) ∅

Tactic:
rw [AnalyticSet]

Premises used: MeasureTheory.AnalyticSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = ∅

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Eq.{u_1 + 1} (α := Set α) ∅ ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = ∅

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
inl : IsEmpty β → AnalyticSet (range f)
inr : Nonempty β → AnalyticSet (range f)
⊢ AnalyticSet (range f)

Tactic:
cases isEmpty_or_nonempty β

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : IsEmpty β
inl : AnalyticSet.{u_1} (α := α) ∅
⊢ AnalyticSet (range f)

Tactic:
rw [range_eq_empty]

Premises used: Set.range_eq_empty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : IsEmpty β
⊢ AnalyticSet.{u_1} (α := α) ∅

Tactic:
analyticSet_empty

Premises used: MeasureTheory.analyticSet_empty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : IsEmpty β
⊢ AnalyticSet.{u_1} (α := α) ∅

Tactic:
exact analyticSet_empty

Premises used: MeasureTheory.analyticSet_empty
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
inr : range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
⊢ AnalyticSet (range f)

Tactic:
rw [AnalyticSet]

Premises used: MeasureTheory.AnalyticSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
⊢ ∃ (g : (ℕ → ℕ) → β), Continuous[_, inst_1] g ∧ Surjective g

Tactic:
exists_nat_nat_continuous_surjective β

Premises used: PolishSpace.exists_nat_nat_continuous_surjective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
inr :
  ∀ (g : (ℕ → ℕ) → β) (g_cont : Continuous[_, inst_1] g) (hg : Surjective g),
    range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f
⊢ range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f

Tactic:
obtain ⟨g, g_cont, hg⟩ : ∃ g : (ℕ → ℕ) → β, Continuous g ∧ Surjective g :=
      exists_nat_nat_continuous_surjective β

Premises used: PolishSpace.exists_nat_nat_continuous_surjective
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst_1] g
hg : Surjective g
⊢ range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f

Tactic:
Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩

Premises used: Continuous.comp, Function.comp, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst_1] g
hg : Surjective g
inr : range (f ∘ g) = range f
⊢ range f = ∅ ∨ ∃ (f_1 : (ℕ → ℕ) → α), Continuous[_, inst] f_1 ∧ range f_1 = range f

Tactic:
refine Or.inr ⟨f ∘ g, f_cont.comp g_cont, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
f : β → α
f_cont : Continuous[inst_1, inst] f
h : Nonempty β
g : (ℕ → ℕ) → β
g_cont : Continuous[_, inst_1] g
hg : Surjective g
inr inr₁ : range f = range f
⊢ range (f ∘ g) = range f

Tactic:
rw [hg.range_comp]

Premises used: Function.Surjective.range_comp
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
rw : AnalyticSet.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β))
⊢ AnalyticSet (f '' s)

Tactic:
rw [image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
⊢ PolishSpace.{u_3} (↑s : Type u_3)

Tactic:
haveI : PolishSpace s := hs.polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
this : PolishSpace.{u_3} (↑s : Type u_3)
⊢ AnalyticSet.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β))

Tactic:
analyticSet_range_of_polishSpace (f_cont.comp continuous_subtype_val)

Premises used: continuous_subtype_val, Continuous.comp, MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
inst_2 : PolishSpace β
s : Set β
hs : IsOpen[inst_1] s
f : β → α
f_cont : Continuous[inst_1, inst] f
this : PolishSpace.{u_3} (↑s : Type u_3)
⊢ AnalyticSet.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : β))

Tactic:
exact analyticSet_range_of_polishSpace (f_cont.comp continuous_subtype_val)

Premises used: continuous_subtype_val, Continuous.comp, MeasureTheory.analyticSet_range_of_polishSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
mp :
  AnalyticSet s →
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s
mpr :
  (∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s) →
    AnalyticSet s
⊢ AnalyticSet s ↔
    ∃ (β : Type) (h : TopologicalSpace β) (_ : PolishSpace β) (f : β → α), Continuous[_, inst] f ∧ range f = s

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : AnalyticSet s
⊢ s = ∅ ∨ ∃ (f : (ℕ → ℕ) → α), Continuous[_, inst] f ∧ range f = s

Tactic:
rw [AnalyticSet] at h

Premises used: MeasureTheory.AnalyticSet