awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
inl : Tendsto (β := Γ₀) (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 0)
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 (HMul.hMul (α := Γ₀) (0, 0).1 (0, 0).2))

Tactic:
rw [zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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)

Tactic:
((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2
        fun γ hγ => ⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Prod.mk, WithZeroTopology.hasBasis_nhds_zero, Filter.HasBasis.prod_nhds, And.intro, Exists.intro, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
inl : ∀ (γ : Γ₀) (hγ : γ ≠ 0), ∀ x ∈ SProd.sprod (β := Set Γ₀) (Iio (γ, 1).1) (Iio (γ, 1).2), x.1 * x.2 ∈ Iio γ
⊢ Tendsto (β := Γ₀) (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, 0)) (𝓝 0)

Tactic:
refine ((hasBasis_nhds_zero.prod_nhds hasBasis_nhds_zero).tendsto_iff hasBasis_nhds_zero).2
        fun γ hγ => ⟨(γ, 1), ⟨hγ, one_ne_zero⟩, ?_⟩

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Prod.mk, WithZeroTopology.hasBasis_nhds_zero, Filter.HasBasis.prod_nhds, And.intro, Exists.intro, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
γ : Γ₀
hγ : γ ≠ 0
x y : Γ₀
hx : x < γ
hy : y < 1
⊢ (x, y).1 * (x, y).2 ∈ Iio γ

Tactic:
(mul_lt_mul'' hx hy zero_le' zero_le').trans_eq (mul_one γ)

Premises used: Set.Mem, setOf, LT.lt.trans_eq, mul_lt_mul'', zero_le', mul_one, Set.Iio
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
hle : LE.le.{u_2} (α := Γ₀) 0 0
γ : Γ₀
hγ : γ ≠ 0
x y : Γ₀
hx : x < γ
hy : y < 1
⊢ (x, y).1 * (x, y).2 ∈ Iio γ

Tactic:
exact (mul_lt_mul'' hx hy zero_le' zero_le').trans_eq (mul_one γ)

Premises used: LT.lt.trans_eq, mul_lt_mul'', zero_le', mul_one
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
inl : Tendsto.{u_2, u_2} (α := Γ₀) (β := Γ₀) ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) (𝓝 0) (𝓝 0)
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (0, y)) (𝓝 ((0, y).1 * (0, y).2))

Tactic:
rw [zero_mul, nhds_prod_eq, nhds_of_ne_zero hy, prod_pure, tendsto_map'_iff]

Premises used: MulZeroClass.zero_mul, Filter.tendsto_map'_iff, WithZeroTopology.nhds_of_ne_zero, Filter.prod_pure, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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)

Tactic:
(hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, WithZeroTopology.hasBasis_nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
inl :
  ∀ (γ : Γ₀) (hγ : γ ≠ 0),
    ∃ (ia : Γ₀), ia ≠ 0 ∧ ∀ x ∈ Iio ia, ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ
⊢ Tendsto.{u_2, u_2} (α := Γ₀) (β := Γ₀) ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) (𝓝 0) (𝓝 0)

Tactic:
refine (hasBasis_nhds_zero.tendsto_iff hasBasis_nhds_zero).2 fun γ hγ => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, WithZeroTopology.hasBasis_nhds_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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 γ

Tactic:
⟨γ / y, div_ne_zero hγ hy, fun x hx => ?_⟩

Premises used: HDiv.hDiv, div_ne_zero, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
inl : ∀ (x : Γ₀) (hx : x ∈ Iio (γ / y)), ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ
⊢ ∃ (ia : Γ₀), ia ≠ 0 ∧ ∀ x ∈ Iio ia, ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ

Tactic:
refine ⟨γ / y, div_ne_zero hγ hy, fun x hx => ?_⟩
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ x * y < γ / y * y

Tactic:
mul_lt_mul_of_pos_right hx (zero_lt_iff.2 hy)

Premises used: Iff.mpr, mul_lt_mul_of_pos_right, zero_lt_iff
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ γ / y * y = γ

Tactic:
div_mul_cancel₀ _ hy

Premises used: div_mul_cancel₀
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
y : Γ₀
hle : 0 ≤ y
hy : y ≠ 0
γ : Γ₀
hγ : γ ≠ 0
x : Γ₀
hx : x ∈ Iio (γ / y)
⊢ ((fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) ∘ fun (a : Γ₀) ↦ (a, y)) x ∈ Iio γ

Tactic:
calc x * y < γ / y * y := mul_lt_mul_of_pos_right hx (zero_lt_iff.2 hy)
      _ = γ := div_mul_cancel₀ _ hy

Premises used: Iff.mpr, div_mul_cancel₀, mul_lt_mul_of_pos_right, zero_lt_iff
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := ((zero_lt_iff.mpr hx).trans_le hle).ne'
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
x y : Γ₀
hle : x ≤ y
hx : x ≠ 0
hy : y ≠ 0
inr : Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (pure (x, y)) (𝓝 ((x, y).1 * (x, y).2))
⊢ Tendsto (fun (p : Γ₀ × Γ₀) ↦ p.1 * p.2) (𝓝 (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]

Premises used: Filter.prod_pure_pure, WithZeroTopology.nhds_of_ne_zero, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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) (pure (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
pure_le_nhds (x * y)

Premises used: HMul.hMul, Set.Mem, pure_le_nhds, setOf, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
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) (pure (x, y)) (𝓝 ((x, y).1 * (x, y).2))

Tactic:
exact pure_le_nhds (x * y)

Premises used: HMul.hMul, pure_le_nhds
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
rw : Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)
⊢ ContinuousAt Inv.inv γ

Tactic:
rw [ContinuousAt, nhds_of_ne_zero h]

Premises used: ContinuousAt, WithZeroTopology.nhds_of_ne_zero
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)

Tactic:
pure_le_nhds γ⁻¹

Premises used: Set.Mem, pure_le_nhds, setOf, Inv.inv, Set.preimage, Filter.Tendsto
-- Module: Mathlib.Topology.Algebra.WithZeroTopology
Goal:
α : Type u_1
Γ₀ : Type u_2
inst : LinearOrderedCommGroupWithZero Γ₀
γ_1 γ₁ γ₂ : Γ₀
l : Filter α
f : α → Γ₀
γ : Γ₀
h : γ ≠ 0
⊢ Tendsto Inv.inv (pure γ) (𝓝 γ⁻¹)

Tactic:
exact pure_le_nhds γ⁻¹

Premises used: pure_le_nhds, Inv.inv
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
m : α
⊢ Tendsto (fun (x : α) ↦ m * x) (pure 1) (𝓝 m)

Tactic:
simpa using tendsto_pure_nhds (m * ·) (1 : α)

Premises used: HMul.hMul, tendsto_pure_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
m : α
⊢ Tendsto (fun (x : α) ↦ x * m) (pure 1) (𝓝 m)

Tactic:
simpa using tendsto_pure_nhds (· * m) (1 : α)

Premises used: HMul.hMul, tendsto_pure_nhds, OfNat.ofNat
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : SeparatelyContinuousMul α
m : α
⊢ Tendsto (fun (x : α) ↦ m * x) (𝓝 1) (𝓝 m)

Tactic:
simpa using tendsto_id (x := 𝓝 1) |>.const_mul m

Premises used: Filter.tendsto_id, Filter.Tendsto.const_mul
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : SeparatelyContinuousMul α
m : α
⊢ Tendsto (fun (x : α) ↦ x * m) (𝓝 1) (𝓝 m)

Tactic:
simpa using tendsto_id (x := 𝓝 1) |>.mul_const m

Premises used: Filter.tendsto_id, Filter.Tendsto.mul_const
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : SeparatelyContinuousMul α
l : Filter α
hl : l.IsApproximateUnit
⊢ l ≤ 𝓝 1

Tactic:
simpa using hl.tendsto_mul_left 1

Premises used: Filter.IsApproximateUnit.tendsto_mul_left, OfNat.ofNat
-- Module: Mathlib.Topology.ApproximateUnit
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MulOneClass α
inst_2 : SeparatelyContinuousMul α
l : Filter α
inst_3 : l.NeBot
⊢ l.IsApproximateUnit ↔ l ≤ 𝓝 1

Tactic:
simpa [iff_neBot_and_le_nhds_one] using fun _ ↦ ‹_›

Premises used: Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
⊢ coborder s ∈ residual α

Tactic:
residual_of_dense_open hs.isOpen_coborder dense_coborder

Premises used: dense_coborder, residual_of_dense_open, IsLocallyClosed.isOpen_coborder
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
rw : ∀ᵇ (x : α), x ∈ closure[inst] s ↔ x ∈ s
⊢ closure[inst] s =ᶠ[residual α] s

Tactic:
rw [Filter.eventuallyEq_set]

Premises used: Filter.eventuallyEq_set
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
h : ∀ (x : α) (hx : x ∈ coborder s), x ∈ closure[inst] s ↔ x ∈ s
⊢ ∀ᵇ (x : α), x ∈ closure[inst] s ↔ x ∈ s

Tactic:
filter_upwards [coborder_mem_residual hs] with x hx

Premises used: coborder_mem_residual
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
h : x ∈ closure[inst] s ↔ x ∈ closure[inst] s ∩ coborder s
⊢ x ∈ closure[inst] s ↔ x ∈ s

Tactic:
nth_rewrite 2 [← closure_inter_coborder (s := s)]

Premises used: closure_inter_coborder
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure[inst] s ↔ x ∈ closure[inst] s ∩ coborder s

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : s ∈ residual α
⊢ BaireMeasurableSet s

Tactic:
eventuallyMeasurableSet_of_mem_filter (α := α) h

Premises used: BaireMeasurableSet, EventuallyMeasurableSet, eventuallyMeasurableSet_of_mem_filter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
h : MeasurableSet s
⊢ BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst_1 : TopologicalSpace α
s : Set α
inst_2 : MeasurableSpace α
inst_3 : BorelSpace α
h : MeasurableSet s
inst : BorelSpace α
⊢ MeasurableSet s

Tactic:
borelize α
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : BorelSpace α
h : MeasurableSet s
this : MeasurableSpace α := borel α
⊢ BaireMeasurableSet s

Tactic:
h.eventuallyMeasurableSet

Premises used: BaireMeasurableSet, MeasurableSet.eventuallyMeasurableSet, EventuallyMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : BorelSpace α
h : MeasurableSet s
this : MeasurableSpace α := borel α
⊢ BaireMeasurableSet s

Tactic:
exact h.eventuallyMeasurableSet

Premises used: MeasurableSet.eventuallyMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsOpen[inst] s
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsOpen[inst] s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ BaireMeasurableSet s

Tactic:
h.measurableSet.baireMeasurableSet

Premises used: IsOpen.measurableSet, MeasurableSet.baireMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsOpen[inst] s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
⊢ BaireMeasurableSet s

Tactic:
exact h.measurableSet.baireMeasurableSet

Premises used: IsOpen.measurableSet, MeasurableSet.baireMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
⊢ BaireMeasurableSet sᶜ

Tactic:
MeasurableSet.compl h

Premises used: BaireMeasurableSet, MeasurableSet.compl
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet sᶜ
⊢ BaireMeasurableSet s

Tactic:
MeasurableSet.of_compl h

Premises used: MeasurableSet.of_compl, BaireMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : IsMeagre s
⊢ BaireMeasurableSet s

Tactic:
(of_mem_residual h).of_compl

Premises used: BaireMeasurableSet.of_mem_residual, BaireMeasurableSet.of_compl
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_3
inst_1 : Countable ι
s : ι → Set α
h : ∀ (i : ι), BaireMeasurableSet (s i)
⊢ BaireMeasurableSet.{u_1} (α := α) (⋃ (i : ι), s i)

Tactic:
MeasurableSet.iUnion h

Premises used: BaireMeasurableSet, MeasurableSet.iUnion
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
s : ι → Set α
t : Set ι
ht : t.Countable
h : ∀ i ∈ t, BaireMeasurableSet (s i)
⊢ BaireMeasurableSet.{u_1} (α := α) (⋃ i ∈ t, s i)

Tactic:
MeasurableSet.biUnion ht h

Premises used: BaireMeasurableSet, MeasurableSet.biUnion
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, BaireMeasurableSet t
⊢ BaireMeasurableSet (⋃₀ s)

Tactic:
MeasurableSet.sUnion hs h

Premises used: BaireMeasurableSet, MeasurableSet.sUnion
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Sort u_3
inst_1 : Countable ι
s : ι → Set α
h : ∀ (i : ι), BaireMeasurableSet (s i)
⊢ BaireMeasurableSet.{u_1} (α := α) (⋂ (i : ι), s i)

Tactic:
MeasurableSet.iInter h

Premises used: BaireMeasurableSet, MeasurableSet.iInter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
ι : Type u_3
s : ι → Set α
t : Set ι
ht : t.Countable
h : ∀ i ∈ t, BaireMeasurableSet (s i)
⊢ BaireMeasurableSet.{u_1} (α := α) (⋂ i ∈ t, s i)

Tactic:
MeasurableSet.biInter ht h

Premises used: BaireMeasurableSet, MeasurableSet.biInter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, BaireMeasurableSet t
⊢ BaireMeasurableSet (⋂₀ s)

Tactic:
MeasurableSet.sInter hs h

Premises used: BaireMeasurableSet, MeasurableSet.sInter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hs : BaireMeasurableSet s
ht : BaireMeasurableSet t
⊢ BaireMeasurableSet (s ∪ t)

Tactic:
MeasurableSet.union hs ht

Premises used: BaireMeasurableSet, MeasurableSet.union
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hs : BaireMeasurableSet s
ht : BaireMeasurableSet t
⊢ BaireMeasurableSet (s ∩ t)

Tactic:
MeasurableSet.inter hs ht

Premises used: BaireMeasurableSet, MeasurableSet.inter
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hs : BaireMeasurableSet s
ht : BaireMeasurableSet t
⊢ BaireMeasurableSet (s \ t)

Tactic:
MeasurableSet.diff hs ht

Premises used: MeasurableSet.diff, BaireMeasurableSet
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s t : Set α
hs : BaireMeasurableSet s
h : s =ᶠ[residual α] t
⊢ BaireMeasurableSet t

Tactic:
EventuallyMeasurableSet.congr (α := α) hs h.symm

Premises used: BaireMeasurableSet, EventuallyMeasurableSet, EventuallyMeasurableSet.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
U : Set α
hU : IsOpen[inst] U
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ U =ᶠ[residual α] u

Tactic:
⟨U, hU, .rfl⟩

Premises used: And.intro, Exists.intro, Filter.EventuallyEq.rfl
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
inst_1 : MeasurableSpace α
inst_2 : BorelSpace α
U : Set α
hU : IsOpen[inst] U
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ U =ᶠ[residual α] u

Tactic:
exact ⟨U, hU, .rfl⟩
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
compl :
  ∀ (U : Set α) (Uo : IsOpen[inst] U) (hsU : s =ᶠ[residual α] U), ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u

Tactic:
obtain ⟨U, Uo, hsU⟩ := ihs
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
right : sᶜ =ᶠ[residual α] (closure[inst] U)ᶜ
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ sᶜ =ᶠ[residual α] u

Tactic:
use (closure U)ᶜ, isClosed_closure.isOpen_compl

Premises used: IsClosed.isOpen_compl, closure
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
⊢ sᶜ =ᶠ[residual α] (closure[inst] U)ᶜ

Tactic:
.compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed

Premises used: Filter.EventuallyEq.trans, IsOpen.isLocallyClosed, closure_residualEq, Filter.EventuallyEq.compl, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
⊢ sᶜ =ᶠ[residual α] (closure[inst] U)ᶜ

Tactic:
exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed

Premises used: Filter.EventuallyEq.trans, IsOpen.isLocallyClosed, closure_residualEq
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
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
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ ⋃ (i : ℕ), f i =ᶠ[residual α] u

Tactic:
choose u uo su using ihf
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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)
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:
⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩

Premises used: Filter.EventuallyEq.countable_iUnion, isOpen_iUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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)
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:
exact ⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩
-- Module: Mathlib.Topology.Baire.BaireMeasurable
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
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
⊢ ∃ (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⟩

Premises used: IsClosed.isOpen_compl, Compl.compl
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
⊢ let this := borel α;
  BorelSpace α

Tactic:
borelize α
-- Module: Mathlib.Topology.Baire.BaireMeasurable
Goal:
α : Type u_1
inst : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
this : MeasurableSpace α := borel α
this_1 : BorelSpace α
rcases :
  ∀ (t : Set α) (ht : MeasurableSet t) (hst : s =ᶠ[residual α] t), ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ s =ᶠ[residual α] u

Tactic:
rcases h with ⟨t, ht, hst⟩