mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ D ⊆ C

Tactic:
by
  simp_rw [← union]
  exact subset_union_left

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

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : (iso_map C J) a = (iso_map C J) b
i : I
⊢ ↑a i = ↑b i

Tactic:
Subtype.ext_iff

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
⊢ ↑a i = ↑b i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : (i : I) → (fun i ↦ Bool) i
hy : y ∈ C
⊢ (fun i ↦ if hi : J i then ↑⟨(precomp Subtype.val) y, ⋯⟩ ⟨i, hi⟩ else false) ∈ π C J

Tactic:
exact ⟨y, hy, rfl⟩

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

Goal state before:
pp: case neg.h₁.cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs

Tactic:
rw [List.isChain_cons_cons] at ha

Goal state after:
case neg.h₁.cons
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
a : I
c : Products I →₀ ℤ
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
m : Products I
hm : c m ≠ 0
b : I
bs : List I
ha : a > b ∧ List.IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hc : ↑c.support ⊆ {m | ↑m ≤ b :: bs}
hmas : ↑m ≤ b :: bs
⊢ b :: bs < a :: b :: bs
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
⊢ range C = ⋃ e, smaller C ↑e

Tactic:
ext p

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ p ∈ range C ↔ p ∈ ⋃ e, smaller C ↑e
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp : ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p

Tactic:
obtain ⟨l, hl, rfl⟩ := hp
    rw [contained_eq_proj C o hsC, Products.limitOrdinal C ho] at hl
    obtain ⟨o', ho'⟩ := hl
    refine ⟨o', ho'.1, eval (π C (ord I · < o')) ⟨l, ho'.2⟩, ⟨l, ho'.2, rfl⟩, ?_⟩
    exact Products.eval_πs C (Products.prop_of_isGood C _ ho'.2)

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ⊆ ↑E

Tactic:
by
  simp_rw [← union]
  exact subset_union_left

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
l : ℕ
lltm : ↑l < m
xmeml : ∃ i, x ∈ closedCell l i
⊢ ∃ i, ↑i < n ∧ ∃ i_1, x ∈ closedCell i i_1

Tactic:
exact ⟨l, lt_of_lt_of_le lltm h, xmeml⟩

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ ⋃ i, ↑(skeletonLT C ↑i)

Tactic:
← union_iUnion_openCell_eq_complex,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ D ∪ ⋃ n, ⋃ j, openCell n j ⊆ ⋃ i, ↑(skeletonLT C ↑i)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ C ⊆ ⋃ i, ↑(skeleton C ↑i)

Tactic:
← union_iUnion_openCell_eq_complex,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ D ∪ ⋃ n, ⋃ j, openCell n j ⊆ ⋃ i, ↑(skeleton C ↑i)
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
i : I
hi : 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

Tactic:
exfalso

Goal state after:
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
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ False
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
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 ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ 0 = 1

Tactic:
exfalso

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 ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ False
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}
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
⊢ (Linear_CC' C hsC ho) (eval C l) = eval (C' C ho) l.Tail

Tactic:
by
  have hlc : ((term I ho) :: l.Tail.val).IsChain (· > ·) := by
    rw [← max_eq_o_cons_tail ho l hl hlh]; exact l.prop
  rw [max_eq_o_cons_tail' ho l hl hlh hlc, Products.evalCons]
  ext x
  simp only [Linear_CC', Linear_CC'₁, LocallyConstant.comapₗ, Linear_CC'₀, Subtype.coe_eta,
    LinearMap.sub_apply, LinearMap.coe_mk, AddHom.coe_mk, LocallyConstant.sub_apply,
    LocallyConstant.coe_comap, LocallyConstant.coe_mul, ContinuousMap.coe_mk, Function.comp_apply,
    Pi.mul_apply]
  rw [CC'₁, CC'₀, Products.eval_eq, Products.eval_eq, Products.eval_eq]
  simp only [mul_ite, mul_one, mul_zero]
  have hi' : ∀ i, i ∈ l.Tail.val → (x.val i = SwapTrue o x.val i) := by
    intro i hi
    simp only [SwapTrue, @eq_comm _ (x.val i), ite_eq_right_iff, ord_term ho]
    rintro rfl
    exact ((List.IsChain.rel_cons hlc hi).ne rfl).elim
  have H : (∀ i, i ∈ l.Tail.val → (x.val i = true)) =
      (∀ i, i ∈ l.Tail.val → (SwapTrue o x.val i = true)) := by
    apply forall_congr; intro i; apply forall_congr; intro hi; rw [hi' i hi]
  simp only [H]
  split_ifs with h₁ h₂ h₃ <;> try (dsimp [e])
  · rw [if_pos (swapTrue_eq_true _ _), if_neg]
    · rfl
    · simp [mem_C'_eq_false C ho x x.prop]
  · push Not at h₂; obtain ⟨i, hi⟩ := h₂; exfalso; rw [hi' i hi.1] at hi; exact hi.2 (h₁ i hi.1)
  · 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:
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
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {mk y}))

Tactic:
rw [connectedComponents_preimage_singleton]

Goal state after:
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
y : Y
this : ConnectedSpace ↑(connectedComponent y)
⊢ Finite (ConnectedComponents ↑(f ⁻¹' connectedComponent y))
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : tsupport ⇑f = ∅
⊢ f = 0

Tactic:
tsupport_eq_empty_iff,

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ⇑f = 0
⊢ f = 0
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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : MaxToGood C hC hsC ho h₁ m = MaxToGood C hC hsC ho h₁ n
⊢ ↑↑m = ↑↑n

Tactic:
Subtype.ext_iff

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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : ↑(MaxToGood C hC hsC ho h₁ m) = ↑(MaxToGood C hC hsC ho h₁ n)
⊢ ↑↑m = ↑↑n
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f) (Subtype.val '' (K U) n) V

Tactic:
rw [mapsTo_image_iff]

Goal state after:
case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f ∘ Subtype.val) ((K U) n) V
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
⊢ x ∈ s → ∃ ε > 0, Metric.eball x ε ⊆ s

Tactic:
xs

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : x ∈ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
h : ∀ (x : X), (↑f).IsConstant
⊢ IsLocallyConstant f

Tactic:
by
  intro s
  rw [isOpen_iff_mem_nhds]
  intro a ha
  obtain ⟨b, hb⟩ := h a
  apply mem_of_superset hb
  intro x hx
  have : f x = f a := (mem_of_mem_nhds hb) ▸ hx
  rw [mem_preimage, this]
  exact ha

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

Goal state before:
pp: case inr
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this : ∀ (s : Set ℚ), IsPreconnected s → ∀ x ∈ s, ∀ y ∈ s, x ≠ y → x < y → False
hlt : ¬x < y
⊢ False

pp: s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False

Tactic:
· apply this s hs y hy x hx H.symm <| H.lt_or_gt.resolve_left hlt

Goal state after:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False

Tactic:
rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩

Goal state after:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : ↑x < z
hzy : z < ↑y
⊢ False
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
j : ↑S
⊢ reorderRestrictProd S s p ↑j = p.2 j

Tactic:
by
  have hj : ↑j ∈ S := j.prop
  simp [reorderRestrictProd, hj]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) (r (a :: l))

Tactic:
tendsto_cons_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
a : α
l : List α
⊢ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
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 : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ Cube.boundary N,
      {
            toFun := fun x_2 ↦
              { toContinuousMap := homotopyFrom i H, map_zero_left := ?refine_1, map_one_left := ?refine_2 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        ↑p x_1

Tactic:
rintro t y ⟨j, jH⟩
    erw [homotopyFrom_apply]
    obtain rfl | h := eq_or_ne j i
    · simp only [Prod.map_apply, id_eq, funSplitAt_apply, Function.uncurry_apply_pair]
      rw [H.eq_fst]
      exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]
    · rw [p.2 _ ⟨j, jH⟩]; apply boundary; exact ⟨⟨j, h⟩, jH⟩

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun x ↦ x.eraseIdx 0) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
tendsto_cons_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun x ↦ x.eraseIdx (n + 1)) (𝓝 (a :: l)) (𝓝 ((a :: l).eraseIdx (n + 1)))

Tactic:
tendsto_cons_iff

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
a : α
l : List α
⊢ Tendsto (fun p ↦ (p.1 :: p.2).eraseIdx (n + 1)) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx (n + 1)))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ ContinuousAt (fun p ↦ insertIdx p.1 i p.2) (a, l)

Tactic:
by
    rw [ContinuousAt, nhds_prod_eq]; exact tendsto_insertIdx

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✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
⊢ (fun p ↦ ⟨{ toFun := fun c ↦ p (c default), continuous_toFun := ⋯ }, ⋯⟩)
      ((fun p ↦ { toFun := fun t ↦ p fun x ↦ t, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }) p) =
    p

Tactic:
by ext y; exact congr_arg p (eq_const_of_unique y).symm

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
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦symmAt i p⟧

Tactic:
by
  rw [symmAt_indep (Classical.arbitrary N) p, ← fromLoop_symm_toLoop]
  apply Quotient.sound
  rfl

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✝
N : Type ?u.15
inst✝ : Unique N
a b : HomotopyGroup N X x
p q : ↑(Ω^ N X x)
⊢ (homotopyGroupEquivFundamentalGroupOfUnique N).toFun (⟦p⟧ * ⟦q⟧) =
    (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦p⟧ * (homotopyGroupEquivFundamentalGroupOfUnique N).toFun ⟦q⟧

Tactic:
simp only [HomotopyGroup.mul_spec (i := default)]
    apply Quotient.sound
    simp [genLoopEquivOfUnique_transAt]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
hX : IsEmpty X
⊢ eHolderNorm r f = 0

Tactic:
by
  rw [eHolderNorm, ← ENNReal.bot_eq_zero, iInf₂_eq_bot]
  exact fun ε hε => ⟨0, .of_isEmpty, hε⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x y : α
⊢ ∀ x_1 ∈ {x, y}, ∀ y_1 ∈ {x, y}, x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1

Tactic:
mem_insert_iff,

Goal state after:
α : Type u_1
inst✝ : EDist α
x y : α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 ∈ {y} →
      ∀ (y_1 : α), y_1 = x ∨ y_1 ∈ {y} → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
⊢ s.infsep = if s.Nontrivial then ⨅ d, uncurry dist ↑d else 0

Tactic:
split_ifs with hs
  · have hb : BddBelow (uncurry dist '' s.offDiag) := by
      refine ⟨0, fun d h => ?_⟩
      simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
      rcases h with ⟨_, _, _, rfl⟩
      exact dist_nonneg
    refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
  · exact (not_nontrivial_iff.mp hs).infsep_zero

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

Goal state before:
pp: case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ edist x✝¹ x✝ ^ α = ENNReal.ofReal (dist x✝¹ x✝ ^ α)

Tactic:
← ENNReal.ofReal_rpow_of_nonneg,

Goal state after:
case toSnowflaking.toSnowflaking
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ edist x✝¹ x✝ ^ α = ENNReal.ofReal (dist x✝¹ x✝) ^ α

case toSnowflaking.toSnowflaking.hx_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ dist x✝¹ x✝

case toSnowflaking.toSnowflaking.hp_nonneg
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x✝¹ x✝ : X
⊢ 0 ≤ α
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
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
⊢ F (x, y) ≤ diam (range Φ ∪ range Ψ)

Tactic:
have A : ∀ z : X ⊕ Y, f z ∈ range Φ ∪ range Ψ := by
                intro z
                cases z
                · apply mem_union_left; apply mem_range_self
                · apply mem_union_right; apply mem_range_self

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
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
A : ∀ (z : X ⊕ Y), f z ∈ range Φ ∪ range Ψ
⊢ F (x, y) ≤ diam (range Φ ∪ range Ψ)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ Continuous ⇑some

Tactic:
simp only [OrderTopology.continuous_iff, ofLex_toLex, Subtype.forall, Lex.forall, Prod.forall]
  refine fun x q ⟨hx₁, hx₂⟩ ↦ ⟨?_, ?_⟩
  · obtain hq | hq := le_or_gt 0 q
    · convert isOpen_Ioi (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := not_isSuccPrelimit_iff.1 <| mt hx₁ hq.not_ge
      convert isOpen_Ioi (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_right
  · obtain hq | hq := le_or_gt q 0
    · convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]
    · obtain ⟨y, hy⟩ := not_isPredPrelimit_iff.1 <| mt hx₂ hq.not_ge
      convert isOpen_Iio (a := y)
      ext
      simpa [some, Prod.Lex.lt_iff, hq, le_iff_lt_or_eq] using hy.le_iff_lt_left

Goal state after: