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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) ((sheafComposeNatTrans J F adj₁ adj₂).app P)

Tactic:
dsimp [ObjectProperty.ι_obj, sheafComposeNatTrans, id_obj]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝² : Category.{v_1, u_1} A
inst✝¹ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
inst✝ : J.HasSheafCompose F
P : Cᵒᵖ ⥤ A
α : G₂.obj (P ⋙ F) ⟶ (sheafCompose J F).obj (G₁.obj P)
hα : adj₂.unit.app (P ⋙ F) ≫ (sheafToPresheaf J B).map α = whiskerRight (adj₁.unit.app P) F
⊢ (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))) α =
    (adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P)))
      ((adj₂.homEquiv (P ⋙ F) ((sheafCompose J F).obj (G₁.obj P))).symm (whiskerRight (adj₁.unit.app P) F))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case h_obj
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = (Discrete.functor F').obj X

Tactic:
exact fun i ↦ rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case h_obj
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = (Discrete.functor F').obj X

pp: case h_map
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y), F.map f ≍ (Discrete.functor F').map f

Tactic:
· exact fun i ↦ rfl

Goal state after:
case h_map
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
F' : Fin (n + 1) → C := ⋯
⊢ ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y), F.map f ≍ (Discrete.functor F').map f
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map (f i)).app (op V))) (shrinkYonedaObjObjEquiv.symm a) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)

Tactic:
shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm a (f i),

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
Y : C
i : ι
a : V ⟶ X i
fac : a ≫ f i = v ≫ g
⊢ shrinkYonedaObjObjEquiv.symm (a ≫ f i) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1.isTrue
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasInitial C
ι : Type u_3
X : ι → C
c : Cofan X
hc : IsVanKampenColimit c
i j : ι
inst✝ : DecidableEq ι
k : ι
h✝ : k = i
⊢ eqToHom ⋯ ≫ c.ι.app { as := k } = eqToHom ⋯ ≫ c.inj i

Tactic:
subst ‹k = i›; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
⊢ ∀ (e : Ext S.X₂ Y i), e = 0

Tactic:
x₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₃ : HasProjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ x₂ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian

Goal state before:
pp: C : Type u'
inst✝² : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
⊢ Abelian (SheafOfModules R)

Tactic:
let adj := PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)
  exact abelianOfAdjunction _ _ (asIso (adj.counit)) adj

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
i : I
⊢ (free J).unitHomEquiv.symm ((free J).freeHomEquiv (𝟙 (free J)) (f i)) = ιFree (f i)

Tactic:
unitHomEquiv_symm_freeHomEquiv_apply,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝¹ : HasWeakSheafify J✝ AddCommGrpCat
inst✝ : J✝.WEqualsLocallyBijective AddCommGrpCat
I J : Type u
f : I → J
i : I
⊢ ιFree (f i) ≫ 𝟙 (free J) = ιFree (f i)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
⊢ f₁ = f₂

Tactic:
let α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
    { app := fun X => eqToHom (by simp [← h₁]) }
  let α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
    { app := fun X => eqToHom (by simp [← h₂]) }
  let c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
    (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F) :)).obj
      (c.toStructuredArrowCone F f₁)
  let c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
    (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F) :)).obj
      (c.toStructuredArrowCone F f₂)
  -- The two cones can then be combined and we may obtain a cone over the two cones since
  -- `StructuredArrow s.pt F` is cofiltered.
  let c₀ := IsCofiltered.cone (biconeMk _ c₁ c₂)
  let g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
  let g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
  -- Then `g₁.right` and `g₂.right` are two maps from the same cone into the `c`.
  have : ∀ j : J, g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j := by
    intro j
    injection c₀.π.naturality (BiconeHom.left j) with _ e₁
    injection c₀.π.naturality (BiconeHom.right j) with _ e₂
    convert! e₁.symm.trans e₂ <;> simp [c₁, c₂]
  have : c.extend g₁.right = c.extend g₂.right := by
    unfold Cone.extend
    congr 1
    ext x
    apply this
  -- And thus they are equal as `c` is the limit.
  have : g₁.right = g₂.right := calc
    g₁.right = hc.lift (c.extend g₁.right) := by
      apply hc.uniq (c.extend _)
      simp
    _ = hc.lift (c.extend g₂.right) := by
      congr
    _ = g₂.right := by
      symm
      apply hc.uniq (c.extend _)
      simp
  -- Finally, since `fᵢ` factors through `F(gᵢ)`, the result follows.
  calc
    f₁ = c₀.pt.hom ≫ F.map g₁.right := g₁.w.symm
    _ = c₀.pt.hom ≫ F.map g₂.right := by rw [this]
    _ = f₂ := g₂.w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S T : C
E✝¹ : PreZeroHypercover S
F✝¹ : PreZeroHypercover S
E✝ : PreZeroHypercover S
F✝ : PreZeroHypercover S
G : PreZeroHypercover S
E : PreZeroHypercover S
F : PreZeroHypercover S
f g : E.Hom F
hs : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
hs

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S T : C
E✝¹ : PreZeroHypercover S
F✝¹ : PreZeroHypercover S
E✝ : PreZeroHypercover S
F✝ : PreZeroHypercover S
G : PreZeroHypercover S
E : PreZeroHypercover S
F : PreZeroHypercover S
f g : E.Hom F
hs : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (g.s₀ i)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ ((topologyOfClosureOperator c pb).close S).arrows f ↔ ((c X) S).arrows f

Tactic:
change c _ (Sieve.pullback f S) = ⊤ ↔ c _ S f

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
c : (X : C) → ClosureOperator (Sieve X)
pb : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
Y : C
f : Y ⟶ X
⊢ (c Y) (Sieve.pullback f S) = ⊤ ↔ ((c X) S).arrows f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
⊢ ∀ b ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}, J.toGrothendieck ≤ b

Tactic:
intro K hK _ _ hS

Goal state after:
case refine_1
C : Type u_2
inst✝ : Category.{u_1, u_2} C
J : Precoverage C
K : GrothendieckTopology C
hK : K ∈ {K | ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, Sieve.generate S ∈ K X}
i✝ : C
a✝ : Sieve i✝
hS : a✝ ∈ J.toGrothendieck i✝
⊢ a✝ ∈ K i✝
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case mpr.pullback
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y✝ : C
f✝ : Y✝ ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y✝
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback f✝ S)).arrows

Tactic:
rw [← S.pullback_comp]

Goal state after:
case mpr.pullback
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
X✝ : C
S✝ : Sieve X✝
X : C
S : Sieve X
hS : J.Saturate X S
Y✝ : C
f✝ : Y✝ ⟶ X
ih : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
Y : C
f : Y ⟶ Y✝
⊢ Presieve.IsSheafFor P (Sieve.pullback (f ≫ f✝) S).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ (E.sum F.toPreZeroHypercover).presieve₀ ∈ J.coverings S

Tactic:
by
    rw [PreZeroHypercover.presieve₀_sum]
    exact J.sup_mem_coverings E.mem₀ F.mem₀

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F✝ : C ⥤ D
K : Precoverage D
F : C ⥤ D
E : J.ZeroHypercover S
h : J ≤ comap F K
⊢ E.presieve₀ ∈ (comap F K).coverings S

Tactic:
exact h _ E.mem₀

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g R).arrows f → Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.pullback g S)).arrows

Tactic:
intro Y f _
      rw [← pullback_comp]
      apply (hS _ _).isSeparatedFor

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
W : C
q : W ⟶ Z
⊢ (equalizerSieve ((ConcreteCategory.hom (F.map m.op)) a) ((ConcreteCategory.hom (F.map m.op)) b)).arrows q →
    (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))).arrows q

Tactic:
hq

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
W : C
q : W ⟶ Z
hq : (equalizerSieve ((ConcreteCategory.hom (F.map m.op)) a) ((ConcreteCategory.hom (F.map m.op)) b)).arrows q
⊢ (Sieve.functorPullback H (Sieve.pullback m (equalizerSieve a b))).arrows q
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT : T ∈ K.toGrothendieck (F.obj U)
R : Presieve (F.obj U)
hR : R ∈ K.coverings (F.obj U)
hle : R ≤ T.arrows
⊢ ∃ R ∈ K.coverings (F.obj U), R ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT⟩)).arrows

Tactic:
refine ⟨_, H hR, ?_⟩

Goal state after:
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT : T ∈ K.toGrothendieck (F.obj U)
R : Presieve (F.obj U)
hR : R ∈ K.coverings (F.obj U)
hle : R ≤ T.arrows
⊢ map F (functorPullback F R) ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT⟩)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
i j : F.I₀
k : F.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv) ≫
      E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k)) =
    F.p₁ k ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ i

Tactic:
by
    obtain ⟨i, rfl⟩ := s₀.surjective i
    obtain ⟨j, rfl⟩ := s₀.surjective j
    obtain ⟨k, rfl⟩ := s₁.surjective k
    rw [← cancel_epi (h₁ k).hom, reassoc_of% w₁₁ k]
    simp only [PreZeroHypercover.isoMk_inv_s₀, Category.assoc, PreZeroHypercover.isoMk_inv_h₀,
      Equiv.symm_apply_apply, eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id,
      Category.comp_id]
    rw [PreOneHypercover.isoMk_aux_assoc, ← eqToHom_naturality, eqToHom_refl, Category.comp_id,
      congrIndexOneOfEqIso_inv_p₁]
    apply PreOneHypercover.congrIndexOneOfEq_equiv

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Connected

Goal state before:
pp: J : Type u_1
⊢ IsConnected (WidePullbackShape J)

Tactic:
apply IsConnected.of_constant_of_preserves_morphisms
  intro α F H
  suffices ∀ i, F i = F none from fun j j' ↦ (this j).trans (this j').symm
  rintro ⟨⟩
  exacts [rfl, H (.term _)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
⊢ IsIso (colimitLimitToLimitColimitCone F)

Tactic:
have : IsIso (colimitLimitToLimitColimitCone F).hom := by
    suffices IsIso (colimitLimitToLimitColimit (uncurry.obj F) ≫
        lim.map (whiskerRight (currying.unitIso.app F).inv colim)) by
      apply IsIso.comp_isIso
    infer_instance

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F✝ : J × K ⥤ Type v
inst✝ : IsFiltered K
F : J ⥤ K ⥤ Type v
this : IsIso (colimitLimitToLimitColimitCone F).hom
⊢ IsIso (colimitLimitToLimitColimitCone F)
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁷ : Category.{v₃, u₃} A
B : Type u₄
inst✝⁶ : Category.{v₄, u₄} B
F : A ⥤ B
inst✝⁵ : G.IsCoverDense J
inst✝⁴ : G.Full
inst✝³ : G.IsContinuous K J
inst✝² : (G.sheafPushforwardContinuous B K J).EssSurj
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.PreservesSheafification F
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
hf : K.W (G.op.whiskerLeft f)
this✝ : K.W ((G.op.associator P F).hom ≫ G.op.whiskerLeft (whiskerRight f F) ≫ (G.op.associator Q F).inv)
this : K.W (G.op.whiskerLeft (whiskerRight f F))
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
rwa [K.W_whiskerLeft_iff (G := G) (J := J) (f := whiskerRight f F)] at this

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
⊢ ((overEquiv U) (functorPullback (Over.map f) S)).arrows g ↔ ((overEquiv ((Over.map f).obj U)) S).arrows g

Tactic:
let u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) :=
    Over.homMk (𝟙 Z) (by simp)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
⊢ ((overEquiv U) (functorPullback (Over.map f) S)).arrows g ↔ ((overEquiv ((Over.map f).obj U)) S).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ ((overEquiv U) (functorPullback (Over.map f) S)).arrows g ↔ ((overEquiv ((Over.map f).obj U)) S).arrows g

Tactic:
have : IsIso u :=
    ⟨Over.homMk (𝟙 Z) (by simp), by ext; simp [u], by ext; simp [u]⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
this : IsIso u
⊢ ((overEquiv U) (functorPullback (Over.map f) S)).arrows g ↔ ((overEquiv ((Over.map f).obj U)) S).arrows g
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ hf.functor.obj U
x : ↑Y
h : x ∈ V.1
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f)

Tactic:
obtain ⟨_, _, rfl⟩ := i.le h

Goal state after:
X Y : TopCat
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this : Mono f
U : Opens ↑X
V : Opens ↑Y
i : V ⟶ hf.functor.obj U
w✝ : ↑X
left✝ : w✝ ∈ ↑U
h : (ConcreteCategory.hom f) w✝ ∈ V.1
⊢ (ConcreteCategory.hom f) w✝ ∈ Set.range ⇑(ConcreteCategory.hom f)
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ { hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ } =
    𝟙 (Cone.whisker (generateEquivalenceOpensLe U hY).op.functor (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
ext
    simp [eqToHom_map]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
Y : Opens ↑X
hY : Y = iSup U
⊢ { hom := F.map (eqToHom ⋯), w := ⋯ } ≫ { hom := F.map (eqToHom ⋯), w := ⋯ } =
    𝟙 (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op)

Tactic:
ext
    simp [eqToHom_map]

Goal state after: