mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
A : D
h : j.essImage A
⊢ IsIso ((coreflectorAdjunction j).counit.app A)

Tactic:
isIso_counit_app_iff_mem_essImage

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
A : D
h : j.essImage A
⊢ j.essImage A
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ ∃ a, (map f).map a = e

Tactic:
refine ⟨homMk e.hom.left ?_, rfl⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ Over.Hom.left e.hom ≫ h.arrow = g.arrow
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)
S : ShortComplex C
hS : S.Exact
hf : Epi S.g
⊢ (S.map F).Exact ∧ Epi (F.map S.g)

Tactic:
by
    have := preservesEpimorphisms_of_preserves_shortExact_right F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
    let φ : S.map F ⟶ T.map F :=
      { τ₁ := F.map <| Abelian.factorThruImage S.f
        τ₂ := 𝟙 _
        τ₃ := 𝟙 _
        comm₁₂ := show _ ≫ F.map (kernel.ι _) = F.map _ ≫ 𝟙 _ by
          rw [← F.map_comp, Abelian.image.fac, Category.comp_id] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
hX : IsInitial X
⊢ Subsingleton (Subobject X)

Tactic:
suffices ∀ (S : Subobject X), S = .mk (𝟙 _) from ⟨by simp [this]⟩
  intro S
  obtain ⟨A, i, _, rfl⟩ := S.mk_surjective
  have fac : hX.to A ≫ i = 𝟙 X := hX.hom_ext _ _
  let e : A ≅ X :=
    { hom := i
      inv := hX.to A
      hom_inv_id := by rw [← cancel_mono i, assoc, fac, id_comp, comp_id]
      inv_hom_id := fac }
  exact mk_eq_mk_of_comm i (𝟙 X) e (by simp [e])

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
⊢ ∀ (j : Finset (Discrete α)),
    (colimit.cocone (liftToFinsetObj (Discrete.functor f))).ι.app j ≫
        ((liftToFinsetColimitCocone (Discrete.functor f)).isColimit.coconePointUniqueUpToIso
            (colimit.isColimit (Discrete.functor f))).hom =
      (finiteSubcoproductsCocone f).ι.app j

Tactic:
intro S
    simp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
      colimit.cocone_x, colimit.cocone_ι, finiteSubcoproductsCocone_ι_app]
    ext j
    rw [← Category.assoc]
    convert!
      IsColimit.comp_coconePointUniqueUpToIso_hom
        (liftToFinsetColimitCocone (Discrete.functor f)).isColimit (colimit.isColimit _) j
    · simp [← colimit.w (liftToFinsetObj _) (homOfLE (x := {j.1}) (y := S) (by simp))]
    · simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L'.HasPointwiseLeftKanExtensionAt F' Y

Tactic:
rw [hasPointwiseLeftKanExtensionAt_iff_of_natIso_left _ e₁.symm]

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
⊢ L.HasPointwiseLeftKanExtensionAt F' Y
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'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
ex : L'.LeftExtension F
⊢ StructuredArrow.IsUniversal ex ≃ StructuredArrow.IsUniversal ((postcomp₁ G e.inv F).obj ex)

Tactic:
by
  apply IsInitial.isInitialIffObj (LeftExtension.postcomp₁ G e.inv F)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
let eq : (RightExtension.mk _ α).IsUniversal ≃
    (RightExtension.mk _
      ((associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
    (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))
  constructor
  · exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩
  · exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
D : Type u_1
J : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} D
inst✝⁹ : Category.{v_2, u_2} J
inst✝⁸ : HasLimitsOfShape J C
inst✝⁷ : HasLimitsOfShape J D
inst✝⁶ : HasExactLimitsOfShape J D
F : C ⥤ D
inst✝⁵ : PreservesFiniteColimits F
inst✝⁴ : ReflectsFiniteColimits F
inst✝³ : HasFiniteColimits C
inst✝² : PreservesLimitsOfShape J F
I : Type
inst✝¹ : SmallCategory I
inst✝ : FinCategory I
G : I ⥤ J ⥤ C
c : Cocone G
hc : IsColimit c
i : I
⊢ limMap (whiskerRight (c.ι.app i) F) ≫ (preservesLimitIso F c.pt).inv =
    (preservesLimitIso F (G.obj i)).inv ≫ F.map (limMap (c.ι.app i))

Tactic:
exact (preservesLimitNatIso F).inv.naturality _

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
⊢ HasInitial (StructuredArrow A G)

Tactic:
obtain ⟨T, hT⟩ := has_weakly_initial_of_weakly_initial_set_and_hasProducts hB'

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
B' : ι → StructuredArrow A G := fun i ↦ StructuredArrow.mk (f i)
hB' : ∀ (A' : StructuredArrow A G), ∃ i, Nonempty (B' i ⟶ A')
T : StructuredArrow A G
hT : ∀ (X : StructuredArrow A G), Nonempty (T ⟶ X)
⊢ HasInitial (StructuredArrow A G)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ (c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt).Final

