mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso' F).hom =
    (S₁.mapHomologyIso' F).hom ≫ F.map (homologyMap φ)

Tactic:
dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']

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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫
      (S₂.homologyData.right.map F).homologyIso.hom ≫ F.map S₂.homologyData.right.homologyIso.inv =
    ((S₁.homologyData.right.map F).homologyIso.hom ≫ F.map S₁.homologyData.right.homologyIso.inv) ≫
      F.map (homologyMap φ)
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ ∃ h, f ≫ h = g

Tactic:
by
    refine ⟨biproduct.lift fun b => factorThru (g ≫ biproduct.π _ _) f, ?_⟩
    ext
    simp only [Category.assoc, biproduct.lift_π, comp_factorThru]

Goal state after:
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
inst✝² : S.HasHomology
inst✝¹ : HasKernel S.g
inst✝ : HasCokernel S.f
this✝ : HasCokernel (kernel.lift S.g S.f ⋯)
this : HasKernel (cokernel.desc S.f S.g ⋯)
⊢ S.Exact ↔ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
exact S.exact_iff_i_p_zero (LeftHomologyData.ofHasKernelOfHasCokernel S)
    (RightHomologyData.ofHasCokernelOfHasKernel S)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ Y.arrow = X.arrow
⊢ X ≤ Y

Tactic:
convert! mk_le_mk_of_comm _ w <;> simp

Goal state after:
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 ↔ Epi (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel']
  apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
  exact Arrow.isoMk (imageSubobjectIso S.f).symm (kernelSubobjectIso S.g).symm

Goal state after:
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 ↔ IsIso (imageToKernel' S.f S.g ⋯)

Tactic:
simp only [S.exact_iff_epi_imageToKernel', isIso_iff_mono_and_epi, iff_and_self]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel' S.f S.g ⋯) → Mono (imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
⊢ [Mono f, kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE

Tactic:
by
  tfae_have 2 → 1 := mono_of_kernel_ι_eq_zero _
  tfae_have 1 → 2
  | _ => by rw [← cancel_mono f, kernel.condition, zero_comp]
  tfae_have 3 ↔ 1 := ShortComplex.exact_iff_mono _ (by simp)
  tfae_finish

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f₁ : MonoOver A
f₂ : Subobject A
⊢ (inf.obj (Quotient.mk'' f₁)).obj f₂ = (map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)

Tactic:
by
  induction f₂ using Quotient.inductionOn'
  rfl

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

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
L✝ : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limMap (L.ran.map f) ≫ ((L.ran.obj Y✝).limitIsoOfIsRightKanExtension (L.ranCounit.app Y✝)).hom ≫ limit.π Y✝ i =
    limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ranCounit.app X✝).app i ≫ f.app i

Tactic:
limitIsoOfIsRightKanExtension_hom_π,

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
L✝ : C ⥤ D
H : Type u_3
inst✝⁴ : Category.{v_3, u_3} H
inst✝³ : ∀ (F : C ⥤ H), L✝.HasRightKanExtension F
L : C ⥤ D
inst✝² : ∀ (G : C ⥤ H), L.HasRightKanExtension G
inst✝¹ : HasLimitsOfShape C H
inst✝ : HasLimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ limMap (L.ran.map f) ≫ limit.π (L.ran.obj Y✝) (L.obj i) ≫ (L.ranCounit.app Y✝).app i =
    limit.π (L.ran.obj X✝) (L.obj i) ≫ (L.ranCounit.app X✝).app i ≫ f.app i
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsFiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
h : j.right ≤ i.right
⊢ Nonempty (j ⟶ i)

Tactic:
exact ⟨StructuredArrow.homMk (homOfLE h) rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ (hom (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) })).toFun x =
    (hom
          ((↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
            ((restrictedULiftYoneda A).obj E).map g)).toFun
      x

Tactic:
let φ : CostructuredArrow.mk (uliftYonedaEquiv.{max w v₂}.symm (P.map g x)) ⟶
          CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
            CostructuredArrow.homMk g.unop (by
              dsimp
              rw [uliftYonedaEquiv_symm_map])

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
φ : CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (P.map g)) x)) ⟶ CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ (hom (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) })).toFun x =
    (hom
          ((↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
            ((restrictedULiftYoneda A).obj E).map g)).toFun
      x
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj X = F.obj X

Tactic:
by cases X <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j ↦ F.map (line j)).obj X

Tactic:
by cases X <;> cat_disch

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

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ T
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ (isoMk (Subobject.underlyingIso f.unop.left.op).unop ⋯).op.hom ≫ f =
    (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq).op

Tactic:
· exact Quiver.Hom.unop_inj (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
X : WalkingParallelFamily J
⊢ F.obj X = (parallelFamily fun j ↦ F.map (line j)).obj X

Tactic:
by cases X <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X✝ Y : C
f : J → (X✝ ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
X : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj X = F.obj X

Tactic:
by cases X <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case one
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one

Tactic:
· simpa using w =≫ f (Classical.arbitrary J)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
this : ∀ (X : K), Epi ((whiskerRight f H).app X)
⊢ Epi (whiskerRight f H)

Tactic:
apply NatTrans.epi_of_epi_app

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
⊢ f = g

Tactic:
ext P : 3

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
f g : Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom ⟶ Φ
P : Cᵒᵖ ⥤ Type (max (max w v₁) v₂)
⊢ (StructuredArrow.Hom.right f).app P = (StructuredArrow.Hom.right g).app P
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
c : Fan f
hc : IsLimit c
⊢ IsCoseparator c.pt ↔ (ObjectProperty.ofObj f).IsCoseparating

Tactic:
by
  refine ⟨fun h X Y u v huv => ?_, fun h => isCoseparator_of_isLimit_fan h hc⟩
  refine h.def _ _ fun g => hc.hom_ext fun b => ?_
  simpa using! huv (f b.as) (by simp) (g ≫ c.proj _)

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (yoneda.obj G).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
this : IsIso ((yoneda.obj G).map f.op)
⊢ IsIso f.op

Tactic:
by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h

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

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
⊢ Function.Injective (c.inj i)

Tactic:
intro y₁ y₂ h
  simpa using (equivOfIsColimit hc).injective (a₁ := ⟨i, y₁⟩) (a₂ := ⟨i, y₂⟩) h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : SubtractionCommMonoid α
h : Periodic f c
a : α
⊢ Periodic (fun x ↦ f (x - a)) c

Tactic:
by
  simpa only [sub_eq_add_neg] using h.add_const (-a)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : SubtractionCommMonoid α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (fun x ↦ f (x - a)) c

Tactic:
by
  simpa only [sub_eq_add_neg] using h.add_const (-a)

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

Goal state before:
pp: case inr.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ (d * x).gcd (d * a) = d

Tactic:
gcd_mul_left,

Goal state after:
case inr.hi
d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ d * x.gcd a = d
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : (d * x).gcd (d * q) = d
⊢ x.Coprime q

Tactic:
gcd_mul_left,

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x q : ℕ
hb1 : d * q < d * x
hb2 : d * x.gcd q = d
⊢ x.Coprime q
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 + p) = a

Tactic:
by
  rw [toIcoMod_eq_iff hp, Set.left_mem_Ico]
  exact ⟨lt_add_of_pos_right _ hp, 1, 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 : α
⊢ b - toIocDiv hp (a + c) b • p ∈ Set.Ioc (a + c) (a + c + p)

Tactic:
exact sub_toIocDiv_zsmul_mem_Ioc hp (a + c) b

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
ι : Sort v
inst✝¹ : TopologicalSpace X
inst✝ : Finite ι
s : ι → Set X
h : ∀ (i : ι), IsClosed[inst✝¹] (s i)
⊢ IsClosed[inst✝¹] (⋃ i, s i)

Tactic:
by
  simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact isOpen_iInter_of_finite h

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 x✝ : α
⊢ toIcoMod hp a x✝ = toIocMod hp a x✝ ↔ ∃ i, x✝ ∈ Set.Ioo (a + i • p) (a + p + i • p)

Tactic:
← Set.sub_mem_Ioo_iff_left,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ toIcoMod hp a x✝ = toIocMod hp a x✝ ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x F ↔ (F.lift' closure[inst✝] ⊓ pure x).NeBot

Tactic:
by
  rw [clusterPt_iff_lift'_closure, inf_comm]
  constructor
  · intro h
    simp [h, pure_neBot]
  · intro h U hU
    simp_rw [← forall_mem_nonempty_iff_neBot, mem_inf_iff] at h
    simpa using h ({x} ∩ U) ⟨{x}, by simp, U, hU, rfl⟩

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

Goal state before:
pp: case H.H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝³ z✝² z✝¹ : α
h₁₂₃ : btw ↑z✝³ ↑z✝² ↑z✝¹ ∧ ¬btw ↑z✝¹ ↑z✝² ↑z✝³
z✝ : α
h₂₃₄ : btw ↑z✝² ↑z✝ ↑z✝¹ ∧ ¬btw ↑z✝¹ ↑z✝ ↑z✝²
⊢ btw ↑z✝³ ↑z✝ ↑z✝¹ ∧ ¬btw ↑z✝¹ ↑z✝ ↑z✝³

Tactic:
simp_rw [btw_coe_iff] at h₁₂₃ h₂₃₄ ⊢

Goal state after:
case H.H.H.H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
n : ℤ
hp' : Fact (0 < p)
z✝³ z✝² z✝¹ z✝ : α
h₁₂₃ : toIcoMod ⋯ z✝³ z✝² ≤ toIocMod ⋯ z✝³ z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝² ≤ toIocMod ⋯ z✝¹ z✝³
h₂₃₄ : toIcoMod ⋯ z✝² z✝ ≤ toIocMod ⋯ z✝² z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝ ≤ toIocMod ⋯ z✝¹ z✝²
⊢ toIcoMod ⋯ z✝³ z✝ ≤ toIocMod ⋯ z✝³ z✝¹ ∧ ¬toIcoMod ⋯ z✝¹ z✝ ≤ toIocMod ⋯ z✝¹ z✝³
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Ico (n • p) ((n + 1) • p) = univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_zsmul hp 0

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'⟩
      obtain ⟨y, rfl⟩ := H ⟨_, ⟨x, rfl⟩, (e'.trans (congr_fun h x)).symm⟩
      rw [← hg ((congr_fun h y).trans e')]
      exact e.le hy

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

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t U V : Set X
U_open : IsOpen[inst✝] U
V_open : IsOpen[inst✝] V
h_sub_U : s ⊆ U
k_sub_V : t ⊆ V
UV_dis : Disjoint U V
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
exact
      ⟨⟨fun _ ↦ U,
        h_sub_U.trans (iUnion_const U).symm.subset,
        fun _ ↦
          ⟨U_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) k_sub_V (UV_dis.closure_left V_open)⟩⟩,
       ⟨fun _ ↦ V,
        k_sub_V.trans (iUnion_const V).symm.subset,
        fun _ ↦
          ⟨V_open, disjoint_of_subset (fun ⦃a⦄ a ↦ a) h_sub_U (UV_dis.closure_right U_open).symm⟩⟩⟩

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := nhdsAdjoint a f
t : Set α
hat : a ∈ t
htf : t ∈ f
⊢ t ∈ 𝓝 a

Tactic:
exact IsOpen.mem_nhds (fun _ ↦ htf) hat

Goal state after:
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
y : Y
⊢ comap (⇑h) (𝓝 y) = comap (⇑h) (𝓝 (h (h.symm y)))

Tactic:
h.apply_symm_apply

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
y : Y
⊢ comap (⇑h) (𝓝 y) = comap (⇑h) (𝓝 y)
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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ (map f (F.lift' closure[inst✝¹]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
← comap_principal,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ (map f (F.lift' closure[inst✝¹]) ⊓ pure y).NeBot ↔ (F.lift' closure[inst✝¹] ⊓ comap f (𝓟 {y})).NeBot
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 : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (𝓟 (f ⁻¹' {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)

Tactic:
← comap_principal,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
x : X
l : Filter Y
⊢ ClusterPt x (comap f (𝓟 {f x}ᶜ) ⊓ comap f l) ↔ ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: Y : Type v
Z : Type u_2
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
X : Type u_5
seq : X → Y × Z
f : Filter X
p : Y × Z
⊢ Tendsto seq f (𝓝 p) ↔ Tendsto (fun n ↦ (seq n).1) f (𝓝 p.1) ∧ Tendsto (fun n ↦ (seq n).2) f (𝓝 p.2)

Tactic:
rw [nhds_prod_eq, Filter.tendsto_prod_iff']

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ i ∈ {t | a ∈ t ∧ IsOpen[inst✝] t}, Tendsto f l (𝓟 (i ∩ s))
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
mem_ofPred_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen[inst✝] i → Tendsto f l (𝓟 (i ∩ s))
⊢ ∀ᶠ (i : β) in l, f i ∈ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : 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 = Subtype.val ⁻¹' f ⁻¹' t) ↔
    ∃ u, IsClosed[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
simp only [Subtype.preimage_coe_eq_preimage_coe_iff, eq_comm, Set.inter_comm s]

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

Goal state before:
pp: 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
f : X → Y
g : Z → W
hf : IsInducing f
hg : IsInducing g
x✝ : X × Z
x : X
z : Z
⊢ 𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))

Tactic:
by simp_rw [Prod.map_def, nhds_prod_eq, hf.nhds_eq_comap,
    hg.nhds_eq_comap, prod_comap_comap_eq]

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

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
⊢ (IsInducing f ∧ Injective f) ∧
      (IsInducing g ∧ Injective g) ∧
        Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g)) →
    (IsInducing f ∧
        IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
      Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
intro ⟨⟨hf₁, hf₂⟩, ⟨hg₁, hg₂⟩, hFg, hfG⟩

Goal state after:
case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ (IsInducing f ∧
      IsInducing g ∧ Disjoint (closure[inst✝] (range f)) (range g) ∧ Disjoint (range f) (closure[inst✝] (range g))) ∧
    Injective f ∧ Injective g ∧ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
refine ⟨⟨hf₁, hg₁, hFg, hfG⟩, ⟨hf₂, hg₂, ?_⟩⟩

Goal state after:
case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ ∀ (a : X) (b : Y), f a ≠ g b
Module: Mathlib.Topology.Ultrafilter

Goal state before:
pp: X : Type u
x : X
inst✝ : TopologicalSpace X
f : Filter X
⊢ ClusterPt x f ↔ ∃ u, ↑u ≤ f ∧ ↑u ≤ 𝓝 x

Tactic:
simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Goal state after: