awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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

Tactic:
exact MeasurableSpace.measurableSet_generateFrom s_open

Premises used: MeasurableSpace.measurableSet_generateFrom
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ PolishSpace γ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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}
⊢ u.Countable

Tactic:
have hu : Set.Countable u := MonotoneOn.countable_setOf_two_preimages hg
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h : ∀ (x : α), x ∈ t' ↔ Membership.mem (γ := Set α) (⋃ c ∈ u, t ∩ g ⁻¹' {c}) x
⊢ t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c}

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
x : α
⊢ x ∈ t' ↔ Membership.mem (γ := Set α) (⋃ c ∈ u, t ∩ g ⁻¹' {c}) x

Tactic:
simp [t']
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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}

Tactic:
have : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c} := by ext; simp [t']
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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}
rw : MeasurableSet.{u_6} (α := α) (⋃ c ∈ u, t ∩ g ⁻¹' {c})
⊢ MeasurableSet t'

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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}
apply : ∀ (c : β) (hc : c ∈ u), MeasurableSet (t ∩ g ⁻¹' {c})
⊢ MeasurableSet.{u_6} (α := α) (⋃ c ∈ u, t ∩ g ⁻¹' {c})

Tactic:
apply MeasurableSet.biUnion hu (fun c hc ↦ ?_)

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
⊢ ∃ (v : Set α), v.OrdConnected ∧ t ∩ g ⁻¹' {c} = t ∩ v

Tactic:
ordConnected_singleton.preimage_monotoneOn hg

Premises used: Set.ordConnected_singleton, Set.OrdConnected.preimage_monotoneOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
obtain : ∀ (v : Set α) (hv : v.OrdConnected) (tv : t ∩ g ⁻¹' {c} = t ∩ v), MeasurableSet (t ∩ g ⁻¹' {c})
⊢ MeasurableSet (t ∩ g ⁻¹' {c})

Tactic:
obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ t ∩ g ⁻¹' {c} = t ∩ v :=
      ordConnected_singleton.preimage_monotoneOn hg

Premises used: Set.ordConnected_singleton, Set.OrdConnected.preimage_monotoneOn
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
v : Set α
hv : v.OrdConnected
tv : t ∩ g ⁻¹' {c} = t ∩ v
⊢ MeasurableSet (t ∩ g ⁻¹' {c})

Tactic:
tv ▸ ht.inter hv.measurableSet

Premises used: Set.OrdConnected.measurableSet, Eq.rec, Eq.symm, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
v : Set α
hv : v.OrdConnected
tv : t ∩ g ⁻¹' {c} = t ∩ v
⊢ MeasurableSet (t ∩ g ⁻¹' {c})

Tactic:
exact tv ▸ ht.inter hv.measurableSet
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'

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
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
simp [← image_union, t']

Premises used: Set.image_union
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
have : g '' t = g '' (t \ t') ∪ g '' t' := by simp [← image_union, t']
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'
rw : MeasurableSet (g '' (t \ t') ∪ g '' t')
⊢ MeasurableSet (g '' t)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'))
h₂ : MeasurableSet (g '' t')
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')

Tactic:
apply MeasurableSet.union

Premises used: MeasurableSet.union
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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₁ : InjOn g (t \ t')
⊢ MeasurableSet (g '' (t \ t'))

Tactic:
apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono diff_subset)

Premises used: MeasurableSet.diff, Set.diff_subset, MeasurableSet.image_of_continuousOn_injOn, ContinuousOn.mono
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
h₁ : ∀ (hxy : x ≠ y), g x ≠ g y
⊢ x = y

Tactic:
contrapose! hxy
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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
wlog! : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y
⊢ g x ≠ g y

Tactic:
wlog! H : x < y generalizing x y with h
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y
H : y ≤ x
⊢ y < x

Tactic:
have : y < x := lt_of_le_of_ne H hxy.symm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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_1 : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
h : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y
H : y ≤ x
this : y < x
⊢ g x ≠ g y

Tactic:
(h hy hx hxy.symm this).symm

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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_1 : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
y : α
hy : y ∈ t \ t'
hxy : x ≠ y
h : ∀ ⦃x : α⦄ (hx : x ∈ t \ t') ⦃y : α⦄ (hy : y ∈ t \ t') (hxy : x ≠ y) (H : x < y), g x ≠ g y
H : y ≤ x
this : y < x
⊢ g x ≠ g y

Tactic:
exact (h hy hx hxy.symm this).symm

Premises used: Ne.symm
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : x < y
h : g x = g y
⊢ False

Tactic:
hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 : x < y
h : g x = g y
⊢ False

Tactic:
exact hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩

Premises used: And.right, And.left, And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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'
⊢ g '' t' ⊆ u

Tactic:
simp [t']
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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')

Tactic:
exact hu.mono (by simp [t']) |>.measurableSet

Premises used: Set.Countable.measurableSet, Set.Countable.mono
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
⊢ t'.Countable

Tactic:
have ht' : Set.Countable t' := hg.countable_not_continuousWithinAt
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
rw : g '' t = g '' (t \ t' ∪ t')
⊢ g '' t = g '' (t \ t') ∪ g '' t'

Tactic:
rw [← image_union]

Premises used: Set.image_union
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
h : t = t \ t' ∪ t'
⊢ g '' t = g '' (t \ t' ∪ t')

Tactic:
congr!
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
h : ∀ (x : α), x ∈ t ↔ x ∈ t \ t' ∪ t'
⊢ t = t \ t' ∪ t'

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Constructions.Polish.Basic
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
x : α
h : x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
⊢ x ∈ t ↔ x ∈ t \ t' ∪ t'

Tactic:
simp only [sdiff_sep_self, not_not, mem_union, mem_setOf_eq, t']

Premises used: Set.mem_union, Classical.not_not, Set.mem_setOf_eq, Set.sdiff_sep_self