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

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
H : ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
P : Sheaf K (Type (max u₁ v₁ u₂ v₂))
Y : C
f : Y ⟶ X
⊢ Function.Bijective fun g ↦ (Sieve.shrinkFunctor.{max (max (max u₁ u₂) v₁) v₂, v₁, u₁} (Sieve.pullback f S)).ι ≫ g

Tactic:
exact (adj.map_comp_bijective_iff _ _).mp (H f _ P.property)

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
h : F.restrictedTopology K = J
⊢ F.inducedTopology K = J

Tactic:
by
  subst h
  rw [restrictedTopology_eq_inducedTopology]

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
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ K.W (G.op.whiskerLeft f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f

Tactic:
rfl

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
R : Presieve Y.left := fun Z g ↦ S (Over.homMk g ⋯)
Z : C
g : Z ⟶ Y.left
⊢ functorPullback (Over.forget X) R (Over.homMk g ⋯) = S (Over.homMk g ⋯)

Tactic:
rfl

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
Z : Over X
f : Z ⟶ Y
⊢ ((overEquiv Y).symm S).arrows f ↔ S.arrows (Over.Hom.left f)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X : C
⊢ (x.familyOfElements X).Compatible

Tactic:
by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ ⟨i₁, ⟨φ₁⟩⟩ ⟨i₂, ⟨φ₂⟩⟩ _
  simpa [hx.familyOfElements_apply f₁ i₁ φ₁,
    hx.familyOfElements_apply f₂ i₂ φ₂] using hx Z i₁ i₂ (g₁ ≫ φ₁) (g₂ ≫ φ₂)

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
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover 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)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (E.inter F.toPreOneHypercover).sieve₁ p₁ p₂ ∈ J W

Tactic:
rw [PreOneHypercover.sieve₁_inter h]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
A : Type u_1
inst✝³ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
inst✝² : HasPullbacks C
E : J.OneHypercover S
F : J.OneHypercover 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)
i₁ i₂ : (E.inter F.toPreOneHypercover).I₀
W : C
p₁ : W ⟶ (E.inter F.toPreOneHypercover).X i₁
p₂ : W ⟶ (E.inter F.toPreOneHypercover).X i₂
h : p₁ ≫ (E.inter F.toPreOneHypercover).f i₁ = p₂ ≫ (E.inter F.toPreOneHypercover).f i₂
⊢ (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.fst (E.f i₂.1) (F.f i₂.2))).arrows
      fun x f x_1 ↦
      Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i₁.1) (F.f i₁.2)) (p₂ ≫ pullback.snd (E.f i₂.1) (F.f i₂.2)))) ∈
    J W
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: case hex
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
Y₁ Y₂ : C
f : Y₂ ⟶ Y₁
Z : C
φ : Z ⟶ Y₂
i : I
g : Z ⟶ Y i
⊢ (ConcreteCategory.hom (F.map φ.op)) ((ConcreteCategory.hom (F.map f.op)) (s Y₁)) =
    (ConcreteCategory.hom (F.map f.op ≫ F.map φ.op)) (s Y₁)

Tactic:
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 : PreZeroHypercover S
inst✝ : E.HasPullbacks
⊢ E.toPreOneHypercover.HasPullbacks

Tactic:
by
  dsimp
  infer_instance

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

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
M✝ N P : SheafOfModules R
inst✝¹ : ∀ (X : C), HasWeakSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
q : M.LocalGeneratorsData
X Y : C
hY : Y ⟶ X
H : (Sieve.ofObjects q.X X).arrows hY
i : q.I
hi : Y ⟶ q.X i
⊢ q.X i = (fun i ↦ q.X (Exists.choose ⋯)) ⟨q.X i, ⋯⟩

Tactic:
grind

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀

Tactic:
rw [PreOneHypercover.sieve₁']
  congr
  ext <;> simp [PreOneHypercover.toPullback]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ S.arrows (Over.homMk (F.map g) ⋯)

Tactic:
convert! (Sieve.overEquiv_iff _ _).mp hg

Goal state after:
case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ F.map (g ≫ U.hom) = F.map g ≫ ((Over.post F).obj U).hom
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y
⊢ S ∈ (J.over X) Y ↔ (Sieve.overEquiv Y) S ∈ J Y.left

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
⊢ J.overMapPullback A f = J.overMapPullback A f

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
⊢ ∀ (j₁ j₂ : StructuredArrow Y F) (x : j₁ ⟶ j₂),
    (F ⋙ P).ιColimitType j₁.right ∘ ⇑(ConcreteCategory.hom (P.map j₁.hom)) =
      (F ⋙ P).ιColimitType j₂.right ∘ ⇑(ConcreteCategory.hom (P.map j₂.hom))

Tactic:
intro Z₁ Z₂ f

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
⊢ (F ⋙ P).ιColimitType Z₁.right ∘ ⇑(ConcreteCategory.hom (P.map Z₁.hom)) =
    (F ⋙ P).ιColimitType Z₂.right ∘ ⇑(ConcreteCategory.hom (P.map Z₂.hom))
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

Goal state before:
pp: 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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝ : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
M : SheafOfModules R
f : unit R ⟶ M
X : Cᵒᵖ
this : (ConcreteCategory.hom ((unitToPushforwardObjUnit φ).val.app X)) 1 = (ConcreteCategory.hom (φ.hom.app X)) 1
⊢ (ConcreteCategory.hom (f.val.app (Opposite.op (F.obj (Opposite.unop X))))) 1 =
    (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ.hom).map f.val).app X)) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
by_contra h
  have := isIso_of_epi_of_nonzero h
  exact w (eq_zero_of_mono_cokernel f)

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:
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:
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
x✝¹ : m✝ ≫ homOfLE ⋯ = s✝.fst
x✝ : m✝ ≫ homOfLE ⋯ = s✝.snd
⊢ m✝ = homOfLE ⋯

Tactic:
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:
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:
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
x✝¹ : homOfLE ⋯ ≫ m✝ = s✝.inl
x✝ : homOfLE ⋯ ≫ m✝ = s✝.inr
⊢ m✝ = homOfLE ⋯

Tactic:
rfl

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

Goal state before:
pp: X : TopCat
⊢ map (𝟙 X) = 𝟭 (Opens ↑X)

Tactic:
rfl

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
⊢ map f = map f

Tactic:
rfl

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

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

Tactic:
rfl

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
X : SheafOfModules R
U : Cᵒᵖ
⊢ RingCat.Hom.hom (φ.hom.app U) = RingCat.Hom.hom (φ.hom.app U)

Tactic:
rfl

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
X : SheafOfModules R
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ ((forget S).obj ((pushforward φ).obj X)).map x✝ ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map x✝))).map
        ((ModuleCat.restrictScalarsCongr ⋯).app
            (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝¹)).hom =
    ((ModuleCat.restrictScalarsCongr ⋯).app
          (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X.val).obj x✝²)).hom ≫
      ((forget S).obj ((pushforward φ).obj X)).map x✝

Tactic:
rfl

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
X✝ Y✝ : SheafOfModules R
x✝ : X✝ ⟶ Y✝
⊢ (pushforward φ).map x✝ ≫
      ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj Y✝.val).obj U))
            ⋯)).hom =
    ((fullyFaithfulForget S).preimageIso
          (PresheafOfModules.isoMk
            (fun U ↦
              (ModuleCat.restrictScalarsCongr ⋯).app
                (((PresheafOfModules.pushforward₀ F ((sheafToPresheaf K RingCat).obj R)).obj X✝.val).obj U))
            ⋯)).hom ≫
      (pushforward φ).map x✝

Tactic:
rfl

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
K' : GrothendieckTopology D'
K'' : GrothendieckTopology D''
G : D ⥤ D'
R' : Sheaf K' RingCat
inst✝³ : G.IsContinuous K K'
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R'
G' : D' ⥤ D''
R'' : Sheaf K'' RingCat
inst✝² : G'.IsContinuous K' K''
inst✝¹ : (G ⋙ G').IsContinuous K K''
inst✝ : (F ⋙ G).IsContinuous J K'
ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R''
x✝¹ : SheafOfModules R''
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫
                      pushforwardComp (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) ψ').hom.app
                x✝¹).val.app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                      isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                        pushforwardComp φ (ψ ≫ (G.sheafPushforwardContinuous RingCat K K').map ψ')).hom.app
                x✝¹).val.app
          X✝))
      x✝

Tactic:
rfl

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
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
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).val.app X✝))
      x✝

Tactic:
rfl

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
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
x✝¹ : SheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).val.obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).val.app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).val.app X✝))
      x✝

Tactic:
rfl

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

Tactic:
ext
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨⟨x, trivial, rfl⟩, hx⟩
  · rintro ⟨⟨x, -, rfl⟩, hx⟩
    exact ⟨x, hx, rfl⟩

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.inf f = Fintype.elems.inf f

Tactic:
rfl

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

Goal state before:
pp: α : Type u
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
ι : Type u
inst✝ : Fintype ι
f : ι → α
⊢ Finset.univ.sup f = Fintype.elems.sup f

Tactic:
rfl

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

Goal state before:
pp: 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
F : Presheaf C X
U V W : Opens ↑X
e₁ : U ≤ V
e₂ : V ≤ W
x : ToType (F.obj (op W))
⊢ (ConcreteCategory.hom (F.map ((homOfLE e₂).op ≫ (homOfLE e₁).op))) x = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) x

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
this :
  u.app j.left ≫ ((Opens.map f).op.leftKanExtensionUnit 𝒢).app j.left =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left)))
⊢ ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫ ((Opens.map f).op.lan.obj 𝒢).map j.hom =
    ((Opens.map f).op.leftKanExtensionUnit ℱ).app j.left ≫
      ((Opens.map f).op.lan.map u).app (op ((Opens.map f).obj (unop j.left))) ≫
        ((Opens.map f).op.leftKanExtension 𝒢).map j.hom

Tactic:
rfl

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
C : Type u'
inst✝¹ : Category.{v', u'} C
inst✝ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
x : C
U V : Cᵒᵖ
f : U ⟶ V
⊢ R.obj.map (f ≫ prod.snd.op) = R.obj.map (prod.snd ≫ f.unop).op

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) =
    ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)).ι.app
        j
⊢ ℱ.map
        (Limits.IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            j).left ≫
      u.app (op { carrier := ⇑(ConcreteCategory.hom f) '' ↑U, is_open' := ⋯ }) =
    ℱ.map
        (Limits.IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            j).left ≫
      u.app (op (hf.functor.obj U))

Tactic:
rfl

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

Goal state before:
pp: case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
⊢ U ≤ iSup (coveringOfPresieve U R)

Tactic:
intro x hxU

Goal state after:
case a
X : TopCat
U : Opens ↑X
R : Presieve U
hR : Sieve.generate R ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hxU : x ∈ U
⊢ x ∈ iSup (coveringOfPresieve U R)
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : TopCat
ι : Type u_1
B : ι → Opens ↑X
F : Presheaf C X
F' : Sheaf C X
h : Opens.IsBasis (Set.range B)
α : (inducedFunctor B).op ⋙ F ⟶ (inducedFunctor B).op ⋙ F'.obj
i : ι
⊢ ((restrictHomEquivHom F F' h) α).app (op (B i)) =
    ((restrictHomEquivHom F F' h).invFun ((restrictHomEquivHom F F' h).toFun α)).app (op i)

Tactic:
rfl

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

Goal state before:
pp: case single.pair.left
C : Type u_1
inst✝² : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
h : F.IsCompatible U sf
G : (CategoryTheory.Pairwise ι)ᵒᵖ ⥤ Type u_4 := (Pairwise.diagram U).op ⋙ F
i j' : ι
⊢ (ConcreteCategory.hom (((Pairwise.diagram U).op ⋙ F).map (op (Pairwise.Hom.left i j'))))
      (objPairwiseOfFamily sf (op (Pairwise.single i))) =
    objPairwiseOfFamily sf (op (Pairwise.pair i j'))

Tactic:
rfl

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

Goal state before:
pp: case e'_2.single
X : TopCat
F : Presheaf (Type u_4) X
ι : Type x
U : ι → Opens ↑X
s : (j : (CategoryTheory.Pairwise ι)ᵒᵖ) → ((Pairwise.diagram U).op ⋙ F).obj j
h :
  ∃! s_1,
    ∀ (i : (CategoryTheory.Pairwise ι)ᵒᵖ),
      (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app i)) s_1 =
        objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) i
hs : s ∈ ((Pairwise.diagram U).op ⋙ F).sections
e_1✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt = ToType (F.obj (op (iSup U)))
x✝ : (Functor.mapCone F (Pairwise.cocone U).op).pt
a✝ : (CategoryTheory.Pairwise ι)ᵒᵖ
i : ι
⊢ s (op (Pairwise.single i)) = objPairwiseOfFamily (fun i ↦ s (op (Pairwise.single i))) (op (Pairwise.single i))

Tactic:
rfl

Goal state after: