awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs₀ : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
hh₀ : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)
hh₁ :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯
⊢ e.hom.s₁ (e.inv.s₁ k) =
    (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ i j) → F.I₁ (e.hom.s₀ (e.inv.s₀ i)) (e.hom.s₀ (e.inv.s₀ j))) k

Tactic:
simpa using hs₁ i j k
-- 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.335121, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ E.X i = E.X (e.inv.s₀ (e.hom.s₀ i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
⊢ ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
⊢ ∃ (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).s₁ k =
        (congrIndexOneOfEq ⋯ ⋯ :
            (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
          (Hom.s₁ (𝟙 E) k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
h :
  ∃ (hs₁ :
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).s₁ k =
        (congrIndexOneOfEq ⋯ ⋯ :
            (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
          (Hom.s₁ (𝟙 E) k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh i
-- 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.337364, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ F.X i = F.X (e.hom.s₀ (e.inv.s₀ i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
⊢ ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
⊢ ∃ (hs₁ :
    ∀ (i j : F.I₀) (k : F.I₁ i j),
      (e.inv ≫ e.hom).s₁ k =
        (congrIndexOneOfEq ⋯ ⋯ :
            (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
          (Hom.s₁ (𝟙 F) k)),
    ∀ (i j : F.I₀) (k : F.I₁ i j),
      (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
h :
  ∃ (hs₁ :
    ∀ (i j : F.I₀) (k : F.I₁ i j),
      (e.inv ≫ e.hom).s₁ k =
        (congrIndexOneOfEq ⋯ ⋯ :
            (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
          (Hom.s₁ (𝟙 F) k)),
    ∀ (i j : F.I₀) (k : F.I₁ i j),
      (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh i
-- 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.339607, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
e_j :
  (congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k =
    e.inv.s₁ (e.hom.s₁ k)
⊢ E.Y (i₁ := e.inv.s₀ (e.hom.s₀ i)) (i₂ := e.inv.s₀ (e.hom.s₀ j))
      ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k) =
    E.Y (e.inv.s₁ (e.hom.s₁ k))

Tactic:
congr 1
-- 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.339607, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k =
    e.inv.s₁ (e.hom.s₁ k)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
⊢ ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
w : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
⊢ ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
w : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
w₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)
⊢ ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
hs : (e.hom ≫ e.inv).s₀ = (Hom.toHom (𝟙 E)).s₀
w : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (Hom.toHom (𝟙 E)).h₀ i ≫ eqToHom ⋯
w_1 :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : E.I₁ ((𝟙 E).s₀ i) ((𝟙 E).s₀ j)) → E.I₁ ((e.hom ≫ e.inv).s₀ i) ((e.hom ≫ e.inv).s₀ j))
        (Hom.s₁ (𝟙 E) k)
hh :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    (e.hom ≫ e.inv).h₁ k = Hom.h₁ (𝟙 E) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 E) k)) ≫ eqToHom ⋯
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simpa using hh i j k
-- 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.344064, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
e_j :
  (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ i j) → F.I₁ (e.hom.s₀ (e.inv.s₀ i)) (e.hom.s₀ (e.inv.s₀ j))) k =
    e.hom.s₁ (e.inv.s₁ k)
⊢ F.Y (i₁ := e.hom.s₀ (e.inv.s₀ i)) (i₂ := e.hom.s₀ (e.inv.s₀ j))
      ((congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ i j) → F.I₁ (e.hom.s₀ (e.inv.s₀ i)) (e.hom.s₀ (e.inv.s₀ j))) k) =
    F.Y (e.hom.s₁ (e.inv.s₁ k))

Tactic:
congr 1
-- 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.344064, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯ : (a : F.I₁ i j) → F.I₁ (e.hom.s₀ (e.inv.s₀ i)) (e.hom.s₀ (e.inv.s₀ j))) k =
    e.hom.s₁ (e.inv.s₁ k)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
⊢ (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
⊢ ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
w : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
⊢ ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
w : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
w₁ :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)
⊢ ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯

Tactic:
obtain ⟨hs, _, _, hh⟩ := Hom.ext'_iff.mp e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.Hom.ext'_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.One
Goal:
C : Type u
inst : Category.{v, u} C
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : F.I₀
k : F.I₁ i j
hs : (e.inv ≫ e.hom).s₀ = (Hom.toHom (𝟙 F)).s₀
w : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (Hom.toHom (𝟙 F)).h₀ i ≫ eqToHom ⋯
w_1 :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).s₁ k =
      (congrIndexOneOfEq ⋯ ⋯ :
          (a : F.I₁ ((𝟙 F).s₀ i) ((𝟙 F).s₀ j)) → F.I₁ ((e.inv ≫ e.hom).s₀ i) ((e.inv ≫ e.hom).s₀ j))
        (Hom.s₁ (𝟙 F) k)
hh :
  ∀ (i j : F.I₀) (k : F.I₁ i j),
    (e.inv ≫ e.hom).h₁ k = Hom.h₁ (𝟙 F) k ≫ Iso.inv (congrIndexOneOfEqIso ⋯ ⋯ (Hom.s₁ (𝟙 F) k)) ≫ eqToHom ⋯
⊢ e.inv.h₁ k ≫ e.hom.h₁ (e.inv.s₁ k) = (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simpa using hh i j k
-- 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.348521, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ E.X (e.inv.s₀ (e.hom.s₀ i)) = E.X i

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.348521, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
h :
  e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))
⊢ IsIso (e.hom.h₀ i)

Tactic:
use e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom (by simp)

Premises used: CategoryTheory.PreZeroHypercover.Hom.h₀, CategoryTheory.eqToHom, CategoryTheory.PreOneHypercover.Hom.toHom, CategoryTheory.PreZeroHypercover.Hom.s₀, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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.348521, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ e.inv.s₀ (e.hom.s₀ i) = i

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.348521, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
h :
  Eq.{v + 1} (α := E.X i ⟶ E.X i) (𝟙 (E.X i)) (𝟙 (E.X i)) ∧
    Eq.{v + 1} (α := F.X (e.hom.s₀ i) ⟶ F.X (e.hom.s₀ i)) (eqToHom ⋯ ≫ eqToHom ⋯) (𝟙 (F.X (e.hom.s₀ i)))
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯ = 𝟙 (E.X i) ∧
    (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
rw [PreOneHypercover.hom_inv_h₀_assoc, eqToHom_trans, eqToHom_refl, Category.assoc,
    ← eqToHom_naturality _ (by simp), PreOneHypercover.inv_hom_h₀_assoc]

Premises used: CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc, CategoryTheory.Category.assoc, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_naturality, CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc, CategoryTheory.eqToHom_trans
-- 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.348521, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : E.I₀
⊢ Eq.{v + 1} (α := E.X i ⟶ E.X i) (𝟙 (E.X i)) (𝟙 (E.X i)) ∧
    Eq.{v + 1} (α := F.X (e.hom.s₀ i) ⟶ F.X (e.hom.s₀ i)) (eqToHom ⋯ ≫ eqToHom ⋯) (𝟙 (F.X (e.hom.s₀ i)))

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.352161, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i : F.I₀
⊢ IsIso (e.inv.h₀ i)

Tactic:
.of_isIso_fac_right (PreOneHypercover.inv_hom_h₀ e i)

Premises used: CategoryTheory.IsIso.of_isIso_fac_right, CategoryTheory.PreOneHypercover.inv_hom_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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
e_j :
  e.inv.s₁ (e.hom.s₁ k) =
    (congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k
⊢ E.Y (e.inv.s₁ (e.hom.s₁ k)) =
    E.Y (i₁ := e.inv.s₀ (e.hom.s₀ i)) (i₂ := e.inv.s₀ (e.hom.s₀ j))
      ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k)

Tactic:
congr 1
-- 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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.s₁ (e.hom.s₁ k) =
    (congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) 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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ i = e.inv.s₀ (e.hom.s₀ i)

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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ j = e.inv.s₀ (e.hom.s₀ j)

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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
h :
  e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom = 𝟙 (E.Y k) ∧
    (e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom) ≫ e.hom.h₁ k = 𝟙 (F.Y (e.hom.s₁ k))
⊢ IsIso (e.hom.h₁ k)

Tactic:
use e.inv.h₁ _ ≫ eqToHom (by congr 1; simp) ≫ (E.congrIndexOneOfEqIso (by simp) (by simp) k).hom

Premises used: CategoryTheory.eqToHom, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso, CategoryTheory.PreOneHypercover.Hom.h₁, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
h :
  e.inv.h₁ (e.hom.s₁ k) ≫
      eqToHom ⋯ ≫
        e.hom.h₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k) ≫
          eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)) =
    𝟙 (F.Y (e.hom.s₁ k))
⊢ e.hom.h₁ k ≫ e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom = 𝟙 (E.Y k) ∧
    (e.inv.h₁ (e.hom.s₁ k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).hom) ≫ e.hom.h₁ k = 𝟙 (F.Y (e.hom.s₁ k))

Tactic:
simp only [PreOneHypercover.hom_inv_h₁_assoc, eqToHom_trans_assoc, eqToHom_refl, Category.id_comp,
    Iso.inv_hom_id, Category.assoc, true_and, PreOneHypercover.congrIndexOneOfEqIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality, CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans_assoc, true_and, CategoryTheory.Category.id_comp
-- 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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
h :
  e.inv.h₁ (e.hom.s₁ k) ≫
      e.hom.h₁ (e.inv.s₁ (e.hom.s₁ k)) ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)) =
    𝟙 (F.Y (e.hom.s₁ k))
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      eqToHom ⋯ ≫
        e.hom.h₁ ((congrIndexOneOfEq ⋯ ⋯ : (a : E.I₁ i j) → E.I₁ (e.inv.s₀ (e.hom.s₀ i)) (e.inv.s₀ (e.hom.s₀ j))) k) ≫
          eqToHom ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)) =
    𝟙 (F.Y (e.hom.s₁ k))

Tactic:
rw [← eqToHom_naturality_assoc _ (by simp)]

Premises used: CategoryTheory.eqToHom_naturality_assoc
-- 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.354132, v, u} S_1
S : C
E F : PreOneHypercover.{w, v, u} 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 ⋯ ≫ Iso.hom (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)) =
    𝟙 (F.Y (e.hom.s₁ k))

Tactic:
simp