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

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

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g → ((overEquiv ((Over.map f).obj Z)).symm S).arrows g

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : Over X
S : Sieve Z.left
W : Over Y
g : W ⟶ (Over.map f).obj Z
⊢ ((overEquiv ((Over.map f).obj Z)).symm S).arrows g → (functorPushforward (Over.map f) ((overEquiv Z).symm S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: 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:
constructor

Goal state after:
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

case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y : C
f : Y ⟶ X
⊢ (↑S).arrows f → S.preOneHypercover.sieve₀.arrows f
Module: Mathlib.CategoryTheory.Sites.Over

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

Tactic:
ext

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

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

Tactic:
ext

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

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

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ Over.Hom.left (Over.homMk (𝟙 Z) ⋯ ≫ u) = Over.Hom.left (𝟙 (Over.mk (g ≫ U.hom ≫ f)))
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
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso (G.map F η).π

Tactic:
GeneratingSections.map_π_eq

Goal state after:
C : Type u'
inst✝⁷ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝⁶ : HasWeakSheafify J AddCommGrpCat
inst✝⁵ : J.WEqualsLocallyBijective AddCommGrpCat
M✝ N P : SheafOfModules R
C' : Type u₁
inst✝⁴ : Category.{v₁, u₁} C'
J' : GrothendieckTopology C'
S : Sheaf J' RingCat
inst✝³ : HasSheafify J' AddCommGrpCat
inst✝² : J'.WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
G : M.GeneratingSections
F : SheafOfModules R ⥤ SheafOfModules S
inst✝¹ : PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v', max (max (u + 1) u₁) v₁} F
η : unit S ≅ F.obj (unit R)
inst✝ : IsIso G.π
⊢ IsIso ((mapFreeIso F G.I η).hom ≫ F.map G.π)
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₀
⊢ (fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).f

Tactic:
ext

Goal state after:
case h₀
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₀
x✝ : (E.refineOneHypercover F).I₁ i j
⊢ (E.refineOneHypercover F).toPullback x✝ ≫
      pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j) =
    (F i j).f x✝ ≫ pullback.fst ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)

case h₁
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₀
x✝ : (E.refineOneHypercover F).I₁ i j
⊢ (E.refineOneHypercover F).toPullback x✝ ≫
      pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j) =
    (F i j).f x✝ ≫ pullback.snd ((E.refineOneHypercover F).f i) ((E.refineOneHypercover F).f j)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
W' : Over X := Over.mk (f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk f₁ ⋯
g₂' : W' ⟶ Y₂ := Over.homMk f₂ ⋯
⊢ g₁' ≫ g₁ = g₂' ≫ g₂

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
x✝² : Sheaf J (Type u_1)
Z : Over X
x✝¹ : Presieve Z
x✝ : Presieve.FamilyOfElements ((Over.forget X).op ⋙ x✝².obj) x✝¹
hx : x✝.Compatible
Y₁ Y₂ : Over X
W : C
f₁ : W ⟶ (Over.forget X).obj Y₁
f₂ : W ⟶ (Over.forget X).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝¹ g₁
hg₂ : x✝¹ g₂
h : f₁ ≫ (Over.forget X).map g₁ = f₂ ≫ (Over.forget X).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: 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) ⋯
⊢ g₁' ≫ g₁ = g₂' ≫ g₂

Tactic:
ext

Goal state after:
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 := ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)
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) ⋯
⊢ f₁ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)

Tactic:
ext

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 := ⋯
⊢ Over.Hom.left f₁ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯))
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) ⋯
⊢ f₂ = (Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)

Tactic:
ext

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 := ⋯
⊢ Over.Hom.left f₂ =
    Over.Hom.left ((Over.isoMk (Iso.refl W.left) ⋯).inv ≫ (Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
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₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W

Tactic:
intro i₁

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
i₁ : E.I₀
⊢ ∀ (i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
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:
ext

Goal state after:
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.Hom.left (Over.homMk p₁ ⋯ ≫ E.f i₁) = Over.Hom.left (Over.homMk p₂ ⋯ ≫ E.f i₂)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W

Tactic:
intro i₁

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
i₁ : E.I₀
⊢ ∀ (i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
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.overMapPullbackComp A f (𝟙 Y)).inv ≫
      Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f) ≫
        (J.overMapPullback A f).leftUnitor.hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
ext

Goal state after:
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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A f (𝟙 Y)).inv ≫
                Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f) ≫
                  (J.overMapPullback A f).leftUnitor.hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝
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.overMapPullbackComp A (𝟙 X) f).inv ≫
      (J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom ≫ (J.overMapPullback A f).rightUnitor.hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
ext

Goal state after:
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
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A (𝟙 X) f).inv ≫
                (J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom ≫
                  (J.overMapPullback A f).rightUnitor.hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝
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 Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
⊢ (J.overMapPullbackComp A f (g ≫ h)).inv ≫
      Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f) ≫
        ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom ≫
          (J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom ≫
            (J.overMapPullbackComp A (f ≫ g) h).hom =
    (J.overMapPullbackCongr A ⋯).hom

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ (((J.overMapPullbackComp A f (g ≫ h)).inv ≫
                Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f) ≫
                  ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom ≫
                    (J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom ≫
                      (J.overMapPullbackComp A (f ≫ g) h).hom).app
            x✝¹).hom.app
      x✝ =
    ((J.overMapPullbackCongr A ⋯).hom.app x✝¹).hom.app x✝
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) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
⊢ φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f)) = φ Y₁

Tactic:
ext

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) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
⊢ (φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ = φ Y₁ x✝
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
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (unit S).val.map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map f))).map
        (ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app Y✝)) ⋯) =
    ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app X✝)) ⋯ ≫ ((pushforward φ).obj (unit R)).val.map f

Tactic:
ext

Goal state after:
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✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ (ModuleCat.Hom.hom
        ((unit S).val.map f ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom (S.obj.map f))).map
            (ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app Y✝)) ⋯)))
      1 =
    (ModuleCat.Hom.hom
        (ModuleCat.homMk ((forget₂ RingCat AddCommGrpCat).map (φ.hom.app X✝)) ⋯ ≫
          ((pushforward φ).obj (unit R)).val.map f))
      1
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f → f ≠ 0

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X

Tactic:
constructor

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0

case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝ : Set (Opens ↑Y)
⊢ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝), is_open' := ⋯ } =
    sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝)

Tactic:
ext

Goal state after:
X Y Z : TopCat
U V W : Opens ↑X
f : X ⟶ Y
x✝¹ : Set (Opens ↑Y)
x✝ : ↑X
⊢ x✝ ∈ ↑{ carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑(sSup x✝¹), is_open' := ⋯ } ↔
    x✝ ∈ ↑(sSup ((fun U ↦ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' ↑U, is_open' := ⋯ }) '' x✝¹))
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
⊢ (map f).obj (iSup U) = iSup ((map f).obj ∘ U)

Tactic:
ext

Goal state after:
X Y : TopCat
f : X ⟶ Y
ι : Type u_1
U : ι → Opens ↑Y
x✝ : ↑X
⊢ x✝ ∈ ↑((map f).obj (iSup U)) ↔ x✝ ∈ ↑(iSup ((map f).obj ∘ U))
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
U : Set ↑X
hU : IsOpen U
hx : x ∈ { carrier := U, is_open' := hU }
⊢ x ∈ (Opens.map f).obj (hf.functorObj { carrier := U, is_open' := hU })

Tactic:
obtain ⟨t, ht, rfl⟩ := hf.isOpen_iff.mp hU

Goal state after:
case a
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
x : ↑X
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
hx : x ∈ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
⊢ x ∈ (Opens.map f).obj (hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU })
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 ∈ U

Tactic:
conv_rhs => rw [← hf.map_functorObj U]
  rfl

Goal state after: