mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Opposites

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsLimitsOfShape (Discrete (Fin x✝)) F.leftOp

Tactic:
apply +allowSynthFailures reflectsLimitsOfShape_leftOp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ Dᵒᵖ
inst✝ : ReflectsFiniteCoproducts F
x✝ : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
⊢ smul α φ (r + r') m = smul α φ r m + smul α φ r' m

Tactic:
have hS : S ∈ J X.unop := by
    refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
    all_goals apply Presheaf.imageSieve_mem

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ (r + r') m = smul α φ r m + smul α φ r' m
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
⊢ smul α φ (r * r') m = smul α φ r (smul α φ r' m)

Tactic:
have hS : S ∈ J X.unop := by
    refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
    all_goals apply Presheaf.imageSieve_mem

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
⊢ smul α φ (r * r') m = smul α φ r (smul α φ r' m)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
⊢ ∀ S ∈ J₁ X, Presieve.IsSheafFor (Functor.closedSieves J₁).toFunctor S.arrows

Tactic:
S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → Presieve.IsSheafFor (Functor.closedSieves J₁).toFunctor S.arrows
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (N ⊓ ?m.161) ∈ J₁ Y

pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve X

Tactic:
← MSNS

Goal state after:
case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (M ⊓ S) ∈ J₁ Y
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
⊢ J₁ X ⊆ J₂ X

Tactic:
S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
S : Sieve X
⊢ S ∈ J₁ X → S ∈ J₂ X
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f ((c X) R) = ⊤

Tactic:
← hc

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (c Y) (Sieve.pullback f R) = ⊤
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
⊢ ∀ S ∈ J.toGrothendieck X, Presieve.IsSheafFor P S.arrows

Tactic:
S

Goal state after:
case mpr
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Sieve X
⊢ S ∈ J.toGrothendieck X → Presieve.IsSheafFor P S.arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))

Tactic:
intro i
    rw [Presieve.ofArrows_pUnit]
    exact K.mem_coverings_of_isIso _

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve Y
inst✝ : R.HasPullbacks f
⊢ (Presieve.pullbackArrows f R).FactorsThruAlong R f

Tactic:
by
  intro Z g ⟨W, b, hb⟩
  have := R.hasPullback f hb
  refine ⟨_, pullback.fst _ _, b, hb, pullback.condition⟩

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
⊢ ∀ S ∈ {S | Sieve.generate S ∈ J X}, ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f

Tactic:
S

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
J : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ {S | Sieve.generate S ∈ J X} → ∃ T ∈ {S | Sieve.generate S ∈ J Y}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
H : K.toGrothendieck ≤ J
X : C
⊢ K.coverings X ⊆ J.toCoverage.coverings X

Tactic:
S

Goal state after:
case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
H : K.toGrothendieck ≤ J
X : C
S : Presieve X
⊢ S ∈ K.coverings X → S ∈ J.toCoverage.coverings X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
H : K ≤ J.toCoverage
X : C
⊢ K.toGrothendieck X ⊆ J X

Tactic:
S

Goal state after:
case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
H : K ≤ J.toCoverage
X : C
S : Sieve X
⊢ S ∈ K.toGrothendieck X → S ∈ J X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X : C
⊢ K.toGrothendieck X ⊆ J X

Tactic:
S

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X : C
S : Sieve X
⊢ S ∈ K.toGrothendieck X → S ∈ J X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
⊢ K.coverings X ⊆ K.toGrothendieck.toCoverage.coverings X

Tactic:
S

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Presieve X
⊢ S ∈ K.coverings X → S ∈ K.toGrothendieck.toCoverage.coverings X
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_1.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hle : ∃ R_1 ∈ J.coverings X, R_1 ≤ R.arrows
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
| transitive X R S hR hRS hle hfS =>

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

Goal state before:
pp: case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
⊢ ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
S

Goal state after:
case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X : C
S : Presieve X
⊢ S ∈ K.coverings X → IsSheafFor P S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
⊢ ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
S

Goal state after:
case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
⊢ S ∈ K.coverings X → IsSheafFor P (Sieve.pullback f (Sieve.generate S)).arrows
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : D ⥤ C
x✝ : E
⊢ (((whiskeringLeft E D C).obj G).map
            ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
                  naturality := ⋯ }.app
              X) ≫
          { app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom, naturality := ⋯ }.app
            (((whiskeringLeft E D C).obj G).obj X)).app
      x✝ =
    (𝟙 (((whiskeringLeft E D C).obj G).obj X)).app x✝

Tactic:
simp [← X.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Whiskering

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : D ⥤ E
G : E ⥤ D
adj : F ⊣ G
X : E ⥤ C
x✝ : D
⊢ ({ app := fun X ↦ ((𝟭 (D ⥤ C)).obj X).leftUnitor.inv ≫ whiskerRight adj.unit X ≫ (F.associator G X).hom,
                naturality := ⋯ }.app
            (((whiskeringLeft D E C).obj F).obj X) ≫
          ((whiskeringLeft D E C).obj F).map
            ({ app := fun X ↦ (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
                  naturality := ⋯ }.app
              X)).app
      x✝ =
    (𝟙 (((whiskeringLeft D E C).obj F).obj X)).app x✝

Tactic:
simp [← X.map_comp]

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

Goal state before:
pp: 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)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
F : J.ZeroHypercover (E.X i)
hle' : Presieve.ofArrows F.X F.f ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
use F

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
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₂)
⊢ (E.map F).sieve₁ (F.map p₁) (F.map p₂) ≤ Sieve.functorPushforward F (E.sieve₁ p₁ p₂)

Tactic:
rintro T f ⟨k, u, hf₁, hf₂⟩

Goal state after:
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
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
⊢ ∀ ⦃S : Sieve X⦄, S ∈ J X → K.W (H'.map (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S).ι)

Tactic:
S

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve X
⊢ S ∈ J X → K.W (H'.map (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S).ι)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_1
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
⊢ ∀ {S : Sieve U}, S ∈ K U → Sieve.functorPushforward G S ∈ J (G.obj U)

Tactic:
S

Goal state after:
case refine_1
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : F.IsCocontinuous J K
U : D
S : Sieve U
⊢ S ∈ K U → Sieve.functorPushforward G S ∈ J (G.obj U)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_2
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
⊢ ∀ {S : Sieve (F.obj U)}, S ∈ K (F.obj U) → Sieve.functorPullback F S ∈ J U

Tactic:
S

Goal state after:
case refine_2
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
⊢ S ∈ K (F.obj U) → Sieve.functorPullback F S ∈ J U
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
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
X : D
⊢ ∀ (S : K.Cover X), Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.obj)))

Tactic:
S

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
inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
ℱ : Sheaf J A
X : D
S : K.Cover X
⊢ Nonempty (IsLimit (S.multifork (G.op.ran.obj ℱ.obj)))
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
⊢ G.imageSieve (G.map f) = ⊤

Tactic:
by
  ext W g; simpa using ⟨g ≫ f, by simp⟩

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

Tactic:
simp only [TypeCat.Fun.toFun_apply, types_comp_apply, ← map_comp_apply]

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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ (ConcreteCategory.hom (ℱ'.obj.map f'.op))
      ((ConcreteCategory.hom (appHom α (unop Y))) ((ConcreteCategory.hom (ℱ.map f)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (f ≫ f'.op))) ((ConcreteCategory.hom (appHom α (unop X))) x)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
this :
  (f₁ ≫ (G.op.ranCounit.app Y.obj).app (op U)) ≫ Y.obj.map iVU.op =
    (f₂ ≫ (G.op.ranCounit.app Y.obj).app (op U)) ≫ Y.obj.map iVU.op
⊢ (f₁ ≫ (G.op.ran.obj Y.obj).map (op g) ≫ (G.op.ranCounit.app Y.obj).app (op W)) ≫ Y.obj.map iVW.op =
    (f₂ ≫ (G.op.ran.obj Y.obj).map (op g) ≫ (G.op.ranCounit.app Y.obj).app (op W)) ≫ Y.obj.map iVW.op

Tactic:
simp only [Category.assoc, ← NatTrans.naturality] at this ⊢

Goal state after:
case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
this :
  f₁ ≫ (G.op ⋙ G.op.ran.obj Y.obj).map iVU.op ≫ (G.op.ranCounit.app Y.obj).app (op V) =
    f₂ ≫ (G.op ⋙ G.op.ran.obj Y.obj).map iVU.op ≫ (G.op.ranCounit.app Y.obj).app (op V)
⊢ f₁ ≫
      (G.op.ran.obj Y.obj).map (op g) ≫ (G.op ⋙ G.op.ran.obj Y.obj).map iVW.op ≫ (G.op.ranCounit.app Y.obj).app (op V) =
    f₂ ≫
      (G.op.ran.obj Y.obj).map (op g) ≫ (G.op ⋙ G.op.ran.obj Y.obj).map iVW.op ≫ (G.op.ranCounit.app Y.obj).app (op V)