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

Goal state before:
pp: case h
α : 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'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
        (T s.head)
s : Stream'.Seq α
⊢ ((opf ∘ op) s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      ((fun hd? ↦
          match T hd? with
          | none =>
            Option.map
              (fun x ↦
                match x with
                | (hd, opf') => (hd, ⟨(fun x ↦ ↑opf' nil) ∘ op, ⋯⟩))
              (h_opf.unfold none)
          | some (hd, opf', op') =>
            Option.map
              (fun x ↦
                match x with
                | (hd', opf'') => (hd', ⟨(↑opf'' ∘ ↑opf') ∘ ↑op', ⋯⟩))
              (h_opf.unfold (some hd)))
        s.head)

Tactic:
specialize hT s

Goal state after:
case h
α : 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'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
hT :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
      (T s.head)
⊢ ((opf ∘ op) s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      ((fun hd? ↦
          match T hd? with
          | none =>
            Option.map
              (fun x ↦
                match x with
                | (hd, opf') => (hd, ⟨(fun x ↦ ↑opf' nil) ∘ op, ⋯⟩))
              (h_opf.unfold none)
          | some (hd, opf', op') =>
            Option.map
              (fun x ↦
                match x with
                | (hd', opf'') => (hd', ⟨(↑opf'' ∘ ↑opf') ∘ ↑op', ⋯⟩))
              (h_opf.unfold (some hd)))
        s.head)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i ↦ α)

Tactic:
refine le_antisymm (UniformSpace.comap_mono UniformFun.uniformContinuous_toFun) ?_

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (Pi.uniformSpace fun i ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed (Set.range toContinuousMap)

Tactic:
simp only [range_toContinuousMap, Set.ofPred_and, Set.ofPred_forall]

Goal state after:
A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed ({a | a 1 = 1} ∩ ⋂ i, ⋂ i_1, {x | x (i * i_1) = x i * x i_1})
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : EquicontinuousAt (fun f ↦ ⇑↑f) 1
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
replace h := equicontinuous_of_equicontinuousAt_one _ h

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
h : Equicontinuous (DFunLike.coe ∘ Subtype.val)
⊢ LocallyCompactSpace (X →ₜ* Y)
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ ⊓ 𝓟 V = 𝓕₂ ⊓ 𝓟 V
⊢ t₁ = t₂

Tactic:
replace H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V := by simpa [← H]

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
⊢ t₁ = t₂
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
⊢ ∀ {n : ℕ} {x : Circle}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)

Tactic:
intro n x h1 h2

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : x ∈ Vn n
h2 : x * x ∈ Vn n
⊢ x ∈ Vn (n + 1)
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
⊢ DiscreteTopology (PontryaginDual A)

Tactic:
let V : Set (PontryaginDual A) := {ψ | Set.MapsTo ψ Set.univ (Circle.centeredArc (π / 2))}
  have hVopen : IsOpen V := by
    dsimp only [V]
    exact isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo isCompact_univ
      (Circle.isOpen_centeredArc (π / 2)))
  have hVeq : V = ({1} : Set (PontryaginDual A)) := by
    ext ψ
    rw [Set.mem_singleton_iff]
    refine ⟨fun hψ ↦ ?_, ?_⟩
    · ext1 a
      refine Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two fun n hn ↦ ?_
      simpa using hψ (Set.mem_univ (a ^ n))
    · rintro rfl _ _
      rw [Circle.mem_centeredArc (by linarith [pi_pos])]
      simp [pi_pos]
  exact discreteTopology_of_isOpen_singleton_one (by simpa [hVeq] using hVopen)

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : v x < 1
⊢ Tendsto (fun n ↦ x ^ n) atTop (𝓝 0)

Tactic:
simp only [(hasBasis_nhds_zero _ _).tendsto_right_iff, mem_ofPred_eq, map_pow, eventually_atTop,
    forall_const]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : v x < 1
⊢ ∀ (i : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ a, ∀ (b : ℕ), a ≤ b → v.restrict x ^ b < ↑i
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ Preperfect s ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s

Tactic:
rw [preperfect_iff_eq_relDerivedSet, eq_comm,
    ← (gfpApprox_eq_all_of_fixedPoint relDerivedSet (relDerivedSet_subset))]
  simp [iteratedDerivedSet]

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∈ D ∨ ∃ i, ∃ (_ : i < n), ∃ i_1, ∃ (_ : i_1 ∈ J i), x ∈ openCell i i_1
⊢ x ∈ D ∨
    ∃ i,
      ∃ (_ : i < n),
        ∃ i_1,
          ∃ (h : i_1 ∈ E.I i) (_ : ⟨i_1, ⋯⟩ ∈ (J i).preimage Subtype.val ⋯),
            x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1

Tactic:
Finset.mem_preimage,

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
x : X
hx : x ∈ ↑(map n ↑i) '' sphere 0 1
hJ : x ∈ D ∨ ∃ i, ∃ (_ : i < n), ∃ i_1, ∃ (_ : i_1 ∈ J i), x ∈ openCell i i_1
⊢ x ∈ D ∨ ∃ i, ∃ (_ : i < n), ∃ i_1, ∃ (_ : i_1 ∈ E.I i) (_ : i_1 ∈ J i), x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1
Module: Mathlib.Topology.Category.Locale

Goal state before:
pp: X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : topToLocale.map (compHausToTop.map a₁✝) = topToLocale.map (compHausToTop.map a₂✝)
⊢ a₁✝ = a₂✝

Tactic:
exact ConcreteCategory.ext (Opens.comap_injective (congr_arg Frm.Hom.hom
      (Quiver.Hom.op_inj h)))

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

Goal state before:
pp: case true
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ true
hx : ↑x a = true
⊢ (LocallyConstant.evalMonoidHom y) (e (π C fun x ↦ x ∈ s) a) = 0

Tactic:
rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]

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

Goal state before:
pp: case a.tr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
m : ℕ
hm : ↑m < n
j : cell C m
⊢ openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ ↑m ≤ as

Tactic:
apply hc

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
hsm :
  ∀ (c : ℤ) (x : LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c • x = c • (e (π C fun x ↦ x ∈ s) a * x)
⊢ m ∈ ↑c.support
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)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

Tactic:
rcases a with ⟨_, y, hy, rfl⟩
      exact ⟨y, hy, rfl⟩

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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] A

Tactic:
rw [closed C A hAC]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)) ∧ IsClosed[t] (A ∩ D)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: 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
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
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
⊢ m ∈ ↑c.support

Tactic:
by simpa only [Finset.mem_coe, Finsupp.mem_support_iff] using hm

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 ∈ 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) ℤ
hn : ((πs C o) n + m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l
hn' : n ∈ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ False

Tactic:
rw [Finsupp.mem_span_range_iff_exists_finsupp] at hn'

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 ∈ 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) ℤ
hn : ((πs C o) n + m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) = Products.eval C ↑l
hn' : ∃ c, (c.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ False
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
⊢ ∃ a ∈ A, MapClusterPt a atTop x

Tactic:
by_contra! hac

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
hac : ∀ a ∈ A, ¬MapClusterPt a atTop x
⊢ False
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous fun x ↦ ⇑↑x

Tactic:
isUniformEmbedding_subtype_val.isUniformInducing.equicontinuous_iff

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous ((fun x ↦ Subtype.val ∘ x) ∘ fun x ↦ ⇑↑x)
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
x : α
⊢ 𝓝 (pure x) = 𝓟 {⊥, pure x}

Tactic:
rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
⊢ (delayReflRight 1 γ) t = γ t

Tactic:
exact congr_arg γ (qRight_one_right t)

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] (reorderRestrictProd S s)

Tactic:
refine continuous_pi fun j ↦ ?_

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ reorderRestrictProd S s a j
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 : ∀ (n : ℕ), a n ≠ 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:
specialize h 0

Goal state after:
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)
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : TopologicalSpace α
⊢ Tendsto length (pure []) (pure [].length)

pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
· exact tendsto_pure_pure _ _

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α) (a : α),
    Tendsto length (𝓝 l) (pure l.length) → Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (fromLoop i (Path.trans (toLoop i f) (toLoop i g))) x✝ =
    if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))

Tactic:
dsimp only [Path.trans, fromLoop, Path.coe_mk_mk, Function.comp_apply, mk_apply,
        ContinuousMap.comp_apply, ContinuousMap.coe_coe, funSplitAt_apply,
        ContinuousMap.uncurry_apply, ContinuousMap.coe_mk, Function.uncurry_apply_pair]

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (↑(if ↑(x✝ i) ≤ 1 / 2 then (Path.extend (toLoop i f)) (2 * ↑(x✝ i)) else (Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1))
      fun j ↦ x✝ ↑j) =
    if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
⊢ range g ⊆ A

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
⊢ C = f '' range g

Tactic:
· rwa [Set.range_subset_iff]

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
⊢ C = f '' range g
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
x : Snowflaking X α hα₀ hα₁
d : ℝ≥0∞
⊢ ⇑ofSnowflaking '' closedEBall x d = closedEBall (ofSnowflaking x) (d ^ α⁻¹)

Tactic:
by
  rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedEBall]

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case refine_1
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)
⊢ Nat.pair n i = Nat.pair n j

Tactic:
apply hd.eq

Goal state after:
case refine_1
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)
⊢ ¬(Disjoint on U) (Nat.pair n i) (Nat.pair n j)
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a b : α
⊢ a ⤳ b ↔ b ≤ a

Tactic:
simp only [specializes_iff_closure_subset, closure_singleton, Iic_subset_Iic]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rcases h.eq_or_lt with rfl | hlt

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)