mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
F' : C ⥤ B
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
h✝ : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : C ⥤ B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
x : A
⊢ (L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
          (L.associator F'' G).inv ≫ whiskerRight α' G).app
      x =
    ((L.associator F' G).inv ≫ whiskerRight α G).app x

Tactic:
;

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} A
inst✝³ : Category.{v_2, u_2} B
inst✝² : Category.{v_3, u_3} C
inst✝¹ : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
F' : C ⥤ B
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
h✝ : (F' ⋙ G).IsRightKanExtension ((L.associator F' G).inv ≫ whiskerRight α G)
F'' : C ⥤ B
α' : L ⋙ F'' ⟶ F
h : F''.IsRightKanExtension α'
x : A
⊢ (L.whiskerLeft (isoWhiskerRight (F'.rightKanExtensionUnique α F'' α') G).hom ≫
          (L.associator F'' G).inv ≫ whiskerRight α' G).app
      x =
    ((L.associator F' G).inv ≫ whiskerRight α G).app x
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.HasIsos
x✝¹ : C
x✝ : Sieve x✝¹
⊢ x✝ ∈ (toPretopology C J).toGrothendieck x✝¹ ↔ x✝ ∈ J.toGrothendieck x✝¹

Tactic:
exact J.mem_toGrothendieck_iff_of_isStableUnderComposition.symm

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

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.ofArrows P p₁ ∈ J Y

Tactic:
Sieve.ofArrows_eq_pullback_of_isPullback _ h

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.pullback g (Sieve.ofArrows X f) ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F'.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F'.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
⊢ f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j =
    g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j

Tactic:
apply hF.hom_ext ⟨_, G.cover_lift J K (K.pullback_stable j.hom.unop S.2)⟩

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
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
W : A
f g : W ⟶ R.obj (op X)
h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op
j : StructuredArrow (op X) G.op
⊢ ∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩),
    (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op =
      (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ ⊤.arrows g

Tactic:
;

Goal state after:
C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
U V : C
f : U ⟶ V
W : C
g : W ⟶ U
⊢ (G.imageSieve (G.map f)).arrows g ↔ ⊤.arrows g
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y✝ : C
f✝ : Y✝ ⟶ U
⊢ (equalizer f f).arrows f✝ ↔ ⊤.arrows f✝

Tactic:
;

Goal state after:
C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y✝ : C
f✝ : Y✝ ⟶ U
⊢ (equalizer f f).arrows f✝ ↔ ⊤.arrows f✝
Module: Mathlib.CategoryTheory.Sites.LocallyFullyFaithful

Goal state before:
pp: C : Type uC
inst✝³ : Category.{vC, uC} C
D : Type uD
inst✝² : Category.{vD, uD} D
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Faithful
U✝ V✝ : C
f₁ : U✝ ⟶ V✝
e : G.map f₁ = G.map f₁
⊢ Sieve.functorPushforward G (Sieve.equalizer f₁ f₁) ∈ K (G.obj U✝)

Tactic:
;

Goal state after:
C : Type uC
inst✝³ : Category.{vC, uC} C
D : Type uD
inst✝² : Category.{vD, uD} D
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Faithful
U✝ V✝ : C
f₁ : U✝ ⟶ V✝
e : G.map f₁ = G.map f₁
⊢ Sieve.functorPushforward G (Sieve.equalizer f₁ f₁) ∈ K (G.obj U✝)
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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈
    K W

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iWZ
      (Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T)))) ∈
    K W
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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)

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
K : GrothendieckTopology D
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : C
T : ↑(K (G.obj X))
Y : D
iYX : Y ⟶ G.obj X
hiYX : (↑T).arrows iYX
W : D
Z : C
iWZ : W ⟶ G.obj Z
iZY : G.obj Z ⟶ Y
⊢ Sieve.pullback iZY (Sieve.pullback iYX (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))) ∈ K (G.obj Z)
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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x✝ : (G.op ⋙ ℱ).obj (op Y)
⊢ (ConcreteCategory.hom (α.app (op Y) ≫ ℱ'.obj.map i.op)).toFun x✝ =
    (ConcreteCategory.hom (ℱ.map i.op ≫ α.app (op X))).toFun x✝

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
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝ : G.IsLocallyFull K
X Y : C
i : G.obj X ⟶ G.obj Y
x✝ : (G.op ⋙ ℱ).obj (op Y)
⊢ (ConcreteCategory.hom (α.app (op Y) ≫ ℱ'.obj.map i.op)).toFun x✝ =
    (ConcreteCategory.hom (ℱ.map i.op ≫ α.app (op X))).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S W : C
p : W ⟶ S
Y✝ : C
f✝ : Y✝ ⟶ W
⊢ ((trivial S).sieve₁ p p).arrows f✝ ↔ ⊤.arrows f✝

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S W : C
p : W ⟶ S
Y✝ : C
f✝ : Y✝ ⟶ W
⊢ ((trivial S).sieve₁ p p).arrows f✝ ↔ ⊤.arrows 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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
⊢ ∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ unop Y),
    (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (ℱ.map f ≫ appHom α (unop Y))).toFun x) =
      (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (appHom α (unop X) ≫ ℱ'.obj.map f)).toFun x)

Tactic:
intro Y' f'

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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ (ConcreteCategory.hom (ℱ'.obj.map f'.op)) ((ConcreteCategory.hom (ℱ.map f ≫ appHom α (unop Y))).toFun x) =
    (ConcreteCategory.hom (ℱ'.obj.map f'.op)) ((ConcreteCategory.hom (appHom α (unop X) ≫ ℱ'.obj.map f)).toFun x)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₁ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g))) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₂ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g)))

Tactic:
have := congr($e ≫ Y.1.map iVU.op)

Goal state after:
case left
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₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
this :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ ≫ Y.obj.map iVU.op =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂ ≫ Y.obj.map iVU.op
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₁ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g))) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₂ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g)))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
⊢ (x✝ ≫ α.app X) ≫ ℱ'.obj.map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((x✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (G.obj (Nonempty.some hf).1))) ≫
      ℱ'.obj.map (Nonempty.some hf).lift.op

Tactic:
;

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
⊢ (x✝ ≫ α.app X) ≫ ℱ'.obj.map ((Nonempty.some hf).map.op ≫ (Nonempty.some hf).lift.op) =
    ((x✝ ≫ ℱ.map (Nonempty.some hf).map.op) ≫ α.app (op (G.obj (Nonempty.some hf).1))) ≫
      ℱ'.obj.map (Nonempty.some hf).lift.op
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝² E✝¹ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E✝.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq ⋯ ⋯) k) = E.Y k

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝² E✝¹ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E✝.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq ⋯ ⋯) k) = E.Y k
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯) k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯) k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), Presieve.IsSheaf J (yoneda.obj X)
X : C
⊢ Presieve.IsSheaf J (yoneda.obj X)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
h : ∀ (X : C), Presieve.IsSheaf J (yoneda.obj X)
X : C
⊢ Presieve.IsSheaf J (yoneda.obj X)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
k✝ : E.I₁ i j
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝ E : PreOneHypercover S
F : PreOneHypercover S
G : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
i j : E.I₀
k✝ : E.I₁ i j
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
x✝ : E.I₀
⊢ ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
          let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
            h₁ := fun {i j} k ↦
              (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
            w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
x✝ : E.I₀
⊢ ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
          let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
          { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
            h₁ := fun {i j} k ↦
              (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
            w₁₁ := ⋯, w₁₂ := ⋯ }).s₀
      x✝ =
    (𝟙 E).s₀ x✝