mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ (ofMkLEMk g f h ≫ f).unop = 0

Tactic:
unop_comp,

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ f.unop ≫ (ofMkLEMk g f h).unop = 0
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:
revert i m

Goal state after:
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 ∈ s, (P i).Factors (s.inf P).arrow
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✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ IsIso ((L.lanAdjunction H).unit.app F)

Tactic:
by
  rw [lanAdjunction_unit]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
q : YonedaCollection F X
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
h : fst ⟨p, p'⟩ = q.fst
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) q.snd = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = q

Tactic:
rcases q with ⟨q, q'⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
p : A.obj (op X)
p' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm p)))
q : A.obj (op X)
q' : F.obj (op (CostructuredArrow.mk (yonedaEquiv.symm q)))
h : fst ⟨p, p'⟩ = fst ⟨q, q'⟩
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) (snd ⟨q, q'⟩) = snd ⟨p, p'⟩
⊢ ⟨p, p'⟩ = ⟨q, q'⟩
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₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y)) (uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop)) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))

Tactic:
rw [uliftYonedaEquiv_apply, uliftYonedaEquiv_apply,
          ← NatTrans.naturality_apply]

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₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.map f.unop).app (op (unop Y)))) { down := 𝟙 (unop Y) }) =
    (hom ((s.ι.app (op (P.elementsMk X x))).app Y))
      ((hom ((uliftYoneda.{w, v₁, u₁}.obj (unop X)).map f)) { down := 𝟙 (unop X) })
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
⊢ ∃! h', f.unop ≫ h' = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f

Tactic:
refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
⊢ ∃! h', h' ≫ f.unop = h
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case i.refine_2
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
⊢ S.map (Subobject.underlyingIso f.unop.left.op).unop.hom ≫ (mk q).hom = (unop P).hom

Tactic:
refine (cancel_epi (S.map f.unop.left)).1 ?_

Goal state after:
case i.refine_2
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
⊢ S.map f.unop.left ≫ S.map (Subobject.underlyingIso f.unop.left.op).unop.hom ≫ (mk q).hom =
    S.map f.unop.left ≫ (unop P).hom
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v, u'} D
inst✝³ : HasLimits D
inst✝² : WellPowered.{v, v, u'} D
P : ObjectProperty D
inst✝¹ : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : D ⥤ C
inst✝ : PreservesLimits G
⊢ G.IsRightAdjoint

Tactic:
have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦
    hasInitial_of_isCoseparating.{v} (StructuredArrow.isCoseparating_inverseImage_proj A G hP)

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v, u'} D
inst✝³ : HasLimits D
inst✝² : WellPowered.{v, v, u'} D
P : ObjectProperty D
inst✝¹ : ObjectProperty.Small.{v, v, u'} P
hP : P.IsCoseparating
G : D ⥤ C
inst✝ : PreservesLimits G
this : ∀ (A : C), HasInitial (StructuredArrow A G)
⊢ G.IsRightAdjoint
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ f ≫
      F.op.lanUnit.app Q ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    presheafHom φ P ≫ F.op.whiskerLeft (G.map f)

Tactic:
Functor.descOfIsLeftKanExtension_fac,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ f ≫ presheafHom φ Q = presheafHom φ P ≫ F.op.whiskerLeft (G.map f)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsDetector (op G) ↔ IsCodetector G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsDetector G ↔ (coyoneda.obj (op G)).ReflectsIsomorphisms

Tactic:
refine
    ⟨fun hG => ⟨fun f hf => hG.def _ fun h => ?_⟩, fun h =>
      (isDetector_def _).2 fun X Y f hf => ?_⟩
  · rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
    exact hf h
  · suffices IsIso ((coyoneda.obj (op G)).map f) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
    rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A : AddCommGrpCat
⊢ ∀ ⦃Y : AddCommGrpCat⦄ (f g : A ⟶ Y),
    (∀ (G : AddCommGrpCat),
        ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g) →
      f = g

Tactic:
B

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
A B : AddCommGrpCat
⊢ ∀ (f g : A ⟶ B),
    (∀ (G : AddCommGrpCat),
        ObjectProperty.singleton (AddCommGrpCat.of (ULift.{u, 0} ℤ)) G → ∀ (h : G ⟶ A), h ≫ f = h ≫ g) →
      f = g
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
this :
  IsTerminal
    (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt) ≅
    (overEquivPresheafCostructuredArrow c.pt).inverse.obj
      (colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ yoneda))

Tactic:
refine ?_ ≪≫ (preservesColimitIso (overEquivPresheafCostructuredArrow c.pt).inverse _).symm

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

Goal state before:
pp: A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a ↦ a ^ n
x✝ : A
⊢ (if x : 0 = 0 then 1 else ⋯.choose) = 1

Tactic:
exact dif_pos rfl

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤

Tactic:
trivial

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

Goal state before:
pp: case convert_2
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' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0

Tactic:
sub_smul,

Goal state after:
case convert_2
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' : R
eq1 : r • y = r' • y
⊢ r • y - r' • y = 0
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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ (r - snd i x) • ?m.277 ∈ (extensionOfMax i f).domain

Tactic:
rw [← eq2]

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
x : ↥(supExtensionOfMaxSingleton i f y)
r : R
a : N
ha : a ∈ (extensionOfMax i f).domain
eq1 : ↑x = ↑⟨a, ha⟩ + r • y
eq2 : ↑(fst i x) - a = (r - snd i x) • y
⊢ ↑(fst i x) - a ∈ (extensionOfMax i f).domain
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝ : NeZero (m * n)
this : NeZero m
⊢ φ (m * n) = φ m * φ n

Tactic:
have : NeZero n := ⟨right_ne_zero_of_mul hmn0⟩

Goal state after:
m n : ℕ
h : m.Coprime n
hmn0 : ¬m * n = 0
this✝¹ : NeZero (m * n)
this✝ : NeZero m
this : NeZero n
⊢ φ (m * n) = φ m * φ n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ (d * x / d) = #({k ∈ range (d * x) | (d * x).gcd k = d})

Tactic:
Nat.mul_div_cancel_left x hd0

Goal state after:
case inr
d : ℕ
hd0 : d > 0
x : ℕ
⊢ φ x = #({k ∈ range (d * x) | (d * x).gcd k = d})
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
⊢ φ (a.gcd b) * φ (a * b) = φ a * φ b * a.gcd b

Tactic:
have shuffle :
    ∀ a1 a2 b1 b2 c1 c2 : ℕ,
      b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2) := by
    intro a1 a2 b1 b2 c1 c2 h1 h2
    calc
      a1 / b1 * c1 * (a2 / b2 * c2) = a1 / b1 * (a2 / b2) * (c1 * c2) := by apply mul_mul_mul_comm
      _ = a1 * a2 / (b1 * b2) * (c1 * c2) := by
        congr 1
        exact div_mul_div_comm h1 h2
  simp only [totient_eq_div_primeFactors_mul]
  rw [shuffle, shuffle]
  rotate_left
  repeat' apply prod_primeFactors_dvd
  simp only [prod_primeFactors_gcd_mul_prod_primeFactors_mul]
  rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]
  exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)

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 : α
m : ℤ
⊢ b - (toIcoDiv hp a b - m) • p ∈ Set.Ico (a + m • p) (a + m • p + p)

Tactic:
sub_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIcoDiv hp a b • p - m • p) ∈ Set.Ico (a + m • p) (a + m • p + p)
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 : ℤ
⊢ b - (toIocDiv hp a b - m) • p ∈ Set.Ioc (a + m • p) (a + m • p + p)

Tactic:
sub_smul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ b - (toIocDiv hp a b • p - m • p) ∈ Set.Ioc (a + m • p) (a + m • p + p)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ (⋃₀ s)ᶜ ∈ T

Tactic:
simp only [Set.compl_sUnion]
    exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

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 : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
simp only [toIcoMod, toIcoDiv_add_zsmul', sub_smul, sub_add]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ closure (⋃₀ range f) = ⋃ i, closure (f i)

Tactic:
(finite_range _).closure_sUnion,

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
ι : Sort v
inst✝ : Finite ι
f : ι → Set X
⊢ ⋃ s ∈ range f, closure s = ⋃ i, closure (f i)
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 : ∀ a ∉ s, f a = x
⊢ Tendsto f (l ⊓ 𝓟 s) (𝓝 x) ↔ Tendsto f l (𝓝 x)

Tactic:
rw [tendsto_iff_comap, tendsto_iff_comap]
  replace h : 𝓟 sᶜ ≤ comap f (𝓝 x) := by
    rintro U ⟨t, ht, htU⟩ x hx
    have : f x ∈ t := (h x hx).symm ▸ mem_of_mem_nhds ht
    exact htU this
  refine ⟨fun h' => ?_, le_trans inf_le_left⟩
  have := sup_le h' h
  rw [sup_inf_right, sup_principal, union_compl_self, principal_univ, inf_top_eq, sup_le_iff]
    at this
  exact this.1

Goal state after:
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 : ℤ
⊢ toIocMod hp (a + ↑m * p) b = toIocMod hp a b + ↑m * p

Tactic:
by
  simpa using toIocMod_add_zsmul' hp a b m

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
ind : IsInducing f
surj : Surjective f
V : Set Y
hV : IsOpen[inst✝] V
U_open : IsOpen[inst✝¹] (f ⁻¹' V)
⊢ IsOpen[inst✝] (f '' f ⁻¹' V)

Tactic:
rwa [V.image_preimage_eq surj]

Goal state after:
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace W
inst✝² : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝¹ : TopologicalSpace X'
inst✝ : TopologicalSpace Y'
f : X ≃ₜ Y
g : Y → X
hg : Function.RightInverse g ⇑f
this : g = ⇑f.symm
⊢ Continuous[inst✝⁴, inst✝⁵] g

Tactic:
convert! f.symm.continuous

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
t : TopologicalSpace α
⊢ t ≠ ⊤ ↔ ∃ x y, ¬Inseparable x y

Tactic:
← TopologicalSpace.nontrivial_iff_exists_not_inseparable,

Goal state after:
α : Type u
t : TopologicalSpace α
⊢ t ≠ ⊤ ↔ NontrivialTopology α
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
⊢ IsOpenMap f ↔ ∀ {s : Set X}, closure[inst✝] (kernImage f s) ⊆ kernImage f (closure[inst✝¹] s)

Tactic:
by
  rw [isOpenMap_iff_image_interior, compl_surjective.forall]
  simp [kernImage_eq_compl]

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
ε : Type u_3
ζ : Type u_4
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y✝
inst✝³ : TopologicalSpace Z✝
inst✝² : TopologicalSpace W
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
X : Type ?u.28
Y : Type ?u.32
Z : Type ?u.36
f : X → Y → Z
ta1 ta2 : TopologicalSpace X
tb1 tb2 : TopologicalSpace Y
tc1 : TopologicalSpace Z
⊢ Sort ?u.37

Tactic:
haveI := ta2; haveI := tb2; exact Continuous fun p : X × Y => f p.1 p.2

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
tx : Set X
ty : Set Y
⊢ s ∈ 𝓝[tx ×ˢ ty] (x, y) ↔ ∃ u ∈ 𝓝[tx] x, ∃ v ∈ 𝓝[ty] y, u ×ˢ v ⊆ s

Tactic:
by
  rw [nhdsWithin_prod_eq, mem_prod_iff]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[≠] x = 𝓝[<] x ⊔ 𝓝[>] x

Tactic:
← Iio_union_Ioi,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
x : α
⊢ 𝓝[Iio x ∪ Ioi x] x = 𝓝[<] x ⊔ 𝓝[>] x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : s ∩ u = s ∩ f ⁻¹' t
⊢ f ⁻¹' t ∩ s = u ∩ s

Tactic:
by simpa only [Set.inter_comm, eq_comm] using useq

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ s ∩ u = s ∩ f ⁻¹' t

Tactic:
by simpa only [Set.inter_comm, eq_comm] using useq

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto (t.piecewise f g) (𝓝[s] a) l

Tactic:
apply Tendsto.piecewise

Goal state after:
case h₀
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto f (𝓝[s] a ⊓ 𝓟 t) l

case h₁
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f g : α → β
t : Set α
inst✝ : (x : α) → Decidable (x ∈ t)
a : α
s : Set α
l : Filter β
h₀ : Tendsto f (𝓝[s ∩ t] a) l
h₁ : Tendsto g (𝓝[s ∩ tᶜ] a) l
⊢ Tendsto g (𝓝[s] a ⊓ 𝓟 tᶜ) l
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ ContinuousAt f x

Tactic:
rw [ContinuousAt, ← nhdsWithin_eq_nhds.2 hi]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Sort u_5
s : ι → Set α
hs : ∀ (x : α), ∃ i, s i ∈ 𝓝 x
hf : ∀ (i : ι), ContinuousOn f (s i)
x : α
i : ι
hi : s i ∈ 𝓝 x
⊢ Tendsto f (𝓝[s i] x) (𝓝 (f x))
Module: Mathlib.Topology.Constructions.SumProd

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

Tactic:
compl_range_inr

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inl)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ ContinuousWithinAt g s₁ x

Tactic:
unfold ContinuousWithinAt

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f g : α → β
s s₁ : Set α
h : ContinuousOn f s
h' : EqOn g f s₁
h₁ : s₁ ⊆ s
x : α
hx : x ∈ s₁
⊢ Tendsto g (𝓝[s₁] x) (𝓝 (g x))