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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim

Tactic:
apply e.symm.congrRight.fullyFaithfulFunctor.preimageIso

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.symm.congrRight.functor.obj (e.congrRight.inverse ⋙ lim ⋙ e.functor) ≅ e.symm.congrRight.functor.obj lim
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
rw [this]
    infer_instance

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₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop ≫ uliftYonedaEquiv.symm (unop x₂).snd = uliftYonedaEquiv.symm (unop x₁).snd

Tactic:
← uliftYonedaEquiv_symm_map,

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₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYonedaEquiv.symm ((hom (P.map ↑f.unop)) (unop x₂).snd) = uliftYonedaEquiv.symm (unop x₁).snd
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.RightInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
by rintro (_ | (_ | _)) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)

Tactic:
refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).unop.left.op ?_
      refine Quiver.Hom.unop_inj ?_
      have := congr_arg Quiver.Hom.unop (Subobject.ofMkLEMk_comp h)
      simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk_obj, Over.mk_left,
        MonoOver.mk_arrow, unop_comp, Quiver.Hom.unop_op, comp_left]
          using congr_arg CommaMorphism.left this

Goal state after:
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
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this :
  (ConcreteCategory.hom c.inr) x ∈ Set.range ⇑(ConcreteCategory.hom c.inl) ⊓ Set.range ⇑(ConcreteCategory.hom c.inr)
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x

Tactic:
rw [disjoint_iff.mp h₃.1] at this

Goal state after:
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
x : (pair X Y).obj { as := right }
y : X
e : (ConcreteCategory.hom c.inl) y = (ConcreteCategory.hom c.inr) x
this : (ConcreteCategory.hom c.inr) x ∈ ⊥
⊢ (ConcreteCategory.hom f)
      ((Equiv.ofInjective (⇑(ConcreteCategory.hom c.inl)) h₁).symm ⟨(ConcreteCategory.hom c.inr) x, ⋯⟩) =
    (ConcreteCategory.hom g) x
Module: Mathlib.Algebra.Ring.NegOnePow

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

Tactic:
rw [Int.not_even_iff_odd] at h₂

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩
  simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: case property
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
x dx y dy : α
h : dy < dx
hx : 0 < dx
h' : x < y
⊢ x ∈ Ico x (x + dx) \ Ico y (y + dy)

Tactic:
simp [*, not_le.2 h']

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

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

Tactic:
by
  rcases Nat.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_nsmul_periodic]
    simp
  · rw [h.odd_nsmul_antiperiodic]
    simp [pow_add]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) = Fintype.card { k // k < n ∧ p k }

Tactic:
Fintype.card_of_subtype

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #({x ∈ range n | p x}) = #?s

case s
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ Finset ℕ

case H
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ ?s ↔ x < n ∧ p x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case succ
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + (n % a + a * (i + 1))) | a.Coprime x}) ≤ φ a * (i + 1 + 1)

Tactic:
simp only [mul_succ]

Goal state after:
case succ
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + (n % a + a * i)) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + (n % a + (a * i + a))) | a.Coprime x}) ≤ φ a * i + φ a + φ a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ (φ m).Coprime (φ n) → (m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2

Tactic:
rw [← not_imp_not]

Goal state after:
case mp
m n : ℕ
⊢ ¬((m = 1 ∨ m = 2) ∨ n = 1 ∨ n = 2) → ¬(φ m).Coprime (φ n)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
H : ∀ t ∈ iInf f, ⨅ i, (f i).lift g ≤ g t
⊢ ∀ x ∈ iInf f, s ∈ g x → s ∈ ⨅ i, (f i).lift g

Tactic:
exact fun t ht hs => H t ht hs

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ interior (⋂ i ∈ S, i) = ⋂ s ∈ S, interior s

Tactic:
hS.interior_biInter

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ ⋂ i ∈ S, interior i = ⋂ s ∈ S, interior s
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ⊆ interior s ∪ interior t

Tactic:
← (interior _).inter_univ,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) ∩ univ ⊆ interior s ∪ interior t
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₃
h₃₂₁ : btw x₃ x₂ x₁
⊢ x₁ = x₂ ∨ x₂ = x₃ ∨ x₃ = x₁

Tactic:
induction x₁ using QuotientAddGroup.induction_on
      induction x₂ using QuotientAddGroup.induction_on
      induction x₃ using QuotientAddGroup.induction_on
      rw [btw_cyclic] at h₃₂₁
      simp_rw [btw_coe_iff] at h₁₂₃ h₃₂₁
      simp_rw [← modEq_iff_eq_mod_zmultiples]
      simpa only [modEq_comm] using toIxxMod_antisymm _ h₁₂₃ h₃₂₁

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s ↔ SeparatedNhds s t

Tactic:
by
  constructor
  · rintro ⟨⟨u, u_cov, u_props⟩, ⟨v, v_cov, v_props⟩⟩
    have open_lemma : ∀ (u₀ a : ℕ → Set X), (∀ n, IsOpen (u₀ n)) →
      IsOpen (⋃ n, u₀ n \ closure (a n)) := fun _ _ u₀i_open ↦
        isOpen_iUnion fun i ↦ (u₀i_open i).sdiff isClosed_closure
    have cover_lemma : ∀ (h₀ : Set X) (u₀ v₀ : ℕ → Set X),
        (h₀ ⊆ ⋃ n, u₀ n) → (∀ n, Disjoint (closure (v₀ n)) h₀) →
        (h₀ ⊆ ⋃ n, u₀ n \ closure (⋃ m ≤ n, v₀ m)) :=
        fun h₀ u₀ v₀ h₀_cov dis x xinh ↦ by
      rcases h₀_cov xinh with ⟨un, ⟨n, rfl⟩, xinun⟩
      simp only [mem_iUnion]
      refine ⟨n, xinun, ?_⟩
      simp_all only [closure_iUnion₂_le_nat, disjoint_right, mem_iUnion,
        exists_false, not_false_eq_true]
    refine
      ⟨⋃ n : ℕ, u n \ (closure (⋃ m ≤ n, v m)),
       ⋃ n : ℕ, v n \ (closure (⋃ m ≤ n, u m)),
       open_lemma u (fun n ↦ ⋃ m ≤ n, v m) (fun n ↦ (u_props n).1),
       open_lemma v (fun n ↦ ⋃ m ≤ n, u m) (fun n ↦ (v_props n).1),
       cover_lemma s u v u_cov (fun n ↦ (v_props n).2),
       cover_lemma t v u v_cov (fun n ↦ (u_props n).2),
       ?_⟩
    rw [Set.disjoint_left]
    rintro x ⟨un, ⟨n, rfl⟩, xinun⟩
    suffices ∀ (m : ℕ), x ∈ v m → x ∈ closure (⋃ m' ∈ {m' | m' ≤ m}, u m') by simpa
    intro m xinvm
    have n_le_m : n ≤ m := by
      by_contra m_gt_n
      exact xinun.2 (subset_closure (mem_biUnion (le_of_lt (not_le.mp m_gt_n)) xinvm))
    exact subset_closure (mem_biUnion n_le_m xinun.1)
  · rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩
    exact
      ⟨⟨fun _ ↦ U,
        h_sub_U.trans (iUnion_const U).symm.subset,
        fun _ ↦
          ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
       ⟨fun _ ↦ V,
        k_sub_V.trans (iUnion_const V).symm.subset,
        fun _ ↦
          ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : Y ≃ₜ Z
f : X → Y
h : IsOpenQuotientMap (⇑e ∘ f)
⊢ IsOpenQuotientMap f

Tactic:
by simpa [← Function.comp_assoc] using e.symm.isOpenQuotientMap.comp h

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
⊢ tβ = induced f tα ↔ ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))

Tactic:
simp only [ext_iff_nhds, nhds_induced]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ Continuous[inst✝, _] p ↔ IsOpen[inst✝] {x | p x}

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
p : α → Prop
⊢ (∀ (x : α), p x → ∀ᶠ (x : α) in 𝓝 x, p x) ↔ ∀ x ∈ {x | p x}, {x | p x} ∈ 𝓝 x
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
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set X
hs : IsOpen[inst✝¹] s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s

Tactic:
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ u, IsOpen[inst✝] u ∧ a ∈ u ∧ u ∩ s ⊆ t

Tactic:
simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
𝔖 : Set (Set ι)
⊢ induced (⋃₀ 𝔖).domRestrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.domRestrict topologicalSpace

Tactic:
simp_rw [Pi.induced_domRestrict, iInf_sUnion]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : IsOpenMap (s.domRestrict f)
finv : β → α
hleft : LeftInvOn finv f s
t : Set α
ht : IsOpen[inst✝¹] t
⊢ IsOpen[inst✝] (f '' (t ∩ s))

Tactic:
rw [← image_domRestrict]
    exact h _ (ht.preimage continuous_subtype_val)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
hs' : ⋃ i, s i = univ
⊢ ContinuousOn f (⋃ i, s i)

Tactic:
exact ContinuousOn.iUnion_of_isOpen hf hs

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
U : ι → Set β
F : Finset ι
hU : ∀ i ∈ F, U i ∈ T i
⊢ IsOpen[⨅ i, t i] (⋂ i ∈ F, U i)

Tactic:
refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

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

Goal state before:
pp: case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι
    exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
ι : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology X
⊢ SigmaCompactSpace X

Tactic:
by
  choose K hKc hxK using fun x : X => exists_compact_mem_nhds x
  rcases countable_cover_nhds hxK with ⟨s, hsc, hsU⟩
  refine SigmaCompactSpace.of_countable _ (hsc.image K) (forall_mem_image.2 fun x _ => hKc x) ?_
  rwa [sUnion_image]

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

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ⋃ n, (fun n ↦ univ.pi fun i ↦ compactCovering (X i) n) n = univ

Tactic:
iUnion_univ_pi_of_monotone

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ (univ.pi fun i ↦ ⋃ j, compactCovering (X i) j) = univ

X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ∀ (i : ι), Monotone (compactCovering (X i))
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ p s

Tactic:
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
this : sᶜ ∈ f
⊢ p s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x

Tactic:
simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff, Ultrafilter.mem_coe]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
⊢ IsCompact (s ∪ t)

Tactic:
by
  rw [union_eq_iUnion]; exact isCompact_iUnion fun b => by cases b <;> assumption

Goal state after:
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
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → ⋃₀ Q ≠ univ
⊢ ⋃₀ P ≠ univ

Tactic:
simp_rw [← Set.nonempty_compl, Set.compl_sUnion] at hP ⊢

Goal state after:
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
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
⊢ (⋂₀ (compl '' P)).Nonempty
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
inst✝ : NoncompactSpace X
i✝ : Set X
hs : ¬i✝ᶜ.Nonempty
⊢ ¬IsCompact i✝

Tactic:
rw [not_nonempty_iff_eq_empty, compl_empty_iff] at hs

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
inst✝ : NoncompactSpace X
i✝ : Set X
hs : i✝ = univ
⊢ ¬IsCompact i✝
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:
by rw [hf.isInducing.isCompact_iff, image_univ]; exact hf.isClosed_range.isCompact

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

Goal state before:
pp: case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
⊢ f x ≠ g x

Tactic:
obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
hfg : ∀ᶠ (x : X) in 𝓝 x, f x ≠ g x
t : Set X
h₁t : ∀ y ∈ t, f y ≠ g y
h₂t : IsOpen[inst✝²] t
h₃t : x ∈ t
⊢ f x ≠ g x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case h₁
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ 𝓟 {x | x ⤳ p} ≤ 𝓝 p

Tactic:
Filter.principal_le_iff

Goal state after:
case h₁
X : Type u_1
inst✝ : TopologicalSpace X
p : X
s : Set X
hs : Disjoint (𝓝[s] p) cofinite
⊢ ∀ V ∈ 𝓝 p, {x | x ⤳ p} ⊆ V
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert.refine_1.inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
x : ι
t : Finset ι
hx : x ∉ t
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hsC : s ⊆ U x ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U x) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₁ : K₁ ⊆ U x
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hi : i ≠ x
⊢ IsCompact (update K x K₁ i)

Tactic:
· simp only [update_of_ne hi, h1K]

Goal state after:
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
⊢ IsClosed[inst✝] (s ∩ a)

Tactic:
convert! this using 1

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s a b : Set X
h : IsClopen s
cover : s ⊆ a ∪ b
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
hab : Disjoint a b
this : IsClosed[inst✝] (s ∩ bᶜ)
⊢ s ∩ a = s ∩ bᶜ
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ u' ∩ s ∩ (v' ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty

Tactic:
← u'_eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
H : IsPreconnected s
f : α → β
hf : ContinuousOn f s
u v : Set β
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : α
xs : x ∈ s
xu : f x ∈ u
y : α
ys : y ∈ s
yv : f y ∈ v
u' : Set α
hu' : IsOpen[inst✝¹] u'
u'_eq : f ⁻¹' u ∩ s = u' ∩ s
v' : Set α
hv' : IsOpen[inst✝¹] v'
v'_eq : f ⁻¹' v ∩ s = v' ∩ s
huv : s ⊆ u' ∪ v'
z : α
hz : z ∈ f ⁻¹' u ∩ s ∩ (v' ∩ s)
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (s ∪ t)

Tactic:
rw [union_eq_iUnion]; exact isLindelof_iUnion fun b => by cases b <;> assumption

Goal state after: