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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)

pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
V : C
iUV : V ⟶ r.Z
hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op)

Tactic:
·

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯) = G.map (r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    f
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
hab : a ≫ b = f
⊢ ((E.inter F).sieve₁ p₁ p₂).arrows f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
V : C
iUV : V ⟶ r.Z
hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op)

Tactic:
·

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
V : C
iUV : V ⟶ r.Z
hiUV : iUV ≫ r.g₁ ≫ l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯ = iUV ≫ r.g₂ ≫ l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₁.Y (unop g.2) U I₁.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₁.op) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iUV.op))
      ((f ≫ Y.obj.map (l I₂.Y (unop g.2) U I₂.f g.hom.unop ⋯).op) ≫ Y.obj.map r.g₂.op)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g₁ g₂ : StructuredArrow (op (G.obj U)) G.op
i : g₁ ⟶ g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map i ≫
      ⋯.amalgamate ⟨G.imageSieve g₂.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₂.2) U I.f g₂.hom.unop ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₁.2) U I.f g₁.hom.unop ⋯).op) ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
g₁ g₂ : StructuredArrow (op (G.obj U)) G.op
i : g₁ ⟶ g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map i ≫
      ⋯.amalgamate ⟨G.imageSieve g₂.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₂.2) U I.f g₂.hom.unop ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g₁.2) U I.f g₁.hom.unop ⋯).op) ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map i
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((a ≫ b) ≫ p₁) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₁ (k, l)) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((a ≫ b) ≫ p₁) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₁ (k, l)) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ b) ≫ p₂ = pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)

Tactic:
·

Goal state after:
case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ b) ≫ p₂ = pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((a ≫ b) ≫ p₂) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd)

Tactic:
·

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := ⋯
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.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 j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ ((a ≫ b) ≫ p₂) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd) =
    (pullback.lift (a ≫ e) u ⋯ ≫ (E.inter F).p₂ (k, l)) ≫
      pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
        (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case right
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
⊢ (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))
      ((G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c) =
    f

Tactic:
·

Goal state after:
case right
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj) :=
  { pt := X,
    π :=
      {
        app := fun g ↦
          ⋯.amalgamate ⟨G.imageSieve g.hom.unop, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y (unop g.2) U I.f g.hom.unop ⋯).op) ⋯,
        naturality := ⋯ } }
⊢ (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X)))
      ((G.op.isPointwiseRightKanExtensionRanCounit Y.obj (op (G.obj U))).lift c) =
    f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)

Tactic:
·

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)