Tactic:
apply Functor.final_of_isTerminal_colimit_comp_yoneda

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ IsTerminal (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
⊢ btw a b c → btw c b a → a = b ∨ b = c ∨ c = a

Tactic:
rintro (⟨hab, hbc⟩ | ⟨hbc, hca⟩ | ⟨hca, hab⟩) (⟨hcb, hba⟩ | ⟨hba, hac⟩ | ⟨hac, hcb⟩)

Goal state after:
case inl.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

case inl.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inl.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

case inr.inl.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

case inr.inl.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inr.inl.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hbc : b ≤ c
hca : c ≤ a
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hcb : c ≤ b
hba : b ≤ a
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inl
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hba : b ≤ a
hac : a ≤ c
⊢ a = b ∨ b = c ∨ c = a

case inr.inr.inr.inr
α : Type u_1
inst✝ : PartialOrder α
a b c : α
hca : c ≤ a
hab : a ≤ b
hac : a ≤ c
hcb : c ≤ b
⊢ a = b ∨ b = c ∨ c = a
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑k = ↑(k * n) / ↑n

Tactic:
cast_mul,

Goal state after:
K : Type u_1
inst✝ : DivisionSemiring K
n : ℕ
hn : ↑n ≠ 0
k : ℕ
this : n ≠ 0
⊢ ↑k = ↑k * ↑n / ↑n
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False

Tactic:
simpa [heq] using count_strict_mono hm hmn

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

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

Tactic:
simp only [add_zero, mul_one, mul_zero, zero_add]

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

Goal state before:
pp: case inr.hi
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a ∈ {a ∈ range x | x.Coprime a}, d * a ∈ {k ∈ range (d * x) | (d * x).gcd k = d}

pp: case inr.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ {a ∈ range x | x.Coprime a}, ∀ a₂ ∈ {a ∈ range x | x.Coprime a}, d * a₁ = d * a₂ → a₁ = a₂

pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ a, ∃ (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b

Tactic:
· simp only [mem_filter, mem_range, and_imp, Coprime]
    refine fun a ha1 ha2 => ⟨by gcongr, ?_⟩
    rw [gcd_mul_left, ha2, mul_one]

Goal state after:
case inr.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ {a ∈ range x | x.Coprime a}, ∀ a₂ ∈ {a ∈ range x | x.Coprime a}, d * a₁ = d * a₂ → a₁ = a₂

case inr.i_surj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ b ∈ {k ∈ range (d * x) | (d * x).gcd k = d}, ∃ a, ∃ (_ : a ∈ {a ∈ range x | x.Coprime a}), d * a = b
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
p : α × α → Prop
⊢ (∀ᶠ (x : α × α) in atBot, p x) ↔ ∃ a, ∀ k ≤ a, ∀ l ≤ a, p (k, l)

Tactic:
by
  simp only [eventually_atBot_prod_self, forall_cond_comm]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ∀ (ns : ℕ → ι), Tendsto ns atTop l → ∃ ms, Tendsto (fun n ↦ x (ns (ms n))) atTop f
⊢ Tendsto x l f

Tactic:
contrapose! hxy
  obtain ⟨s, hs, hfreq⟩ : ∃ s ∈ f, ∃ᶠ n in l, x n ∉ s := by
    rwa [not_tendsto_iff_exists_frequently_notMem] at hxy
  obtain ⟨y, hy_tendsto, hy_freq⟩ := exists_seq_forall_of_frequently hfreq
  refine ⟨y, hy_tendsto, fun ms hms_tendsto ↦ ?_⟩
  rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩
  exact absurd hn <| hy_freq _

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

Goal state before:
pp: case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
apply le_of_mul_le_mul_right _ hd0

Goal state after:
a b : ℕ
d : ℕ := ⋯
ha0 : a > 0
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d
Module: Mathlib.Topology.ContinuousMap.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f; cases g; congr

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : ∃ n, c - b = n • p
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
rcases h with ⟨z, hz⟩
    rw [sub_eq_iff_eq_add] at hz
    rw [hz, toIocMod_zsmul_add]

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
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp x₁ x₃

Tactic:
rw [(not_modEq_iff_toIcoMod_eq_toIocMod hp).1 h] at h₂₃₄'

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ x₄ : α
h₁₂₃ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃ ∧ ¬toIcoMod hp x₃ x₂ ≤ toIocMod hp x₃ x₁
h₂₃₄ : toIcoMod hp x₂ x₄ ≤ toIocMod hp x₂ x₃ ∧ ¬toIcoMod hp x₃ x₄ ≤ toIocMod hp x₃ x₂
h : ¬x₃ ≡ x₂ [PMOD p]
h₁₂₃' : toIcoMod hp x₃ x₁ ≤ toIocMod hp x₃ x₂
h₂₃₄' : toIocMod hp x₃ x₂ ≤ toIocMod hp x₃ x₄
⊢ toIcoMod hp x₁ x₄ ≤ toIocMod hp 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
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed[inst✝] s ↔ IsClosed[inst✝] (f '' f ⁻¹' s)

Tactic:
image_preimage_eq_of_subset hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed[inst✝] s ↔ IsClosed[inst✝] s
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 X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ range f = g ⁻¹' range (g ∘ f)

Tactic:
rw [range_comp, hg.injective.preimage_image]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (X × X)
x : X
hx : s ∈ 𝓝 (x, x)
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ s

Tactic:
by
  simpa [nhds_prod_eq, (nhds_basis_opens x).prod_self.mem_iff, and_assoc, and_left_comm] using hx

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ IsClosed[instTopologicalSpaceSubtype] (s.domRestrict f ⁻¹' t) ↔ ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
isClosed_induced_iff,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsClosed[inst✝¹] t_1 ∧ Subtype.val ⁻¹' t_1 = s.domRestrict f ⁻¹' t) ↔
    ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ comap Subtype.val (𝓝 ↑a) ⊓ 𝓟 u ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
principal_subtype,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ comap Subtype.val (𝓝 ↑a) ⊓ comap Subtype.val (𝓟 (Subtype.val '' u)) ↔
    t ∈ comap Subtype.val (𝓝[Subtype.val '' 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
⊢ IsOpen[inst✝¹] (f ⁻¹' t)

Tactic:
convert! (continuousOn_open_iff hs).mp h t ht

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 = s ∩ f ⁻¹' t
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_2
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
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g

Tactic:
rw [(isOpenQuotientMap_snd (X := X)).isOpenMap_iff]
    exact isOpenMap_snd.comp h

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set Y
hu : IsOpen[inst✝] u
⊢ IsOpen[instTopologicalSpaceSum] (inr '' u)

Tactic:
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : { x // x ∈ s }), ↑x ∈ closure[inst✝] (val '' t)) ↔ s ⊆ closure[inst✝] ↑t

Tactic:
SetCoe.forall

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
t : Set ↑s
⊢ (∀ (x : X) (h : x ∈ s), ↑⟨x, h⟩ ∈ closure[inst✝] (val '' t)) ↔ s ⊆ closure[inst✝] ↑t
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : ↑g ⊆ s
⊢ (fun f ↦ ⋂₀ f) ↑g ∈ s

Tactic:
exact hsi.finiteInter_mem g hgs

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 ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
by
  rw [nhds_pi, pi_mem_pi_iff hI]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace ≤ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

case refine_2
ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s} ≤ Pi.topologicalSpace
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
hs : IsSeparable s
f : α → β
hf : Continuous[t, inst✝] f
⊢ IsSeparable (f '' s)

Tactic:
rcases hs with ⟨c, c_count, hc⟩
  refine ⟨f '' c, c_count.image _, ?_⟩
  rw [image_subset_iff]
  exact hc.trans (closure_subset_preimage_closure_image hf)

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 ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, IsOpen[⨅ i, t i] u

pp: case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
⊢ ∀ (a : β) (u : Set β),
    a ∈ u → IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u

Tactic:
· rintro - ⟨U, F, hU, rfl⟩
    refine isOpen_biInter_finset fun i hi ↦
      (h_basis i).isOpen (t := t i) (hU i hi) |>.mono (iInf_le _ _)

Goal state after:
case refine_2
β : Type u_1
ι : Type u_2
t : ι → TopologicalSpace β
T : ι → Set (Set β)
h_basis : ∀ (i : ι), IsTopologicalBasis (T i)
x✝ : TopologicalSpace β := ⨅ i, t i
⊢ ∀ (a : β) (u : Set β),
    a ∈ u → IsOpen[⨅ i, t i] u → ∃ v ∈ {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, U i}, a ∈ v ∧ v ⊆ u
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬↑f ≤ g

Tactic:
by
  rw [← inf_neBot_iff, neBot_iff, Ne, not_not, disjoint_iff]

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

Goal state before:
pp: α : Type u_1
⊢ ⊤.lift' powerset = ⊤

Tactic:
lift'_top,

Goal state after:
α : Type u_1
⊢ 𝓟 (𝒫 univ) = ⊤
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: case neg
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
rw [if_neg h]
        exact CompactSpace.isCompact_univ

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
by
  refine hs.compl_mem_sets fun x hx => ?_
  rcases hf x hx with ⟨t, ht, hst⟩
  replace ht := mem_inf_principal.1 ht
  apply mem_inf_of_inter ht hst
  rintro x ⟨h₁, h₂⟩ hs
  exact h₂ (h₁ hs)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
by
  refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩
  choose! U hxU hUl using fun x hx => (nhds_basis_opens x).disjoint_iff_left.1 (H x hx)
  choose hxU hUo using hxU
  rcases hs.elim_nhds_subcover U fun x hx => (hUo x hx).mem_nhds (hxU x hx) with ⟨t, hts, hst⟩
  refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩
  rw [compl_iUnion₂, biInter_finset_mem]
  exact fun x hx => hUl x (hts x hx)

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ⋃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
Ultrafilter.finite_biUnion_mem_iff hs

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
hl : ∃ i ∈ s, f i ∈ l
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x