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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
⊢ Unique (b ⟶ y)

Tactic:
let u : (LeftExtension.precomp₂ L' α).obj b ⟶
      (LeftExtension.precomp₂ L' α).obj y := hb.to _

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
⊢ Unique (b ⟶ y)
Module: Mathlib.CategoryTheory.Subobject.Comma

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
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ ((mk q).hom ≫ T.map (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)).hom) ≫ T.map (Hom.right f) =
    P.hom ≫ T.map (Hom.right f)

Tactic:
dsimp; simpa [← T.map_comp] using hq

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : IsIso f
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))

Tactic:
rw [isIso_iff_coyoneda_map_bijective] at h

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X : C
inst✝ : HasProduct (P.productToFamily X)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ P.productTo X = v ≫ P.productTo X
G : C
hG : P G
h : X ⟶ G
⊢ u ≫ h = v ≫ h

Tactic:
by simpa using huv =≫ P.πProductTo h hG

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ (ObjectProperty.singleton (unop G)).IsCodetecting ↔ (ObjectProperty.singleton G).IsDetecting

Tactic:
← isCodetecting_unop_iff,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ (ObjectProperty.singleton (unop G)).IsCodetecting ↔ (ObjectProperty.singleton G).unop.IsCodetecting
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
⊢ f = default

Tactic:
ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]

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

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
⊢ f = default

Tactic:
ext x
    have : x = 1 := Subsingleton.elim _ _
    rw [this, map_one, map_one]

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
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : (shrinkYoneda.{w, v₁, u₁}.obj X₁).obj (op u.fst)
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd)).toFun
      g =
    (ConcreteCategory.hom ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f)).toFun
      g

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X₁ X₂ : C
f : X₁ ⟶ X₂
u : F.Elements
g : unop (op u.fst) ⟶ X₁
⊢ (ConcreteCategory.hom
          ((shrinkYoneda.{w, v₁, u₁}.map f).app (op u.fst) ≫
            ↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd)).toFun
      (shrinkYonedaObjObjEquiv.symm g) =
    (ConcreteCategory.hom ((↾fun t ↦ (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv t))) u.snd) ≫ F.map f)).toFun
      (shrinkYonedaObjObjEquiv.symm g)
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: case snd
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).2 = (p, q).2

Tactic:
· exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mpr
X Y : Type u
c : BinaryCofan X Y
⊢ Injective ⇑(ConcreteCategory.hom c.inl) ∧
      Injective ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(ConcreteCategory.hom c.inl)) (Set.range ⇑(ConcreteCategory.hom c.inr)) →
    Nonempty (IsColimit c)

Tactic:
· rintro ⟨h₁, h₂, h₃⟩
      have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
        rw [eq_compl_iff_isCompl.mpr h₃.symm]
        exact fun _ => or_not
      refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩
      · intro T f g
        refine ↾fun x => ?_
        exact
          if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁).symm ⟨x, h⟩)
          else g ((Equiv.ofInjective _ h₂).symm ⟨x, (this x).resolve_left h⟩)
      · intro T f g
        ext x
        simp
      · 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
      · rintro T _ _ m rfl rfl
        ext x
        simp only [TypeCat.Fun.toFun_apply, Functor.const_obj_obj, pair_obj_left, Set.mem_range,
          comp_apply, pair_obj_right, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk]
        split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

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

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
⊢ Baer R M ↔ ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))

Tactic:
refine ⟨fun h I g ↦ ?_, fun h I g ↦ ?_⟩

Goal state after:
case refine_1
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ a, (LinearMap.lcomp R M (Submodule.subtype I)) a = g

case refine_2
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩
Module: Mathlib.Order.Circular

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

Tactic:
rcases le_total a b with hab | hba

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
⊢ btw a b c ∨ btw c b a

case inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hba : b ≤ a
⊢ btw a b c ∨ btw c b a
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Tactic:
simp only [sub_mem_Ioc_iff_right, sub_self, sub_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Periodic f c₁
h2 : Antiperiodic f c₂
⊢ Antiperiodic f (c₁ - c₂)

Tactic:
simpa only [sub_eq_add_neg] using h1.add_antiperiod h2.neg

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

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (r • ExtensionOfMaxAdjoin.fst i a) +
      (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (r • ExtensionOfMaxAdjoin.snd i a) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
⊢ ↑F ⊆ S → ⋂₀ ↑F ∈ S

Tactic:
by
  refine Finset.induction_on F (fun _ => ?_) ?_
  · simp [cond.univ_mem]
  · intro a s _ h1 h2
    suffices a ∩ ⋂₀ ↑s ∈ S by simpa
    exact
      cond.inter_mem (h2 (Finset.mem_insert_self a s))
        (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

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

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop

Tactic:
obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)

Goal state after:
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
⊢ ∃ xs, Monotone xs ∧ Tendsto xs atTop atTop
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

Tactic:
rotate_left

Goal state after:
case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
ψ : ℕ → ℕ
hψ : StrictMono ψ
hψφ : StrictMono (φ ∘ ψ)
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
exact ⟨φ ∘ ψ, hψφ, hφ.2.comp hψ.tendsto_atTop⟩

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

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

Tactic:
← totient_gcd_mul_totient_mul a b,

Goal state after:
a b : ℕ
d : ℕ := a.gcd b
ha0 : a > 0
hd0 : 0 < d
⊢ φ (a.gcd b) * φ (a * b) ≤ φ (a * b) * d
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
tfae_3_to_2 : toIcoMod hp a b ≠ toIocMod hp a b → ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
x✝ : toIcoMod hp a b + p = toIocMod hp a b
h : toIcoMod hp a b + p = toIocMod hp a b := x✝
⊢ toIcoMod hp a b ≠ toIocMod hp a b

Tactic:
rw [← h, Ne, eq_comm, add_eq_left]
    exact hp.ne'

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ⊆ interior s ∪ s ↔ IsClosed s

Tactic:
union_eq_right.mpr interior_subset,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s ⊆ s ↔ IsClosed s
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ 𝓟 univ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
principal_univ,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ ⊤ ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
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 : IsCoinducing g
hf : IsCoinducing f
⊢ coinduced g (coinduced f inst✝²) = coinduced (g ∘ f) inst✝²

Tactic:
coinduced_compose

Goal state after:
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 : IsCoinducing g
hf : IsCoinducing f
⊢ coinduced (g ∘ f) inst✝² = coinduced (g ∘ f) inst✝²
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
hf : IsQuotientMap f
⊢ coinduced g (coinduced f inst✝²) ≤ inst✝ ↔ coinduced (g ∘ f) inst✝² ≤ inst✝

Tactic:
coinduced_compose

Goal state after:
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
hf : IsQuotientMap f
⊢ coinduced (g ∘ f) inst✝² ≤ inst✝ ↔ coinduced (g ∘ f) inst✝² ≤ inst✝
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:
preimage_image_eq _ h₂,

Goal state after:
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
⊢ sᶜᶜ = s
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ 𝓟 univ = 𝓝 a

Tactic:
principal_univ,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝 a ⊓ ⊤ = 𝓝 a
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝 x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case inl
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : univ.pi s = ∅
⊢ IsSeparable (univ.pi s)

Tactic:
he

Goal state after:
case inl
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : univ.pi s = ∅
⊢ IsSeparable ∅
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ u, (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s

pp: case intro.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
· rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
    rw [← pi_inter_compl (I : Set ι)]
    exact inter_subset_left

Goal state after:
case intro.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
β : Type u_2
inst✝ : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
⊢ IsSeparable (s ×ˢ t)

Tactic:
rcases hs with ⟨cs, cs_count, hcs⟩
  rcases ht with ⟨ct, ct_count, hct⟩
  refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩
  rw [closure_prod_eq]
  gcongr

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ s ∈ ofComapInfPrincipal h

Tactic:
let f := Filter.comap m g ⊓ 𝓟 s

Goal state after:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ s ∈ ofComapInfPrincipal h
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
⊢ map m (ofComapInfPrincipal h) = g

Tactic:
let f := Filter.comap m g ⊓ 𝓟 s

Goal state after:
α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
⊢ map m (ofComapInfPrincipal h) = g
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_1
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ T ⊆ (fun x ↦ a ↑x) ⁻¹' t

Tactic:
rintro ⟨x, xu⟩ -

Goal state after:
case refine_1
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
x : α
xu : x ∈ u
⊢ ⟨x, xu⟩ ∈ (fun x ↦ a ↑x) ⁻¹' t
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ i ∈ s, S i)

Tactic:
biUnion_eq_iUnion

Goal state after:
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
s : Set ι
S : ι → Set X
hc : s.Countable
hcomp : ∀ i ∈ s, IsSigmaCompact (S i)
this : Countable ↑s
⊢ IsSigmaCompact (⋃ x, S ↑x)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed[inst✝] (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
by
    rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
    rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
    refine ⟨t, ?_⟩
    rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
K : Set X
hK : IsCompact K
l : Filter X
⊢ l ⊓ 𝓝ˢ K = ⨆ x ∈ K, l ⊓ 𝓝 x

Tactic:
simp only [inf_comm l, hK.nhdsSet_inf_eq_biSup]

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : DiscreteTopology X
⊢ cocompact X = cofinite

Tactic:
by
  simp only [cocompact, hasBasis_cofinite.eq_biInf, isCompact_iff_finite]

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).ker = {y | y ⤳ x}

Tactic:
by
  ext; simp [specializes_iff_pure, le_def]

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

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

Tactic:
refine ⟨?_⟩
  rw [Sigma.univ]
  exact isCompact_iUnion fun i => isCompact_range continuous_sigmaMk

Goal state after: