mathlib-initiative/mathlib-tactics huggingface dataset:
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₁)
s : Cocone (functorToRepresentables P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))), naturality := ⋯ }

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), (coconeOfRepresentable P).ι.app j ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (m.app X)).toFun x =
    (hom ({ app := fun X ↦ ↾fun x ↦ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))), naturality := ⋯ }.app X)).toFun
      x
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
this✝² : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝¹ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this✝ : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
this : ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
⊢ f = default

Tactic:
by
      apply this

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (free.map f)

Tactic:
by_cases! hX : IsEmpty X
    · constructor
      intros
      apply (IsInitial.isInitialObj free _
        ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt
    · have hf : Function.Injective f := by rwa [← mono_iff_injective]
      obtain ⟨g, hg⟩ := hf.hasLeftInverse
      have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }
      infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
      { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ } =
    { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫ ((const F.Elementsᵒᵖ).obj F).map g

Tactic:
ext X x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).obj u).obj X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
                { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ }).app
            X)).toFun
      x =
    (ConcreteCategory.hom
          (({ app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫
                ((const F.Elementsᵒᵖ).obj F).map g).app
            X)).toFun
      x
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X Y : Type u
c : BinaryCofan X Y
h₁ : Injective ⇑(ConcreteCategory.hom c.inl)
h₂ : Injective ⇑(ConcreteCategory.hom c.inr)
h₃ : IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr))
⊢ ∀ (x : (fun X ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })),
    x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ∨ x ∈ (Set.range ⇑(ConcreteCategory.hom c.inl))ᶜ

Tactic:
exact fun _ => or_not

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

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn : n ∈ ℤ ∙ 0
⊢ 0 n = g ⟨n, hn⟩

Tactic:
rw [Submodule.span_zero_singleton] at hn

Goal state after:
case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ ℤ ∙ 0
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddMonoid α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℕ
⊢ f (x + (2 * k + 1) • c) = (-1) ^ (2 * k + 1) • f x

Tactic:
· rw [h.odd_nsmul_antiperiodic]
    simp [pow_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
x : R
mx : x ∈ I
⊢ (g' ∘ₗ ↑eR.symm) x = g ⟨x, mx⟩

Tactic:
by simpa [eI, eR] using hg' (equivShrink I ⟨x, mx⟩)

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

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
hf : ∀ (x : R) (hx : x ∈ I'), f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, ⋯⟩)
f' : R →ₗ[R] M
hf' : ∀ (x : R) (mem : x ∈ I'), f' x = f ⟨x, mem⟩
⊢ ∃ g', ∀ (x : S) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
exact ⟨e₂.toLinearMap ∘ₛₗ f' ∘ₛₗ e₁.toSemilinearEquiv.symm.toLinearMap, by simp_all [I']⟩

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

Goal state before:
pp: a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
⊢ a = b

Tactic:
by_cases ha' : a = 0

Goal state after:
case pos
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : a = 0
⊢ a = b

case neg
a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
ha' : ¬a = 0
⊢ a = b
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_right_comm]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
⊢ x ∈ U → (U ∩ s).Nonempty

Tactic:
x_in

Goal state after:
case mpr
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (U : Set X), IsOpen U → U.Nonempty → (U ∩ s).Nonempty
x : X
U : Set X
U_op : IsOpen U
x_in : x ∈ U
⊢ (U ∩ s).Nonempty
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 x✝ : α
⊢ ¬a ≡ x✝ [PMOD p] ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)

Tactic:
modEq_iff_forall_notMem_Ioo_mod hp,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ (¬∀ (z : ℤ), x✝ - z • p ∉ Set.Ioo a (a + p)) ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Sort w
x : X
t : Set X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ (i : ι), p i → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i

Tactic:
simp only [Set.Nonempty, mem_inter_iff, and_comm]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X → Y
he : IsHomeomorph e
f : Y → Z
s : Set Z
⊢ f ∘ e '' frontier (f ∘ e ⁻¹' s) = f '' frontier (f ⁻¹' s)

Tactic:
by
  simp only [Set.preimage_comp, Set.image_comp, he.image_frontier,
    Set.image_preimage_eq _ he.surjective]

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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l

Tactic:
exact inf_le_inf_right (comap f l) (by simp)

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 : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] (f '' f ⁻¹' s)

Tactic:
image_preimage_eq_inter_range,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsOpen[inst✝] s ↔ IsOpen[inst✝] (s ∩ range f)
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 : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (comap f (𝓟 {f x}ᶜ ⊓ l)) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)

Tactic:
hf.isOpenMap.clusterPt_comap_iff hf.continuous

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t] a = 𝓝[u] a

Tactic:
nhdsWithin_restrict' t hs,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t u : Set α
hs : s ∈ 𝓝 a
h₂ : t ∩ s = u ∩ s
⊢ 𝓝[t ∩ s] a = 𝓝[u] a
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst✝¹] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t = f ⁻¹' t ∩ s

Tactic:
inter_eq_self_of_subset_left hp

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
h : ContinuousOn f s
hs : IsOpen[inst✝¹] s
hp : f ⁻¹' t ⊆ s
ht : IsOpen[inst✝] t
⊢ f ⁻¹' t = f ⁻¹' t
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
⊢ Tendsto f (𝓝[s] x) (𝓝 (f x)) ↔ ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ 𝓝[s] x

Tactic:
simp only [TopologicalSpace.nhds_generateFrom, tendsto_iInf, tendsto_principal, mem_ofPred_eq,
      and_imp]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s : Set α
⊢ map f (𝓝ˢ s) = 𝓝ˢ[range f] (f '' s)

Tactic:
rw [nhdsSet_induced, Filter.map_comap, nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
t : Set Y
H : MapsTo f s t
hs : IsOpen[inst✝¹] s
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' f '' s)

Tactic:
exact continuous_subtype_val.1 _ (hf.isOpenMap _ hs)

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X ⊕ Y
⊢ comap (Sum.elim f g) (𝓝 (Sum.elim f g x)) ≤ 𝓝 x

Tactic:
obtain x | x := x <;>
  simp only [comap_sumElim_eq, nhds_inl, nhds_inr, elim_inl, elim_inr, ← hf.nhds_eq_comap,
    ← hg.nhds_eq_comap, sup_le_iff, le_rfl, true_and, and_true] <;>
  convert! bot_le (α := Filter (X ⊕ Y)) <;>
  rw [map_eq_bot_iff, comap_eq_bot_iff_compl_range]

Goal state after:
case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ (range g)ᶜ ∈ 𝓝 (f x)

case e'_3
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : Y
⊢ (range f)ᶜ ∈ 𝓝 (g x)
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 : α × β → γ
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔ ∀ (b : β), Continuous[inst✝³, inst✝¹] fun x ↦ f (x, b)

Tactic:
by
  simp_rw [← continuousOn_univ]; exact continuousOn_prod_of_discrete_right

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

Goal state before:
pp: case mp
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ ((IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b) →
    (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))

Tactic:
intro ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, f_ne_g⟩⟩
    exact ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
nontriviality ∀ i, X i

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n m : ℕ
hm : accumulate s n ⊆ s m
k : ℕ
hk : s m ⊆ s k ∧ s (n + 1) ⊆ s k
⊢ accumulate s (n + 1) ⊆ s k

Tactic:
simp; grind

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
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ comk (fun x ↦ x ∈ B) empty_mem subset_mem union_mem ≤ cofinite

Tactic:
simpa [le_cofinite_iff_compl_singleton_mem]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
s : (a : ι) → Set (A a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
⊢ IsOpen[Pi.topologicalSpace] ((↑i).pi s)

Tactic:
let := fun a => generateFrom (g a)

Goal state after:
case refine_1
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
s : (a : ι) → Set (A a)
i : Finset ι
hi : ∀ a ∈ i, s a ∈ g a
this : (a : ι) → TopologicalSpace (A a) := fun a ↦ generateFrom (g a)
⊢ IsOpen[Pi.topologicalSpace] ((↑i).pi s)
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
⊢ 𝓟 (𝒫 ∅) = pure ∅

pp: α : Type u_1
⊢ Monotone powerset

Tactic:
powerset_empty,

Goal state after:
α : Type u_1
⊢ 𝓟 {∅} = pure ∅

α : Type u_1
⊢ Monotone powerset
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
ht : IsSigmaCompact t
hs : IsClosed[inst✝] s
h : s ⊆ t
⊢ IsSigmaCompact s

Tactic:
rcases ht with ⟨K, hcompact, hcov⟩
  refine ⟨(fun n ↦ s ∩ (K n)), fun n ↦ (hcompact n).inter_left hs, ?_⟩
  rw [← inter_iUnion, hcov]
  exact inter_eq_left.mpr h

Goal state after:
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
⊢ x ∈ s

pp: case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b

Tactic:
· obtain ⟨a, has, hax⟩ := h.prop
    rwa [h.eq_of_ge ⟨a, has, rfl.le⟩ hax]

Goal state after:
case refine_2
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : x ∈ s
b : α
x✝ : (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) b
hbx : b ≤ x
a : α
has : a ∈ s
hab : a ≤ b
⊢ x ≤ b
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
⊢ IsBounded (f '' s)

Tactic:
choose U hU using hf
  obtain ⟨I, hI⟩ := hs.elim_nhds_subcover U (fun x _ => (hU x).1)
  have : f '' ⋃ x ∈ I, U x = ⋃ x ∈ I, f '' U x := by simp [Set.image_iUnion₂]
  exact ((isBounded_biUnion_finset I).2 fun i _ => (hU i).2).subset (this ▸ Set.image_mono hI.2)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: case neg.inl.hs
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}) x

pp: case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x

Tactic:
· exact (hf x hx).congr (fun y hy => if_pos hy.2) (if_pos hx.2)

Goal state after:
case neg.inl.ht
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s : Set α
p : α → Prop
f g : α → β
inst✝ : (a : α) → Decidable (p a)
hpf : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto f (𝓝[s ∩ {a | p a}] a) (𝓝 (if p a then f a else g a))
hpg : ∀ a ∈ s ∩ frontier {a | p a}, Tendsto g (𝓝[s ∩ {a | ¬p a}] a) (𝓝 (if p a then f a else g a))
hf : ContinuousOn f (s ∩ {a | p a})
hg : ContinuousOn g (s ∩ {a | ¬p a})
x : α
hx' : x ∉ frontier {a | p a}
hx : x ∈ s ∩ {a | p a}
⊢ ContinuousWithinAt (fun a ↦ if p a then f a else g a) (s ∩ {a | p a}ᶜ) x
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝²] (s.piecewise f g ⁻¹' U)

Tactic:
piecewise_preimage,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
this : ∀ (U : Set Y), IsOpen[inst✝¹] U → g ⁻¹' U ⊆ f ⁻¹' U
U : Set Y
hU : IsOpen[inst✝¹] U
⊢ IsOpen[inst✝²] (s.ite (f ⁻¹' U) (g ⁻¹' U))
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsOpen[inst✝] s → (x ∈ s ↔ y ∈ s)

Tactic:
by
  simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def,
    Iff.comm]

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)
hf' : Injective f
x : X
hx : x ∈ f ⁻¹' s
⊢ Tendsto f (𝓝[f ⁻¹' s] x) (𝓝[s] f x)

Tactic:
exact (hf.continuousWithinAt hx).tendsto_nhdsWithin (Set.mapsTo_preimage _ _)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
let := hs.1

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsDiscrete s
a b : X
hab : a ⤳ b
ha : a ∈ s
hb : b ∈ s
this : DiscreteTopology ↑s := hs.to_subtype
⊢ a = b
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a x : α
⊢ {x}ᶜ ∈ 𝓝[≠] a

Tactic:
rcases eq_or_ne a x with rfl | hx

Goal state after:
case inl
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a : α
⊢ {a}ᶜ ∈ 𝓝[≠] a

case inr
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a x : α
hx : a ≠ x
⊢ {x}ᶜ ∈ 𝓝[≠] a
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
by
  constructor
  · rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]
    intro h x U hxU
    rcases h x U hxU with ⟨V, hVU, hV₁, hxV, hV₂⟩
    exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩
  · rw [locallyConnectedSpace_iff_connectedComponentIn_open]
    refine fun h U hU x _ => isOpen_iff_mem_nhds.mpr fun y hy => ?_
    rw [connectedComponentIn_eq hy]
    rcases h y U (hU.mem_nhds <| (connectedComponentIn_subset _ _) hy) with ⟨V, hVy, hV, hVU⟩
    exact Filter.mem_of_superset hVy (hV.subset_connectedComponentIn (mem_of_mem_nhds hVy) hVU)

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

Goal state before:
pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsConnected t
⊢ IsConnected (inr '' t)

Tactic:
· exact ht.image _ continuous_inr.continuousOn

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

Goal state before:
pp: case refine_2.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
t : Set β
ht : IsPreconnected t
⊢ IsPreconnected (inr '' t)

Tactic:
· exact ht.image _ continuous_inr.continuousOn

Goal state after: