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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑U),
    (∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑U)),
    IsOpen s → IsOpen[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑U),
    (∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsOpen[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑U)),
    IsOpen s → IsOpen[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.Germ

Goal state before:
pp: 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 ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f

Tactic:
]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
⊢ ∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f a ∈ s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
s : Set Y
a : X
ha : a ∈ f ⁻¹' s
b : Y
hb : f =ᶠ[𝓝 a] fun x ↦ b
x : X
hx : x ∈ {x | (fun x ↦ f x = (fun x ↦ b) x) x}
this : f x = f a
⊢ f a ∈ s
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ DiscreteTopology ↑{none}

Tactic:
]

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ DiscreteTopology ↑{none}
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y

Tactic:
]

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y
Module: Mathlib.Topology.Hom.Open

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
g : β →CO γ
f₁ f₂ : α →CO β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝³ i] (⇑f ⁻¹' V)

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝³ i] (⇑f ⁻¹' V)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case some.some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
val✝¹ val✝ : α
xy : edist (some val✝¹) (some val✝) = 0
⊢ some val✝ = some val✝

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑F),
    (∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑F)),
    IsClosed s → IsClosed[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
this :
  ∀ (V : Set ↑F),
    (∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)) →
      IsClosed[instTopologicalSpaceSubtype] V
⊢ ∀ (s : Set (WithGeneratedByTopology X ↑F)),
    IsClosed s → IsClosed[instTopologicalSpaceSubtype] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed[inst✝³ i] (⇑f ⁻¹' V)

Tactic:
]

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set Y
hV✝ : V ⊆ F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' Subtype.val ⁻¹' V)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsClosed[inst✝³ i] (⇑f ⁻¹' V)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1

Tactic:
]

Goal state after:
θ : ↑I
⊢ ↑θ + 1 ≤ 1 + 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * ↑t, ⋯⟩ = 2 * ↑t

pp: t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)

Tactic:
]

Goal state after:
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑⟨1, ⋯⟩ = 1

pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

pp: t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
]

Goal state after:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t

Tactic:
]

Goal state after:
t : ↑I
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ x = x

Tactic:
]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ y = y

Tactic:
]

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

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1

Tactic:
]

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑⟨2 * ↑t, ⋯⟩

Tactic:
]

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ (if ↑t ≤ 1 / 2 then 2 * ↑t else 1) = ↑⟨2 * ↑t, ⋯⟩
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, ContractibleSpace ↑r ∧ r ⊆ t

Tactic:
]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
ι : Type u_3
p : X → ι → Prop
s : X → ι → Set X
h : ∀ (x : X), (𝓝 x).HasBasis (p x) (s x)
h' : ∀ (x : X) (i : ι), p x i → ContractibleSpace ↑(s x i)
x : X
⊢ ∀ t ∈ 𝓝 x, ∃ r ∈ 𝓝 x, ContractibleSpace ↑r ∧ r ⊆ t
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y : X
ι : Type u_3
inst✝ : StronglyLocallyContractibleSpace X
x : X
s : Set X
x✝ : s ∈ 𝓝 x ∧ ContractibleSpace ↑s
hs : s ∈ 𝓝 x
hs' : ContractibleSpace ↑s
⊢ PathConnectedSpace ↑s

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x✝¹ y : X
ι : Type u_3
inst✝ : StronglyLocallyContractibleSpace X
x : X
s : Set X
x✝ : s ∈ 𝓝 x ∧ ContractibleSpace ↑s
hs : s ∈ 𝓝 x
hs' : ContractibleSpace ↑s
⊢ PathConnectedSpace ↑s
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis
    (fun x_1 ↦
      match (x, y) with
      | (x, y) =>
        match x_1 with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
    fun x ↦
    match x with
    | (Ux, Uy) => Ux ×ˢ Uy

Tactic:
]

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis
    (fun x_1 ↦
      match (x, y) with
      | (x, y) =>
        match x_1 with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
    fun x ↦
    match x with
    | (Ux, Uy) => Ux ×ˢ Uy
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ Nat.find ⋯

Tactic:
]

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ 1 ≤ Nat.find ⋯
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ ↑(#({x ∈ V | edist t x ≤ ↑(Nat.find ⋯) * c})) ≤ a ^ Nat.find ⋯

Tactic:
]

Goal state after:
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
⊢ ↑(#({x ∈ V | edist t x ≤ ↑(Nat.find ⋯) * c})) ≤ a ^ Nat.find ⋯
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case neg
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
⊢ a ^ (Nat.find ⋯ - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))

Tactic:
]

Goal state after:
case neg
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
⊢ a ^ (Nat.find ⋯ - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_1
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)

Tactic:
simpa using isOpen_Ioi

Goal state after:
Module: Mathlib.Topology.Instances.PNat

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈↑↑n - r⌉₊ ⌊↑↑n + r⌋₊)

Tactic:
]

Goal state after:
n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈↑↑n - r⌉₊ ⌊↑↑n + r⌋₊)
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).2 ∩ (s, o).1ᶜ).Nonempty

Tactic:
]

Goal state after:
p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).2 ∩ (s, o).1ᶜ).Nonempty
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
]

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: a✝ : (𝓝 ∞).IsCountablyGenerated
this : (cocompact ℚ).IsCountablyGenerated
⊢ False

Tactic:
]

Goal state after:
a✝ : (𝓝 ∞).IsCountablyGenerated
this : (cocompact ℚ).IsCountablyGenerated
⊢ False
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this : (Rat.cast '' s).OrdConnected
⊢ False

Tactic:
]

Goal state after:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
this : (Rat.cast '' s).OrdConnected
⊢ False
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset.Nonempty

Tactic:
]

Goal state after:
case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J

Tactic:
]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
⊢ ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J

Tactic:
]

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
⊢ ∀ x ∈ Finset.range #J, pairSetSeq J a c x ⊆ J ×ˢ J
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (t₀, t).1 = 0 ∨ (t₀, t).1 = 1

Tactic:
]

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (t₀, t).1 = 0 ∨ (t₀, t).1 = 1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (t₀, t).2 j = 0 ∨ (t₀, t).2 j = 1

Tactic:
]

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (t₀, t).2 j = 0 ∨ (t₀, t).2 j = 1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
        a ^ ((logSizeBallSeq J hJ a c i).radius - ?m.162 i + ?m.162 i) ≤
    a * ↑(#J)

pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ℕ → ℕ

Tactic:
]

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∑ i ∈ Finset.range #J,
      (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
        a ^ ((logSizeBallSeq J hJ a c i).radius - ?m.162 i + ?m.162 i) ≤
    a * ↑(#J)

T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ℕ → ℕ
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ a *
      ∑ i ∈ Finset.range #J,
        (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    a * ↑(#J)

Tactic:
]

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ a *
      ∑ i ∈ Finset.range #J,
        (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    a * ↑(#J)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case h₂
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#((Finset.range #J).biUnion fun x ↦ (logSizeBallSeq J hJ a c x).smallBall c)) ≤ ↑(#J)

Tactic:
]

Goal state after:
case h₂
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#((Finset.range #J).biUnion fun x ↦ (logSizeBallSeq J hJ a c x).smallBall c)) ≤ ↑(#J)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∈ Cube.boundary (M ⊕ N) ↔ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
by
  constructor
  · rintro ⟨i | i, hi⟩
    · exact Or.inl ⟨i, hi⟩
    · exact Or.inr ⟨i, hi⟩
  · rintro (⟨m, hm⟩ | ⟨n, hn⟩)
    · exact ⟨Sum.inl m, hm⟩
    · exact ⟨Sum.inr n, hn⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∀ x ∈ Finset.range #J,
    {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c} ⊆
      J

Tactic:
]

Goal state after:
case a
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ∀ x ∈ Finset.range #J,
    {x_1 ∈ (logSizeBallSeq J hJ a c x).finset |
        edist (logSizeBallSeq J hJ a c x).point x_1 ≤ (↑(logSizeBallSeq J hJ a c x).radius - 1) * c} ⊆
      J