mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
G : D ⥤ H
α : F ⟶ L ⋙ G
Y : D
⊢ ((L.pointwiseLeftKanExtension F).descOfIsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F) G α).app Y =
    colimit.desc (CostructuredArrow.proj L Y ⋙ F) (L.costructuredArrowMapCocone F G α Y)

Tactic:
by
  let β : L.pointwiseLeftKanExtension F ⟶ G :=
    { app := fun Y ↦ colimit.desc _ (costructuredArrowMapCocone L F G α Y) }
  have h : (pointwiseLeftKanExtension L F).descOfIsLeftKanExtension
      (pointwiseLeftKanExtensionUnit L F) G α = β := by
    apply hom_ext_of_isLeftKanExtension (α := pointwiseLeftKanExtensionUnit L F)
    aesop
  exact NatTrans.congr_app h Y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X

Tactic:
intro G
              apply asIso (prodComparison ((evaluation C D).obj k) F G)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
e : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left })) ≅ X :=
  CostructuredArrow.isoMk
    (Iso.refl (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left)
    ⋯
⊢ ((fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ })
          ((fun f ↦
              { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
                naturality := ⋯ })
            f)).app
      X =
    f.app X

Tactic:
simpa [e] using! f.naturality e.inv

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj X =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj zero =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj one =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
X : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      X =
    (𝟭 WalkingParallelPair).obj X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.zero =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.one =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj X = F.obj X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j ↦ F.map (line j)).obj X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j ↦ F.map (line j)).obj X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj X = F.obj X

Tactic:
cases X

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj zero = F.obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
⊢ (parallelFamily fun j ↦ F.map (line j)).obj one = F.obj one
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝ : HasFiniteLimits C
this : HasProductsOfShape (Subtype P) C
⊢ HasInitial C

Tactic:
have := fun A => hasProductsOfShape_of_small.{w} C (StructuredArrow A P.ι)

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝¹ : HasFiniteLimits C
this✝ : HasProductsOfShape (Subtype P) C
this : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
⊢ HasInitial C
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C✝ : Type u
F✝ : C✝ → Type v
C : Type u
F : C → Type v
c : Cofan F
hc : IsColimit c
i j : C
x : F i
y : F j
hij : i = j
⊢ F i = F j

Tactic:
by rw [hij]

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
hn : Odd n
⊢ n.negOnePow = -1

Tactic:
by
  obtain ⟨k, rfl⟩ := hn
  simp only [negOnePow_add, negOnePow_two_mul, negOnePow_one, mul_neg, mul_one]

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n₁ n₂ : ℤ
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
by
  by_cases h₂ : Even n₂
  · rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]
    tauto
  · rw [Int.not_even_iff_odd] at h₂
    rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]
    tauto

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ f (↑n * c) = 0

Tactic:
h.nat_mul_eq_of_eq_zero hi n

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
hi : f 0 = 0
n : ℕ
⊢ 0 = 0
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ (d * x).gcd (d * a) = d

Tactic:
rw [gcd_mul_left, ha2, mul_one]

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 = A ∩ (Q ∩ T2)

Tactic:
simp only [Set.inter_assoc]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)

Tactic:
have hn' : (n : ℚ) ≠ 0 := by simp [hn]

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
⊢ ↑(φ n) = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
by
  let d := a.gcd b
  rcases eq_zero_or_pos a with (rfl | ha0)
  · simp
  have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0
  apply le_of_mul_le_mul_right _ hd0
  grw [← totient_gcd_mul_totient_mul a b, mul_comm, d.totient_le]

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ φ a ∣ φ b

Tactic:
totient_eq_prod_factorization ha0,

Goal state after:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) ∣ φ b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ φ (2 * n) = φ n

Tactic:
totient_mul_of_prime_of_not_dvd prime_two hn.not_two_dvd_nat,

Goal state after:
n : ℕ
hn : Odd n
⊢ (2 - 1) * φ n = φ n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a : ℕ
ha : ¬a = 0
c : ℕ
h' : c = 1 ∨ c = 2
hb : ¬a * c = 0
this : a.Coprime c
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
obtain rfl | rfl := h'

Goal state after:
case inl
a : ℕ
ha : ¬a = 0
hb : ¬a * 1 = 0
this : a.Coprime 1
⊢ a = a * 1 ∨ 2 * a = a * 1

case inr
a : ℕ
ha : ¬a = 0
hb : ¬a * 2 = 0
this : a.Coprime 2
⊢ a = a * 2 ∨ 2 * a = a * 2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (p * a * d)

Tactic:
mul_comm p

Goal state after:
case neg
a : ℕ
ha : ¬a = 0
p : ℕ
hp : Prime p
hap : p ∣ a
d : ℕ
h' : φ a = φ (a * (p * d))
hb : ¬a * (p * d) = 0
⊢ φ a < φ (a * p * d)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * p) - k * p ^ (k - 1) - p ^ (k - 1)) =
    p ^ (p ^ (k - 1) * (p * k) - p ^ (k - 1) * k - p ^ (k - 1))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
by
  rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (-a) b = -(toIocDiv hp a (-b) + 1)

Tactic:
simpa only [neg_neg] using toIcoDiv_neg hp (-a) (-b)

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: case insert
X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ t ∈ s✝, IsOpen[inst✝] t) → IsOpen[inst✝] (⋂₀ s✝)
h : IsOpen[inst✝] a✝¹ ∧ ∀ x ∈ s✝, IsOpen[inst✝] x
⊢ IsOpen[inst✝] (a✝¹ ∩ ⋂₀ s✝)

Tactic:
exact h.1.inter (ih h.2)

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i ∈ f, ∃ x ∈ g i, id x ⊆ s) ↔ ∃ t ∈ f, s ∈ g t

Tactic:
by
    simp only [id, exists_mem_subset_iff]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ (map g f).lim = Classical.choice hX

Tactic:
lim,

Goal state after:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ (Classical.epsilon fun x ↦ map g f ≤ 𝓝 x) = Classical.choice hX
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
    rintro U ⟨t, ht, htU⟩ x hx
    have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
    exact htU this

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
wcovBy_iff_eq_or_covBy,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b ⋖ toIcoDiv hp a b
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
⊢ AccPt x (𝓟 C) ↔ ∃ᶠ (y : X) in 𝓝[≠] x, y ∈ C

Tactic:
rw [accPt_iff_frequently, this]

Goal state after:
X : Type u_3
inst✝ : TopologicalSpace X
x : X
C : Set X
this : (∃ᶠ (z : X) in 𝓝[≠] x, z ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
⊢ (∃ᶠ (y : X) in 𝓝 x, y ≠ x ∧ y ∈ C) ↔ ∃ᶠ (z : X) in 𝓝 x, z ∈ C ∧ z ∈ {x}ᶜ
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
h : (pure x ⊓ F.lift' closure[inst✝]).NeBot
U : Set X
hU : U ∈ F.lift' closure[inst✝]
⊢ U ∈ pure x

Tactic:
← forall_mem_nonempty_iff_neBot,

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
U : Set X
hU : U ∈ F.lift' closure[inst✝]
h : ∀ s ∈ pure x ⊓ F.lift' closure[inst✝], s.Nonempty
⊢ U ∈ pure x
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
x₁ x₂ x₃ : α ⧸ AddSubgroup.zmultiples p
h : btw x₁ x₂ x₃
⊢ btw x₂ x₃ x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on
    induction x₂ using QuotientAddGroup.induction_on
    induction x₃ using QuotientAddGroup.induction_on
    simp_rw [btw_coe_iff] at h ⊢
    apply toIxxMod_cyclic_left _ h

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝² z✝¹ z✝ : α
⊢ toIcoMod ⋯ z✝² z✝¹ ≤ toIocMod ⋯ z✝² z✝ ∨ toIcoMod ⋯ z✝ z✝¹ ≤ toIocMod ⋯ z✝ z✝²

Tactic:
apply toIxxMod_total

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
f : Filter X
s : Set X
⊢ 𝓝ˢ s ≤ f ↔ ∀ x ∈ s, 𝓝 x ≤ f

Tactic:
simp [nhdsSet]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝ˢ {x} = 𝓝 x

Tactic:
simp [nhdsSet]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
by rw [Set.inter_union_compl s t]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ x ∈ s

Tactic:
rw [nhds_discrete, mem_pure]

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ Tendsto (g ∘ f) (𝓝 x) (𝓝 ((g ∘ f) x)) ↔ Tendsto g (𝓝 (f x)) (𝓝 (g (f x)))

Tactic:
Filter.Tendsto,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : IsInducing f
x : X
h : range f ∈ 𝓝 (f x)
⊢ map (g ∘ f) (𝓝 x) ≤ 𝓝 ((g ∘ f) x) ↔ map g (𝓝 (f x)) ≤ 𝓝 (g (f x))
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ comap (⇑h) (𝓝 y) = 𝓝 (h.symm y)

Tactic:
rw [h.nhds_eq_comap, h.apply_symm_apply]

Goal state after:
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedMap f
p : X → Prop
y₀ : Y
H : ∀ᶠ (x : X) in comap f (𝓝 y₀), p x
⊢ ∀ᶠ (y : Y) in 𝓝 y₀, ∀ x ∈ f ⁻¹' {y}, p x

Tactic:
rwa [eventually_comap] at H

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
u : Set X
hu : u ∈ s
this : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u
⊢ TopologicalSpace.IsOpen (Prod.fst ⁻¹' u)

Tactic:
rw [← this]
            exact
              isOpen_iUnion fun v =>
                isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x} x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_singleton, tendsto_pure_nhds]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
⊢ ContinuousWithinAt f (s \ {x}) x

Tactic:
simp_all [ContinuousWithinAt, AccPt, ← nhdsWithin_inter', Set.sdiff_eq, Set.inter_comm]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : Continuous[inst✝¹, inst✝] f
⊢ ContinuousOn f s

Tactic:
by
  rw [← continuousOn_univ] at h
  exact h.mono (subset_univ _)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
subst hy; exact hg.comp_of_preimage_mem_nhdsWithin hf h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
⊢ SeparableSpace (α × β)

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s✝ : Set α
inst✝² : TopologicalSpace β
inst✝¹ : SeparableSpace α
inst✝ : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SeparableSpace (α × β)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
⊢ IsSeparable (closure[t] s) ↔ IsSeparable s

Tactic:
simp only [IsSeparable, isClosed_closure.closure_subset_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
⊢ IsOpen[generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}] ((↑i).pi t ∩ (↑i)ᶜ.pi c)

Tactic:
classical
    rw [← univ_pi_piecewise]
    refine GenerateOpen.basic _ ⟨_, fun a => ?_, rfl⟩
    by_cases a ∈ i <;> simp [*]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α

Tactic:
rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
  let := t.induced f
  refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
  rw [eq, induced_generateFrom_eq]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ s ∈ S, IsOpen[t] s
⊢ ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
by
  simpa only [and_left_comm, sUnion_eq_biUnion] using! isOpen_biUnion_countable S id H

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
⊢ IsCompact (f '' s)

Tactic:
intro l lne ls

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ x ∈ f '' s, ClusterPt x l