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
⊢ IsGeneratedBy X ↑U

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ edist a b = ∞ ↔ a ≠ b ∧ (a = ∞ ∨ b = ∞)

Tactic:
by

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
⊢ IsGeneratedBy X ↑F

Tactic:
by

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)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ F

Tactic:
by

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)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ Continuous fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2))

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ { toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ } ((e, e), e, e) = (e, e)

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
⊢ Continuous G

Tactic:
by

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
⊢ IsGeneratedBy X ↑F

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y)))).HomotopyRel
    (ContinuousMap.id (X × Y)) {(e, e)}

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
⊢ Continuous G

Tactic:
by

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e)))).HomotopyRel
    (ContinuousMap.id (X × Y)) {(e, e)}

Tactic:
by

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

Goal state before:
pp: M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
⊢ { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((const M 1).prodMk (ContinuousMap.id M)) =
    ContinuousMap.id M

Tactic:
by

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

Goal state before:
pp: M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
⊢ { toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (const M 1)) =
    ContinuousMap.id M

Tactic:
by

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

Goal state before:
pp: G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : IsTopologicalGroup G'
⊢ hSpace (G × G') = HSpace.prod G G'

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 2 * ↑p.1

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 1 + ↑p.2

Tactic:
by

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

Goal state before:
pp: θ : ↑I
⊢ 2 * ↑(0, θ).1 / (1 + ↑(0, θ).2) ≤ 0

Tactic:
by

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

Goal state before:
pp: θ : ↑I
⊢ 1 * (1 + ↑(1, θ).2) ≤ 2 * ↑(1, θ).1

Tactic:
by

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

Goal state before:
pp: t : ↑I
⊢ ↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Tactic:
by

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

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

Tactic:
by

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
⊢ Continuous fun t ↦ γ (qRight (t, θ))

Tactic:
by

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
⊢ γ (qRight (0, θ)) = x

Tactic:
by

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
⊢ γ (qRight (1, θ)) = y

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 0 γ = γ.trans (refl y)

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflRight 1 γ = γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 0 γ = (refl x).trans γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 1 γ = γ

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflLeft p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((const (Path x x) (refl x)).prodMk (ContinuousMap.id (Path x x))))
          x_1

Tactic:
by

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflRight p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (Path x x)).prodMk (const (Path x x) (refl x))))
          x_1

Tactic:
by

Goal state after:
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
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ ContractibleSpace ↑s) id

Tactic:
by

Goal state after:
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
⊢ (𝓝 x).HasBasis (fun s ↦ s ∈ 𝓝 x ∧ IsPathConnected s) id

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 ≤ logSizeRadius t V a c

Tactic:
by

Goal state after:
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 ≤ ↑(logSizeRadius t V a c) * c})) ≤ a ^ logSizeRadius t V a c

Tactic:
by

Goal state after:
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
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ t ∈ {x ∈ V | edist t x = 0}

Tactic:
by

Goal state after:
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
inst✝ : StronglyLocallyContractibleSpace Y
⊢ StronglyLocallyContractibleSpace (X × Y)

Tactic:
by

Goal state after:
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
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
⊢ Nat.find ⋯ - 1 < Nat.find ⋯

Tactic:
by

Goal state after:
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
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
this : Nat.find ⋯ - 1 < Nat.find ⋯
h : 1 ≤ Nat.find ⋯ - 1 → a ^ (Nat.find ⋯ - 1) < ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))
⊢ 1 ≤ Nat.find ⋯ - 1

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
⊢ LocallyContractibleSpace X

Tactic:
by

Goal state after:
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
ht : t ∈ V
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).finset ⊆ J

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: ⊢ Continuous toENNReal

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ ↑(#({x ∈ J | edist (Exists.choose hJ) x ≤ ↑n * c})) ≤ ↑(#J)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).radius ≤ n

Tactic:
by

Goal state after:
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
ha : 1 < a
i : ℕ
⊢ 1 ≤ (logSizeBallSeq J hJ a c i).radius

Tactic:
by

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

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (closedBall n r)

Tactic:
by

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

Goal state before:
pp: ⊢ (Filter.cocompact ℕ+).NeBot

Tactic:
by

Goal state after:
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
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ (logSizeBallSeq J hJ a c i).finset

Tactic:
by

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

Goal state before:
pp: p : ℚ
s : Set ℚ
⊢ (cocompact ℚ ⊓ 𝓝 p).NeBot

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∈ J

Tactic:
by

Goal state after:
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
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∉ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
by

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

Goal state before:
pp: ⊢ ¬(cocompact ℚ).IsCountablyGenerated

Tactic:
by

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

Goal state before:
pp: a✝ : (𝓝 ∞).IsCountablyGenerated
⊢ (comap OnePoint.some (𝓝 ∞)).IsCountablyGenerated

Tactic:
by

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

Goal state before:
pp: ⊢ ¬(𝓝 ∞).IsCountablyGenerated

Tactic:
by

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

Goal state before:
pp: ⊢ ¬FirstCountableTopology ℚ∞

Tactic:
by

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

Goal state before:
pp: a✝ : SecondCountableTopology ℚ∞
⊢ False

Tactic:
exact not_firstCountableTopology_opc inferInstance

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

Goal state before:
pp: ⊢ ¬SecondCountableTopology ℚ∞

Tactic:
by

Goal state after:
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
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (logSizeBallSeq J hJ a c i).finset

Tactic:
by

Goal state after:
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
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset < #(logSizeBallSeq J hJ a c i).finset

Tactic:
by

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

Goal state before:
pp: p : ℚ
s : Set ℚ
⊢ TotallyDisconnectedSpace ℚ

Tactic:
by

Goal state after:
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
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
this : #(logSizeBallSeq J hJ a c i).finset = 0
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - (i + 1)

Tactic:
by

Goal state after:
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
i : ℕ
⊢ #(logSizeBallSeq J hJ a c i).finset ≤ #J - i

Tactic:
by

Goal state after:
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 = 0

Tactic:
by

Goal state after:
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
i j : ℕ
hij : i ≠ j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
x✝² x✝¹ : ↑(Ω^ N X x)
f : (N → ↑I) → X
continuous_toFun✝¹ : Continuous[_, inst✝] f
property✝¹ : { toFun := f, continuous_toFun := continuous_toFun✝¹ } ∈ Ω^ N X x
g : (N → ↑I) → X
continuous_toFun✝ : Continuous[_, inst✝] g
property✝ : { toFun := g, continuous_toFun := continuous_toFun✝ } ∈ Ω^ N X x
x✝ :
  (fun f ↦ ⇑↑f) ⟨{ toFun := f, continuous_toFun := continuous_toFun✝¹ }, property✝¹⟩ =
    (fun f ↦ ⇑↑f) ⟨{ toFun := g, continuous_toFun := continuous_toFun✝ }, property✝⟩
⊢ ⟨{ toFun := f, continuous_toFun := continuous_toFun✝¹ }, property✝¹⟩ =
    ⟨{ toFun := g, continuous_toFun := continuous_toFun✝ }, property✝⟩

Tactic:
by

Goal state after:
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
⊢ pairSet J a c ⊆ J ×ˢ J

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ { toFun := g, continuous_toFun := ⋯ } ∈ Ω^ N X x

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x : X
f : ↑(Ω^ N X x)
g : (N → ↑I) → X
h : g = ⇑f
⊢ copy f g h = f

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
⊢ Continuous fun t m ↦ t (e m)

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ y (e (e.symm n)) = 0 ∨ y (e (e.symm n)) = 1

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
y : N → ↑I
x✝ : y ∈ Cube.boundary N
n : N
hn : y n = 0 ∨ y n = 1
⊢ ((↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }) y = x

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
⊢ Continuous fun t n ↦ t (e.symm n)

Tactic:
by

Goal state after:
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
i : ℕ
ha : 1 < a
⊢ ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ y (e.symm (e m)) = 0 ∨ y (e.symm (e m)) = 1

Tactic:
by

Goal state after:
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
i : ℕ
ha : 1 < a
⊢ (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c i).smallBall c))

Tactic:
match i with
  | 0 =>
    simpa [finset_logSizeBallSeq_zero, hJ, logSizeBallStruct.smallBall, radius_logSizeBallSeq_zero]
      using! pow_logSizeRadius_le_card_le_logSizeRadius ha (Exists.choose_spec hJ)
  | i + 1 =>
    by_cases! h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
    · simpa [h, logSizeBallStruct.smallBall, radius_logSizeBallSeq_add_one] using!
        pow_logSizeRadius_le_card_le_logSizeRadius ha
          (point_mem_finset_logSizeBallSeq hJ _ h)
    simp [h]

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ ((↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }) y = x

Tactic:
by

Goal state after:
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
i : ℕ
ha : 1 < a
⊢ (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ ((logSizeBallSeq J hJ a c i).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c i).smallBall c))

Tactic:
by

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
⊢ (fun p ↦ ⟨(↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ ⟨(↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }, ⋯⟩) p) =
    p

Tactic:
by

Goal state after: