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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
⊢ e = 0

Tactic:
let u := biprod.desc e (0 : Y ⟶ R)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
b : ↑B
hb : h b = g b
r : b ∉ ↑(Hom.hom f).range
eq1 : (h b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
eq2 : (g b) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ = fromCoset ⟨b • ↑(Hom.hom f).range, ⋯⟩

Tactic:
by rw [← eq1, ← eq2, DFunLike.congr_fun hb]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ S₁.rightHomologyIso.inv ≫ rightHomologyMap φ = homologyMap φ ≫ S₂.rightHomologyIso.inv

Tactic:
simpa only [RightHomologyData.homologyIso_rightHomologyData, Iso.symm_inv] using!
    RightHomologyData.rightHomologyIso_hom_naturality φ S₁.rightHomologyData S₂.rightHomologyData

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
⊢ f' ≫ h.π = 0

Tactic:
simp only [hf'', assoc, f'_π, comp_zero]

Goal state after:
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
inst✝ : S.HasRightHomology
⊢ S.fromOpcycles.op ≫ S.cyclesOpIso.inv = S.op.toCycles

Tactic:
by
  dsimp [cyclesOpIso, fromOpcycles]
  rw [← cancel_mono S.op.iCycles, assoc, toCycles_i,
    LeftHomologyData.cyclesIso_inv_comp_iCycles, RightHomologyData.op_i,
    ← op_comp, RightHomologyData.p_g', op_f]

Goal state after:
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
hr : S.RightHomologyData
F : C ⥤ D
inst✝³ : F.PreservesZeroMorphisms
inst✝² : S.HasHomology
inst✝¹ : (S.map F).HasHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ S.mapHomologyIso' F = (hr.map F).homologyIso ≪≫ F.mapIso hr.homologyIso.symm

Tactic:
by
  ext
  dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, mapHomologyIso', homologyIso,
    rightHomologyIso, rightHomologyMapIso', ShortComplex.rightHomologyIso]
  simp only [assoc, F.map_comp, map_rightHomologyMap', ← rightHomologyMap'_comp_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ f ≫ (kernel.ι f.op).unop = 0

Tactic:
by
      rw [← f.unop_op, ← unop_comp, f.unop_op]
      simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0

Tactic:
by
      rw [← f.unop_op, ← unop_comp, f.unop_op]
      simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
have := h.hasHomology

Goal state after:
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
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.rightHomologyData.H = 0
⊢ (S.map F).Exact

Tactic:
rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
    ← F.map_id, h, F.map_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).Exact

Tactic:
have := h.hasHomology

Goal state after:
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
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesLeftHomologyOf S
inst✝ : F.PreservesRightHomologyOf S
this : S.HasHomology
⊢ (S.map F).Exact
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
⊢ a ≫ b = 0

Tactic:
have := h.hasHomology

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
this : S.HasHomology
⊢ a ≫ b = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
⊢ Mono S.g

Tactic:
have := h.hasHomology

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ Mono S.g
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
h : S.Exact
⊢ Epi S.f

Tactic:
have := h.hasHomology

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hg : S.g = 0
h : S.Exact
this : S.HasHomology
⊢ Epi S.f
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ mk i₁ < mk i₂

Tactic:
exfalso

Goal state after:
case inr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ False
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
s : Finset I
P : I → Subobject B
i : I
m : i ∈ s
⊢ (P i).Factors (s.inf P).arrow

Tactic:
by
  classical
  revert i m
  induction s using Finset.induction_on with
  | empty => rintro _ ⟨⟩
  | insert _ _ _ ih =>
    intro _ m
    rw [Finset.inf_insert]
    simp only [Finset.mem_insert] at m
    rcases m with (rfl | m)
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_left _ _)]
      exact factors_comp_arrow _
    · rw [← factorThru_arrow _ _ (inf_arrow_factors_right _ _)]
      apply factors_of_factors_right
      exact ih _ m

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X Y : A
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) L

Tactic:
by
    have := preservesEpimorphisms_of_map_exact _ hL
    apply preservesColimit_of_preserves_colimit_cocone (cokernelIsCokernel f)
    apply (CokernelCofork.isColimitMapCoconeEquiv _ L).2
    have : Epi ((ShortComplex.mk _ _ (cokernel.condition f)).map L).g := by
      dsimp
      infer_instance
    exact (hL (ShortComplex.mk _ _ (cokernel.condition f))
      (ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel f))).gIsCokernel

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

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

Tactic:
have : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ IsGrothendieckAbelian.{w, v₂, u₂} D

Tactic:
refine ⟨?_, hasFilteredColimits, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ LocallySmall.{w, v₂, u₂} D

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D
Module: Mathlib.CategoryTheory.Generator.Basic

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

Tactic:
← isCoseparating_unop_iff,

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

Goal state before:
pp: A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ RootableBy.root a ↑n ^ n = a

Tactic:
have := RootableBy.root_cancel a (show (n : ℤ) ≠ 0 from mod_cast hn)

Goal state after:
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
this : RootableBy.root a ↑n ^ ↑n = a
⊢ RootableBy.root a ↑n ^ n = a
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a b : ℕ
h : count p a < count p b
⊢ ∃ x ∈ Set.Ico a b, p x

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_lt (lt_of_count_lt_count h)
  rw [add_assoc, count_add, Nat.lt_add_right_iff_pos] at h
  obtain ⟨t, ht, hp⟩ := count_ne_iff_exists.mp h.ne'
  simp_rw [Set.mem_Ico]
  exact ⟨a + t, by grind⟩

Goal state after:
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 l : α), k ≤ a → l ≤ a → p (k, l)

Tactic:
by
  simp [← prod_atBot_atBot_eq, (@atBot_basis α _ _).prod_self.eventually_iff]

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIcoMod hp a a = a

Tactic:
rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]
  exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ toIocMod hp a (a + p) = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]
  exact ⟨lt_add_of_pos_right _ hp, 0, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Topology.Closure

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

Tactic:
← closure_compl,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier sᶜ = closure sᶜ ∩ (interior sᶜ)ᶜ
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 : α ⧸ AddSubgroup.zmultiples p
⊢ ↑((equivIcoMod ⋯ 0) (x - x)) ≤ ↑((equivIocMod ⋯ 0) (x - x))

Tactic:
simp [sub_self, hp'.out.le]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)

Tactic:
by
  rw [nhdsSet_union]
  exact union_mem_sup h₁ h₂

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.inter
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
s✝ t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) s✝
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

Tactic:
rcases h₁ with (rfl | rfl)

Goal state after:
case refl.refine_1.inter.inl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) ∅
⊢ ∅ ∩ t✝ = ∅ ∨ ∅ ∩ t✝ = univ

case refl.refine_1.inter.inr
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
t✝ : Set α
a✝¹ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) t✝
h₂ : t✝ = ∅ ∨ t✝ = univ
a✝ : TopologicalSpace.GenerateOpen (OrderDual.ofDual ⊤) univ
⊢ univ ∩ t✝ = ∅ ∨ univ ∩ t✝ = univ
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
⊢ h.trans h.symm = Homeomorph.refl X

Tactic:
ext
  apply symm_apply_apply

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
b : α
I₁ I₂ : Set α
hI : univ = I₁ ∪ I₂
⊢ 𝓝 b = 𝓝[I₁] b ⊔ 𝓝[I₂] b

Tactic:
rw [← nhdsWithin_univ b, hI, nhdsWithin_union]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
x : α
⊢ x ∈ s → ContinuousWithinAt f s x

Tactic:
xs

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (s.domRestrict f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[≠] a ⊔ 𝓝[{a}] a = 𝓝 a

Tactic:
← nhdsWithin_union,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}ᶜ ∪ {a}] a = 𝓝 a
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
x : ↑s
⊢ 𝓝[s ↓∩ t] x = ⊥ ↔ 𝓝[t] ↑x ⊓ 𝓟 s = ⊥

Tactic:
rw [inf_principal_eq_bot_iff_comap, nhdsWithin, nhdsWithin, comap_inf, comap_principal,
    nhds_induced]

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

Goal state before:
pp: case inr.mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
⊢ IsOpen[inst✝¹] s ∧ IsOpen[inst✝] t ∨ s = ∅ ∨ t = ∅ → IsOpen[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
intro H
      simp only [st.1.ne_empty, st.2.ne_empty, or_false] at H
      exact H.1.prod H.2

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
⊢ x ∈ s → ContinuousWithinAt f s x

Tactic:
xs

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
s : Set α
x : α
g : β → γ
t : Set β
y : β
hg : ContinuousWithinAt g t y
hf : ContinuousWithinAt f s x
h : MapsTo f s t
hy : f x = y
⊢ ContinuousWithinAt (g ∘ f) s x

Tactic:
by
  subst hy; exact hg.comp hf h

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case h
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ DirectedOn (𝓟 ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) {s | a ∈ s ∧ s ∈ b}

Tactic:
rintro s ⟨hs₁, hs₂⟩ t ⟨ht₁, ht₂⟩
    let ⟨u, hu₁, hu₂, hu₃⟩ := hb.1 _ hs₂ _ ht₂ _ ⟨hs₁, ht₁⟩
    exact ⟨u, ⟨hu₂, hu₁⟩, le_principal_iff.2 (hu₃.trans inter_subset_left),
      le_principal_iff.2 (hu₃.trans inter_subset_right)⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case ne
α : Type u
t : TopologicalSpace α
a : α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ {s | a ∈ s ∧ s ∈ b}.Nonempty

Tactic:
· rcases eq_univ_iff_forall.1 hb.sUnion_eq a with ⟨i, h1, h2⟩
    exact ⟨i, h2, h1⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : 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 : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ∃ I u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s

Tactic:
refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩

Goal state after:
case refine_1.refine_1
ι : 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 : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ IsOpen[T i] ((fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i) ∧
    a i ∈ (fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) i

case refine_1.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 : (i : ι) → Set (A i)
h1 : ∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1
h2 : (↑I).pi t ⊆ s
⊢ ((↑I).pi fun a_1 ↦ eval a_1 '' (↑I).pi fun a_2 ↦ ⋯.choose) ⊆ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:

Tactic:
f ×ˢ 𝓝ˢ t
    _ ≤ (𝓟 K) ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ (Filter.le_principal_iff.mpr hKf)
    _ ≤ 𝓝ˢ K ×ˢ 𝓝ˢ t := Filter.prod_mono_left _ principal_le_nhdsSet
    _ = 𝓝ˢ (K ×ˢ t) := (hK.nhdsSet_prod_eq ht).symm
    _ ≤ 𝓝ˢ (Set.univ ×ˢ t) := nhdsSet_mono (prod_mono_left le_top)

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ mk ⁻¹' mk '' s = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen[inst✝] s
⊢ mk ⁻¹' mk '' s ⊆ s
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ mk ⁻¹' mk '' s = s

Tactic:
refine Subset.antisymm ?_ (subset_preimage_image _ _)

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed[inst✝] s
⊢ mk ⁻¹' mk '' s ⊆ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ι
t : (i : ι) → Set (X i)
hs : s.Finite
ht : ∀ i ∈ s, IsCompact (t i)
⊢ IsCompact (⋃ i ∈ s, Sigma.mk i '' t i)

Tactic:
exact hs.isCompact_biUnion fun i hi ↦ (ht i hi).image continuous_sigmaMk

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
α : Type u_4
inst✝ : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
l : Filter α
⊢ Tendsto (lift f hf) (𝓝 (mk x)) l ↔ Tendsto f (𝓝 x) l

Tactic:
by
  simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]

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

Goal state before:
pp: case refine_3
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : T1Space X
inst✝¹ : DecidableEq X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
x : X
y : Y
x✝ : x ∈ s
⊢ ContinuousWithinAt (update f x y) s x ↔ Tendsto f (𝓝[s \ {x}] x) (𝓝 y)

Tactic:
exact continuousWithinAt_update_same

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 ∈ insert x s ↔ x_1 ∈ insert x t) ∧ (x ∈ insert x s ↔ x ∈ insert x t)

Tactic:
mem_insert_iff,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
x y : X
h : ∀ᶠ (x : X) in 𝓝[{y}ᶜ] x, x ∈ s ↔ x ∈ t
⊢ (∀ᶠ (x_1 : X) in 𝓝[≠] x, x_1 = x ∨ x_1 ∈ s ↔ x_1 = x ∨ x_1 ∈ t) ∧ (True ∨ x ∈ s ↔ True ∨ x ∈ t)
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a

Tactic:
by
  simp only [← Ici_sdiff_left, continuousWithinAt_sdiff_self]

Goal state after:
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
← nhdsWithin_union,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[Iic a ∪ Ici a] a = 𝓝 a