awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
i : 𝒰.I₀
⊢ 𝒰.f i ≫
      𝒰.glueMorphisms
          (fun (i : 𝒰.I₀) ↦
            CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
          ⋯ ≫
        f =
    𝒰.f i ≫ 𝟙 Y

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
X Y : C
f : X ⟶ Y
𝒰 : J.ZeroHypercover Y
H : ∀ (i : 𝒰.I₀), IsIso (X := pullback f (𝒰.f i)) (pullback.snd f (𝒰.f i))
⊢ 𝒰.glueMorphisms
        (fun (i : 𝒰.I₀) ↦
          CategoryStruct.comp (Y := pullback f (𝒰.f i)) (inv (pullback.snd f (𝒰.f i))) (pullback.fst f (𝒰.f i)))
        ⋯ ≫
      f =
    𝟙 Y

Tactic:
exact 𝒰.hom_ext fun i ↦ by simp [pullback.condition]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.hom_ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
i : (pullback₁ fst 𝒰).I₀
⊢ (pullback₁ fst 𝒰).f i ≫ fst ≫ f = (pullback₁ fst 𝒰).f i ≫ snd ≫ g

Tactic:
simpa [pullback.condition_assoc] using (H i).w

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
⊢ fst ≫ f = snd ≫ g

Tactic:
have h : fst ≫ f = snd ≫ g := (𝒰.pullback₁ fst).hom_ext fun i ↦ by
    simpa [pullback.condition_assoc] using (H i).w
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
this : IsIso (Y := pullback f g) (pullback.lift fst snd h)
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom (asIso (pullback.lift fst snd h))) (pullback.fst f g) = fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
this : IsIso (Y := pullback f g) (pullback.lift fst snd h)
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom (asIso (pullback.lift fst snd h))) (pullback.snd f g) = snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
suffices : IsIso (Y := pullback f g) (pullback.lift fst snd h)
⊢ IsPullback fst snd f g

Tactic:
suffices IsIso (pullback.lift fst snd h) from
    .of_iso_pullback ⟨h⟩ (asIso (pullback.lift _ _ h)) (by simp) (by simp)
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
simp_rw :
  ∀ (i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))),
    IsIso (X :=
      pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
      (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
⊢ IsIso (Y := pullback f g) (pullback.lift fst snd h)

Tactic:
simp_rw [← isomorphisms.iff, IsLocalAtTarget.iff_of_zeroHypercover (P := isomorphisms C)
    (𝒰.pullbackCoverOfLeft f g), isomorphisms.iff]

Premises used: CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover, CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
⊢ (𝒰.f i ≫ f) ≫ 𝟙 Z = 𝒰.f i ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
⊢ g ≫ 𝟙 Z = 𝟙 Y ≫ g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)

Tactic:
simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), m] using .of_hasPullback _ _

Premises used: CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
⊢ IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)

Tactic:
have : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst _ _) := by
    simpa [← IsPullback.paste_vert_iff (.of_hasPullback _ _), m] using .of_hasPullback _ _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ Z) (pullback.snd fst (𝒰.f i) ≫ 𝒰.f i ≫ f) ((pullback.fst fst (𝒰.f i) ≫ snd) ≫ g)

Tactic:
simp [← h, pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
h₀ :
  Eq (α := pullback fst (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.fst f g))
    ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g)
h₁ :
  Eq (α := pullback fst (𝒰.f i) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.snd f g))
    ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.snd f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h)
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ X)
    (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.fst f g))
    ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.fst f g)

Tactic:
simp [m, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ Eq (α := pullback fst (𝒰.f i) ⟶ Y)
    (CategoryStruct.comp (Y := pullback f g) (pullback.fst fst (𝒰.f i) ≫ pullback.lift fst snd h) (pullback.snd f g))
    ((pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ m) ≫ pullback.snd f g)

Tactic:
simp [m, pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
rw :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.fst (𝒰.f i ≫ f) g))
    (CategoryStruct.comp (Y := pullback f g) (pullback.lift fst snd h) (pullback.fst f g)) (𝒰.f i)
⊢ IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m

Tactic:
rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [m, pullback.condition])]

Premises used: CategoryTheory.IsPullback.paste_vert_iff, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (CategoryStruct.comp (Y := pullback (𝒰.f i ≫ f) g)
      (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.fst (𝒰.f i ≫ f) g))
    (CategoryStruct.comp (Y := pullback f g) (pullback.lift fst snd h) (pullback.fst f g)) (𝒰.f i)

Tactic:
simpa using .of_hasPullback _ _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m

Tactic:
have H' : IsPullback (pullback.fst fst (𝒰.f i))
      (pullback.lift (pullback.snd _ _) (pullback.fst _ _ ≫ snd)
        (by simp [← h, pullback.condition_assoc]))
      (pullback.lift fst snd h) m := by
    rw [← IsPullback.paste_vert_iff this.flip (by ext <;> simp [m, pullback.condition])]
    simpa using .of_hasPullback _ _
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
rw :
  CategoryStruct.comp (Y :=
      pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
      (Iso.hom H'.isoPullback)
      (pullback.snd (pullback.lift fst snd h)
        (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)) =
    Iso.hom ⋯.isoPullback
⊢ Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)

Tactic:
rw [Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
⊢ Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)

Tactic:
have heq : pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i) =
      H'.isoPullback.inv ≫ (H i).isoPullback.hom := by
    rw [Iso.eq_inv_comp]
    cat_disch
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
heq :
  Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)
rw :
  IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)) (Y :=
    PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))

Tactic:
rw [heq]
-- Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
Goal:
C : Type u
inst : Category.{v, u} C
J : Precoverage.{v, u} C
inst_1 : J.toGrothendieck.Subcanonical
inst_2 : Limits.HasPullbacks.{v, u} C
inst_3 : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H :
  ∀ (i : 𝒰.I₀),
    IsPullback (P := pullback fst (𝒰.f i)) (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : PreZeroHypercover.I₀ (S := pullback f g) (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g))
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
H' :
  IsPullback (P := pullback fst (𝒰.f i)) (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯) (pullback.lift fst snd h) m
heq :
  Eq (α :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i) ⟶
      PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (pullback.snd (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i))
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)
⊢ IsIso (X :=
    pullback (pullback.lift fst snd h) (PreZeroHypercover.f (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)) (Y :=
    PreZeroHypercover.X (toPreZeroHypercover (𝒰.pullbackCoverOfLeft f g)) i)
    (Iso.inv H'.isoPullback ≫ Iso.hom ⋯.isoPullback)

Tactic:
infer_instance