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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
⊢ ∀ (f_1 : Z ⟶ T), (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows f_1 → (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows f_1

Tactic:
g

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
g : Z ⟶ T
⊢ (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows g → (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows g
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.generate (Presieve.map F (ofArrows Y f))).arrows

Tactic:
← Presieve.isSheafFor_iff_generate,

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 (Presieve.map F (ofArrows Y f))
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
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
⊢ sheafHom (G.op.whiskerLeft α) = α

Tactic:
by
  ext X
  apply yoneda.map_injective
  ext U
  dsimp [sheafHom, -yoneda_obj_obj, -yoneda_map_app]
  rw [yoneda.map_preimage]
  symm
  change (show (ℱ'.obj ⋙ coyoneda.obj (op (unop U))).obj (op (unop X)) from _) = _
  apply sheaf_eq_amalgamation ℱ' (G.is_cover_of_isCoverDense _ _)
  -- Porting note: next line was not needed in mathlib3
  · exact (pushforwardFamily_compatible _ _)
  intro Y f hf
  conv_lhs => rw [← hf.some.fac]
  dsimp; simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
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
⊢ 𝟙 X ≫ ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)

Tactic:
Category.id_comp

Goal state after:
case refine_2
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
⊢ ⋯.amalgamate ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
⊢ (d.ι (f.s₀ (E.multicospanShape.fst k)) ≫ P.map (f.h₀ (E.multicospanShape.fst k)).op) ≫ (E.multicospanIndex P).fst k =
    (d.ι (f.s₀ (E.multicospanShape.snd k)) ≫ P.map (f.h₀ (E.multicospanShape.snd k)).op) ≫ (E.multicospanIndex P).snd k

Tactic:
simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
      multicospanIndex_fst, assoc, multicospanShape_snd, multicospanIndex_snd]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map (f.h₀ k.fst.1).op ≫ P.map (E.p₁ k.snd).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map (f.h₀ k.fst.2).op ≫ P.map (E.p₂ k.snd).op
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
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
        ((sheafifyOfIsEquivalence J K G A).map f ≫ g)) =
    (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g)

Tactic:
congr 1
    apply adj₁.homEquiv_naturality_left

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (E.multicospanIndex P)
⊢ (id E).mapMultiforkOfIsLimit P hc d = Multifork.IsLimit.lift hc d.ι ⋯

Tactic:
apply Multifork.IsLimit.hom_ext hc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (E.multicospanIndex P)
⊢ ∀ (a : E.multicospanShape.L), (id E).mapMultiforkOfIsLimit P hc d ≫ c.ι a = Multifork.IsLimit.lift hc d.ι ⋯ ≫ c.ι a
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: 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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
g : F.Hom G
t : Multifork (G.multicospanIndex P)
hd : IsLimit d
⊢ (f.comp g).mapMultiforkOfIsLimit P hc t = g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d

Tactic:
apply Multifork.IsLimit.hom_ext hc

Goal state after:
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
g : F.Hom G
t : Multifork (G.multicospanIndex P)
hd : IsLimit d
⊢ ∀ (a : E.multicospanShape.L),
    (f.comp g).mapMultiforkOfIsLimit P hc t ≫ c.ι a =
      (g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d) ≫ c.ι a
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.restrictedTopology K = F.inducedTopology K

Tactic:
refine le_antisymm ?_ inducedTopology_le_restrictedTopology
  rw [le_inducedTopology_iff]
  infer_instance

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

Goal state before:
pp: 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
⊢ ∀ ⦃f : Y ⟶ Opposite.unop X⦄,
    (Sieve.coverByImage H (Opposite.unop X)).arrows f → Sieve.pullback f (equalizerSieve a b) ∈ K Y

Tactic:
g

Goal state after:
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
⊢ (Sieve.coverByImage H (Opposite.unop X)).arrows g → Sieve.pullback g (equalizerSieve a b) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case mp
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
X : C
Y : Over X
T : ↑(J ((Over.forget X).obj Y))
Z : C
f : Z ⟶ (Over.forget X).obj Y
⊢ (Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T)).arrows f → (↑T).arrows f

Tactic:
rintro ⟨_, _, g', hg, rfl⟩
      exact T.val.downward_closed hg g'

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
        E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₁ k ≫ (h₀ i).hom ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ i)

Tactic:
simp only [PreZeroHypercover.isoMk_inv_s₀, Category.assoc, PreZeroHypercover.isoMk_inv_h₀,
      Equiv.symm_apply_apply, eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id,
      Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫
        eqToHom ⋯ ≫
          (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv ≫ E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₁ k ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: 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✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
⊢ ∀ ⦃f_1 : Y ⟶ X⦄, (Sieve.coverByImage H X).arrows f_1 → Sieve.pullback f_1 (imageSieve f a) ∈ K Y

Tactic:
g

Goal state after:
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✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
⊢ (Sieve.coverByImage H X).arrows g → Sieve.pullback g (imageSieve f a) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
        E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₂ k ≫ (h₀ j).hom ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ j)

Tactic:
simp only [PreZeroHypercover.isoMk_inv_s₀, Category.assoc, PreZeroHypercover.isoMk_inv_h₀,
      Equiv.symm_apply_apply, eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id,
      Category.comp_id]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫
        eqToHom ⋯ ≫
          (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv ≫ E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    E.p₂ k ≫ eqToHom ⋯
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✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
← eqToHom_naturality _ (by simp),

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ e.inv.h₀ (e.hom.s₀ i) ≫ e.hom.h₀ (e.inv.s₀ (e.hom.s₀ i)) ≫ eqToHom ⋯ = 𝟙 (F.X (e.hom.s₀ i))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S✝ S : C
⊢ (PreOneHypercover.trivial S).sieve₀ ∈ J S

Tactic:
simp only [PreOneHypercover.sieve₀_trivial, J.top_mem]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
hg : ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
⊢ (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g

Tactic:
exact ⟨Over.mk (g.left ≫ Z.hom), Over.homMk g.left,
      Over.homMk (𝟙 _) (by simpa using Over.w g), hg, by cat_disch⟩

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

Goal state before:
pp: case refine_2
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)
Z : C
⊢ ∀ (f : Z ⟶ U.left),
    (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows f →
      ((overEquiv U) (functorPullback (Over.post F) S)).arrows f

Tactic:
g

Goal state after:
case refine_2
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)
Z : C
g : Z ⟶ U.left
⊢ (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g →
    ((overEquiv U) (functorPullback (Over.post F) S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (PreZeroHypercover.map (Over.post F) E.toPreZeroHypercover).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

Tactic:
PreZeroHypercover.sieve₀_map,

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ Sieve.functorPushforward (Over.post F) E.sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
⊢ (Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))

Tactic:
by
  intro Y E
  let E' := (E.map (Over.forget X) J).map F K
  refine ⟨?_, ?_⟩
  · dsimp [-Over.post_obj]
    rw [PreZeroHypercover.sieve₀_map, GrothendieckTopology.mem_over_iff,
      Sieve.functorPushforward_ofArrows, Sieve.overEquiv_ofArrows]
    exact E'.mem₀
  · intro i₁ i₂ W p₁ p₂ w
    simp_rw [GrothendieckTopology.mem_over_iff, Sieve.overEquiv_preOneHypercover_sieve₁,
      ← PreOneHypercover.map_comp, Over.post_forget_eq_forget_comp, PreOneHypercover.map_comp]
    exact E'.mem₁ _ _ _ _ congr($(w).left)

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
· intro h
    replace h := h =≫ biprod.snd
    simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr.inl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f

pp: case mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f

Tactic:
· rw [Subobject.mk_eq_bot_iff_zero] at h
      exact False.elim (i h)

Goal state after:
case mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: case g
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := ⋯
s : Cone (empty (CostructuredArrow (Opens.map f).op (op U)))
⊢ ⇑(ConcreteCategory.hom f) '' ↑(unop ((Opens.map f).op.obj s.pt.left)) ⊆ ↑(unop s.pt.1)

Tactic:
exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)

Goal state after:
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
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
ι σ : Type u
M : SheafOfModules R
f : free ι ⟶ free σ
g : free σ ⟶ M
H : f ≫ g = 0
H' : IsColimit (CokernelCofork.ofπ g H)
⊢ Epi (M.freeHomEquiv.symm (M.freeHomEquiv g))

Tactic:
simpa using! epi_of_isColimit_cofork H'

Goal state after: