mathlib-initiative/mathlib-tactics huggingface dataset:
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Function.Injective (sum_to C ho)

Tactic:
refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
    (fun ⟨a,ha⟩ ⟨b,hb⟩ ↦ (fun (hab : a = b) ↦ ?_))
  rw [← hab] at hb
  have ha' := Products.prop_of_isGood C _ ha (term I ho) hb.2
  simp only [ord_term_aux, lt_self_iff_false] at ha'

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inr
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 : Infinite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
· simp only [ENat.card_eq_top_of_infinite, top_le_iff, ENat.eq_top_iff_forall_ge]
      intro m
      obtain ⟨U, hU1, hU2, hU3, hU4⟩ := exists_fun_isClopen_of_infinite X (m + 1) (by simp)
      exact le_trans (by simp) (h U hU1 hU2 hU3 hU4)

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ¬∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0

pp: case pos
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ¬∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 0 = 1

Tactic:
· push Not at h₂; obtain ⟨i, hi⟩ := h₂; exfalso; rw [hi' i hi.1] at hi; exact hi.2 (h₁ i hi.1)

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
inst✝¹ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ¬∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 0 = 1
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
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 ∈ Finsupp.supported ℤ ℤ {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)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ w q • (πs C o) (eval (π C fun x ↦ ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.smul_mem

Goal state after:
case h₁
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 ∈ Finsupp.supported ℤ ℤ {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)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ (πs C o) (eval (π C fun x ↦ ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.ContinuousMap.LocallyConvex

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
E : Type u_3
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Semiring 𝕜
inst✝⁶ : PartialOrder 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : LocallyConvexSpace 𝕜 E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
K : Set X
U : Set E
hK : IsCompact (K, U).1
hU₀ : (K, U).2 ∈ 𝓝 0
hUc : Convex 𝕜 (K, U).2
f : C(X, E)
hf : f ∈ {f | Set.MapsTo ⇑f (K, U).1 (id (K, U).2)}
g : C(X, E)
hg : g ∈ {f | Set.MapsTo ⇑f (K, U).1 (id (K, U).2)}
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : X
hx : x ∈ (K, U).1
⊢ (a • f + b • g) x ∈ id (K, U).2

Tactic:
exact hUc (hf hx) (hg hx) ha hb hab

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

Goal state before:
pp: case h₂
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 ∈ Finsupp.supported ℤ ℤ {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)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : Products I
hq : m q ≠ 0
⊢ m q • (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.smul_mem

Goal state after:
case h₂
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 ∈ Finsupp.supported ℤ ℤ {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)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : Products I
hq : m q ≠ 0
⊢ (List.map (e C) (term I ho :: ↑q)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
A B : Set E
inst✝¹ : SequentialSpace E
inst✝ : CountablyCompactSpace E
⊢ SeqCompactSpace E

Tactic:
by_contra
  simp only [seqCompactSpace_iff, IsSeqCompact, mem_univ, not_forall,
    true_and, not_exists, not_and, exists_const] at this
  obtain ⟨x, hx⟩ := this
  -- Consider the set `A = ⋃ i, closure {x i}`. It is closed by `isClosed_of_not_tendsto` and thus
  -- countably compact.
  let A := ⋃ i, closure {x i}
  have : IsCountablyCompact A :=
    (isClosed_iUnion_closure_singleton_of_not_tendsto hx).isCountablyCompact
  -- We use the countably compactness of `A` to find a cluster point `a`. Eventually `a` does not
  -- belong to the closure of `{x n}` as `x` has no convergent subsequence, and this contradicts `a`
  -- being a cluster point.
  obtain ⟨a, ha⟩ : ∃ a ∈ A, MapClusterPt a atTop x := by
    refine isCountablyCompact_iff_seq_clusterPt.1 this _ (.of_forall fun n => ?_)
    exact mem_iUnion_of_mem n <| subset_closure <| mem_singleton (x n)
  obtain ⟨k, hk⟩ : ∃ k, ∀ n > k, a ∉ closure {x n} := by
    by_contra!
    obtain ⟨φ, hφ1, hφ2⟩ := Nat.exists_strictMono_subsequence this
    refine hx a φ hφ1 (tendsto_atTop_nhds.2 fun U ha hUo => ⟨0, fun n _ => ?_⟩)
    simpa using mem_closure_iff.1 (hφ2 n) U hUo ha
  have : a ∉ ⋃ i, closure {x (i + (k + 1))} := by
    simpa [← iUnion_ge_eq_iUnion_nat_add (fun n => closure {x n}) (k + 1)] using!
      fun i hi => hk i (Nat.lt_of_lt_of_eq hi rfl)
  apply this
  suffices h : closure (x '' Ici (k + 1)) ⊆ ⋃ i, closure {x (i + (k + 1))} from
    h <| mapClusterPt_atTop_iff_forall_mem_closure.1 ha.2 (k + 1)
  refine (IsClosed.closure_subset_iff
    (isClosed_iUnion_closure_singleton_of_not_tendsto fun l φ hφ => ?_)).2 ?_
  · exact hx l _ ((strictMono_id.add_const _).comp hφ)
  · simp only [image_eq_iUnion, mem_Ici, iUnion_ge_eq_iUnion_nat_add _ (k + 1)]
    exact iUnion_mono fun i => subset_closure

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
s : Set X
x✝ : s ∈ 𝓝 x ∧ ContractibleSpace ↑s
hs : s ∈ 𝓝 x
hs' : ContractibleSpace ↑s
⊢ IsPathConnected s

Tactic:
rw [isPathConnected_iff_pathConnectedSpace]

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

Tactic:
simp [point_logSizeBallSeq_add_one, h, Exists.choose_spec]

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 congr

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:
simpa using p.2 _ ⟨e m, by simpa using hm⟩

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
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp ↑(Cube.splitAt i) ∈ Ω^ N X x

Tactic:
by
    rintro y ⟨j, Hj⟩
    simp only [ContinuousMap.comp_apply,
      funSplitAt_apply, ContinuousMap.uncurry_apply, ContinuousMap.coe_mk,
      Function.uncurry_apply_pair]
    obtain rfl | Hne := eq_or_ne j i
    · rcases Hj with Hj | Hj <;> simp only [Hj, p.coe_toContinuousMap, p.source, p.target] <;> rfl
    · exact GenLoop.boundary _ _ ⟨⟨j, Hne⟩, Hj⟩

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

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (0, x✝)) =
    ↑p x✝

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]

Goal state after:
case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (((toLoop i p) (x✝ i)) fun j ↦ x✝ ↑j) = ↑p x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j ↦ x✝ ↑j) = x✝

Tactic:
apply (Cube.splitAt i).left_inv

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

Goal state before:
pp: case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (1, x✝)) =
    ↑q x✝

Tactic:
simp only [Prod.map_apply, id_eq, funSplitAt_apply,
      Function.uncurry_apply_pair, ContinuousMap.HomotopyWith.apply_zero,
      ContinuousMap.HomotopyWith.apply_one, ne_eq, Path.coe_toContinuousMap]

Goal state after:
case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ (((toLoop i q) (x✝ i)) fun j ↦ x✝ ↑j) = ↑q x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_2
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
x✝ : N → ↑I
⊢ ↑(Cube.insertAt i) (x✝ i, fun j ↦ x✝ ↑j) = x✝

Tactic:
apply (Cube.splitAt i).left_inv

Goal state after:
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
⊢ (s.sup' hs fun i ↦ (f i) x z) ≤ max (s.sup' hs fun i ↦ (f i) x y) (s.sup' hs fun i ↦ (f i) y z)

Tactic:
apply Finset.sup'_le

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
⊢ ∀ b ∈ s, (f b) x z ≤ max (s.sup' hs fun i ↦ (f i) x y) (s.sup' hs fun i ↦ (f i) y z)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
z : (l : ℕ) → ↥(s (n + l))
hz₀ : ↑(z 0) = x
hz : ∀ (k : ℕ), edist ↑(z k) ↑(z (k + 1)) ≤ B n / 2 ^ k
this : CauchySeq fun k ↦ ↑(z k)
y : α
y_lim : Tendsto (fun k ↦ ↑(z k)) atTop (𝓝 y)
k : ℕ
⊢ ∀ᶠ (x : ℕ) in atTop, ↑(z x) ∈ ⋃ m, ⋃ (_ : m ≥ k), ↑(s m)

Tactic:
by
            simp only [exists_prop, Set.mem_iUnion, Filter.eventually_atTop]
            exact ⟨k, fun m hm => ⟨n + m, by lia, (z m).2⟩⟩

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

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

Tactic:
rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩
  exact ⟨_, hx, _, hy, hxy⟩

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

Goal state before:
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.inr (einfsep_le_edist_of_mem hy hz hyz)

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

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

Tactic:
by
  rw [einfsep_top] at hs
  exact fun _ hx _ hy => of_not_not fun hxy => edist_ne_top _ _ (hs _ hx _ hy hxy)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ (if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
dif_pos hs

Goal state after:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Fintype ↑s
hs : s.Nontrivial
⊢ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ (if hs : s.Nontrivial then ⋯.toFinset.inf' ⋯ (uncurry dist) else 0) = ⋯.toFinset.inf' ⋯ (uncurry dist)

Tactic:
dif_pos hs

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag.Nonempty
⊢ (if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0) = s.offDiag.inf' hs (uncurry dist)

Tactic:
dif_pos hs

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Finset α
hs : s.offDiag.Nonempty
⊢ s.offDiag.inf' hs (uncurry dist) = s.offDiag.inf' hs (uncurry dist)
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 Ψ')
A : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
⊢ ∃ Ψ, Isometry Ψ ∧ range Ψ = ↑A

Tactic:
exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩

Goal state after:
Module: Mathlib.Topology.NatEmbedding

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

Tactic:
suffices ∃ U : ℕ → Set X, (∀ n, (U n).Nonempty ∧ IsOpen (U n) ∧ (U n)ᶜ ∈ 𝓝 x) ∧
        Pairwise (Disjoint on U) by
      rcases this with ⟨U, hU, hd⟩
      exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen[inst✝²] s
⊢ IsUpperSet (f ⁻¹' s)

Tactic:
exact (IsUpper.isUpperSet_of_isOpen hs).preimage hf

Goal state after: