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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
ι : Type u_2
inst✝ : Small.{max w v, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ uliftYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
⊢ Sieve.ofArrows X f ∈ J S ↔
    Presheaf.IsLocallySurjective J (Cofan.IsColimit.desc hc fun i ↦ uliftYoneda.{w, v, u}.map (f i))

Tactic:
by
  let e : Discrete.functor (fun i ↦ uliftYoneda.{w}.obj (X i)) ≅
      Discrete.functor (fun i ↦ shrinkYoneda.{max w v}.obj (X i)) :=
    Discrete.natIso (fun i ↦ uliftYonedaIsoShrinkYoneda.{w}.app (X i.as))
  let hc' := (IsColimit.precomposeInvEquiv e _).2 hc
  rw [ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map.{max w v} J f hc']
  have :
      Cofan.IsColimit.desc hc (fun i ↦ uliftYoneda.map (f i)) ≫
        uliftYonedaIsoShrinkYoneda.hom.app _ =
      Cofan.IsColimit.desc hc' (fun i ↦ shrinkYoneda.map (f i)) :=
    Cofan.IsColimit.hom_ext hc _ _ (fun i ↦ by
      rw [Cofan.IsColimit.fac_assoc, NatTrans.naturality,
        ← Cofan.IsColimit.fac hc' (fun i ↦ shrinkYoneda.map (f i)) i]
      simp [Cofan.inj, e])
  rw [← this, Presheaf.isLocallySurjective_comp_iff J]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun x ↦ q₂ x ≫ a.inj x) v u

Tactic:
let c : Cofan P := Cofan.mk (pullback v u)
    fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) (by simp [(hP i).w, hu])
  obtain ⟨hc⟩ := hau.nonempty_isColimit_of_isPullback_left f u
    v q₁ q₂ hP (IsPullback.of_hasPullback _ _) c (Iso.refl _)
  refine (IsPullback.of_hasPullback v u).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
  · exact hc.coconePointUniqueUpToIso hd
  · refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_fst _ _ _
  · refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_snd _ _ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
⊢ IsPullback (Cofan.IsColimit.desc hd fun p ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v

Tactic:
by
  let c : Cofan P := Cofan.mk (pullback u v)
    fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj _)
      (by simp [(hP p.1 p.2).w, hu, hv])
  obtain ⟨hc⟩ := hau.nonempty_isColimit_prod_of_isPullback hbu f g u
    v hP (IsPullback.of_hasPullback _ _) (d := c) (Iso.refl _)
  refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
  · exact hc.coconePointUniqueUpToIso hd
  · refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_fst _ _ _
  · refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_snd _ _ _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝⁶ : Presheaf.IsLocallyInjective J α
inst✝⁵ : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝⁴ : Presheaf.IsLocallyInjective J φ
inst✝³ : Presheaf.IsLocallySurjective J φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
⊢ Presheaf.IsSheaf J (sheafify α φ').val.presheaf

Tactic:
by exact A'.property

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
ι : Type w'
e : ι ≃ E.I₀
⊢ (E.restrictIndex ⇑e).presieve₀ = E.presieve₀

Tactic:
refine le_antisymm (fun Y g ⟨i⟩ ↦ ⟨e i⟩) fun Y g ⟨i⟩ ↦ ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
ι : Type w'
e : ι ≃ E.I₀
Y : C
g : Y ⟶ S
x✝ : E.presieve₀ g
i : E.I₀
⊢ (E.restrictIndex ⇑e).presieve₀ (E.f i)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
⊢ ∃ W x x, True

Tactic:
let U := IsCofiltered.min (T.obj A) (T.obj B)

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
⊢ ∃ W x x, True
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
i✝ : ↑R.uncurry ⊕ ↑T.uncurry
i : ↑R.uncurry
⊢ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) (Sum.inl i) ⟶ S

Tactic:
by exact i.1.2

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
i✝ : ↑R.uncurry ⊕ ↑T.uncurry
i : ↑T.uncurry
⊢ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) (Sum.inr i) ⟶ S

Tactic:
by exact i.1.2

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

Goal state before:
pp: case refine_1.transitive
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
J : Pretopology C
T : C
S✝ : Sieve T
X : C
R S : Sieve X
hR : J.toCoverage.Saturate X R
hRS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.toCoverage.Saturate Y (Sieve.pullback f S)
hle : ∃ R_1 ∈ J.coverings X, R_1 ≤ R.arrows
hfS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f S).arrows
⊢ ∃ R ∈ J.coverings X, R ≤ S.arrows

Tactic:
obtain ⟨R', hR', hle⟩ := hle
        choose S' hS' hS'le using hfS
        refine ⟨Presieve.bind R' (fun Y f hf ↦ S' (hle _ _ hf)), ?_, fun Z u hu ↦ ?_⟩
        · exact J.transitive R' (fun Y f hf ↦ S' (hle Y _ hf)) hR' fun Y f H ↦ hS' (hle Y _ H)
        · obtain ⟨W, g, w, hw, hg, rfl⟩ := hu
          exact hS'le _ _ _ hg

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
a : A
⊢ (L.leftKanExtensionUnit (F ⋙ G)).app a ≫ (G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
    G.map ((L.leftKanExtensionUnit F).app a)

Tactic:
by
  simpa [-leftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (leftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
⊢ Sieve.functorPullback G S ∈ J U

Tactic:
refine J.superset_covering ?_ (F.cover_lift J K (K.pullback_stable (e.hom.app U) hS))
    intro Y f (hf : S.arrows (F.map f ≫ e.hom.app U))
    have := S.downward_closed hf (e.inv.app Y)
    rwa [e.hom.naturality f, ← Category.assoc, Iso.inv_hom_id_app, Category.id_comp] at this

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

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
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
⊢ f = g

Tactic:
by
  apply (hR (op X)).hom_ext
  intro j
  apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩
  intro ⟨W, i, hi⟩
  have eq := h (GrothendieckTopology.Cover.Arrow.mk _ (G.map i ≫ j.hom.unop) hi)
  dsimp at eq ⊢
  simp only [Category.assoc, ← NatTrans.naturality, Functor.comp_map, ← Functor.map_comp_assoc,
    Functor.op_map, Quiver.Hom.unop_op]
  rw [reassoc_of% eq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X : C
⊢ F.obj.map (𝟙 (op X)) = 𝟙 (F.obj.obj (op X))

Tactic:
map_id

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X : C
⊢ 𝟙 (F.obj.obj (op X)) = 𝟙 (F.obj.obj (op X))
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₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
k✝ : E.I₁ i j
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq ⋯ ⋯) k) = E.Y (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))

Tactic:
congr 1; apply E.congrIndexOneOfEq_equiv s₀ s₁ _

Goal state after:
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
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ x✝ ∈ (e.inverse.inducedTopology J) x✝¹

Tactic:
rw [mem_inducedTopology_iff_of_isCoverDense]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝ : IsDenseSubsite K J e.inverse
x✝¹ : D
x✝ : Sieve x✝¹
⊢ x✝ ∈ K x✝¹ ↔ Sieve.functorPushforward e.inverse x✝ ∈ J (e.inverse.obj x✝¹)
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      homMk (c.π.app Y) ⋯ =
    homMk (c.π.app X) ⋯ ≫ F.map f

Tactic:
apply CommaMorphism.ext
    · simpa using (c.w f).symm
    · simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y.left
⊢ functorPushforward (Over.forget X) (functorPullback (Over.forget X) S) = S

Tactic:
apply arrows_ext
  simp [← arrows_generate_map_eq_functorPushforward]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
⊢ ∀ {a b : Sieve Y}, functorPushforward (Over.forget X) a ≤ functorPushforward (Over.forget X) b ↔ a ≤ b

Tactic:
exact ⟨fun h ↦ by simpa using functorPullback_monotone _ _ h,
      fun h ↦ functorPushforward_monotone _ _ h⟩

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

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ (pullback.lift (f.h₁ k) (g.h₁ k) ⋯ ≫ (E.inter F).p₁ (f.s₁ k, g.s₁ k)) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd) =
    (G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝) ≫
      pullback.snd
        (E.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).fst)
        (F.f
          ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm
              ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i✝)).snd)

Tactic:
· simpa using g.w₁₁ k

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ S.preOneHypercover.sieve₀.arrows f → (↑S).arrows f

Tactic:
rintro ⟨_, _, _, ⟨g⟩, rfl⟩
    exact S.1.downward_closed g.hf _

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

Goal state before:
pp: C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ Presieve.functorPushforward (Over.star X ⋙ Over.forget X) S.arrows f

Tactic:
refine ⟨_, _, prod.lift (f ≫ prod.fst) (𝟙 _), hf, Limits.prod.hom_ext ?_ ?_⟩

Goal state after:
case refine_1
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ f ≫ prod.fst = (prod.lift (f ≫ prod.fst) (𝟙 y) ≫ (Over.star X ⋙ Over.forget X).map (f ≫ prod.snd)) ≫ prod.fst

case refine_2
C : Type u'
inst✝¹ : Category.{v_1, u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
X U : C
S : Sieve U
hs : S ∈ J U
y : C
f : y ⟶ ((Over.star X).obj U).left
hf : (Sieve.pullback prod.snd S).arrows f
⊢ f ≫ prod.snd = (prod.lift (f ≫ prod.fst) (𝟙 y) ≫ (Over.star X ⋙ Over.forget X).map (f ≫ prod.snd)) ≫ prod.snd
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ (grothendieckTopology T).toPretopology ≤ pretopology T

Tactic:
intro X R hR x hx

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (grothendieckTopology T).toPretopology.coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, R f ∧ x ∈ U
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
⊢ pretopology T ≤ (grothendieckTopology T).toPretopology

Tactic:
intro X R hR x hx

Goal state after:
case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ CoverPreserving (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X) (Opens.map f)

Tactic:
by
  constructor
  intro U S hS x hx
  obtain ⟨V, i, hi, hxV⟩ := hS (f x) hx
  exact ⟨_, (Opens.map f).map i, ⟨_, _, 𝟙 _, hi, Subsingleton.elim _ _⟩, hxV⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1))

Tactic:
apply @Continuous.comp R (R × R) R τR (@instTopologicalSpaceProd R R τR (moduleTopology R R))
      (moduleTopology R R)

Goal state after:
case hg
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun rs ↦ rs.1 • rs.2

case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ (ConcreteCategory.hom (cM.ι.app i)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app i)) r • (ConcreteCategory.hom (cM.ι.app i)) m

Tactic:
apply α.addCommGroupIsoToAddEquiv.eq_symm_apply.mpr ?_

Goal state after:
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
⊢ α.addCommGroupIsoToAddEquiv ((ConcreteCategory.hom (cM.ι.app i)) (r • m)) =
    ↑(hcR.coconePointUniqueUpToIso
                  (RingCat.FilteredColimits.colimitCoconeIsColimit
                    R)).ringCatIsoToRingEquiv.toRingHom.toMonoidWithZeroHom
        ((ConcreteCategory.hom (cR.ι.app i)) r) •
      (hcM.coconePointUniqueUpToIso
              (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)).addCommGroupIsoToAddEquiv.toFun
        ((ConcreteCategory.hom (cM.ι.app i)) m)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ kerι φ ≫ φ = 0

Tactic:
ext ⟨_, hm⟩

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
val✝ : ↑M.toModuleCat
hm : val✝ ∈ (↑(Hom.hom φ)).ker
⊢ (ConcreteCategory.hom (kerι φ ≫ φ)) ⟨val✝, hm⟩ = (ConcreteCategory.hom 0) ⟨val✝, hm⟩
Module: Mathlib.CategoryTheory.Presentable.Finite

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : F.IsFinitelyAccessible
H : ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
exact H

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
x✝ : PreservesFilteredColimitsOfSize.{w, w, v, v', u, u'} F
H : ∀ (J : Type w) [inst : Category.{w, w} J] [IsFiltered J], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], PreservesColimitsOfShape J F

Tactic:
exact H

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasCardinalFilteredColimits C ℵ₀
H : ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], HasColimitsOfShape J C
⊢ ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C

Tactic:
exact H

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
x✝ : HasFilteredColimitsOfSize.{w, w, v, u} C
H : ∀ (I : Type w) [inst : Category.{w, w} I] [IsFiltered I], HasColimitsOfShape I C
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsFiltered J], HasColimitsOfShape J C

Tactic:
exact H

Goal state after: