mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
⊢ PreservesFiniteLimits (presheafToSheaf J A ⋙ (G.sheafPushforwardContinuous A J K).inv)

Tactic:
by

Goal state after:
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'
k : E.I₁ i j
⊢ E.X j = E.X j'

Tactic:
by

Goal state after:
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✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
this : PreservesFiniteLimits (presheafToSheaf J A ⋙ (G.sheafPushforwardContinuous A J K).inv)
⊢ PreservesFiniteLimits (sheafifyOfIsEquivalence J K G A)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ E.p₂ ((congrIndexOneOfEq hii' hjj') k) = E.p₂ k ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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✝¹ : HasSheafify J A
inst✝ : HasFiniteLimits A
⊢ HasSheafify K A

Tactic:
by

Goal state after:
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 i' j 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)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ F.Y (u₁ i' j' ((congrIndexOneOfEq hii' hjj') k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j 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)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).hom ≫ z i j k =
    z i' j' ((congrIndexOneOfEq hii' hjj') k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
f : Y ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback f ⊤).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ Y
⊢ Presieve.IsSheafFor P (Sieve.pullback g (Sieve.pullback f S)).arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j 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)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ z i' j' ((congrIndexOneOfEq hii' hjj') k) ≫ eqToHom ⋯ =
    z i j k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
⊢ Presieve.IsSheafFor P (Sieve.pullback g R).arrows

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
Ps : Set (Cᵒᵖ ⥤ Type w)
h : P ∈ Ps
X : C
S : Sieve X
hS : S ∈ (finestTopology Ps) X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
X : C
S : Sieve X
H : ∀ P ∈ Ps, ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows
⊢ S ∈ (finestTopology Ps) X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
⊢ J ≤ finestTopology Ps

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) P

Tactic:
by

Goal state after:
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)
⊢ ∀ P ∈ Set.range yoneda.obj, Presieve.IsSheaf J P

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J K : GrothendieckTopology C
h : J ≤ K
inst✝ : K.Subcanonical
x✝³ x✝² : C
x✝¹ : Sieve x✝²
x✝ : x✝¹ ∈ J x✝²
⊢ generate x✝¹.arrows ∈ J x✝²

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X✝ : C
J✝ J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
⊢ Presheaf.IsSheaf J (CategoryTheory.yoneda.obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : Sheaf K (Type (max u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf (F.inducedTopology K) (F.op ⋙ G.obj)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
⊢ J ≤ F.inducedTopology K ↔ F.IsContinuous J K

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (gs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (gs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (gs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₀ i =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₁ k =
      { toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₁ k ≫
        (congrIndexOneOfEqIso ⋯ ⋯ ({ toHom := toHomf, s₁ := gs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)).inv ≫
          eqToHom ⋯
⊢ fs₁ = gs₁

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
⊢ S ∈ (F.inducedTopology K) X ↔
    ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
J : GrothendieckTopology E
⊢ F.inducedTopology (G.inducedTopology J) ≤ (F ⋙ G).inducedTopology J

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
⊢ F.inducedTopology K = G.inducedTopology K

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv ≫ eqToHom ⋯
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ K (F.obj X)
⊢ S ∈ (F.restrictedTopology K) X

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : F.IsContinuous (F.restrictedTopology K) K
⊢ F.restrictedTopology K = F.inducedTopology K

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
h : F.restrictedTopology K = J
⊢ F.inducedTopology K = J

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
by

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : Precoverage D
⊢ (comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
by

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

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ Sieve.functorPushforward G S ∈ K (G.obj X) ↔ ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
by

Goal state after:
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)
i j : E.I₀
k : E.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) = F.Y (f.s₁ k)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
⊢ f = g ↔
    ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯) (hs₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
      ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = g.h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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
⊢ s₀ i = s₀ (s₀.symm (s₀ i))

Tactic:
by

Goal state after:
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
⊢ s₀ j = s₀ (s₀.symm (s₀ j))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : 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
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
by

Goal state after:
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
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)) = F.Y (s₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))))

Tactic:
by

Goal state after:
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
⊢ E.Y ((congrIndexOneOfEq ⋯ ⋯) k) = E.Y (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : 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₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ i = s₀.symm (s₀ i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : 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₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ j = s₀.symm (s₀ j)

Tactic:
by

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

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ G.map (iU₁U ≫ iUY ≫ f) = G.map (iU₁W ≫ iWX)

Tactic:
by

Goal state after:
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
⊢ IsIso ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))

Tactic:
by

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

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S : Sieve X
a✝ : (Precoverage.comap G K.toPrecoverage).Saturate X S
Y : C
f : Y ⟶ X
ih : Sieve.functorPushforward G S ∈ K (G.obj X)
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map f = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ f = iU₂U₁ ≫ iU₁W ≫ iWX
⊢ ((iZU₂ ≫ G.map iU₂U₁) ≫ G.map iU₁U) ≫ G.map iUY = iZU₂ ≫ G.map (iU₂U₁ ≫ iU₁U ≫ iUY)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : 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₀
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
k : E.I₁ i j
⊢ (h₁ k).hom ≫ (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv =
    (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
by

Goal state after:
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
i j : F.I₀
k : F.I₁ i j
⊢ i = s₀ (__Hom✝.s₀ i)

Tactic:
by

Goal state after:
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
i j : F.I₀
k : F.I₁ i j
⊢ j = s₀ (__Hom✝.s₀ j)

Tactic:
by

Goal state after:
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
i j : F.I₀
k : F.I₁ i j
⊢ F.Y ((congrIndexOneOfEq ⋯ ⋯) k) = F.Y (s₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k)))

Tactic:
by

Goal state after: