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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ Presieve.singleton h ∈ {S | ∃ X f, (S = Presieve.ofArrows (fun x ↦ X) fun x ↦ f) ∧ EffectiveEpi f}

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ (Presieve.singleton h).FactorsThruAlong S f

Tactic:
· exact ⟨W, h, by {rw [Presieve.ofArrows_pUnit h]}, inferInstance⟩

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
X Y : C
f : Y ⟶ X
S : Presieve X
Z : C
π : Z ⟶ X
hπ : S = Presieve.ofArrows (fun x ↦ Z) fun x ↦ π
h_epi : EffectiveEpi π
W : C
h : W ⟶ Y
w✝ : EffectiveEpi h
i : W ⟶ Z
this : i ≫ π = h ≫ f
⊢ (Presieve.singleton h).FactorsThruAlong S f
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
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf : (D₂ D hι u).W f
⊢ f = φ ⟨i, ⟨j, hj⟩⟩

Tactic:
simp only [D₂_W] at hf

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
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
i : ι
j : J
hj : (D i).P j
f : j ⟶ m
hf :
  (((⨆ i, (D i).W) ⊔ MorphismProperty.ofHoms fun x ↦ 𝟙 m) ⊔
      MorphismProperty.ofHoms fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst)
    f
⊢ f = φ ⟨i, ⟨j, hj⟩⟩
Module: Mathlib.CategoryTheory.RegularCategory.Basic

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

Tactic:
by
    rw [frobeniusMorphism, ← inf_comp_left, ← Category.assoc,
      (inf_isPullback ((«exists» f).obj A') B').flip.lift_snd]
    simp [← imageFactorisation_F_m]

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

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ≤ S.arrows

pp: case hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).coverings X

Tactic:
· exact fun _ _ h ↦ by cases h; exact hπ.2 _

Goal state after:
case hR
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
X : C
S : Sieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
hπ : EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
⊢ Presieve.ofArrows Y π ∈ (coherentCoverage C).coverings X
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Tactic:
apply coyonedaJointlyReflectsLimits

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ (X : Dᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : Preadditive A
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) colim

Tactic:
by
    apply +allowSynthFailures preservesProductsOfShape_of_preservesBiproductsOfShape
    apply preservesBiproductsOfShape_of_preservesCoproductsOfShape

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₃)
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)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) φ f₁ f₂ ⋯ ⋯ ≫
      pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₂ f₃ ⋯ ⋯ =
    pullHom' hom q f₁ f₃ ⋯ ⋯

Tactic:
← pullHom_pullHom' hom φ (sq₃ i₁ i₂ i₃).p _ (sq₃ i₁ i₂ i₃).p₁ (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₃)
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)
hom_comp :
  ∀ (i₁ i₂ i₃ : ι),
    pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
        pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
      pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
Y : C
q : Y ⟶ S
i₁ i₂ i₃ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
f₃ : Y ⟶ X i₃
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hf₃ : f₃ ≫ f i₃ = q
φ : Y ⟶ (sq₃ i₁ i₂ i₃).pullback
left✝¹ : φ ≫ (sq₃ i₁ i₂ i₃).p₁ = f₁
left✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₂ = f₂
right✝ : φ ≫ (sq₃ i₁ i₂ i₃).p₃ = f₃
⊢ pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯) φ f₁ f₂ ⋯ ⋯ ≫
      pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₂ f₃ ⋯ ⋯ =
    pullHom (pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯) φ f₁ f₃ ⋯ ⋯
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)
⊢ Sieve.pullback
      (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.sieve₁' i.fst j.fst) ≤
    (cylinder f g).sieve₁' i j

Tactic:
· rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]
    rintro Z u ⟨W, v, ⟨k⟩⟩
    simp_rw [← pullbackSymmetry_inv_comp_fst]
    apply (((cylinder f g).sieve₁' i j)).downward_closed
    rw [sieve₁']
    convert! Sieve.ofArrows_mk _ _ (ULift.up k)
    simp [toPullback_cylinder f g ⟨k⟩]

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

Goal state before:
pp: 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✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
⊢ pullback.snd
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (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) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      E.p₁ k.down =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)

Tactic:
have : E.p₁ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.fst _ _ := by simp
    nth_rw 2 [this]
    rw [← pullback.condition_assoc]
    simp

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

Tactic:
reassoc_of% h₁

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 : ι
p : X i ⟶ (sq i i).pullback
h₁ : p ≫ (sq i i).p₁ = 𝟙 (X i)
h₂ : p ≫ (sq i i).p₂ = 𝟙 (X i)
⊢ f i = f i
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))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄ (h₁ : (sieve f f' i).arrows f₁)
    (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
f₁

Goal state after:
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))
⊢ ∀ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄ (h₁ : (sieve f f' i).arrows f₁) (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
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))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
⊢ g₁ ≫ f₁ = g₂ ≫ f₂ →
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
fac

Goal state after:
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))
f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))
h₁ : (sieve f f' i).arrows f₁
h₂ : (sieve f f' i).arrows f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f✝ : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f✝ (𝒰.f i))
i j : 𝒰.I₀
f : pullback (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f✝ (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ pullback.fst (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f i)) ≫ pullback.fst f✝ (𝒰.f i) =
    pullback.snd (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f j)) ≫ pullback.fst f✝ (𝒰.f j)

Tactic:
rw [← cancel_epi ((pullbackRightPullbackFstIso _ _ _).hom ≫ f)]

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
X Y : C
f✝ : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (pullback.snd f✝ (𝒰.f i))
i j : 𝒰.I₀
f : pullback (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) ⟶ pullback (𝒰.f i) (𝒰.f j) :=
  pullback.map (pullback.fst f✝ (𝒰.f i) ≫ f✝) (𝒰.f j) (𝒰.f i) (𝒰.f j) (pullback.snd f✝ (𝒰.f i)) (𝟙 (𝒰.X j)) (𝟙 Y) ⋯ ⋯
⊢ ((pullbackRightPullbackFstIso f✝ (𝒰.f j) (pullback.fst f✝ (𝒰.f i))).hom ≫ f) ≫
      pullback.fst (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f i)) ≫ pullback.fst f✝ (𝒰.f i) =
    ((pullbackRightPullbackFstIso f✝ (𝒰.f j) (pullback.fst f✝ (𝒰.f i))).hom ≫ f) ≫
      pullback.snd (𝒰.f i) (𝒰.f j) ≫ inv (pullback.snd f✝ (𝒰.f j)) ≫ pullback.fst f✝ (𝒰.f j)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 ↦ g ≫ g_1
⊢ Function.Bijective fun g_1 ↦ F ◁ g ≫ g_1

Tactic:
← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
    ((ihom.adjunction _).homEquiv _ _).bijective

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : MonoidalCategory A
inst✝² : MonoidalClosed A
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective fun g_1 ↦ g ≫ g_1
⊢ Function.Bijective (curry ∘ fun g_1 ↦ F ◁ g ≫ g_1)
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
β : ι' → ι
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₂ : ι'
⊢ ∀ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' j₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom

Tactic:
f₁

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
β : ι' → ι
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₂ : ι'
f₁ : Y ⟶ X' j₁
⊢ ∀ (f₂ : Y ⟶ X' j₂) (hf₁ : f₁ ≫ f' j₁ = q) (hf₂ : f₂ ≫ f' j₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' j₁ ≫ f (α j₁)) (p' j₁) (p'' j₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' j₂ ≫ f (α j₂)) (p' j₂) (p'' j₂) ⋯ ⋯).hom
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
i₁ i₂ : ι
⊢ ∀ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom

Tactic:
f₁

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
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
⊢ ∀ (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom
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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
⊢ ∀ (f₁ : Y ⟶ X'' k₁) (f₂ : Y ⟶ X'' k₂) (hf₁ : f₁ ≫ f'' k₁ = s) (hf₂ : f₂ ≫ f'' k₂ = s),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β k₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom s f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom s f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β k₂)))).hom

Tactic:
f₁

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
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : q ≫ p = r
hr' : ∀ (k : ι''), q' k ≫ p' (β k) = r' k
D : F.DescentData f
Y : C
s : Y ⟶ S''
k₁ k₂ : ι''
f₁ : Y ⟶ X'' k₁
⊢ ∀ (f₂ : Y ⟶ X'' k₂) (hf₁ : f₁ ≫ f'' k₁ = s) (hf₂ : f₂ ≫ f'' k₂ = s),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β k₁)).op.toLoc (q' k₁).op.toLoc (r' k₁).op.toLoc ⋯)).symm.app
              (D.obj (α (β k₁)))).hom ≫
        ((pullFunctor F ⋯).obj D).hom s f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w ⋙ pullFunctor F w').obj D).hom s f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapComp' (p' (β k₂)).op.toLoc (q' k₂).op.toLoc (r' k₂).op.toLoc ⋯)).symm.app
              (D.obj (α (β k₂)))).hom
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

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

Tactic:
rw [← Coverage.toGrothendieck_toPrecoverage]

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
K : Coverage C
h : K.Generates J
⊢ K.toGrothendieck = J
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : (fun X ↦ X) (S.obj (op α))
x : (fun X ↦ X) β
⊢ (ConcreteCategory.hom (eval S β ((ConcreteCategory.hom (S.map f.op)) s))) x =
    (ConcreteCategory.hom (eval S α s)) ((ConcreteCategory.hom f) x)

Tactic:
by
  simp_rw [eval, ← comp_apply, ← Functor.map_comp, ← op_comp]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : MonoOver F
f : X ⟶ Y
⊢ range (Over.Hom.left f.hom ≫ Y.arrow) ≤ range Y.arrow

Tactic:
apply range_comp_le

Goal state after: