awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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'
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
⊢ g x ≠ g y
have this₁ : y < x
Tactic: have : y < x := lt_of_le_of_ne H hxy.symm
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
⊢ MeasurableSet (g '' t)
have ht' : t'.Countable
Tactic: have ht' : Set.Countable t' := hg.countable_not_continuousWithinAt
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t') ∪ g '' t'
have rw : g '' t = g '' (t \ t' ∪ t')
Tactic: rw [← image_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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ g '' t = g '' (t \ t' ∪ t')
have h : t = t \ t' ∪ t'
Tactic: congr!
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ t = t \ t' ∪ t'
have h : ∀ (x : α), x ∈ t ↔ x ∈ t \ t' ∪ t'
Tactic: ext
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
x : α
⊢ x ∈ t ↔ x ∈ t \ t' ∪ t'
have h : x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
Tactic: simp only [sdiff_sep_self, not_not, mem_union, mem_setOf_eq, 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
x : α
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
Tactic: tauto
-- 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 β
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 ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₆ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
h₆ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₇ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
h₆ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₇ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₈ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₉ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₁₀ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₁₁ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₁₂ : x ∈ t → ContinuousWithinAt g t x → x ∉ t → False
Tactic: tauto
-- 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 β
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
h₁ : x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x → x ∈ t
h₂ h₃ : x ∈ t → x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
h₄ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → x ∈ t
h₅ : x ∈ t → ¬(x ∈ t ∧ ContinuousWithinAt g t x) → ¬ContinuousWithinAt g t x
h₆ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₇ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₈ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₉ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₁₀ : x ∈ t → ContinuousWithinAt g t x → x ∈ t
h₁₁ : x ∈ t → ¬ContinuousWithinAt g t x → x ∈ t
h₁₂ : x ∈ t → ContinuousWithinAt g t x → x ∉ t → False
⊢ x ∈ t ↔ x ∈ t ∧ ContinuousWithinAt g t x ∨ x ∈ t ∧ ¬ContinuousWithinAt g t x
have h₁₃ : x ∈ t → ContinuousWithinAt g t x → ¬ContinuousWithinAt g t x → False
Tactic: tauto
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
⊢ MeasurableSet (g '' t)
have this : g '' t = g '' (t \ t') ∪ g '' t'
Tactic: have : g '' t = g '' (t \ t') ∪ g '' t' := by
    rw [← image_union]
    congr!
    ext
    simp only [sdiff_sep_self, not_not, mem_union, mem_setOf_eq, t']
    tauto
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t') ∪ g '' t')
have apply : MeasurableSet (g '' (t \ t'))
Tactic: apply MeasurableSet.union _ (ht'.image g).measurableSet
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
⊢ MeasurableSet (g '' (t \ t'))
have apply : ContinuousOn g (t \ t')
Tactic: apply MeasurableSet.image_of_monotoneOn_of_continuousOn (ht.diff ht'.measurableSet)
    (hg.mono diff_subset)
-- 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 β
inst_11 : SecondCountableTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
t' : Set α := {x : α | x ∈ t ∧ ¬ContinuousWithinAt g t x}
ht' : t'.Countable
this : g '' t = g '' (t \ t') ∪ g '' t'
x : α
hx : x ∈ t \ t'
⊢ ContinuousWithinAt g (t \ t') x
have hx₁ : x ∈ t ∧ ContinuousWithinAt g t x
Tactic: simp only [sdiff_sep_self, not_not, mem_setOf_eq, t'] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
inst_4 : TopologicalSpace γ
inst_5 : SecondCountableTopology γ
inst_6 : PseudoMetrizableSpace γ
inst_7 : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet.{u_5} (α := β) {x : β | Tendsto (fun (n : ι) ↦ f n x) l (𝓝 (g x))}
have simp_rw : MeasurableSet.{u_5} (α := β) {x : β | Tendsto (β := ℝ) (fun (b : ι) ↦ dist (f b x) (g x)) l (𝓝 0)}
Tactic: simp_rw [tendsto_iff_dist_tendsto_zero (f := fun n ↦ f n _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
have inl : ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥],
  MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 c)}
Tactic: rcases l.eq_or_neBot with rfl | hl
Cleared hypotheses: l, inst_6
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_2} (α := ι) ⊥],
    MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) ⊥ (𝓝 c)}
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
have inr : ∀ (hl : l.NeBot), MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
Tactic: rcases l.eq_or_neBot with rfl | hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
have inr : ∀ (u : ℕ → Set ι) (hu : l.HasAntitoneBasis u),
  MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
Tactic: rcases l.exists_antitone_basis with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet.{u_5} (α := β) {x : β | ∃ (c : γ), Tendsto (fun (n : ι) ↦ f n x) l (𝓝 c)}
have inr : MeasurableSet.{u_5} (α := β) {x : β | Cauchy.{u_3} (α := γ) (map (fun (n : ι) ↦ f n x) l)}
Tactic: simp_rw [← cauchy_map_iff_exists_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (hypothesis)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      NeBot.{u_3} (α := γ) (map (fun (n : ι) ↦ f n x) l) ∧
        SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (n : ι) ↦ f n x) l) (map (fun (n : ι) ↦ f n x) l) ≤
          uniformity γ}
have this₁ : ∀ (x : β),
  (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
        (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
    fun (n : ℕ) ↦
    SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
Tactic: have : ∀ x, (map (f · x) l ×ˢ map (f · x) l).HasAntitoneBasis fun n =>
      ((f · x) '' u n) ×ˢ ((f · x) '' u n) := fun x => (hu.map _).prod (hu.map _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Polish.Basic (goal)
Goal:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst : MeasurableSpace β
inst_1 : TopologicalSpace γ
inst_2 : IsCompletelyPseudoMetrizableSpace γ
inst_3 : SecondCountableTopology γ
inst_4 : MeasurableSpace γ
hγ : OpensMeasurableSpace γ
inst_5 : Countable ι
l : Filter ι
inst_6 : l.IsCountablyGenerated
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
hl : l.NeBot
this_1 : UpgradedIsCompletelyPseudoMetrizableSpace γ := upgradeIsCompletelyPseudoMetrizable γ
u : ℕ → Set ι
hu : l.HasAntitoneBasis u
this :
  ∀ (x : β),
    (SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (x_1 : ι) ↦ f x_1 x) l)
          (map (fun (x_1 : ι) ↦ f x_1 x) l)).HasAntitoneBasis
      fun (n : ℕ) ↦
      SProd.sprod (α := Set γ) (β := Set γ) ((fun (x_1 : ι) ↦ f x_1 x) '' u n) ((fun (x_1 : ι) ↦ f x_1 x) '' u n)
⊢ MeasurableSet.{u_5} (α := β)
    {x : β |
      NeBot.{u_3} (α := γ) (map (fun (n : ι) ↦ f n x) l) ∧
        SProd.sprod (α := Filter γ) (β := Filter γ) (map (fun (n : ι) ↦ f n x) l) (map (fun (n : ι) ↦ f n x) l) ≤
          uniformity γ}
have inr : MeasurableSet.{u_5} (α := β)
  (⋂ (i : ℕ),
    ⋂ (_ : True),
      {x : β |
        ∃ (i_2 : ℕ),
          True ∧
            SProd.sprod (α := Set γ) (β := Set γ) ((fun (n : ι) ↦ f n x) '' u i_2) ((fun (n : ι) ↦ f n x) '' u i_2) ⊆
              {p : γ × γ | dist p.1 p.2 < 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1}})
Tactic: simp_rw [and_iff_right (hl.map _),
    Filter.HasBasis.le_basis_iff (this _).toHasBasis Metric.uniformity_basis_dist_inv_nat_succ,
    Set.setOf_forall]