awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
have he : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u
Tactic: apply hk.induction_on (p := fun t ↦ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
he : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
have hmono : ∀ ⦃s_1 t : Set β⦄,
  s_1 ⊆ t → (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u
Tactic: apply hk.induction_on (p := fun t ↦ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
he : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u
hmono :
  ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
have hunion : ∀ ⦃s_1 t : Set β⦄,
  (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u
Tactic: apply hk.induction_on (p := fun t ↦ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
he : ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ (x : β), Membership.mem (γ := Set β) ∅ x → (f p x, f q x) ∈ u
hmono :
  ∀ ⦃s_1 t : Set β⦄,
    s_1 ⊆ t →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u
hunion :
  ∀ ⦃s_1 t : Set β⦄,
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1, (f p x, f q x) ∈ u) →
      (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ s_1 ∪ t, (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
have hnhds : ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Tactic: apply hk.induction_on (p := fun t ↦ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t' t : Set β
ht't : t' ⊆ t
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u
have hmono : ∀ (v : Set α) (v_mem : v ∈ 𝓝[s] q) (hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u),
  ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u
Tactic: ⟨v, v_mem, hv⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u) →
    (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
have hunion : ∀ (v : Set α) (v_mem : v ∈ 𝓝[s] q) (hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u),
  (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
Tactic: ⟨v, v_mem, hv⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
⊢ (∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t', (f p x, f q x) ∈ u) → ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
have hunion : ∀ (v' : Set α) (v'_mem : v' ∈ 𝓝[s] q) (hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u),
  ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
Tactic: ⟨v', v'_mem, hv'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
⊢ ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t ∪ t', (f p x, f q x) ∈ u
have hunion : ∀ (p : α) (hp : p ∈ v ∩ v') (x : β) (hx : x ∈ t ∪ t'), (f p x, f q x) ∈ u
Tactic: refine ⟨v ∩ v', inter_mem v_mem v'_mem, fun p hp x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
hx : x ∈ t ∪ t'
⊢ (f p x, f q x) ∈ u
have hunion : ∀ (h'x : x ∈ t), (f p x, f q x) ∈ u
Tactic: rcases hx with h'x | h'x
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
t t' : Set β
v : Set α
v_mem : v ∈ 𝓝[s] q
hv : ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
v' : Set α
v'_mem : v' ∈ 𝓝[s] q
hv' : ∀ p ∈ v', ∀ x ∈ t', (f p x, f q x) ∈ u
p : α
hp : p ∈ v ∩ v'
x : β
hx : x ∈ t ∪ t'
hunion : ∀ (h'x : x ∈ t), (f p x, f q x) ∈ u
⊢ (f p x, f q x) ∈ u
have hunion₁ : ∀ (h'x : x ∈ t'), (f p x, f q x) ∈ u
Tactic: rcases hx with h'x | h'x
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
⊢ ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
have hnhds : ∀ (u' : Set (E × E)) (u'_mem : u' ∈ 𝓤 E) (u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u')
  (hu' : SetRel.comp u' u' ⊆ u), ∀ x ∈ k, ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Tactic: rcases comp_symm_of_uniformity hu with ⟨u', u'_mem, u'_symm, hu'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
have hnhds : ∀ (v : Set α) (hv : v ∈ 𝓝[s] q) (w : Set β) (hw : w ∈ 𝓝[k] x)
  (hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}),
  ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
Tactic: obtain ⟨v, hv, w, hw, hvw⟩ :
      ∃ v ∈ 𝓝[s] q, ∃ w ∈ 𝓝[k] x, v ×ˢ w ⊆ f.uncurry ⁻¹' {z | (f q x, z) ∈ u'} :=
        mem_nhdsWithin_prod_iff.1 (hf (q, x) ⟨hq, hx⟩ (mem_nhds_left (f q x) u'_mem))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
⊢ ∃ t ∈ 𝓝[k] x, ∃ v ∈ 𝓝[s] q, ∀ p ∈ v, ∀ x ∈ t, (f p x, f q x) ∈ u
have hnhds : ∀ (p : α) (hp : p ∈ v) (y : β) (hy : y ∈ w), (f p y, f q y) ∈ u
Tactic: refine ⟨w, hw, v, hv, fun p hp y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
⊢ (f p y, f q y) ∈ u
have A : (f q x, f p y) ∈ u'
Tactic: have A : (f q x, f p y) ∈ u' := hvw (⟨hp, hy⟩ : (p, y) ∈ v ×ˢ w)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_4
β : Type u_5
E : Type u_6
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z : E | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
⊢ (f p y, f q y) ∈ u
have B : (f q x, f q y) ∈ u'
Tactic: have B : (f q x, f q y) ∈ u' := hvw (⟨mem_of_mem_nhdsWithin hq hv, hy⟩ : (q, y) ∈ v ×ˢ w)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h : Equicontinuous F
⊢ UniformEquicontinuous F
have h₁ : Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
  ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
Tactic: rw [equicontinuous_iff_continuous] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Type u_4
F : ι → β → α
inst_2 : CompactSpace β
h :
  Continuous[inst_1.toTopologicalSpace, UniformFun.topologicalSpace ι α]
    ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
⊢ UniformEquicontinuous F
have rw : UniformContinuous (β := UniformFun ι α)
  ((⇑UniformFun.ofFun : (a : ι → α) → UniformFun ι α) ∘ Function.swap (φ := fun (a : ι) (a_1 : β) ↦ α) F)
Tactic: rw [uniformEquicontinuous_iff_uniformContinuous]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x : α
h : x ∈ s
x_1 : Set (β × β)
h_1 : x_1 ∈ 𝓤 β
⊢ (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    Membership.mem (γ := Filter (β × β)) (map (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x)) x_1
have simp_rw : (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
  (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ⁻¹' x_1 ∈ p ×ˢ 𝓝[s] x
Tactic: simp_rw [mem_map, mem_prod_iff_right, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
x : α
h : x ∈ s
x_1 : Set (β × β)
h_1 : x_1 ∈ 𝓤 β
simp_rw :
  (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ⁻¹' x_1 ∈ p ×ˢ 𝓝[s] x
⊢ (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
    Membership.mem (γ := Filter (β × β)) (map (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x)) x_1
have simp_rw₁ : (∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ x_1) ↔
  ∃ t ∈ 𝓝[s] x,
    ∀ᶠ (x : ι) in p, ∀ y ∈ t, Membership.mem (γ := Set (ι × α)) ((fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ⁻¹' x_1) (x, y)
Tactic: simp_rw [mem_map, mem_prod_iff_right, mem_preimage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
hs : IsOpen[inst] s
x : α
hx : x ∈ s
⊢ Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔
    Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
have rw : Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β) ↔
  Tendsto (fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
Tactic: rw [hs.nhdsWithin_eq hx]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔
    TendstoLocallyUniformly (fun (i : ι) (x : (↑s : Type u_1)) ↦ F i (↑x : α))
      (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p
have simp : (∀ (x : { a : α // a ∈ s }),
    Tendsto ((fun (y : ι × α) ↦ (f y.2, F y.1 y.2)) ∘ Prod.map id (Subtype.val (p := fun (x : α) ↦ x ∈ s))) (p ×ˢ 𝓝 x)
      (𝓤 β)) ↔
  ∀ (x : (↑s : Type u_1)),
    Tendsto
      (fun (y : Prod.{u_4, u_1} ι (↑s : Type u_1)) ↦
        ((f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) y.2, F y.1 (↑y.2 : α)))
      (p ×ˢ 𝓝 x) (𝓤 β)
Tactic: simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
h : TendstoLocallyUniformlyOn F f p s
h' : s' ⊆ s
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s'
⊢ ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
have rcases : ∀ (t : Set α) (ht : t ∈ 𝓝[s] x) (H : ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u),
  ∃ t ∈ 𝓝[s'] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Tactic: rcases h u hu x (h' hx) with ⟨t, ht, H⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen[inst] s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ S)
have rw : TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst] s
hs₂ : IsOpen[inst] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ TendstoLocallyUniformlyOn F f p (s ∪ s')
have rw : TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})
Tactic: rw [← sUnion_pair]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst] s
hs₂ : IsOpen[inst] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})
have refine_1 : ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → IsOpen[inst] s_1
Tactic: refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
p : Filter ι
hs₁ : IsOpen[inst] s
hs₂ : IsOpen[inst] s'
h₁ : TendstoLocallyUniformlyOn F f p s
h₂ : TendstoLocallyUniformlyOn F f p s'
refine_1 : ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → IsOpen[inst] s_1
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ {s, s'})
have refine_2 : ∀ (s_1 : Set α), Membership.mem (γ := Set (Set α)) {s, s'} s_1 → TendstoLocallyUniformlyOn F f p s_1
Tactic: refine tendstoLocallyUniformlyOn_sUnion _ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
⊢ TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
have refine : ∀ (h : TendstoLocallyUniformly F f p) (V : Set (β × β)) (hV : V ∈ 𝓤 β), ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Tactic: refine ⟨fun h V hV => ?_, TendstoUniformly.tendstoLocallyUniformly⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
have choose : ∀ (U : (x : α) → Set α) (hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V),
  ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Tactic: choose U hU using h V hV
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
have obtain : ∀ (t : Finset (↑univ : Type u_1)) (ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))),
  ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
Tactic: obtain ⟨t, ht⟩ := isCompact_univ.elim_nhds_subcover' (fun k _ => U k) fun k _ => (hU k).1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V
t : Finset (↑univ : Type u_1)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
have hU₁ : ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U (↑(↑x : (↑univ : Type u_1)) : α), (f y, F n y) ∈ V
Tactic: replace hU := fun x : t => (hU x).2
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
t : Finset (↑univ : Type u_1)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ (x : ↥t), ∀ᶠ (n : ι) in p, ∀ y ∈ U (↑(↑x : (↑univ : Type u_1)) : α), (f y, F n y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
have hU₁ : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
Tactic: rw [← eventually_all] at hU
Cleared hypotheses: hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
t : Finset (↑univ : Type u_1)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
have refine : ∀ (i : ι) (hi : ∀ (i_1 : ↥t), ∀ y ∈ U (↑(↑i_1 : (↑univ : Type u_1)) : α), (f y, F i y) ∈ V) (x : α), (f x, F i x) ∈ V
Tactic: refine hU.mono fun i hi x => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
t : Finset (↑univ : Type u_1)
ht : Subset.{u_1} (α := Set α) univ (⋃ x ∈ t, U (↑x : α))
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U (↑(↑i_1 : (↑univ : Type u_1)) : α), (f y, F i y) ∈ V
x : α
⊢ (f x, F i x) ∈ V
have ht₁ : Membership.mem (γ := Set α) (⋃ x ∈ t, U (↑x : α)) x
Tactic: specialize ht (mem_univ x)
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.LocallyUniformConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : TopologicalSpace α
inst_1 : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst_2 : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : (x : α) → Set α
t : Finset (↑univ : Type u_1)
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U (↑(↑i : (↑univ : Type u_1)) : α), (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U (↑(↑i_1 : (↑univ : Type u_1)) : α), (f y, F i y) ∈ V
x : α
ht : Membership.mem (γ := Set α) (⋃ x ∈ t, U (↑x : α)) x
⊢ (f x, F i x) ∈ V
have ht₁ : ∃ (x_1 : α),
  (∃ (x : Membership.mem (γ := Set α) univ x_1),
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) univ x) x_1 sorry ∈ t) ∧
    x ∈ U x_1
Tactic: simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht
Cleared hypotheses: ht