awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E_1 E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{?u.219515, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
heq :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
rw :
  d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₁ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map
        (f.h₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) ≫
            F.p₂ (f.s₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)))).op
⊢ d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)) ≫
        P.map (E.p₁ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op =
    d.ι (f.s₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2) ≫
      P.map (Quiver.Hom.op (f.h₀ k.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)) ≫
        P.map (E.p₂ (k.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2))).op

Tactic:
rw [← Functor.map_comp, ← op_comp, ← Hom.w₁₁, ← Functor.map_comp, ← op_comp, ← Hom.w₁₂]

Premises used: CategoryTheory.op_comp, CategoryTheory.PreOneHypercover.Hom.w₁₁, CategoryTheory.Functor.map_comp, CategoryTheory.PreOneHypercover.Hom.w₁₂
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
a : E.I₀
⊢ f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op

Tactic:
simp [mapMultiforkOfIsLimit]

Premises used: CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (E.multicospanIndex P)
apply :
  ∀ (a : E.multicospanShape.L), (id E).mapMultiforkOfIsLimit P hc d ≫ c.ι a = Multifork.IsLimit.lift hc d.ι ⋯ ≫ c.ι a
⊢ (id E).mapMultiforkOfIsLimit P hc d = Multifork.IsLimit.lift hc d.ι ⋯

Tactic:
apply Multifork.IsLimit.hom_ext hc

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (E.multicospanIndex P)
⊢ ∀ (a : E.multicospanShape.L), (id E).mapMultiforkOfIsLimit P hc d ≫ c.ι a = Multifork.IsLimit.lift hc d.ι ⋯ ≫ c.ι a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{u_2, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
g : F.Hom G
t : Multifork (G.multicospanIndex P)
hd : IsLimit d
apply :
  ∀ (a : E.multicospanShape.L),
    (f.comp g).mapMultiforkOfIsLimit P hc t ≫ c.ι a =
      (g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d) ≫ c.ι a
⊢ (f.comp g).mapMultiforkOfIsLimit P hc t = g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d

Tactic:
apply Multifork.IsLimit.hom_ext hc

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
G : PreOneHypercover.{u_2, v, u} S
f : E.Hom F
P : Functor.{v, v_1, u, u_1} Cᵒᵖ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
g : F.Hom G
t : Multifork (G.multicospanIndex P)
hd : IsLimit d
⊢ ∀ (a : E.multicospanShape.L),
    (f.comp g).mapMultiforkOfIsLimit P hc t ≫ c.ι a =
      (g.mapMultiforkOfIsLimit P hd t ≫ f.mapMultiforkOfIsLimit P hc d) ≫ c.ι a

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
⊢ Eq.{w + 1} (α := E.I₁ i j ≃ E.I₁ i j) (congrIndexOneOfEq ⋯ ⋯) (Equiv.refl (E.I₁ i j))

Tactic:
simp [congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
i'' j'' : E.I₀
hii'' : i' = i''
hjj'' : j' = j''
k : E.I₁ i j
subst :
  ∀ (hii'' : i = i'') (hjj'' : j = j''),
    Eq (α := E.I₁ i'' j'')
      ((congrIndexOneOfEq hii'' hjj'' : (a : E.I₁ i j) → E.I₁ i'' j'')
          ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) :
        E.I₁ i'' j'')
      ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i'' j'') k : E.I₁ i'' j'')
⊢ Eq (α := E.I₁ i'' j'')
    ((congrIndexOneOfEq hii'' hjj'' : (a : E.I₁ i' j') → E.I₁ i'' j'')
        ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) :
      E.I₁ i'' j'')
    ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i'' j'') k : E.I₁ i'' j'')

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j i'' j'' : E.I₀
k : E.I₁ i j
hii'' : i = i''
hjj'' : j = j''
⊢ Eq (α := E.I₁ i'' j'')
    ((congrIndexOneOfEq hii'' hjj'' : (a : E.I₁ i j) → E.I₁ i'' j'')
        ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) :
      E.I₁ i'' j'')
    ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i'' j'') k : E.I₁ i'' j'')

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
subst :
  Eq.{w' + 1} (α := F.I₁ (u₀ i) (u₀ j)) (u₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k))
    ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ k))
⊢ Eq.{w' + 1} (α := F.I₁ (u₀ i') (u₀ j')) (u₁ ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k))
    ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i') (u₀ j')) (u₁ k))

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
⊢ Eq.{w' + 1} (α := F.I₁ (u₀ i) (u₀ j)) (u₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k))
    ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ k))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.245181, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i' j_1 j' : E.I₀
hii' : i_1 = i'
hjj' : j_1 = j'
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
i j : E.I₀
k : E.I₁ i j
⊢ v₀ i = u₀ i

Tactic:
simp [h₀]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.245181, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i' j_1 j' : E.I₀
hii' : i_1 = i'
hjj' : j_1 = j'
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
i j : E.I₀
k : E.I₁ i j
⊢ v₀ j = u₀ j

Tactic:
simp [h₀]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
u₀ v₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)
h₀ : u₀ = v₀
h₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (v₀ i) (v₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k)
i j : E.I₀
k : E.I₁ i j
subst :
  ∀ {v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)}
    (h₁ :
      ∀ (i j : E.I₀) (k : E.I₁ i j),
        u₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k)),
    (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k) = u₁ k
⊢ (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (v₀ i) (v₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k) = u₁ k

Tactic:
subst h₀
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
i j : E.I₀
k : E.I₁ i j
v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
h₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k)
⊢ (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (v₁ k) = u₁ k

Tactic:
simp [h₁]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
a b : E.I₁'
left : a.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1 = b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1
right : a.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2 = b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2
h :
  (congrIndexOneOfEq left right : (a : E.I₁ a.fst.1 a.fst.2) → E.I₁ b.fst.1 b.fst.2)
      (a.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)) =
    b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
obtain :
  ∀ (i j : E.I₀) (k : E.I₁ (i, j).1 (i, j).2)
    (left :
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)).1 =
        b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).1)
    (right :
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)).2 =
        b.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2).2)
    (h :
      (congrIndexOneOfEq left right : (a : E.I₁ ⟨(i, j), k⟩.fst.1 ⟨(i, j), k⟩.fst.2) → E.I₁ b.fst.1 b.fst.2)
          (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)) =
        b.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)),
    Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k = b
⊢ a = b

Tactic:
obtain ⟨⟨i, j⟩, k⟩ := a
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k k' : E.I₁ (i, j).1 (i, j).2
h :
  Eq (α :=
    E.I₁
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
      (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)
    ((congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ⟨(i, j), k⟩.fst.1 ⟨(i, j), k⟩.fst.2) → E.I₁ ⟨(i, j), k'⟩.fst.1 ⟨(i, j), k'⟩.fst.2)
        (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
          (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)) :
      E.I₁
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)
    (Sigma.snd (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
        (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k') :
      E.I₁
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).1
        (Sigma.fst (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2)
            (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')).2)
⊢ Eq (α := E.I₁') (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k)
    (Sigma.mk (β := fun (i : E.I₀ × E.I₀) ↦ E.I₁ i.1 i.2) (i, j) k')

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.248471, v, u} S_1
S : C
E_3 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i'_1 j_1 j'_1 : E_3.I₀
hii'_1 : i_1 = i'_1
hjj'_1 : j_1 = j'_1
E : PreOneHypercover.{u_2, v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
subst : E.Y (i₁ := i) (i₂ := j) ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.Y k
⊢ E.Y (i₁ := i') (i₂ := j') ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) = E.Y k

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.248471, v, u} S_1
S : C
E_3 : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i' j_1 j' : E_3.I₀
hii' : i_1 = i'
hjj' : j_1 = j'
E : PreOneHypercover.{u_2, v, u} S
i j : E.I₀
k : E.I₁ i j
⊢ E.Y (i₁ := i) (i₂ := j) ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.Y k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k : E.I₁ i j
⊢ congrIndexOneOfEqIso ⋯ ⋯ k =
    Iso.refl (E.Y (i₁ := i) (i₂ := j) ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k))

Tactic:
simp [congrIndexOneOfEqIso]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.252120, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
rw rw₁ : E.X i' = E.X i'
⊢ E.X i' = E.X i

Tactic:
rw [hii']
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
subst :
  (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ E.p₁ k = E.p₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫ eqToHom ⋯
⊢ (congrIndexOneOfEqIso hii' hjj' k).hom ≫ E.p₁ k =
    E.p₁ ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) ≫ eqToHom ⋯

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ E.p₁ k = E.p₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫ eqToHom ⋯

Tactic:
simp [congrIndexOneOfEqIso, congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.253910, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
rw rw₁ : E.X i' = E.X i'
⊢ E.X i = E.X i'

Tactic:
rw [hii']
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
subst :
  (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.p₁ k ≫ eqToHom ⋯
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ E.p₁ ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) =
    E.p₁ k ≫ eqToHom ⋯

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.p₁ k ≫ eqToHom ⋯

Tactic:
simp [congrIndexOneOfEqIso, congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.255701, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
rw rw₁ : E.X j' = E.X j'
⊢ E.X j = E.X j'

Tactic:
rw [hjj']
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
subst :
  (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₂ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.p₂ k ≫ eqToHom ⋯
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ E.p₂ ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) =
    E.p₂ k ≫ eqToHom ⋯

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₂ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) = E.p₂ k ≫ eqToHom ⋯

Tactic:
simp [congrIndexOneOfEqIso, congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.258677, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i'_1 j_1 j'_1 : E.I₀
hii'_1 : i_1 = i'_1
hjj'_1 : j_1 = j'_1
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
subst :
  F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k)) =
    F.Y (i₁ := u₀ i) (i₂ := u₀ j) ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ i j k))
⊢ F.Y (u₁ i' j' ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k)) =
    F.Y (i₁ := u₀ i') (i₂ := u₀ j')
      ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i') (u₀ j')) (u₁ i j k))

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.258677, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i' j_1 j' : E.I₀
hii' : i_1 = i'
hjj' : j_1 = j'
i 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)
k : E.I₁ i j
⊢ F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k)) =
    F.Y (i₁ := u₀ i) (i₂ := u₀ j) ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ i j k))

Tactic:
simp [congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} 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
subst :
  (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ z i j k =
    z i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫
      eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))
⊢ (congrIndexOneOfEqIso hii' hjj' k).hom ≫ z i j k =
    z i' j' ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k) ≫
      eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))

Tactic:
subst hii' hjj'
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i 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)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ z i j k =
    z i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k) ≫
      eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k))

Tactic:
simp [congrIndexOneOfEqIso, congrIndexOneOfEq]

Premises used: CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.congrIndexOneOfEq
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u_1
inst_1 : Category.{v_1, u_1} A
S_1 : C
E_1 E_2 : PreOneHypercover.{w, v, u} S_1
F_1 : PreOneHypercover.{w', v, u} S_1
G : PreOneHypercover.{?u.261170, v, u} S_1
S : C
E : PreOneHypercover.{w, v, u} S
F : PreOneHypercover.{w', v, u} S
i_1 i'_1 j_1 j'_1 : E.I₀
hii'_1 : i_1 = i'_1
hjj'_1 : j_1 = j'_1
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
subst :
  F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ i j) k)) =
    F.Y (i₁ := u₀ i) (i₂ := u₀ j) ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i) (u₀ j)) (u₁ i j k))
⊢ F.Y (u₁ i' j' ((congrIndexOneOfEq hii' hjj' : (a : E.I₁ i j) → E.I₁ i' j') k)) =
    F.Y (i₁ := u₀ i') (i₂ := u₀ j')
      ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ (u₀ i) (u₀ j)) → F.I₁ (u₀ i') (u₀ j')) (u₁ i j k))

Tactic:
subst hii' hjj'