mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Cofork (Sigma.map' f fun x ↦ 𝟙 R) 0
m : (sigmaConstCokernelCofork R f).pt ⟶ s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
⊢ m =
    Sigma.desc fun x ↦
      match x with
      | ⟨b, property⟩ => Sigma.ι (fun x ↦ R) b ≫ s.π

Tactic:
dsimp
      ext ⟨b, hb⟩
      rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]

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

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
cases f <;> cases g <;> cases h

Goal state after:
case left_id.left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left_id =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left_id

case left_id.left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ BiconeHom.left j✝ =
    BiconeHom.left_id ≫ BiconeHom.left_id ≫ BiconeHom.left j✝

case left_id.left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ BiconeHom.diagram f✝

case right_id.right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right_id =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right_id

case right_id.right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ BiconeHom.right j✝ =
    BiconeHom.right_id ≫ BiconeHom.right_id ≫ BiconeHom.right j✝

case right_id.right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ BiconeHom.diagram f✝

case left.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.left j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝

case right.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.right j✝ ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝

case diagram.diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝² : J
f✝² : j✝ ⟶ k✝²
k✝¹ : J
f✝¹ : k✝² ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
⊢ (BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹) ≫ BiconeHom.diagram f✝ =
    BiconeHom.diagram f✝² ≫ BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝
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✝ : ReflectsFiniteProducts F
x✝ : ℕ
⊢ ReflectsColimitsOfShape (Discrete (Fin x✝)) F.op

Tactic:
by
    apply +allowSynthFailures reflectsColimitsOfShape_op
    exact reflectsLimitsOfShape_of_equiv (Discrete.opposite _).symm _

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤

Tactic:
· intro hS
    rw [_root_.eq_top_iff]
    intro Y f _
    apply J₁.pullback_stable _ hS

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ hc.lift (c.extend (Hom.right g₂)) = Hom.right g₂

Tactic:
symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := ⋯
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := ⋯
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) := ⋯
c₀ : Cone (biconeMk J c₁ c₂) := ⋯
g₁ : c₀.pt ⟶ c₁.pt := ⋯
g₂ : c₀.pt ⟶ c₂.pt := ⋯
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₂ = hc.lift (c.extend (Hom.right g₂))
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 = ⊤}
⊢ (c X) ((c X) R) = ⊤

Tactic:
eq_top_iff,

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 = ⊤}
⊢ ⊤ ≤ (c X) ((c X) R)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  φ.app T.left ≫ (F.leftKanExtensionUnit G₂).app T.left =
    (F.leftKanExtensionUnit G₁).app T.left ≫
      ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
            (φ ≫ F.leftKanExtensionUnit G₂)).app
        (F.obj T.left)
h₁ :
  ∀ (G : C ⥤ E),
    (F.leftKanExtensionUnit G).app T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      colimit.ι (CostructuredArrow.proj F X ⋙ G) T
⊢ (F.leftKanExtensionUnit G₁).app T.left ≫
      (F.leftKanExtension G₁).map T.hom ≫
        ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
                (φ ≫ F.leftKanExtensionUnit G₂)).app
            X ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    colimit.ι (CostructuredArrow.proj F X ⋙ G₁) T ≫ colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)

Tactic:
NatTrans.naturality_assoc,

Goal state after:
C D : Type u₁
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
E : Type u₂
inst✝¹ : Category.{u₁, u₂} E
F : C ⥤ D
X : D
inst✝ : ∀ (X : D), HasColimitsOfShape (CostructuredArrow F X) E
G₁ G₂ : C ⥤ E
φ : G₁ ⟶ G₂
T : CostructuredArrow F X
h₂ :
  φ.app T.left ≫ (F.leftKanExtensionUnit G₂).app T.left =
    (F.leftKanExtensionUnit G₁).app T.left ≫
      ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
            (φ ≫ F.leftKanExtensionUnit G₂)).app
        (F.obj T.left)
h₁ :
  ∀ (G : C ⥤ E),
    (F.leftKanExtensionUnit G).app T.left ≫
        (F.leftKanExtension G).map T.hom ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G))).hom =
      colimit.ι (CostructuredArrow.proj F X ⋙ G) T
⊢ (F.leftKanExtensionUnit G₁).app T.left ≫
      ((F.leftKanExtension G₁).descOfIsLeftKanExtension (F.leftKanExtensionUnit G₁) (F.leftKanExtension G₂)
              (φ ≫ F.leftKanExtensionUnit G₂)).app
          (F.obj T.left) ≫
        (F.leftKanExtension G₂).map T.hom ≫
          (IsColimit.coconePointUniqueUpToIso (F.isPointwiseLeftKanExtensionLeftKanExtensionUnit G₂ X)
              (colimit.isColimit (CostructuredArrow.proj F X ⋙ G₂))).hom =
    colimit.ι (CostructuredArrow.proj F X ⋙ G₁) T ≫ colimMap ((CostructuredArrow.proj F X).whiskerLeft φ)
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 : S ∈ {S | (c X) S = ⊤}
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
⊢ R ∈ {S | (c X) S = ⊤}

Tactic:
rw [Set.mem_ofPred_eq] at hS
    rw [Set.mem_ofPred_eq, ← (c X).idempotent, eq_top_iff, ← hS]
    apply (c X).monotone fun Y f hf => _
    intro Y f hf
    rw [Sieve.mem_iff_pullback_eq_top, ← hc]
    apply hR hf

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i✝ : E.I₀
i : ↑R.uncurry
⊢ (↑i).fst ≅ YR (↑i).snd ⋯

Tactic:
symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S := ⋯
F : PreZeroHypercover S := ⋯
i✝ : E.I₀
i : ↑R.uncurry
⊢ YR (↑i).snd ⋯ ≅ (↑i).fst
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
S T : C
inst✝¹ : J.IsStableUnderComposition
inst✝ : J.HasIsos
X Y : C
f : X ⟶ Y
hf : Presieve.singleton f ∈ J.coverings Y
E : J.ZeroHypercover X
⊢ (PreZeroHypercover.pushforward f E.toPreZeroHypercover).presieve₀ ∈ J.coverings Y

Tactic:
rw [PreZeroHypercover.mem_iff_of_iso (E.pushforwardIsoBind _)]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : Precoverage C
S T : C
inst✝¹ : J.IsStableUnderComposition
inst✝ : J.HasIsos
X Y : C
f : X ⟶ Y
hf : Presieve.singleton f ∈ J.coverings Y
E : J.ZeroHypercover X
⊢ ((PreZeroHypercover.singleton f).bind fun x ↦ E.toPreZeroHypercover).presieve₀ ∈ J.coverings Y
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.transitive
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✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ J Y
⊢ S ∈ J X

Tactic:
exact J.transitive H1 _ H2

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

Goal state before:
pp: case a.transitive
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✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ J Y
⊢ S ∈ J X

Tactic:
exact J.transitive H1 _ H2

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

Goal state before:
pp: case refine_1.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
S : Presieve X
hS : S ∈ J.toCoverage.coverings X
⊢ ∃ R ∈ J.coverings X, R ≤ (Sieve.generate S).arrows

Tactic:
use S, hS, Sieve.le_generate S

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
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
by
  refine le_antisymm ?_ ?_ <;>
  · intro Z g ⟨k, u, hu₁, hu₂⟩
    cat_disch

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
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.coverByImage G B ∈ K B

Tactic:
refine K.superset_covering ?_ h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (ConcreteCategory.hom (appHom (homOver α (unop Y)) (unop U))) (f.unop ≫ x) =
    f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x

Tactic:
symm

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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x =
    (ConcreteCategory.hom (appHom (homOver α (unop Y)) (unop U))) (f.unop ≫ x)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (ConcreteCategory.hom (((sheafYonedaHom α).app (op (G.obj (unop X)))).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝

Tactic:
symm

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
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝ =
    (ConcreteCategory.hom (((sheafYonedaHom α).app (op (G.obj (unop X)))).app U)) x✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (ConcreteCategory.hom (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app U)) x✝ =
    (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝

Tactic:
symm

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
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝ =
    (ConcreteCategory.hom (((sheafYonedaHom (G.op.whiskerLeft α)).app X).app U)) x✝
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case mp
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
X : C
Y : Over X
T : ↑(J ((Over.forget X).obj Y))
Z : C
w✝¹ : Over X
w✝ : w✝¹ ⟶ Y
g' : Z ⟶ (Over.forget X).obj w✝¹
hg : (Sieve.functorPullback (Over.forget X) ↑T).arrows w✝
⊢ (↑T).arrows (g' ≫ (Over.forget X).map w✝)

Tactic:
exact T.val.downward_closed hg g'

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

Goal state before:
pp: 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
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT✝ : T ∈ K.toGrothendieck (F.obj U)
hT : ∃ R ∈ K.coverings (F.obj U), R ≤ T.arrows
⊢ ∃ R ∈ K.coverings (F.obj U), R ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT✝⟩)).arrows

Tactic:
obtain ⟨R, hR, hle⟩ := hT

Goal state after:
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
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT : T ∈ K.toGrothendieck (F.obj U)
R : Presieve (F.obj U)
hR : R ∈ K.coverings (F.obj U)
hle : R ≤ T.arrows
⊢ ∃ R ∈ K.coverings (F.obj U), R ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT⟩)).arrows
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case 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
hT : ∃ R ∈ K.coverings (F.obj X), R ≤ (Sieve.functorPushforward F T).arrows
⊢ T ∈ (comap F K).toGrothendieck X

Tactic:
obtain ⟨R, hR, hle⟩ := hT

Goal state after:
case 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
⊢ T ∈ (comap F K).toGrothendieck X
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ limit.cone (F ⋙ colim) ≅ colim.mapCone c

Tactic:
symm

Goal state after:
J✝ : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J✝
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J✝
F✝ : J✝ × K ⥤ Type v
inst✝ : IsFiltered K
J : Type v₂
𝒥✝ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ K ⥤ Type v
c : Cone F
hc : IsLimit c
⊢ colim.mapCone c ≅ limit.cone (F ⋙ colim)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ (J.overMapPullbackComp A (𝟙 X) f).inv ≫
      (J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom ≫ (J.overMapPullback A f).rightUnitor.hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
by
  ext
  dsimp
  simp only [overMapPullbackComp_inv_app_hom_app, overMapPullbackId_hom_app_hom_app,
    Functor.sheafPushforwardContinuous_obj_obj_map, Quiver.Hom.unop_op,
    comp_id, ← Functor.map_comp, ← op_comp]
  congr
  cat_disch

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

Goal state before:
pp: X : TopCat
U : Opens ↑X
⊢ Set.range ⇑(ConcreteCategory.hom U.inclusion') = ↑U

Tactic:
by
  ext x
  constructor
  · rintro ⟨x, rfl⟩
    exact x.2
  · intro h
    exact ⟨⟨x, h⟩, rfl⟩

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

Goal state before:
pp: α : Type u
J : Type w
inst✝³ : SmallCategory J
inst✝² : FinCategory J
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
this : ∀ (x y : α), HasColimit (pair x y)
⊢ HasBinaryCoproducts α

Tactic:
apply hasBinaryCoproducts_of_hasColimit_pair

Goal state after: