mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

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

Tactic:
simpa using

Goal state after:
case left
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ c.π.app Y = c.π.app X ≫ (F.map f).left
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
⊢ PreservesFiniteLimits colim

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v₂}

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
⊢ ∀ (J : Type v₂) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J colim
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
simpa using

Goal state after:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ f.h₁ k ≫ E.p₁ (f.s₁ k) = G.p₁ k ≫ f.h₀ i✝
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Presieve Y
h :
  { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      a✝ ≤
    { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      b✝
⊢ a✝ ≤ b✝

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Presieve Y
h :
  { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      a✝ ≤
    { toFun := fun S ↦ map (Over.forget X) S, invFun := fun S' ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
        right_inv := ⋯ }
      b✝
⊢ a✝ ≤ b✝
Module: Mathlib.CategoryTheory.Sites.Over

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

Tactic:
rw [Equiv.coe_fn_mk]

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

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
a✝ b✝ : Sieve Y
h : functorPushforward (Over.forget X) a✝ ≤ functorPushforward (Over.forget X) b✝
⊢ a✝ ≤ b✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
simpa using

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ g.h₁ k ≫ F.p₁ (g.s₁ k) = G.p₁ k ≫ g.h₀ i✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
simpa using

Goal state after:
case h₀
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ f.h₁ k ≫ E.p₂ (f.s₁ k) = G.p₂ k ≫ f.h₀ j✝
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.obj
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ (f ≫ c.π.app Z) ≫ F.obj.map { Y := W, f := a, hf := ⋯ }.f.op =
    (g ≫ c.π.app Z) ≫ F.obj.map { Y := W, f := a, hf := ⋯ }.f.op

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J A
c : Cone F.obj
hc : IsLimit c
X : A
f g : X ⟶ c.pt
h : ∀ (i : I), f ≫ c.π.app (Opposite.op (Y i)) = g ≫ c.π.app (Opposite.op (Y i))
Z : Cᵒᵖ
W : C
a : W ⟶ Opposite.unop Z
i : I
b : W ⟶ Y i
⊢ f ≫ c.π.app (Opposite.op W) = g ≫ c.π.app (Opposite.op W)
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
T : C
a : T ⟶ Opposite.unop W
i : I
b : T ⟶ Y i
⊢ (ConcreteCategory.hom (F.obj.map a.op)) (↑x W) = (ConcreteCategory.hom (F.obj.map a.op)) (↑y W)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
I : Type u_1
Y : I → C
hY : J.CoversTop Y
F : Sheaf J (Type u_2)
x y : ↑F.obj.sections
h : ∀ (i : I), ↑x (Opposite.op (Y i)) = ↑y (Opposite.op (Y i))
W : Cᵒᵖ
T : C
a : T ⟶ Opposite.unop W
i : I
b : T ⟶ Y i
⊢ ↑x (Opposite.op T) = ↑y (Opposite.op T)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
simpa using

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ g.h₁ k ≫ F.p₂ (g.s₁ k) = G.p₂ k ≫ g.h₀ j✝
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 Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
a✝ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
    (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ ⋯)

Tactic:
simpa using

Goal state after:
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 Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
a✝ : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (F.map g₁.op)) ((ConcreteCategory.hom (F.map φ₁.op)) (x i₁)) =
    (ConcreteCategory.hom (F.map g₂.op)) ((ConcreteCategory.hom (F.map φ₂.op)) (x i₂))
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₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ b ≫ (E.Y k).hom = (Over.mk (f✝ ≫ W.hom)).hom

Tactic:
simpa using

Goal state after:
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₂
Y✝ : C
f✝ : Y✝ ⟶ W.left
k : (E.map (Over.forget X)).I₁ i₁ i₂
b : Y✝ ⟶ (E.map (Over.forget X)).Y k
hb₁ : f✝ ≫ Over.Hom.left p₁ = b ≫ (E.map (Over.forget X)).p₁ k
hb₂ : f✝ ≫ Over.Hom.left p₂ = b ≫ (E.map (Over.forget X)).p₂ k
⊢ b ≫ (E.Y k).hom = f✝ ≫ W.hom
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
hg : ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
⊢ 𝟙 W.left ≫ ((Over.map f).obj (Over.mk (Over.Hom.left g ≫ Z.hom))).hom = W.hom

Tactic:
simpa using

Goal state after:
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
hg : ((overEquiv ((Over.map f).obj Z)).symm S).arrows g
⊢ Over.Hom.left g ≫ Z.hom ≫ f = W.hom
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:
rw [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.Over

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

Tactic:
simpa using

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
Y : Over X
S : Sieve Y.left
hS : S ∈ J Y.left
⊢ S ∈ J Y.left
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree

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
I : Type u
⊢ IsIso (free.generatingSections I).π

Tactic:
rw [free.generatingSections_π]
  infer_instance

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 : C
f : Over X
⊢ ∀ {X_1 : Over f.left} {S : Sieve X_1},
    Sieve.functorPushforward f.iteratedSliceEquiv.inverse S ∈
        ((J.over X).over f) (f.iteratedSliceEquiv.inverse.obj X_1) ↔
      S ∈ (J.over f.left) X_1

Tactic:
simp [GrothendieckTopology.mem_over_iff, Sieve.overEquiv,
      ← Over.iteratedSliceBackward_forget_forget f, Sieve.functorPushforward_comp]

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.Initial
⊢ Function.Bijective F.sectionsPrecomp

Tactic:
refine ⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩

Goal state after:
case refine_1
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.Initial
s₁ s₂ : ↑P.sections
h : F.sectionsPrecomp s₁ = F.sectionsPrecomp s₂
⊢ s₁ = s₂

case refine_2
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.Initial
t : ↑(F ⋙ P).sections
⊢ ∃ a, F.sectionsPrecomp a = t
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_2
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.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
X : C
⊢ ↑(F.sectionsPrecomp ⟨val, ⋯⟩) X = ↑t X

Tactic:
simpa using

Goal state after:
case refine_2.refine_2
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.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
X : C
⊢ val (F.obj X) = ↑t 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✝
⊢ (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

Tactic:
exact ConcreteCategory.congr_hom (φ.hom.naturality f) _

Goal state after:
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
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ f = 0

Tactic:
simpa using

Goal state after:
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
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ f = 0
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
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0

Tactic:
by_contra h
  exact w (isIso_of_mono_of_nonzero h)

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬IsZero X

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬𝟙 X = 0
Module: Mathlib.CategoryTheory.Simple

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

Tactic:
simpa using

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 0 ≫ biprod.snd
⊢ IsZero Y
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ).map
      (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
        ((CostructuredArrow.map (homOfLE le).op).obj j)) =
    (coconeOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ)).ι.app
        j ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
Limits.coconeOfDiagramTerminal_ι_app

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
            (op U)).ι.app
      ((CostructuredArrow.map (homOfLE le).op).obj j)
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ).map
      (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
        ((CostructuredArrow.map (homOfLE le).op).obj j)) =
    (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ).map
        (IsTerminal.from { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ } j) ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ Nonempty (StructuredArrow U (Opens.map f))

Tactic:
· exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

Goal state after: