mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ ∃ U a x, (ιR cR) a = r ∧ ιM x = m

Tactic:
obtain ⟨U, ⟨a, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      (isColimitOfPreserves (forget AddCommGrpCat) hcM)) ⟨r, m⟩
  rw [Prod.ext_iff] at h
  obtain ⟨rfl, rfl⟩ := h
  exact ⟨U, a, x, rfl, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : F.rightAdjointObjIsDefined = ⊤
⊢ F.IsLeftAdjoint

Tactic:
by
  replace h : ∀ X, IsRepresentable (F.op ⋙ yoneda.obj X) := fun X ↦ by
    simp only [← rightAdjointObjIsDefined_iff, h, Pi.top_apply, Prop.top_eq_true]
  exact (Adjunction.adjunctionOfEquivRight
    (fun X Y ↦ (F.op ⋙ yoneda.obj Y).representableBy.homEquiv.symm)
    (fun X Y Y' g f ↦ (RepresentableBy.comp_homEquiv_symm ..).symm)).isLeftAdjoint

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M ↔ ⊤ M

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, iff_true]

Goal state after:
C D : Type u
inst✝¹ : SmallCategory C
inst✝ : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ pullbackObjIsDefined φ M
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
⊢ IsIso ⊤.ι

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Pretopology

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X Z : C
g : Z ⟶ X
i✝ : IsIso g
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → Presieve.singleton g f → Presieve Y
hS :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : Presieve.singleton g f), Ti f H ∈ {S | ∃ Y_1 f, ∃ (_ : IsIso f), S = Presieve.singleton f}
Y : C
f : Y ⟶ Z
i : IsIso f
hTi : Ti g ⋯ = Presieve.singleton f
⊢ IsIso (f ≫ g)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f : Y ⟶ X
g : Z✝ ⟶ X
inst✝ : HasPullback g f
Z : C
h : Z ⟶ X
⊢ HasPullback g f

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
ι : Type u_1
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
Z : C
g : Z ⟶ S
hg : ofArrows X f g
⊢ Z = X (ofArrows.idx ⋯)

Tactic:
simp [ofArrows.obj_idx]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
Z : C
g : Z ⟶ Y
hg : singleton f g
⊢ Z = X

Tactic:
cases hg

Goal state after:
case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ X = X
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
hg : R g
⊢ (ConcreteCategory.hom (f.app (op X) ≫ Q.map g.op)) t = (ConcreteCategory.hom (f.app (op Y))) (x g hg)

Tactic:
rw [← f.naturality, comp_apply, h g hg]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P R
x : FamilyOfElements P (generate R).arrows
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P R → IsSeparatedFor P (generate R).arrows

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P (generate R).arrows → IsSeparatedFor P R

Tactic:
· intro h x t₁ t₂ ht₁ ht₂
    apply h (x.restrict (le_generate R)) t₁ t₂ _ _
    · exact isAmalgamation_restrict _ x t₁ ht₁
    · exact isAmalgamation_restrict _ x t₂ ht₂

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSeparatedFor P (generate R).arrows → IsSeparatedFor P R
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
h : x.Compatible → ∃! t, x.IsAmalgamation t
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X✝ : C
R : Presieve X✝
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ e (e.symm ((ConcreteCategory.hom (P₂.map f.op)) x)) = e ((ConcreteCategory.hom (P₁.map f.op)) (e.symm x))

Tactic:
simp only [Equiv.apply_symm_apply, he]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
⊢ (fun t ↦ x₂.IsAmalgamation t) t₂ → t₂ = e (hP₁.amalgamate x₁ hx₁)

Tactic:
ht₂

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X : C
R : Presieve X
hP₁ : IsSheafFor P₁ R
x₂ : FamilyOfElements P₂ R
hx₂ : x₂.Compatible
he' :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₂.obj (op Y)),
    e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)
x₁ : FamilyOfElements P₁ R := fun Y f hf ↦ e.symm (x₂ f hf)
hx₁ : x₁.Compatible
this : ∀ (t₂ : P₂.obj (op X)), x₂.IsAmalgamation t₂ ↔ x₁.IsAmalgamation (e.symm t₂)
t₂ : P₂.obj (op X)
ht₂ : x₂.IsAmalgamation t₂
⊢ t₂ = e (hP₁.amalgamate x₁ hx₁)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
⊢ (Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) (multiequalizer ((unop S).index P))
          (fun I ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback (g.unop ≫ f.unop)).index P))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback (g.unop ≫ f.unop)).index P) (I.map e.inv)) ⋯) ≫
      Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I =
    (Multiequalizer.lift (((unop S).pullback f.unop).index P) (multiequalizer ((unop S).index P))
          (fun I ↦ Multiequalizer.ι ((unop S).index P) I.base) ⋯ ≫
        Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          (multiequalizer (((unop S).pullback f.unop).index P))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) I.base) ⋯) ≫
      Multiequalizer.ι ((((unop S).pullback f.unop).pullback g.unop).index P) I

Tactic:
simp only [Multiequalizer.lift_ι, Category.assoc]

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
I : (unop (op (((unop S).pullback f.unop).pullback g.unop))).shape.L
⊢ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I e.inv).base =
    Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I).base
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
t₁ t₂ : P'.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
t₁ t₂ : P'.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
h : IsSeparatedFor Q R
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
inst✝ : Mono f
h : IsSeparatedFor Q R
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
⊢ x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
ht₂

Goal state after:
case left
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
S : Sieve X
R : Presieve X
h : S.arrows ≤ R
hS : IsSheafFor P S.arrows
trans : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → IsSeparatedFor P (Sieve.pullback f S).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⋯
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
⊢ ∀ (j : WalkingMulticospan T.shape), e ≫ (T.multifork P).π.app j = K.π.app j

Tactic:
rintro (a | b)

Goal state after:
case h.right.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
a : T.shape.L
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.left a) = K.π.app (WalkingMulticospan.left a)

case h.right.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
e : E ⟶ P.obj (op X)
he : x.IsAmalgamation e
b : T.shape.R
⊢ e ≫ (T.multifork P).π.app (WalkingMulticospan.right b) = K.π.app (WalkingMulticospan.right b)
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Mono ((toRange p).app i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Epi ((toRange p).app i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : Presieve.IsSheafFor (P' ⋙ coyoneda.obj X) R
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))

Tactic:
rw [Equalizer.Presieve.sheaf_condition] at q

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
X : A'ᵒᵖ
q : Nonempty (IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj X) R) ⋯))
⊢ IsLimit ((coyoneda.obj X).mapCone (Fork.ofι (forkMap R P') ⋯))
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso ((sheafToPresheaf J B).map ((sheafCompose J F).map f))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F✝ F'✝ F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F✝
F F' : Sheaf J (Type w)
f : F ⟶ F'
⊢ Mono (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

Tactic:
intro

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
Module: Mathlib.Topology.Category.TopCat.EpiMono

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)

Tactic:
intro

Goal state after:
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Mono f
⊢ Mono ((forget TopCat).map f)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coneOfConeForget (forget.mapCone c)).π.app j =
      (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom ≫
        c.π.app j

Tactic:
intro

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
h : c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str
j✝ : J
⊢ (coneOfConeForget (forget.mapCone c)).π.app j✝ =
    (isoOfHomeo
          (let __Equiv := Equiv.refl ↑(coneOfConeForget (forget.mapCone c)).pt;
          { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom ≫
      c.π.app j✝
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit F → HasLimit (F ⋙ forget)

Tactic:
intro

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit F
⊢ HasLimit (F ⋙ forget)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasLimit (F ⋙ forget) → HasLimit F

Tactic:
intro

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit (F ⋙ forget)
⊢ HasLimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasLimit F
⊢ HasLimit (F ⋙ forget)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
hP : Presheaf.IsSheaf J P
this : IsIso (J.toPlus P)
⊢ IsIso (J.toPlus P ≫ (J.plusFunctor D).map (J.toPlus P))

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} ↑(F ⋙ forget).sections

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁶ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁴ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝³ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝ : (forget D).ReflectsIsomorphisms
F G : Sheaf J D
f : F ⟶ G
m : Mono f
⊢ Mono f.hom

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
⊢ ∀ (j : J),
    (coconeOfCoconeForget (forget.mapCocone c)).ι.app j ≫
        (isoOfHomeo
            (let __Equiv := Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt;
            { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom =
      c.ι.app j

Tactic:
intro

Goal state after:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit (forget.mapCocone c)
h : c.pt.str = ⨆ j, coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
j✝ : J
⊢ (coconeOfCoconeForget (forget.mapCocone c)).ι.app j✝ ≫
      (isoOfHomeo
          (let __Equiv := Equiv.refl ↑(coconeOfCoconeForget (forget.mapCocone c)).pt;
          { toEquiv := __Equiv, continuous_toFun := ⋯, continuous_invFun := ⋯ })).hom =
    c.ι.app j✝
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit F → HasColimit (F ⋙ forget)

Tactic:
intro

Goal state after:
case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit F
⊢ HasColimit (F ⋙ forget)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
⊢ HasColimit (F ⋙ forget) → HasColimit F

Tactic:
intro

Goal state after:
case mpr
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit (F ⋙ forget)
⊢ HasColimit F
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: case mp
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
a✝ : HasColimit F
⊢ HasColimit (F ⋙ forget)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J✝ : Type v
inst✝² : Category.{w, v} J✝
F✝ : J✝ ⥤ TopCat
J : Type v
inst✝¹ : Category.{v_1, v} J
inst✝ : Small.{u, v} J
F : J ⥤ TopCat
⊢ Small.{u, max u v} (F ⋙ forget).ColimitType

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3.snd
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
m : S.pt ⟶ (pullbackCone f g).pt
h₁ : m ≫ (pullbackCone f g).fst = S.fst
h₂ : m ≫ (pullbackCone f g).snd = S.snd
x : ↑S.pt
⊢ (↑((ConcreteCategory.hom m) x)).2 =
    (↑((ConcreteCategory.hom
            (ofHom
              { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
                continuous_toFun := ⋯ }))
          x)).2

Tactic:
· simpa using! ConcreteCategory.congr_hom h₂ x

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: J : Type v
inst✝³ : Category.{w, v} J
X✝ Y✝ Z✝ : TopCat
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
hf : Continuous[inst✝², inst✝] f
g : Y → Z
hg : IsEmbedding g
⊢ Function.LeftInverse (fun x ↦ ⟨(↑x, Exists.choose ⋯), ⋯⟩) fun x ↦ ⟨(↑x).1, ⋯⟩

Tactic:
intro x
    ext <;> dsimp
    apply hg.injective
    convert! x.prop
    exact Exists.choose_spec (p := fun y ↦ g y = f (↑x : X × Y).1) _

Goal state after: