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

Goal state before:
pp: case refine_1.refine_1
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    (F.map c ≫ (Nonempty.some hb).map ≫ p) ≫ f

Tactic:
assoc,

Goal state after:
case refine_1.refine_1
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ ((Nonempty.some hb).map ≫ p) ≫ f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_1.refine_1
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ ((Nonempty.some hb).map ≫ p) ≫ f

Tactic:
assoc,

Goal state after:
case refine_1.refine_1
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ F.map c ≫ (Nonempty.some hb).map ≫ Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) =
    F.map c ≫ (Nonempty.some hb).map ≫ p ≫ f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: case refine_1.refine_2
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ (a ≫ b) ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p

Tactic:
assoc,

Goal state after:
case refine_1.refine_2
C₀ : Type u₀
C : Type u
inst✝² : Category.{v₀, u₀} C₀
inst✝¹ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
inst✝ : IsDenseSubsite J₀ J F
X : C
data : F.OneHypercoverDenseData J₀ J X
X₀ : C₀
f : F.obj X₀ ⟶ X
this✝ : F.IsCoverDense J
this : F.IsLocallyFull J
R : ⦃W : C⦄ → ⦃p : W ⟶ F.obj X₀⦄ → (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p → Sieve W :=
  fun W p hp ↦
    Sieve.bind (Sieve.coverByImage F W).arrows fun U π hπ ↦
      Sieve.pullback (Nonempty.some hπ).lift (Sieve.functorPushforward F (F.imageSieve ((Nonempty.some hπ).map ≫ p)))
W' W : C
p : W ⟶ F.obj X₀
hp : (Sieve.pullback f data.toOneHypercover.sieve₀).arrows p
Y₀ : C
a : W' ⟶ Y₀
b : Y₀ ⟶ W
hb : (Sieve.coverByImage F W).arrows b
U : C₀
c : U ⟶ (Nonempty.some hb).obj
d : W' ⟶ F.obj U
fac : a ≫ (Nonempty.some hb).lift = d ≫ F.map c
x₁ : U ⟶ X₀
w₁ : F.map x₁ = F.map c ≫ (Nonempty.some hb).map ≫ p
hp' : Sieve.ofArrows.h hp ≫ data.f (Sieve.ofArrows.i hp) = p ≫ f
⊢ a ≫ b ≫ p = d ≫ F.map c ≫ (Nonempty.some hb).map ≫ p
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows ((F.map d ≫ c) ≫ (data X).f j)

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝³ : Category.{v₀, u₀} C₀
inst✝² : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
G : Cᵒᵖ ⥤ A
hG₀ : Presheaf.IsSheaf J₀ (F.op ⋙ G)
hG : (X : C) → IsLimit ((data X).toOneHypercover.multifork G)
X : C
S : J.Cover X
s : Multifork (S.index G)
a : S.Arrow
i : (data a.Y).I₀
X₀ : C₀
b : X₀ ⟶ (data a.Y).X i
Y : C
j : (data X).I₀
c : F.obj X₀ ⟶ F.obj ((data X).X j)
fac₁ : c ≫ (data X).f j = F.map b ≫ (data a.Y).f i ≫ a.f
Y₀ : C₀
d : Y₀ ⟶ X₀
e : Y₀ ⟶ (data X).X j
fac₂ : F.map e = F.map d ≫ c
⊢ (↑S).arrows (F.map d ≫ c ≫ (data X).f j)
Module: Mathlib.CategoryTheory.Sites.ConstantSheaf

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ ((sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).inv ≫
        sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom) ≫
      ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U

Tactic:
assoc,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasWeakSheafify J D
B : Type u_3
inst✝³ : Category.{v_3, u_3} B
U : D ⥤ B
inst✝² : HasWeakSheafify J B
inst✝¹ : J.PreservesSheafification U
inst✝ : J.HasSheafCompose U
F : Sheaf J D
T : C
hT : IsTerminal T
⊢ (sheafifyComposeIso J U ((const Cᵒᵖ).obj (F.obj.obj (Opposite.op T)))).inv ≫
      sheafifyMap J (constComp Cᵒᵖ (F.obj.obj (Opposite.op T)) U).hom ≫
        ((constantSheafAdj J B hT).counit.app ((sheafCompose J U).obj F)).hom =
    whiskerRight ((constantSheafAdj J D hT).counit.app F).hom U
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ (F.map a ≫ h₁.q) ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = (F.map a ≫ h₂.q) ≫ (data X).f h₂.i₀

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
X₀ Y₀ : C₀
f : F.obj X₀ ⟶ X
g : Y₀ ⟶ X₀
h₁ h₂ : (data X).SieveStruct f g
Z₀ : C₀
a : Z₀ ⟶ Y₀
b₁ : Z₀ ⟶ (data X).X h₁.i₀
w₁ : F.map b₁ = F.map a ≫ h₁.q
b₂ : Z₀ ⟶ (data X).X h₂.i₀
w₂ : F.map b₂ = F.map a ≫ h₂.q
⊢ F.map a ≫ h₁.q ≫ (data X).f h₁.i₀ = F.map a ≫ h₂.q ≫ (data X).f h₂.i₀
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
X : C
E : PreZeroHypercover X
⊢ E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ .mk _ h⟩
  rw [PreZeroHypercoverFamily.mem_precoverage_iff] at h
  obtain ⟨F, h, heq⟩ := h
  rw [P.iff_shrink] at h ⊢
  rwa [PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ heq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ (presheafMap data G₀ g ≫ restriction data G₀ f) ≫ G₀.obj.map (d.op ≫ c.op) =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map (d.op ≫ c.op)

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
⊢ presheafMap data G₀ g ≫ restriction data G₀ f ≫ G₀.obj.map (d.op ≫ c.op) =
    restriction data G₀ (f ≫ g) ≫ G₀.obj.map (d.op ≫ c.op)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ (restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
        IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd)) ≫
      G₀.obj.map a.op =
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj.map a.op

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) ≫ G₀.obj.map a.op =
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) ≫ G₀.obj.map a.op =
    (presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc)) ≫
      G₀.obj.map a.op

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y : C
X₀ : C₀
f : F.obj X₀ ⟶ X
g : X ⟶ Y
U₀ Y₀ : C₀
c : U₀ ⟶ Y₀
d : Y₀ ⟶ X₀
hd : Presieve.functorPullback F (Sieve.pullback f (data X).toPreOneHypercover.sieve₀).arrows d
hc :
  Presieve.functorPullback F
    (Sieve.pullback (Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g)
        (data Y).toPreOneHypercover.sieve₀).arrows
    c
hc' :
  Sieve.ofArrows.h hc ≫ (data Y).f (Sieve.ofArrows.i hc) =
    F.map c ≫ Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) ≫ g
hd' : Sieve.ofArrows.h hd ≫ (data X).f (Sieve.ofArrows.i hd) = F.map d ≫ f
this : F.imageSieve (Sieve.ofArrows.h hc) ⊓ Sieve.pullback c (F.imageSieve (Sieve.ofArrows.h hd)) ∈ J₀ U₀
V₀ : C₀
a : V₀ ⟶ U₀
x₁ : V₀ ⟶ (data Y).X (Sieve.ofArrows.i hc)
fac₁ : F.map x₁ = F.map a ≫ Sieve.ofArrows.h hc
x₂ : V₀ ⟶ (data X).X (Sieve.ofArrows.i hd)
fac₂ : F.map x₂ = F.map (a ≫ c) ≫ Sieve.ofArrows.h hd
⊢ restriction data G₀ ((data X).f (Sieve.ofArrows.i hd) ≫ g) ≫
      IsDenseSubsite.mapPreimage J F G₀ (F.map c ≫ Sieve.ofArrows.h hd) ≫ G₀.obj.map a.op =
    presheafObjπ data G₀ Y (Sieve.ofArrows.i hc) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hc) ≫ G₀.obj.map a.op
Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Goal state before:
pp: σ : Type u_1
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : SetLike σ A
inst✝² : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst✝¹ : GradedRing 𝒜
inst✝ : Algebra.FiniteType (↥(𝒜 0)) A
O : Type u_2
commRing✝ : CommRing O
domain✝ : IsDomain O
valuationRing✝ : ValuationRing O
K : Type u_2
field✝ : Field K
algebra✝ : Algebra O K
isFractionRing✝ : IsFractionRing O K
i₁ : Spec (CommRingCat.of K) ⟶ Proj 𝒜
i₂ : Spec (CommRingCat.of O) ⟶ Spec (CommRingCat.of ↥(𝒜 0))
w : CommSq i₁ (Spec.map (CommRingCat.ofHom (algebraMap O K))) (toSpecZero 𝒜) i₂
x✝ : Finset A
hx : Algebra.adjoin ↥(𝒜 0) ↑x✝ = ⊤
d : (i : A) → i ∈ x✝ → ℕ
hd : ∀ (i : A) (a : i ∈ x✝), d i a ≠ 0
hxd : ∀ (i : A) (a : i ∈ x✝), i ∈ 𝒜 (d i a)
i : ↥x✝
hi : i₁ (IsLocalRing.closedPoint K) ∈ basicOpen 𝒜 ↑i
this : Set.range ⇑i₁ ⊆ ↑(Hom.opensRange (awayι 𝒜 ↑i ⋯ ⋯))
φ : Spec (CommRingCat.of K) ⟶ Spec (CommRingCat.of (Away 𝒜 ↑i)) := IsOpenImmersion.lift (awayι 𝒜 ↑i ⋯ ⋯) i₁ this
H :
  Spec.preimage i₂ ≫ CommRingCat.ofHom (algebraMap O K) =
    CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers ↑i)) ≫ Spec.preimage φ
i₀ : ↥x✝
φ' : Away 𝒜 (↑i * ↑i₀) →+* K
hφ : φ'.comp (awayMap 𝒜 ⋯ ⋯) = CommRingCat.Hom.hom (Spec.preimage φ)
hφ' : (φ'.comp (awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range
e : O ≃+* ↥(algebraMap O K).range := (AlgEquiv.ofInjective (Algebra.ofId O K) ⋯).toRingEquiv
φ'' : Away 𝒜 ↑i₀ →+* O := e.symm.toRingHom.comp ((Subring.inclusion hφ').comp (φ'.comp (awayMap 𝒜 ⋯ ⋯)).rangeRestrict)
x : Away 𝒜 ↑i₀
⊢ ((algebraMap O K).comp φ'') x = (φ'.comp (awayMap 𝒜 ⋯ ⋯)) x

Tactic:
exact congr_arg Subtype.val (e.apply_symm_apply _)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i =
    (presheafMap data G₀ g ≫ presheafMap data G₀ f) ≫ presheafObjπ data G₀ X i

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
i : (data X).I₀
⊢ presheafMap data G₀ (f ≫ g) ≫ presheafObjπ data G₀ X i =
    presheafMap data G₀ g ≫ presheafMap data G₀ f ≫ presheafObjπ data G₀ X i