mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ≅ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ≅ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    (mapComp (f ≫ g) h).hom ≫
        (mapComp f g).hom ▷ map h ≫
          (α_ (map f) (map g) (map h)).hom ≫ map f ◁ (mapComp g h).inv ≫ (mapComp f (g ≫ h)).inv =
      eqToHom ⋯
map₂_left_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp (𝟙 b₀) f).hom ≫ (mapId b₀).hom ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor :
  ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), (mapComp f (𝟙 b₁)).hom ≫ map f ◁ (mapId b₁).hom ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
x✝ : b✝ ⟶ c✝
⊢ eqToHom ⋯ = (mapComp f✝ x✝).hom ≫ eqToHom ⋯ ▷ map x✝ ≫ (mapComp g✝ x✝).inv

Tactic:
by
    obtain rfl := obj_ext_of_isDiscrete η
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
⊢ ∀ (g : b✝ ⟶ c✝), eqToHom ⋯ ≫ mapComp f'✝ g = mapComp f✝ g ≫ eqToHom ⋯ ▷ map g

Tactic:
by
    obtain rfl := obj_ext_of_isDiscrete η
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete

Goal state before:
pp: B : Type u_1
C : Type u_2
inst✝² : Bicategory B
inst✝¹ : IsLocallyDiscrete B
inst✝ : Bicategory C
obj : B → C
map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b')
mapId : (b : B) → map (𝟙 b) ⟶ 𝟙 (obj b)
mapComp : {b₀ b₁ b₂ : B} → (f : b₀ ⟶ b₁) → (g : b₁ ⟶ b₂) → map (f ≫ g) ⟶ map f ≫ map g
map₂_associator :
  ∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
    eqToHom ⋯ ≫ mapComp f (g ≫ h) ≫ map f ◁ mapComp g h =
      mapComp (f ≫ g) h ≫ mapComp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom
map₂_left_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp (𝟙 b₀) f ≫ mapId b₀ ▷ map f ≫ (λ_ (map f)).hom = eqToHom ⋯
map₂_right_unitor : ∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁), mapComp f (𝟙 b₁) ≫ map f ◁ mapId b₁ ≫ (ρ_ (map f)).hom = eqToHom ⋯
a✝ b✝ c✝ : B
x✝² : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ eqToHom ⋯ ≫ mapComp x✝² x✝ = mapComp x✝² x✝¹ ≫ map x✝² ◁ eqToHom ⋯

Tactic:
by
    obtain rfl := obj_ext_of_isDiscrete η
    simp

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ Z✝ : Bicone J
f : BiconeHom J X✝ Y✝
g : BiconeHom J Y✝ Z✝
⊢ BiconeHom J X✝ Z✝

Tactic:
by
    rcases f with (_ | _ | _ | _ | f)
    · exact g
    · exact g
    · cases g
      apply BiconeHom.left
    · cases g
      apply BiconeHom.right
    · rcases g with (_ | _ | _ | _ | g)
      exact BiconeHom.diagram (f ≫ g)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
Y : C
f : Y ⟶ X
a✝ : J.Covers ⊤ f
⊢ ⊤.arrows f

Tactic:
trivial

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

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
Z : C
g : Z ⟶ Y
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows gg
⊢ (Sieve.pullback f S).arrows (gg ≫ g)

Tactic:
simpa using hgg

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
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
this : HasPullback b f
⊢ ∃ W_1 i e, R e ∧ i ≫ e = pullback.snd b f ≫ f

Tactic:
refine ⟨_, pullback.fst _ _, b, hb, pullback.condition⟩

Goal state after:
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
⊢ K.toGrothendieck ≤ sInf {J | K ≤ J.toCoverage}

Tactic:
apply le_sInf
    intro J hJ X S hS
    induction hS with
    | of X S hS => apply hJ; assumption
    | top => apply J.top_mem
    | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S : Sieve T
x✝ : ∃ R ∈ J.coverings T, R ≤ S.arrows
R : Presieve T
hR : R ∈ J.coverings T
hle : R ≤ S.arrows
⊢ J.toCoverage.Saturate T S

Tactic:
· refine Coverage.saturate_of_superset _ ?_ (.of _ _ hR)
    rwa [Sieve.generate_le_iff]

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

Goal state before:
pp: case h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ : (Sieve.pullback f R).arrows f₁
h₂ : (Sieve.pullback f R).arrows f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback g₁ (Sieve.pullback (f₁ ≫ f) S)).arrows gg
⊢ (Sieve.pullback (𝟙 Y₁) (Sieve.pullback (f₁ ≫ f) S)).arrows (gg ≫ g₁)

Tactic:
simpa using hgg

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

Goal state before:
pp: case mpr.transitive.refine_2.h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
hq : q.Compatible
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
⊢ (Sieve.pullback f R).arrows (gg ≫ g)

Tactic:
simpa using hgg

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

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
⊢ ((∀ (i j : ι),
        (ConcreteCategory.hom (P.map (F.map (pullback.fst (f i) (f j))).op)) (x i) =
          (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j)) →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i) ↔
    (∀ (i j : ι),
        (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
          (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)) →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom (P.map (F.map (f i)).op)) t = x i

Tactic:
rw [forall₂_congr]

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
⊢ ∀ (a b : ι),
    (ConcreteCategory.hom (P.map (F.map (pullback.fst (f a) (f b))).op)) (x a) =
        (ConcreteCategory.hom (P.map (F.map (pullback.snd (f a) (f b))).op)) (x b) ↔
      (ConcreteCategory.hom (P.map (pullback.fst (F.map (f a)) (F.map (f b))).op)) (x a) =
        (ConcreteCategory.hom (P.map (pullback.snd (F.map (f a)) (F.map (f b))).op)) (x b)
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.IsCocontinuous J K
⊢ G.IsContinuous K J

Tactic:
have := adj.isRightAdjoint

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.IsCocontinuous J K
this : G.IsRightAdjoint
⊢ G.IsContinuous K J
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: case hex
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
hF₁ : CompatiblePreserving K F
hF₂ : CoverPreserving J K F
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
x : FamilyOfElements (F.op ⋙ G.obj) S.arrows
hx : x.Compatible
⊢ ∃ x_1, x.IsAmalgamation x_1

Tactic:
have H := (isSheaf_iff_isSheaf_of_type _ _).1 G.2 _ (hF₂.cover_preserve hS)
      exact ⟨H.amalgamate (x.functorPushforward F) (hx.functorPushforward hF₁),
        fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
          (hF₁.apply_map _ hx hf)⟩

Goal state after:
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
J : GrothendieckTopology C
K : GrothendieckTopology D
U V : C
f : G.obj U ⟶ G.obj V
Y₁ Y₂ : C
i₁ : Y₁ ⟶ U
l : Y₁ ⟶ V
hl : G.map l = G.map i₁ ≫ f
i₂ : Y₂ ⟶ Y₁
⊢ G.map (i₂ ≫ l) = G.map (i₂ ≫ i₁) ≫ f

Tactic:
by simp [hl]

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
⊢ ∀ ⦃Z_1 : C⦄ (j : Z_1 ⟶ V₂),
    j ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = j ≫ iV₂Y₂ ≫ g₂ →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op))
          ((ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
            ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
              ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁))))) =
        (ConcreteCategory.hom (ℱ.obj.map (G.map j).op))
          ((ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
            ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
              ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)))))

Tactic:
intro V₃ iV₃ e₄

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
eq : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
W : C
i : G.obj W ⟶ X
V₁ : C
iVW : V₁ ⟶ W
iV₁Y₁ : V₁ ⟶ Y₁
e₁ : G.map iV₁Y₁ = G.map iVW ≫ i ≫ f₁
V₂ : C
iV₂V₁ : V₂ ⟶ V₁
iV₂Y₂ : V₂ ⟶ Y₂
e₂ : G.map iV₂Y₂ = G.map iV₂V₁ ≫ G.map iVW ≫ i ≫ f₂
V₃ : C
iV₃ : V₃ ⟶ V₂
e₄ : iV₃ ≫ iV₂V₁ ≫ iV₁Y₁ ≫ g₁ = iV₃ ≫ iV₂Y₂ ≫ g₂
⊢ (ConcreteCategory.hom (ℱ.obj.map (G.map iV₃).op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
        ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
          ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁))))) =
    (ConcreteCategory.hom (ℱ.obj.map (G.map iV₃).op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map iV₂V₁).op))
        ((ConcreteCategory.hom (ℱ.obj.map (G.map iVW).op))
          ((ConcreteCategory.hom (ℱ.obj.map i.op)) ((ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)))))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

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
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 : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
i : W₂ ⟶ W₁
hi : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op (G.map i ≫ g₁))).hom
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (G.map i ≫ g₁), ⋯⟩
⊢ G.map (l I.Y W₂ U I.f (G.map i ≫ g₁) ⋯) = G.map (I.f ≫ i) ≫ g₁

Tactic:
by simp [hl]

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

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
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 : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
this :
  (G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c ≫ (G.op.ranCounit.app Y.obj).app (op U) =
    c.π.app (StructuredArrow.mk (𝟙 (op (G.obj U))))
I : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve (𝟙 (G.obj U)), ⋯⟩
⊢ G.map (l I.Y U U I.f (𝟙 (G.obj U)) ⋯) = G.map I.f

Tactic:
by simp [hl]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
a b : E.I₁'
left : a.fst.1 = b.fst.1
right : a.fst.2 = b.fst.2
h : (congrIndexOneOfEq left right) a.snd = b.snd
⊢ a = b

Tactic:
obtain ⟨⟨i, j⟩, k⟩ := a

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
b : E.I₁'
i j : E.I₀
k : E.I₁ (i, j).1 (i, j).2
left : ⟨(i, j), k⟩.fst.1 = b.fst.1
right : ⟨(i, j), k⟩.fst.2 = b.fst.2
h : (congrIndexOneOfEq left right) ⟨(i, j), k⟩.snd = b.snd
⊢ ⟨(i, j), k⟩ = b
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ (homMk (x✝¹.π.app x✝) ⋯).left = x✝¹.π.app x✝

Tactic:
CostructuredArrow.homMk_left _ _

Goal state after:
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
K✝ : J ⥤ CostructuredArrow K B
c✝ : Cone K✝
hc : IsLimit c✝
x✝¹ : Cone (K✝ ⋙ proj K B)
x✝ : J
⊢ x✝¹.π.app x✝ = x✝¹.π.app x✝
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Presieve Y
h :
  { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      a✝ ≤
    { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      b✝
⊢ a✝ ≤ b✝

Tactic:
simpa using functorPullback_monotone h

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
T : Over X
a : T ⟶ Z
b : W ⟶ (Over.map f).obj T
ha : ((overEquiv Z).symm S).arrows a
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows (b ≫ (Over.map f).map a)

Tactic:
exact S.downward_closed ha _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y₁ Y₂ : Over X
S₁ : Sieve Y₁
f : Y₂ ⟶ Y₁
h₁ : S₁ ∈ ⇑(Sieve.overEquiv Y₁) ⁻¹' J Y₁.left
⊢ Sieve.pullback f S₁ ∈ ⇑(Sieve.overEquiv Y₂) ⁻¹' J Y₂.left

Tactic:
by
    rw [Set.mem_preimage, Sieve.overEquiv_pullback]
    exact J.pullback_stable _ h₁

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case mp
X : TopCat
U : Opens ↑X
x : ↑((toTopCat X).obj U)
⊢ (ConcreteCategory.hom U.inclusion') x ∈ ↑U
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
⊢ ↑((Pairwise.diagram U).op ⋙ F).sections

Tactic:
by
  refine ⟨objPairwiseOfFamily sf, ?_⟩
  let G := (Pairwise.diagram U).op ⋙ F
  rintro (i | ⟨i, j⟩) (i' | ⟨i', j'⟩) (_ | _ | _ | _)
  · exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.single i) _
  · rfl
  · exact (h i' i).symm
  · exact ConcreteCategory.congr_hom (G.map_id <| op <| Pairwise.pair i j) _

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 : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
⊢ IsIso (stalkPushforward C f F x)

Tactic:
by
  have := Functor.initial_of_adjunction (hf.adjunctionNhds x)
  convert!
    (Functor.Final.colimitIso (OpenNhds.map f x).op ((OpenNhds.inclusion x).op ⋙ F)).isIso_hom
  refine stalk_hom_ext _ fun U hU ↦ (stalkPushforward_germ _ f F _ x hU).trans ?_
  symm
  exact colimit.ι_pre ((OpenNhds.inclusion x).op ⋙ F) (OpenNhds.map f x).op _

Goal state after: