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

Tactic:
simp

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

Goal state before:
pp: case h
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.h₁ (e.hom.s₁ k) ≫
      e.hom.h₁ (e.inv.s₁ (e.hom.s₁ k)) ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))

Tactic:
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:
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:
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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: case right
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ (((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
        homMk (c.π.app Y) ⋯).right =
    (homMk (c.π.app X) ⋯ ≫ F.map f).right

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X✝ : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom))).map f ≫
      homMk (c.π.app Y) ⋯ =
    homMk (c.π.app X) ⋯ ≫ F.map f

Tactic:
by
    apply CommaMorphism.ext
    · simpa using (c.w f).symm
    · 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:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m.left ≫ c.π.app j = (homMk (t.lift ((proj K✝ B).mapCone s)) ⋯).left ≫ c.π.app j

Tactic:
intro j

Goal state after:
J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
j : J
⊢ m.left ≫ c.π.app j = (homMk (t.lift ((proj K✝ B).mapCone s)) ⋯).left ≫ c.π.app j
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h
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
x✝ : E.multicospanShape.R
⊢ (congrIndexOneOfEq ?left ?right) x✝.snd =
    ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩.snd

Tactic:
simp

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

Goal state before:
pp: case left
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
x✝ : E.multicospanShape.R
⊢ x✝.fst.1 = ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩.fst.1

Tactic:
simp

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

Goal state before:
pp: case right
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
x✝ : E.multicospanShape.R
⊢ x✝.fst.2 = ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩.fst.2

Tactic:
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
x✝ : E.multicospanShape.R
⊢ (𝟭 (WalkingMulticospan E.multicospanShape)).obj (WalkingMulticospan.right x✝) =
    (Hom.mapMulticospan f.hom ⋙ Hom.mapMulticospan f.inv).obj (WalkingMulticospan.right x✝)

Tactic:
dsimp; congr; apply PreOneHypercover.I₁'.ext <;> simp

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

Goal state before:
pp: case w.h
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
x✝ : E.multicospanShape.R
⊢ (congrIndexOneOfEq ?w.left ?right) x✝.snd =
    ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩.snd

Tactic:
simp

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

Goal state before:
pp: case w.left
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
x✝ : E.multicospanShape.R
⊢ x✝.fst.1 = ⟨(f.inv.s₀ (f.hom.s₀ x✝.fst.1), f.inv.s₀ (f.hom.s₀ x✝.fst.2)), f.inv.s₁ (f.hom.s₁ x✝.snd)⟩.fst.1

Tactic:
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:
simp

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

Goal state before:
pp: case h
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
x✝ : F.multicospanShape.R
⊢ (congrIndexOneOfEq ?left ?right)
      ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩.snd =
    x✝.snd

Tactic:
simp

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

Goal state before:
pp: case left
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
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩.fst.1 = x✝.fst.1

Tactic:
simp

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

Goal state before:
pp: case right
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
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩.fst.2 = x✝.fst.2

Tactic:
simp

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

Goal state before:
pp: case w.h
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
x✝ : F.multicospanShape.R
⊢ (congrIndexOneOfEq ?w.left ?right)
      ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩.snd =
    x✝.snd

Tactic:
simp

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

Goal state before:
pp: case w.left
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
x✝ : F.multicospanShape.R
⊢ ⟨(f.hom.s₀ (f.inv.s₀ x✝.fst.1), f.hom.s₀ (f.inv.s₀ x✝.fst.2)), f.hom.s₁ (f.inv.s₁ x✝.snd)⟩.fst.1 = x✝.fst.1

Tactic:
simp

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

Goal state before:
pp: case left
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
a✝ : E.multicospanShape.L
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.left a✝))

Tactic:
simp

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

Goal state before:
pp: case right
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
a✝ : E.multicospanShape.R
⊢ eqToHom ⋯ ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝)) =
    𝟙 ((Hom.mapMulticospan f.hom).obj (WalkingMulticospan.right a✝))

Tactic:
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:
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✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = G.p₁ k ≫ g.h₀ i✝ ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
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
S : Sieve Y
⊢ (functorPullback (Over.forget X) (functorPushforward (Over.forget X) S)).arrows = S.arrows

Tactic:
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:
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)
c : T ⟶ Y₁ := Over.homMk g ⋯
d : T ⟶ W := Over.homMk b ⋯
⊢ c ≫ f = d ≫ a

Tactic:
ext; exact w

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
Z : C
f : Z ⟶ Y.left
S : Sieve Y.left
⊢ ((overEquiv Y) ((overEquiv Y).symm S)).arrows f ↔ ((overEquiv Y).symm S).arrows (Over.homMk f ⋯)

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
⊢ ∀ (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)

Tactic:
⟨i₂, ⟨φ₂⟩⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
i₁ : I
φ₁ : Y₁ ⟶ Y i₁
i₂ : I
φ₂ : Y₂ ⟶ Y i₂
⊢ g₁ ≫ f₁ = g₂ ≫ f₂ →
    (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ ⋯) =
      (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ ⋯)
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:
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:
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✝ S : C
x✝³ x✝² : (PreOneHypercover.trivial S).I₀
x✝¹ : C
x✝ : x✝¹ ⟶ (PreOneHypercover.trivial S).X x✝³
⊢ (PreOneHypercover.trivial S).sieve₁ x✝ x✝ ∈ J x✝¹

Tactic:
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:
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:
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:
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:
simp

Goal state after: