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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
have := hm (L.obj j)

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.coneOfIsRightKanExtension α c).π.app (L.obj j) = s.π.app (L.obj j)
⊢ m ≫ c.π.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T

Tactic:
rw [Category.assoc, Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ i ≫ h ≫ e ≫ i = i ≫ 𝟙 T
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {f : (forget₂ CommGrpCat CommMonCat).obj X ⟶ Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
        f =
      { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X ≫ CommMonCat.units.map f

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {g : X ⟶ CommMonCat.units.obj Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
            invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯,
            right_inv := ⋯ }.symm
        g =
      (forget₂ CommGrpCat CommMonCat).map g ≫
        { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y

Tactic:
intros; rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
I : Ideal ℤ
g : ↥I →ₗ[ℤ] A
⊢ ∃ g', ∀ (x : ℤ) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
by
  rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
  obtain rfl | h0 := eq_or_ne m 0
  · refine ⟨0, fun n hn ↦ ?_⟩
    rw [Submodule.span_zero_singleton] at hn
    subst hn
    exact (map_zero g).symm
  let gₘ := g ⟨m, Submodule.subset_span (Set.mem_singleton _)⟩
  refine ⟨LinearMap.toSpanSingleton ℤ A (DivisibleBy.div gₘ m), fun n hn ↦ ?_⟩
  rcases Submodule.mem_span_singleton.mp hn with ⟨n, rfl⟩
  rw [map_zsmul, LinearMap.toSpanSingleton_apply, DivisibleBy.div_cancel gₘ h0, ← map_zsmul g,
    SetLike.mk_smul_mk]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
⊢ Periodic l.prod c

Tactic:
by
  induction l with
  | nil => simp
  | cons g l ih =>
    rw [List.forall_mem_cons] at hl
    simpa only [List.prod_cons] using hl.1.mul (ih hl.2)

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
m : M
⊢ f m =
    ↑{ domain := i.range, toFun := { toFun := fun x ↦ f (Exists.choose ⋯), map_add' := ⋯, map_smul' := ⋯ } } ⟨i m, ⋯⟩

Tactic:
simp only [LinearPMap.mk_apply, LinearMap.coe_mk]

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
m : M
⊢ f m = { toFun := fun x ↦ f (Exists.choose ⋯), map_add' := ⋯ } ⟨i m, ⋯⟩
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (b ^ n) (b ^ (n + 1)))

Tactic:
by
  simpa only [one_mul] using pairwise_disjoint_Ioc_mul_zpow 1 b

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r ∈ ideal i f y

Tactic:
change (r • y) ∈ (extensionOfMax i f).toLinearPMap.domain

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
eq1 : r • y = 0
⊢ r • y ∈ (extensionOfMax i f).domain
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: case inr
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
this : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ}, p m → p n → count p m = count p n → m ≠ n → m < n → False
hmn : ¬m < n
⊢ False

Tactic:
exact this hn hm heq.symm h.symm (by grind)

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
⊢ (extensionOfMax i f).domain = ⊤

Tactic:
by
  refine Submodule.eq_top_iff'.mpr fun y => ?_
  rw [← extensionOfMax_is_max i f _ (extensionOfMax_le i f h), extensionOfMaxAdjoin,
    Submodule.mem_sup]
  exact ⟨0, Submodule.zero_mem _, y, Submodule.mem_span_singleton_self _, zero_add _⟩

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝³ : Ring R
Q : Type v
inst✝² : AddCommGroup Q
inst✝¹ : Module R Q
inst✝ : Small.{v, u} R
inj : Injective R Q
I : Ideal R
g : ↥I →ₗ[R] Q
eI : Shrink.{v, u} ↥I ≃ₗ[R] ↥I := Shrink.linearEquiv R ↥I
eR : Shrink.{v, u} R ≃ₗ[R] R := Shrink.linearEquiv R R
g' : Shrink.{v, u} R →ₗ[R] Q
hg' : ∀ (x : Shrink.{v, u} ↥I), g' ((↑eR.symm ∘ₗ Submodule.subtype I ∘ₗ ↑eI) x) = (g ∘ₗ ↑eI) x
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
exact ⟨g' ∘ₗ eR.symm.toLinearMap, fun x mx ↦ by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)⟩

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

Goal state before:
pp: case inl
n : ℕ
hnd : 0 ∣ n
⊢ φ (n / 0) = #({k ∈ range n | n.gcd k = 0})

pp: case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})

Tactic:
· simp [eq_zero_of_zero_dvd hnd]

Goal state after:
case inr
n d : ℕ
hnd : d ∣ n
hd0 : d > 0
⊢ φ (n / d) = #({k ∈ range n | n.gcd k = d})
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 : α
m : ℤ
⊢ b - (toIcoDiv hp a b • p - m • p) ∈ Set.Ico (a + m • p) (a + m • p + p)

Tactic:
← sub_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIcoDiv hp a b • p + m • p ∈ Set.Ico (a + m • p) (a + m • p + p)
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 : α
m : ℤ
⊢ b - (toIocDiv hp a b • p - m • p) ∈ Set.Ioc (a + m • p) (a + m • p + p)

Tactic:
← sub_add,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - toIocDiv hp a b • p + m • p ∈ Set.Ioc (a + m • p) (a + m • p + p)
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 : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Tactic:
by
  simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_sub]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
⊢ IsOpen[inst✝] {x} ↔ 𝓝[≠] x = ⊥

Tactic:
by
  rw [isOpen_singleton_iff_nhds_eq_pure, nhdsWithin, ← mem_iff_inf_principal_compl,
      le_antisymm_iff]
  simp [pure_le_nhds x]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ (𝓝[s] x).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ 𝓝 x → (t ∩ s).Nonempty

Tactic:
rw [nhdsWithin, inf_neBot_iff]
  exact forall₂_congr fun U _ ↦
    ⟨fun h ↦ h (mem_principal_self _), fun h u hsu ↦ h.mono <| inter_subset_inter_right _ hsu⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a < b + ↑⌊(a + p - b) / p⌋ * p

Tactic:
← add_lt_add_iff_right p,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ a + p < b + ↑⌊(a + p - b) / p⌋ * p + p
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: α : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ s = ⊥ → s = ∅

Tactic:
simp [← empty_mem_iff_bot, mem_nhdsSet_iff_forall, eq_empty_iff_forall_notMem]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ (∀ x ∈ s, ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x

Tactic:
rintro h ⟨x, xs⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (s.domRestrict f) ⟨x, xs⟩
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
x : (i : ι) → X i
inst✝ : ∀ (i : ι), (𝓝[s i] x i).NeBot
⊢ (𝓝[univ.pi s] x).NeBot

Tactic:
by
  simpa [nhdsWithin_pi_neBot]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.snd (𝓝[Prod.fst ⁻¹' {x.1}] x) = 𝓝 x.2

Tactic:
refine le_antisymm (continuousAt_snd.mono_left inf_le_left) fun s hs => ?_
  rcases x with ⟨x, y⟩
  rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs
  rcases hs with ⟨u, hu, v, hv, H⟩
  simp only [prod_subset_iff, mem_singleton_iff, mem_ofPred_eq, mem_preimage] at H
  exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ 𝓝 x ↔ U ∈ pure x ⊔ cofinite

Tactic:
simp_rw [mem_nhds_iff, isOpen_iff]

Goal state after:
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ (∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t) ↔ U ∈ pure x ⊔ cofinite
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
a : X
b : Z
⊢ 𝓝 (Prod.map f g (a, b)).1 ×ˢ 𝓝 (Prod.map f g (a, b)).2 ≤ map f (𝓝 a) ×ˢ map g (𝓝 b)

Tactic:
exact Filter.prod_mono (hf.nhds_le a) (hg.nhds_le b)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
β : Type u_5
T : Set (Set β)
f : α → β
x : α
x✝ : x ∈ s
⊢ (∀ (i : Set β), f x ∈ i → i ∈ T → ∀ᶠ (a : α) in 𝓝[s] x, f a ∈ i) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
exact forall_congr' fun t => forall_comm

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 γ
inst✝ : DiscreteTopology α
f : α × β → γ
x : α × β
⊢ ContinuousAt f x ↔ ContinuousAt (fun x_1 ↦ f (x.1, x_1)) x.2

Tactic:
by
  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_left

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : α → Set β
⊢ accumulate s ⊥ = s ⊥

Tactic:
by
  simp [Set.accumulate_def]

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

Goal state before:
pp: ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
⊢ {x} ∈ B

Tactic:
rw [sUnion_eq_univ_iff] at sUnion_univ

Goal state after:
ι : Type u_1
α✝ : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
⊢ {x} ∈ B
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ u ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}

Tactic:
rw [← hf u hu, sInter_eq_biInter]

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
u : Set α
hu : u ∈ s'
⊢ ⋂ i ∈ f u, i ∈ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
h : ∀ (x : ↑s), ∃ i, (↑x ∈ i ∧ IsOpen[inst✝] i) ∧ iᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i

Tactic:
choose U hU hUf using h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
f : Filter X
hf : f.NeBot
hfs : f ≤ 𝓟 s
U : ↑s → Set X
hU : ∀ (x : ↑s), ↑x ∈ U x ∧ IsOpen[inst✝] (U x)
hUf : ∀ (x : ↑s), (U x)ᶜ ∈ f
⊢ ∃ ι U, (∀ (i : ι), IsOpen[inst✝] (U i)) ∧ s ⊆ ⋃ i, U i ∧ ∀ (t : Finset ι), ¬s ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
⊢ CompactSpace X

Tactic:
refine compactSpace_generateFrom hT fun P hP𝔅 hP ↦ ?_
  contrapose! hP
  simp_rw [← Set.nonempty_compl, Set.compl_sUnion] at hP ⊢
  refine h _ ?_ fun Q hQP hQ ↦ ?_
  · rintro _ ⟨S, hS, rfl⟩
    exact h𝔅 _ (hP𝔅 hS)
  · replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
    exact hP hQP (hQ.image _)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact univ

Tactic:
rw [hf.isInducing.isCompact_iff, image_univ]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact univ

Tactic:
rw [← pi_univ univ]

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (univ.pi fun i ↦ univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
⊢ (∃ K, IsCompact K ∧ s ⊆ K) ↔ ∀ (i : ι), ∃ Ki, IsCompact Ki ∧ s ⊆ eval i ⁻¹' Ki

Tactic:
constructor
  · intro ⟨K, hK, hsK⟩ i
    exact ⟨eval i '' K, hK.image <| continuous_apply i, hsK.trans <| K.subset_preimage_image _⟩
  · intro H
    choose K hK hsK using H
    exact ⟨pi univ K, isCompact_univ_pi hK, fun _ hx i _ ↦ hsK i hx⟩

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

Tactic:
by_cases hcne : c.Nonempty

Goal state after:
case pos
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub

case neg
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
hcne : ¬c.Nonempty
⊢ ∃ ub ∈ opens, ∀ s ∈ c, s ⊆ ub
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : R0Space X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
a b : Y
⊢ a ⤳ b → b ⤳ a

Tactic:
by
    simpa only [← hf.specializes_iff] using Specializes.symm

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hs : IsDiscrete s
hf : ContinuousOn f (f ⁻¹' s)
H : ∀ (x : Y), IsDiscrete (f ⁻¹' {x})
⊢ IsDiscrete (f ⁻¹' s)

Tactic:
by
  refine .of_nhdsWithin fun x hx ↦ ?_
  have h := ((H (f x)).nhdsWithin _ rfl).le
  grw [nhdsWithin, ← comap_pure, ← hs.nhdsWithin _ hx, ← (hf.continuousWithinAt hx
    |>.tendsto_nhdsWithin fun _ ↦ by exact id).le_comap, inf_eq_right.mpr nhdsWithin_le_nhds] at h
  exact h

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE

Tactic:
tfae_have 1 ↔ 2 := ⟨fun h => h.1, fun h => ⟨h⟩⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed[inst✝] {x}
⊢ [T1Space X, ∀ (x : X), IsClosed[inst✝] {x}, ∀ (x : X), IsOpen[inst✝] {x}ᶜ, Continuous[inst✝, _] ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
⊢ IsPreirreducible S ↔ ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)

Tactic:
refine ⟨fun h _ ↦ ?_, fun h ↦ ?_⟩
  · exact subset_closure_inter_of_isPreirreducible_of_isOpen h
  · intro a b ha hb ⟨p, pS, pa⟩ bS
    by_contra! h0
    suffices p ∉ closure (S ∩ b) from this <| (h b hb bS) pS
    simp only [closure, mem_sInter, mem_ofPred_eq, and_imp, not_forall, exists_prop]
    use aᶜ
    grind [isClosed_compl_iff, subset_compl_iff_disjoint_left, disjoint_iff_inter_eq_empty]

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦ by
    rcases eq_or_ne x y with rfl | hne
    · rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
    · suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne
  rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this
  exact eventually_prod_self_iff.1 this

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ (univ \ {a})] a = 𝓝[s \ {a}] a

Tactic:
inter_sdiff_left_comm,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[univ ∩ (s \ {a})] a = 𝓝[s \ {a}] a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ 𝓝[≠] x = ⊥

Tactic:
rw [← isOpen_singleton_iff_punctured_nhds]

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
hx : (𝓝[≠] x).NeBot
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ IsOpen[inst✝¹] {x}