mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesLimit K F

Tactic:
let := preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left)
        (K.map WalkingParallelPairHom.right)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesLimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesEqualizer_of_preservesKernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesLimit K F
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: case mpr
S : ShortComplex Ab
⊢ (∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    Function.Surjective ⇑S.abToCycles

Tactic:
· rintro h ⟨x₂, hx₂⟩
    obtain ⟨x₁, rfl⟩ := h x₂ hx₂
    exact ⟨x₁, rfl⟩

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✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact ↔ Mono S.g

Tactic:
by
  constructor
  · intro h
    have := h.hasHomology
    simp only [exact_iff_isZero_homology] at h
    have := S.isIso_pOpcycles hf
    have := mono_of_isZero_kernel' _ S.homologyIsKernel h
    rw [← S.p_fromOpcycles]
    apply mono_comp
  · intro
    rw [(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        inferInstance (isZero_zero C))).exact_iff]
    exact isZero_zero C

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ Q.Factors f → P.Factors f

Tactic:
· rintro ⟨i, w⟩
        exact ⟨i ≫ h.inv.hom.left, by rw [Category.assoc, Over.w h.inv.hom, w]⟩

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✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
⊢ e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + e.inv.τ₂ ≫ S₁.g ≫ s.s ≫ e.hom.τ₂

Tactic:
e.inv.comm₂₃_assoc

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✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
eq : e.inv.τ₂ ≫ (s.r ≫ S₁.f + S₁.g ≫ s.s) ≫ e.hom.τ₂ = 𝟙 S₂.X₂
⊢ e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂ =
    e.inv.τ₂ ≫ s.r ≫ S₁.f ≫ e.hom.τ₂ + S₂.g ≫ e.inv.τ₃ ≫ s.s ≫ e.hom.τ₂
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
f g : MonoOver X
h : f.obj.left ≅ g.obj.left
w : h.hom ≫ g.arrow = f.arrow
⊢ h.inv ≫ f.arrow = g.arrow

Tactic:
h.inv_comp_eq,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
f g : MonoOver X
h : f.obj.left ≅ g.obj.left
w : h.hom ≫ g.arrow = f.arrow
⊢ f.arrow = h.hom ≫ g.arrow
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject X
h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)
⊢ A ≤ B

Tactic:
simpa only [← map_comp, e.hom_inv_id, map_id] using h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ IsIso (coimageImageComparison α)

Tactic:
have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) := by
    intros
    rw [coimageImageComparison_app']
    infer_instance
  apply NatIso.isIso_of_isIso_app

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

Goal state before:
pp: case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ underlying.obj (sSup s) ⟶ underlying.obj f

pp: case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ?f ≫ f.arrow = (sSup s).arrow

Tactic:
· refine (underlyingIso _).hom ≫ image.lift ⟨_, f.arrow, ?_, ?_⟩
    · refine Sigma.desc ?_
      rintro ⟨g, m⟩
      refine underlying.map (homOfLE (k _ ?_))
      simpa using m
    · ext
      dsimp [smallCoproductDesc]
      simp

Goal state after:
case w
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
k : ∀ g ∈ s, g ≤ f
⊢ ((underlyingIso (image.ι (smallCoproductDesc s))).hom ≫
        image.lift
          { I := underlying.obj f, m := f.arrow, m_mono := ⋯,
            e := Sigma.desc fun b ↦ Subtype.casesOn b fun g m ↦ underlying.map (homOfLE ⋯), fac := ⋯ }) ≫
      f.arrow =
    (sSup s).arrow
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
f : Fan Z
hf : IsLimit f
e : (Discrete.functor fun x ↦ Opposite.op (Z x)) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
  Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Opposite.op (Z x)).obj x)
x✝ : Discrete α
a : α
⊢ ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).ι.app { as := a } ≫
      (Iso.refl
          ((Cocone.precompose e.hom).obj (Cocone.whisker (Discrete.opposite α).symm.functor (Cone.op f))).pt).hom =
    f.op.ι.app { as := a }

Tactic:
simp [e, Fan.proj]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl = prod.fst.op ≫ (opProdIsoCoprod A B).hom

Tactic:
fst_opProdIsoCoprod_hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl = coprod.inl
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteProducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ (evaluation (Finset (Discrete α))ᵒᵖ C).obj (op I)).map x✝ ≫
      (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Y✝.obj ↑x).obj x))).hom =
    (HasLimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ X✝.obj ↑x).obj x))).hom ≫
      ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x) ⋙ lim).map x✝

Tactic:
by dsimp; ext; simp [Pi.map]

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α' ↔ IsIso φ

Tactic:
by
  constructor
  · intro
    rw [F'.hom_ext_of_isLeftKanExtension α φ (leftKanExtensionUnique _ α _ α').hom
      (by simp [comm])]
    infer_instance
  · intro
    exact isLeftKanExtension_of_iso (asIso φ) α α' comm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
⊢ unitBackward η X ∘ unitForward η X = id

Tactic:
refine funext fun p => YonedaCollection.ext ?_ (OverArrows.ext ?_)

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ ((unitBackward η X ∘ unitForward η X) p).fst = (id p).fst

case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
exact Quiver.Hom.unop_inj (by simp only [unop_comp, Quiver.Hom.unop_op, comp_epiDesc])

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 ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Y : ℰ
f : L.obj P ⟶ Y
Z : Cᵒᵖ
z : P.obj Z
⊢ (hom ((((uliftYonedaAdjunction L α).homEquiv P Y) f).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) ≫ f }

Tactic:
by
  simp [uliftYonedaAdjunction, restrictedULiftYonedaHomEquiv,
    restrictedULiftYonedaHomEquiv', IsColimit.homEquiv]

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✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
⊢ uliftYonedaEquiv
      ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
        ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom) =
    uliftYonedaEquiv
      (((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
        (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f)

Tactic:
have eq₁ := ConcreteCategory.congr_hom
        ((uliftYoneda.{max w v₁}.obj (F.obj Y)).descOfIsLeftKanExtension_fac_app
        (uliftYonedaMap F Y) (F.op.lan.obj (uliftYoneda.obj Y))
          (F.op.lanUnit.app (uliftYoneda.obj Y)) _) ⟨f⟩

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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
eq₁ :
  (hom
        ((uliftYonedaMap F Y).app (op X) ≫
          ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).descOfIsLeftKanExtension (uliftYonedaMap F Y)
                (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))
                (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).app
            (F.op.obj (op X))))
      { down := f } =
    (hom ((F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y)).app (op X))) { down := f }
⊢ uliftYonedaEquiv
      ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
        ((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj Y)).leftKanExtensionUnique (uliftYonedaMap F Y)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj Y))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y))).hom) =
    uliftYonedaEquiv
      (((uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).leftKanExtensionUnique (uliftYonedaMap F X)
            (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
            (F.op.lanUnit.app (uliftYoneda.{max v₂ w, v₁, u₁}.obj X))).hom ≫
        (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f)
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)
⊢ ∀ {X Y : WalkingParallelFamily (ULift.{w, 0} Bool)} (f : X ⟶ Y),
    (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map f ≫ (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
              parallelPair (line { down := true }) (line { down := false })).map
          f

Tactic:
rintro _ _ (_ | ⟨_ | _⟩) <;> 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.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (x + n • c) = ↑n.negOnePow • f x

Tactic:
by
  rcases Int.even_or_odd' n with ⟨k, rfl | rfl⟩
  · rw [h.even_zsmul_periodic, Int.negOnePow_two_mul, Units.val_one, one_zsmul]
  · rw [h.odd_zsmul_antiperiodic, Int.negOnePow_two_mul_add_one, Units.val_neg,
      Units.val_one, neg_zsmul, one_zsmul]

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (a + ↑n) (a + ↑n + 1))

Tactic:
by
  simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
    pairwise_disjoint_Ioc_add_zsmul a (1 : α)

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

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

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r r' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) r - (extendIdealTo i f h y) r' = 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 : ↑(fst i x) + snd i x • y = a + r • y
⊢ ↑(fst i x) - a = (r - snd i x) • y

Tactic:
← sub_eq_zero,

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 : ↑(fst i x) + snd i x • y - (a + r • y) = 0
⊢ ↑(fst i x) - a = (r - snd i x) • y
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
rw [← prod_atTop_atTop_eq] at hp

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: α : Type u_3
f : Filter α
s : ℕ → Set α
hs : f.HasAntitoneBasis s
r : ℕ → ℕ → Prop
hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in atTop, r m n
this : ∀ (t : Set ℕ), t.Finite → ∀ᶠ (n : ℕ) in atTop, ∀ m ∈ t, m < n ∧ r m n
φ : ℕ → ℕ
hφ : (∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → φ x_1 < φ x) ∧ ∀ (x : ℕ) ⦃x_1 : ℕ⦄, x_1 < x → r (φ x_1) (φ x)
⊢ ∃ φ, StrictMono φ ∧ ∀ (m n : ℕ), m < n → r (φ m) (φ n)

Tactic:
exact ⟨φ, forall_comm.2 hφ.1, forall_comm.2 hφ.2⟩

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

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

Tactic:
by
  obtain ⟨ys, h⟩ := exists_seq_tendsto (atTop : Filter α)
  choose c hleft hright using exists_ge_ge (α := α)
  set xs : ℕ → α := fun n => (List.range n).foldl (fun x n ↦ c x (ys n)) (ys 0)
  have hsucc (n : ℕ) : xs (n + 1) = c (xs n) (ys n) := by simp [xs, List.range_succ]
  refine ⟨xs, ?_, ?_⟩
  · refine monotone_nat_of_le_succ fun n ↦ ?_
    rw [hsucc]
    apply hleft
  · refine (tendsto_add_atTop_iff_nat 1).1 <| tendsto_atTop_mono (fun n ↦ ?_) h
    rw [hsucc]
    apply hright

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Goal state after:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen[inst✝] s₁
h₂ : IsOpen[inst✝] s₂
⊢ IsOpen[inst✝] (⋃ b, bif b then s₁ else s₂)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] ((⋃ i, f i) ∩ s)

Tactic:
iUnion_inter

Goal state after:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] (⋃ i, f i ∩ s)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
f : Filter X
h : x ∈ s
o : IsOpen[inst✝] s
sf : 𝓟 s ≤ f
⊢ ⨅ s ∈ {s | x ∈ s ∧ IsOpen[inst✝] s}, 𝓟 s ≤ f

Tactic:
exact iInf₂_le_of_le s ⟨h, o⟩ sf

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed[inst✝] t
⊢ 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
exact h.nhdsSet_le_sup s

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: ⊢ ⨅ s ∈ {s | False ∈ s ∧ s ∈ {{True}}}, 𝓟 s = ⊤

Tactic:
simp [@and_comm (_ ∈ _)]

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2

Tactic:
have hX := continuous_sInf_dom hX continuous_id

Goal state after:
X : Type u_5
Y : Type u_6
Z : Type u_7
f : X → Y → Z
tas : Set (TopologicalSpace X)
tbs : Set (TopologicalSpace Y)
tX : TopologicalSpace X
tY : TopologicalSpace Y
tc : TopologicalSpace Z
hX✝ : tX ∈ tas
hY : tY ∈ tbs
hf : Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
hX : Continuous[sInf tas, tX] id
⊢ Continuous[instTopologicalSpaceProd, tc] fun p ↦ f p.1 p.2
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
isClosedEmbedding_iff,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsEmbedding (g ∘ f) ∧ IsClosed[inst✝] (range (g ∘ f)) ↔ IsEmbedding f ∧ IsClosed[inst✝¹] (range f)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousAt f x

Tactic:
← continuousWithinAt_compl_self

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
h : ¬AccPt x (𝓟 {x}ᶜ)
⊢ ContinuousWithinAt f {x}ᶜ x
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : ↑s
⊢ map Subtype.val (𝓝 x) = 𝓝[s] ↑x

Tactic:
rw [IsInducing.subtypeVal.map_nhds_eq, Subtype.range_val]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ⋃ a ∈ {f | f.Finite ∧ f ⊆ s}, ⋂₀ a = univ

Tactic:
iUnion₂_eq_univ_iff

Goal state after:
case refine_2
α : Type u
s : Set (Set α)
this : TopologicalSpace α := generateFrom s
⊢ ∀ (a : α), ∃ i, ∃ (_ : i ∈ {f | f.Finite ∧ f ⊆ s}), a ∈ ⋂₀ i
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[t] s

Tactic:
rw [hb.eq_generateFrom]
  exact .basic s hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
u : Set ↑s
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
⊢ ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ v).Nonempty

Tactic:
intro t ht ht'

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
u : Set ↑s
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ u).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
hv2 : Subtype.val ⁻¹' v = u
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
⊢ (t ∩ v).Nonempty
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∃ n, accumulate s n = univ) → ∃ n, s n = univ

Tactic:
contrapose!

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∀ (n : ℕ), s n ≠ univ) → ∀ (n : ℕ), accumulate s n ≠ univ