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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ Cofork.π c ≫ (hc.ofIsoColimit (Cofork.ext (Iso.refl c.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯) = Cofork.π c ≫ 0

Tactic:
by simp [hg]

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 : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ h.cyclesIso.hom ≫ h.i = S.iCycles

Tactic:
dsimp [iCycles, LeftHomologyData.cyclesIso]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ cyclesMap' (𝟙 S) S.leftHomologyData h ≫ h.i = S.leftHomologyData.i
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
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (homologyMap φ ≫ S₂.homologyι)

Tactic:
rw [homologyι_naturality φ]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Mono (opcyclesMap φ)
⊢ Mono (S₁.homologyι ≫ opcyclesMap φ)
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₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
⊢ (S.map F).RightHomologyData

Tactic:
have hg' : g' = F.map h.g' := by
    apply Cofork.IsColimit.hom_ext hp
    rw [Cofork.IsColimit.π_desc hp]
    simp only [Cofork.π_ofπ, CokernelCofork.map_π, map_g, ← F.map_comp, p_g']

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₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
⊢ (S.map F).RightHomologyData
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.PreservesEpimorphisms
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
g : P ⟶ X✝
f : E✝ ⟶ X✝
x✝ : Epi f
⊢ ∃ f', f' ≫ f = g

Tactic:
by
    obtain ⟨h, fac⟩ := hP.factors (F.map g) (F.map f)
    exact ⟨F.preimage h, F.map_injective (by simp [fac])⟩

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

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

Tactic:
by rw [assoc]

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
h : S.HomologyData
⊢ S.Exact ↔ IsZero h.right.H

Tactic:
by
  have := HasHomology.mk' h
  exact RightHomologyData.exact_iff h.right

Goal state after:
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
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
⊢ ∀ {c : Cone (parallelPair f g)} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))

Tactic:
intro c i

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
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))
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), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
⊢ ∀ {c : Cocone (parallelPair f g)} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))

Tactic:
intro c i

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), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
⊢ Nonempty (IsColimit (F.mapCocone c))
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject A) ≅ lower e.functor ⋙ lower e.inverse

Tactic:
apply eqToIso

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ 𝟭 (Subobject A) = lower e.functor ⋙ lower e.inverse
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor ≅ 𝟭 (Subobject B)

Tactic:
apply eqToIso

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver A ≌ MonoOver B
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject B)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
    Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)

Tactic:
dsimp only [Subobject.lift_mk]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk (cokernel.π f).op ≤ Subobject.mk (cokernel.π g).op
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: 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
⊢ Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
    Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)

Tactic:
dsimp only [Subobject.lift_mk]

Goal state after:
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
⊢ Subobject.mk (kernel.ι f.unop) ≤ Subobject.mk (kernel.ι g.unop)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
W'✝ : C
x✝² : W'✝ ⟶ S.X₂
x✝¹ : x✝² ≫ S.g = 0
x✝ : W'✝ ⟶ Abelian.image S.f
hm : x✝ ≫ Abelian.image.ι S.f = x✝²
⊢ x✝ = kernel.lift (cokernel.π S.f) x✝² ⋯

Tactic:
← cancel_mono (Abelian.image.ι S.f),

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : kernel.ι S.g ≫ cokernel.π S.f = 0
W'✝ : C
x✝² : W'✝ ⟶ S.X₂
x✝¹ : x✝² ≫ S.g = 0
x✝ : W'✝ ⟶ Abelian.image S.f
hm : x✝ ≫ Abelian.image.ι S.f = x✝²
⊢ x✝ ≫ Abelian.image.ι S.f = kernel.lift (cokernel.π S.f) x✝² ⋯ ≫ Abelian.image.ι S.f
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.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ colimit.ι X✝ i ≫ colimMap f ≫ ((L.lan.obj Y✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app Y✝)).inv =
    colimit.ι X✝ i ≫ ((L.lan.obj X✝).colimitIsoOfIsLeftKanExtension (L.lanUnit.app X✝)).inv ≫ colimMap (L.lan.map f)

Tactic:
rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv,
        ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← 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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
inst✝² : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
inst✝¹ : HasColimitsOfShape C H
inst✝ : HasColimitsOfShape D H
X✝ Y✝ : C ⥤ H
f : X✝ ⟶ Y✝
i : C
⊢ (f.app i ≫ (L.lanUnit.app Y✝).app i) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i) =
    ((L.lanUnit.app X✝).app i ≫ (L.lan.map f).app (L.obj i)) ≫ colimit.ι (L.lan.obj Y✝) (L.obj i)
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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
rw [YonedaCollection.map₁_fst]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
X : C
⊢ (((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
          CostructuredArrow.hom E).app
      X =
    (CostructuredArrow.hom G).app X

Tactic:
simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _))

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
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))
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))

Tactic:
apply isConnected_of_zigzag

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
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))
⊢ ∀ (j₁ j₂ : StructuredArrow d (sequentialFunctor J)), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
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 (i ⟶ j) ∨ Nonempty (j ⟶ i)

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

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
⊢ IsConnected (CostructuredArrow (sequentialFunctor J) d)

Tactic:
apply isConnected_of_zigzag

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
⊢ ∀ (j₁ j₂ : CostructuredArrow (sequentialFunctor J) d), ∃ l, List.IsChain Zag (j₁ :: l) ∧ (j₁ :: l).getLast ⋯ = j₂
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
X : C
⊢ (hom ((uliftYonedaMap F X).app (op X))) { down := 𝟙 X } = { down := 𝟙 (F.obj X) }

Tactic:
by simp [uliftYonedaMap]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
⊢ IsCoseparator G ↔ ∀ (A : C), Mono (Pi.lift fun f ↦ f)

Tactic:
rw [isCoseparator_def]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔ ∀ (A : C), Mono (Pi.lift fun f ↦ f)
Module: Mathlib.CategoryTheory.Generator.Basic

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

Tactic:
rw [isCoseparator_def]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g
Module: Mathlib.CategoryTheory.Generator.Basic

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

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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

Goal state before:
pp: case refine_2
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
⊢ IsIso ((yoneda.obj G).map f.op)

Tactic:
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ G, IsSeparator G

Tactic:
by
    use AddCommGrpCat.of (ULift ℤ)
    intro A B f g h; simp_all only [ObjectProperty.singleton_iff, AddCommGrpCat.ext_iff,
      AddCommGrpCat.hom_comp, AddMonoidHom.coe_comp, Function.comp_apply, forall_eq', ULift.forall]
    (intro x; specialize h (AddCommGrpCat.ofHom
    (AddMonoidHom.mk' (fun y => y • x) fun y z => by simp only [add_smul])) 1; aesop)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
⊢ ∀ (Y : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements)
    (m : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X)) ⟶ Y),
    m = ⟨shrinkYonedaObjObjEquiv Y.snd, ⋯⟩

Tactic:
rintro u ⟨m, hm⟩
    ext
    simp [← hm, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addRightEmbedding a) s)

Tactic:
← addLeftEmbedding_eq_addRightEmbedding

Goal state after:
a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)
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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ = ExtensionOfMaxAdjoin.extensionToFun i f h ⟨i m, ⋯⟩

Tactic:
ExtensionOfMaxAdjoin.extensionToFun_wd i f h _ ⟨i m, _⟩ 0 _,

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
m : M
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨i m, ⋯⟩ =
    ↑(extensionOfMax i f).toLinearPMap ⟨i m, ?m.544⟩ + (ExtensionOfMaxAdjoin.extendIdealTo i f h y) 0

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
m : M
⊢ i m ∈ (extensionOfMax i f).domain

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
m : M
⊢ ↑⟨i m, ⋯⟩ = ↑⟨i m, ?m.544⟩ + 0 • y
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
⊢ ↑(insert a s) ⊆ S → ⋂₀ ↑(insert a s) ∈ S

Tactic:
h2

Goal state after:
case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ ⋂₀ ↑(insert a s) ∈ S
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
⊢ b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
h2

Goal state after:
a b a1 a2 b1 b2 c1 c2 : ℕ
h1 : b1 ∣ a1
h2 : b2 ∣ a2
⊢ a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (f ⊓ map u g).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f

Tactic:
← Filter.push_pull',

Goal state after:
α : Type u_1
ι : Type u_3
g : Filter ι
inst✝¹ : g.IsCountablyGenerated
u : ι → α
f : Filter α
inst✝ : f.IsCountablyGenerated
hx : (map u (comap u f ⊓ g)).NeBot
⊢ ∃ θ, Tendsto θ atTop g ∧ Tendsto (u ∘ θ) atTop f
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f

Tactic:
obtain ⟨φ, hφ⟩ := exists_seq_comp_tendsto hx

Goal state after:
α : Type u_1
f : Filter α
inst✝ : f.IsCountablyGenerated
u : ℕ → α
hx : (f ⊓ map u atTop).NeBot
φ : ℕ → ℕ
hφ : Tendsto φ atTop atTop ∧ Tendsto (u ∘ φ) atTop f
⊢ ∃ θ, StrictMono θ ∧ Tendsto (u ∘ θ) atTop f
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
hh : Monotone h
⊢ (∀ s ∈ f, (𝓟 (h s)).NeBot) ↔ ∀ s ∈ f, (h s).Nonempty

Tactic:
simp only [principal_neBot_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ t ⊆ s, IsOpen t ∧ x ∈ t

Tactic:
rw [← subset_interior_iff_isOpen]
  simp only [subset_def, mem_interior]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ x ∈ closure[inst✝] s → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s

Tactic:
mem_closure_iff_frequently

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
⊢ (∃ᶠ (x : X) in 𝓝 x, x ∈ s) → x ∈ s ↔ (∃ᶠ (y : X) in 𝓝 x, y ∈ s) → x ∈ s
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen[inst✝] U ∧ t ⊆ U ∧ U ⊆ s

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen[inst✝] U ∧ t ⊆ U ∧ U ⊆ s

Tactic:
by
  rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]

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

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

Tactic:
simp only [ContinuousAt, ← h.map_nhds_eq, tendsto_map'_iff, comp_def]

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

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

Tactic:
← Filter.push_pull',

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

Goal state before:
pp: case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ 𝓝 a ≤ pure a ⊔ f

pp: case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ pure a ⊔ f ≤ 𝓝 a

Tactic:
· rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩
    exact IsOpen.mem_nhds (fun _ ↦ htf) hat

Goal state after:
case a
α : Type u
a : α
f : Filter α
x✝ : TopologicalSpace α := ⋯
⊢ pure a ⊔ f ≤ 𝓝 a
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 : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)

Tactic:
apply (hf.clusterPt_comap h).mono

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l