mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
Y : D
⊢ ∀ (f_1 : Y ⟶ B), (Sieve.generate (Presieve.singleton f)).arrows f_1 → (Sieve.coverByImage G B).arrows f_1

Tactic:
f

Goal state after:
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
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f✝ : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f✝) ∈ K B
Y : D
f : Y ⟶ B
⊢ (Sieve.generate (Presieve.singleton f✝)).arrows f → (Sieve.coverByImage G B).arrows 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
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
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
x : ℱ.obj.obj (op X)
Y : C
⊢ ∀ (f : G.obj Y ⟶ X),
    (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (appHom i.hom X ≫ appHom i.inv X)).toFun x) =
      (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (𝟙 (ℱ.obj.obj (op X)))).toFun x)

Tactic:
f

Goal state after:
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
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
x : ℱ.obj.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (appHom i.hom X ≫ appHom i.inv X)).toFun x) =
    (ConcreteCategory.hom (ℱ.obj.map f.op)) ((ConcreteCategory.hom (𝟙 (ℱ.obj.obj (op X)))).toFun x)
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
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
x : ℱ'.obj.obj (op X)
Y : C
⊢ ∀ (f : G.obj Y ⟶ X),
    (ConcreteCategory.hom (ℱ'.obj.map f.op)) ((ConcreteCategory.hom (appHom i.inv X ≫ appHom i.hom X)).toFun x) =
      (ConcreteCategory.hom (ℱ'.obj.map f.op)) ((ConcreteCategory.hom (𝟙 (ℱ'.obj.obj (op X)))).toFun x)

Tactic:
f

Goal state after:
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
ℱ✝ : Dᵒᵖ ⥤ Type v
ℱ'✝ : Sheaf K (Type v)
α : G.op ⋙ ℱ✝ ⟶ G.op ⋙ ℱ'✝.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K (Type v)
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : D
x : ℱ'.obj.obj (op X)
Y : C
f : G.obj Y ⟶ X
⊢ (ConcreteCategory.hom (ℱ'.obj.map f.op)) ((ConcreteCategory.hom (appHom i.inv X ≫ appHom i.hom X)).toFun x) =
    (ConcreteCategory.hom (ℱ'.obj.map f.op)) ((ConcreteCategory.hom (𝟙 (ℱ'.obj.obj (op X)))).toFun x)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case hT
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
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ Sieve.coverByImage G (unop U) ∈ K (unop U)

Tactic:
apply G.is_cover_of_isCoverDense

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

Goal state before:
pp: case h
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
⊢ ∀ (f : Y ⟶ G.obj (unop X)) (h : (Sieve.coverByImage G (G.obj (unop X))).arrows f),
    (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
        (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
        this) =
      pushforwardFamily (homOver α (unop U)) x✝ f h

Tactic:
f

Goal state after:
case h
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
⊢ ∀ (h : (Sieve.coverByImage G (G.obj (unop X))).arrows f),
    (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
        (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
        this) =
      pushforwardFamily (homOver α (unop U)) x✝ f h
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
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
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
⊢ ∀ (f : Y ⟶ unop X) (h : (Sieve.coverByImage G (unop X)).arrows f),
    (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
        (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
        this) =
      pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝ f h

Tactic:
f

Goal state after:
case h
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
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
⊢ ∀ (h : (Sieve.coverByImage G (unop X)).arrows f),
    (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
        (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
        this) =
      pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝ f h
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
⊢ ∀ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows

Tactic:
f

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
⊢ (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
⊢ ∀ ⦃f : Y ⟶ Z⦄, (Sieve.pullback g S).arrows f → Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
f

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
⊢ (Sieve.pullback g S).arrows f → Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
Module: Mathlib.CategoryTheory.Sites.InducedTopology

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
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
hS : S ∈ (F.inducedTopology K) X
Y : C
⊢ ∀ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

Tactic:
f

Goal state after:
case refine_1
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
hS : S ∈ (F.inducedTopology K) X
Y : C
f : Y ⟶ X
⊢ K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
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
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (h₁ k).hom ≫ (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
← PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc
      (z := fun i j k ↦ (h₁ k).hom) (hii' := by simp) (hjj' := by simp),

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫
      (h₁ ((congrIndexOneOfEq ⋯ ⋯) k)).hom ≫
        eqToHom ⋯ ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯
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
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone (limit.cone F) ≅ limit.cone (F ⋙ colim)

Tactic:
exact asIso (colimitLimitToLimitColimitCone F)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
⊢ ∀ (f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)),
    ⊤.arrows f → (E.toPreOneHypercover.sieve₁' i j).arrows f

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
⊢ ⊤.arrows f → (E.toPreOneHypercover.sieve₁' i j).arrows f
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
a✝ : ⊤.arrows f
⊢ (E.toPreOneHypercover.sieve₁' i j).arrows f

Tactic:
refine ⟨pullback (E.f i) (E.f j), f, 𝟙 _, ?_, by simp⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
a✝ : ⊤.arrows f
⊢ Presieve.ofArrows E.toPreOneHypercover.Y (fun j_1 ↦ E.toPreOneHypercover.toPullback j_1)
    (𝟙 (pullback (E.f i) (E.f j)))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
⊢ ∀ (f : y ⟶ ((Over.star X).obj U).left),
    (Sieve.pullback prod.snd S).arrows f →
      ((Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)).arrows f

Tactic:
f

Goal state after:
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
⊢ (Sieve.pullback prod.snd S).arrows f →
    ((Sieve.overEquiv ((Over.star X).obj U)) (Sieve.functorPushforward (Over.star X) S)).arrows f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1.transitive
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y✝ : C
right : Discrete PUnit.{1}
R✝ : Sieve Y✝
Y : C
R S : Sieve Y
hR : K.toCoverage.Saturate Y R
H : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → K.toCoverage.Saturate Y_1 (Sieve.pullback f S)
ih :
  ∀ (s : Y ⟶ X),
    (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
      (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
ih' :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f →
      ∀ (s : Y_1 ⟶ X),
        (Sieve.overEquiv { left := Y_1, right := right, hom := s }).symm (Sieve.pullback f S) ∈
          (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y_1, right := right, hom := s }
s : Y ⟶ X
⊢ (Sieve.overEquiv { left := Y, right := right, hom := s }).symm S ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }

Tactic:
| transitive Y R S hR H ih ih' =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: 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
Y : D
Z₁ Z₂ : StructuredArrow Y F
⊢ ∀ (x : Z₁ ⟶ Z₂),
    (F ⋙ P).ιColimitType Z₁.right ∘ ⇑(ConcreteCategory.hom (P.map Z₁.hom)) =
      (F ⋙ P).ιColimitType Z₂.right ∘ ⇑(ConcreteCategory.hom (P.map Z₂.hom))

Tactic:
f

Goal state after:
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
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
⊢ (F ⋙ P).ιColimitType Z₁.right ∘ ⇑(ConcreteCategory.hom (P.map Z₁.hom)) =
    (F ⋙ P).ιColimitType Z₂.right ∘ ⇑(ConcreteCategory.hom (P.map Z₂.hom))
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
intro h
        have j : IsIso (f ≫ i.hom) := by
          apply isIso_of_mono_of_nonzero
          intro w
          apply h
          simpa using (cancel_mono i.inv).2 w
        rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
        infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: 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) [Mono f], IsIso f ↔ f ≠ 0

Tactic:
f

Goal state after:
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
⊢ ∀ [Mono f], IsIso f ↔ f ≠ 0
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
⊢ ⋯.functor = map (inclusionTopIso X).inv

Tactic:
refine CategoryTheory.Functor.ext ?_ ?_

Goal state after:
case refine_1
X : TopCat
⊢ ∀ (X_1 : Opens ↑((toTopCat X).obj ⊤)), ⋯.functor.obj X_1 = (map (inclusionTopIso X).inv).obj X_1

case refine_2
X : TopCat
⊢ ∀ (X_1 Y : Opens ↑((toTopCat X).obj ⊤)) (f : X_1 ⟶ Y),
    ⋯.functor.map f = eqToHom ⋯ ≫ (map (inclusionTopIso X).inv).map f ≫ eqToHom ⋯
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
this :
  u.app j.left ≫ ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left)))
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    u.app j.left ≫
      ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left ≫ ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
rw [reassoc_of% this]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
this :
  u.app j.left ≫ ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left)))
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫
        ((Opens.map f).op.leftKanExtension 𝒢).map j.hom
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
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
⊢ ∀ (f : G.obj X ⟶ Y),
    PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁,
        max (max (u + 1) u₂) v₂}
      (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))

Tactic:
f

Goal state after:
C : Type u₁
inst✝¹⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹³ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝¹² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
S : Sheaf K RingCat
inst✝¹⁰ : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝⁹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝⁸ : ∀ (X : D), HasSheafify (K.over X) AddCommGrpCat
G : D ⥤ C
inst✝⁷ : G.IsContinuous K J
inst✝⁶ : G.IsCocontinuous K J
φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R
η : (pushforward φ).obj (unit R) ≅ unit S
inst✝⁵ : G.IsLeftAdjoint
inst✝⁴ : IsIso φ
inst✝³ : ∀ (X : D), (Over.post G).IsContinuous (K.over X) (J.over (G.obj X))
inst✝² : HasPullbacks C
inst✝¹ : HasPullbacks D
M : SheafOfModules R
inst✝ : M.IsQuasicoherent
X : D
Y : C
f : G.obj X ⟶ Y
⊢ PreservesColimitsOfSize.{u, u, max (max u u₁) v₁, max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
    (pushforward (((Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).map φ))
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 Y✝ : C
⊢ ∀ (f : Y✝ ⟶ x), (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f

Tactic:
f

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 Y✝ : C
f : Y✝ ⟶ x
⊢ (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (diagram U).obj X_1 ⟶ (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj X_1

Tactic:
rintro (i | ⟨i, j⟩) <;> exact 𝟙 _

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
⊢ (X_1 : CategoryTheory.Pairwise ι) →
    (pairwiseToOpensLeCover U ⋙ ObjectProperty.ι fun V ↦ ∃ i, V ≤ U i).obj X_1 ⟶ (diagram U).obj X_1

Tactic:
rintro (i | ⟨i, j⟩) <;> exact 𝟙 _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
x : ↑X
U V : (OpenNhds x)ᵒᵖ
i : U ⟶ V
W : Opens ↑Y
hW : unop (op ((OpenNhds.inclusion x).obj (unop U))) ≤ (Opens.map f).obj W
⊢ ((pullbackPushforwardAdjunction C f).unit.app F).app (op W) ≫
      ((pullback C f).obj F).map ((homOfLE hW).op ≫ (⋯.functor.map i.unop).op) ≫
        germToPullbackStalk C f F (↑(unop V)) x ⋯ =
    F.germ W ((ConcreteCategory.hom f) x) ⋯

Tactic:
erw [pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk]

Goal state after: