mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih : ∀ (U : C) (g : U ⟶ X✝), R g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
K.mem_iff_exists_zeroHypercover

Goal state after:
case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
h : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih : ∀ (U : C) (g : U ⟶ X✝), R g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
hS : ∀ (i : E.I₀), S i ∈ K.coverings (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)

Tactic:
K.mem_iff_exists_zeroHypercover

Goal state after:
case refine_1.of_presieve
C : Type u
inst✝⁶ : Category.{v, u} C
K : Precoverage C
P : MorphismProperty C
inst✝⁵ : P.RespectsIso
inst✝⁴ : P.RespectsLeft K.morphismProperty
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
X Y : C
f✝ : X ⟶ Y
X✝ Y✝ : C
f : X✝ ⟶ Y✝
E : K.ZeroHypercover X✝
h : ∀ (U : C) (g : U ⟶ X✝), Presieve.ofArrows E.X E.f g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    Presieve.ofArrows E.X E.f g → ∃ R ∈ K.coverings U, ∀ (U_1 : C) (g_1 : U_1 ⟶ U), R g_1 → P (g_1 ≫ g ≫ f)
S : (i : E.I₀) → Presieve (E.X i)
h' : ∀ (i : E.I₀) (U : C) (g : U ⟶ E.X i), S i g → P (g ≫ E.f i ≫ f)
hS : ∀ (i : E.I₀), ∃ 𝒰, S i = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ R ∈ K.coverings X✝, ∀ (U : C) (g : U ⟶ X✝), R g → P (g ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.LocalEpi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Z : C
x✝ : P Z
⊢ Function.Injective fun g ↦ 𝟙 X ≫ g

Tactic:
by simpa using! Function.injective_id

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ →o Subobject X), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
G : ℕ ⥤ MonoOver X
⊢ IsFiltered.IsEventuallyConstant G

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m

Tactic:
· obtain ⟨n, hn⟩ := h (G ⋙ (Subobject.equivMonoOver _).inverse).toOrderHom
    refine ⟨n, fun m hm ↦ ?_⟩
    rw [MonoOver.isIso_iff_subobjectMk_eq]
    exact hn m (leOfHom hm)

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (F : ℕ ⥤ MonoOver X), IsFiltered.IsEventuallyConstant F
F : ℕ →o Subobject X
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → F n = F m
Module: Mathlib.CategoryTheory.ObjectProperty.Comma

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} D
F₁ : C₁ ⥤ D
F₂ : C₂ ⥤ D
P₁ : ObjectProperty C₁
P₂ : ObjectProperty C₂
inst✝² : ObjectProperty.EssentiallySmall.{w, v_1, u_1} P₁
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} P₂
inst✝ : LocallySmall.{w, v_3, u_3} D
⊢ ObjectProperty.EssentiallySmall.{w, max v_1 v_2, max (max u_1 u_2) v_3} (comma F₁ F₂ P₁ P₂)

Tactic:
obtain ⟨Q₁, _, h₁, h₁'⟩ := EssentiallySmall.exists_small_le.{w} P₁
  obtain ⟨Q₂, _, h₂, h₂'⟩ := EssentiallySmall.exists_small_le.{w} P₂
  refine ⟨comma F₁ F₂ Q₁ Q₂, inferInstance, fun f hf ↦ ?_⟩
  simp only [comma_iff] at hf
  obtain ⟨X₁, hX₁, ⟨e₁⟩⟩ := h₁' _ hf.1
  obtain ⟨X₂, hX₂, ⟨e₂⟩⟩ := h₂' _ hf.2
  exact ⟨Comma.mk _ _ (F₁.map e₁.inv ≫ f.hom ≫ F₂.map e₂.hom), by tauto,
    ⟨Comma.isoMk e₁ e₂⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
n : ℕ
α : F ⟶ G
⊢ (n • T.map α.f) ≫ G.a = F.a ≫ (n • α.f)

Tactic:
nsmul_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
n : ℕ
α : F ⟶ G
⊢ n • T.map α.f ≫ G.a = F.a ≫ (n • α.f)
Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ (n • F.map α.f) ≫ A₂.str = n • A₁.str ≫ α.f

Tactic:
nsmul_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ n • F.map α.f ≫ A₂.str = n • A₁.str ≫ α.f
Module: Mathlib.CategoryTheory.Pi.Monoidal

Goal state before:
pp: I : Type w₁
C : I → Type u₁
inst✝² : (i : I) → Category.{v₁, u₁} (C i)
inst✝¹ : (i : I) → MonoidalCategory (C i)
inst✝ : (i : I) → BraidedCategory (C i)
X Y Z : (i : I) → C i
⊢ (α_ X Y Z).inv ≫ (isoMk fun i ↦ β_ ((X ⊗ Y) i) (Z i)).hom ≫ (α_ Z X Y).inv =
    X ◁ (isoMk fun i ↦ β_ (Y i) (Z i)).hom ≫ (α_ X Z Y).inv ≫ (isoMk fun i ↦ β_ (X i) (Z i)).hom ▷ Y

Tactic:
ext i; apply hexagon_reverse

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ (fun z ↦ biproduct.matrix fun j k ↦ if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0)
      ((fun z i j k ↦ eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯) z) =
    z

Tactic:
ext j k
    simp only [biproduct.matrix_π, biproduct.ι_desc]
    split_ifs with h
    · simp
      rfl
    · symm
      apply o.eq_zero h

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
⊢ finrank 𝕜 (X ⟶ Y) = 1

Tactic:
have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y

Goal state after:
case mpr
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
f : X ≅ Y
le_one : finrank 𝕜 (X ⟶ Y) ≤ 1
⊢ finrank 𝕜 (X ⟶ Y) = 1
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
⊢ ∀ (a b c_1 : CoconePt hc),
    (∃ j x' y',
        ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = b), x' ≤ y') →
      (∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = b) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = c_1),
            x' ≤ y') →
        ∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = c_1), x' ≤ y'

Tactic:
rintro x y z ⟨j, x₁, y₁, hx₁, hy₁, hxy⟩ ⟨k, y₂, z₁, hy₂, hz₁, hyz⟩

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y z : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
hxy : x₁ ≤ y₁
k : J
y₂ z₁ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hz₁ : (ConcreteCategory.hom (c.ι.app k)) z₁ = z
hyz : y₂ ≤ z₁
⊢ ∃ j x' y', ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = x) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = z), x' ≤ y'
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : f ≫ g₁ ≫ p.ι.app j₁ = f ≫ g₂ ≫ p.ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv : f ≫ g₁ ≫ p.diag.map u = f ≫ g₂ ≫ p.diag.map v
⊢ g₁ ≫ p.ι.app j₁ = g₂ ≫ p.ι.app j₂

Tactic:
← p.w u,

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : f ≫ g₁ ≫ p.ι.app j₁ = f ≫ g₂ ≫ p.ι.app j₂
j₃ : J
u : j₁ ⟶ j₃
v : j₂ ⟶ j₃
huv : f ≫ g₁ ≫ p.diag.map u = f ≫ g₂ ≫ p.diag.map v
⊢ g₁ ≫ p.diag.map u ≫ p.ι.app j₃ = g₂ ≫ p.ι.app j₂
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
x : X
⊢ x ∈ A ↔ x ∈ Set.univ

Tactic:
have := congr_hom hf x

Goal state after:
X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
x✝ : IsCardinalPresentable X κ
this✝ :
  ∀ (J : Type u) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J (coyoneda.obj (op X))
A : Set X
hA : HasCardinalLT (↑A) κ
f : (HasCardinalLT.Set.functor X κ ⋙ coyoneda.obj (op X)).obj ⟨A, hA⟩
hf : (hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f = 𝟙 X
x : X
this :
  (hom ((hom (((coyoneda.obj (op X)).mapCocone (HasCardinalLT.Set.cocone X κ)).ι.app ⟨A, hA⟩)) f)) x = (hom (𝟙 X)) x
⊢ x ∈ A ↔ x ∈ Set.univ
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_4.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
X Y : J
i : ι
j : J
hj : (D i).P j
⊢ ∃ li lj, (D₂ D hι u).W li ∧ (D₂ D hι u).W lj ∧ ((D ⟨i, ⟨j, hj⟩⟩.fst).isTerminal.lift ⋯ ≫ u ⟨i, ⟨j, hj⟩⟩.fst) ≫ lj = li

Tactic:
· refine ⟨φ ⟨i, j, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp [φ]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ Sieve.generate (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S

Tactic:
rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
Y : C
π : Y ⟶ X
h : EffectiveEpi π ∧ S.arrows π
⊢ (Presieve.ofArrows (fun x ↦ Y) fun x ↦ π) ≤ S.arrows
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

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
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
⊢ IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Tactic:
constructor
  · intro h
    rw [IsSheaf] at h
    refine ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ?_⟩⟩⟩
    constructor
    apply coyonedaJointlyReflectsLimits
    intro ⟨E⟩
    specialize h E
    rw [Presieve.isSheaf_iff_preservesFiniteProducts] at h
    exact isLimitOfPreserves (F.comp (coyoneda.obj ⟨E⟩)) hc
  · intro _ E
    rw [Presieve.isSheaf_iff_preservesFiniteProducts]
    exact ⟨inferInstance⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ S ∈ (extensiveTopology C) X →
    ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X

Tactic:
· intro h
    induction h with
    | of X S hS =>
      obtain ⟨α, _, Y, π, h, h'⟩ := hS
      refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩
      · have : IsIso (Sigma.desc (Cofan.mk X π).inj) := by simpa using! h'
        exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩
      · obtain ⟨rfl, _⟩ := h
        exact ⟨Y a, 𝟙 Y a, π a, Presieve.ofArrows.mk a, by simp⟩
    | top X =>
      refine ⟨Unit, inferInstance, fun _ => X, fun _ => (𝟙 X), ⟨?_⟩, by simp⟩
      have : IsIso (Sigma.desc (Cofan.mk X fun (_ : Unit) ↦ 𝟙 X).inj) := by
        have : IsIso (coproductUniqueIso (fun () => X)).hom := inferInstance
        exact this
      exact Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X _)
    | transitive X R S _ _ a b =>
      obtain ⟨α, w, Y₁, π, h, h'⟩ := a
      choose β _ Y_n π_n H using fun a => b (h' a)
      exact ⟨(Σ a, β a), inferInstance, fun ⟨a,b⟩ => Y_n a b, fun ⟨a, b⟩ => (π_n a b) ≫ (π a),
        ⟨Limits.Cofan.isColimitTrans _ h.some _ (fun a ↦ (H a).1.some)⟩,
        fun c => (H c.fst).2 c.snd⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (extensiveTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
⊢ (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })))
      ((ConcreteCategory.hom (f.app (op (∐ Z)))) ((ConcreteCategory.hom i'.hom) x)) =
    (ConcreteCategory.hom ((G.mapCone (Cocone.op (Cofan.mk (∐ Z) (Sigma.ι Z)))).π.app (op { as := a })))
      ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)

Tactic:
simp only [Functor.comp_obj, Functor.op_obj, Discrete.functor_obj_eq_as, Functor.mapCone_pt,
      Cocone.op_pt, Cofan.mk_pt, Functor.const_obj_obj, Functor.mapCone_π_app, Cocone.op_π,
      NatTrans.op_app, Cofan.mk_ι_app, Functor.mapIso_symm, Iso.trans_hom, Iso.symm_hom,
      Functor.mapIso_inv, comp_apply, ← f.naturality_apply (Sigma.ι Z a).op, i']

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preregular C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
U✝ : C
y : ToType (G.obj (op U✝))
α : Type
w✝ : Finite α
Z : α → C
π : (a : α) → Z a ⟶ U✝
h : EffectiveEpiFamily Z π
h' : ∀ (a : α), (Presheaf.imageSieve f y).arrows (π a)
x : (a : α) → F.obj (op (Z a)) := fun a ↦ Exists.choose ⋯
i' : ((a : α) → F.obj (op (Z a))) ≅ F.obj (op (∐ Z)) :=
  (Types.productIso fun a ↦ F.obj (op (Z a))).symm ≪≫
    (PreservesProduct.iso F fun a ↦ op (Z a)).symm ≪≫ F.mapIso (opCoproductIsoProduct Z).symm
this : PreservesLimitsOfShape (Discrete α)ᵒᵖ G
a : α
⊢ (ConcreteCategory.hom (f.app (op (Z a))))
      ((ConcreteCategory.hom (F.map (Sigma.ι Z a).op))
        ((ConcreteCategory.hom (F.map (opCoproductIsoProduct Z).inv))
          ((ConcreteCategory.hom (PreservesProduct.iso F fun a ↦ op (Z a)).inv)
            ((ConcreteCategory.hom (Types.productIso fun a ↦ F.obj (op (Z a))).inv) x)))) =
    (ConcreteCategory.hom (G.map (Sigma.ι Z a).op)) ((ConcreteCategory.hom (G.map (Sigma.desc π).op)) y)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj j)
hom_self : ∀ (i : ι), pullHom' hom (f i) (𝟙 (X i)) (𝟙 (X i)) ⋯ ⋯ = 𝟙 ((F.map (𝟙 (X i)).op.toLoc).toFunctor.obj (obj i))
Y : C
q : Y ⟶ S
i : ι
g : Y ⟶ X i
hg : g ≫ f i = q
⊢ pullHom' hom q g g hg hg = 𝟙 ((F.map g.op.toLoc).toFunctor.obj (obj i))

Tactic:
by
  simp [← pullHom_pullHom' hom g (f i) q (𝟙 (X i)) (𝟙 (X i)) g g hg, hom_self, pullHom]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (φ.hom i₁) ≫ D₂.hom i₁ i₂) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
φ.comm,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (φ.hom i₂)) ≫
        (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
⊢ ∃ φ,
    ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))

Tactic:
by
  let c : Cone ((Presieve.diagram (Sieve.pullback g S).arrows).op ⋙ G) :=
    { pt := F.obj (op Y)
      π :=
        { app := fun ⟨Z, hZ⟩ => F.map Z.hom.op ≫ (x _ hZ).app (op (Over.mk (𝟙 _)))
          naturality := by
            rintro ⟨Z₁, hZ₁⟩ ⟨Z₂, hZ₂⟩ ⟨⟨f : Z₂ ⟶ Z₁⟩⟩
            dsimp
            rw [id_comp, assoc]
            have H := hx f.left (𝟙 _) hZ₁ hZ₂ (by simp)
            simp only [op_id, Functor.map_id, id_apply] at H
            let φ : Over.mk f.left ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk f.left
            have H' := (x (Z₁.hom ≫ g) hZ₁).naturality φ.op
            dsimp at H H' ⊢
            erw [← H, ← H', presheafHom_map_app_op_mk_id, ← F.map_comp_assoc,
              ← op_comp, Over.w f] } }
  use (hG g).lift c
  intro Z p hp
  exact ((hG g).fac c ⟨Over.mk p, hp⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
X✝ Y✝ : F.DescentData f
φ : X✝ ⟶ Y✝
⊢ (pullFunctor F w).map φ ≫ (isoMk (fun j ↦ Y✝.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯).hom =
    (isoMk (fun j ↦ X✝.iso (p' j ≫ f (α j)) (p' j) (p'' j) ⋯ ⋯) ⋯).hom ≫ (pullFunctor F w').map φ

Tactic:
by
      ext j
      exact φ.comm _ _ _ rfl (by cat_disch)

Goal state after: