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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
H : S.FactorsThru T
hS : IsSheafFor P S
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
⊢ IsSheafFor P T

Tactic:
simp only [← Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor] at *
  choose W i e h1 h2 using H
  refine ⟨?_, fun x hx => ?_⟩
  · intro x y₁ y₂ h₁ h₂
    refine hS.1.ext (fun Y g hg => ?_)
    simp only [← h2 hg, op_comp, P.map_comp, types_comp_apply, h₁ _ (h1 _), h₂ _ (h1 _)]
  let y : S.FamilyOfElements P := fun Y g hg => P.map (i _).op (x (e hg) (h1 _))
  have hy : y.Compatible := by
    intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h
    rw [← types_comp_apply (P.map (i h₁).op) (P.map g₁.op),
      ← types_comp_apply (P.map (i h₂).op) (P.map g₂.op),
      ← P.map_comp, ← op_comp, ← P.map_comp, ← op_comp]
    apply hx
    simp only [h2, h, Category.assoc]
  let ⟨_, h2'⟩ := hS
  obtain ⟨z, hz⟩ := h2' y hy
  refine ⟨z, fun Y g hg => ?_⟩
  obtain ⟨R, hR1, hR2⟩ := h hg
  choose WW ii ee hh1 hh2 using hR2
  refine hR1.ext (fun Q t ht => ?_)
  rw [← types_comp_apply (P.map g.op) (P.map t.op), ← P.map_comp, ← op_comp, ← hh2 ht,
    op_comp, P.map_comp, types_comp_apply, hz _ (hh1 _),
    ← types_comp_apply _ (P.map (ii ht).op), ← P.map_comp, ← op_comp]
  apply hx
  simp only [Category.assoc, h2, hh2]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
⊢ x = y

Tactic:
obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
hS : S ∈ J X
⊢ Nonempty (IsLimit (Cover.multifork ⟨S, hS⟩ P))

Tactic:
obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
hS : S ∈ J X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
⊢ Nonempty (IsLimit (Cover.multifork ⟨S, hS⟩ P))
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.PreservesRightKanExtension F L
inst✝ : L.HasRightKanExtension F
a : A
⊢ (G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫ G.map ((L.rightKanExtensionCounit F).app a) =
    (L.rightKanExtensionCounit (F ⋙ G)).app a

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

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

Goal state before:
pp: case mpr.transitive.refine_2.h
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
hx : x.Compatible
y : ⦃Z : C⦄ → (g : Z ⟶ Y) → Presieve.FamilyOfElements P (Sieve.pullback (𝟙 Z) (Sieve.pullback (g ≫ f) S)).arrows :=
  fun Z g ZZ gg hgg ↦ x (gg ≫ g) ⋯
hy : ∀ ⦃Z : C⦄ (g : Z ⟶ Y), (y g).Compatible
z : ⦃Z : C⦄ → ⦃g : Z ⟶ Y⦄ → (Sieve.pullback f R).arrows g → P.obj (Opposite.op Z)
hz : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ Y⦄ (hg : (Sieve.pullback f R).arrows g), (y g).IsAmalgamation (z hg)
q : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows := fun Z g hg ↦ z hg
hq : q.Compatible
t : P.obj (Opposite.op Y)
ht : q.IsAmalgamation t
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f S).arrows g
ZZ : C
gg : ZZ ⟶ Z
hgg : (Sieve.pullback (g ≫ f) R).arrows gg
ZZZ : C
ggg : ZZZ ⟶ ZZ
hggg : (Sieve.pullback (𝟙 ZZ) (Sieve.pullback (gg ≫ g ≫ f) S)).arrows ggg
⊢ (Sieve.pullback (𝟙 ZZ) (Sieve.pullback ((gg ≫ g) ≫ f) S)).arrows ggg

Tactic:
simpa using hggg

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Sieve.functorPushforward F (E.sieve₁' i₁ i₂) ≤
    (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))

Tactic:
rw [PreOneHypercover.sieve₁'_eq_sieve₁]

Goal state after:
case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Sieve.functorPushforward F (E.sieve₁ (pullback.fst (E.f i₁) (E.f i₂)) (pullback.snd (E.f i₁) (E.f i₂))) ≤
    (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂)))
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h
      apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _)) <;>
        simp [← h.left, ← h.right, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (Presieve.map F (ofArrows Y f))

Tactic:
Presieve.map_ofArrows

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
X : C
ι : Type (max u₁ v₁)
Y : ι → C
f : (i : ι) → Y i ⟶ X
hS : Sieve.ofArrows Y f ∈ J X
⊢ IsSheafFor (Functor.closedSieves K).toFunctor (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))
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
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'
i : IsIso (G.op.whiskerLeft α.hom)
⊢ IsIso α

Tactic:
convert! (sheafIso (asIso (whiskerLeft G.op α.hom))).isIso_hom using 1
  ext1
  apply (sheafHom_eq _ _).symm

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
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g

Tactic:
have := IsDenseSubsite.isLocallyFull J K G
  have := IsDenseSubsite.isCoverDense J K G
  let adj₁ := (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
  let adj₂ := sheafificationAdjunction J A
  change IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _
    ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
      f ≫ IsCoverDense.restrictHomEquivHom (adj₂.homEquiv _ _ (adj₁.homEquiv _ _ g))
  rw [← IsCoverDense.restrictHomEquivHom_naturality_left]
  congr 2
  trans adj₂.homEquiv _ _ ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫
    (adj₁.homEquiv _ _) g)
  · congr 1
    apply adj₁.homEquiv_naturality_left
  · apply adj₂.homEquiv_naturality_left

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 : Presieve Y
⊢ functorPullback (Over.forget X) (map (Over.forget X) S) = S

Tactic:
by
  let R : Presieve Y.left := fun Z g ↦ S (Over.homMk g : Over.mk (g ≫ Y.hom) ⟶ Y)
  suffices hR : (R.functorPullback (Over.forget X)) = S by
    rw [← hR, functorPullback_map_functorPullback]
  funext Z f
  obtain ⟨Z, fZ, rfl⟩ := Z.mk_surjective
  obtain ⟨g : Z ⟶ Y.left, rfl : g ≫ Y.hom = fZ, rfl⟩ := Over.homMk_surjective f
  rfl

Goal state after:
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 : 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) =
    G.p₁ k ≫ (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i✝

Tactic:
by
    apply pullback.hom_ext
    · simpa using f.w₁₁ k
    · simpa using g.w₁₁ k

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

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₁ hg₁)

Tactic:
apply ConcreteCategory.congr_hom

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
e : (Over.map f).obj W' ≅ W := ⋯
⊢ F.obj.map f₁.op =
    F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom
        (F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)))
      (x g₂ hg₂)

Tactic:
apply ConcreteCategory.congr_hom

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
e : (Over.map f).obj W' ≅ W := ⋯
⊢ F.obj.map f₂.op =
    F.obj.map (((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op ≫ (Over.isoMk (Iso.refl W.left) ⋯).inv.op)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
⊢ Precoverage.comap (Over.forget X) K ≤ (K.toGrothendieck.over X).toPrecoverage

Tactic:
intro Y R hR

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X : C
Y : Over X
R : Presieve Y
hR : R ∈ (Precoverage.comap (Over.forget X) K).coverings Y
⊢ R ∈ (K.toGrothendieck.over X).toPrecoverage.coverings Y
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi f

Tactic:
rw [← image.fac f]
  have : IsIso (image.ι f) := isIso_of_mono_of_nonzero fun h => w (eq_zero_of_image_eq_zero h)
  apply epi_comp

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

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
⊢ ((pushforwardId R).inv ≫
            pushforwardNatTrans (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R)) adj.counit ≫
              (pushforwardCongr ⋯).hom ≫ (pushforwardComp ψ φ).inv).app
        ((pushforward ψ).obj X) ≫
      (pushforward ψ).map
        (((pushforwardComp φ ψ).hom ≫
              pushforwardNatTrans (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) adj.unit ≫
                (pushforwardCongr ⋯).hom ≫ (pushforwardId S).hom).app
          X) =
    𝟙 ((pushforward ψ).obj X)

Tactic:
by
    ext U x
    change (X.val.presheaf.map (G.map (adj.counit.app U.unop)).op ≫
      X.val.presheaf.map (adj.unit.app (G.obj U.unop)).op) _ = _
    rw [← Functor.map_comp, ← op_comp, adj.right_triangle_components]
    simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk (homOfLE ⋯).op
⊢ ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H })

Tactic:
have hx : IsTerminal x :=
    { lift := fun s ↦ by
        fapply CostructuredArrow.homMk
        · change op (unop _) ⟶ op (⟨_, H⟩ : Opens _)
          refine (homOfLE ?_).op
          apply (Set.image_mono s.pt.hom.unop.le).trans
          exact Set.image_preimage.l_u_le (SetLike.coe s.pt.left.unop)
        · simp [eq_iff_true_of_subsingleton] }

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
X✝ : TopCat
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U : Opens ↑X
H : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
x : CostructuredArrow (Opens.map f).op (op U) := CostructuredArrow.mk (homOfLE ⋯).op
hx : IsTerminal x
⊢ ((pullback C f).obj ℱ).obj (op U) ≅ ℱ.obj (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := H })
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p ↦ p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a ↦ a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m ↦ a • m) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
rw [← nhds_prod_eq] at hmul
    refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;>
      simpa [ContinuousAt]

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.hom.app (op U)))

Tactic:
intro t

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X := ⋯
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst ∧
    F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
        m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
          m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s

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

Goal state after:
case property.refine_1
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst

case property.refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
    m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
      m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s