mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : 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 := ⋯
φ : ↑J.obj → ↑(F.obj m).obj := ⋯
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
x : ↑J.obj
⊢ (PartOrdEmb.Hom.hom f.hom) x = (ConcreteCategory.hom (c.ι.app (j x))) (g x)

pp: κ : 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 := ⋯
φ : ↑J.obj → ↑(F.obj m).obj := ⋯
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
x : ↑J.obj
⊢ (ConcreteCategory.hom (c.ι.app (j x))) (g x) =
    (PartOrdEmb.Hom.hom
        (ObjectProperty.homMk (PartOrdEmb.ofHom { toFun := φ, inj' := ⋯, map_rel_iff' := ⋯ }) ≫ c.ι.app m).hom)
      x

Tactic:
· exact (hg x).symm

Goal state after:
κ : 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 := ⋯
φ : ↑J.obj → ↑(F.obj m).obj := ⋯
hφ : ∀ (x : ↑J.obj), (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.ι.app m)) (φ x)
x : ↑J.obj
⊢ (ConcreteCategory.hom (c.ι.app (j x))) (g x) =
    (PartOrdEmb.Hom.hom
        (ObjectProperty.homMk (PartOrdEmb.ofHom { toFun := φ, inj' := ⋯, map_rel_iff' := ⋯ }) ≫ c.ι.app m).hom)
      x
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 : C ⥤ D
inst✝ : F.Additive
X : Mat_ C
i j : X.ι
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i

Tactic:
by_cases h : j = i

Goal state after:
case pos
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
X : Mat_ C
i j : X.ι
h : j = i
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i

case neg
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
X : Mat_ C
i j : X.ι
h : ¬j = i
⊢ biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫
      (biproduct.matrix fun i j ↦ F.map (𝟙 X i j)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i =
    biproduct.ι (fun i ↦ F.obj (X.X i)) j ≫ 𝟙 (⨁ fun i ↦ F.obj (X.X i)) ≫ biproduct.π (fun i ↦ F.obj (X.X i)) i
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : 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)
j : A
f g : J ⟶ F.obj j
h : f ≫ c.ι.app j = g ≫ c.ι.app j
k : ↑J.obj → A
a : (x : ↑J.obj) → j ⟶ k x
hk :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (F.map (a x))) (f.hom.hom' x) = (ConcreteCategory.hom (F.map (a x))) (g.hom.hom' x)
⊢ ∃ l c b, ∀ (x : ↑J.obj), a x ≫ b x = c

Tactic:
by
        let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ :=
          a x ≫ IsCardinalFiltered.toMax k hJ x
        exact ⟨IsCardinalFiltered.coeq φ hJ,
          IsCardinalFiltered.toCoeq φ hJ,
          fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ,
          fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩

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)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m₀ : ι → J
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩)

Tactic:
rintro ⟨⟨i₁, i₂, j⟩, _, _⟩ ⟨⟨i₁', i₂', j'⟩, _, _⟩ h

Goal state after:
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
t₀ : (i : ι) → (D i).top ⟶ m₀ i
hm₀ : ∀ (i : ι), IsEmpty (m₀ i ⟶ (D i).top)
m₁ : J := max m₀ hι
t₁ : (i : ι) → m₀ i ⟶ m₁ := fun i ↦ toMax m₀ hι i
u : (i : ι) → (D i).top ⟶ m₁ := fun i ↦ t₀ i ≫ t₁ i
S : Type (max 0 w) := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }
shape : MultispanShape :=
  { L := { x // (D x.1).P x.2.2 ∧ (D x.2.1).P x.2.2 }, R := PUnit.{w + 1}, fst := fun x ↦ PUnit.unit,
    snd := fun x ↦ PUnit.unit }
index : MultispanIndex shape J :=
  { left := fun x ↦ (↑x).2.2, right := fun x ↦ m₁, fst := fun x ↦ (D (↑x).1).isTerminal.lift ⋯ ≫ u (↑x).1,
    snd := fun x ↦ (D (↑x).2.1).isTerminal.lift ⋯ ≫ u (↑x).2.1 }
hκ : Cardinal.aleph0 ≤ κ
this : HasCardinalLT (ι × (i : ι) × Subtype (D i).P) κ
i₁ i₂ : ι
j : J
left✝¹ : (D (i₁, i₂, j).1).P (i₁, i₂, j).2.2
right✝¹ : (D (i₁, i₂, j).2.1).P (i₁, i₂, j).2.2
i₁' i₂' : ι
j' : J
left✝ : (D (i₁', i₂', j').1).P (i₁', i₂', j').2.2
right✝ : (D (i₁', i₂', j').2.1).P (i₁', i₂', j').2.2
h :
  (fun x ↦
        match x with
        | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
      ⟨(i₁, i₂, j), ⋯⟩ =
    (fun x ↦
        match x with
        | ⟨(i₁, i₂, j), ⋯⟩ => (i₁, ⟨i₂, ⟨j, h₂⟩⟩))
      ⟨(i₁', i₂', j'), ⋯⟩
⊢ ⟨(i₁, i₂, j), ⋯⟩ = ⟨(i₁', i₂', j'), ⋯⟩
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
j : J
hj : (D i).P j
hi : Arrow.mk f = Arrow.mk ((D ⟨i, ⟨j, hj⟩⟩.fst).isTerminal.lift ⋯ ≫ u ⟨i, ⟨j, hj⟩⟩.fst)
⊢ f = 𝟙 m

Tactic:
obtain rfl : m = j := congr_arg Arrow.leftFunc.obj hi

Goal state after:
case inr
J : Type w
inst✝¹ : SmallCategory J
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hD : ∀ {i : ι}, ¬(D i).P m
f : m ⟶ m
i : ι
hj : (D i).P m
hi : Arrow.mk f = Arrow.mk ((D ⟨i, ⟨m, hj⟩⟩.fst).isTerminal.lift ⋯ ≫ u ⟨i, ⟨m, hj⟩⟩.fst)
⊢ f = 𝟙 m
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
a : ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), R.arrows (π a)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)

Tactic:
obtain ⟨α, w, Y₁, π, ⟨h₁, h₂⟩⟩ := a

Goal state after:
case mp.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S✝ : Sieve X
Y : C
R S : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y R
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, R.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S)
b :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    R.arrows f → ∃ α, ∃ (_ : Finite α), ∃ Y_2 π, EffectiveEpiFamily Y_2 π ∧ ∀ (a : α), (Sieve.pullback f S).arrows (π a)
α : Type
w : Finite α
Y₁ : α → C
π : (a : α) → Y₁ a ⟶ Y
h₁ : EffectiveEpiFamily Y₁ π
h₂ : ∀ (a : α), R.arrows (π a)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y_1 π, EffectiveEpiFamily Y_1 π ∧ ∀ (a : α), S.arrows (π a)
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 π, EffectiveEpi π ∧ S.arrows π) → S ∈ (regularTopology C) X

Tactic:
by
  rintro ⟨Y, π, h⟩
  have h_le : Sieve.generate (Presieve.ofArrows (fun () ↦ Y) (fun _ ↦ π)) ≤ S := by
    rw [Sieve.generate_le_iff (Presieve.ofArrows _ _) S]
    apply Presieve.le_of_factorsThru_sieve (Presieve.ofArrows _ _) S _
    intro W g f
    refine ⟨W, 𝟙 W, ?_⟩
    cases f
    exact ⟨π, ⟨h.2, Category.id_comp π⟩⟩
  apply Coverage.saturate_of_superset (regularCoverage C) h_le
  exact Coverage.Saturate.of X _ ⟨Y, π, rfl, h.1⟩

Goal state after:
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₁ π₁
⊢ ∃ β, ∃ (_ : Finite β), ∃ X₂ π₂, EffectiveEpiFamily X₂ π₂ ∧ ∃ i ι, ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f

Tactic:
by
    refine ⟨α, inferInstance, ?_⟩
    obtain ⟨Y, g, _, g', hg⟩ := Preregular.exists_fac f (Sigma.desc π₁)
    let X₂ := fun a ↦ pullback g' (Sigma.ι X₁ a)
    let π₂ := fun a ↦ pullback.fst g' (Sigma.ι X₁ a) ≫ g
    let π' := fun a ↦ pullback.fst g' (Sigma.ι X₁ a)
    have _ := FinitaryPreExtensive.isIso_sigmaDesc_fst (fun a ↦ Sigma.ι X₁ a) g' inferInstance
    refine ⟨X₂, π₂, ?_, ?_⟩
    · have : (Sigma.desc π' ≫ g) = Sigma.desc π₂ := by ext; simp [π₂, π']
      rw [← effectiveEpi_desc_iff_effectiveEpiFamily, ← this]
      infer_instance
    · refine ⟨id, fun b ↦ pullback.snd _ _, fun b ↦ ?_⟩
      simp only [X₂, π₂, id_eq, Category.assoc, ← hg]
      rw [← Category.assoc, pullback.condition]
      simp

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

Goal state before:
pp: case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ Nonempty (IsColimit (Cofan.mk X π))

Tactic:
exact ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : IsSheaf (coherentTopology C) (F ⋙ s)
⊢ IsSheaf (coherentTopology C) F

Tactic:
by
  rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢
  exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).obj.obj (op X))
hh : EffectiveEpi (limit.π (preimageDiagram hF X y) (op 0))
⊢ (ConcreteCategory.hom ((c.π.app (op 0)).hom.app (op (limit (preimageDiagram hF X y)))))
      ((coherentTopology C).yonedaEquiv (hc.lift (cone hF X y))) =
    (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op (limit.π (preimageDiagram hF X y) (op 0))))) y

Tactic:
simp only [← (coherentTopology C).yonedaEquiv_comp, cone,
    IsLimit.fac, NatTrans.ofOpSequence_app, (coherentTopology C).yonedaEquiv_comp,
    (coherentTopology C).yonedaEquiv_yoneda_map]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
h : ∀ (G : ℕᵒᵖ ⥤ C), (∀ (n : ℕ), EffectiveEpi (G.map (homOfLE ⋯).op)) → EffectiveEpi (limit.π G (op 0))
X : C
y : ToType ((F.obj (op 0)).obj.obj (op X))
hh : EffectiveEpi (limit.π (preimageDiagram hF X y) (op 0))
⊢ (ConcreteCategory.hom
        (((coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x 0)).hom.app
          (op (limit (preimageDiagram hF X y)))))
      (limit.π (preimageDiagram hF X y) (op 0)) =
    (ConcreteCategory.hom ((F.obj (op 0)).obj.map (op (limit.π (preimageDiagram hF X y) (op 0))))) y
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
T₁ T₂ : Over S'
f : unop (op T₂) ⟶ unop (op T₁)
g : ((Over.map q).op ⋙ F.presheafHom M N).obj (op T₁)
⊢ (q.op.toLoc ≫ T₁.hom.op.toLoc) ≫ (Over.Hom.left f).op.toLoc = q.op.toLoc ≫ T₂.hom.op.toLoc

Tactic:
simp only [← Quiver.Hom.comp_toLoc, ← op_comp, Over.w_assoc]

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)
obj 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)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom (pullHom' hom q f₁ f₂ hf₁ hf₂) g gf₁ gf₂ ⋯ ⋯ = pullHom' hom q' gf₁ gf₂ ⋯ ⋯

Tactic:
by
  let p := (sq i₁ i₂).isPullback.lift f₁ f₂ (by cat_disch)
  rw [pullHom'_eq_pullHom _ _ _ _ p, pullHom'_eq_pullHom _ _ _ _ (g ≫ p)]
  dsimp [pullHom]
  simp only [Functor.map_comp, Category.assoc]
  rw [F.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app_assoc
    _ _ _ _ _ _ (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_fst])
    rfl (by cat_disch),
    F.mapComp'_inv_whiskerRight_mapComp'₀₂₃_inv_app _ _ _ _ _ _
      (by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]) rfl (by cat_disch)]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₂ : (sieve f f' i).arrows f₂
h₁ : (sieve f f' i).arrows (Over.homMk Y₁.hom ⋯)
fac : g₁ ≫ Over.homMk Y₁.hom ⋯ = g₂ ≫ f₂
⊢ Over.Hom.left f₂ = Over.Hom.left (Over.homMk Y₂.hom ⋯)

Tactic:
simpa using Over.w f₂

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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
        (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
      pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯

Tactic:
pullHom'_eq_pullHom _ _ _ _ (sq₃ i₁ i₂ i₃).p₁₂,

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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
        ⋯ ≫
      pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom' (fun i₁ i₂ ↦ D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom (pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯) g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc (gf₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc (gf₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))

Tactic:
pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂)

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
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
D : F.DescentData f
Y' Y : C
g : Y' ⟶ Y
q : Y ⟶ S'
q' : Y' ⟶ S'
hq : g ≫ q = q'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
gf₁ : Y' ⟶ X' j₁
gf₂ : Y' ⟶ X' j₂
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
⊢ pullHom
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂)))
      g gf₁ gf₂ ⋯ ⋯ =
    (F.mapComp' (p' j₁).op.toLoc gf₁.op.toLoc (gf₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q' ≫ p) (gf₁ ≫ p' j₁) (gf₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.mapComp' (p' j₂).op.toLoc gf₂.op.toLoc (gf₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ j₃ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
f₃ : Y ⟶ X' j₃
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hf₃ : f₃ ≫ f' j₃ = q
⊢ pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫ pullFunctorObjHom w D (f₂ ≫ f' j₂) f₂ f₃ ⋯ ⋯ =
    pullFunctorObjHom w D (f₁ ≫ f' j₁) f₁ f₃ ⋯ ⋯

Tactic:
rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃)]

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
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
D : F.DescentData f
Y : C
q : Y ⟶ S'
j₁ j₂ j₃ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
f₃ : Y ⟶ X' j₃
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
hf₃ : f₃ ≫ f' j₃ = q
⊢ ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
        D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))) ≫
      (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc (f₂ ≫ p' j₂).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₂)) ≫
        D.hom (q ≫ p) (f₂ ≫ p' j₂) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
          (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₃)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc (f₁ ≫ p' j₁).op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)) ≫
      D.hom (q ≫ p) (f₁ ≫ p' j₁) (f₃ ≫ p' j₃) ⋯ ⋯ ≫
        (F.mapComp' (p' j₃).op.toLoc f₃.op.toLoc (f₃ ≫ p' j₃).op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₃))