mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsStableUnderShift A
a : A
⊢ P.retractClosure ≤ P.retractClosure.shift a

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsStableUnderShift A
a : A
X : C
⊢ P.retractClosure X ≤ P.retractClosure.shift a X
Module: Mathlib.CategoryTheory.ObjectProperty.ClosureShift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
⊢ P.limitsClosure J ≤ (P.limitsClosure J).shift a

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddGroup A
inst✝² : HasShift C A
α : Type u_3
J : α → Type u_4
inst✝¹ : (i : α) → Category.{u_5, u_4} (J i)
inst✝ : P.IsStableUnderShift A
a : A
X : C
⊢ P.limitsClosure J X ≤ (P.limitsClosure J).shift a X
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).hom ≫ (isoMk fun i ↦ β_ (X i) ((Y ⊗ Z) i)).hom ≫ (α_ Y Z X).hom =
    (isoMk fun i ↦ β_ (X i) (Y i)).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (isoMk fun i ↦ β_ (X i) (Z i)).hom

Tactic:
ext i; apply hexagon_forward

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

Goal state after:
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)
j : β
k : α
⊢ biproduct.ι (fun a ↦ s (f a)) k ≫
      (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) ≫
        biproduct.π (fun b ↦ s (g b)) j =
    biproduct.ι (fun a ↦ s (f a)) k ≫ z ≫ biproduct.π (fun b ↦ s (g b)) j
Module: Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
⊢ ∀ {E X : C} (f : P ⟶ X) (e : E ⟶ X) [Epi e], ∃ f', f' ≫ e = f

Tactic:
intro X

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P Z : C
hZ : IsZero Z
h : (MorphismProperty.epimorphisms C).llp 0
X : C
⊢ ∀ {X_1 : C} (f : P ⟶ X_1) (e : X ⟶ X_1) [Epi e], ∃ f', f' ≫ e = f
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mp
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
⊢ finrank 𝕜 (X ⟶ Y) = 1 → Nonempty (X ≅ Y)

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
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1

Tactic:
· intro h
    rw [finrank_eq_one_iff'] at h
    obtain ⟨f, nz, -⟩ := h
    rw [← isIso_iff_nonzero] at nz
    exact ⟨asIso f⟩

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
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ x_1,
      if h : x_1.fst = j then
        if h_1 : ⋯ ▸ x_1.snd = x then if h_2 : x_1.fst = j' then if h_3 : ⋯ ▸ x_1.snd = y then eqToHom ⋯ else 0 else 0
        else 0
      else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y

Tactic:
rw [← Finset.univ_sigma_univ, Finset.sum_sigma]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j j' : Fin n
x : (f j).ι
y : (f j').ι
⊢ (∑ a,
      ∑ s,
        if h : ⟨a, s⟩.fst = j then
          if h_1 : ⋯ ▸ ⟨a, s⟩.snd = x then
            if h_2 : ⟨a, s⟩.fst = j' then if h_3 : ⋯ ▸ ⟨a, s⟩.snd = y then eqToHom ⋯ else 0 else 0
          else 0
        else 0) =
    (if h : j = j' then eqToHom ⋯ else 0) x y
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
⊢ b ≠ i →
    (∑ j_1,
        (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
          if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
hb

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : Fin n
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ (∑ j_1,
      (if h : i = b then if h' : h ▸ j = j_1 then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = b then if h' : h ▸ j' = j_1 then eqToHom ⋯ else 0 else 0) =
    0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
⊢ b ≠ j →
    ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
        if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
      0

Tactic:
hb

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i : Fin n
j : (f i).ι
i' : Fin n
j' : (f i').ι
b : (f i).ι
a✝ : b ∈ Finset.univ
hb : b ≠ j
⊢ ((if h : i = i then if h' : h ▸ j = b then eqToHom ⋯ else 0 else 0) ≫
      if h : i' = i then if h' : h ▸ j' = b then eqToHom ⋯ else 0 else 0) =
    0
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
⊢ b ≠ i → ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0

Tactic:
hb

Goal state after:
case h₀
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j b : M.ι
a✝ : b ∈ Finset.univ
hb : b ≠ i
⊢ ((fun j x ↦ if h : j = b then eqToHom ⋯ else 0) ≫ fun x k ↦ if h : b = k then eqToHom ⋯ else 0) i j = 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: case refine_1
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi

Tactic:
have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by
        dsimp [φ]
        rw [← hg, ← ConcreteCategory.comp_apply, c.w]
        rfl

Goal state after:
case refine_1
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
⊢ ∃ i xi, f = (ConcreteCategory.hom (((coyoneda.obj (Opposite.op J)).mapCocone c).ι.app i)) xi
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case e_a.e_a
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 : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
⊢ (fun j k ↦ L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom) =
    fun j k ↦
    (α.app (X✝.X j)).hom ≫ ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))

Tactic:
ext j k

Goal state after:
case e_a.e_a
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 : C ⥤ D
inst✝¹ : F.Additive
L : Mat_ C ⥤ D
inst✝ : L.Additive
α : embedding C ⋙ L ≅ F
X✝ Y✝ : Mat_ C
f : X✝ ⟶ Y✝
j : X✝.ι
k : Y✝.ι
⊢ L.map ((embedding C).map (f j k)) ≫ (α.app (Y✝.X k)).hom ≫ ((embeddingLiftIso F).symm.app (Y✝.X k)).hom =
    (α.app (X✝.X j)).hom ≫ ((embeddingLiftIso F).symm.app (X✝.X j)).hom ≫ (lift F).map ((embedding C).map (f j k))
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
D₂ : Diagram J κ
top' : J
h₂ : D₂.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₂.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.W =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.P =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' } =
    { toDiagram := D₂, top := top', isTerminal := h₂, uniq_terminal := h₂' }

Tactic:
obtain rfl : D₁ = D₂ := by aesop

Goal state after:
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D₁ : Diagram J κ
top : J
h₁ : D₁.IsTerminal top
h₁' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top
top' : J
h₂ : D₁.IsTerminal top'
h₂' : ∀ (j : J) (hj : D₁.IsTerminal j), j = top'
hW :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.W =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }.W
hP :
  { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' }.P =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }.P
⊢ { toDiagram := D₁, top := top, isTerminal := h₁, uniq_terminal := h₁' } =
    { toDiagram := D₁, top := top', isTerminal := h₂, uniq_terminal := h₂' }
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : HasCardinalLT (↑B) κ₂
b : X
⊢ b ∈ B → b ∈ φ₀ Y m B hB

Tactic:
hb

Goal state after:
case pos
κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
hB : HasCardinalLT (↑B) κ₂
b : X
hb : b ∈ B
⊢ b ∈ φ₀ Y m B hB
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: case isMin
κ₁ κ₂ : 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 : IsMin j
⊢ HasCardinalLT (↑(transfiniteIterate (φ Y m) j A)) κ₂

Tactic:
have := Cardinal.nonempty_ord_toType (c := κ₁) (IsRegular.ne_zero Fact.out)
    let := WellFoundedLT.toOrderBot κ₁.ord.ToType
    simpa [hj.eq_bot]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
⊢ W.isLocal (reflectionObj W Z κ)

Tactic:
intro X

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X : C
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), W f → Function.Bijective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.F.obj j
h : (fun g ↦ f ≫ g) (g₁ ≫ H.incl.app j) = (fun g ↦ f ≫ g) (g₂ ≫ H.incl.app j)
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j

Tactic:
dsimp at h

Goal state after:
case refine_1
C : Type u
inst✝⁷ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝⁶ : HasPushouts C
inst✝⁵ : ∀ (Z : C), HasCoproduct D₁.obj₁
inst✝⁴ : ∀ (Z : C), HasCoproduct D₁.obj₂
inst✝³ : ∀ (Z : C), HasMulticoequalizer (D₂.multispanIndex W Z)
κ : Cardinal.{w}
inst✝² : OrderBot κ.ord.ToType
inst✝¹ : HasIterationOfShape κ.ord.ToType C
inst✝ : Fact κ.IsRegular
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
H : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ) :=
  transfiniteCompositionOfShapeReflection W Z κ
X Y : C
f : X ⟶ Y
hf : W f
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j : κ.ord.ToType
g₁ g₂ : Y ⟶ H.F.obj j
h : f ≫ g₁ ≫ H.incl.app j = f ≫ g₂ ≫ H.incl.app j
⊢ g₁ ≫ H.incl.app j = g₂ ≫ H.incl.app j
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
      ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ X_1 f, (S = Presieve.ofArrows (fun x ↦ X_1) fun x ↦ f) ∧ EffectiveEpi f},
      ∃ T ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
      ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X_1 π, S = Presieve.ofArrows X_1 π ∧ IsIso (Sigma.desc π)},
      ∃ T ∈ {S | ∃ α, ∃ (x : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π)}, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W : C
⊢ ∀ (B : C) (α : Type) [Finite α] (X : α → C) (π : (a : α) → X a ⟶ B),
    EffectiveEpiFamily X π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X π)

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
W X : C
⊢ ∀ (α : Type) [Finite α] (X_1 : α → C) (π : (a : α) → X_1 a ⟶ X),
    EffectiveEpiFamily X_1 π → Presieve.IsSheafFor (yoneda.obj W) (Presieve.ofArrows X_1 π)
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
⊢ Presheaf.IsSheaf J R → Function.Bijective fun g ↦ whiskerRight f G ≫ g

Tactic:
hR

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
hR : Presheaf.IsSheaf J R
⊢ Function.Bijective fun g ↦ whiskerRight f G ≫ g
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W : C
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor (yoneda.obj W) R

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
⊢ ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor (yoneda.obj W) R
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R

Tactic:
intro X

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
⊢ ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝¹ : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
⊢ EqualizerCondition (F.op ⋙ P)

Tactic:
intro X

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝¹ : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X : E
⊢ ∀ ⦃B : E⦄ (π : X ⟶ B) [EffectiveEpi π], SingleEqualizerCondition (F.op ⋙ P) π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] (c : PullbackCone π π) (x : IsLimit c),
    Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
⊢ EqualizerCondition P

Tactic:
intro X

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
hP :
  ∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] (c : PullbackCone π π) (x : IsLimit c),
    Function.Bijective ⇑(ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯))
X : C
⊢ ∀ ⦃B : C⦄ (π : X ⟶ B) [EffectiveEpi π], SingleEqualizerCondition P π
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: 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 :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
⊢ (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b →
    ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b

Tactic:
hb

Goal state after:
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 :
  ∀ (b : (fun X ↦ X) ↑{x | (ConcreteCategory.hom (P.map c.fst.op)) x = (ConcreteCategory.hom (P.map c.snd.op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π c.fst c.snd ⋯)) a = b
hc : IsLimit c
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
⊢ ∃! x, (ConcreteCategory.hom (P.map π.op)) x = b