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

Goal state before:
pp: 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 ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
h₁ : S ≤ Presheaf.imageSieve α r
h₂ : S ≤ Presheaf.imageSieve φ m
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows :=
  Presieve.FamilyOfElements.restrict h₁ (Presieve.FamilyOfElements.localPreimage (whiskerRight α (forget RingCat)) r)
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows :=
  Presieve.FamilyOfElements.restrict h₂ (Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget Ab)) m)
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
⊢ (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m

Tactic:
Presieve.FamilyOfElements.restrict_map

Goal state after:
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 ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
h₁ : S ≤ Presheaf.imageSieve α r
h₂ : S ≤ Presheaf.imageSieve φ m
r₀ : Presieve.FamilyOfElements (R₀ ⋙ forget RingCat) S.arrows :=
  Presieve.FamilyOfElements.restrict h₁ (Presieve.FamilyOfElements.localPreimage (whiskerRight α (forget RingCat)) r)
m₀ : Presieve.FamilyOfElements (M₀.presheaf ⋙ forget Ab) S.arrows :=
  Presieve.FamilyOfElements.restrict h₂ (Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget Ab)) m)
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
⊢ (Presieve.FamilyOfElements.restrict h₂
        ((Presieve.FamilyOfElements.localPreimage (whiskerRight φ (forget Ab)) m).map
          (whiskerRight φ (forget Ab)))).IsAmalgamation
    m
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Fintype J
j : Bicone J
⊢ j ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

Tactic:
by
    cases j <;> simp [Fintype.complete]

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)
inst✝¹ : HasFiniteLimits C
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
⊢ PreservesFiniteLimits F.op.lan

Tactic:
have := flat_of_preservesFiniteLimits F
  infer_instance

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

Goal state before:
pp: case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ (ConcreteCategory.hom (P.map gg.op)) ((ConcreteCategory.hom (P.map g.op)) t₁) =
    (ConcreteCategory.hom (P.map gg.op)) ((ConcreteCategory.hom (P.map g.op)) t₂)

Tactic:
simp only [← comp_apply]

Goal state after:
case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f R).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : S.arrows (gg ≫ g ≫ f)
⊢ (ConcreteCategory.hom (P.map g.op ≫ P.map gg.op)) t₁ = (ConcreteCategory.hom (P.map g.op ≫ P.map gg.op)) t₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.IsStableUnderComposition
E : J.ZeroHypercover T
F : J.ZeroHypercover T
inst✝ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ (E.inter F.toPreZeroHypercover).presieve₀ ∈ J.coverings T

Tactic:
PreZeroHypercover.inter_def,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.IsStableUnderComposition
E : J.ZeroHypercover T
F : J.ZeroHypercover T
inst✝ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
⊢ ((E.bind fun i ↦ PreZeroHypercover.pullback₁ (E.f i) F.toPreZeroHypercover).reindex
        (Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm).presieve₀ ∈
    J.coverings T
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.h
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (Sieve.pullback f (Sieve.generate S)).arrows f_1 → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong T f_1

Tactic:
intro Z g _
      obtain ⟨R, hR1, hR2⟩ := K.pullback g _ hT1
      exact ⟨R, (H _ hR1).isSeparatedFor, hR2⟩

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
← PreZeroHypercover.sieve₀,

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F 𝒰.sieve₀.arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W✝ : A
f g : W✝ ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi : (↑⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)

Tactic:
reassoc_of% eq

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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W✝ : A
f g : W✝ ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
W : C
i : W ⟶ unop j.right
hi : (↑⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i
eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)
⊢ g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
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.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map 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 (G.imageSieve i)).arrows f →
      (ConcreteCategory.hom (ℱ.obj.map f.op)) s = (ConcreteCategory.hom (ℱ.obj.map f.op)) t

Tactic:
rintro Z _ ⟨W, iWX, iZW, ⟨iWY, e⟩, 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.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map 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
iWY : W ⟶ Y
e : G.map iWY = G.map iWX ≫ i
⊢ (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) s = (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) t
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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
Z : C
iZY : G.obj Z ⟶ Y
W : D
V : C
iVZ : V ⟶ Z
iWV : W ⟶ G.obj V
iVX : V ⟶ X
e : G.map iVX = G.map iVZ ≫ iZY ≫ iYX
⊢ (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))).arrows
    (iWV ≫ G.map iVZ)

Tactic:
exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
h₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯) (v₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k

Tactic:
subst h₀
  simp [h₁]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ (i, j).1 (i, j).2
i' j' : E.I₀
k' : E.I₁ (i', j').1 (i', j').2
left : i = i'
right : j = j'
h : (congrIndexOneOfEq left right) ⟨(i, j), k⟩.snd = ⟨(i', j'), k'⟩.snd
⊢ ⟨(i, j), k⟩ = ⟨(i', j'), k'⟩

Tactic:
subst left right

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j : E.I₀
k k' : E.I₁ (i, j).1 (i, j).2
h : (congrIndexOneOfEq ⋯ ⋯) ⟨(i, j), k⟩.snd = ⟨(i, j), k'⟩.snd
⊢ ⟨(i, j), k⟩ = ⟨(i, j), k'⟩
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (Precoverage.comap G K.toPrecoverage).toGrothendieck U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)

Tactic:
induction hS with
    | of X S hS => rwa [← Sieve.generate_map_eq_functorPushforward]
    | top X => simp
    | pullback X S _ Y f ih =>
      apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
        ⟨_, K.pullback_stable (G.map f) ih⟩)
      rintro Z _ ⟨U, iUY, iZU, ⟨W, iWX, iUW, hiWX, e₁⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU Z
      apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
      rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable
      clear iZU₁ Z
      apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
        (iU₁U ≫ iUY ≫ f) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
      rintro Z _ ⟨U₂, iU₂U₁, iZU₂, e₃ : _ = _, rfl⟩
      refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
      simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)
    | transitive X S R _ _ hS H' =>
      apply K.transitive hS
      rintro Y _ ⟨Z, g, i, hg, rfl⟩
      rw [Sieve.pullback_comp]
      apply K.pullback_stable i
      refine K.superset_covering ?_ (H' hg)
      rintro W _ ⟨Z', g', i', hg, rfl⟩
      refine ⟨Z', g' ≫ g, i', hg, ?_⟩
      simp

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

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom (F.obj.map e.inv.op))
      ((ConcreteCategory.hom (((Over.map f).op ⋙ F.obj).map g₁'.op)) (x g₁ hg₁))

pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom (F.obj.map e.inv.op))
      ((ConcreteCategory.hom (((Over.map f).op ⋙ F.obj).map g₂'.op)) (x g₂ hg₂))

Tactic:
all_goals
      dsimp [e, W', g₁', g₂']
      rw [← Functor.map_comp_apply]
      apply ConcreteCategory.congr_hom
      congr 1
      rw [← op_comp]
      congr 1
      ext
      simp

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ (ConcreteCategory.hom f) x ∈ hf.functorObj U ↔ x ∈ U

Tactic:
by
  conv_rhs => rw [← hf.map_functorObj U]
  rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
D' : Type u₃
inst✝² : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝¹ : Category.{v₄, u₄} D''
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
⊢ pushforward φ ⋙ forgetToSheafModuleCat S X hX ≅
    forgetToSheafModuleCat R (F.op.obj X) hX' ⋙
      sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X))) ⋙
        F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K

Tactic:
refine NatIso.ofComponents (fun M ↦ ObjectProperty.isoMk _ ?_) ?_
  · refine NatIso.ofComponents (fun U ↦ ?_) ?_
    · refine (ModuleCat.restrictScalarsComp'App _ _ _ ?_ _).symm ≪≫
        (ModuleCat.restrictScalarsComp _ _).app _
      rw [← RingCat.hom_comp, ← RingCat.hom_comp, φ.hom.naturality]
      dsimp
      rw [hX'.hom_ext (hX'.to (Opposite.op (F.obj (Opposite.unop U)))) _]
    · cat_disch
  · cat_disch

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

Goal state before:
pp: case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
h :
  ∀ (sf : (i : ι) → ToType (F.obj (op (U i)))),
    F.IsCompatible U sf →
      ∃! s,
        ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
          (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s = objPairwiseOfFamily sf i
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j

Tactic:
specialize h (fun i ↦ s <| op <| Pairwise.single i) fun i j ↦
      (hs <| op <| Pairwise.Hom.left i j).trans (hs <| op <| Pairwise.Hom.right i j).symm

Goal state after:
case refine_2
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
⊢ ∃! x,
    ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x : C
⊢ Sieve.ofObjects id x = ⊤

Tactic:
Sieve.ext_iff

Goal state after:
C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ x), (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : ContinuousAdd B'
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
have : Continuous φ := continuous_of_linearMapₛₗ hσ.continuous φ

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Ring R
inst✝⁷ : Ring S
A : Type u_3
inst✝⁶ : AddCommGroup A
inst✝⁵ : Module R A
inst✝⁴ : TopologicalSpace A
inst✝³ : IsModuleTopology R A
B' : Type u_5
inst✝² : AddCommGroup B'
inst✝¹ : Module S B'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝¹ : ContinuousAdd A
this✝ : ContinuousAdd B'
this : Continuous[inst✝⁴, τB] ⇑φ
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
⊢ Projective ((uliftFunctor.{v', v, u} R).obj M)

Tactic:
by
    have := small_lift.{u, v'} R
    dsimp
    infer_instance

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : ¬IsInvertible 0
⊢ inverse 0 = 0

Tactic:
exact inverse_of_not_isInvertible h

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

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| f (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₁ : J.fst b = J.snd b
f : (left (J.snd b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| False
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
x✝ : ↑X.toModuleCat
⊢ (hom (ofHom ↑e ≫ ofHom ↑e.symm)) x✝ = (hom (𝟙 X)) x✝

Tactic:
exact e.symm_apply_apply _

Goal state after: