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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
hER : E.presieve₀ = R
⊢ F.presieve₀ ≤ T

Tactic:
rintro - - ⟨i⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
hER : E.presieve₀ = R
Y : C
i : F.I₀
⊢ T (F.f i)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → Presieve.ofArrows Y f g → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
refine ⟨ι, fun i ↦ j _ _ (.mk i), ?_⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
j : (Z : C) → (g : Z ⟶ S) → Presieve.ofArrows Y f g → E.I₀
h₁ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), Z = E.X (j Z g hg)
h₂ : ∀ (Z : C) (g : Z ⟶ S) (hg : Presieve.ofArrows Y f g), g = eqToHom ⋯ ≫ E.f (j Z g hg)
⊢ (E.restrictIndex fun i ↦ j (Y i) (f i) ⋯).presieve₀ ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1.transitive
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleS : ∃ R ∈ J.coverings X, R ≤ S.arrows
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
| transitive X S T hS hT hleS hleT =>

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

Goal state before:
pp: case refine_1
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₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ k) (E.p₂ k) ⋯
⊢ f ≫ F.map l = u ≫ F.map r

Tactic:
apply (IsPullback.map _ (.of_hasPullback _ _)).hom_ext

Goal state after:
case refine_1.h₀
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₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := ⋯
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := ⋯
⊢ (f ≫ F.map l) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂))

case refine_1.h₁
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₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := ⋯
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
hl₂ : l ≫ pullback.snd (E.f i₁) (E.f i₂) = p₂
r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := ⋯
⊢ (f ≫ F.map l) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) = (u ≫ F.map r) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩),
    (liftAux hF α s f ≫ F.map a.op) ≫ F.map I.f.op = (liftAux hF α s f' ≫ F.map b.op) ≫ F.map I.f.op

Tactic:
rintro ⟨T, g, hg⟩

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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y Y' : C
f : G.obj Y ⟶ X
f' : G.obj Y' ⟶ X
W : C
a : W ⟶ Y
b : W ⟶ Y'
w : G.map a ≫ f = G.map b ≫ f'
T : C
g : T ⟶ W
hg : (↑⟨Sieve.functorPullback G (Sieve.pullback (G.map a ≫ f) ↑S), ⋯⟩).arrows g
⊢ (liftAux hF α s f ≫ F.map a.op) ≫ F.map { Y := T, f := g, hf := hg }.f.op =
    (liftAux hF α s f' ≫ F.map b.op) ≫ F.map { Y := T, f := g, hf := hg }.f.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_1.h₀
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ (f ≫ p) ≫ pullback.fst ((E.inter F).f i) ((E.inter F).f j) =
    (a ≫ (E.inter F).toPullback k) ≫ pullback.fst ((E.inter F).f i) ((E.inter F).f j)

Tactic:
apply pullback.hom_ext <;> simp [p, h₁, toPullback]

Goal state after:
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).map f ≫ presheafHom (homOver α (unop Y)) =
    presheafHom (homOver α (unop X)) ≫ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj).map f

Tactic:
ext U x
    change
      appHom (homOver α (unop Y)) (unop U) (f.unop ≫ x) =
        f.unop ≫ appHom (homOver α (unop X)) (unop U) x
    symm
    apply sheaf_eq_amalgamation
    · apply G.is_cover_of_isCoverDense
    -- Porting note: the following line closes a goal which didn't exist before reenableeta
    · exact pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)
    intro Y' f' hf'
    dsimp
    simp only [Category.assoc]
    congr 1
    conv_lhs => rw [← hf'.some.fac]
    simp only [← Category.assoc, op_comp, Functor.map_comp]
    congr 1
    exact (appHom_restrict (homOver α (unop X)) hf'.some.map.op x).trans (by simp)

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

Goal state before:
pp: case h.right
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
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
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
x : Aᵒᵖ
⊢ ((sheafYonedaHom i.inv).app X).app x ≫ ((sheafYonedaHom i.hom).app X).app x = 𝟙 ((yoneda.obj (ℱ'.obj.obj X)).obj x)

Tactic:
exact ((Types.presheafIso (isoOver i (unop x))).app X).inv_hom_id

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

Goal state before:
pp: case refine_1.refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ pullback.fst p ((E.inter F).toPullback k) ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₁ k.1

Tactic:
have : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = p ≫ pullback.fst _ _ ≫ pullback.fst _ _ := by
          simp [p]
        simp [this, pullback.condition_assoc, toPullback]

Goal state after:
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
W : C
q : W ⟶ Z
hq : (equalizerSieve ((ConcreteCategory.hom (F.map m.op)) a) ((ConcreteCategory.hom (F.map m.op)) b)).arrows q
⊢ (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))).arrows q

Tactic:
simpa using hq

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

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePullbackShape J)

Tactic:
apply IsConnected.of_constant_of_preserves_morphisms

Goal state after:
J : Type u_1
⊢ ∀ {α : Type u_1} (F : WidePullbackShape J → α),
    (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePullbackShape J), F j = F j'
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePushoutShape J)

Tactic:
apply IsConnected.of_constant_of_preserves_morphisms

Goal state after:
J : Type u_1
⊢ ∀ {α : Type u_1} (F : WidePushoutShape J → α),
    (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : WidePushoutShape J), F j = F j'
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
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).map (WalkingMulticospan.Hom.fst x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).map (WalkingMulticospan.Hom.fst x✝)

Tactic:
by dsimp; rw [eqToHom_naturality]; apply PreOneHypercover.I₁'.ext <;> simp

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
E F : PreOneHypercover S
f : E ≅ F
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).map (WalkingMulticospan.Hom.snd x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).map (WalkingMulticospan.Hom.snd x✝)

Tactic:
by dsimp; rw [eqToHom_naturality]; apply PreOneHypercover.I₁'.ext <;> simp

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
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).map (WalkingMulticospan.Hom.fst x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (𝟭 (WalkingMulticospan F.multicospanShape)).map (WalkingMulticospan.Hom.fst x✝)

Tactic:
by dsimp; rw [eqToHom_naturality]; apply PreOneHypercover.I₁'.ext <;> simp

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
E F : PreOneHypercover S
f : E ≅ F
x✝ : F.multicospanShape.R
⊢ (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).map (WalkingMulticospan.Hom.snd x✝) ≫ eqToHom ⋯ =
    eqToHom ⋯ ≫ (𝟭 (WalkingMulticospan F.multicospanShape)).map (WalkingMulticospan.Hom.snd x✝)

Tactic:
by dsimp; rw [eqToHom_naturality]; apply PreOneHypercover.I₁'.ext <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
⊢ ((E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)).arrows f✝ →
    (E.sieve₁ p₁ p₂).arrows (Over.homMk f✝ ⋯)

Tactic:
intro ⟨k, b, hb₁, hb₂⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ (E.sieve₁ p₁ p₂).arrows (Over.homMk f✝ ⋯)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
hg : ((overEquiv Y) (generate R)).arrows g
⊢ (generate (Presieve.functorPushforward (Over.forget X) R)).arrows g

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)

Tactic:
· rw [overEquiv_iff] at hg
    obtain ⟨W, u, v, hv, huv⟩ := hg
    exact ⟨W.left, u.left, v.left, ⟨W, v, 𝟙 _, hv, by simp⟩, congr($(huv).left)⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
⊢ generate (Presieve.functorPushforward (Over.forget X) R) ≤ (overEquiv Y) (generate R)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
⊢ S.preOneHypercover.sieve₁ p₁ p₂ = ⊤

Tactic:
ext Y f
  simp only [Sieve.top_apply, iff_true]
  exact ⟨{ w := w, .. }, f, rfl, rfl⟩

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
I : Type u
⊢ Epi ((free I).freeHomEquiv.symm fun i ↦ freeSection i)

Tactic:
by
    simp only [Equiv.symm_apply_apply]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
⊢ HasColimit F

Tactic:
have : HasColimit (pair (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)) :=
      ⟨⟨⟨_, isColimitBinaryCofan (F.obj ⟨WalkingPair.left⟩) (F.obj ⟨WalkingPair.right⟩)⟩⟩⟩

Goal state after:
C : Type u
inst✝ : SemilatticeSup C
F : Discrete WalkingPair ⥤ C
this : HasColimit (pair (F.obj { as := WalkingPair.left }) (F.obj { as := WalkingPair.right }))
⊢ HasColimit F
Module: Mathlib.Topology.Sheaves.Sheaf

Goal state before:
pp: case refine_1
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ Sieve.generate (Presieve.ofArrows V fun x ↦ homOfLE ⋯) ∈ (Opens.grothendieckTopology ↑X) (unop U)

Tactic:
exact fun x hx ↦ ⟨V ⟨x, hx⟩, homOfLE (hV _), Sieve.ofArrows_mk _ _ _, hxV _⟩

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

Goal state before:
pp: case zero
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
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.zero ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.zero

Tactic:
simp [Presentation.mapRelations, GeneratingSections.mapFreeHom, ← Functor.map_comp]

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

Goal state before:
pp: case one
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
C' : Type u₂
inst✝³ : Category.{v₂, u₂} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝² : HasSheafify J' AddCommGrpCat
inst✝¹ : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
F : SheafOfModules R ⥤ SheafOfModules S
inst✝ : PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F
η : unit S ≅ F.obj (unit R)
⊢ ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).ι.app
        WalkingParallelPair.one ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPairIsoMk (mapFreeIso F P.relations.I η).symm (mapFreeIso F P.generators.I η).symm ⋯
                      ⋯).inv).obj
              (F.mapCocone (CokernelCofork.ofπ P.generators.π ⋯))).pt).hom =
    (CokernelCofork.ofπ (P.mapGenerators F η) ⋯).ι.app WalkingParallelPair.one

Tactic:
simp [Presentation.mapRelations, GeneratingSections.mapFreeHom, ← Functor.map_comp]

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

Goal state before:
pp: case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
U₁ U₂ V : Opens ↑X
i₁ : U₁ ⟶ V
i₂ : U₂ ⟶ V
hcover : V ≤ U₁ ⊔ U₂
s t : ToType (F.obj.obj (op V))
h₁ : (ConcreteCategory.hom (F.obj.map i₁.op)) s = (ConcreteCategory.hom (F.obj.map i₁.op)) t
h₂ : (ConcreteCategory.hom (F.obj.map i₂.op)) s = (ConcreteCategory.hom (F.obj.map i₂.op)) t
⊢ ∀ (i : Bool),
    (ConcreteCategory.hom (F.obj.map (if h : i = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) s =
      (ConcreteCategory.hom (F.obj.map (if h : i = true then eqToHom ⋯ ≫ i₁ else eqToHom ⋯ ≫ i₂).op)) t

Tactic:
· rintro ⟨_ | _⟩
    any_goals exact h₁
    any_goals exact h₂

Goal state after: