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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
T : C
u : T ⟶ S
hu : Presieve.ofArrows X f u
⊢ T = X (incl (Sum.inl ⟨⟨T, u⟩, hu⟩))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
T : C
u : T ⟶ S
hu : Presieve.ofArrows X f u
⊢ u = eqToHom ⋯ ≫ f (incl (Sum.inl ⟨⟨T, u⟩, hu⟩))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : ι'
u : T ⟶ X (incl (Sum.inl i))
hu : Presieve.ofArrows (Y (incl (Sum.inl i))) (g (incl (Sum.inl i))) u
⊢ T = Y (incl (Sum.inl i)) (fibincl (Sum.inl i) ⟨⟨T, u⟩, hu⟩)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : ι'
u : T ⟶ X (incl (Sum.inl i))
hu : Presieve.ofArrows (Y (incl (Sum.inl i))) (g (incl (Sum.inl i))) u
⊢ u = eqToHom ⋯ ≫ g (incl (Sum.inl i)) (fibincl (Sum.inl i) ⟨⟨T, u⟩, hu⟩)

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : α
u : T ⟶ X (incl (Sum.inr i))
hu : Presieve.ofArrows (Y (incl (Sum.inr i))) (g (incl (Sum.inr i))) u
⊢ T = Y (incl (Sum.inr i)) (fibincl (Sum.inr i) (Sum.inr ⟨⟨T, u⟩, hu⟩))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : α
u : T ⟶ X (incl (Sum.inr i))
hu : Presieve.ofArrows (Y (incl (Sum.inr i))) (g (incl (Sum.inr i))) u
⊢ u = eqToHom ⋯ ≫ g (incl (Sum.inr i)) (fibincl (Sum.inr i) (Sum.inr ⟨⟨T, u⟩, hu⟩))

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ (generate R).arrows ≤ S.arrows

Tactic:
apply giGenerate.gc.monotone_u

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
PK : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X : C
S : Sieve X
R : Presieve X
hR : R ∈ K.coverings X
RS : R ≤ S.arrows
⊢ generate R ≤ S
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : HasPullbacks C
K : Pretopology C
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) → IsSheaf K.toGrothendieck P

Tactic:
rintro PK X S ⟨R, hR, RS⟩
    have gRS : ⇑(generate R) ≤ S := by
      apply giGenerate.gc.monotone_u
      rwa [generate_le_iff]
    apply isSheafFor_subsieve P gRS _
    intro Y f
    rw [← pullbackArrows_comm, ← isSheafFor_iff_generate]
    exact PK (pullbackArrows f R) (K.pullbacks f R hR)

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
h : T ⟶ Y
⊢ ofArrows (fun i ↦ pullback (g i) f) (fun x ↦ pullback.snd (g x) f) h → pullbackArrows f (ofArrows Z g) h

Tactic:
rintro ⟨hk⟩
    exact pullbackArrows.mk _ _ (ofArrows.mk hk)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
s : Cocone S.arrows.diagram
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
hf₁ : S.arrows f₁
hf₂ : S.arrows f₂
hgf : g₁ ≫ f₁ = g₂ ≫ f₂
Hs :
  ∀ ⦃X_1 Y : S.arrows.category⦄ (f : X_1 ⟶ Y),
    S.arrows.diagram.map f ≫ s.ι.app Y = s.ι.app X_1 ≫ ((Functor.const S.arrows.category).obj s.pt).map f
hgf₁ : S.arrows (g₁ ≫ f₁)
hgf₂ : S.arrows (g₂ ≫ f₂)
F : Over.mk (g₁ ≫ f₁) ⟶ Over.mk (g₂ ≫ f₂) := Over.homMk (𝟙 Z) ⋯
F₁ : Over.mk (g₁ ≫ f₁) ⟶ Over.mk f₁ := Over.homMk g₁ ⋯
F₂ : Over.mk (g₂ ≫ f₂) ⟶ Over.mk f₂ := Over.homMk g₂ ⋯
hF :
  S.arrows.diagram.map (ObjectProperty.homMk F) ≫ s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F)
hF₁ :
  S.arrows.diagram.map (ObjectProperty.homMk F₁) ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } =
    s.ι.app { obj := Over.mk (g₁ ≫ f₁), property := hgf₁ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F₁)
hF₂ :
  S.arrows.diagram.map (ObjectProperty.homMk F₂) ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ } =
    s.ι.app { obj := Over.mk (g₂ ≫ f₂), property := hgf₂ } ≫
      ((Functor.const S.arrows.category).obj s.pt).map (ObjectProperty.homMk F₂)
⊢ g₁ ≫ s.ι.app { obj := Over.mk f₁, property := hf₁ } = g₂ ≫ s.ι.app { obj := Over.mk f₂, property := hf₂ }

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H✝ : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
f : S.arrows.category
H : ∃! t, (S.arrows.yonedaFamilyOfElements_fromCocone s).IsAmalgamation t
ht :
  (ConcreteCategory.hom ((yoneda.obj s.pt).map f.obj.hom.op)) (Exists.choose H) =
    S.arrows.yonedaFamilyOfElements_fromCocone s f.obj.hom ⋯
⊢ S.arrows.cocone.ι.app f ≫ Exists.choose ⋯ = s.ι.app f

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a : Presieve.FamilyOfElements P S.arrows
| (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
rw [(firstObjEqFamily P S.arrows).toEquiv_symm_apply]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
a : Presieve.FamilyOfElements P S.arrows
| (ConcreteCategory.hom (firstObjEqFamily P S.arrows).inv) a
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
R : Presieve X
inst✝ : LocallySmall.{w, v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
t : (shrinkFunctor.{w, v₁, u₁} S).toFunctor ⟶ F
⊢ (fun t ↦ { app := fun X_1 ↦ ↾fun f ↦ ↑t (shrinkYonedaObjObjEquiv ↑f) ⋯, naturality := ⋯ })
      ((fun t ↦ ⟨fun Y f hf ↦ (ConcreteCategory.hom (t.app (op Y))) ⟨shrinkYonedaObjObjEquiv.symm f, ⋯⟩, ⋯⟩) t) =
    t

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
S : Sieve X
⊢ sieveOfUliftSubfunctor S.uliftFunctorInclusion = S

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ Y✝ Z✝ : C
f✝ : Y✝ ⟶ X✝
S✝ R : Sieve X✝
inst✝ : LocallySmall.{w, v₁, u₁} C
X : C
S : Sieve X
Y Z : Cᵒᵖ
g : Y ⟶ Z
f : (shrinkYoneda.{w, v₁, u₁}.obj X).obj Y
hf : f ∈ {f | S.arrows (shrinkYonedaObjObjEquiv f)}
⊢ f ∈ ⇑(hom ((shrinkYoneda.{w, v₁, u₁}.obj X).map g)) ⁻¹' {f | S.arrows (shrinkYonedaObjObjEquiv f)}

Tactic:
simpa [shrinkYonedaObjObjEquiv_obj_map] using S.downward_closed hf _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (ConcreteCategory.hom (forkMap P X π)) t =
      (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)

Tactic:
rw [Equiv.eq_symm_apply, ← Equiv.symm_apply_eq]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    (equivShrink ((j : I) → P.obj (op (X j)))).symm
        ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
      x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F G : Sheaf J A
f g : F ⟶ G
⊢ f = g ↔ f.hom = g.hom

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
F G : Sheaf J A
f g : F ⟶ G
h : f.hom = g.hom
⊢ f = g

Tactic:
cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
⊢ Over.homMk (Over.Hom.left g₁) ⋯ ≫ f i₁ = Over.homMk (Over.Hom.left g₂) ⋯ ≫ f i₂

Tactic:
cat_disch

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

Goal state before:
pp: case e'_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₁ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)

Tactic:
cat_disch

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

Goal state before:
pp: case e'_3
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
Y : I → Over B
f : (i : I) → Y i ⟶ X
s : Subtype (Arrows.Compatible ((Over.map p).op ⋙ P) f)
i₁ i₂ : I
Z : Over B'
g₁ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₁
g₂ : Z ⟶ (fun i ↦ (Over.map p).obj (Y i)) i₂
h : Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) = Over.Hom.left g₂ ≫ Over.Hom.left (f i₂)
φ : Z ⟶ (Over.map p).obj (Over.mk (Over.Hom.left g₁ ≫ Over.Hom.left (f i₁) ≫ X.hom)) := Over.homMk (𝟙 Z.left) ⋯
this :
  (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₁) ⋯)).op)) (↑s i₁) =
    (ConcreteCategory.hom (P.map (φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)).op)) (↑s i₂)
⊢ g₂ = φ ≫ (Over.map p).map (Over.homMk (Over.Hom.left g₂) ⋯)

Tactic:
cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
G' : Subfunctor F'
⊢ G.image f ≤ G' ↔ G ≤ G'.preimage f

Tactic:
by
  simp [Subfunctor.le_def]

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

Goal state before:
pp: case e'_2.refine_1.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
B B' : C
p : B ⟶ B'
P : (Over B')ᵒᵖ ⥤ Type w
X : Over B
X' : Over B'
e : (Over.map p).obj X ≅ X'
ι : Type (max u₁ v₁)
Z : ι → Over B
g : (i : ι) → Z i ⟶ X
W : Over B'
T : Over B
a : W ⟶ (Over.map p).obj T
Y : Over B
i : ι
b : T ⟶ Z i
⊢ Over.homMk (Over.Hom.left a ≫ Over.Hom.left b) ⋯ ≫ (Over.map p).map (g i) = a ≫ (Over.map p).map (b ≫ g i)

Tactic:
cat_disch

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

Goal state before:
pp: case left.left.id
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
a : S.shape.L
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a)) ≫
      (match WalkingMulticospan.left a with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left a with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))

Tactic:
cat_disch

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

Goal state before:
pp: case left.right.fst
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.fst b) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (S.shape.fst b) with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.fst b)

Tactic:
cat_disch

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

Goal state before:
pp: case left.right.snd
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.snd b) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (S.shape.snd b) with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.snd b)

Tactic:
cat_disch

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

Goal state before:
pp: case right.right.id
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁴ : Category.{v₂, u₂} A
B : Type u₃
inst✝³ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝² : J.HasSheafCompose F
inst✝¹ : J.HasSheafCompose G
inst✝ : J.HasSheafCompose H
P : Cᵒᵖ ⥤ A
X : C
S : J.Cover X
b : S.shape.R
⊢ (S.index (P ⋙ F)).multicospan.map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b)) ≫
      (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.right b with
        | WalkingMulticospan.left a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((S.index (P ⋙ F)).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      ((S.index P).multicospan ⋙ F).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))

Tactic:
cat_disch

Goal state after: