mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: case e'_2
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) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ (g₁ ≫ pullback.snd e k₁) ≫ pullback.fst (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.fst f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f)

pp: case e'_3
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) ⋯
g₁ : pullback f f ⟶ pullback e k₁ := pullback.lift (pullback.fst f f) d ⋯
g₂ : pullback f f ⟶ pullback k₂ e := pullback.lift d (pullback.snd f f) ⋯
h : IsPullback g₁ g₂ (pullback.snd e k₁) (pullback.fst k₂ e)
this : IsRegularEpi g₁
⊢ (g₁ ≫ pullback.snd e k₁) ≫ pullback.snd (coequalizer.desc f ⋯) (coequalizer.desc f ⋯) =
    pullback.snd f f ≫ coequalizer.π (pullback.fst f f) (pullback.snd f f)

Tactic:
all_goals cat_disch

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x.IsAmalgamation t) y → y = t

Tactic:
· exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Goal state after:
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
⊢ (∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) → S ∈ (coherentTopology C) X

Tactic:
intro ⟨α, _, Y, π, hπ⟩
  apply (coherentCoverage C).mem_toGrothendieck_sieves_of_superset (R := Presieve.ofArrows Y π)
  · exact fun _ _ h ↦ by cases h; exact hπ.2 _
  · exact ⟨_, inferInstance, Y, π, rfl, hπ.1⟩

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

Goal state before:
pp: case inr
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₁
X Y j : J
hj : D.P j
⊢ ∃ li lj, (D₄ D φ).W li ∧ (D₄ D φ).W lj ∧ φ ⟨j, hj⟩ ≫ lj = li

Tactic:
exact ⟨φ ⟨_, hj⟩, 𝟙 _, Or.inr ⟨_⟩, Or.inl (Or.inr ⟨⟨⟩⟩), by simp⟩

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 X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor (yoneda.obj W) R

Tactic:
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
W X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ 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 : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor F R

Tactic:
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk 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 : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular

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.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
⊢ ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f

Tactic:
obtain ⟨W, f', _, i, w⟩ := Preregular.exists_fac (F.map f) (F.map g)

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
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.EffectivelyEnough
inst✝² : Preregular D
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Z✝ ⟶ Y✝
x✝ : EffectiveEpi g
W : D
f' : W ⟶ F.obj X✝
w✝ : EffectiveEpi f'
i : W ⟶ F.obj Z✝
w : i ≫ F.map g = f' ≫ F.map f
⊢ ∃ W h, ∃ (_ : EffectiveEpi h), ∃ i, i ≫ g = h ≫ f
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), S.arrows (π a)
i✝ : α
⊢ S.arrows (π i✝)

Tactic:
exact h' _

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
h : ∃ Y π, EffectiveEpi π ∧ (Presheaf.imageSieve f y).arrows π
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y

Tactic:
obtain ⟨X', π, h, h'⟩ := h

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
X : C
y : ToType (G.obj (op X))
X' : C
π : X' ⟶ X
h : EffectiveEpi π
h' : (Presheaf.imageSieve f y).arrows π
⊢ ∃ X' φ,
    ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: case refine_1
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
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)

Tactic:
apply (mem_sieves_iff_hasEffectiveEpi (Sieve.functorPushforward _ S)).mpr

Goal state after:
case refine_1
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
x✝ : ∃ Y π, EffectiveEpi π ∧ S.arrows π
Y : C
π : Y ⟶ X
H₁ : EffectiveEpi π
H₂ : S.arrows π
⊢ ∃ Y π, EffectiveEpi π ∧ (Sieve.functorPushforward F S).arrows π
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
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
rw [isSheaf_coherent_iff_regular_and_extensive]
  exact and_congr (isSheaf_iff_preservesFiniteProducts _)
    (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows.cocone
x : FamilyOfElements (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
hx : x.Compatible
x_ext : FamilyOfElements (yoneda.obj W) (Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (ofArrows (fun x ↦ Y) fun x ↦ f)
t : (yoneda.obj W).obj (op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∀ (y : (yoneda.obj W).obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = t

Tactic:
· exact fun y hy ↦ t_uniq y <| Presieve.isAmalgamation_sieveExtend x y hy

Goal state after:
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 : (Over S')ᵒᵖ
e : (F.map ((Over.map q).obj (unop T)).hom.op.toLoc).toFunctor ≅
  (F.map q.op.toLoc ≫ F.map (unop T).hom.op.toLoc).toFunctor :=
  Cat.Hom.toNatIso (F.mapComp' q.op.toLoc (unop T).hom.op.toLoc ((Over.map q).obj (unop T)).hom.op.toLoc ⋯)
⊢ ((Over.map q).op ⋙ F.presheafHom M N).obj T ≃
    (F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N)).obj T

Tactic:
exact (Iso.homFromEquiv (e.app M)).trans (Iso.homToEquiv (e.app N))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    (pullback.snd (E.toPullback k)
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯))

Tactic:
← pullbackSymmetry_inv_comp_fst

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    ((pullbackSymmetry
          (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
            (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
            (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
          (E.toPullback k)).inv ≫
      pullback.fst
        (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
          (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
          (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
        (E.toPullback k))
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ 𝟙 (X i) ≫ f i = f i

pp: case hq
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p = f i

pp: case hf₁
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ (sq i i).p₁ ≫ f i = (sq i i).p

pp: case hf₂
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ (sq i i).p₂ ≫ f i = (sq i i).p

pp: case hgf₁
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p₁ = 𝟙 (X i)

pp: case hgf₂
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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
this : p ≫ (sq i i).p = f i
⊢ p ≫ (sq i i).p₂ = 𝟙 (X i)

Tactic:
all_goals cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.right
b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op

Tactic:
obtain ⟨φ, rfl, rfl⟩ := PullbackCone.IsLimit.lift' h₁.isLimit _ _ fac.symm

Goal state after:
case right.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
φ : W ⟶ sq.pullbackCone.pt
fac :
  (φ ≫ sq.pullbackCone.snd) ≫ WalkingPair.casesOn WalkingPair.right sq.f₂₄ sq.f₃₄ =
    (φ ≫ sq.pullbackCone.fst) ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.right s.fst s.snd ≫ F.obj.map (φ ≫ sq.pullbackCone.snd).op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map (φ ≫ sq.pullbackCone.fst).op
Module: Mathlib.CategoryTheory.Sites.Point.Monoidal

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
X✝¹ Y✝ P : Cᵒᵖ ⥤ A
f : X✝¹ ⟶ Y✝
X✝ : C
x✝ : Φ.fiber.obj X✝
⊢ Φ.toPresheafFiber X✝ x✝ (P ⊗ X✝¹) ≫
      Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x X✝¹) ⋯ ≫
        Φ.presheafFiber.obj P ◁ Φ.presheafFiber.map f =
    Φ.toPresheafFiber X✝ x✝ (P ⊗ X✝¹) ≫
      Φ.presheafFiber.map (P ◁ f) ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P ⊗ₘ Φ.toPresheafFiber X x Y✝) ⋯

Tactic:
simp [tensorHom_def, ← MonoidalCategory.whiskerLeft_comp, whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
R : Sieve U
hR : R ∈ ⊥ U
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
⊢ R = ⊤

Tactic:
by simpa using hR

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
⊢ K.toGrothendieck = J → K.Generates J

Tactic:
rintro rfl

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
⊢ K.Generates K.toGrothendieck
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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
⊢ Nonempty (F.toDescentData f).FullyFaithful ↔ Nonempty (F.toDescentData f').FullyFaithful

Tactic:
by
  obtain ⟨e, ⟨iso⟩⟩ := DescentData.exists_equivalence_of_sieve_eq F f f' h
  exact ⟨fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulFunctor).ofIso iso⟩,
    fun ⟨h⟩ ↦ ⟨(h.comp e.fullyFaithfulInverse).ofIso iso.symm.compInverseIso⟩⟩

Goal state after:
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
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    ∀ (g : Z ⟶ Y), ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a

Tactic:
⟨a, ha⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun X ↦ X) (F.obj (Opposite.op Y))
ha : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
⊢ ∀ (g : Z ⟶ Y), ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
⊢ ∀ T ∈ distinguishedTriangles, P.triangEnvelope T.obj₁ → P.triangEnvelope T.obj₃ → P.triangEnvelope T.obj₂

Tactic:
intro T

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
T : Triangle C
⊢ T ∈ distinguishedTriangles → P.triangEnvelope T.obj₁ → P.triangEnvelope T.obj₃ → P.triangEnvelope T.obj₂
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
⊢ Triangle.mk
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
              SpectralObject._proof_2 SpectralObject._proof_4).app
          (mk₂ f g)))
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
              SpectralObject._proof_4 SpectralObject._proof_4).app
          (mk₂ f g)))
      ({ app := fun D ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }.app (mk₂ f g)) ∈
    distinguishedTriangles

Tactic:
exact t.triangleω₁δ_distinguished a b c (leOfHom f) (leOfHom g) X

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
x y : EInt
f : x ⟶ y
⊢ WithBotTop.rec 0 t.truncLT (𝟭 C) x ⟶ WithBotTop.rec 0 t.truncLT (𝟭 C) y

Tactic:
induction x using WithBotTop.rec with

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = b → a = c

Tactic:
rintro rfl

Goal state after:
case refine_1
s : Set ℕ
a : ℕ
_ha : a ∈ s
c : ℕ
hc : c ∈ s
hb : a ∈ s
habc : a + c = a + a
⊢ a = c
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
c : ℕ
hc : c ∈ s
habc : a + c = b + b
⊢ a = c → a = b

Tactic:
rintro rfl

Goal state after:
case refine_2
s : Set ℕ
a : ℕ
_ha : a ∈ s
b : ℕ
hb : b ∈ s
hc : a ∈ s
habc : a + a = b + b
⊢ a = b