awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
rw : IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))
⊢ IsGδ s

Tactic:
rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]

Premises used: IsClosed.closure_eq, Filter.HasBasis.biInter_biUnion_ball
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)))

Tactic:
.biInter (to_countable _) fun n _ => IsOpen.isGδ ?_

Premises used: Set.Mem, Set.to_countable, IsOpen.isGδ, IsGδ.biInter
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
refine :
  ∀ (n : ℕ),
    Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) n → IsOpen.{u_1} (X := X) (⋃ x ∈ s, UniformSpace.ball x (id (U n)))
⊢ IsGδ.{u_1} (X := X) (⋂ (i : ℕ), ⋂ (_ : True), ⋃ x ∈ s, UniformSpace.ball x (id (U i)))

Tactic:
refine .biInter (to_countable _) fun n _ => IsOpen.isGδ ?_
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
n : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) n
⊢ IsOpen.{u_1} (X := X) (⋃ x ∈ s, UniformSpace.ball x (id (U n)))

Tactic:
isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2

Premises used: UniformSpace.isOpen_ball, And.right, isOpen_biUnion
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
n : ℕ
h : Membership.mem (γ := Set ℕ) (fun (i : ℕ) ↦ True) n
⊢ IsOpen.{u_1} (X := X) (⋃ x ∈ s, UniformSpace.ball x (id (U n)))

Tactic:
exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2

Premises used: UniformSpace.isOpen_ball, And.right, isOpen_biUnion
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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
⊢ (uniformity Y).IsCountablyGenerated

Tactic:
have := pseudoMetrizableSpaceUniformity_countably_generated Y
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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
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}
⊢ IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}

Tactic:
obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric Y _).exists_antitone_subbasis

Premises used: Filter.HasBasis.exists_antitone_subbasis, uniformity_hasBasis_open_symmetric
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
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)}
⊢ IsGδ.{u_1} (X := X) {x : X | ContinuousAt f x}

Tactic:
simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]

Premises used: nhds_prod_eq, Uniform.continuousAt_iff_prod
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
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)})
⊢ 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 [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis,
    forall_prop_of_true, setOf_forall]

Premises used: Filter.HasAntitoneBasis.toHasBasis, Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, forall_prop_of_true, nhds_basis_opens, Set.setOf_forall
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)})

Tactic:
.iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_

Premises used: Iff.mpr, IsGδ.iInter, isOpen_iff_mem_nhds, IsOpen.isGδ
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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)
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
⊢ 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:
refine .iInter fun k ↦ IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x ↦ ?_
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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
a : X
hy : a ∈ s
⊢ ∃ (ia : Set X), (a ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)

Tactic:
⟨s, ⟨hy, hso⟩, hsU⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.GDelta.MetrizableSpace
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
h₁ h₂ : ∀ (a : X) (hy : a ∈ s), ∃ (ia : Set X), (a ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)
⊢ {x : X | ∃ (ia : Set X), (x ∈ ia ∧ IsOpen ia) ∧ ∀ x ∈ ia ×ˢ ia, (f x.1, f x.2) ∈ id (U k)} ∈ nhds x

Tactic:
filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.Germ
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
dsimp : f x = g x
⊢ Eq.{u_5 + 1} (α := α) ((fun (f : X → α) ↦ f x) f) ((fun (f : X → α) ↦ f x) g)

Tactic:
dsimp only
-- Module: Mathlib.Topology.Germ
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
rw rw₁ : g x = g x
⊢ f x = g x

Tactic:
rw [Eventually.self_of_nhds h]

Premises used: Filter.Eventually.self_of_nhds
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
x : X
⊢ value (x := x) (↑f : (𝓝 x).Germ Y) = f x

Tactic:
rfl

Premises used: Filter.Germ.value, Quotient.liftOn', rfl
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
c : Y
x : X
⊢ value.{u_1, u_2} (X := X) (x := x) (↑c : (𝓝 x).Germ Y) = c

Tactic:
rfl

Premises used: Filter.Germ.value, Quotient.liftOn', rfl
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
α : Type u_4
β : Type u_5
inst_1 : SMul α β
φ : (𝓝 x).Germ α
ψ : (𝓝 x).Germ β
⊢ (φ • ψ).value = φ.value • ψ.value

Tactic:
Germ.inductionOn φ fun _ ↦ Germ.inductionOn ψ fun _ ↦ rfl

Premises used: Filter.Germ.inductionOn
-- Module: Mathlib.Topology.Germ
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)
apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, f x = f' x) → P x (↑f' : (𝓝 x).Germ Y)
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑f' : (𝓝 y).Germ Y)

Tactic:
apply (hf.and <| Eventually.eventually_nhds hff').mono

Premises used: Filter.Eventually.eventually_nhds, Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Topology.Germ
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
hy : P y (↑f : (𝓝 y).Germ Y)
hy' : ∀ᶠ (x : X) in 𝓝 y, f x = f' x
rwa rwa₁ rwa₂ rwa₃ : P y (↑f : (𝓝 y).Germ Y)
⊢ P y (↑f' : (𝓝 y).Germ Y)

Tactic:
rwa [Germ.coe_eq.mpr (EventuallyEq.symm hy')]

Premises used: Iff.mpr, Filter.Germ.coe_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Topology.Germ
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
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)
⊢ ∀ᶠ (x : X) in 𝓝ˢ A, P x (↑g : (𝓝 x).Germ Y)

Tactic:
rw [eventually_nhdsSet_iff_forall] at *

Premises used: eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Germ
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
apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x (↑g : (𝓝 x).Germ Y)
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑g : (𝓝 y).Germ Y)

Tactic:
apply ((hf x hx).and (h x hx).eventually_nhds).mono

Premises used: Filter.Eventually.eventually_nhds, Filter.Eventually.and, Filter.Eventually.mono
-- Module: Mathlib.Topology.Germ
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 (↑f : (𝓝 y).Germ Y)

Tactic:
hy.1

Premises used: And.left
-- Module: Mathlib.Topology.Germ
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
h₁ : Eq (α := (𝓝 y).Germ Y) (↑g : (𝓝 y).Germ Y) (↑f : (𝓝 y).Germ Y)
⊢ P y (↑g : (𝓝 y).Germ Y)

Tactic:
convert! hy.1 using 1

Premises used: And.left
-- Module: Mathlib.Topology.Germ
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
⊢ Eq (α := (𝓝 y).Germ Y) (↑g : (𝓝 y).Germ Y) (↑f : (𝓝 y).Germ Y)

Tactic:
Germ.coe_eq.mpr hy.2

Premises used: Iff.mpr, Filter.Germ.coe_eq, And.right
-- Module: Mathlib.Topology.Germ
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
⊢ Eq (α := (𝓝 y).Germ Y) (↑g : (𝓝 y).Germ Y) (↑f : (𝓝 y).Germ Y)

Tactic:
exact Germ.coe_eq.mpr hy.2

Premises used: Iff.mpr, Filter.Germ.coe_eq, And.right
-- Module: Mathlib.Topology.Germ
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
apply : ∀ (x : X), (P x (↑f : (𝓝 x).Germ Y) ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x (↑g : (𝓝 x).Germ Y)
⊢ ∀ᶠ (y : X) in 𝓝 x, P y (↑g : (𝓝 y).Germ Y)

Tactic:
apply ((hf hx).and <| (eventually_nhdsSet_iff_forall.mp h x hx).eventually_nhds).mono

Premises used: Filter.Eventually.eventually_nhds, Filter.Eventually.and, Filter.Eventually.mono, Iff.mp, eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Germ
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
hy : P y (↑f : (𝓝 y).Germ Y)
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
rwa rwa₁ rwa₂ rwa₃ : P y (↑f : (𝓝 y).Germ Y)
⊢ P y (↑g : (𝓝 y).Germ Y)

Tactic:
rwa [Germ.coe_eq.mpr h'y]

Premises used: Iff.mpr, Filter.Germ.coe_eq
-- Module: Mathlib.Topology.Germ
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
rw : (∀ (x : X), RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)) ↔ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)
⊢ (∀ (x : X), RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x (↑f : (𝓝 x).Germ Y)

Tactic:
rw [eventually_nhdsSet_iff_forall]

Premises used: eventually_nhdsSet_iff_forall
-- Module: Mathlib.Topology.Germ
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 ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y (↑f : (𝓝 y).Germ Y)

Tactic:
rfl
-- Module: Mathlib.Topology.Germ
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
h : ∀ (x : X), P x (↑f : (𝓝 x).Germ Y)
⊢ ∀ (x : X), RestrictGermPredicate P A x (↑f : (𝓝 x).Germ Y)

Tactic:
forall_restrictGermPredicate_iff.mpr (Eventually.of_forall h)

Premises used: Iff.mpr, Filter.Eventually.of_forall, forall_restrictGermPredicate_iff
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
x : X
inst_1 : TopologicalSpace Y
y : Y
f : X × Y → Z
⊢ Eq (α := (𝓝 (x, y).1).Germ Z) (sliceLeft (↑f : (𝓝 (x, y)).Germ Z)) (↑fun (x' : X) ↦ f (x', y) : (𝓝 (x, y).1).Germ Z)

Tactic:
rfl

Premises used: Filter.Germ.compTendsto, Filter.Germ.ofFun, Filter.Germ.compTendsto', Filter.Germ.map', Quotient.mk', Filter.Germ.liftOn, Quotient.map', Filter.Germ.map, Filter.Germ.sliceLeft, rfl
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : TopologicalSpace X
x : X
inst_1 : TopologicalSpace Y
y : Y
f : X × Y → Z
⊢ Eq (α := (𝓝 (x, y).2).Germ Z) (sliceRight (↑f : (𝓝 (x, y)).Germ Z)) (↑fun (y' : Y) ↦ f (x, y') : (𝓝 (x, y).2).Germ Z)

Tactic:
rfl

Premises used: Filter.Germ.compTendsto, Filter.Germ.ofFun, Filter.Germ.compTendsto', Filter.Germ.map', Filter.Germ.sliceRight, Quotient.mk', Filter.Germ.liftOn, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
s : Set X
f : X → Y
x : (↑s : Type u_1)
hf : IsConstant (l := 𝓝 (↑x : X)) (↑f : (𝓝 (↑x : X)).Germ Y)
⊢ IsConstant (α := (↑s : Type u_1)) (l := 𝓝 x) (↑(f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ s)) : (𝓝 x).Germ Y)

Tactic:
isConstant_comp_tendsto hf continuousAt_subtype_val

Premises used: continuousAt_subtype_val, Filter.Germ.isConstant_comp_tendsto
-- Module: Mathlib.Topology.Germ
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
rw : ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
⊢ IsOpen[inst] (f ⁻¹' s)

Tactic:
rw [isOpen_iff_mem_nhds]

Premises used: isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Germ
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
obtain : ∀ (b : Y) (hb : f =ᶠ[𝓝 a] fun (x : X) ↦ b), f ⁻¹' s ∈ 𝓝 a
⊢ f ⁻¹' s ∈ 𝓝 a

Tactic:
obtain ⟨b, hb⟩ := h a
-- Module: Mathlib.Topology.Germ
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
apply : {x : X | (fun (x : X) ↦ f x = (fun (x : X) ↦ b) x) x} ⊆ f ⁻¹' s
⊢ f ⁻¹' s ∈ 𝓝 a

Tactic:
apply mem_of_superset hb

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.Germ
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
⊢ f x = f a

Tactic:
have : f x = f a := (mem_of_mem_nhds hb) ▸ hx
-- Module: Mathlib.Topology.Germ
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
rw : f a ∈ s
⊢ x ∈ f ⁻¹' s

Tactic:
rw [mem_preimage, this]

Premises used: Set.mem_preimage
-- Module: Mathlib.Topology.Germ
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
⊢ f a ∈ s

Tactic:
ha

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.Germ
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
⊢ f a ∈ s

Tactic:
exact ha
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
x x' : X
⊢ Membership.mem (γ := Set X) univ x

Tactic:
trivial
-- Module: Mathlib.Topology.Germ
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), Germ.IsConstant (l := 𝓝 x) (↑f : (𝓝 x).Germ Y)
x x' : X
⊢ Membership.mem (γ := Set X) univ x'

Tactic:
trivial
-- Module: Mathlib.Topology.Germ
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)
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)
⊢ f x = f x'

Tactic:
change (f ∘ i) (⟨x, x_in⟩ : s) = (f ∘ i) (⟨x', x'_in⟩ : s)

Premises used: Function.comp, Subtype.mk
-- Module: Mathlib.Topology.Germ
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)
⊢ PreconnectedSpace.{u_1} (↑s : Type u_1)

Tactic:
have : PreconnectedSpace s := Subtype.preconnectedSpace hs
-- Module: Mathlib.Topology.Germ
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)
this : PreconnectedSpace.{u_1} (↑s : Type u_1)
⊢ (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:
eq_of_germ_isConstant (fun y ↦ Germ.isConstant_comp_subtype (h y y.2)) _ _

Premises used: Filter.Germ.isConstant_comp_subtype, eq_of_germ_isConstant
-- Module: Mathlib.Topology.Germ
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)
this : PreconnectedSpace.{u_1} (↑s : Type u_1)
⊢ (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:
exact eq_of_germ_isConstant (fun y ↦ Germ.isConstant_comp_subtype (h y y.2)) _ _

Premises used: Filter.Germ.isConstant_comp_subtype, eq_of_germ_isConstant