mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
⊢ FriendlyOperation op

Tactic:
apply FriendlyOperation.coind motive'

Goal state after:
case h_base
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
⊢ motive' op

case h_step
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
⊢ ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive' op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
⊢ FriendlyOperation op

Tactic:
apply FriendlyOperation.coind motive'

Goal state after:
case h_base
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
⊢ motive' op

case h_step
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop := ⋯
⊢ ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive' op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, op') => (hd, ↑op' s.tail))
              (T s.head)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
basis : Basis
h_basis : WellFormedBasis basis
exps_hd : ℝ
exps_tl : List ℝ
h_length : (exps_hd :: exps_tl).length = List.length basis
h_firstIsPos : FirstNonzeroIsPos (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) basis) atTop atTop

Tactic:
| cons exps_hd exps_tl =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
basis : Basis
h_basis : WellFormedBasis basis
exps_hd : ℝ
exps_tl : List ℝ
h_length : (exps_hd :: exps_tl).length = List.length basis
h_firstIsNeg : FirstNonzeroIsNeg (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) basis) atTop (𝓝 0)

Tactic:
| cons exps_hd exps_tl =>

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
basis : Basis
exps_hd : ℝ
exps_tl : List ℝ
h_allZero : AllZero (exps_hd :: exps_tl)
⊢ Tendsto (toFun (exps_hd :: exps_tl) basis) atTop (𝓝 1)

Tactic:
| cons exps_hd exps_tl =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
⊢ IsSuccLimit (ω ^ a'.repr * ω) ∧
    (∀ (i : ℕ),
        0 < ω ^ a'.repr ∧
          ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω ∧ ((a.oadd 1 0).NF → (a'.oadd i.succPNat 0).NF)) ∧
      ∀ a < ω ^ a'.repr * ω, ∃ i, a < ω ^ a'.repr * ↑i + ω ^ a'.repr

Tactic:
refine
        ⟨isSuccLimit_mul_right this isSuccLimit_omega0, fun i =>
          ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega0'⟩

Goal state after:
case oadd.inl.none.inl.some.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
e' : m.natPred = 0
this : 0 < ω ^ a'.repr
i : ℕ
⊢ ω ^ a'.repr * ↑i + ω ^ a'.repr < ω ^ a'.repr * ω
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_1
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

Tactic:
exact Nat.mod_lt _ (Nat.le_of_ble_eq_true hn)

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ a ∈ (withDefault A y).zeroDefaultSupp ↔ (withDefault A y).zeroDefault.apply a ≠ 0

Tactic:
simp only [zeroDefaultSupp, List.mem_map, List.mem_filter, exists_and_right,
      List.mem_toFinset, exists_eq_right, Sigma.exists, Ne, zeroDefault]

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y : β
⊢ (∃ x, ⟨a, x⟩ ∈ A.dedupKeys ∧ (decide ¬x = 0) = true) ↔ ¬(withDefault A 0).apply a = 0
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.zero
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

Tactic:
simp only [length_cons, lt_add_iff_pos_left, add_pos_iff, Nat.lt_add_one, or_true,
        getElem?_eq_getElem, getElem_cons_zero, Option.some.injEq] at h₂
      subst h₂
      cases ys
      · cases h₁
      · simp

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩

Goal state after:
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ (U ∩ Set.range (etaFn G)).Nonempty
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case F_eqcont
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ ∀ K ∈ {K | IsCompact K}, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

Tactic:
· exact fun K _ ↦ hS2.equicontinuousOn K

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen[inst✝] s
⊢ BaireMeasurableSet s

Tactic:
borelize α
  exact h.measurableSet.baireMeasurableSet

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: case compl
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
ihs : ∃ u, IsOpen[inst✝²] u ∧ s =ᶠ[residual α] u
⊢ ∃ u, IsOpen[inst✝²] u ∧ sᶜ =ᶠ[residual α] u

Tactic:
| compl s _ ihs =>

Goal state after:
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ g ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
rw [IsGeneratedBy.equiv_symm_comp_continuous_iff,
    WithGeneratedByTopology.continuous_from_iff]
  rfl

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

Goal state before:
pp: case a.sr.hi
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm' : ∀ m_1 ≤ m, ↑m_1 < n → ∀ (j : cell C m_1), cellFrontier m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
hm : ↑(m + 1) < n
j : cell C (m + 1)
⊢ cellFrontier (m + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
obtain ⟨I, hI⟩ := cellFrontier_subset_base_union_finite_closedCell (m + 1) j
        apply hI.trans
        apply union_subset subset_union_left
        apply iUnion₂_subset fun l hl ↦ iUnion₂_subset fun i _ ↦ ?_
        rw [← cellFrontier_union_openCell_eq_closedCell]
        apply union_subset
        · exact (hm' l (Nat.le_of_lt_succ hl) ((ENat.natCast_lt_natCast.2 hl).trans hm) i)
        · apply subset_union_of_subset_right
          exact subset_iUnion₂_of_subset l ((ENat.natCast_lt_natCast.2 hl).trans hm) <|
            subset_iUnion _ i

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

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ Submodule.span ℤ (eval {fun x ↦ false} '' {nil}) = ⊤

Tactic:
rw [Set.image_singleton, eq_top_iff]
  intro f _
  rw [Submodule.mem_span_singleton]
  refine ⟨f default, ?_⟩
  simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]
  ext x
  obtain rfl : x = default := by simp only [Set.default_coe_singleton, eq_iff_true_of_subsingleton]
  rfl

Goal state after:
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}
⊢ LinearIndependent ℤ (eval (π C fun x ↦ ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p

Tactic:
rw [GoodProducts.linearIndependent_iff_range,
    ← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]
  exact linearIndependent_equiv _

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 ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, openCell n j

Tactic:
exact union_subset_union_right _ (iUnion_mono fun _ ↦ iUnion_mono' fun j ↦ ⟨j, subset_rfl⟩)

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
⊢ ⋂ y, ⋂ (_ : y ≤ n), C y ⊆ ∅

Tactic:
exact le_trans (fun x ↦ by simp; grind) g

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

Goal state before:
pp: case 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✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ∀ (i : ConnectedComponents Y), IsClopen (f ⁻¹' mk ⁻¹' {i})

Tactic:
exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε

Tactic:
have : ∀ x : α, ∃ U, x ∈ U ∧ IsOpen U ∧
      ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂ := fun x =>
    let ⟨U, nhdsU, hU⟩ := H x _ ε₂0
    let ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU
    ⟨V, xV, openV, fun y hy z hz f hf => hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
this : ∀ (x : α), ∃ U, x ∈ U ∧ IsOpen U ∧ ∀ y ∈ U, ∀ z ∈ U, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_1
ι : 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
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
l : E
φ : ℕ → ℕ
hφ : StrictMono φ
⊢ ¬Tendsto ((fun i ↦ x (i + (k + 1))) ∘ φ) atTop (𝓝 l)

pp: case refine_2
ι : 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
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ x '' Ici (k + 1) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}

Tactic:
· exact hx l _ ((strictMono_id.add_const _).comp hφ)

Goal state after:
case refine_2
ι : 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
x : ℕ → E
hx : ∀ (x_1 : E) (x_2 : ℕ → ℕ), StrictMono x_2 → ¬Tendsto (x ∘ x_2) atTop (𝓝 x_1)
A : Set E := ⋃ i, closure[inst✝³] {x i}
this✝ : IsCountablyCompact A
a : E
ha : a ∈ A ∧ MapClusterPt a atTop x
k : ℕ
hk : ∀ n > k, a ∉ closure[inst✝³] {x n}
this : a ∉ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
⊢ x '' Ici (k + 1) ⊆ ⋃ i, closure[inst✝³] {x (i + (k + 1))}
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: 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
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ MapsTo (⇑f) (⋃₀ (L '' ↑s)) (⋃₀ t)

Tactic:
rw [mapsTo_sUnion, forall_mem_image]

Goal state after:
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
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x y : Option α
xy : edist x y = 0
⊢ x = y

Tactic:
by
      rw [congr(@edist _ $h_edist x y)] at xy
      cases x <;> cases y
      · rfl
      · simp at xy
      · simp at xy
      rw [m.eq_of_edist_eq_zero xy]

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

Goal state before:
pp: case h
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
h : a 0 ≠ 1
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑(a 0) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑(a 0) + ofDigits fun i ↦ a (i + 1)

Tactic:
generalize a 0 = x at h

Goal state after:
case h
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
x : Fin 3
h : x ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑x + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑x + ofDigits fun i ↦ a (i + 1)
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:
rw [tendsto_cons_iff]
    dsimp [eraseIdx]
    exact tendsto_fst.cons ((@tendsto_eraseIdx n l).comp tendsto_snd)

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.16
x : X
inst✝ : IsEmpty N
⊢ ∀ (a₁ a₂ : ↑(Ω^ N X x)),
    (Homotopic.setoid N x) a₁ a₂ ↔
      (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)

Tactic:
intro a₁

Goal state after:
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x✝ : X
inst✝¹ : DecidableEq N✝
N : Type ?u.16
x : X
inst✝ : IsEmpty N
a₁ : ↑(Ω^ N X x)
⊢ ∀ (a₂ : ↑(Ω^ N X x)),
    (Homotopic.setoid N x) a₁ a₂ ↔
      (pathSetoid X) ((genLoopHomeoOfIsEmpty N x).toEquiv a₁) ((genLoopHomeoOfIsEmpty N x).toEquiv a₂)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inl.inl
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a : ℝ≥0∞
n : ℕ
J : Finset T
hJ_card : ↑(#J) ≤ a ^ n
c : ℝ≥0∞
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha1 : a ≤ 1
hJ : IsEmpty ↥J
⊢ ∃ K ⊆ J ×ˢ J,
    ↑(#K) ≤ a * ↑(#J) ∧
      (∀ (s t : T), (s, t) ∈ K → edist s t ≤ ↑n * c) ∧
        ∀ (f : T → E), ⨆ s, ⨆ t, edist (f ↑s) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
simp only [Finset.isEmpty_coe_sort] at hJ
      simp [hJ]

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

Goal state before:
pp: case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ Quotient.mk'
      ((loopHomeo i).symm
        (((loopHomeo i).toEquiv ((loopHomeo j).symm (((loopHomeo j).toEquiv d).trans ((loopHomeo j).toEquiv c)))).trans
          ((loopHomeo i).toEquiv ((loopHomeo j).symm (((loopHomeo j).toEquiv b).trans ((loopHomeo j).toEquiv a)))))) =
    Quot.mk (⇑(Homotopic.setoid N x)) a * Quot.mk (⇑(Homotopic.setoid N x)) c *
      (Quot.mk (⇑(Homotopic.setoid N x)) b * Quot.mk (⇑(Homotopic.setoid N x)) d)

Tactic:
apply congr_arg Quotient.mk'

Goal state after:
case neg.mk.mk.mk.mk
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
a✝ : HomotopyGroup N X x
a : ↑(Ω^ N X x)
b✝ : HomotopyGroup N X x
b : ↑(Ω^ N X x)
c✝ : HomotopyGroup N X x
c : ↑(Ω^ N X x)
d✝ : HomotopyGroup N X x
d : ↑(Ω^ N X x)
⊢ (loopHomeo i).symm
      (((loopHomeo i).toEquiv ((loopHomeo j).symm (((loopHomeo j).toEquiv d).trans ((loopHomeo j).toEquiv c)))).trans
        ((loopHomeo i).toEquiv ((loopHomeo j).symm (((loopHomeo j).toEquiv b).trans ((loopHomeo j).toEquiv a))))) =
    (loopHomeo j).symm
      (((loopHomeo j).toEquiv ((loopHomeo i).symm (((loopHomeo i).toEquiv d).trans ((loopHomeo i).toEquiv b)))).trans
        ((loopHomeo j).toEquiv ((loopHomeo i).symm (((loopHomeo i).toEquiv c).trans ((loopHomeo i).toEquiv a)))))