mathlib-initiative/mathlib-tactics huggingface dataset:
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
x y : 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
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂

Tactic:
obtain ⟨l₁, a, b, h₃⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := x₁) (xj := x₂)).1
          (hx₁.trans hx₂.symm)

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 : 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
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
⊢ ∃ l a b x₃ y₃,
    x₃ = (ConcreteCategory.hom (F.map a)) x₁ ∧
      x₃ = (ConcreteCategory.hom (F.map b)) x₂ ∧
        y₃ = (ConcreteCategory.hom (F.map a)) y₁ ∧ y₃ = (ConcreteCategory.hom (F.map b)) y₂
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
⊢ (succStruct W Z).prop ≤ W.isLocal.isLocal

Tactic:
by
    rintro Z₀ _ _ ⟨_⟩
    exact isLocal_isLocal_toSucc W Z₀

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝² : Fact κ₁.IsRegular
inst✝¹ : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
X : Type w
inst✝ : PartialOrder X
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂
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
hm : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : SetCardinalLT κ₁ ↑B) (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC
A : Set X
hA : HasCardinalLT (↑A) κ₂
⊢ IsCardinalFiltered (↑(⋃ j, transfiniteIterate (φ Y m) j A)) κ₁

Tactic:
suffices ∀ ⦃K : Type w⦄ (j : κ₁.ord.ToType) (f : K → (transfiniteIterate (φ Y m) j A : Set _))
      (hK : HasCardinalLT K κ₁),
      ∃ (x : (transfiniteIterate (φ Y m) (Order.succ j) A : Set _)),
          ∀ (k : K), (f k).val ≤ x.val by
    refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)
    rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
    have (k : K) : ∃ (j : κ₁.ord.ToType), (f k).val ∈ transfiniteIterate (φ Y m) j A := by
      simpa only [Set.mem_iUnion] using (f k).prop
    choose a ha using this
    obtain ⟨⟨z, hz⟩, hz'⟩ := this (IsCardinalFiltered.max a hK) (fun k ↦
      ⟨(f k).val, monotone_transfiniteIterate_φ Y hY' m A
          (leOfHom (IsCardinalFiltered.toMax a hK k)) (ha k)⟩) hK
    exact ⟨⟨z, Set.subset_iUnion _ _ hz⟩, hz'⟩
  intro K j f hK
  obtain ⟨⟨x, hx⟩, hx'⟩ := hφ₀ Y hY' m hm _
    (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA _) f hK
  refine ⟨⟨x, ?_⟩, hx'⟩
  have : NoMaxOrder κ₁.ord.ToType := noMaxOrder (IsRegular.aleph0_le Fact.out)
  rwa [transfiniteIterate_succ _ _ _ (not_isMax j),
    φ_eq _ _ _ (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA _)]

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

Goal state before:
pp: ⊢ (ObjectProperty.singleton PUnit.{u + 1}).IsStrongGenerator

Tactic:
rw [ObjectProperty.isStrongGenerator_iff]
  refine ⟨isSeparator_punit, fun _ _ i hi₁ hi₂ ↦ ?_⟩
  · rw [mono_iff_injective] at hi₁
    rw [isIso_iff_bijective]
    refine ⟨hi₁, fun y ↦ ?_⟩
    obtain ⟨f, hf⟩ := hi₂ PUnit ⟨.unit⟩ (↾fun _ ↦ y)
    exact ⟨f .unit, ConcreteCategory.congr_hom hf .unit⟩

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
⊢ F.IsRepresentedBy (R.homEquiv (𝟙 X))

Tactic:
rw [IsRepresentedBy.iff_isIso_uliftYonedaEquiv]
  convert!
    (RepresentableBy.equivUliftYonedaIso _ _ <|
        representableByUliftFunctorEquiv.{v}.symm R).isIso_hom
  ext
  simpa [uliftYonedaEquiv] using (homEquiv_eq _ _).symm

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 κ
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₁
⊢ ∀ ⦃j : J⦄, (D₄ D φ).P j → ∀ (l₁ l₂ : j ⟶ m₁), (D₄ D φ).W l₁ → (D₄ D φ).W l₂ → l₁ = l₂

Tactic:
rintro j (hj | ⟨⟨⟨⟩⟩⟩) l₁ l₂ hl₁ hl₂
        · obtain rfl := h₂ hj hl₁
          obtain rfl := h₂ hj hl₂
          rfl
        · rw [h₃ hl₁, h₃ hl₂]

Goal state after:
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
⊢ IsSheaf (extensiveCoverage C).toGrothendieck (yoneda.obj W)

Tactic:
isSheaf_coverage

Goal state after:
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
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : IsSheaf (extensiveCoverage C).toGrothendieck F
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F

Tactic:
isSheaf_coverage

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
⊢ ∀ {X : C} {S : Sieve X}, Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X) ↔ S ∈ (coherentTopology C) X

Tactic:
by simp [eq_induced F]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
⊢ ∀ {X : C} {S : Sieve X}, Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X) ↔ S ∈ (regularTopology C) X

Tactic:
by simp [eq_induced F]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        ((IsLimit.map (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone (isLimitOfPreserves F ht')
              (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom ≫
            F.map (π a).op) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
erw [IsLimit.map_π]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        (((Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone.π.app { as := a } ≫
            (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : Cᵒᵖ ⥤ D
inst✝¹ : Preregular C
inst✝ : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ (∀ ⦃X : C⦄,
      ∀ R ∈ (regularCoverage C).coverings X, Nonempty (IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op))) →
    EqualizerCondition F

Tactic:
· intro hF Y X f _
    exact (equalizerConditionMap_iff_nonempty_isLimit F f).2 (hF _ ⟨_, f, rfl, inferInstance⟩)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W : C
⊢ IsSheaf (regularCoverage C).toGrothendieck (yoneda.obj W)

Tactic:
isSheaf_coverage

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' gf₁.op.toLoc g'.op.toLoc g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map g'.op.toLoc).toFunctor.map ((F.mapComp' f₁.op.toLoc g.op.toLoc gf₁.op.toLoc ⋯).hom.toNatTrans.app M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map f₂.op.toLoc).toFunctor.obj M₂) ≫
            (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂

Tactic:
F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc _ _ _ _ _ _ _ rfl (by aesop)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
X₁ X₂ : C
M₁ : ↑(F.obj { as := op X₁ })
M₂ : ↑(F.obj { as := op X₂ })
Y : C
f₁ : Y ⟶ X₁
f₂ : Y ⟶ X₂
φ : (F.map f₁.op.toLoc).toFunctor.obj M₁ ⟶ (F.map f₂.op.toLoc).toFunctor.obj M₂
Y' : C
g : Y' ⟶ Y
gf₁ : Y' ⟶ X₁
gf₂ : Y' ⟶ X₂
Y'' : C
g' : Y'' ⟶ Y'
g'f₁ : Y'' ⟶ X₁
g'f₂ : Y'' ⟶ X₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
hg'f₁ : g' ≫ gf₁ = g'f₁
hg'f₂ : g' ≫ gf₂ = g'f₂
⊢ (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).hom.toNatTrans.app
          ((F.map f₁.op.toLoc).toFunctor.obj M₁) ≫
        (F.map g'.op.toLoc).toFunctor.map ((F.map g.op.toLoc).toFunctor.map φ) ≫
          (F.mapComp' g.op.toLoc g'.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) ⋯).inv.toNatTrans.app
              ((F.map f₂.op.toLoc).toFunctor.obj M₂) ≫
            (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂ =
    (F.mapComp' f₁.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₁.op.toLoc ⋯).hom.toNatTrans.app M₁ ≫
      (F.map (g.op.toLoc ≫ g'.op.toLoc)).toFunctor.map φ ≫
        (F.mapComp' f₂.op.toLoc (g.op.toLoc ≫ g'.op.toLoc) g'f₂.op.toLoc ⋯).inv.toNatTrans.app M₂
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst✝ : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra fun x ↦ f
i₂ : ι
⊢ ((𝟭 (F.DescentDataAsCoalgebra fun x ↦ f)).obj D).hom default i₂ ≫
      (F.map f.op.toLoc).l.toFunctor.map ((F.map f.op.toLoc).r.toFunctor.map (eqToIso ⋯).hom) =
    (eqToIso ⋯).hom ≫
      (({ obj := fun D ↦ { A := D.obj default, a := D.hom default default, counit := ⋯, coassoc := ⋯ },
                  map := fun {X_1 Y} φ ↦ { f := φ.hom default, h := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun A ↦ { obj := fun x ↦ A.A, hom := fun x x_1 ↦ A.a, counit := ⋯, coassoc := ⋯ },
                  map := fun {X_1 Y} φ ↦ { hom := fun i ↦ φ.f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
            D).hom
        default i₂

Tactic:
obtain rfl := Subsingleton.elim i₂ default

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type u_1
inst✝ : Unique ι
X S : C
f : X ⟶ S
D : F.DescentDataAsCoalgebra fun x ↦ f
⊢ ((𝟭 (F.DescentDataAsCoalgebra fun x ↦ f)).obj D).hom default default ≫
      (F.map f.op.toLoc).l.toFunctor.map ((F.map f.op.toLoc).r.toFunctor.map (eqToIso ⋯).hom) =
    (eqToIso ⋯).hom ≫
      (({ obj := fun D ↦ { A := D.obj default, a := D.hom default default, counit := ⋯, coassoc := ⋯ },
                  map := fun {X_1 Y} φ ↦ { f := φ.hom default, h := ⋯ }, map_id := ⋯, map_comp := ⋯ } ⋙
                { obj := fun A ↦ { obj := fun x ↦ A.A, hom := fun x x_1 ↦ A.a, counit := ⋯, coassoc := ⋯ },
                  map := fun {X_1 Y} φ ↦ { hom := fun i ↦ φ.f, comm := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj
            D).hom
        default default
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
have heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) =
      H'.isoPullback.inv ≫ (H i).isoPullback.hom := by
    rw [Iso.eq_inv_comp]
    cat_disch

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (pullback.fst fst (𝒰.f i)) (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯)
    (pullback.lift fst snd h) m
heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) = H'.isoPullback.inv ≫ ⋯.isoPullback.hom
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))
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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
M N : ↑(F.obj { as := op S })
⊢ Presieve.IsSheafFor (F.presheafHom M N)
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm (Sieve.generate (Presieve.ofArrows X f))).arrows

Tactic:
refine ((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf J M N)).isSheafFor _ ?_

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
M N : ↑(F.obj { as := op S })
⊢ Sieve.generate ((Sieve.overEquiv (Over.mk (𝟙 S))).symm (Sieve.generate (Presieve.ofArrows X f))).arrows ∈
    (J.over S) (Over.mk (𝟙 S))
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) (χ m) (truth C)

Tactic:
refine IsPullback.of_forall_isPullback_app fun X => ?_
  rw [Types.isPullback_iff]
  refine ⟨congr(($(comp_χ_eq m)).app X), ?_, ?_⟩
  · simpa using! (mono_iff_injective (m.app X)).mp (inferInstance)
  · simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]
    intro p hp
    simpa [eq_comm] using! congr($(hp).arrows (𝟙 _))

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
φ : P✝ ⟶ Z
⊢ φ ≫ (adj.homEquiv Z T.obj₃) h = 0 → φ = 0

Tactic:
hφ

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ φ = 0