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

Goal state before:
pp: case rj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve α r ∈ J (Opposite.unop X)

pp: case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve φ m ∈ J (Opposite.unop X)

Tactic:
all_goals apply Presheaf.imageSieve_mem

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

Goal state before:
pp: case rj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve α r ∈ J (Opposite.unop X)

pp: case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
⊢ Presheaf.imageSieve φ m ∈ J (Opposite.unop X)

Tactic:
all_goals apply Presheaf.imageSieve_mem

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
⊢ Presheaf.imageSieve α r ∈ J (Opposite.unop X)

pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
⊢ Presheaf.imageSieve φ m ∈ J (Opposite.unop X)

pp: case refine_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m m' : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m ⊓ Presheaf.imageSieve φ m'
⊢ Presheaf.imageSieve φ m' ∈ J (Opposite.unop X)

Tactic:
all_goals apply Presheaf.imageSieve_mem

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
⊢ Presheaf.imageSieve α r ∈ J (Opposite.unop X)

pp: case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
⊢ Presheaf.imageSieve α r' ∈ J (Opposite.unop X)

pp: case refine_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
⊢ Presheaf.imageSieve φ m ∈ J (Opposite.unop X)

Tactic:
all_goals apply Presheaf.imageSieve_mem

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

Goal state before:
pp: case rj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y) := ⋯
⊢ Presheaf.imageSieve α ((ConcreteCategory.hom (R.obj.map π)) r) ∈ J (Opposite.unop Y)

pp: case sj
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop Y) := ⋯
⊢ Presheaf.imageSieve φ ((ConcreteCategory.hom (A.obj.map π)) m) ∈ J (Opposite.unop Y)

Tactic:
all_goals apply Presheaf.imageSieve_mem

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝¹⁰ : SmallCategory C
inst✝⁹ : SmallCategory D
E : Type u₂
inst✝⁸ : Category.{u₁, u₂} E
FE : E → E → Type u_1
CE : E → Type u₁
inst✝⁷ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝⁶ : ConcreteCategory E FE
inst✝⁵ : HasLimits E
inst✝⁴ : HasColimits E
inst✝³ : ReflectsLimits (forget E)
inst✝² : PreservesFilteredColimits (forget E)
inst✝¹ : PreservesLimits (forget E)
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F.op.lan

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{u₁}
  intro J _ _
  apply preservesLimitsOfShape_of_evaluation (F.op.lan : (Cᵒᵖ ⥤ E) ⥤ Dᵒᵖ ⥤ E) J
  intro K
  have : IsFiltered (CostructuredArrow F.op K) :=
    IsFiltered.of_equivalence (structuredArrowOpEquivalence F (unop K))
  exact preservesLimitsOfShape_of_natIso (lanEvaluationIsoColim _ _ _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
let T := StructuredArrow.pre X F G
  obtain ⟨Y⟩ := IsCofiltered.nonempty (C := StructuredArrow X G)
  obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)
  have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩
  suffices IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G)) by constructor
  refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩
  · let U := IsCofiltered.min (T.obj A) (T.obj B)
    let A' : StructuredArrow U.right F := .mk (IsCofiltered.minToLeft (T.obj A) (T.obj B)).right
    let B' : StructuredArrow U.right F := .mk (IsCofiltered.minToRight (T.obj A) (T.obj B)).right
    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom,
      StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_,
      StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_, trivial⟩
    · simp [← Functor.map_comp, A', T]
    · simp [← Functor.map_comp, B', T]
  · let U := IsCofiltered.eq (T.map f) (T.map g)
    let A' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g)).right
    let B' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f).right
    let f' : A' ⟶ B' := StructuredArrow.homMk f.right rfl
    let g' : A' ⟶ B' := StructuredArrow.homMk g.right
      congr($(IsCofiltered.eq_condition (T.map f) (T.map g)).right).symm
    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom,
      StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_, ?_⟩
    · simp [← Functor.map_comp, A', T]
    · ext
      exact congr($(IsCofiltered.eq_condition f' g').right)

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X),
    j ≫ i₁ = j ≫ i₂ →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s = (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t
⊢ ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj X⦄,
    (Sieve.functorPushforward G (Sieve.equalizer i₁ i₂)).arrows f →
      (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t

Tactic:
rintro Z _ ⟨W, iWX, iZW, hiWX, rfl⟩

Goal state after:
C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_2)
X Y : C
i₁ i₂ : X ⟶ Y
e : G.map i₁ = G.map i₂
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X),
    j ≫ i₁ = j ≫ i₂ →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s = (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
hiWX : (Sieve.equalizer i₁ i₂).arrows iWX
⊢ (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) s = (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) t
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ equalizerSieve ((ConcreteCategory.hom (F.map m.op)) a) ((ConcreteCategory.hom (F.map m.op)) b) ≤
    Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))

pp: case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) a) =
    (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) b)

Tactic:
· intro W q hq
      simpa using hq

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) a) =
    (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map m.op)) b)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
⊢ functorPushforward (Over.forget X) (functorPullback (Over.forget X) S) = S

Tactic:
by
  apply arrows_ext
  simp [← arrows_generate_map_eq_functorPushforward]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
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)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map φ.op)) (s Y₂)

Tactic:
rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]

Goal state after:
case hex
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)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map f.op ≫ F.map φ.op)) (s Y₁)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
⊢ Sieve.functorPushforward (Over.star X) S ∈ (J.over X) ((Over.star X).obj U)

Tactic:
refine J.superset_covering ?_ (J.pullback_stable prod.snd hs)
    intro y f hf
    dsimp [Sieve.overEquiv]
    rw [← Presieve.functorPushforward_comp]
    refine ⟨_, _, prod.lift (f ≫ prod.fst) (𝟙 _), hf, Limits.prod.hom_ext ?_ ?_⟩ <;> simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
U V : Opens ↑X
i : U ⟶ V
x : ↑X
hx : x ∈ U
inst✝ : ConcreteCategory C FC
s : CC (F.obj (op V))
⊢ (ConcreteCategory.hom (F.germ U x hx)) ((ConcreteCategory.hom (F.map i.op)) s) =
    (ConcreteCategory.hom (F.germ V x ⋯)) s

Tactic:
rw [← ConcreteCategory.comp_apply, germ_res]

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : OpenNhds x
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op U) ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op U) ≫ f₂

Tactic:
obtain ⟨U, hxU⟩ := U; exact ih U hxU

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ ℱ.map ((NatTrans.op (OpenNhds.inclusionMapIso (𝟙 X) x).inv).app (op ⟨U✝, hxU✝⟩)) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op ⟨U✝, hxU✝⟩) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ) (op ⟨U✝, hxU✝⟩) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom

Tactic:
erw [CategoryTheory.Functor.map_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
ℱ : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : (ConcreteCategory.hom (𝟙 X)) x ∈ U✝
⊢ 𝟙 (ℱ.obj ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x) ⋙ Opens.map (𝟙 X)).op.obj (op ⟨U✝, hxU✝⟩))) ≫
      colimit.ι
          ((OpenNhds.map (𝟙 X) x).op ⋙
            ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (op ⟨U✝, hxU✝⟩) ≫
        colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ)
          (OpenNhds.map (𝟙 X) x).op =
    colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom (𝟙 X)) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ) (op ⟨U✝, hxU✝⟩) ≫
      (stalkFunctor C x).map (Pushforward.id ℱ).hom
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (ConcreteCategory.hom (G.map iWU₁.op)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.map iWU₂.op)) ((ConcreteCategory.hom (f.app (op U₂))) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t

Tactic:
rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply, ← f.naturality, ← f.naturality,
    ConcreteCategory.comp_apply, ConcreteCategory.comp_apply] at heq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom (G.germ U₁ x hxU₁)) ((ConcreteCategory.hom (f.app (op U₁))) s) =
    (ConcreteCategory.hom (G.germ U₂ x hxU₂)) ((ConcreteCategory.hom (f.app (op U₂))) t)
W : Opens ↑X
hxW : x ∈ W
iWU₁ : W ⟶ U₁
iWU₂ : W ⟶ U₂
heq :
  (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₁.op)) s) =
    (ConcreteCategory.hom (f.app (op W))) ((ConcreteCategory.hom (F.map iWU₂.op)) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous id

Tactic:
show (id : R → R) = (fun rs ↦ rs.1 • rs.2) ∘ (fun r ↦ (r, 1)) by ext; simp

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1))
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (uliftFunctor.{v', v} R)).out 1 3).mp
    (uliftFunctor_map_exact R)
  exact this.2

Goal state after: