mathlib-initiative/mathlib-tactics huggingface dataset:
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 φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ + (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' =
    (ConcreteCategory.hom (R.obj.map f.op)) (r + r')

Tactic:
_root_.map_add,

Goal state after:
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 φ
X : Cᵒᵖ
r r' : ↑(R.obj.obj X)
m : ↑(A.obj.obj X)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ↑(R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
r₀' : ↑(R₀.obj (Opposite.op Y))
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' = (ConcreteCategory.hom (R.obj.map f.op)) r'
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ + (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀' =
    (ConcreteCategory.hom (R.obj.map f.op)) r + (ConcreteCategory.hom (R.obj.map f.op)) r'
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (N ⊓ ?m.161) ∈ J₁ Y

pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve X

Tactic:
rw [← MSNS]

Goal state after:
case refine_1.mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
Y : C
f : Y ⟶ X
q : ∀ ⦃Z : C⦄ (g : Z ⟶ X), S.arrows g → Sieve.pullback g M = Sieve.pullback g N
MSNS : M ⊓ S = N ⊓ S
hf : J₁.Covers M f
⊢ Sieve.pullback f (M ⊓ S) ∈ J₁ Y
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
⊢ x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
hx

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
⊢ topologyOfClosureOperator J₁.closureOperator ⋯ = J₁

Tactic:
by
  ext X S
  apply GrothendieckTopology.close_eq_top_iff_mem

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
⊢ x.Compatible →
    ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂),
      f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
        (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
hx

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
⊢ ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂),
    f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
      (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
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
X : D
S : K.Cover X
s : Multifork (S.index R)
Y : C
f : G.obj Y ⟶ X
W : C
g : W ⟶ Y
i : S.Arrow
h : G.obj W ⟶ i.Y
w : h ≫ i.f = G.map g ≫ f
⊢ (↑S).arrows (G.map g ≫ f)

Tactic:
by simpa only [← w] using S.1.downward_closed i.hf h

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
this :
  ∀ (x : (i : ι) → (F.op ⋙ (Functor.closedSieves K).toFunctor).obj (op (Y i))),
    Arrows.Compatible (F.op ⋙ (Functor.closedSieves K).toFunctor) f x →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ (Functor.closedSieves K).toFunctor).map (f i).op)) t = x i
x : (i : ι) → (Functor.closedSieves K).toFunctor.obj (op (F.obj (Y i)))
⊢ Arrows.Compatible (Functor.closedSieves K).toFunctor (fun i ↦ F.map (f i)) x →
    ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((Functor.closedSieves K).toFunctor.map (F.map (f i)).op)) t = x i

Tactic:
hx

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
this :
  ∀ (x : (i : ι) → (F.op ⋙ (Functor.closedSieves K).toFunctor).obj (op (Y i))),
    Arrows.Compatible (F.op ⋙ (Functor.closedSieves K).toFunctor) f x →
      ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((F.op ⋙ (Functor.closedSieves K).toFunctor).map (f i).op)) t = x i
x : (i : ι) → (Functor.closedSieves K).toFunctor.obj (op (F.obj (Y i)))
hx : Arrows.Compatible (Functor.closedSieves K).toFunctor (fun i ↦ F.map (f i)) x
⊢ ∃! t, ∀ (i : ι), (ConcreteCategory.hom ((Functor.closedSieves K).toFunctor.map (F.map (f i)).op)) t = x 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
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
⊢ Sieve.functorPushforward G (Sieve.functorPullback G ↑T) ∈ K (G.obj X)

Tactic:
by
  refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_
  apply K.transitive (G.is_cover_of_isCoverDense _ _) _
  rintro W _ ⟨Z, iWZ, iZY, rfl⟩
  rw [Sieve.pullback_comp]; apply K.pullback_stable; clear W iWZ
  apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))
  rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩
  exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
⊢ x.Compatible →
    ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂),
      f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
        (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
hx

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
⊢ ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ G.obj Y₁) (f₂ : X ⟶ G.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁) (hg₂ : T g₂),
    f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
      (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
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:
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: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
E : PreOneHypercover Y
i₁ i₂ : E.I₀
W : Over X
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
⊢ (overEquiv W) (E.sieve₁ p₁ p₂) = (E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)

Tactic:
ext
  rw [overEquiv_iff]
  refine ⟨fun ⟨k, b, hb₁, hb₂⟩ ↦ ⟨k, b.left, congr($(hb₁).left), congr($(hb₂).left)⟩, ?_⟩
  intro ⟨k, b, hb₁, hb₂⟩
  exact ⟨k, Over.homMk b (by simpa using (hb₁ =≫ (E.X i₁).hom).symm), by cat_disch, by cat_disch⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ (Over.forget X).obj (E.X i₁)
p₂ : W ⟶ (Over.forget X).obj (E.X i₂)
w : p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂)
this : p₁ ≫ (E.X i₁).hom = p₂ ≫ (E.X i₂).hom
⊢ Over.homMk p₁ ⋯ ≫ E.f i₁ = Over.homMk p₂ ⋯ ≫ E.f i₂

Tactic:
by ext; simpa

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

Goal state before:
pp: case refine_1.of
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ (Sieve.overEquiv { left := Z, right := right, hom := s }).symm (Sieve.generate S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }

Tactic:
rw [Sieve.overEquiv_symm_generate]

Goal state after:
case refine_1.of
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
R : Sieve Y
Z : C
S : Presieve Z
hS : S ∈ K.toCoverage.coverings Z
s : Z ⟶ X
⊢ Sieve.generate (Presieve.functorPullback (Over.forget X) S) ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Z, right := right, hom := s }
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
fconstructor
    · intros
      have hx := cokernel.π_of_epi f
      by_contra h
      subst h
      exact (h _).mp inferInstance hx
    · intro hf
      suffices Epi f by exact isIso_of_mono_of_epi _
      apply Preadditive.epi_of_cokernel_zero
      by_contra h'
      exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.fst

Tactic:
by intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.snd

Tactic:
by intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeInf C
X Y : C
⊢ ∀ (s : BinaryFan X Y) (m : s.pt ⟶ X ⊓ Y), m ≫ homOfLE ⋯ = s.fst → m ≫ homOfLE ⋯ = s.snd → m = homOfLE ⋯

Tactic:
by intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inl

Tactic:
by intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y), homOfLE ⋯ ≫ homOfLE ⋯ = s.inr

Tactic:
by intros; rfl

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

Goal state before:
pp: C : Type u
inst✝ : SemilatticeSup C
X Y : C
⊢ ∀ (s : BinaryCofan X Y) (m : X ⊔ Y ⟶ s.pt), homOfLE ⋯ ≫ m = s.inl → homOfLE ⋯ ≫ m = s.inr → m = homOfLE ⋯

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U✝ V W : Opens ↑X
f g : X ⟶ Y
h : f = g
U : Opens ↑Y
⊢ (map f).obj U = (map g).obj U

Tactic:
rw [congr_arg map h]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
⊢ x ∈ U → x ∈ (Opens.map f).obj (hf.functorObj U)

Tactic:
hx

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ x ∈ (Opens.map f).obj (hf.functorObj U)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
⊢ x ∈ V → x ∈ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
hx

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
x : ↑Y
hx : x ∈ V
⊢ x ∈ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (grothendieckTopology T).toPretopology.coverings X
x : T
⊢ x ∈ X → ∃ U f, R f ∧ x ∈ U

Tactic:
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
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
⊢ x ∈ X → ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
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 : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
⊢ x ∈ iSup U → ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
hx

Goal state after:
X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
U : Opens ↑X
x : ↑X
⊢ x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
hx

Goal state after:
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
⊢ x ∈ U → ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1

Tactic:
hx

Goal state after:
case mpr
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hb : ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ ∃ U_1 f, (Sieve.coverByImage B U).arrows f ∧ x ∈ U_1
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
⊢ x ∈ (Opens.map f).obj U → ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1

Tactic:
hx

Goal state after:
X Y : TopCat
f : X ⟶ Y
U : Opens ↑Y
S : Sieve U
hS : S ∈ (Opens.grothendieckTopology ↑Y) U
x : ↑X
hx : x ∈ (Opens.map f).obj U
⊢ ∃ U_1 f_1, (Sieve.functorPushforward (Opens.map f) S).arrows f_1 ∧ x ∈ U_1
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
⊢ Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.counit)
      (R.over ((D i.fst).X i.snd).left).obj =
    (𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
      ((D i.fst).X i.snd).iteratedSliceEquiv.inverse.op.whiskerLeft
        (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom

Tactic:
ext : 2; exact R.1.map_id _

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
⊢ (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom ≫
      ((D i.fst).X i.snd).iteratedSliceEquiv.functor.op.whiskerLeft (𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
        Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.unit)
          ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj =
    𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj

Tactic:
ext : 2; exact R.1.map_id _

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)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
t : CC ((stalkFunctor C x).obj F)
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
hst :
  (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U₁ x hxU₁)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) t
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = t

Tactic:
rcases exists_germ_eq F t with ⟨U₂, hxU₂, t, rfl⟩

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)
F G : Presheaf C X
f : F ⟶ G
h : ∀ (U : Opens ↑X), Function.Injective ⇑(ConcreteCategory.hom (f.app (op U)))
x : ↑X
U₁ : Opens ↑X
hxU₁ : x ∈ U₁
s : ToType (F.obj (op U₁))
U₂ : Opens ↑X
hxU₂ : x ∈ U₂
t : ToType (F.obj (op U₂))
hst :
  (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U₁ x hxU₁)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.germ U₂ x hxU₂)) t)
⊢ (ConcreteCategory.hom (F.germ U₁ x hxU₁)) s = (ConcreteCategory.hom (F.germ U₂ x hxU₂)) t