mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : F.Additive
M N : Mat_ C
f : M ⟶ N
i : N.ι
j : M.ι
⊢ ((fun x k ↦ if h : j = k then eqToHom ⋯ else 0) ≫ f ≫ fun j x ↦ if h : j = i then eqToHom ⋯ else 0) PUnit.unit
      PUnit.unit =
    (embedding C).map (f j i) PUnit.unit PUnit.unit

Tactic:
simp [comp_apply, dite_comp, comp_dite]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
⊢ (fun i j ↦ MulOpposite.unop (𝟙 X i j)) = 𝟙 (FintypeCat.of X.ι)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X : Mat_ (SingleObj Rᵐᵒᵖ)
i✝ j✝ : (FintypeCat.of X.ι).obj
⊢ MulOpposite.unop (𝟙 X i✝ j✝) = 𝟙 (FintypeCat.of X.ι) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (fun i j ↦ MulOpposite.unop ((f ≫ g) i j)) = (fun i j ↦ MulOpposite.unop (f i j)) ≫ fun i j ↦ MulOpposite.unop (g i j)

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ Z✝ : Mat_ (SingleObj Rᵐᵒᵖ)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
i✝ : (FintypeCat.of X✝.ι).obj
j✝ : (FintypeCat.of Z✝.ι).obj
⊢ MulOpposite.unop ((f ≫ g) i✝ j✝) = ((fun i j ↦ MulOpposite.unop (f i j)) ≫ fun i j ↦ MulOpposite.unop (g i j)) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
R : Type
inst✝ : Ring R
X✝ Y✝ : Mat_ (SingleObj Rᵐᵒᵖ)
a₁✝ a₂✝ : X✝ ⟶ Y✝
w : (equivalenceSingleObjInverse R).map a₁✝ = (equivalenceSingleObjInverse R).map a₂✝
i✝ : X✝.ι
j✝ : Y✝.ι
⊢ a₁✝ i✝ j✝ = a₂✝ i✝ j✝
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
f : Arrow J
hf : f ∈ (MorphismProperty.ofHoms fun x ↦ 𝟙 j).toSet
⊢ (fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩) PUnit.unit = ⟨f, hf⟩

Tactic:
ext

Goal state after:
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
j : J
f : Arrow J
hf : f ∈ (MorphismProperty.ofHoms fun x ↦ 𝟙 j).toSet
⊢ ↑((fun x ↦ ⟨Arrow.mk (𝟙 j), ⋯⟩) PUnit.unit) = ↑⟨f, hf⟩
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
⊢ HasCardinalLT (↑(φ₀ Y m (transfiniteIterate (φ Y m) j A) hj')) κ₂

Tactic:
refine hasCardinalLT_iUnion _ (hY _ _)
      (fun ⟨C, hC⟩ ↦ hasCardinalLT_union hκ₂.aleph0_le ?_
        (hasCardinalLT_of_finite _ _ hκ₂.aleph0_le))

Goal state after:
case succ
κ₁ κ₂ : Cardinal.{w}
inst✝¹ : Fact κ₁.IsRegular
inst✝ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
hA : HasCardinalLT (↑A) κ₂
j : κ₁.ord.ToType
hj : ¬IsMax j
hj' : HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂
hκ₂ : κ₂.IsRegular
x✝ : ↑(Y (transfiniteIterate (φ Y m) j A) hj')
C : SetCardinalLT κ₁ ↑(transfiniteIterate (φ Y m) j A)
hC : C ∈ Y (transfiniteIterate (φ Y m) j A) hj'
⊢ HasCardinalLT (↑(Subtype.val '' ↑↑⟨C, hC⟩)) κ₂
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
X : Type u
κ : Cardinal.{u}
hκ : Cardinal.aleph0 ≤ κ
this : IsFiltered (HasCardinalLT.Set X κ)
x : (cocone X κ).pt
⊢ ∃ i xi, x = (hom ((cocone X κ).ι.app i)) xi

Tactic:
exact ⟨⟨{x}, hasCardinalLT_of_finite _ _ hκ⟩, ⟨x, by simp⟩, rfl⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := fun a ↦ pullback f (π a)
π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst f (π a)
⊢ Presieve.ofArrows Z' π' ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}

Tactic:
constructor

Goal state after:
case refine_1.h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := ⋯
π' : (a : α) → Z' a ⟶ Y := ⋯
⊢ ∃ (x : Finite ?refine_1.w), ∃ X π, Presieve.ofArrows Z' π' = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)

case refine_1.w
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X Y : C
f : Y ⟶ X
S : Presieve X
α : Type
hα : Finite α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
h_iso : IsIso (Sigma.desc π)
Z' : α → C := ⋯
π' : (a : α) → Z' a ⟶ Y := ⋯
⊢ Type
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
d : pullback f f ⟶ pullback m m := pullback.lift (pullback.fst f f ≫ e) (pullback.snd f f ≫ e) ⋯
⊢ pullback.fst f f ≫ e = d ≫ k₁

Tactic:
simp [d, k₁]

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
R : F.RepresentableBy X
⊢ uliftYonedaEquiv.symm { down := R.homEquiv (𝟙 X) } =
    ((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X) (representableByUliftFunctorEquiv.symm R)).hom

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
R : F.RepresentableBy X
x✝¹ : Cᵒᵖ
x✝ : (uliftYoneda.{w, v, u}.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := R.homEquiv (𝟙 X) }).app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom
          (((equivUliftYonedaIso (F ⋙ uliftFunctor.{v, w}) X) (representableByUliftFunctorEquiv.symm R)).hom.app
            x✝¹)).toFun
      x✝
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
A B : C
f : A ⟶ B
A' : Subobject A
B' : Subobject B
⊢ IsPullback (frobeniusMorphism f A' B' ≫ ((«exists» f).obj A' ⊓ B').ofLE B' ⋯)
    ((A' ⊓ (Subobject.pullback f).obj B').ofLE A' ⋯) B'.arrow
    ((imageFactorisation f A').F.e ≫ ((«exists» f).obj A').arrow)

Tactic:
simpa [frobeniusMorphism, IsPullback.lift_fst, ← imageFactorisation_F_m,
    (isPullback f B').paste_horiz_iff] using
    (inf_isPullback A' ((Subobject.pullback f).obj B')).flip

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ (isoOfIso
          { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
            inv_hom_id := ⋯ }
          ⋯ ⋯).hom ≫
      M.whiskerLeft
        (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom =
    whiskerRight
      (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
          ⋯).hom
      N

Tactic:
ext

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ ((isoOfIso
            { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
              inv_hom_id := ⋯ }
            ⋯ ⋯).hom ≫
        M.whiskerLeft
          (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom).hom =
    (whiskerRight
        (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
            ⋯).hom
        N).hom
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P ↔
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ Presieve.IsSheaf (coherentTopology C) P →
    ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
P : Cᵒᵖ ⥤ Type w
⊢ (∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
      EffectiveEpiFamily X π → Presieve.IsSheafFor P (Presieve.ofArrows X π)) →
    Presieve.IsSheaf (coherentTopology C) P
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ (coherentCoverage C).Saturate X (Sieve.generate (Presieve.ofArrows Y π))

pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      (coherentCoverage C).Saturate Y_1
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows
              (fun x ↦
                match x with
                | ⟨a, b⟩ => Y_n a b)
              fun x ↦
              match x with
              | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
· apply Coverage.Saturate.of
    use α, inferInstance, Y, π

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ X⦄,
    (Sieve.generate (Presieve.ofArrows Y π)).arrows f →
      (coherentCoverage C).Saturate Y_1
        (Sieve.pullback f
          (Sieve.generate
            (Presieve.ofArrows
              (fun x ↦
                match x with
                | ⟨a, b⟩ => Y_n a b)
              fun x ↦
              match x with
              | ⟨a, b⟩ => π_n a b ≫ π a)))
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ (coherentTopology C) X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ S ∈ (coherentTopology C) X → ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
⊢ ∀ ⦃i j : J⦄ (f : i ⟶ j), (D₄ D φ).W f → ∃ li lj, (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ f ≫ lj = li

Tactic:
by
      rintro j k f ((hf | ⟨⟨⟩⟩) | ⟨⟨j, hj⟩⟩)
      · exact ⟨φ ⟨_, D.src hf⟩, φ ⟨_, D.tgt hf⟩,
          Or.inr ⟨_⟩, Or.inr ⟨_⟩, D.isTerminal.comm_assoc _ hf _⟩
      · exact ⟨𝟙 _, 𝟙 _, Or.inl (Or.inr ⟨⟨⟩⟩), Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩
      · exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
this : IsFiltered κ.ord.ToType
⊢ ∃ α x, ∃ (_ : IsCardinalFiltered α κ), ∃ F, F.Final

Tactic:
obtain ⟨α, _, _, F, _⟩ :=
    exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
      ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
        have : NoMaxOrder κ.ord.ToType :=
          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
        exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)

Goal state after:
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
this : IsFiltered κ.ord.ToType
α : Type w
w✝¹ : PartialOrder α
w✝ : IsCardinalFiltered α κ
F : α ⥤ J × κ.ord.ToType
h✝ : F.Final
⊢ ∃ α x, ∃ (_ : IsCardinalFiltered α κ), ∃ F, F.Final
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
⊢ S ∈ (regularTopology C) X ↔ ∃ Y π, EffectiveEpi π ∧ S.arrows π

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ S ∈ (regularTopology C) X → ∃ Y π, EffectiveEpi π ∧ S.arrows π

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
S : Sieve X
⊢ (∃ Y π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
⊢ Sigma.desc π' ≫ g = Sigma.desc π₂

Tactic:
ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
b✝ : α
⊢ Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π' ≫ g =
    Sigma.ι (fun b ↦ Limits.pullback g' (Sigma.ι X₁ b)) b✝ ≫ Sigma.desc π₂
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
this : Sigma.desc π' ≫ g = Sigma.desc π₂
⊢ EffectiveEpiFamily X₂ π₂

Tactic:
← effectiveEpi_desc_iff_effectiveEpiFamily,

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : Preregular C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
x✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
h : EffectiveEpiFamily X₁ π₁
Y : C
g : Y ⟶ B₂
w✝ : EffectiveEpi g
g' : Y ⟶ ∐ X₁
hg : g' ≫ Sigma.desc π₁ = g ≫ f
X₂ : α → C := fun a ↦ Limits.pullback g' (Sigma.ι X₁ a)
π₂ : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ B₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
π' : (a : α) → Limits.pullback g' (Sigma.ι X₁ a) ⟶ Y := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
x✝ : IsIso (Sigma.desc fun x ↦ pullback.fst g' (Sigma.ι X₁ x))
this : Sigma.desc π' ≫ g = Sigma.desc π₂
⊢ EffectiveEpi (Sigma.desc π₂)
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

Goal state after:
case mp
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

case mpr
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
⊢ PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

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
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor

Goal state after:
case mp
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
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mpr
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
⊢ PreservesFiniteProducts F → IsSheaf (extensiveTopology C) F

Tactic:
intro _ E

Goal state after:
case mpr
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
a✝ : PreservesFiniteProducts F
E : D
⊢ Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
⊢ (fun a ↦ (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = ⟨b, hb⟩) a

Tactic:
ext

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hP :
  ∀ (y : P.obj (op X)),
    (ConcreteCategory.hom (P.map c.fst.op)) y = (ConcreteCategory.hom (P.map c.snd.op)) y →
      ∃! x, (ConcreteCategory.hom (P.map π.op)) x = y
hc : IsLimit c
b : P.obj (op X)
hb : b ∈ {x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}
a : P.obj (op B)
ha₁ : (ConcreteCategory.hom (P.map π.op)) a = b
ha₂ : ∀ (y : P.obj (op B)), (fun x ↦ (ConcreteCategory.hom (P.map π.op)) x = b) y → y = a
⊢ ↑((ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a) = ↑⟨b, hb⟩
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: 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)

Tactic:
constructor

Goal state after:
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)

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