mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F

Tactic:
by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
  intro J _ _; constructor
  intro K; constructor
  intro c hc
  constructor
  exact
    { lift := PreservesFiniteLimitsOfFlat.lift F hc
      fac := PreservesFiniteLimitsOfFlat.fac F hc
      uniq := fun s m h => by
        apply PreservesFiniteLimitsOfFlat.uniq F hc
        · exact h
        · exact PreservesFiniteLimitsOfFlat.fac F hc s }

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } ≫
      { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } =
    𝟙 (pullback₁ f E)

Tactic:
apply Hom.ext (by rfl)
    simp only [heq_eq_eq]
    ext i
    simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S✝ T✝ : C
E✝ : PreZeroHypercover S✝
F : PreZeroHypercover S✝
S T : C
f : S ⟶ T
E : PreZeroHypercover T
inst✝¹ : ∀ (i : E.I₀), HasPullback f (E.f i)
inst✝ : ∀ (i : E.I₀), HasPullback (E.f i) f
⊢ { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).inv, w₀ := ⋯ } ≫
      { s₀ := id, h₀ := fun i ↦ (pullbackSymmetry f (E.f i)).hom, w₀ := ⋯ } =
    𝟙 (pullback₂ f E)

Tactic:
apply Hom.ext (by rfl)
    simp only [heq_eq_eq]
    ext i
    simp

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J K : Precoverage C
inst✝ : J.Small
of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X
S : C
E : (J ⊓ K).ZeroHypercover S
⊢ (E.restrictIndex (ZeroHypercover.Small.restrictFun (E.weaken ⋯))).presieve₀ ∈ K.coverings S

Tactic:
exact of_le (by simp) E.mem₀.2

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

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_1, u_2} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R

Tactic:
Coverage.toGrothendieck_toPrecoverage,

Goal state after:
C : Type u_2
inst✝² : Category.{v_1, u_2} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toCoverage.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor P R
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
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ F.map f ≫ F.map p₁ = F.map u ≫ (E.map F).p₁ k

Tactic:
simp [← Functor.map_comp, hf₁]

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
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
⊢ Sieve.functorPushforward F (E.sieve₁' i₁ 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₂)))

Tactic:
have : HasPullback ((E.map F).f i₁) ((E.map F).f i₂) :=
    hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
  refine le_antisymm ?_ ?_
  · rw [PreOneHypercover.sieve₁'_eq_sieve₁]
    apply PreOneHypercover.functorPushforward_sieve₁_map_le
  · 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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
P : Sheaf K E
⊢ (F.sheafPushforwardContinuous E J K).map
        ({ app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).unit.app P.obj }, naturality := ⋯ }.app P) ≫
      { app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).counit.app P.obj }, naturality := ⋯ }.app
        ((F.sheafPushforwardContinuous E J K).obj P) =
    𝟙 ((F.sheafPushforwardContinuous E J K).obj P)

Tactic:
by
    ext : 1
    exact (adj.op.whiskerLeft _).left_triangle_components P.obj

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (Sieve.functorPushforward F (Sieve.ofArrows Y f)).arrows

Tactic:
rw [Sieve.ofArrows, ← Sieve.generate_map_eq_functorPushforward,
      ← Presieve.isSheafFor_iff_generate, Presieve.map_ofArrows]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
I' : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g₁, ⋯⟩ := { Y := I.Y, f := I.f ≫ i, hf := ⋯ }
⊢ G.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯) = G.map (l I.Y W₁ U I'.f g₁ ⋯)

Tactic:
by simp [I', hl]

Goal state after:
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
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
H : ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
P : Sheaf K (Type (max u₁ v₁ u₂ v₂))
Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor (F.op ⋙ P.obj) (Sieve.pullback f S).arrows

Tactic:
rw [Presieve.isSheafFor_iff_bijective_shrinkFunctor_ι_comp]

Goal state after:
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
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
H : ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
P : Sheaf K (Type (max u₁ v₁ u₂ v₂))
Y : C
f : Y ⟶ X
⊢ Function.Bijective fun g ↦ (Sieve.shrinkFunctor.{max (max (max u₁ u₂) v₁) v₂, v₁, u₁} (Sieve.pullback f S)).ι ≫ g
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: case e'_2
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : (Functor.const J).obj (K.obj c.pt) ⟶ (Functor.const J).obj B := ⋯
e_1✝ :
  (K.obj
        (((Functor.const J).obj
                (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).obj
            j).left ⟶
      B) =
    (((Functor.const J).obj (K.obj c.pt)).obj j ⟶ ((Functor.const J).obj B).obj j)
⊢ K.map (c.π.app j) ≫ (F.obj j).hom = z.app j

Tactic:
simp [z]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: case e'_3
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : (Functor.const J).obj (K.obj c.pt) ⟶ (Functor.const J).obj B := ⋯
e_1✝ :
  (K.obj
        (((Functor.const J).obj
                (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).obj
            j).left ⟶
      B) =
    (((Functor.const J).obj (K.obj c.pt)).obj j ⟶ ((Functor.const J).obj B).obj j)
⊢ (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).obj
        j).hom =
    z.app (Classical.arbitrary J)

Tactic:
simp [z]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f) →
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f

pp: case mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f →
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)

Tactic:
· rintro h _ ⟨R, rfl⟩
    exact (h₂ R).1 (h _ ⟨R, rfl⟩)

Goal state after:
case mpr
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
h₂ : ∀ (R : Sheaf J A), (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g
⊢ ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A).obj) f →
    ObjectProperty.isLocal (fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj)
      (((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map f)
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W (whiskerRight (G.op.whiskerLeft f) F)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
rw [whiskerRight_left] at this

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
⊢ PreservesFiniteLimits colim

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v₂}
  intro J _ _
  refine ⟨fun {F} => ⟨fun {c} hc => ⟨IsLimit.ofIsoLimit (limit.isLimit _) ?_⟩⟩⟩
  symm
  trans colim.mapCone (limit.cone F)
  · exact Functor.mapIso _ (hc.uniqueUpToIso (limit.isLimit F))
  · exact asIso (colimitLimitToLimitColimitCone F)

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

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.fst
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd) =
    (G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝) ≫
      pullback.fst
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd)

Tactic:
simpa using f.w₁₁ k

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)
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i

Tactic:
have hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (_ : W ⟶ Y i), F.map a.op (s X) = s W := by
      intro W X a i b
      rw [hs i b]
      exact (Presieve.IsSheafFor.valid_glue (H _ (hY X))
        (hx.familyOfElements_isCompatible _) a ⟨i, ⟨b⟩⟩).trans (familyOfElements_apply hx _ _ _)

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
⊢ ∃ x_1, ∀ (i : I), ↑x_1 (Opposite.op (Y i)) = x i
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback (Over.post F) S ≤
    functorPullback (Over.forget X) (functorPullback F (functorPushforward (Over.forget (F.obj X)) S))

Tactic:
← Sieve.functorPullback_comp

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback (Over.post F) S ≤ functorPullback (Over.forget X ⋙ F) (functorPushforward (Over.forget (F.obj X)) S)
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
⊢ Function.Injective (F.colimitTypePrecomp P)

pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x

Tactic:
· have h (Y : D) : ∃ (a : P.obj Y → (F ⋙ P).ColimitType), ∀ (j : StructuredArrow Y F),
        (F ⋙ P).ιColimitType j.right ∘ P.map j.hom = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ f
      ext x
      dsimp
      rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]
      simp [← comp_apply, ← Functor.map_comp]
    choose φ hφ using h
    let c : P.CoconeTypes :=
      { pt := (F ⋙ P).ColimitType
        ι Y := φ Y
        ι_naturality {Y₁ Y₂} f := by
          ext
          have X : StructuredArrow Y₂ F := Classical.arbitrary _
          rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]
          simp }
    refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)
    obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x
    simp [c, ← hφ (F.obj X) (StructuredArrow.mk (𝟙 _))]

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
x : P.ColimitType
⊢ ∃ a, F.colimitTypePrecomp P a = x
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
X✝ Y✝ : SheafOfModules R
e : X✝ ≅ Y✝
⊢ isFinitePresentation R X✝ → isFinitePresentation R Y✝

Tactic:
intro ⟨σ, hσ⟩

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
X✝ Y✝ : SheafOfModules R
e : X✝ ≅ Y✝
σ : X✝.QuasicoherentData
hσ : σ.IsFinitePresentation
⊢ isFinitePresentation R Y✝
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair.pair
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ List.IsChain Zag
    [{ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a },
      { left := { as := PUnit.unit }, right := single i, hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := single i', hom := ObjectProperty.homMk (homOfLE ⋯) },
      { left := { as := PUnit.unit }, right := Pairwise.pair i' j', hom := b }]

Tactic:
exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.cons_cons
                  (Or.inr
                    ⟨{  left := 𝟙 _
                        right := left i' j' }⟩)
                  (List.IsChain.singleton _))))

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 v
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝ : PreservesFilteredColimits (forget C)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
s t : CC ((stalkFunctor C x).obj F)
hst : (ConcreteCategory.hom ((stalkFunctor C x).map α)) s = (ConcreteCategory.hom ((stalkFunctor C x).map α)) t
⊢ s = t

Tactic:
obtain ⟨U₁, hxU₁, hU₁, s, rfl⟩ := exists_mem_germ_eq_of_isBasis hB _ x s

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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F G : Presheaf C X
α : F ⟶ G
hα : ∀ U ∈ B, Function.Injective ⇑(ConcreteCategory.hom (α.app (op U)))
x : ↑X
t : CC ((stalkFunctor C x).obj F)
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
hU₁ : U₁ ∈ B
s : ToType (F.obj (op U₁))
hst :
  (ConcreteCategory.hom ((stalkFunctor C x).map α)) ((ConcreteCategory.hom (F.germ U₁ x hxU₁)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map α)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = t