awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inr : ∀ (this : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2)))
  (hle : ¬x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Tactic: wlog hle : x ≤ y generalizing x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
inr :
  ∀ (this : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2)))
    (hle : ¬x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have wlog : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Tactic: wlog hle : x ≤ y generalizing x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (hypothesis)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
this : ∀ (x y : Γ₀) (hle : x ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
hle : ¬x ≤ y
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have this₁ : Tendsto ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ Prod.swap) (𝓝 (x, y)) (𝓝 ((y, x).1 * (y, x).2))
Tactic: have := (this y x (le_of_not_ge hle)).comp (continuous_swap.tendsto (x, y))
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inl : ∀ (hle : 0 ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
Cleared hypotheses: x, hle
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
inl : ∀ (hle : 0 ≤ y), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inr : ∀ (hx : x ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Tactic: rcases eq_or_ne x 0 with (rfl | hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
have inl : ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
  Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
Cleared hypotheses: y, hle
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
inl :
  ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
    Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
have inl₁ : ∀ (hy : y ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
Tactic: rcases eq_or_ne y 0 with (rfl | hy)
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inl : ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
  Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
Tactic: rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
Cleared hypotheses: x, y, hle
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
inl :
  ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
    Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inl₁ : ∀ (hle : 0 ≤ y) (hy : y ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
Tactic: rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
Cleared hypotheses: x, hle
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
inl :
  ∀ (hle : LE.le.{u_2} (α := Γ₀) 0 0),
    Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
inl₁ : ∀ (hle : 0 ≤ y) (hy : y ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inr : ∀ (hx : x ≠ 0), Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Tactic: rcases eq_or_ne x 0 with (rfl | hx) <;> [rcases eq_or_ne y 0 with (rfl | hy); skip]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))
have inl : Tendsto (β := Γ₀) (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 0)
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
⊢ Tendsto (β := Γ₀) (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 0)
have inl : ∀ (γ : Γ₀) (hγ : γ ≠ 0), ∀ x ∈ SProd.sprod (β := Set Γ₀) (Iio (γ, 1).1) (Iio (γ, 1).2), x.1 * x.2 ∈ Iio γ
Tactic: refine ((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2
        fun γ hγ => ⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))
have inl : Tendsto.{u_2, u_2} (α := Γ₀) (β := Γ₀) ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) (𝓝 0) (𝓝 0)
Tactic: rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
⊢ Tendsto.{u_2, u_2} (α := Γ₀) (β := Γ₀) ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) (𝓝 0) (𝓝 0)
have inl : ∀ (γ : Γ₀) (hγ : γ ≠ 0),
  ∃ (ia : Γ₀), ia ≠ 0 ∧ ∀ x ∈ Iio ia, ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ
Tactic: refine (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
⊢ ∃ (ia : Γ₀), ia ≠ 0 ∧ ∀ x ∈ Iio ia, ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ
have inl : ∀ (x : Γ₀) (hx : x ∈ Iio (γ / y)), ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ
Tactic: refine ⟨γ / y, div_ne_zero hγ hy, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (hypothesis)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := ((zero_lt_iff.mpr hx).trans_le hle).ne'
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (x, y)) (𝓝 ((x, y).1 * (x, y).2))
have inr : Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (pure (x, y)) (𝓝 ((x, y).1 * (x, y).2))
Tactic: rw [nhds_prod_eq, nhds_of_ne_zero hx, nhds_of_ne_zero hy, prod_pure_pure]
-- Lean 4 proof step from Mathlib.Topology.Algebra.WithZeroTopology (goal)
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ ContinuousAt Inv.inv γ
have rw : Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)
Tactic: rw [ContinuousAt, nhds_of_ne_zero h]
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ closure[inst] s =ᶠ[residual α] s
have rw : ∀ᵇ (x : α), x ∈ closure[inst] s ↔ x ∈ s
Tactic: rw [Filter.eventuallyEq_set]
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ ∀ᵇ (x : α), x ∈ closure[inst] s ↔ x ∈ s
have h : ∀ (x : α) (hx : x ∈ coborder s), x ∈ closure[inst] s ↔ x ∈ s
Tactic: filter_upwards [coborder_mem_residual hs] with x hx
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure[inst] s ↔ x ∈ s
have h : x ∈ closure[inst] s ↔ x ∈ closure[inst] s ∩ coborder s
Tactic: nth_rewrite 2 [← closure_inter_coborder (s := s)]
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
h : MeasurableSet s
⊢ BaireMeasurableSet s
have inst : BorelSpace α
Tactic: borelize α
Cleared hypotheses: inst_1, inst_2, h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
inst_1 : TopologicalSpace α
s : Set α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
h : MeasurableSet s
inst : BorelSpace α
⊢ BaireMeasurableSet s
have h₁ : MeasurableSet s
Tactic: borelize α
Cleared hypotheses: inst_2, inst_3, h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsOpen[inst] s
⊢ BaireMeasurableSet s
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s_1 : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
ht : MeasurableSet s
ihs : ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
have compl : ∀ (U : Set α) (Uo : IsOpen[inst] U) (hsU : s =ᶠ[residual α] U), ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
Tactic: obtain ⟨U, Uo, hsU⟩ := ihs
Cleared hypotheses: ihs
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s_1 : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
s : Set α
ht : MeasurableSet s
U : Set α
Uo : IsOpen[inst] U
hsU : s =ᶠ[residual α] U
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
have right : sᶜ =ᶠ[residual α] (closure[inst] U)ᶜ
Tactic: use (closure U)ᶜ, isClosed_closure.isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
f : ℕ → Set α
h : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∃ (u : Set α), IsOpen[inst] u ∧ f i =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ ⋃ (i : ℕ), f i =ᶠ[residual α] u
have iUnion : ∀ (u : (i : ℕ) → Set α) (uo : ∀ (i : ℕ), IsOpen[inst] (u i)) (su : ∀ (i : ℕ), f i =ᶠ[residual α] u i),
  ∃ (u : Set α), IsOpen[inst] u ∧ ⋃ (i : ℕ), f i =ᶠ[residual α] u
Tactic: choose u uo su using ihf
Cleared hypotheses: ihf
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
h : MeasurableSet s
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), ∃ (u : Set α), IsOpen[inst] u ∧ U =ᶠ[residual α] u
Tactic: induction s, h using MeasurableSet.induction_on_open with
  | isOpen U hU => exact ⟨U, hU, .rfl⟩
  | compl s _ ihs =>
    obtain ⟨U, Uo, hsU⟩ := ihs
    use (closure U)ᶜ, isClosed_closure.isOpen_compl
    exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed
  | iUnion f _ _ ihf =>
    choose u uo su using ihf
    exact ⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
h : MeasurableSet s
isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), ∃ (u : Set α), IsOpen[inst] u ∧ U =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have compl : ∀ (s : Set α),
  MeasurableSet s →
    ∀ (ihs : ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u), ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
Tactic: induction s, h using MeasurableSet.induction_on_open with
  | isOpen U hU => exact ⟨U, hU, .rfl⟩
  | compl s _ ihs =>
    obtain ⟨U, Uo, hsU⟩ := ihs
    use (closure U)ᶜ, isClosed_closure.isOpen_compl
    exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed
  | iUnion f _ _ ihf =>
    choose u uo su using ihf
    exact ⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
h : MeasurableSet s
isOpen : ∀ (U : Set α) (hU : IsOpen[inst] U), ∃ (u : Set α), IsOpen[inst] u ∧ U =ᶠ[residual α] u
compl :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (ihs : ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u), ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have iUnion : ∀ (f : ℕ → Set α),
  Pairwise (Function.onFun Disjoint f) →
    (∀ (i : ℕ), MeasurableSet (f i)) →
      ∀ (ihf : ∀ (i : ℕ), ∃ (u : Set α), IsOpen[inst] u ∧ f i =ᶠ[residual α] u),
        ∃ (u : Set α), IsOpen[inst] u ∧ ⋃ (i : ℕ), f i =ᶠ[residual α] u
Tactic: induction s, h using MeasurableSet.induction_on_open with
  | isOpen U hU => exact ⟨U, hU, .rfl⟩
  | compl s _ ihs =>
    obtain ⟨U, Uo, hsU⟩ := ihs
    use (closure U)ᶜ, isClosed_closure.isOpen_compl
    exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed
  | iUnion f _ _ ihf =>
    choose u uo su using ihf
    exact ⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have this : let this := borel α;
BorelSpace α
Tactic: borelize α
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have rcases : ∀ (t : Set α) (ht : MeasurableSet t) (hst : s =ᶠ[residual α] t), ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
Tactic: rcases h with ⟨t, ht, hst⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
have rcases : ∀ (u : Set α) (hu : IsOpen[inst] u) (htu : t =ᶠ[residual α] u), ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
Tactic: rcases ht.residualEq_isOpen with ⟨u, hu, htu⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
⊢ Tendsto f (residual α) (residual β)
have apply : {t : Set β | IsOpen[inst_1] t ∧ Dense t} ⊆ (map f (residual α)).sets
Tactic: apply le_countableGenerate_iff_of_countableInterFilter.mpr
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s : Set β
h : BaireMeasurableSet s
⊢ BaireMeasurableSet (f ⁻¹' s)
have rcases : ∀ (u : Set β) (hu : MeasurableSet u) (hsu : s =ᶠ[residual β] u), BaireMeasurableSet (f ⁻¹' s)
Tactic: rcases h with ⟨u, hu, hsu⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ BaireMeasurableSet (f ⁻¹' s)
have refine : MeasurableSet (f ⁻¹' u)
Tactic: refine ⟨f ⁻¹' u, ?_, hsu.filter_mono <| tendsto_residual_of_isOpenMap hc ho⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
⊢ MeasurableSet (f ⁻¹' u)
have this : let this := borel α;
BorelSpace α
Tactic: borelize α β
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hc : Continuous[inst, inst_1] f
ho : IsOpenMap f
s u : Set β
hu : MeasurableSet u
hsu : s =ᶠ[residual β] u
this :
  let this := borel α;
  BorelSpace α
⊢ MeasurableSet (f ⁻¹' u)
have this₁ : let this := borel β;
BorelSpace β
Tactic: borelize α β
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
⊢ map (⇑h : (a : α) → β) (residual α) = residual β
have refine : ∀ s ∈ residual α, (⇑h : (a : α) → β) '' s ∈ residual β
Tactic: refine le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)
-- Lean 4 proof step from Mathlib.Topology.Baire.BaireMeasurable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, (⇑h : (a : α) → β) '' s ∈ residual β
have simp_rw : ∀ s ∈ residual α, (⇑h.symm : (a : β) → α) ⁻¹' s ∈ residual β
Tactic: simp_rw [← preimage_symm]
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
⊢ BaireSpace X
have refine : ∀ (f : ℕ → Set X) (ho : ∀ (n : ℕ), IsOpen (f n)) (hd : ∀ (n : ℕ), Dense (f n)), Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
Tactic: refine ⟨fun f ho hd => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
⊢ Dense.{u_1} (X := X) (⋂ (n : ℕ), f n)
have Bpos : ∀ (n : ℕ), 0 < B n
Tactic: have Bpos : ∀ n, 0 < B n := fun n ↦
    ENNReal.div_pos one_ne_zero <| by finiteness
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have this : x ∈ closure (f n)
Tactic: have : x ∈ closure (f n) := hd n x
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have rcases : ∀ (y : X) (ys : y ∈ f n) (xy : edist x y < δ / 2),
  ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
Tactic: rcases EMetric.mem_closure_iff.1 this (δ / 2) (ENNReal.half_pos δpos) with ⟨y, ys, xy⟩
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist x y < δ / 2
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have xy₁ : edist y x < δ / 2
Tactic: rw [edist_comm] at xy
Cleared hypotheses: xy
-- Lean 4 proof step from Mathlib.Topology.Baire.CompleteMetrizable (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : IsCompletelyPseudoMetrizableSpace X
x_1 : UpgradedIsCompletelyPseudoMetrizableSpace X := upgradeIsCompletelyPseudoMetrizable X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
B : ℕ → ℝ≥0∞ := fun (n : ℕ) ↦ 1 / HPow.hPow (α := ℝ≥0∞) 2 n
Bpos : ∀ (n : ℕ), 0 < B n
n : ℕ
x : X
δ : ℝ≥0∞
δpos : δ ≠ 0
this : x ∈ closure (f n)
y : X
ys : y ∈ f n
xy : edist y x < δ / 2
⊢ ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
have obtain : ∀ (r : ℝ≥0∞) (rpos : r > 0) (hr : closedEBall y r ⊆ f n),
  ∃ (y : X) (r : ℝ≥0∞), 0 < r ∧ r ≤ B (n + 1) ∧ closedEBall y r ⊆ closedEBall x δ ∩ f n
Tactic: obtain ⟨r, rpos, hr⟩ : ∃ r > 0, closedEBall y r ⊆ f n :=
      nhds_basis_closedEBall.mem_iff.1 (isOpen_iff_mem_nhds.1 (ho n) y ys)