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

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
a : α
l : List α
hl : l.length = n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 ⟨l, hl⟩) (𝓝 (insertIdx a i ⟨l, hl⟩))

Tactic:
rw [insertIdx, tendsto_subtype_rng]
    simp only [insertIdx_val]
    exact List.tendsto_insertIdx tendsto_fst (Tendsto.comp continuousAt_subtype_val tendsto_snd : _)

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j

Tactic:
· rw [h]

Goal state after:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ pi1EquivFundamentalGroup.toFun (⟦p⟧ * ⟦q⟧) = pi1EquivFundamentalGroup.toFun ⟦p⟧ * pi1EquivFundamentalGroup.toFun ⟦q⟧

Tactic:
simp only [HomotopyGroup.mul_spec (i := (0 : Fin 1))]

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
a b : π_ 1 X x
p q : ↑(Ω^ (Fin 1) X x)
⊢ pi1EquivFundamentalGroup.toFun ⟦transAt 0 q p⟧ =
    pi1EquivFundamentalGroup.toFun ⟦p⟧ * pi1EquivFundamentalGroup.toFun ⟦q⟧
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist (inl x) (inl y) = 1 * dist (inl x) (inl y)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case e'_1
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
a b : α
n : ℕ
⊢ dist a (x n) - dist (x 0) (x n) - (dist b (x n) - dist (x 0) (x n)) = dist a (x n) - dist b (x n)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a (x n) + dist b (x n) = 2 * dist a (x n) + (dist b (x n) - dist a (x n))

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist (inr x) (inr y) = 1 * dist (inr x) (inr y)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) =
    dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(maxVar X Y) * max (dist x z) (dist y t) + ↑(maxVar X Y) * max (dist x z) (dist y t) =
    2 * ↑(maxVar X Y) * max (dist x z) (dist y t)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this✝ : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
m : ℕ
m_ge_n : m ≥ n
hm : z ∈ ↑(s m)
this : hausdorffEDist ↑(s m) ↑(s n) < B n
⊢ ∃ y ∈ s n, edist x y ≤ 2 * B n

Tactic:
obtain ⟨y : α, hy : y ∈ (s n : Set α), Dzy : edist z y < B n⟩ :=
      exists_edist_lt_of_hausdorffEDist_lt hm this

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
n : ℕ
x : α
xt0 : x ∈ t0
this✝ : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
z : α
Dxz : edist x z < B n
m : ℕ
m_ge_n : m ≥ n
hm : z ∈ ↑(s m)
this : hausdorffEDist ↑(s m) ↑(s n) < B n
y : α
hy : y ∈ ↑(s n)
Dzy : edist z y < B n
⊢ ∃ y ∈ s n, edist x y ≤ 2 * B n
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ ∀ (i : Set X), IsCover ε A i → ∀ i_2 ⊆ A, IsSeparated (2 * ↑ε) i_2 → i_2.encard ≤ i.encard

Tactic:
intro C hC_cover D hD_subset hD_separated

Goal state after:
X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A C : Set X
hC_cover : IsCover ε A C
D : Set X
hD_subset : D ⊆ A
hD_separated : IsSeparated (2 * ↑ε) D
⊢ D.encard ≤ C.encard
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: X : Set (ℕ → Bool)
h_closed : IsClosed X
h_nonempty : X.Nonempty
f : (ℕ → Bool) → ℕ → Bool
fs : ∀ x ∈ X, f x = x
frange : Set.range f = X
hf : LipschitzWith 1 f
⊢ ∃ f, Continuous f ∧ Set.range f = X

Tactic:
exact ⟨f, hf.continuous, frange⟩

Goal state after:
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
d : ℝ
hs : s.Nontrivial
⊢ d ≤ s.infsep ↔ ∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ dist x y

Tactic:
exact hs.le_infsep_iff

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
f : ℕ → X
hf : IsEmbedding f
⊢ DiscreteTopology ↑(range f)

Tactic:
exact hf.toHomeomorph.symm.isEmbedding.discreteTopology

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam univ + (diam univ + 1 + diam univ) + diam univ = 2 * diam univ + 1 + 2 * diam univ

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
⊢ IsOpen[t] s ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
simp +instances [topology_eq_scottHausdorff (α := α) (D := D), IsOpen, scottHausdorff]

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: x : GHSpace
⊢ dist x x = 0

Tactic:
rcases exists_rep x with ⟨y, hy⟩
    refine le_antisymm ?_ ?_
    · apply csInf_le
      · exact ⟨0, by rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg⟩
      · simp only [mem_image, mem_prod, mem_ofPred_eq, Prod.exists]
        exists y, y
        simpa only [and_self_iff, hausdorffDist_self_zero, eq_self_iff_true, and_true]
    · apply le_csInf
      · exact Set.Nonempty.image _ <| Set.Nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩
      · rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg

Goal state after:
Module: Mathlib.Topology.Separation.NotNormal

Goal state before:
pp: X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
⊢ 2 ^ #↑s ≤ 2 ^ #↑d

Tactic:
have h_closed (t) (ht : t ∈ 𝒫 s) : IsClosed t := by
    rw [← inter_eq_self_of_subset_right ht, ← Subtype.image_preimage_val]
    exact hs.isClosedMap_subtype_val _ (isClosed_discrete _)

Goal state after:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : NormalSpace X
s d : Set X
hs : IsClosed s
inst✝ : DiscreteTopology ↑s
hd : Dense d
h_closed : ∀ t ∈ 𝒫 s, IsClosed t
⊢ 2 ^ #↑s ≤ 2 ^ #↑d
Module: Mathlib.Topology.Sheaves.PUnit

Goal state before:
pp: case e'_5
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ s = ⊤

Tactic:
← Sieve.id_mem_iff_eq_top

Goal state after:
case e'_5
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
hind : X.str = ⊤
F : Presheaf C X
it : IsTerminal (F.obj (op ⊥))
c : C
U : TopologicalSpace.Opens ↑X
s : Sieve U
hs : s ∈ (Opens.grothendieckTopology ↑X) U
this : IndiscreteTopology ↑X
hne : U ≠ ⊥
⊢ s.arrows (𝟙 U)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∈ unop V
⊢ ((if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then a else ⊤_ C)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then b else ⊤_ C)

pp: case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∉ unop V
⊢ ((if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then a else ⊤_ C)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then b else ⊤_ C)

Tactic:
· have hU : p₀ ∈ U.unop := leOfHom i.unop hV
      simp only [skyscraperPresheaf_obj, hU, hV, ↓reduceDIte, eqToHom_trans_assoc, Category.assoc,
        eqToHom_trans]

Goal state after:
case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
A a b : C
f : a ⟶ b
U V : (Opens ↑X)ᵒᵖ
i : U ⟶ V
hV : p₀ ∉ unop V
⊢ ((if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then a else ⊤_ C)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj V)) =
    (if h : p₀ ∈ unop U then eqToHom ⋯ ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then b else ⊤_ C)
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f = eqToHom ⋯ ≫ (skyscraperPresheafCocone p₀ A y).ι.app (op h1.choose) ≫ f

Tactic:
← Category.assoc

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : ¬p₀ ⤳ y
h1 : ∃ U, p₀ ∉ ↑U :=
  match not_specializes_iff_exists_open.mp h with
  | Exists.intro U ⟨ho, ⟨h₀, hy⟩⟩ => Exists.intro ⟨{ carrier := U, is_open' := ho }, h₀⟩ hy
c : Cocone ((OpenNhds.inclusion y).op ⋙ skyscraperPresheaf p₀ A)
f : (skyscraperPresheafCocone p₀ A y).pt ⟶ c.pt
H : ∀ (j : (OpenNhds y)ᵒᵖ), (skyscraperPresheafCocone p₀ A y).ι.app j ≫ f = c.ι.app j
⊢ 𝟙 (skyscraperPresheafCocone p₀ A y).pt ≫ f = (eqToHom ⋯ ≫ (skyscraperPresheafCocone p₀ A y).ι.app (op h1.choose)) ≫ f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δ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 y : ↑(s p)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
this✝¹ : (F p).snd ((E p) x) ((E p) y) = ⌊ε⁻¹ * dist x y⌋
Ap : (F p).snd ⟨i, hip⟩ ⟨j, hjp⟩ = ⌊ε⁻¹ * dist x y⌋
this✝ : (F q).snd ((E q) (Ψ x)) ((E q) (Ψ y)) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq : (F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y)) = ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: δ : ℝ
δ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)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ ε + ε / 2 + ε = δ

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
x : X
A : ⨅ y, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl x, inr default)
⊢ dist x default + 1 + dist default default ≤ diam univ + 1 + diam univ

Tactic:
by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : MetricSpace Y
inst✝³ : CompactSpace X
inst✝² : CompactSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
y : Y
A : ⨅ x, (candidatesBDist X Y) (inl x, inr y) ≤ (candidatesBDist X Y) (inl default, inr y)
⊢ dist default default + 1 + dist default y ≤ diam univ + 1 + diam univ

Tactic:
by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Goal state after:
Module: Mathlib.Topology.Sheaves.Sheafify

Goal state before:
pp: X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ ∃ W iU iV, ∀ (w : ↥↑W), fU (iU w) = fV (iV w)

Tactic:
use ⟨W ⊓ (U' ⊓ V'), ⟨mW, mU, mV⟩⟩

Goal state after:
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U V : OpenNhds x
fU : (y : ↥↑U) → F.stalk ↑y
hU : (Sheafify.isLocallyGerm F).pred fU
fV : (y : ↥↑V) → F.stalk ↑y
hV : (Sheafify.isLocallyGerm F).pred fV
U' : Opens ↑X
mU : ↑⟨x, ⋯⟩ ∈ U'
iU : U' ⟶ ↑U
gU : F.obj (op U')
wU : ∀ (x_1 : ↥U'), (fun x_2 ↦ fU (iU x_2)) x_1 = (ConcreteCategory.hom (F.germ U' ↑x_1 ⋯)) gU
V' : Opens ↑X
mV : ↑⟨x, ⋯⟩ ∈ V'
iV : V' ⟶ ↑V
gV : F.obj (op V')
e : (ConcreteCategory.hom (F.germ U' x ⋯)) gU = (ConcreteCategory.hom (F.germ V' x ⋯)) gV
wV : ∀ (x_1 : ↥V'), (fun x_2 ↦ fV (iV x_2)) x_1 = (ConcreteCategory.hom (F.germ V' ↑x_1 ⋯)) gV
W : Opens ↑X
mW : x ∈ W
iU' : W ⟶ U'
iV' : W ⟶ V'
e' : (ConcreteCategory.hom (F.map iU'.op)) gU = (ConcreteCategory.hom (F.map iV'.op)) gV
⊢ ∃ iU iV, ∀ (w : ↥↑⟨W ⊓ (U' ⊓ V'), ⋯⟩), fU (iU w) = fV (iV w)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: 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 y : ↑(s p)
this✝¹ : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
this✝ : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩)
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y)) = ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝ : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
⊢ (sublevelLeft X f b ↑⟨y, hy⟩).Nonempty

Tactic:
obtain ⟨x, hx, hx_le⟩ := LowerSemicontinuousOn.exists_isMinOn ne_X kX (hfy y hy)

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝ : TopologicalSpace E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
b : β
h : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
hx_le : IsMinOn (fun x ↦ f x y) X x
⊢ (sublevelLeft X f b ↑⟨y, hy⟩).Nonempty
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
⊢ HasSmallInductiveDimensionLT X 1 → IsTopologicalBasis {s | IsClopen s}

Tactic:
intro (.succ _ s hs h)
    refine hs.of_isOpen_of_subset (fun _ hU ↦ hU.isOpen) (fun U hU ↦ ⟨?_, hs.isOpen hU⟩)
    rw [← closure_subset_iff_isClosed]
    cases h U hU
    rwa [isEmpty_coe_sort, (hs.isOpen hU).frontier_eq, sdiff_eq_empty] at ‹_›

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
m n : ℕ
hmn : m ≤ n
H : HasSmallInductiveDimensionLT X m
⊢ HasSmallInductiveDimensionLT X n

Tactic:
induction n generalizing m X with

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: 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)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ 5⁻¹ * δ + 5⁻¹ * δ / 2 + 5⁻¹ * δ = δ / 2

Tactic:
ring

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
s : SetRel X X
inst✝ : s.IsSymm
x✝ : CauchyFilter X
⊢ ∀ (b : CauchyFilter X), (x✝, b) ∈ gen s → (b, x✝) ∈ gen s

Tactic:
simp [CauchyFilter.gen, s.mem_filter_prod_comm]

Goal state after: