mathlib-initiative/mathlib-tactics huggingface dataset:
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 : E.I₀
k : E.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
      E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    F.p₁ (s₁ k) ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ i)

Tactic:
← cancel_epi (h₁ k).hom,

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
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
        E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    (h₁ k).hom ≫ F.p₁ (s₁ k) ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ i)
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
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type v
inst✝³ : Category.{u, v} A
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
X : C
Y : Over X
T : ↑(J ((Over.forget X).obj Y))
⊢ Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) ↑T) ∈ J ((Over.forget X).obj Y)

Tactic:
by
    convert! T.property
    ext Z f
    constructor
    · rintro ⟨_, _, g', hg, rfl⟩
      exact T.val.downward_closed hg g'
    · intro hf
      exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩

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 : E.I₀
k : E.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
      E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    F.p₂ (s₁ k) ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ j)

Tactic:
← cancel_epi (h₁ k).hom,

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
i j : E.I₀
k : E.I₁ i j
⊢ (h₁ k).hom ≫
      ((congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv) ≫
        E.p₂ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) =
    (h₁ k).hom ≫ F.p₂ (s₁ k) ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ (s₀ j)
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),
    ((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₁₂ := ⋯ }) ≫
            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₁₂ := ⋯ }).s₁
        k =
      (congrIndexOneOfEq ⋯ ⋯) ((𝟙 F).s₁ k)

Tactic:
by simp

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
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ i = e.inv.s₀ (e.hom.s₀ i)

Tactic:
by simp

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
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ j = e.inv.s₀ (e.hom.s₀ j)

Tactic:
by simp

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
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ i = e.hom.s₀ (e.inv.s₀ i)

Tactic:
by simp

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
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ j = e.hom.s₀ (e.inv.s₀ j)

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
H✝ : S ∈ J X
Y : D
f : Y ⟶ e.functor.obj X
H : S.arrows (e.inverse.map f ≫ e.unitInv.app X)
⊢ f = e.counitInv.app Y ≫ e.functor.map (e.inverse.map f ≫ e.unitInv.app X)

Tactic:
by simp

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
e : E ≅ F
i : E.I₀
⊢ E.X i = E.X (e.inv.s₀ (e.hom.s₀ i))

Tactic:
by simp

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
e : E ≅ F
i : F.I₀
⊢ F.X i = F.X (e.hom.s₀ (e.inv.s₀ i))

Tactic:
by simp

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
e : E ≅ F
i : E.I₀
⊢ E.X (e.inv.s₀ (e.hom.s₀ i)) = E.X i

Tactic:
by simp

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
e : E ≅ F
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

Tactic:
by simp

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
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.s₁ (e.hom.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
by simp

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 : E.Hom F
X✝ Y✝ Z✝ x✝² x✝¹ : WalkingMulticospan E.multicospanShape
x✝ : x✝¹ ⟶ x✝²
⊢ (match x✝¹, x✝², WalkingMulticospan.Hom.id x✝¹ ≫ x✝ with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match x✝¹, x✝¹, WalkingMulticospan.Hom.id x✝¹ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match x✝¹, x✝², x✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by simp

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 : E.Hom F
X✝ Y✝ Z✝ : WalkingMulticospan E.multicospanShape
a✝ : E.multicospanShape.R
⊢ (match WalkingMulticospan.left (E.multicospanShape.fst a✝), WalkingMulticospan.right a✝,
      WalkingMulticospan.Hom.fst a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match WalkingMulticospan.left (E.multicospanShape.fst a✝), WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.fst a✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by simp

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 : E.Hom F
X✝ Y✝ Z✝ : WalkingMulticospan E.multicospanShape
a✝ : E.multicospanShape.R
⊢ (match WalkingMulticospan.left (E.multicospanShape.snd a✝), WalkingMulticospan.right a✝,
      WalkingMulticospan.Hom.snd a✝ ≫ WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
    | x, .(x), WalkingMulticospan.Hom.id .(x) =>
      WalkingMulticospan.Hom.id
        (match x with
        | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
        | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
    | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
    | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
      WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) =
    (match WalkingMulticospan.left (E.multicospanShape.snd a✝), WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.snd a✝ with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)) ≫
      match WalkingMulticospan.right a✝, WalkingMulticospan.right a✝,
        WalkingMulticospan.Hom.id (WalkingMulticospan.right a✝) with
      | x, .(x), WalkingMulticospan.Hom.id .(x) =>
        WalkingMulticospan.Hom.id
          (match x with
          | WalkingMulticospan.left i => WalkingMulticospan.left (f.s₀ i)
          | WalkingMulticospan.right i => WalkingMulticospan.right (f.s₁' i))
      | .(WalkingMulticospan.left (E.multicospanShape.fst i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.fst i => WalkingMulticospan.Hom.fst (f.s₁' i)
      | .(WalkingMulticospan.left (E.multicospanShape.snd i)), .(WalkingMulticospan.right i),
        WalkingMulticospan.Hom.snd i => WalkingMulticospan.Hom.snd (f.s₁' i)

Tactic:
by simp

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 F : PreOneHypercover S
f : E ≅ F
⊢ ∀ (i : E.multicospanShape.L),
    (𝟭 (WalkingMulticospan E.multicospanShape)).obj (WalkingMulticospan.left i) =
      (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).obj (WalkingMulticospan.left i)

Tactic:
by simp

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 F : PreOneHypercover S
f : E ≅ F
⊢ ∀ (i : F.multicospanShape.L),
    (Hom.mapMulticospan f.inv ⋙ Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left i) =
      (𝟭 (WalkingMulticospan F.multicospanShape)).obj (WalkingMulticospan.left i)

Tactic:
by simp

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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
⊢ ∀ (i : G.I₀),
    (PreZeroHypercover.interLift f.toHom g.toHom).h₀ i ≫
        (E.inter F).f ((PreZeroHypercover.interLift f.toHom g.toHom).s₀ i) =
      G.f i

Tactic:
by simp

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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ f.h₁ k ≫ E.p₁ (f.s₁ k, g.s₁ k).1 ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 =
    g.h₁ k ≫ F.p₁ (f.s₁ k, g.s₁ k).2 ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
rw [f.w₁₁_assoc k, g.w₁₁_assoc k]
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
W : Over X
a : W ⟶ Y₁
b : Z ⟶ W.left
h : S.arrows (a ≫ f)
⊢ (b ≫ Over.Hom.left a) ≫ Over.Hom.left f = b ≫ Over.Hom.left (a ≫ f)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y₁ Y₂ : Over X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom

Tactic:
by dsimp [T]; rw [← Over.w a, ← reassoc_of% w, Over.w f]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoversTop.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
hY : J.CoversTop Y
hF : IsSheaf J F
H : Presieve.IsSheaf J F
s : (X : C) → F.obj (Opposite.op X) := fun X ↦ ⋯.amalgamate (x.familyOfElements X) ⋯
hs : ∀ {X : C} (i : I) (f : X ⟶ Y i), s X = (ConcreteCategory.hom (F.map f.op)) (x i)
hs' : ∀ {W X : C} (a : W ⟶ X) (i : I) (x : W ⟶ Y i), (ConcreteCategory.hom (F.map a.op)) (s X) = s W
i : I
⊢ (ConcreteCategory.hom (F.map (𝟙 (Y i)).op)) (x i) = x i

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
R : Presieve Y
Z : C
g : Z ⟶ Y.left
W : Over X
u : Over.mk (g ≫ Y.hom) ⟶ W
v : W ⟶ Y
hv : R v
huv : u ≫ v = Over.homMk g ⋯
⊢ Over.Hom.left v = 𝟙 W.left ≫ (Over.forget X).map v

Tactic:
by simp

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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
⊢ ∀ (E_1 : Multifork (E.multicospanIndex F.obj)) (m : E_1.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = E_1.ι i) → m = multiforkLift E_1

Tactic:
by
    intro c m hm
    apply F.property.hom_ext_ofArrows _ E.mem₀
    intro i₀
    rw [multiforkLift_map]
    exact hm i₀

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
J : GrothendieckTopology C
S✝ S : C
x✝⁴ x✝³ : (PreOneHypercover.trivial S).I₀
x✝² : C
x✝¹ : x✝² ⟶ (PreOneHypercover.trivial S).X x✝⁴
x✝ : x✝² ⟶ (PreOneHypercover.trivial S).X x✝³
h : x✝¹ ≫ (PreOneHypercover.trivial S).f x✝⁴ = x✝ ≫ (PreOneHypercover.trivial S).f x✝³
⊢ (PreOneHypercover.trivial S).sieve₁ x✝¹ x✝ ∈ J x✝²

Tactic:
by
    simp only [PreOneHypercover.trivial_toPreZeroHypercover, PreZeroHypercover.singleton_X,
      PreZeroHypercover.singleton_f, Category.comp_id] at h
    subst h
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
⊢ 𝟙 Z ≫ (Over.mk (g ≫ U.hom ≫ f)).hom = ((Over.map f).obj (Over.mk (g ≫ U.hom))).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
U : Over X
S : Sieve ((Over.map f).obj U)
Z : C
g : Z ⟶ U.left
u : (Over.map f).obj (Over.mk (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom ≫ f) := Over.homMk (𝟙 Z) ⋯
heq : (Over.map f).map (Over.homMk g ⋯) = u ≫ Over.homMk g ⋯
⊢ 𝟙 Z ≫ ((Over.map f).obj (Over.mk (g ≫ U.hom))).hom = (Over.mk (g ≫ U.hom ≫ f)).hom

Tactic:
by simp

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
J : GrothendieckTopology C
X : C
S : J.Cover X
⊢ S.preOneHypercover.sieve₀ ∈ J X

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreZeroHypercover S
inst✝ : E.HasPullbacks
i j : E.I₀
Y : C
f : Y ⟶ pullback (E.toPreOneHypercover.f i) (E.toPreOneHypercover.f j)
a✝ : ⊤.arrows f
⊢ f ≫ 𝟙 (pullback (E.f i) (E.f j)) = f

Tactic:
by simp

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
J : Precoverage C
S : C
E : J.ZeroHypercover S
inst✝ : E.HasPullbacks
⊢ ∀ (i₁ i₂ : E.toPreOneHypercover.I₀),
    E.toPreOneHypercover.sieve₁' i₁ i₂ ∈
      J.toGrothendieck (pullback (E.toPreOneHypercover.f i₁) (E.toPreOneHypercover.f i₂))

Tactic:
by simp

Goal state after: