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

Goal state before:
pp: t : Monomial
basis : Basis
h_coef : t.coef = 0
⊢ t.toFun basis = 0

Tactic:
simp [toFun, h_coef]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ.inr
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
ih : ∀ {s t : Stream'.Seq α}, motive s t → dist s t ≤ 2⁻¹ ^ n
hd : α
u v : Stream'.Seq α
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * dist (op c u) (op c v) ≤ 2⁻¹ ^ (n + 1)

Tactic:
specialize ih h_next

Goal state after:
case succ.inr
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
hd : α
u v : Stream'.Seq α
ih : dist u v ≤ 2⁻¹ ^ n
c : γ
h_next : motive u v
base : motive (Seq.cons hd (op c u)) (Seq.cons hd (op c v))
⊢ 2⁻¹ * dist (op c u) (op c v) ≤ 2⁻¹ ^ (n + 1)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
⊢ (ms.replaceFun f).Approximates

Tactic:
apply Approximates.coind motive ⟨ms, f, by grind⟩

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop := ⋯
⊢ ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
Module: Mathlib.Tactic.NormNum.NatSqrt

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ (y * y + r).sqrt = y

Tactic:
← pow_two

Goal state after:
x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ (y ^ 2 + r).sqrt = y
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
nx : ℕ
h : IsInt x (Int.negOfNat nx)
⊢ √x = ↑0

Tactic:
simp [Real.sqrt_eq_zero', h.out]

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⟩ ∈ U
⊢ (U ∩ Set.range (etaFn G)).Nonempty

Tactic:
← hsv,

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⟩ ∈ Subtype.val ⁻¹' s
⊢ (U ∩ Set.range (etaFn G)).Nonempty
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE

Tactic:
tfae_have 1 → 3 := by
    rw [mem_closure_iff_clusterPt]
    exact (ClusterPt.mono · (le_principal_iff.2 range_mem_map))

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
tfae_1_to_3 : (MapClusterPt x atTop fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: M : Type u_1
inst✝³ : GroupWithZero M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousInv₀ M
inst✝ : T1Space M
x✝ : M
⊢ x✝ ∈ Set.range Units.val ↔ x✝ ∈ {0}ᶜ

Tactic:
simp only [Set.mem_range, Set.mem_compl_iff, Set.mem_singleton_iff]

Goal state after:
M : Type u_1
inst✝³ : GroupWithZero M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousInv₀ M
inst✝ : T1Space M
x✝ : M
⊢ (∃ y, ↑y = x✝) ↔ ¬x✝ = 0
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y
⊢ ∃ x, cellFrontier 1 e = closedCell 0 x

Tactic:
simp only [closedCell_zero_eq_singleton, union_singleton] at hxy

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
h : (cellFrontier 1 e).Subsingleton
x y : cell C 0
hxy : cellFrontier 1 e = {↑(map 0 y) ![], ↑(map 0 x) ![]}
⊢ ∃ x, cellFrontier 1 e = closedCell 0 x
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) ↑E

Tactic:
simp_rw [← union, disjoint_union_right, disjoint_iUnion_right]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : cell C n
h : i ∉ E.I n
⊢ Disjoint (openCell n i) D ∧ ∀ (i_1 : ℕ) (i_2 : ↑(E.I i_1)), Disjoint (openCell n i) (openCell i_1 ↑i_2)
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : Order.IsSuccLimit a
⊢ sᵈ[a] = ⋂ b, sᵈ[↑b]

Tactic:
simpa [iteratedDerivedSet] using gfpApprox_of_isSuccLimit relDerivedSet ha

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 < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
⊢ x ∈ D ∨ ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1

Tactic:
Decidable.or_iff_not_imp_left

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 < n, ∃ i_1 ∈ J i, x ∈ openCell i i_1
⊢ x ∉ D → ∃ i < n, ∃ i_1 ∈ E.I i, i_1 ∈ J i ∧ x ∈ (fun a ↦ ↑(map i i_1) a) '' closedBall 0 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
⊢ (AA ∩ basic S).Nonempty

Tactic:
rcases claim2 _ hS with ⟨G, hG, hG2⟩

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
S : Set X.A
hS : S ∈ F
G : Ultrafilter X.A
hG : G ∈ basic S
hG2 : X.str G = x
⊢ (AA ∩ basic S).Nonempty
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ¬∀ i ∈ ↑l, ↑x i = true
⊢ (List.map (⇑(LocallyConstant.evalMonoidHom x)) (List.map (e C) ↑l)).prod = 0

Tactic:
simp only [List.map_map, List.prod_eq_zero_iff, List.mem_map, Function.comp_apply]
    push Not at h
    convert! h with i
    dsimp [LocallyConstant.evalMonoidHom, e]
    simp only [ite_eq_right_iff, one_ne_zero]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x ↦ x ∈ s, continuous_toFun := ⋯ } g

Tactic:
obtain ⟨J, g, h⟩ := @Profinite.exists_locallyConstant (Finset I)ᵒᵖ _ _ _
    (spanCone hC.isCompact) ℤ
    (spanCone_isLimit hC.isCompact) f

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
hC : IsClosed C
f : LocallyConstant ↑C ℤ
J : (Finset I)ᵒᵖ
g : LocallyConstant ↑((spanFunctor ⋯).obj J).toTop ℤ
h : f = LocallyConstant.comap (TopCat.Hom.hom ((spanCone ⋯).π.app J).hom) g
⊢ ∃ s g, f = LocallyConstant.comap { toFun := ProjRestrict C fun x ↦ x ∈ s, continuous_toFun := ⋯ } g
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
⊢ Finite (ConnectedComponents X)

Tactic:
by
  suffices h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents (f ⁻¹' mk ⁻¹' {y})) by
    refine .of_equiv _ (equivOfIsClopen (U := fun y ↦ f ⁻¹' mk ⁻¹' {y}) ?_ ?_ ?_).symm
    · exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)
    · exact fun i j hij ↦ (Disjoint.preimage mk (by simpa)).preimage f
    · rw [Set.iUnion_eq_univ_iff]
      exact fun x ↦ ⟨mk (f x), rfl⟩
  intro y
  obtain ⟨y, rfl⟩ := surjective_coe y
  have := isConnected_iff_connectedSpace.mp (isConnected_connectedComponent (x := y))
  rw [connectedComponents_preimage_singleton]
  refine IsOpenMap.finite_connectedComponents_of_finite_preimage_singleton_of_connectedSpace
    (hf₁.restrictPreimage (connectedComponent y)) (hf₂.restrictPreimage (connectedComponent y))
    (y := ⟨y, mem_connectedComponent⟩) ?_
  rw [← Set.finite_image_iff Subtype.val_injective.injOn]
  convert! h y
  aesop (add safe mem_connectedComponent)

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

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
⊢ ∃ a ∈ A, AccPt a (𝓟 B)

Tactic:
let x : ℕ → E := (↑) ∘ f

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
x : ℕ → E := Subtype.val ∘ ⇑f
⊢ ∃ a ∈ A, AccPt a (𝓟 B)
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : {x_1 | x x_1 ∈ A} ∈ cofinite
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite

Tactic:
mem_cofinite,

Goal state after:
E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : {x_1 | x x_1 ∈ A}ᶜ.Finite
hfin : (range x).Infinite
⊢ (range x ∩ A).Infinite
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case a
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
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Tactic:
have hsub : (⋂ L ∈ s, {g : C(X, Y) | MapsTo g L (⋃₀ t)}) ⊆ {g | MapsTo g K U} := by
      simp only [← ofPred_forall, ← mapsTo_iUnion, ← sUnion_eq_biUnion]
      exact fun g hg ↦ hg.mono hKs (sUnion_subset hTU)

Goal state after:
case a
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
s : Set (Set X)
hsS : s ⊆ S
hsf : s.Finite
hKs : K ⊆ ⋃₀ s
hst : MapsTo (⇑f) (⋃₀ s) (⋃₀ t)
hsub : ⋂ L ∈ s, {g | MapsTo (⇑g) L (⋃₀ t)} ⊆ {g | MapsTo (⇑g) K U}
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Tactic:
by
  simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
    le_principal_iff, ← ofPred_forall, ← Filter.le_def]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ s ∈ 𝓝 l ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
Filter.mem_nhds_iff

Goal state after:
α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ (∃ t ∈ l, Iic (𝓟 t) ⊆ s) ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
hf : ∀ᶠ (y : X) in 𝓝 x, P y ↑f
y : X
hy : P y ↑f
hy' : ∀ᶠ (x : X) in 𝓝 y, f x = f' x
⊢ P y ↑f'

Tactic:
rwa [Germ.coe_eq.mpr (EventuallyEq.symm hy')]

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

Goal state before:
pp: G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : IsTopologicalGroup G'
⊢ hSpace (G × G') = HSpace.prod G G'

Tactic:
by
  simp only [HSpace.prod]
  rfl

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

Goal state before:
pp: ⊢ ¬FirstCountableTopology ℚ∞

Tactic:
by
  intro
  exact not_countably_generated_nhds_infty_opc inferInstance

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

Goal state before:
pp: ⊢ ¬SecondCountableTopology ℚ∞

Tactic:
intro
  exact not_firstCountableTopology_opc inferInstance

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

Goal state before:
pp: case hf
⊢ Function.Bijective fun x ↦ x / 3

Tactic:
exact mulRight_bijective₀ 3⁻¹ (by simp)

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
rw [this, Filter.tendsto_map'_iff]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
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 j : N
⊢ auxGroup i = auxGroup j

Tactic:
by_cases h : i = j

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i = j
⊢ auxGroup i = auxGroup j

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : ¬i = j
⊢ auxGroup i = auxGroup j
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : EDist X
x y : Snowflaking X α hα₀ hα₁
⊢ edist (ofSnowflaking x) (ofSnowflaking y) = edist x y ^ α⁻¹

Tactic:
rw [edist_def, ENNReal.rpow_rpow_inv hα₀.ne']

Goal state after:
Module: Mathlib.Topology.NatEmbedding

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

Tactic:
rcases this with ⟨U, hU, hd⟩
      exact ⟨U, fun n ↦ (hU n).1, fun n ↦ (hU n).2.1, hd⟩

Goal state after:
Module: Mathlib.Topology.NatEmbedding

Goal state before:
pp: case neg.refine_3
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
x : X
hx : (𝓝[≠] x).NeBot
this✝ : Std.Symm Disjoint
S : Finset (Set X)
hS : ∀ x_1 ∈ S, x_1.Nonempty ∧ IsOpen[inst✝²] x_1 ∧ x_1ᶜ ∈ 𝓝 x
this : (⋂ U ∈ S, interior Uᶜ) \ {x} ∈ 𝓝[≠] x
y : X
hyU : y ∈ ⋂ U ∈ S, interior Uᶜ
hyx : y ≠ x
V W : Set X
hVo : IsOpen[inst✝²] V
hWo : IsOpen[inst✝²] W
hyV : y ∈ V
hxW : x ∈ W
hVW : Disjoint V W
U : Set X
hU : U ∈ S
⊢ Disjoint U (V ∩ ⋂ U ∈ S, interior Uᶜ)

Tactic:
exact disjoint_left.2 fun z hzU ⟨_, hzU'⟩ ↦ interior_subset (mem_iInter₂.1 hzU' U hU) hzU

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

Goal state before:
pp: case mpr.inl
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] univ

Tactic:
exact isOpen_univ

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : IsPredPrelimit x
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

Tactic:
obtain ⟨z, hz, hz'⟩ := hx.lt_iff_exists_lt.1 h

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : IsPredPrelimit x
z : α
hz : x < z
hz' : z < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩
Module: Mathlib.Topology.Partial

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst✝] s
⊢ ∀ x ∈ f.preimage s, 𝓝 x ≤ 𝓟 (f.preimage s)

Tactic:
rintro x ⟨y, ys, fxy⟩ t

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen[inst✝] s
x : X
y : Y
ys : y ∈ s
fxy : (x, y) ∈ f.graph'
t : Set X
⊢ t ∈ 𝓟 (f.preimage s) → t ∈ 𝓝 x
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case h₂
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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ ∀ b ∈ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = toGHSpace X} ×ˢ {b | ⟦b⟧ = toGHSpace Y},
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ b

Tactic:
· rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩
      exact B p q hp hq

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

Goal state before:
pp: case refine_1.h₁
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ BddBelow ((fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x})

pp: case h₂
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 0 ∈ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x}

Tactic:
· exact ⟨0, by rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg⟩

Goal state after:
case h₂
x : GHSpace
y : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 0 ∈ (fun p ↦ hausdorffDist ↑p.1 ↑p.2) '' {a | ⟦a⟧ = x} ×ˢ {b | ⟦b⟧ = x}
Module: Mathlib.Topology.Separation.PerfectlyNormal

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (s : Set X), IsClosed[inst✝] s → ∃ f, s = ⇑f ⁻¹' {0} ∧ ∀ (x : X), f x ∈ Icc 0 1
s : Set X
hs : IsClosed[inst✝] s
⊢ IsGδ s

Tactic:
by
        by_cases! hse : s = ∅
        · simp_all
        -- pick `f` such that `s = f ⁻¹' {0} = ⋂ n, f ⁻¹' (Iio (1 / (n + 1)))`
        obtain ⟨f, hf, hfr⟩ := h s hs
        refine isGδ_iff_eq_iInter_nat.2 ⟨fun n => f ⁻¹' (Iio (1 / (n + 1))),
          fun n => ?_, ?_⟩
        · exact f.continuous.isOpen_preimage _ isOpen_Iio
        · simp only [hf, ← preimage_iInter,
            ← preimage_range_inter (s := ⋂ (n : ℕ), Iio (1 / (n + 1) : ℝ)), inter_iInter]
          congr
          rw [eq_comm, eq_singleton_iff_unique_mem]
          refine ⟨mem_iInter_of_mem fun n => ?_, fun x h => ?_⟩
          · exact ⟨(hf ▸ hse : (f ⁻¹' {0}).Nonempty), show 0 < (1 / (n + 1) : ℝ) by positivity⟩
          · apply le_antisymm
            · simp only [mem_iInter, mem_inter_iff, mem_Iio] at h
              exact ge_of_tendsto' tendsto_one_div_add_atTop_nhds_zero_nat (fun n => (h n).2.le)
            · rcases (mem_iInter.1 h 0).1 with ⟨x, rfl⟩
              exact (hfr x).1

Goal state after: