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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
⊢ ∀ (U : Cᵒᵖ), Function.Surjective ⇑(ConcreteCategory.hom (f.app U))

Tactic:
intro U

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝³ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
inst✝ : IsIso f
U : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app U))
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁✝ F₂✝ F₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
Y : C
f : Y ⟶ unop X
s : F₁.obj.obj (op Y)
hs : (ConcreteCategory.hom (φ.hom.app (op Y))) s = (ConcreteCategory.hom (F₂.obj.map f.op)) x
h₁ :
  (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)) x)
h₂ :
  (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (F₂.obj.map f.op)) x) =
    (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)) x)
⊢ (ConcreteCategory.hom (f₁.hom.app (op Y))) ((ConcreteCategory.hom (φ.hom.app (op Y))) s) =
    (ConcreteCategory.hom (f₂.hom.app (op Y))) ((ConcreteCategory.hom (φ.hom.app (op Y))) s)

Tactic:
exact ConcreteCategory.congr_hom (congr_app ((sheafToPresheaf J _).congr_map h) (op Y)) s

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
⊢ (Hom.hom S.g).ker = (↑e' ∘ₛₗ Hom.hom S.g).ker

Tactic:
LinearEquiv.ker_comp

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
⊢ (Hom.hom S.g).ker = (Hom.hom S.g).ker
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
a : α
⊢ Sigma.ι (fun x ↦ R) (f a) ≫ Cofork.π (sigmaConstCokernelCofork R f) = 0

Tactic:
dsimp [sigmaConstCokernelCofork]
  rw [Sigma.ι_desc]
  exact dif_neg (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
R : C
inst✝ : HasCoproducts C
α β : Type w
f : α ⟶ β
⊢ HasCokernel ((sigmaConst.obj R).map f)

Tactic:
dsimp; infer_instance

Goal state after:
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
    exact reflectsColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Goal state after:
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
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • r₀' • m₀) =
    (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r (smul α φ r' m))

Tactic:
map_smul_eq α φ r (smul α φ r' m) f.op r₀ hr₀ (r₀' • m₀)
      (map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀).symm

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)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ↑(M₀.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • r₀' • m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • 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₀.obj X)
m₀ : ↑(M₀.obj X)
⊢ (ConcreteCategory.hom (φ.app X)) (r₀ • m₀) = r₀ • (ConcreteCategory.hom (φ.app X)) m₀

Tactic:
simpa using! (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
      r₀ (by simp) m₀ (by simp)).symm

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

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

Tactic:
ext i

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

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

Tactic:
ext i

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫
      G.map ((L.pointwiseRightKanExtensionCounit F).app a) =
    (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a

Tactic:
simpa [-pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.ran ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.rightKanExtensionCompIsoOfPreserves F' L).hom =
    (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.ran).map η

Tactic:
apply hom_ext_of_isRightKanExtension
        (L.rightKanExtension <| F' ⋙ G)
        (L.rightKanExtensionCounit <| F' ⋙ G)

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁶ : Category.{v_1, u_1} A
inst✝⁵ : Category.{v_2, u_2} B
inst✝⁴ : Category.{v_3, u_3} C
inst✝³ : Category.{v_4, u_4} D
G : B ⥤ D
F✝ : A ⥤ B
L : A ⥤ C
inst✝² : G.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ L.whiskerLeft ((L.ran ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.rightKanExtensionCompIsoOfPreserves F' L).hom) ≫
      L.rightKanExtensionCounit (F' ⋙ G) =
    L.whiskerLeft ((G.rightKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.ran).map η) ≫
      L.rightKanExtensionCounit (F' ⋙ G)
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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
⊢ K.W (H.map f)

Tactic:
intro U

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
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
⊢ Presheaf.IsSheaf K U → Function.Bijective fun g ↦ H.map f ≫ g
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
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
⊢ K.W (H.map f)

Tactic:
intro U

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
A : Type u
inst✝¹ : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ A) ⥤ Dᵒᵖ ⥤ A
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ A
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ A
⊢ Presheaf.IsSheaf K U → Function.Bijective fun g ↦ H.map f ≫ g
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:
intro U

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:
intro U

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
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
j j' : StructuredArrow (op X) G.op
φ : j ⟶ j'
⊢ ((Functor.const (StructuredArrow (op X) G.op)).obj s.1).map φ ≫ liftAux hF α s j'.hom.unop =
    liftAux hF α s j.hom.unop ≫ (StructuredArrow.proj (op X) G.op ⋙ F).map φ

Tactic:
simpa using liftAux_map' hF α s j'.hom.unop j.hom.unop (𝟙 _) φ.right.unop
          (Quiver.Hom.op_inj (by simpa using (StructuredArrow.w φ).symm))

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

Goal state before:
pp: case transitive
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
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
⊢ Sieve.functorPushforward G R ∈ K (G.obj X)

Tactic:
apply K.transitive hS

Goal state after:
case transitive
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
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄,
    (Sieve.functorPushforward G S).arrows f → Sieve.pullback f (Sieve.functorPushforward G R) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case refine_2.refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ∈ (comap F K).toGrothendieck X

Tactic:
exact Precoverage.generate_mem_toGrothendieck (H hR)

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

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ J.W f ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f

Tactic:
← W_whiskerLeft_iff J K G f,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁸ : Category.{v₃, u₃} A
inst✝⁷ : G.IsCoverDense J
inst✝⁶ : G.Full
inst✝⁵ : G.IsContinuous K J
inst✝⁴ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝³ : G.IsCocontinuous K J
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : K.WEqualsLocallyBijective A
hG : CoverPreserving K J G
X✝ Y✝ : Cᵒᵖ ⥤ A
f : X✝ ⟶ Y✝
⊢ K.W (G.op.whiskerLeft f) ↔ Presheaf.IsLocallyInjective J f ∧ Presheaf.IsLocallySurjective J f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve U.left
hS : (Sieve.overEquiv U).symm S ∈ (J.over X) U
⊢ S ∈ J ((Over.map f).obj U).left

Tactic:
simpa [mem_over_iff] using! hS

Goal state after:
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
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ (Sieve.overEquiv U) (Sieve.functorPullback (Over.post F) S) ∈ J U.left

Tactic:
Sieve.overEquiv_functorPullback_post

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.IsCocontinuous J K
U : Over X
S : Sieve ((Over.post F).obj U)
hS : (Sieve.overEquiv ((Over.post F).obj U)) S ∈ K ((Over.post F).obj U).left
⊢ Sieve.functorPullback F ((Sieve.overEquiv ((Over.post F).obj U)) S) ∈ J U.left
Module: Mathlib.Topology.Category.TopCat.Opens

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

Tactic:
intro U

Goal state after:
case refine_1
X : TopCat
U : Opens ↑((toTopCat X).obj ⊤)
⊢ ⋯.functor.obj U = (map (inclusionTopIso X).inv).obj U
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
⊢ ∀ (U : Opens ↑X), Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U

Tactic:
intro U

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
⊢ Sieve.coverByImage B U ∈ (Opens.grothendieckTopology ↑X) U
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
⊢ {c : Opens ↑X} → {d : Opens ↑Y} → (d ⟶ hf.functor.obj c) → (c' : Opens ↑X) × (hf.functor.obj c' ≅ d)

Tactic:
intro U

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
⊢ {d : Opens ↑Y} → (d ⟶ hf.functor.obj U) → (c' : Opens ↑X) × (hf.functor.obj c' ≅ d)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
⊢ ∀ (X_1 : Opens ↑X), IsCofiltered (StructuredArrow X_1 (Opens.map f))

Tactic:
intro U

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ IsCofiltered (StructuredArrow U (Opens.map f))
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ ∀ {U : Opens ↑Y} {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑Y) U →
      Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)

Tactic:
intro U

Goal state after:
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
⊢ ∀ {S : Sieve U},
    S ∈ (Opens.grothendieckTopology ↑Y) U →
      Sieve.functorPushforward (Opens.map f) S ∈ (Opens.grothendieckTopology ↑X) ((Opens.map f).obj U)