mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ ∃ t, (ConcreteCategory.hom (f.app (op W))) t = (ConcreteCategory.hom (G.map (j ≫ i).op)) s

Tactic:
refine ⟨F.map j.op t, ?_⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
U : C
s : ToType (G.obj (op U))
V W : C
i : V ⟶ U
t : ToType (F.obj (op V))
ht : (ConcreteCategory.hom (f.app (op V))) t = (ConcreteCategory.hom (G.map i.op)) s
j : W ⟶ V
⊢ (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map j.op)) t) =
    (ConcreteCategory.hom (G.map (j ≫ i).op)) s
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i }))
        (shrinkYonedaObjObjEquiv.symm a)) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ shrinkYonedaObjObjEquiv.symm (v ≫ g) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ shrinkYonedaObjObjEquiv.symm (v ≫ g) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
exact (shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm v.op g).symm

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : projectiveDimension X = ↑⊤
⊢ ↑⊤ ≠ ⊤ ↔ ∃ n, HasProjectiveDimensionLE X n

Tactic:
by_contra!

Goal state after:
case coe.top
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : projectiveDimension X = ↑⊤
this : (↑⊤ ≠ ⊤ ∧ ∀ (n : ℕ), ¬HasProjectiveDimensionLE X n) ∨ ↑⊤ = ⊤ ∧ ∃ n, HasProjectiveDimensionLE X n
⊢ False
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
⊢ Sigma.ι (fun x ↦ R) ⟨b, hb⟩ ≫ m = Sigma.ι (fun x ↦ R) ↑⟨b, hb⟩ ≫ s.π

Tactic:
← hm,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
⊢ Sigma.ι (fun x ↦ R) ⟨b, hb⟩ ≫ m = Sigma.ι (fun x ↦ R) ↑⟨b, hb⟩ ≫ Cofork.π (sigmaConstCokernelCofork R f) ≫ m
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:

Tactic:
f₁ = c₀.pt.hom ≫ F.map g₁.right := g₁.w.symm
    _ = c₀.pt.hom ≫ F.map g₂.right := by rw [this]
    _ = f₂ := g₂.w

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
i✝ : ↑R.uncurry ⊕ ↑T.uncurry
i : ↑T.uncurry
⊢ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) (Sum.inr i) ⟶ S

Tactic:
by exact (eT _ i.2).hom ≫ i.1.2

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J X
⊢ Sieve.generate S.arrows ∈ J.toCoverage.toGrothendieck X

Tactic:
apply Saturate.of

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J X
⊢ S.arrows ∈ J.toCoverage.coverings X
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ Sieve.generate (Presieve.ofArrows (E.map F).X (E.map F).f) = Sieve.functorPushforward F E.sieve₀

Tactic:
← PreZeroHypercover.presieve₀,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ Sieve.generate (E.map F).presieve₀ = Sieve.functorPushforward F E.sieve₀
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ≤
    Sieve.functorPushforward F (E.sieve₁' i₁ i₂)

Tactic:
rw [PreOneHypercover.sieve₁_eq_pullback_sieve₁' _ _ _
      (by simp [← Functor.map_comp, pullback.condition])]
    rintro W f ⟨Z, u, v, ⟨k⟩, h⟩
    refine ⟨E.Y k, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), u, ?_, ?_⟩
    · use E.Y k, 𝟙 _, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), ⟨k⟩
      simp
    · simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h
      apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _)) <;>
        simp [← h.left, ← h.right, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
let adj' : H' ⊣ (Functor.whiskeringLeft _ _ _).obj F.op := F.op.lanAdjunction _

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        G.op.ran.map f.hom ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj H).obj =
    ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom

Tactic:
Functor.map_id,

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
G : C ⥤ D
A : Type w
inst✝³ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝² : G.IsCocontinuous J K
inst✝¹ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝ : G.IsContinuous J K
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      𝟙 (G.op.ran.obj (G.op ⋙ F.obj)) ≫ G.op.ran.map f.hom ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj H).obj =
    ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ b) ≫ g = G.map d

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f = G.map (c ≫ b)

pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
g : G.obj Y ⟶ G.obj Z
T₀ : C
a : T₀ ⟶ X
b : T₀ ⟶ Y
fac₁ : G.map b = G.map a ≫ f
U₀ : C
c : U₀ ⟶ T₀
d : U₀ ⟶ Z
fac₂ : G.map d = G.map (c ≫ b) ≫ g
⊢ G.map (c ≫ a) ≫ f ≫ g = G.map d

Tactic:
all_goals
        simp only [Functor.map_comp, Category.assoc, fac₁, fac₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSheafFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
rw [← pullback_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSheafFor P (Sieve.pullback (g ≫ f) S).arrows
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
x✝ : (Sieve.pullback g R).arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows

Tactic:
rw [← pullback_comp]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
x✝ : (Sieve.pullback g R).arrows f
⊢ Presieve.IsSeparatedFor P (Sieve.pullback (f ≫ g) S).arrows
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ J ≤ F.inducedTopology K

Tactic:
· apply Sheaf.le_finestTopology
    rintro _ ⟨P, rfl⟩
    exact Functor.op_comp_isSheaf_of_types F J K P

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (c ≫ f)

Tactic:
show c ≫ f = d ≫ a by ext; exact w

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ S.arrows (d ≫ a)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
⊢ ∀ (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W

Tactic:
a

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
W X : C
a : W ⟶ X
⊢ ∀ (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ (Sieve.overEquiv Y₂) (Sieve.pullback f S₁) ∈ J Y₂.left

Tactic:
Sieve.overEquiv_pullback

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ Sieve.pullback (Over.Hom.left f) ((Sieve.overEquiv Y₁) S₁) ∈ J Y₂.left
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : (Sieve.overEquiv (Over.mk (f ≫ Y.hom))) (Sieve.pullback (Over.homMk f ⋯) R) ∈ J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z

Tactic:
Sieve.overEquiv_pullback

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
hS : S ∈ ⇑(Sieve.overEquiv Y) ⁻¹' J Y.left
R : Sieve Y
Z : C
f : Z ⟶ Y.left
hR : Sieve.pullback (Over.Hom.left (Over.homMk f ⋯)) ((Sieve.overEquiv Y) R) ∈ J (Over.mk (f ≫ Y.hom)).left
hf : ((Sieve.overEquiv Y) S).arrows f
⊢ Sieve.pullback f ((Sieve.overEquiv Y) R) ∈ J Z
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (E.map (Over.forget X)).sieve₀ ∈ J ((Over.forget X).obj Y)

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
· dsimp
    rw [dsimp% PreZeroHypercover.sieve₀_map (F := Over.forget X)]
    exact E.mem₀

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Simple (of R M) ↔ IsSimpleModule R M

Tactic:
rw [simple_iff_subobject_isSimpleOrder, (subobjectModule (of R M)).isSimpleOrder_iff,
    isSimpleModule_iff]

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ ∀ (x y : α), HasLimit (pair x y)

Tactic:
let := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α

Goal state after:
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
this : (∀ (J : Type u) {𝒥 : SmallCategory J} (x : FinCategory J), HasLimitsOfShape J α) → HasFiniteLimits α :=
  hasFiniteLimits_of_hasFiniteLimits_of_size α
⊢ ∀ (x y : α), HasLimit (pair x y)
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
⊢ HasBinaryProducts α

Tactic:
have : ∀ x y : α, HasLimit (pair x y) := by
    let := hasFiniteLimits_of_hasFiniteLimits_of_size.{u} α
    infer_instance

Goal state after:
α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
this : ∀ (x y : α), HasLimit (pair x y)
⊢ HasBinaryProducts α
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
X : Opens T
S : Presieve X
Ti : ⦃Y : Opens T⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | ∀ x ∈ X, ∃ U f, R f ∧ x ∈ U}
hTi : ∀ ⦃Y : Opens T⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | ∀ x ∈ Y, ∃ U f, R f ∧ x ∈ U}
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : S f
hU : x ∈ U
V : Opens T
g : V ⟶ U
hg : Ti f hf g
hV : x ∈ V
⊢ ∃ U f, S.bind Ti f ∧ x ∈ U

Tactic:
exact ⟨_, _, ⟨_, g, f, hf, hg, rfl⟩, hV⟩

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
⊢ (grothendieckTopology T).CoversTop U ↔ IsOpenCover U

Tactic:
rw [GrothendieckTopology.coversTop_iff_of_isTerminal _ ⊤ isTerminalTop]

Goal state after:
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
⊢ Sieve.ofObjects U ⊤ ∈ (grothendieckTopology T) ⊤ ↔ IsOpenCover U
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
⊢ ((pullback C f).obj ℱ).map (homOfLE le).op ≫ (pullbackObjObjOfImageOpen f ℱ U HU).hom =
    (pullbackObjObjOfImageOpen f ℱ V HV).hom ≫ ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
by
  dsimp [pullbackObjObjOfImageOpen]
  refine ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V)).hom_ext
    (fun j ↦ ?_)
  have eq : ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op V)).ι.app j ≫ ((pullback C f).obj ℱ).map (homOfLE le).op =
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
      (op U)).ι.app ((CostructuredArrow.map (homOfLE le).op).obj j) := by cat_disch
  rw [Limits.IsColimit.comp_coconePointUniqueUpToIso_hom_assoc, reassoc_of% eq,
    Limits.IsColimit.comp_coconePointUniqueUpToIso_hom,
    Limits.coconeOfDiagramTerminal_ι_app, Limits.coconeOfDiagramTerminal_ι_app]
  dsimp
  rw [← Functor.map_comp]
  cat_disch

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
i j : ι
⊢ (ConcreteCategory.hom (F.obj.map ((U i).infLELeft (U j)).op)) (sf i) =
    (ConcreteCategory.hom (F.obj.map ((U i).infLERight (U j)).op)) (sf j)

Tactic:
sf,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
i j : ι
⊢ (ConcreteCategory.hom (F.obj.map ((U i).infLELeft (U j)).op)) ((ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s) =
    (ConcreteCategory.hom (F.obj.map ((U i).infLERight (U j)).op))
      ((ConcreteCategory.hom (F.obj.map (leSupr U j).op)) s)