awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)
have rw : MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
have this : PolishSpace.{u_3} (↑s : Type u_3)
Tactic: haveI : PolishSpace s := IsClosed.polishSpace hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
⊢ MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
have f_cont₁ : Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
Tactic: apply measurableSet_range_of_continuous_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
f_cont₁ : Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
⊢ MeasurableSet.{u_4} (α := β) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
have f_inj₁ : Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
Tactic: apply measurableSet_range_of_continuous_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
⊢ Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
have f_cont₁ : ∀ (f_cont : Continuous[instTopologicalSpaceSubtype, inst_2] (s.restrict (π := fun (a : γ) ↦ β) f)) (f_inj : InjOn f s)
  (this : PolishSpace.{u_3} (↑s : Type u_3)),
  Continuous[instTopologicalSpaceSubtype, inst_2] fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
Tactic: rwa [continuousOn_iff_continuous_restrict] at f_cont
Cleared hypotheses: f_cont, f_inj, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
inst : TopologicalSpace γ
inst_1 : PolishSpace γ
β : Type u_4
inst_2 : TopologicalSpace β
inst_3 : T2Space β
inst_4 : MeasurableSpace β
inst_5 : OpensMeasurableSpace β
s : Set γ
hs : IsClosed[inst] s
f : γ → β
f_cont : ContinuousOn f s
f_inj : InjOn f s
this : PolishSpace.{u_3} (↑s : Type u_3)
⊢ Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
have f_inj₁ : ∀ (f_inj : Injective (s.restrict (π := fun (a : γ) ↦ β) f)) (this : PolishSpace.{u_3} (↑s : Type u_3)),
  Injective.{u_3 + 1, u_4 + 1} (β := β) fun (x : (↑s : Type u_3)) ↦ f (↑x : γ)
Tactic: rwa [injOn_iff_injective] at f_inj
Cleared hypotheses: f_inj, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : OpensMeasurableSpace β
tγ : TopologicalSpace γ
inst_3 : PolishSpace γ
inst_4 : MeasurableSpace γ
inst_5 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
⊢ MeasurableSet (f '' s)
have obtain : ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (t'_polish : PolishSpace γ) (s_closed : IsClosed s),
  IsOpen s → MeasurableSet (f '' s)
Tactic: obtain ⟨t', t't, t'_polish, s_closed, _⟩ :
      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s :=
    hs.isClopenable
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
⊢ MeasurableSet (f '' s)
have rcases : ∀ (τ : TopologicalSpace α), SecondCountableTopology α → T4Space α → OpensMeasurableSpace α → MeasurableSet (f '' s)
Tactic: rcases exists_opensMeasurableSpace_of_countablySeparated α with ⟨τ, _, _, _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
⊢ MeasurableSet (f '' s)
have obtain : ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (f_cont : Continuous[_, τ] f) (t'_polish : PolishSpace γ),
  MeasurableSet (f '' s)
Tactic: obtain ⟨t', t't, f_cont, t'_polish⟩ :
      ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' :=
    f_meas.exists_continuous
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
γ : Type u_3
α : Type u_4
inst : MeasurableSpace α
s : Set γ
f : γ → α
inst_1 : MeasurableSpace.CountablySeparated α
inst_2 : MeasurableSpace γ
inst_3 : StandardBorelSpace γ
hs : MeasurableSet s
f_meas : Measurable f
f_inj : InjOn f s
this : UpgradedStandardBorel γ := upgradeStandardBorel γ
tγ : TopologicalSpace γ := inferInstance
τ : TopologicalSpace α
left : SecondCountableTopology α
left_1 : T4Space α
right : OpensMeasurableSpace α
t' : TopologicalSpace γ
t't : t' ≤ tγ
f_cont : Continuous[t', τ] f
t'_polish : PolishSpace γ
⊢ MeasurableSet (f '' s)
have hs' : MeasurableSet s
Tactic: have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
⊢ MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)
have A : MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
Tactic: have A : MeasurableSet (((↑) : s → γ) '' u) :=
        (MeasurableEmbedding.subtype_coe hs).measurableSet_image.2 hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
A : MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
⊢ MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)
have B : MeasurableSet (f '' Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
Tactic: have B : MeasurableSet (f '' ((↑) : s → γ) '' u) :=
        A.image_of_continuousOn_injOn (f_cont.mono (Subtype.coe_image_subset s u))
          (f_inj.mono (Subtype.coe_image_subset s u))
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
tβ : TopologicalSpace β
inst_1 : T2Space β
s : Set γ
f : γ → β
inst_2 : BorelSpace β
inst_3 : TopologicalSpace γ
inst_4 : PolishSpace γ
inst_5 : MeasurableSpace γ
inst_6 : BorelSpace γ
hs : MeasurableSet s
f_cont : ContinuousOn f s
f_inj : InjOn f s
u : Set (↑s : Type u_3)
hu : MeasurableSet u
A : MeasurableSet (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
B : MeasurableSet (f '' Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)
⊢ MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)
have rwa : ∀ (B : MeasurableSet (f ∘ Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' u)),
  MeasurableSet (s.restrict (π := fun (a : γ) ↦ β) f '' u)
Tactic: rwa [← image_comp] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
⊢ borel γ = borel γ
have refine : borel γ ≤ borel γ
Tactic: refine le_antisymm ?_ (borel_anti hle)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
⊢ MeasurableSet s
have e : MeasurableEmbedding.{u_3, u_3} (α := γ) id
Tactic: have e := @Continuous.measurableEmbedding
    _ _ (@borel _ t') t' _ _ (@BorelSpace.mk _ _ (borel γ) rfl)
    t _ (@borel _ t) (@BorelSpace.mk _ t (@borel _ t) rfl) (continuous_id_of_le hle) injective_id
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
t t' : TopologicalSpace γ
ht : PolishSpace γ
ht' : PolishSpace γ
hle : t ≤ t'
s : Set γ
hs : MeasurableSet s
e : MeasurableEmbedding.{u_3, u_3} (α := γ) id
⊢ MeasurableSet s
have h : s = id '' s
Tactic: convert! e.measurableSet_image.2 hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
⊢ IsClopenable s ↔ MeasurableSet s
have refine : ∀ (hs : IsClopenable s), MeasurableSet s
Tactic: refine ⟨fun hs => ?_, fun hs => hs.isClopenable⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : MeasurableSpace γ
inst_2 : BorelSpace γ
hs : IsClopenable s
⊢ MeasurableSet s
have borelize : ∀ [BorelSpace γ], MeasurableSet s
Tactic: borelize γ
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
hs : IsClopenable s
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
⊢ MeasurableSet s
have obtain : ∀ (t' : TopologicalSpace γ) (t't : t' ≤ tγ) (t'_polish : PolishSpace γ),
  IsClosed s → ∀ (s_open : IsOpen s), MeasurableSet s
Tactic: obtain ⟨t', t't, t'_polish, _, s_open⟩ :
    ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @PolishSpace γ t' ∧ IsClosed[t'] s ∧ IsOpen[t'] s := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
γ : Type u_3
s : Set γ
tγ : TopologicalSpace γ
inst : PolishSpace γ
inst_1 : BorelSpace γ
this : MeasurableSpace γ := borel γ
t' : TopologicalSpace γ
t't : t' ≤ tγ
t'_polish : PolishSpace γ
left : IsClosed[t'] s
s_open : IsOpen[t'] s
⊢ MeasurableSet s
have rw : MeasurableSet s
Tactic: rw [← borel_eq_borel_of_le t'_polish _ t't]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
⊢ MeasurableSet (g '' t)
have hu : u.Countable
Tactic: have hu : Set.Countable u := MonotoneOn.countable_setOf_two_preimages hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
⊢ t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
have h : ∀ (x : α), x ∈ t' ↔ Membership.mem (γ := Set α) (⋃ c ∈ u, t ∩ g ⁻¹' {c}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
⊢ MeasurableSet t'
have this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
Tactic: have : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c} := by ext; simp [t']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
⊢ MeasurableSet t'
have rw : MeasurableSet.{u_6} (α := α) (⋃ c ∈ u, t ∩ g ⁻¹' {c})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
⊢ MeasurableSet.{u_6} (α := α) (⋃ c ∈ u, t ∩ g ⁻¹' {c})
have apply : ∀ (c : β) (hc : c ∈ u), MeasurableSet (t ∩ g ⁻¹' {c})
Tactic: apply MeasurableSet.biUnion hu (fun c hc ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
this : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}
c : β
hc : c ∈ u
⊢ MeasurableSet (t ∩ g ⁻¹' {c})
have obtain : ∀ (v : Set α) (hv : v.OrdConnected) (tv : t ∩ g ⁻¹' {c} = t ∩ v), MeasurableSet (t ∩ g ⁻¹' {c})
Tactic: obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ t ∩ g ⁻¹' {c} = t ∩ v :=
      ordConnected_singleton.preimage_monotoneOn hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
⊢ MeasurableSet (g '' t)
have ht' : MeasurableSet t'
Tactic: have ht' : MeasurableSet t' := by
    have : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c} := by ext; simp [t']
    rw [this]
    apply MeasurableSet.biUnion hu (fun c hc ↦ ?_)
    obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ t ∩ g ⁻¹' {c} = t ∩ v :=
      ordConnected_singleton.preimage_monotoneOn hg
    exact tv ▸ ht.inter hv.measurableSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
⊢ MeasurableSet (g '' t)
have this : g '' t = g '' (t \ t') ∪ g '' t'
Tactic: have : g '' t = g '' (t \ t') ∪ g '' t' := by simp [← image_union, t']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' t)
have rw : MeasurableSet (g '' (t \ t') ∪ g '' t')
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')
have h₁ : MeasurableSet (g '' (t \ t'))
Tactic: apply MeasurableSet.union
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
h₁ : MeasurableSet (g '' (t \ t'))
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')
have h₂ : MeasurableSet (g '' t')
Tactic: apply MeasurableSet.union
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))
have h₁ : InjOn g (t \ t')
Tactic: apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono diff_subset)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : g x = g y
⊢ x = y
have h₁ : ∀ (hxy : x ≠ y), g x ≠ g y
Tactic: contrapose! hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
⊢ g x ≠ g y
have h₁ : ∀ (h : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y) (H : y ≤ x),
  g x ≠ g y
Tactic: wlog! H : x < y generalizing x y with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
inst_3 : LinearOrder α
inst_4 : OrderTopology α
inst_5 : PolishSpace α
inst_6 : TopologicalSpace β
inst_7 : MeasurableSpace β
inst_8 : BorelSpace β
inst_9 : LinearOrder β
inst_10 : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
u : Set β := {c : β | ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
hu : u.Countable
t' : Set α := t ∩ g ⁻¹' u
ht' : MeasurableSet t'
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
h₁ :
  ∀ (h : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y) (H : y ≤ x),
    g x ≠ g y
⊢ g x ≠ g y
have wlog! : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y
Tactic: wlog! H : x < y generalizing x y with h
Cleared hypotheses: x, hx, y, hy, hxy