mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_2
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x : q.Rep), ∃ y, dist x (Φ y) ≤ ε

Tactic:
show ∀ x : q.Rep, ∃ z : s p, dist x (Φ z) ≤ ε

Goal state after:
case refine_2
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ univ ⊆ ⋃ x ∈ s p, ball x ε
N : GHSpace → ℕ := fun p ↦ Nat.card ↑(s p)
E : (p : GHSpace) → ↑(s p) ≃ Fin (Nat.card ↑(s p)) := fun p ↦ Finite.equivFin ↑(s p)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) := fun p ↦ ⟨N p, fun a b ↦ ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x : q.Rep), ∃ z, dist x (Φ z) ≤ ε
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
⊢ y ∈ U

Tactic:
have := U.isOpen

Goal state after:
X : Type v
inst✝² : TopologicalSpace X
inst✝¹ : Preorder X
inst✝ : Topology.IsUpperSet X
x : X
U : Opens X
hx : x ∈ U
y : X
hy : y ∈ principalOpen x
this : IsOpen[inst✝²] ↑U
⊢ y ∈ U
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_2
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x : q.Rep), ∃ y, dist x (Φ y) ≤ ε

Tactic:
show ∀ x : q.Rep, ∃ z : s p, dist x (Φ z) ≤ ε

Goal state after:
case refine_2
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
⊢ ∀ (x : q.Rep), ∃ z, dist x (Φ z) ≤ ε
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
⊢ ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r

Tactic:
rintro _ ⟨z, rfl⟩

Goal state after:
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
⊢ ∃ y ∈ range (optimalGHInjr X Y), dist (optimalGHInjl X Y z) y ≤ r
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
⊢ ∀ x ∈ range (optimalGHInjr X Y), ∃ y ∈ range (optimalGHInjl X Y), dist x y ≤ r

Tactic:
rintro _ ⟨z, rfl⟩

Goal state after:
case refine_2
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : Cb X Y
h : f ∈ candidatesB X Y
r : ℝ
hr : HD (optimalGHDist X Y) < r
A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r
z : Y
⊢ ∃ y ∈ range (optimalGHInjl X Y), dist (optimalGHInjr X Y z) y ≤ r
Module: Mathlib.Topology.UniformSpace.Dini

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone fun x_1 ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformlyOn F f atTop s

Tactic:
rw [tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝⁵ : Preorder ι
inst✝⁴ : TopologicalSpace α
inst✝³ : NormedAddCommGroup G
inst✝² : Lattice G
inst✝¹ : HasSolidNorm G
inst✝ : IsOrderedAddMonoid G
F : ι → α → G
f : α → G
s : Set α
hF_cont : ∀ (i : ι), ContinuousOn (F i) s
hF_mono : ∀ x ∈ s, Monotone fun x_1 ↦ F x_1 x
hf : ContinuousOn f s
h_tendsto : ∀ x ∈ s, Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (f x))
⊢ TendstoLocallyUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) atTop
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X✝ : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X✝ n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X✝ n)
inst✝ : ∀ (n : ℕ), Nonempty (X✝ n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
this : ∀ (n : ℕ), 0 < d n
u : ℕ → GHSpace
hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < d N
X : ℕ → Type := fun n ↦ (u n).Rep
Y : (n : ℕ) → AuxGluingStruct (X n) := auxGluing X
E : ∀ (n : ℕ), GlueSpace ⋯ ⋯ = (Y (n + 1)).Space
c : (n : ℕ) → GlueSpace ⋯ ⋯ → (Y (n + 1)).Space := fun n ↦ cast ⋯
ic : ∀ (n : ℕ), Isometry (c n)
f : (n : ℕ) → (Y n).Space → (Y (n + 1)).Space := fun n ↦ c n ∘ toGlueL ⋯ ⋯
I : ∀ (n : ℕ), Isometry (f n)
Z0 : Type := InductiveLimit I
Z : Type := UniformSpace.Completion Z0
Φ : (n : ℕ) → (Y n).Space → InductiveLimit I := toInductiveLimit I
coeZ : Z0 → UniformSpace.Completion Z0 := UniformSpace.Completion.coe'
X2 : ℕ → Set (UniformSpace.Completion Z0) := fun n ↦ range (coeZ ∘ Φ n ∘ (Y n).embed)
isom : ∀ (n : ℕ), Isometry (coeZ ∘ Φ n ∘ (Y n).embed)
X2n : ∀ (n : ℕ), X2 n = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjl (X n) (X n.succ))
X2nsucc : ∀ (n : ℕ), X2 n.succ = range ((coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯) ∘ optimalGHInjr (X n) (X n.succ))
n : ℕ
⊢ Isometry (coeZ ∘ Φ n.succ ∘ c n ∘ toGlueR ⋯ ⋯)

Tactic:
apply UniformSpace.Completion.coe_isometry.comp _
      exact (toInductiveLimit_isometry _ _).comp ((ic n).comp (toGlueR_isometry _ _))

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Basic

Goal state before:
pp: X : Type u_1
inst✝² : UniformSpace X
x : X
V : SetRel X X
inst✝¹ : V.IsSymm
inst✝ : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsClosed[inst✝².toTopologicalSpace] (ball x V)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_ball_subset]
  exact fun y hy ↦ ⟨V, h', fun z hyz hxz ↦ hy <| V.trans hxz <| V.symm hyz⟩

Goal state after: