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

Goal state before:
pp: case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
⊢ ↑(Fintype.card (ConnectedComponents X)) ≤ (f ⁻¹' {y}).encard

Tactic:
refine h (fun i ↦ ConnectedComponents.mk ⁻¹' {(Fintype.equivFin _).symm i}) (fun i ↦ ?_)
          (fun i ↦ ?_) (fun i j hij ↦ Disjoint.preimage _ (by simp [hij])) ?_

Goal state after:
case inl.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
i : Fin (Fintype.card (ConnectedComponents X))
⊢ IsClopen (mk ⁻¹' {(Fintype.equivFin (ConnectedComponents X)).symm i})

case inl.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
i : Fin (Fintype.card (ConnectedComponents X))
⊢ (mk ⁻¹' {(Fintype.equivFin (ConnectedComponents X)).symm i}).Nonempty

case inl.intro.refine_3
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
⊢ ⋃ i, mk ⁻¹' {(Fintype.equivFin (ConnectedComponents X)).symm i} = Set.univ
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
i j : ConnectedComponents Y
hij : i ≠ j
⊢ Disjoint {i} {j}

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m p.Tail • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑p.Tail)).prod =
    m p.Tail • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑p.Tail)).prod

Tactic:
List.map_cons,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : ↑m.support ⊆ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
hx'' : q < (↑l).Tail
p : Products I
hp : ↑p ≠ [] ∧ (↑p).head! = term I ho ∧ q = p.Tail
⊢ m p.Tail • (Linear_CC' C hsC ho) (e C (term I ho) :: List.map (e C) ↑p.Tail).prod =
    m p.Tail • (Linear_CC' C hsC ho) (e C (term I ho) :: List.map (e C) ↑p.Tail).prod
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
obtain ⟨x, hx⟩ := exist_norm_eq h
      exact fun h ↦ hx ▸ h x

Goal state after:
Module: Mathlib.Topology.ContinuousMap.LocallyConstant

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : Semiring Y
inst✝¹ : Algebra R Y
inst✝ : IsTopologicalSemiring Y
r : R
⊢ ↑((algebraMap R (LocallyConstant X Y)) r) = (algebraMap R C(X, Y)) r

Tactic:
by
    ext x
    simp [Algebra.smul_def]

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
by_cases! hfin : (Set.range x).Finite

Goal state after:
case pos
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

case neg
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Infinite
⊢ ∃ a ∈ A, MapClusterPt a cofinite x
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : b < ↑x
⊢ ((F i).concat (G i)) x ∈ U

Tactic:
· replace hxb : b ≤ x := hxb.le
    rw [concat_right hfg hxb]
    refine hg ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩
    simp [projIccCM, projIcc, hxb, x.2.2]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
l : Filter X
⊢ Tendsto pure l (𝓝 l)

Tactic:
rw [Filter.tendsto_nhds]
  exact fun s hs ↦ Eventually.mono hs fun x ↦ id

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

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
yh : y ∈ Metric.eball a r
yx : some y = x
⊢ some y ∈ Metric.eball (some a) r

Tactic:
simpa

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 ≤ if h : 1 < a then Nat.find ⋯ else 0

Tactic:
dif_pos ha

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 ≤ ↑(if h : 1 < a then Nat.find ⋯ else 0) * c})) ≤ a ^ if h : 1 < a then Nat.find ⋯ else 0

Tactic:
dif_pos ha

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

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

Tactic:
dif_pos ha

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: 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:
intro i hi

Goal state after:
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
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
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
⊢ ∃ i < #J, (s, t) ∈ pairSetSeq J a c i

Tactic:
simpa [pairSet] using h

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

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = ((toLoop i p) x✝) y✝

pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
toLoop_apply

Goal state after:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = ((toLoop i q) x✝) y✝

pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
toLoop_apply

Goal state after:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
⊢ ∀ b ∈ s, (∃ b_1 ∈ s, (f b) x z ≤ (f b_1) x y) ∨ ∃ b_1 ∈ s, (f b) x z ≤ (f b_1) y z

Tactic:
intro i hi

Goal state after:
case inr
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
⊢ (∃ b ∈ s, (f i) x z ≤ (f b) x y) ∨ ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.MetricSpace.HausdorffAlexandroff

Goal state before:
pp: ⊢ Function.Surjective fromBinary

Tactic:
refine Subtype.coind_surjective _ ((ofDigits_SurjOn (by norm_num)).comp ?_)

Goal state after:
⊢ Set.SurjOn (⇑(Homeomorph.piCongrRight fun x ↦ finTwoEquiv.toHomeomorphOfDiscrete.symm)) Set.univ Set.univ
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

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

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

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

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

Tactic:
· exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))

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

case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
𝕜 : Type u_3
inst✝² : SeminormedRing 𝕜
inst✝¹ : Module 𝕜 Y
inst✝ : NormSMulClass 𝕜 Y
c : 𝕜
hc : ‖c‖₊ ≠ 0
⊢ MemHolder r (c • f) ↔ MemHolder r f

Tactic:
by
  refine ⟨fun ⟨h, hh⟩ => ⟨h * ‖c‖₊⁻¹, ?_⟩, .smul⟩
  rw [← HolderWith.smul_iff _ hc, inv_mul_cancel_right₀ hc]
  exact hh

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
x y : α
⊢ (ENNReal.ofReal (dist x y)).toReal = dist x y

Tactic:
exact ENNReal.toReal_ofReal dist_nonneg

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
x y z : α
s t : Set α
inst✝ : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
infsep_zero,

Goal state after:
α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ s.einfsep = 0 ∨ s.einfsep = ∞ ↔ s.Subsingleton
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : MetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.infsep ↔ s.Nontrivial

Tactic:
by
  rw [infsep_pos, einfsep_lt_top_iff, and_iff_right_iff_imp]
  exact fun _ => einfsep_pos_of_finite

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
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')

Tactic:
← this

Goal state after:
X : Type u
inst✝⁶ : MetricSpace X
inst✝⁵ : CompactSpace X
inst✝⁴ : Nonempty X
Y : Type v
inst✝³ : MetricSpace Y
inst✝² : CompactSpace Y
inst✝¹ : Nonempty Y
γ : Type w
inst✝ : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h✝ : xX ∈ univ
s : Set γ := range Φ ∪ range Ψ
Φ' : X → ↑s := fun y ↦ ⟨Φ y, ⋯⟩
Ψ' : Y → ↑s := fun y ↦ ⟨Ψ y, ⋯⟩
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this✝² : IsCompact s
this✝¹ : CompactSpace ↑s
ΦΦ' : Φ = Subtype.val ∘ Φ'
ΨΨ' : Ψ = Subtype.val ∘ Ψ'
this✝ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : ↑s → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding ↑s
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
n i j : ℕ
hij : U (Nat.pair n i) = U (Nat.pair n j)
this : Nat.pair n i = Nat.pair n j
⊢ i = j

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a : α
⊢ 𝓝 a = 𝓟 (Ici a)

Tactic:
by
  rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ 𝓝 a = 𝓟 (Iic a)

Tactic:
by
  rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
by_cases hU : U = univ
  · simp only [hU, isOpen_univ, compl_Ici, true_or]
  refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩
  intro hO
  apply Or.inr
  convert! IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO
  constructor
  · intro ⟨a, ha⟩
    use {U}
    constructor
    · apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)
      use a
    · rw [sUnion_singleton]
  · intro ⟨S, hS1, hS2⟩
    have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)
    use sSup {a | (Ici a)ᶜ ∈ S}
    rw [hS2, sUnion_eq_compl_sInter_compl, compl_inj_iff]
    apply le_antisymm
    · intro b hb
      simp only [sInter_image, mem_iInter, mem_compl_iff]
      intro s hs
      obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs
      subst hS2 ha
      simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_ofPred_eq, mem_Iio, not_lt]
    · intro b hb
      rw [mem_Ici, sSup_le_iff]
      intro c hc
      simp only [sInter_image, mem_iInter] at hb
      rw [← not_lt, ← mem_Iio, ← compl_Ici]
      exact hb _ hc

Goal state after: