awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : IsMeagre s
⊢ IsMeagre (f '' s)
have rw : ∀ (h : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S),
  ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
Tactic: rw [isMeagre_iff_countable_union_isNowhereDense] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
h : ∃ (S : Set (Set X)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
have obtain : ∀ (T : Set (Set X)) (isNowhereDense : ∀ t ∈ T, IsNowhereDense t) (countable : T.Countable) (cover : s ⊆ ⋃₀ T),
  ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
Tactic: obtain ⟨T, isNowhereDense, countable, cover⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
have refine : ∀ t ∈ image f '' T, IsNowhereDense t
Tactic: refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
refine : ∀ t ∈ image f '' T, IsNowhereDense t
⊢ ∃ (S : Set (Set Y)), (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ f '' s ⊆ ⋃₀ S
have refine₁ : f '' s ⊆ ⋃₀ (image f '' T)
Tactic: refine ⟨(Set.image f) '' T, ?isNowhereDense, countable.image _, ?cover⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
⊢ u ∈ image f '' T → IsNowhereDense u
have this : ∀ (t : Set X) (tT : t ∈ T) (tu : f '' t = u), IsNowhereDense u
Tactic: ⟨t, tT, tu⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
u : Set Y
t : Set X
tT : t ∈ T
tu : f '' t = u
⊢ IsNowhereDense u
have rw : IsNowhereDense (f '' t)
Tactic: rw [← tu]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)
have rw : f '' s ⊆ f '' ⋃₀ T
Tactic: rw [← Set.image_sUnion]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ f '' ⋃₀ T
have grw : f '' ⋃₀ T ⊆ f '' ⋃₀ T
Tactic: grw [cover]
-- Lean 4 proof step from Mathlib.Topology.GDelta.Basic (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)
have case : f '' s ⊆ f '' ⋃₀ T
Tactic: case cover =>
    rw [← Set.image_sUnion]
    grw [cover]
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this : UniformSpace X := pseudoMetrizableSpaceUniformity X
⊢ IsGδ s
have this₁ : (uniformity X).IsCountablyGenerated
Tactic: have := pseudoMetrizableSpaceUniformity_countably_generated X
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
⊢ IsGδ s
have rcases : ∀ (U : ℕ → SetRel X X) (hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i))
  (hU : (uniformity X).HasBasis (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦ id (U i)), IsGδ s
Tactic: rcases (@uniformity_hasBasis_open X _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
U : ℕ → SetRel X X
hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i)
hU : (uniformity X).HasBasis (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦ id (U i)
⊢ IsGδ s
have rw : IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))
Tactic: rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : PseudoMetrizableSpace X
s : Set X
hs : IsClosed s
this_1 : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (uniformity X).IsCountablyGenerated
U : ℕ → SetRel X X
hUo : ∀ (i : ℕ), U i ∈ uniformity X ∧ IsOpen (U i)
hU : (uniformity X).HasBasis (fun (x : ℕ) ↦ True) fun (i : ℕ) ↦ id (U i)
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))
have refine : ∀ (n : ℕ),
  Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) n → IsOpen.{u_1} (X := X) (⋃ x ∈ s, UniformSpace.ball x (id (U n)))
Tactic: refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
⊢ IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}
have this₁ : (uniformity Y).IsCountablyGenerated
Tactic: have := pseudoMetrizableSpaceUniformity_countably_generated Y
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
⊢ IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}
have obtain : ∀ (U : ℕ → SetRel Y Y),
  (∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm) →
    ∀ (hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)), IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}
Tactic: obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)
⊢ IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}
have simp : IsGδ.{u_1} (X := X) {x : X | Filter.Tendsto (fun (x : X × X) ↦ (f x.1, f x.2)) (nhds x ×ˢ nhds x) (uniformity Y)}
Tactic: simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)
⊢ IsGδ.{u_1} (X := X) {x : X | Filter.Tendsto (fun (x : X × X) ↦ (f x.1, f x.2)) (nhds x ×ˢ nhds x) (uniformity Y)}
have simp : IsGδ.{u_1} (X := X)
  (⋂ (i : ℕ), {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U i)})
Tactic: simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis,
    forall_prop_of_true, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)
⊢ IsGδ.{u_1} (X := X)
    (⋂ (i : ℕ), {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U i)})
have refine : ∀ (k : ℕ) (x : X),
  Membership.mem (γ := Set X) {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)}
      x →
    {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} ∈ nhds x
Tactic: refine .iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)
k : ℕ
x : X
s : Set X
hsU : ∀ x ∈ s ×ˢ s, (f x.1, f x.2) ∈ id (U k)
hsx : x ∈ s
hso : IsOpen s
⊢ {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} ∈ nhds x
have h : ∀ (a : X),
  Membership.mem (γ := Set X)
    {x : X |
      x ∈ s →
        Membership.mem (γ := Set X)
          {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} x}
    a
Tactic: filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.GDelta.MetrizableSpace (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
inst_2 : PseudoMetrizableSpace Y
f : X → Y
this_1 : UniformSpace Y := pseudoMetrizableSpaceUniformity Y
this : (uniformity Y).IsCountablyGenerated
U : ℕ → SetRel Y Y
left : ∀ (i : ℕ), U i ∈ uniformity Y ∧ IsOpen (U i) ∧ (U i).IsSymm
hU : (uniformity Y).HasAntitoneBasis fun (i : ℕ) ↦ id (U i)
k : ℕ
x : X
s : Set X
hsU : ∀ x ∈ s ×ˢ s, (f x.1, f x.2) ∈ id (U k)
hsx : x ∈ s
hso : IsOpen s
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        x ∈ s →
          Membership.mem (γ := Set X)
            {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} x}
      a
⊢ {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} ∈ nhds x
have h₁ : ∀ a ∈ s, ∃ (ia : Set X), (a ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)
Tactic: filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X_1
f_1 g_1 : X_1 → Y
A : Set X_1
x_1 : X_1
X : Type u_4
α : Type u_5
inst_1 : TopologicalSpace X
x : X
φ : (𝓝 x).Germ α
f g : X → α
h : ((𝓝 x).germSetoid α : (X → α) → (X → α) → Prop) f g
⊢ f x = g x
have rw : g x = g x
Tactic: rw [Eventually.self_of_nhds h]
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
f_1 g : X → Y
A_1 : Set X
x_1 : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
hf : ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑f' : (𝓝 y).Germ Y)
have apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, f x = f' x) → P x (↑f' : (𝓝 x).Germ Y)
Tactic: apply (hf.and <| Eventually.eventually_nhds hff').mono
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ᶠ (x : X) in 𝓝ˢ A, P x (↑f : (𝓝 x).Germ Y)
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x (↑g : (𝓝 x).Germ Y)
have rw : ∀ (hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)) (h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y),
  ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑g : (𝓝 y).Germ Y)
Tactic: rw [eventually_nhdsSet_iff_forall] at *
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
x : X
hx : x ∈ A
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑g : (𝓝 y).Germ Y)
have apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x (↑g : (𝓝 x).Germ Y)
Tactic: apply ((hf x hx).and (h x hx).eventually_nhds).mono
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
x : X
hx : x ∈ A
y : X
hy : P y (↑f : (𝓝 y).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y (↑g : (𝓝 y).Germ Y)
have h₁ : Eq (α := (𝓝 y).Germ Y) (↑g : (𝓝 y).Germ Y) (↑f : (𝓝 y).Germ Y)
Tactic: convert! hy.1 using 1
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑g : (𝓝 y).Germ Y)
have apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x (↑g : (𝓝 x).Germ Y)
Tactic: apply ((hf hx).and <| (eventually_nhdsSet_iff_forall.mp h x hx).eventually_nhds).mono
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x (↑f : (𝓝 x).Germ Y)
have rw : (∀ (x : X), RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)) ↔ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)
Tactic: rw [eventually_nhdsSet_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
s : Set Y
⊢ IsOpen[inst] (f ⁻¹' s)
have rw : ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
Tactic: rw [isOpen_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
⊢ f ⁻¹' s ∈ 𝓝 a
have obtain : ∀ (b : Y) (hb : f =ᶠ[𝓝 a] fun (x : X) ↦ b), f ⁻¹' s ∈ 𝓝 a
Tactic: obtain ⟨b, hb⟩ := h a
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun (x : X) ↦ b
⊢ f ⁻¹' s ∈ 𝓝 a
have apply : {x : X | (fun (x : X) ↦ f x = (fun (x : X) ↦ b) x) x} ⊆ f ⁻¹' s
Tactic: apply mem_of_superset hb
-- Lean 4 proof step from Mathlib.Topology.Germ (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun (x : X) ↦ b
x : X
hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x = (fun (x : X) ↦ b) x) x} x
⊢ x ∈ f ⁻¹' s
have this : f x = f a
Tactic: have : f x = f a := (mem_of_mem_nhds hb) ▸ hx
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun (x : X) ↦ b
x : X
hx : Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x = (fun (x : X) ↦ b) x) x} x
this : f x = f a
⊢ x ∈ f ⁻¹' s
have rw : f a ∈ s
Tactic: rw [mem_preimage, this]
-- Lean 4 proof step from Mathlib.Topology.Germ (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : (↑s : Type u_1) → X := fun (x : (↑s : Type u_1)) ↦ (↑x : X)
⊢ f x = f x'
have change : (f ∘ i) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in) = (f ∘ i) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x' x'_in)
Tactic: change (f ∘ i) (⟨x, x_in⟩ : s) = (f ∘ i) (⟨x', x'_in⟩ : s)
-- Lean 4 proof step from Mathlib.Topology.Germ (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
x : X
s : Set X
h : ∀ x ∈ s, Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
hs : IsPreconnected s
x' : X
x_in : x ∈ s
x'_in : x' ∈ s
i : (↑s : Type u_1) → X := fun (x : (↑s : Type u_1)) ↦ (↑x : X)
⊢ (f ∘ i) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in) = (f ∘ i) (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x' x'_in)
have this : PreconnectedSpace.{u_1} (↑s : Type u_1)
Tactic: have : PreconnectedSpace s := Subtype.preconnectedSpace hs
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
⊢ IsOpen U ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued) (Multicoequalizer.π D.diagram i)) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
have simp_rw : IsOpen U ↔
  ∀ (i : D.J),
    IsOpen (X := (↑(D.U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram))) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
        U)
Tactic: simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
⊢ IsOpen U ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
have rw : IsOpen (X :=
    (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
      Type u))
    ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
        (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
          (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
      U) ↔
  ∀ (i : D.J),
    IsOpen (X := (↑(D.U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram))) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
        U)
Tactic: rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
⊢ IsOpen (X :=
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
      ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
          (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
            (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
        U) ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
have rw : (∀ (j : Discrete (MultispanShape.prod D.J).R),
    IsOpen (X := (↑(Functor.obj (Discrete.functor D.diagram.right) j) : Type u))
      (Set.preimage (β := (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Discrete.functor D.diagram.right) j) (Y := colimit (Discrete.functor D.diagram.right))
              (colimit.ι (Discrete.functor D.diagram.right) j)) :
          (a : (↑((Discrete.functor D.diagram.right).obj j) : Type u)) →
            (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
        (Set.preimage (β :=
          (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
            Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                ∐ D.diagram.right) (Y :=
                coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap)
                (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) :
            (a : (↑(∐ D.diagram.right) : Type u)) →
              (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
          ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
              (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
                (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
            U)))) ↔
  ∀ (i : D.J),
    IsOpen (X := (↑(D.U i) : Type u))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram))) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
        U)
Tactic: rw [coequalizer_isOpen_iff, colimit_isOpen_iff.{u}]