mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
⊢ (Discrete.natTrans fun i ↦ (s i.as).snd) ≫ a.ι =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯).ι ≫
      (const (Discrete ι)).map t.snd

Tactic:
ext

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯ := Cofan.ext e ⋯
x✝ : Discrete ι
⊢ ((Discrete.natTrans fun i ↦ (s i.as).snd) ≫ a.ι).app x✝ =
    ((Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯).ι ≫
          (const (Discrete ι)).map t.snd).app
      x✝
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
⊢ (Discrete.natTrans fun i ↦ (s i.as).fst) ≫ a.ι =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).ι ≫
      (const (Discrete ι)).map t.fst

Tactic:
ext

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
x✝ : Discrete ι
⊢ ((Discrete.natTrans fun i ↦ (s i.as).fst) ≫ a.ι).app x✝ =
    ((Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).ι ≫
          (const (Discrete ι)).map t.fst).app
      x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
s : Cocone (K ⋙ sigmaConst.obj R)
j✝ j'✝ : J
g : j✝ ⟶ j'✝
⊢ (fun k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j'✝) ∘ ⇑(ConcreteCategory.hom (K.map g)) = fun k ↦
    Sigma.ι (fun x ↦ R) k ≫ s.ι.app j✝

Tactic:
ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝¹ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
s : Cocone (K ⋙ sigmaConst.obj R)
j✝ j'✝ : J
g : j✝ ⟶ j'✝
x✝ : (fun X ↦ X) (K.obj j✝)
⊢ ((fun k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j'✝) ∘ ⇑(ConcreteCategory.hom (K.map g))) x✝ =
    Sigma.ι (fun x ↦ R) x✝ ≫ s.ι.app j✝
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
⊢ ((Sigma.map' f fun x ↦ 𝟙 R) ≫ Sigma.desc fun b ↦ if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun x ↦ R) ⟨b, hb⟩ else 0) =
    0

Tactic:
ext

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
b✝ : α
⊢ (Sigma.ι (fun x ↦ R) b✝ ≫
      (Sigma.map' f fun x ↦ 𝟙 R) ≫
        Sigma.desc fun b ↦ if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun x ↦ R) ⟨b, hb⟩ else 0) =
    Sigma.ι (fun x ↦ R) b✝ ≫ 0
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

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 : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
⊢ N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) = N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i))

Tactic:
ext

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 : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
x✝ : I
X✝ : Cᵒᵖ
⊢ ↑(N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) x✝) X✝ =
    ↑(N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i)) x✝) X✝
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)
⊢ smul α φ (r * r') m = smul α φ r (smul α φ r' m)

Tactic:
by
  let S := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve α r' ⊓ Presheaf.imageSieve φ m
  have hS : S ∈ J X.unop := by
    refine J.intersection_covering (J.intersection_covering ?_ ?_) ?_
    all_goals apply Presheaf.imageSieve_mem
  apply A.isSeparated _ _ hS
  rintro Y f ⟨⟨⟨r₀ : R₀.obj _, (hr₀ : (α.app (Opposite.op Y)) r₀ = (R.obj.map f.op) r)⟩,
    ⟨r₀' : R₀.obj _, (hr₀' : (α.app (Opposite.op Y)) r₀' = (R.obj.map f.op) r')⟩⟩,
    ⟨m₀ : M₀.obj _, hm₀⟩⟩
  rw [map_smul_eq α φ (r * r') m f.op (r₀ * r₀')
    (by rw [map_mul, map_mul, hr₀, hr₀']) m₀ hm₀, mul_smul,
    map_smul_eq α φ r (smul α φ r' m) f.op r₀ hr₀ (r₀' • m₀)
      (map_smul_eq α φ r' m f.op r₀' hr₀' m₀ hm₀).symm]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ J₁.close S = ⊤ ↔ S ∈ J₁ X

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ J₁.close S = ⊤ → S ∈ J₁ X

case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
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
⊢ M ⊓ S = N ⊓ S

Tactic:
ext

Goal state after:
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
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (M ⊓ S).arrows f✝ ↔ (N ⊓ S).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1
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
⊢ J₁.Covers M f ↔ J₁.Covers N f

Tactic:
constructor

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
⊢ J₁.Covers M f → J₁.Covers N f

case refine_1.mpr
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
⊢ J₁.Covers N f → J₁.Covers M f
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1.mpr
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 N f
⊢ Sieve.pullback f (M ⊓ ?m.197) ∈ 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 N f
⊢ Sieve X

Tactic:
rw [MSNS]

Goal state after:
case refine_1.mpr
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 N f
⊢ Sieve.pullback f (N ⊓ S) ∈ J₁ Y
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) PreservesLimitsOfShape.preservesLimit._autoParam
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ → ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
        { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).s₀ =
    (𝟙 E).s₀

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : E.I₀
⊢ ({ s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
⊢ ({ s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ } ≫
        { s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ }).s₀ =
    (𝟙 F).s₀

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S✝ T : C
E✝¹ : PreZeroHypercover S✝
F✝¹ : PreZeroHypercover S✝
E✝ : PreZeroHypercover S✝
F✝ : PreZeroHypercover S✝
G : PreZeroHypercover S✝
S : C
E F : PreZeroHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
x✝ : F.I₀
⊢ ({ s₀ := ⇑s₀.symm, h₀ := fun i ↦ eqToHom ⋯ ≫ (h₀ (s₀.symm i)).inv, w₀ := ⋯ } ≫
          { s₀ := ⇑s₀, h₀ := fun i ↦ (h₀ i).hom, w₀ := ⋯ }).s₀
      x✝ =
    (𝟙 F).s₀ x✝
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

Tactic:
constructor

Goal state after:
case mp
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows

case mpr
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    Presieve.IsSheaf J.toGrothendieck P
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A : StructuredArrow Y.right F
this✝ : Nonempty (StructuredArrow X (F ⋙ G))
this : IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G))
⊢ IsCofiltered (StructuredArrow X (F ⋙ G))

Tactic:
constructor

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := IsCofiltered.eq (T.map f) (T.map g)
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g)))
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f))
f' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right f) ⋯
g' : A' ⟶ B' := StructuredArrow.homMk (StructuredArrow.Hom.right g) ⋯
⊢ StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f =
    StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g

Tactic:
ext

Goal state after:
case refine_2.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := ⋯
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
f g : A ⟶ B
U : StructuredArrow X G := ⋯
A' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F := ⋯
B' : StructuredArrow (IsCofiltered.eq (T.map f) (T.map g)).right F := ⋯
f' : A' ⟶ B' := ⋯
g' : A' ⟶ B' := ⋯
⊢ StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ f) =
    StructuredArrow.Hom.right (StructuredArrow.homMk (StructuredArrow.Hom.right (IsCofiltered.eqHom f' g')) ⋯ ≫ g)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S ↔ K.Saturate X S

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S → K.Saturate X S

case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S → K.Saturate X S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
⊢ K.toGrothendieck.sieves = fun X ↦ Set.ofPred (K.Saturate X)

Tactic:
ext

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
x✝¹ : C
x✝ : Sieve x✝¹
⊢ x✝ ∈ K.toGrothendieck.sieves x✝¹ ↔ x✝ ∈ Set.ofPred (K.Saturate x✝¹)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J ↔ K ≤ J.toCoverage

Tactic:
constructor

Goal state after:
case mp
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K.toGrothendieck ≤ J → K ≤ J.toCoverage

case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

Tactic:
constructor

Goal state after:
case mp
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows) →
    ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R

case mpr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) →
    ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ K.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case inr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R

Tactic:
exact h.2 R hR

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P