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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
hsub : ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Tactic:
refine mem_of_superset ((biInter_mem hsf).2 fun L hL ↦ ?_) hsub

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
hsub : ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
L : Set X
hL : L ∈ s
⊢ {g | MapsTo (⇑g) L (⋃₀ t)} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
by
  rw [mem_interior_iff_mem_nhds, Filter.mem_nhds_iff]

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:
ext1

Goal state after:
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((const M 1).prodMk (ContinuousMap.id M))) a✝ =
    (ContinuousMap.id M) a✝
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:
ext1

Goal state after:
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (const M 1))) a✝ =
    (ContinuousMap.id M) a✝
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
⊢ qRight (t, 0) = 1

Tactic:
ext1

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑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
⊢ qRight (t, 0) = ⟨2 * ↑t, ⋯⟩

Tactic:
ext1

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑⟨2 * ↑t, ⋯⟩
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 : ¬logSizeRadius t V a c = 1
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))

Tactic:
rw [logSizeRadius, dif_pos ha] at h_one ⊢

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.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ {(logSizeBallSeq J ⋯ a c i).point}.product ((logSizeBallSeq J ⋯ a c i).ball c) ⊆ J ×ˢ J

Tactic:
apply Finset.product_subset_product

Goal state after:
case pos.hs
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J

case pos.ht
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
⊢ s = t

Tactic:
simp only [Nat.lt_one_iff.mp hn, pow_zero, Nat.cast_le_one] at hJ_card

Goal state after:
case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
hJ_card : #J ≤ 1
⊢ s = t
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
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
rintro ⟨⟨t, ht⟩, hst⟩

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
⊢ edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ ofDigits a ∈ preCantorSet 0

Tactic:
simp only [preCantorSet_zero, Set.mem_Icc]

Goal state after:
case zero
a : ℕ → Fin 3
h : ∀ (n : ℕ), a n ≠ 1
⊢ 0 ≤ ofDigits a ∧ ofDigits a ≤ 1
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l₁✝ l₂✝
ih :
  ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s

Tactic:
rcases mem_nhds_iff.1 ht with ⟨u, hut, hu⟩

Goal state after:
case cons
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u✝ : List (Set α)
a✝¹ : α
b✝ : Set α
l₁✝ : List α
l₂✝ : List (Set α)
ht : b✝ ∈ 𝓝 a✝¹
a✝ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l₁✝ l₂✝
ih :
  ∀ (s : Set (List α)), sequence l₂✝ ⊆ s → ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l₁✝ v ∧ sequence v ⊆ s
s : Set (List α)
hus : sequence (b✝ :: l₂✝) ⊆ s
u : Set α
hut : u ⊆ b✝
hu : IsOpen[inst✝] u ∧ a✝¹ ∈ u
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) (a✝¹ :: l₁✝) v ∧ sequence v ⊆ s
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x y z : X
⊢ (d ⊔ d') x z ≤ (d ⊔ d') x y ⊔ (d ⊔ d') y z

Tactic:
simp only [PseudoMetric.sup_apply]

Goal state after:
X : Type u_1
R : Type u_2
inst✝⁵ : AddZeroClass R
inst✝⁴ : SemilatticeSup R
inst✝³ : AddLeftMono R
inst✝² : AddRightMono R
d d' : PseudoMetric X R
inst✝¹ : d.IsUltra
inst✝ : d'.IsUltra
x y z : X
⊢ d x z ⊔ d' x z ≤ d x y ⊔ d' x y ⊔ (d y z ⊔ d' y z)
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
i : N
f g : ↑(Ω^ N X x)
⊢ (fun t ↦
      if ↑(t i) ≤ 1 / 2 then f (Function.update t i (Set.projIcc 0 1 ⋯ (2 * ↑(t i))))
      else g (Function.update t i (Set.projIcc 0 1 ⋯ (2 * ↑(t i) - 1)))) =
    ⇑(fromLoop i (Path.trans (toLoop i f) (toLoop i g)))

Tactic:
ext1

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))) =
    (fromLoop i (Path.trans (toLoop i f) (toLoop i g))) x✝
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
i : N
f : ↑(Ω^ N X x)
⊢ (fun t ↦ f fun j ↦ if j = i then σ (t i) else t j) = ⇑(fromLoop i (Path.symm (toLoop i f)))

Tactic:
ext1

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) = (fromLoop i (Path.symm (toLoop i f))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (fun j ↦ if j = i then σ (x✝ i) else x✝ j) = ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2)

Tactic:
ext1

Goal state after:
case e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f : ↑(Ω^ N X x)
x✝¹ : N → ↑I
x✝ : N
⊢ (if x✝ = i then σ (x✝¹ i) else x✝¹ x✝) =
    ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝¹).1, (↑(Cube.splitAt i) x✝¹).2) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))

Tactic:
ext1

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))

Tactic:
ext1

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))

Tactic:
ext1

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))

Tactic:
ext1

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
⊢ ∀ (a : ℕ → Bool), f a ∈ KC

Tactic:
by simp [← hf_surjective]

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
KC : Set (ℕ → Bool) := cantorToHilbert ⁻¹' KH
hKC_closed : IsClosed KC
f : (ℕ → Bool) → ℕ → Bool
hf_continuous : Continuous f
hf_surjective : Set.range f = KC
f' : (ℕ → Bool) → ↑KC := Subtype.coind f ⋯
hf'_surjective : Function.Surjective f'
h : ↑KC → ↑KH := KH.restrictPreimage cantorToHilbert
hh_continuous : Continuous h
hh_surjective : Function.Surjective h
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
exact ⟨g.symm ∘ h ∘ f', by fun_prop, g.symm.surjective.comp <| hh_surjective.comp hf'_surjective⟩

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
rw [edist_comm]
    exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep < ∞

Tactic:
rw [lt_top_iff_ne_top]

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ∞
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ ediam (⇑ofSnowflaking ⁻¹' s) = ediam s ^ α

Tactic:
← ENNReal.rpow_inv_rpow hα₀.ne' (ediam _),

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set X
⊢ (ediam (⇑ofSnowflaking ⁻¹' s) ^ α⁻¹) ^ α = ediam s ^ α
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : ¬DiscreteTopology X
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)

Tactic:
simp only [discreteTopology_iff_nhds_ne, not_forall, ← ne_eq, ← neBot_iff] at h

Goal state after:
case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
h : ∃ x, (𝓝[≠] x).NeBot
⊢ ∃ U, (∀ (n : ℕ), (U n).Nonempty) ∧ (∀ (n : ℕ), IsOpen[inst✝²] (U n)) ∧ Pairwise (Disjoint on U)
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
⊢ {S | ∃ a, (hull T a)ᶜ = S} = preimage Subtype.val '' IsLower.lowerBasis α

Tactic:
ext R

Goal state after:
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
⊢ R ∈ {S | ∃ a, (hull T a)ᶜ = S} ↔ R ∈ preimage Subtype.val '' IsLower.lowerBasis α
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
a : α
inst✝ : (𝓝[>] a).NeBot
this : Nonempty ↑(Ioi a)
c : α
hc : a < c
⊢ ∃ i', a < i' ∧ Iic i' ⊆ Iio c

Tactic:
simpa only [Iic_subset_Iio] using! Filter.nonempty_of_mem (Ioo_mem_nhdsGT hc)

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ DirSupClosed s

Tactic:
lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h,

Goal state after:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[S] s ↔ DirSupClosed s
Module: Mathlib.Topology.Sets.BaseChangeNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
U : ↑K.openNhds
L : Set α
h1 : IsCompact L
h2 : ↑K ⊆ interior L
h3 : L ⊆ ↑↑U
⊢ ∃ j₂, K.openRcNhdsToOpenNhds j₂ ≤ U

Tactic:
use ⟨⟨interior L, isOpen_interior⟩,
    ⟨IsCompact.of_isClosed_subset h1 isClosed_closure
      (closure_minimal interior_subset (IsCompact.isClosed h1)),
    h2⟩⟩

Goal state after:
case h
α : Type u_1
inst✝² : TopologicalSpace α
K : Compacts α
inst✝¹ : T2Space α
inst✝ : LocallyCompactSpace α
U : ↑K.openNhds
L : Set α
h1 : IsCompact L
h2 : ↑K ⊆ interior L
h3 : L ⊆ ↑↑U
⊢ K.openRcNhdsToOpenNhds ⟨{ carrier := interior L, is_open' := ⋯ }, ⋯⟩ ≤ U
Module: Mathlib.Topology.Sets.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LE α
s t : ClopenUpperSet α
h : (fun s ↦ s.carrier) s = (fun s ↦ s.carrier) t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s
    obtain ⟨⟨_, _⟩, _⟩ := t
    congr

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1

Tactic:
obtain ⟨U, ho, hu⟩ := isGδ_iff_eq_iInter_nat.1 hs.isGδ

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : PerfectlyNormalSpace X
s : Set X
hs : IsClosed[inst✝] s
U : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen[inst✝] (U n)
hu : s = ⋂ n, U n
⊢ ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op))
      ((ConcreteCategory.hom (F.obj.map ↑h₁.some.right)) (↑i).right.snd)

Tactic:
← Functor.map_comp_apply

Goal state after:
case inr.inl
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑i ⟶ ↑j)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op)) (StructuredArrow.right ↑i).snd =
    (ConcreteCategory.hom (F.obj.map (↑h₁.some.right ≫ ((f i).infLERight (f j)).op))) (↑i).right.snd
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map ((f i).infLELeft (f j)).op))
      ((ConcreteCategory.hom (F.obj.map ↑h₁.some.right)) (↑j).right.snd) =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd

Tactic:
← Functor.map_comp_apply

Goal state after:
case inr.inr
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := fun x ↦ unop (StructuredArrow.right ↑x).fst
i j : ↑c
h₁ : Nonempty (↑j ⟶ ↑i)
⊢ (ConcreteCategory.hom (F.obj.map (↑h₁.some.right ≫ ((f i).infLELeft (f j)).op))) (↑j).right.snd =
    (ConcreteCategory.hom (F.obj.map ((f i).infLERight (f j)).op)) (StructuredArrow.right ↑j).snd