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

Goal state before:
pp: case left
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.left ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

pp: case right
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.right ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

pp: case diagram
J : Type u₁
inst✝ : Fintype J
val✝ : J
⊢ Bicone.diagram val✝ ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

Tactic:
<;>

Goal state after:
case left
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.left ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

case right
J : Type u₁
inst✝ : Fintype J
⊢ Bicone.right ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems

case diagram
J : Type u₁
inst✝ : Fintype J
val✝ : J
⊢ Bicone.diagram val✝ ∈ [Bicone.left, Bicone.right].toFinset ∪ Finset.image Bicone.diagram Fintype.elems
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.left Bicone.left
⊢ Decidable (left_id = g)

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.right Bicone.right
⊢ Decidable (right_id = g)

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.left (Bicone.diagram j✝)
⊢ Decidable (left j✝ = g)

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.right (Bicone.diagram j✝)
⊢ Decidable (right j✝ = g)

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram j✝) (Bicone.diagram k✝)
⊢ Decidable (diagram f✝ = g)

Tactic:
<;>

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.left Bicone.left
⊢ Decidable (left_id = g)

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
g : BiconeHom J Bicone.right Bicone.right
⊢ Decidable (right_id = g)

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.left (Bicone.diagram j✝)
⊢ Decidable (left j✝ = g)

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
g : BiconeHom J Bicone.right (Bicone.diagram j✝)
⊢ Decidable (right j✝ = g)

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram j✝) (Bicone.diagram k✝)
⊢ Decidable (diagram f✝ = g)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)

pp: case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)

pp: case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)

pp: case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)

pp: case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)

Tactic:
<;>

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)

case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)

case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)

case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)

case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True

pp: case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True

pp: case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True

pp: case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True

pp: case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (f✝¹ = f✝)

Tactic:
<;>

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True

case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True

case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True

case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True

case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (f✝¹ = f✝)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left_id = BiconeHom.left_id

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right_id = BiconeHom.right_id

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left j✝ = BiconeHom.left j✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right j✝ = BiconeHom.right j✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ 𝟙 (Bicone.diagram j✝) ≫ BiconeHom.diagram f✝ = BiconeHom.diagram f✝

Tactic:
<;>

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left_id = BiconeHom.left_id

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right_id = BiconeHom.right_id

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.left ≫ BiconeHom.left j✝ = BiconeHom.left j✝

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ 𝟙 Bicone.right ≫ BiconeHom.right j✝ = BiconeHom.right j✝

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ 𝟙 (Bicone.diagram j✝) ≫ BiconeHom.diagram f✝ = BiconeHom.diagram f✝
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.left_id ≫ 𝟙 Bicone.left = BiconeHom.left_id

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.right_id ≫ 𝟙 Bicone.right = BiconeHom.right_id

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.left j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.left j✝

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.right j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.right j✝

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom.diagram f✝ ≫ 𝟙 (Bicone.diagram k✝) = BiconeHom.diagram f✝

Tactic:
<;>

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.left_id ≫ 𝟙 Bicone.left = BiconeHom.left_id

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ BiconeHom.right_id ≫ 𝟙 Bicone.right = BiconeHom.right_id

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.left j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.left j✝

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ BiconeHom.right j✝ ≫ 𝟙 (Bicone.diagram j✝) = BiconeHom.right j✝

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
⊢ BiconeHom.diagram f✝ ≫ 𝟙 (Bicone.diagram k✝) = BiconeHom.diagram f✝
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.left ⟶ Y✝
⊢ (BiconeHom.left_id ≫ g) ≫ h = BiconeHom.left_id ≫ g ≫ h

pp: case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.right ⟶ Y✝
⊢ (BiconeHom.right_id ≫ g) ≫ h = BiconeHom.right_id ≫ g ≫ h

pp: case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.left j✝ ≫ g) ≫ h = BiconeHom.left j✝ ≫ g ≫ h

pp: case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.right j✝ ≫ g) ≫ h = BiconeHom.right j✝ ≫ g ≫ h

pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Y✝
⊢ (BiconeHom.diagram f✝ ≫ g) ≫ h = BiconeHom.diagram f✝ ≫ g ≫ h

Tactic:
<;>

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.left ⟶ Y✝
⊢ (BiconeHom.left_id ≫ g) ≫ h = BiconeHom.left_id ≫ g ≫ h

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
g : Bicone.right ⟶ Y✝
⊢ (BiconeHom.right_id ≫ g) ≫ h = BiconeHom.right_id ≫ g ≫ h

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.left j✝ ≫ g) ≫ h = BiconeHom.left j✝ ≫ g ≫ h

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ : J
g : Bicone.diagram j✝ ⟶ Y✝
⊢ (BiconeHom.right j✝ ≫ g) ≫ h = BiconeHom.right j✝ ≫ g ≫ h

case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Y✝ Z✝ : Bicone J
h : Y✝ ⟶ Z✝
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
g : Bicone.diagram k✝ ⟶ Y✝
⊢ (BiconeHom.diagram f✝ ≫ g) ≫ h = BiconeHom.diagram f✝ ≫ g ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.left ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h = BiconeHom.left_id ≫ BiconeHom.left_id ≫ h

pp: case left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ h = BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ h

pp: case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.right ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h = BiconeHom.right_id ≫ BiconeHom.right_id ≫ h

pp: case right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ h = BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ h

pp: case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.left j✝ ≫ BiconeHom.diagram f✝ ≫ h

pp: case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.right j✝ ≫ BiconeHom.diagram f✝ ≫ h

pp: case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝ ≫ h

Tactic:
<;>

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.left ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left_id) ≫ h = BiconeHom.left_id ≫ BiconeHom.left_id ≫ h

case left_id.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.left_id ≫ BiconeHom.left j✝) ≫ h = BiconeHom.left_id ≫ BiconeHom.left j✝ ≫ h

case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
h : Bicone.right ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right_id) ≫ h = BiconeHom.right_id ≫ BiconeHom.right_id ≫ h

case right_id.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
h : Bicone.diagram j✝ ⟶ Z✝
⊢ (BiconeHom.right_id ≫ BiconeHom.right j✝) ≫ h = BiconeHom.right_id ≫ BiconeHom.right j✝ ≫ h

case left.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.left j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.left j✝ ≫ BiconeHom.diagram f✝ ≫ h

case right.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f✝ : j✝ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.right j✝ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.right j✝ ≫ BiconeHom.diagram f✝ ≫ h

case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝¹ : J
f✝¹ : j✝ ⟶ k✝¹
k✝ : J
f✝ : k✝¹ ⟶ k✝
h : Bicone.diagram k✝ ⟶ Z✝
⊢ (BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝) ≫ h = BiconeHom.diagram f✝¹ ≫ BiconeHom.diagram f✝ ≫ h
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.left ⟶ k)

pp: case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.right ⟶ k)

pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ k)

Tactic:
<;>

Goal state after:
case left
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.left ⟶ k)

case right
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
⊢ Fintype (Bicone.right ⟶ k)

case diagram
J : Type v₁
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
k : Bicone J
val✝ : J
⊢ Fintype (Bicone.diagram val✝ ⟶ k)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S := ⋯
F : PreZeroHypercover S := ⋯
e : E ≅ F := ⋯
hER : E.presieve₀ = R
hFT : F.presieve₀ = T
⊢ E.presieve₀ ∈ J.coverings S

Tactic:
rwa [hER]

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

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

pp: 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

Tactic:
<;>

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: case mp.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Presieve X✝
hS✝ : S✝ ∈ K.coverings X✝
⊢ K.Saturate X✝ (Sieve.generate S✝)

pp: case mp.top
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
⊢ K.Saturate X✝ ⊤

pp: case mp.transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
R✝ S✝ : Sieve X✝
a✝¹ : K.Saturate X✝ R✝
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, R✝.arrows f → K.Saturate Y (Sieve.pullback f S✝)
a_ih✝¹ : K.Saturate X✝ R✝
a_ih✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, R✝.arrows f → K.Saturate Y (Sieve.pullback f S✝)
⊢ K.Saturate X✝ S✝

Tactic:
<;>

Goal state after:
case mp.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Presieve X✝
hS✝ : S✝ ∈ K.coverings X✝
⊢ K.Saturate X✝ (Sieve.generate S✝)

case mp.top
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
⊢ K.Saturate X✝ ⊤

case mp.transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
R✝ S✝ : Sieve X✝
a✝¹ : K.Saturate X✝ R✝
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, R✝.arrows f → K.Saturate Y (Sieve.pullback f S✝)
a_ih✝¹ : K.Saturate X✝ R✝
a_ih✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, R✝.arrows f → K.Saturate Y (Sieve.pullback f S✝)
⊢ K.Saturate X✝ S✝
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Presieve X✝
hS✝ : S✝ ∈ K.coverings X✝
⊢ K.Saturate X✝ (Sieve.generate S✝)

pp: case mpr.top
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
⊢ K.Saturate X✝ ⊤

pp: case mpr.pullback
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Sieve X✝
a✝ : K.Saturate X✝ S✝
Y✝ : C
f✝ : Y✝ ⟶ X✝
a_ih✝ : K.Saturate X✝ S✝
⊢ K.Saturate Y✝ (Sieve.pullback f✝ S✝)

pp: case mpr.transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ R✝ : Sieve X✝
a✝¹ : K.Saturate X✝ S✝
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, S✝.arrows f → K.Saturate Y (Sieve.pullback f R✝)
a_ih✝¹ : K.Saturate X✝ S✝
a_ih✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, S✝.arrows f → K.Saturate Y (Sieve.pullback f R✝)
⊢ K.Saturate X✝ R✝

Tactic:
<;>

Goal state after:
case mpr.of
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Presieve X✝
hS✝ : S✝ ∈ K.coverings X✝
⊢ K.Saturate X✝ (Sieve.generate S✝)

case mpr.top
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
⊢ K.Saturate X✝ ⊤

case mpr.pullback
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ : Sieve X✝
a✝ : K.Saturate X✝ S✝
Y✝ : C
f✝ : Y✝ ⟶ X✝
a_ih✝ : K.Saturate X✝ S✝
⊢ K.Saturate Y✝ (Sieve.pullback f✝ S✝)

case mpr.transitive
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
X✝ : C
S✝ R✝ : Sieve X✝
a✝¹ : K.Saturate X✝ S✝
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, S✝.arrows f → K.Saturate Y (Sieve.pullback f R✝)
a_ih✝¹ : K.Saturate X✝ S✝
a_ih✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X✝⦄, S✝.arrows f → K.Saturate Y (Sieve.pullback f R✝)
⊢ K.Saturate X✝ R✝
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: case refine_2.refine_2.h₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) =
    (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂))

pp: case refine_2.refine_2.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) =
    (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))

Tactic:
<;>

Goal state after:
case refine_2.refine_2.h₀
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) =
    (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)) ≫ F.map (pullback.fst (E.f i₁) (E.f i₂))

case refine_2.refine_2.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).p₁ k = f ≫ F.map (pullback.fst (E.f i₁) (E.f i₂)) ∧
    u ≫ (E.map F).p₂ k = f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
⊢ f ≫ F.map (pullback.snd (E.f i₁) (E.f i₂)) =
    (u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)) ≫ F.map (pullback.snd (E.f i₁) (E.f i₂))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)

Tactic:
<;>

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)

case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h.left
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X = 𝟙 (yoneda.obj (ℱ.obj.obj X))

pp: case h.right
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ (sheafYonedaHom i.inv).app X ≫ yoneda.map ((sheafHom i.hom).app X) = 𝟙 (yoneda.obj (ℱ'.obj.obj X))

Tactic:
<;>

Goal state after:
case h.left
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ yoneda.map ((sheafHom i.hom).app X) ≫ (sheafYonedaHom i.inv).app X = 𝟙 (yoneda.obj (ℱ.obj.obj X))

case h.right
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
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ✝ : Dᵒᵖ ⥤ A
ℱ'✝ ℱ ℱ' : Sheaf K A
i : G.op ⋙ ℱ.obj ≅ G.op ⋙ ℱ'.obj
X : Dᵒᵖ
⊢ (sheafYonedaHom i.inv).app X ≫ yoneda.map ((sheafHom i.hom).app X) = 𝟙 (yoneda.obj (ℱ'.obj.obj X))