mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ Subobject X ≃o (Subobject (op X))ᵒᵈ

Tactic:
refine OrderIso.ofHomInv (cokernelOrderHom X) (kernelOrderHom X) ?_ ?_
  · change (cokernelOrderHom X).comp (kernelOrderHom X) = _
    refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
    intro A f hf
    dsimp only [OrderHom.comp_coe, Function.comp_apply, kernelOrderHom_coe, Subobject.lift_mk,
      cokernelOrderHom_coe, OrderHom.id_coe, id]
    refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
    · exact (Abelian.epiDesc f.unop _ (cokernel.condition (kernel.ι f.unop))).op
    · exact (cokernel.desc _ _ (kernel.condition f.unop)).op
    · rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
      simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
        comp_epiDesc, Category.comp_id]
    · simp only [← cancel_epi f.unop, unop_comp, Quiver.Hom.unop_op, unop_id, comp_epiDesc_assoc,
        cokernel.π_desc, Category.comp_id]
    · exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])
  · change (kernelOrderHom X).comp (cokernelOrderHom X) = _
    refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
    intro A f hf
    dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
      kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op]
    refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
    · exact Abelian.monoLift f _ (kernel.condition (cokernel.π f))
    · exact kernel.lift _ _ (cokernel.condition f)
    · simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
        Category.id_comp]
    · simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]
    · simp only [monoLift_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel f

Tactic:
rw [← this]

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel f

Tactic:
rw [← this]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this✝ : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right (StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯)

Tactic:
apply yonedaEquiv.injective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ yonedaEquiv (StructuredArrow.Hom.right φ) =
    yonedaEquiv
      (StructuredArrow.Hom.right (StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v

Tactic:
refine h.def _ _ fun g => hc.hom_ext fun b => ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Cofan f
hc : IsColimit c
h : IsSeparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ c.ι.app b ≫ g ≫ u = c.ι.app b ≫ g ≫ v
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v

Tactic:
refine h.def _ _ fun g => hc.hom_ext fun b => ?_

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
h : IsCoseparator c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ (u ≫ g) ≫ c.π.app b = (v ≫ g) ≫ c.π.app b
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr.refine_3
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))
this :
  ∀ (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.inr)
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inr ≫
        ↾fun x ↦
          if h : x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) then
            (ConcreteCategory.hom f) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨x, h⟩)
          else (ConcreteCategory.hom g) ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inr)) h₂).symm ⟨x, ⋯⟩)) =
      g

Tactic:
intro T f g
        ext x
        dsimp
        simp only [Set.mem_range, Equiv.ofInjective_symm_apply, dite_eq_right_iff,
          forall_exists_index]
        intro y e
        have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
        rw [disjoint_iff.mp h₃.1] at this
        exact this.elim

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ + z₂).val = Additive.toMul au ^ (z₁.val + z₂.val)

Tactic:
ZMod.val_add,

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ ((z₁.val + z₂.val) % 2) = Additive.toMul au ^ (z₁.val + z₂.val)
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b c d : α
⊢ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b →
    b < d ∧ d < c ∨ d < c ∧ c < b ∨ c < b ∧ b < d → a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
by
    rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hbd, hdc⟩ | ⟨hdc, hcb⟩ | ⟨hcb, hbd⟩) <;>
      first
      | refine .inl ?_; constructor <;> order
      | refine .inr <| .inl ?_; constructor <;> order
      | refine .inr <| .inr ?_; constructor <;> order

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

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

Tactic:
rw [h.even_nsmul_periodic]
    simp

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.factorization.support
h : 0 < n.factorization p
⊢ φ (p ^ n.factorization p) = p ^ (n.factorization p - 1) * (p - 1)

Tactic:
rw [totient_prime_pow (prime_of_mem_primeFactors hp) h]

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

pp: case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : ¬b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
· rw [hb, totient_zero, totient_eq_zero] at h'
    exact False.elim (ha h')

Goal state after:
case neg
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : ¬b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Sort u_6
p : ι → Prop
s✝ : ι → Set α
f : Filter α
hf : f.HasBasis p s✝
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s✝ i)).HasBasis (pg i) (sg i)
gm : Monotone g
s : Set γ
⊢ s ∈ f.lift g ↔ ∃ i, p i ∧ ∃ x, pg i x ∧ sg i x ⊆ s

Tactic:
by
  refine (mem_biInf_of_directed ?_ ⟨univ, univ_sets _⟩).trans ?_
  · intro t₁ ht₁ t₂ ht₂
    exact ⟨t₁ ∩ t₂, inter_mem ht₁ ht₂, gm inter_subset_left, gm inter_subset_right⟩
  · simp only [← (hg _).mem_iff]
    exact hf.exists_iff fun t₁ t₂ ht H => gm ht H

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ interior sᶜ = (closure s)ᶜ

Tactic:
by
  simp [closure_eq_compl_interior_compl]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure sᶜ = (interior s)ᶜ

Tactic:
by
  simp [closure_eq_compl_interior_compl]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
ι : Sort u_3
p : ι → Prop
s : ι → Set X
F : Filter X
hx : (𝓝 x).HasBasis p s
⊢ ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i

Tactic:
by
  simp only [hx.clusterPt_iff F.basis_sets, Filter.frequently_iff, inter_comm (s _),
    Set.Nonempty, id, mem_inter_iff]

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 : α
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
by
  suffices toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b by
    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]
  rw [eq_comm, ← not_modEq_iff_toIcoDiv_eq_toIocDiv, eq_comm, ←
    modEq_iff_toIcoDiv_eq_toIocDiv_add_one]
  exact em' _

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
hg : IsInducing g
hf : IsInducing f
⊢ inst✝¹ = induced (g ∘ f) inst✝

Tactic:
hf.eq_induced,

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
hg : IsInducing g
hf : IsInducing f
⊢ induced f inst✝² = induced (g ∘ f) inst✝
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst✝] s ↔ ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
hf.eq_induced,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[induced f inst✝¹] s ↔ ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = s
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s) → x ∈ s

Tactic:
hf.eq_induced,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsClosed[induced f inst✝¹] s ↔ ∀ (x : X), f x ∈ closure[inst✝¹] (f '' s) → x ∈ s
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[inst✝] s ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
hf.eq_induced,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[induced f inst✝¹] s ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: case refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
f : X → Y
inst✝ : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
⊢ inst✝¹ = ⊤

Tactic:
hf.eq_induced,

Goal state after:
case refl
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
f : X → Y
inst✝ : IndiscreteTopology Y
hf : IsInducing f
this : TopologicalSpace Y := ⊤
⊢ induced 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
⊢ IsQuotientMap f ↔ Surjective f ∧ ∀ (s : Set Y), IsClosed[inst✝] s ↔ IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
simp_rw [isQuotientMap_iff, isCoinducing_iff_isClosed, and_comm, iff_comm]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ 𝓝 (f x) ↔ s ∈ 𝓝 x

Tactic:
← hf.map_nhds_eq,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsOpenEmbedding f
s : Set X
x : X
⊢ f '' s ∈ map f (𝓝 x) ↔ s ∈ 𝓝 x
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]

Goal state after:
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 (⋃ v ∈ t, u ×ˢ v)
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)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (Prod.snd ⁻¹' v)

Tactic:
rw [← this]

Goal state after:
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)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (⋃ u ∈ s, u ×ˢ v)
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 → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst✝¹, inst✝] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝², inst✝] fun x ↦ f x y
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ f x y ∈ closure[inst✝] u

Tactic:
rw [← isClosed_closure.closure_eq]
  apply map_mem_closure (hf₁ x) hy fun b hb ↦ ?_
  apply map_mem_closure (hf₂ b) hx fun a ha ↦ h a ha b hb

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] s = 𝓟 s

Tactic:
simp [nhdsSetWithin, principal_le_nhdsSet]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
i : X ⊕ Y
⊢ ((Homeomorph.refl X).sumCongr (Homeomorph.refl Y)) i = (Homeomorph.refl (X ⊕ Y)) i

Tactic:
cases i <;> rfl

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' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
X'' : Type u_7
Y'' : Type u_8
inst✝¹ : TopologicalSpace X''
inst✝ : TopologicalSpace Y''
h₁ : X ≃ₜ X'
h₂ : Y ≃ₜ Y'
h₃ : X' ≃ₜ X''
h₄ : Y' ≃ₜ Y''
i : X ⊕ Y
⊢ ((h₁.sumCongr h₂).trans (h₃.sumCongr h₄)) i = ((h₁.trans h₃).sumCongr (h₂.trans h₄)) i

Tactic:
cases i <;> rfl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[t] s

Tactic:
hb.eq_generateFrom

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[generateFrom b] s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (i.pi s)

Tactic:
rw [pi_def]

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hi : i.Finite
hs : ∀ a ∈ i, IsOpen[T a] (s a)
⊢ IsOpen[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mpr
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 ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g)) →
    (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

Tactic:
· intro ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩
    refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩
    exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (i.pi s)

Tactic:
rw [pi_def]

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
hs : ∀ a ∈ i, IsClosed[T a] (s a)
⊢ IsClosed[Pi.topologicalSpace] (⋂ a ∈ i, eval a ⁻¹' s a)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t

Tactic:
refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s ⊆ s

case refine_2
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s).Countable

case refine_3
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ Dense ((t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s)

case refine_4
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s

case refine_5
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
s : Set α
inst✝ : SeparableSpace ↑s
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x | IsBot x} ∪ {x | IsTop x})) ∩ s
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsSigmaCompact univ ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = univ

Tactic:
IsSigmaCompact

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = univ) ↔ ∃ K, (∀ (n : ℕ), IsCompact (K n)) ∧ ⋃ n, K n = univ
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
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1

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)
this✝ : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ (coclosedCompact X).HasBasis (fun s ↦ IsClosed[inst✝] s ∧ IsCompact s) compl

Tactic:
by
  simp only [Filter.coclosedCompact, iInf_and']
  refine hasBasis_biInf_principal' ?_ ⟨∅, isClosed_empty, isCompact_empty⟩
  rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
  exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩

Goal state after:
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✝²] (f ⁻¹' U ∩ s ∪ g ⁻¹' U)

Tactic:
exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set Y
⊢ IsDiscrete s ↔ ∀ y ∈ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = {y}

Tactic:
by
  rw [isDiscrete_iff_discreteTopology, discreteTopology_subtype_iff']

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
h : x ≠ y
s : Set X
⊢ 𝓝[s \ {y}] x = 𝓝[s] x

Tactic:
rw [sdiff_eq, inter_comm, nhdsWithin_inter_of_mem]
  exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)

Goal state after: