mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ rightHomologyMap' (𝟙 S) h S.rightHomologyData ≫ S.rightHomologyData.ι = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData

Tactic:
rightHomologyι_naturality'

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData = h.ι ≫ opcyclesMap' (𝟙 S) h S.rightHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

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✝⁵ : HasZeroMorphisms C
inst✝⁴ : HasZeroMorphisms D
S : ShortComplex C
hl : S.LeftHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesLeftHomologyOf S
⊢ S.mapHomologyIso F = (hl.map F).homologyIso ≪≫ F.mapIso hl.homologyIso.symm

Tactic:
by
  ext
  dsimp only [mapHomologyIso, homologyIso, ShortComplex.leftHomologyIso,
    leftHomologyMapIso', leftHomologyIso, Functor.mapIso,
    Iso.symm, Iso.trans, Iso.refl]
  simp only [map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, Functor.map_id,
    Functor.mapShortComplex_obj]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C

Tactic:
all_goals intro H; constructor; intro X; constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f + Hom.τ₂ 0

Tactic:
rw [nullHomotopic_τ₂, zero_τ₂, add_zero]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ h₁ ≫ S₂.f + S₁.g ≫ h₂ = S₁.g ≫ h₂ + h₁ ≫ S₂.f
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ (S.map F).ShortExact

Tactic:
have := hS.mono_f
  have := hS.epi_g
  exact hS.map F

Goal state after:
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
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
⊢ j.essImage A

Tactic:
have : IsIso (ε.app (j.obj ((coreflector j).obj A))) :=
    Functor.essImage.counit_isIso ((j.obj_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
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
this : IsIso (ε.app (j.obj ((coreflector j).obj A)))
⊢ j.essImage A
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
inst✝ : IsSplitEpi ((coreflectorAdjunction j).counit.app A)
ε : coreflector j ⋙ j ⟶ 𝟭 D := (coreflectorAdjunction j).counit
this : IsIso (ε.app (j.obj ((coreflector j).obj A)))
⊢ Mono ((coreflector j ⋙ j).map (section_ (ε.app A)) ≫ ε.app ((coreflector j ⋙ j).obj A))

Tactic:
apply mono_comp _ (ε.app (j.obj ((coreflector j).obj A)))

Goal state after:
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
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ h₁.hom = h₂.hom

Tactic:
apply Over.OverMorphism.ext

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ Over.Hom.left h₁.hom = Over.Hom.left h₂.hom
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }.Exact

Tactic:
by
  symm
  exact ShortComplex.exact_iff_of_epi_of_isIso_of_mono
    { τ₁ := 𝟙 _
      τ₂ := 𝟙 _
      τ₃ := Abelian.factorThruCoimage S.g }

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c.ι.app { as := j } ≫ (hc.desc c').op.unop).op =
    (c.ι.app { as := j } ≫ (hf.lift c'.op ≫ (opCoproductIsoProduct' hc hf).inv).unop).op

Tactic:
simp only [unop_op, Discrete.functor_obj, Quiver.Hom.unop_op, IsColimit.fac,
    Cofan.op, unop_comp, op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hf : IsLimit f
c' : Cofan Z
x✝ : Discrete α
j : α
⊢ (c'.ι.app { as := j }).op =
    hf.lift (Fan.mk (op c'.pt) fun a ↦ (c'.inj a).op) ≫ (opCoproductIsoProduct' hc hf).inv ≫ (c.ι.app { as := j }).op
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
Y : C
η : yoneda.obj Y ⟶ A
X : C
s : yoneda.obj X ⟶ A
f : X ⟶ Y
hf : yoneda.map f ≫ η = s
⊢ MakesOverArrow η s f

Tactic:
simpa only [yonedaEquiv_yoneda_map f] using of_arrow hf

Goal state after:
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
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ StructuredArrow.IsUniversal (LeftExtension.mk F₁ α.hom)

Tactic:
apply LeftExtension.isUniversalPostcomp₁Equiv
    (G := L.functor) L.functor.leftUnitor F₀ _ |>.invFun

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
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ≅ L.functor ⋙ F₁
⊢ StructuredArrow.IsUniversal
    ((LeftExtension.postcomp₁ L.functor L.functor.leftUnitor.inv F₀).obj (LeftExtension.mk F₁ α.hom))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x j, Mono j
⊢ P.IsCoseparating

Tactic:
intro X Y f g h
  obtain ⟨ι, s, hs, c, hc, j, _⟩ := hP Y
  rw [← cancel_mono j]
  exact Fan.IsLimit.hom_ext hc _ _
    (fun i ↦ by simpa using h _ (hs i) (j ≫ c.proj i))

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
𝒢 : ObjectProperty C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ P = Q

Tactic:
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
  refine h𝒢 _ fun G hG f => ?_
  have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
  refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
  · simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]
  · simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
      ofLE_arrow, factorThru_arrow]

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ PreservesFiniteLimits colim

Tactic:
by
  apply Functor.preservesFiniteLimits_of_preservesHomology

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l))
⊢ ∃ h, ∀ (x : X), h (f x) = (ModuleCat.Hom.hom (ModuleCat.ofHom f ≫ l)) x

Tactic:
exact ⟨l.hom, fun _ => rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (match -[a✝+1] with
      | ofNat n => RootableBy.root a n
      | -[n+1] => (RootableBy.root a (n + 1))⁻¹) ^
      -[a✝+1] =
    a

Tactic:
· simp [RootableBy.root_cancel _ (Nat.add_one_ne_zero _)]

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

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

Tactic:
rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
      ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)
Module: Mathlib.Algebra.Order.Interval.Set.Group

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

Tactic:
simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case inter
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q ∈ S, T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
rcases h1 with (h | ⟨Q, hQ, rfl⟩)

Goal state after:
case inter.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
h : T1 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

case inter.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)

Tactic:
by
  rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩
  exact totient_prime_pow_succ hp _

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p b

Tactic:
rw [← Nat.div_add_mod b n]

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
⊢ p (n * (b / n) + b % n)
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 : α
m : ℤ
⊢ toIcoMod hp a (b + m • p) = toIcoMod hp a b

Tactic:
rw [toIcoMod, toIcoDiv_add_zsmul, toIcoMod, add_smul]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s

Tactic:
simp only [hs, le_principal_iff]

Goal state after:
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)
⊢ l ⊓ 𝓟 s ≤ comap f (𝓝 x) ↔ l ≤ comap f (𝓝 x)

Tactic:
refine ⟨fun h' => ?_, le_trans inf_le_left⟩

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)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
m : ℤ
⊢ toIcoDiv hp a (b + ↑m * p) = toIcoDiv hp a b + m

Tactic:
by
  simpa using toIcoDiv_add_zsmul hp a b m

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

Goal state before:
pp: case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
⊢ p x ∈ g ⁻¹' q '' V → p x ∈ U

Tactic:
rintro ⟨y, hy, e'⟩

Goal state after:
case mp.mp
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
V : Set B
hV : IsOpen[inst✝¹] V
e : f ⁻¹' V = p ⁻¹' U
x : A
y : B
hy : y ∈ V
e' : q y = g (p x)
⊢ p x ∈ U
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y

Tactic:
rcases eq_or_ne a a₀ with (rfl | ha)

Goal state after:
case inl
α : Type u
inst✝ : DecidableEq α
l : Filter α
b a : α
s : Set α
h : pure a ≤ l
hs : s ∈ update pure a l a
⊢ ∀ᶠ (y : α) in update pure a l a, s ∈ update pure a l y

case inr
α : Type u
inst✝ : DecidableEq α
a₀ : α
l : Filter α
h : pure a₀ ≤ l
b a : α
s : Set α
hs : s ∈ update pure a₀ l a
ha : a ≠ a₀
⊢ ∀ᶠ (y : α) in update pure a₀ l a, s ∈ update pure a₀ l y
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.basic
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
s✝ : Set α
h : s✝ ∈ OrderDual.ofDual ⊤
⊢ s✝ = ∅ ∨ s✝ = univ

Tactic:
| basic _ h =>

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ MapClusterPt (f x) l f ↔ ClusterPt x l

Tactic:
delta MapClusterPt ClusterPt

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
x : X
l : Filter X
⊢ (𝓝 (f x) ⊓ map f l).NeBot ↔ (𝓝 x ⊓ l).NeBot
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → IsOpen[t₁] s

Tactic:
@isOpen_iff_mem_nhds _ t₁,

Goal state after:
α : Type u_1
t₁ t₂ : TopologicalSpace α
h : ∀ (x : α), 𝓝 x ≤ 𝓝 x
s : Set α
⊢ IsOpen[t₂] s → ∀ x ∈ s, s ∈ 𝓝 x
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : Y
⊢ (h.symm.trans h) x✝ = (Homeomorph.refl Y) x✝

Tactic:
apply apply_symm_apply

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
h : t ∈ 𝓝[s] a
⊢ insert a t ∈ 𝓝[insert a s] a

Tactic:
simp [mem_of_superset h]

Goal state after:
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 ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
by
  simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ s.OrdConnected ↔ ↑(upperClosure s) ∩ ↑(lowerClosure s) = s

Tactic:
refine ⟨Set.OrdConnected.upperClosure_inter_lowerClosure, fun h => ?_⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : ↑(upperClosure s) ∩ ↑(lowerClosure s) = s
⊢ s.OrdConnected
Module: Mathlib.Order.UpperLower.CompleteLattice

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s t : UpperSet α
⊢ Codisjoint ↑s ↑t ↔ Disjoint s t

Tactic:
by
  simp [disjoint_iff, codisjoint_iff, SetLike.ext'_iff]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z

Tactic:
rw [Set.compl_subset_iff_union, ← Set.sUnion_singleton Z, ← Set.sUnion_union,
      Set.sUnion_singleton, Set.sdiff_union_of_subset, sUnion_irreducibleComponents]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
⊢ {Z} ⊆ irreducibleComponents X
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
⊢ IsClosed[inst✝] (U \ s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_eventually]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
⊢ ∀ x ∈ (U \ s)ᶜ, ∀ᶠ (y : X) in 𝓝 x, y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

Tactic:
rw [← Set.inter_eq_right.mpr h]

Goal state after:
case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible univ

Tactic:
← Set.preimage_univ

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ IsPreirreducible (?m.12 ⁻¹' univ)

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Type ?u.22

X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : Y → X
hf : IsOpenEmbedding f
inst✝ : PreirreducibleSpace X
⊢ Y → ?m.11
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f s a ↔ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a

Tactic:
continuousWithinAt_iff_continuous_left_right

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
s : Set α
a : α
f : α → β
⊢ ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a ↔
    ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ mk x = mk y

Tactic:
mk_eq_mk,

Goal state after:
case refine_2.mk.mk
X : Type u_1
inst✝ : TopologicalSpace X
h : Std.Symm Specializes
x✝ : SeparationQuotient X
x : X
y✝ : SeparationQuotient X
y : X
sxspecsy : Quot.mk (⇑(inseparableSetoid X)) x ⤳ Quot.mk (⇑(inseparableSetoid X)) y
xspecy : x ⤳ y
yspecx : y ⤳ x
⊢ Inseparable x y
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ IsOpen[inst✝] s ↔ frontier s = ∅

Tactic:
← interior_eq_iff_isOpen,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure[inst✝] s = s ∧ interior s = s ↔ frontier s = ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
H : ∀ x ∈ ∅, ∀ y ∈ ∅, ∃ t ⊆ ∅, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected ∅

pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
H : ∀ x ∈ s, ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
x : α
hx : x ∈ s
⊢ IsPreconnected s

Tactic:
exacts [isPreconnected_empty, isPreconnected_of_forall x fun y => H x hx y]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ IsConnected s ↔ (∃ t, IsConnected t ∧ s = inl '' t) ∨ ∃ t, IsConnected t ∧ s = inr '' t

Tactic:
by
  refine ⟨fun hs => ?_, ?_⟩
  · obtain ⟨x | x, hx⟩ := hs.nonempty
    · have h : s ⊆ range Sum.inl :=
        hs.isPreconnected.subset_isClopen isClopen_range_inl ⟨.inl x, hx, x, rfl⟩
      refine Or.inl ⟨Sum.inl ⁻¹' s, ?_, ?_⟩
      · exact hs.preimage_of_isOpenMap Sum.inl_injective isOpenMap_inl h
      · exact (image_preimage_eq_of_subset h).symm
    · have h : s ⊆ range Sum.inr :=
        hs.isPreconnected.subset_isClopen isClopen_range_inr ⟨.inr x, hx, x, rfl⟩
      refine Or.inr ⟨Sum.inr ⁻¹' s, ?_, ?_⟩
      · exact hs.preimage_of_isOpenMap Sum.inr_injective isOpenMap_inr h
      · exact (image_preimage_eq_of_subset h).symm
  · rintro (⟨t, ht, rfl⟩ | ⟨t, ht, rfl⟩)
    · exact ht.image _ continuous_inl.continuousOn
    · exact ht.image _ continuous_inr.continuousOn

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (𝓝 b).HasBasis (?m.10 b) (?m.11 b)

Tactic:
by rw [hf.nhds_eq_comap b]; exact (closed_nhds_basis _).comap _

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

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t : Set X✝
X : ι → Type u_2
inst✝² : Countable ι
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LindelofSpace (X i)
⊢ IsLindelof univ

Tactic:
rw [Sigma.univ]
    exact isLindelof_iUnion fun i => isLindelof_range continuous_sigmaMk

Goal state after: