mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_4.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι.app j)
      ((mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)).app j) i (c₂.ι.app j)

Tactic:
rintro ⟨⟨⟩⟩

Goal state after:
case refine_4.refine_2.left
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι.app { as := WalkingPair.left })
    ((mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)).app { as := WalkingPair.left }) i
    (c₂.ι.app { as := WalkingPair.left })

case refine_4.refine_2.right
C : Type u
inst✝¹ : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι.app { as := WalkingPair.right })
    ((mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i)).app { as := WalkingPair.right }) i
    (c₂.ι.app { as := WalkingPair.right })
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
· intro
    constructor <;> infer_instance

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

Goal state before:
pp: case mp
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsIso ((sheafCompose J (forget A)).map f)

Tactic:
← isLocallyBijective_iff_isIso'

Goal state after:
case mp
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
left✝ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsLocallyInjective ((sheafCompose J (forget A)).map f) ∧ IsLocallySurjective ((sheafCompose J (forget A)).map f)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mpr
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F G : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
· intro
    constructor <;> infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
j : Fin (n + 1)
⊢ IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ }))

Tactic:
let F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
    have : F = Discrete.functor F' := by
      apply Functor.hext
      · exact fun i ↦ rfl
      · rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
        simp [F']
    clear_value F'
    subst this
    apply BinaryCofan.IsColimit.mk _ (fun {T} f₁ f₂ ↦ Hc.desc (Cofan.mk T (Fin.cases f₁
      (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))))
    · intro T f₁ f₂
      simp only [Discrete.functor_obj, pair_obj_left, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inl, IsColimit.fac, Cofan.mk_pt, Cofan.mk_ι_app,
        Fin.cases_zero]
    · intro T f₁ f₂
      simp only [Discrete.functor_obj, pair_obj_right, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inr]
      ext j
      simp only [colimit.ι_desc_assoc, Discrete.functor_obj, Cofan.mk_pt,
        Cofan.mk_ι_app, IsColimit.fac, Fin.cases_succ]
    · intro T f₁ f₂ f₃ m₁ m₂
      simp only [Discrete.functor_obj_eq_as, pair_obj_left, BinaryCofan.mk_pt, const_obj_obj,
        BinaryCofan.mk_inl, pair_obj_right, BinaryCofan.mk_inr] at m₁ m₂ ⊢
      refine Hc.uniq (Cofan.mk T (Fin.cases f₁
        (fun i ↦ Sigma.ι (fun (j : Fin n) ↦ (Discrete.functor F').obj ⟨j.succ⟩) _ ≫ f₂))) _ ?_
      intro ⟨j⟩
      simp only [Discrete.functor_obj, Cofan.mk_pt, Cofan.mk_ι_app]
      induction j using Fin.inductionOn
      · simp only [Fin.cases_zero, m₁]
      · simp only [← m₂, colimit.ι_desc_assoc, Discrete.functor_obj,
          Cofan.mk_pt, Cofan.mk_ι_app, Fin.cases_succ]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone v (f i)
hs : (i : ι) → IsLimit (s i)
t : PullbackCone v u
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd ≫ a.inj i
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.fst =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (s i).fst ((s i).snd ≫ a.inj i) ⋯).inj p ≫ t.fst

Tactic:
simp [he₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.fst =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).inj p ≫ t.fst

Tactic:
simp [he₁]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
⊢ IsPullback (Cofan.IsColimit.desc hd fun x ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v

Tactic:
obtain ⟨hc⟩ := hau.nonempty_isColimit_of_isPullback_right f u
    v q₁ q₂ hP (IsPullback.of_hasPullback _ _) c (Iso.refl _)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ IsPullback (Cofan.IsColimit.desc hd fun x ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
s : Cocone (K ⋙ sigmaConst.obj R)
j : J
⊢ ((sigmaConst.obj R).mapCocone c).ι.app j ≫ Sigma.desc (hc.desc (coconeTypes s)) = s.ι.app j

Tactic:
by
        dsimp
        ext k
        simp [dsimp% hc.fac_apply, dsimp% Sigma.ι_desc (hc.desc (coconeTypes s)), coconeTypes]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
s : Cocone (K ⋙ sigmaConst.obj R)
m : ((sigmaConst.obj R).mapCocone c).pt ⟶ s.pt
hm : ∀ (j : J), ((sigmaConst.obj R).mapCocone c).ι.app j ≫ m = s.ι.app j
⊢ m = Sigma.desc (hc.desc (coconeTypes s))

Tactic:
dsimp
        ext x
        obtain ⟨j, k, rfl⟩ := Functor.CoconeTypes.IsColimit.ι_jointly_surjective hc x
        simp [coconeTypes, ← hm, dsimp% hc.fac_apply,
          dsimp% Sigma.ι_desc (hc.desc (coconeTypes s))]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r 0) = (ConcreteCategory.hom (A.obj.map f.op)) 0

Tactic:
(A.obj.map f.op).hom.map_zero,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X : Cᵒᵖ
r : ↑(R.obj.obj X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
⊢ (ConcreteCategory.hom (A.obj.map f.op)) (smul α φ r 0) = 0
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr.a
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ ≤ J₂

Tactic:
apply le_topology_of_closedSieves_isSheaf
      rw [h]
      apply classifier_isSheaf

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ E.X i ≅ F.X ((Equiv.refl E.I₀) i)

Tactic:
match i with
      | .inl i => dsimp [E, F]; symm; exact eR _ _
      | .inr i => dsimp [E, F]; apply eT

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

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ f = u ≫ F.map (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
· simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h
      apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _)) <;>
        simp [← h.left, ← h.right, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
k : E.I₁ i₁ i₂
⊢ E.toPullback k ≫ pullback.fst (E.f i₁) (E.f i₂) = E.p₁ k

Tactic:
by
  rw [pullback.lift_fst]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
f₂ : Y₂ ⟶ X
h₂ : coverByImage G X f₂
l₂ : CoverByImageStructure G f₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ f₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift).op))
      ((ConcreteCategory.hom (α.app (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)))
        ((ConcreteCategory.hom (ℱ.map { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ l₂.lift).op))
      ((ConcreteCategory.hom (α.app (op l₂.1))) ((ConcreteCategory.hom (ℱ.map l₂.map.op)) x))

Tactic:
obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
K : GrothendieckTopology D
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
this :
  ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
W₂ : C
iYW₂ : Y₂ ⟶ G.obj W₂
iWX₂ : G.obj W₂ ⟶ X
h₂ : coverByImage G X (iYW₂ ≫ iWX₂)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ iYW₂ ≫ iWX₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift).op))
      ((ConcreteCategory.hom (α.app (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)))
        ((ConcreteCategory.hom (ℱ.map { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.lift).op))
      ((ConcreteCategory.hom (α.app (op { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.1)))
        ((ConcreteCategory.hom (ℱ.map { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.map.op)) x))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
⊢ ∀ ⦃Y_1 : C⦄ (f_1 : G.obj Y_1 ⟶ unop Y),
    (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (ℱ.map f ≫ appHom α (unop Y))).toFun x) =
      (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (appHom α (unop X) ≫ ℱ'.obj.map f)).toFun x)

Tactic:
intro Y'

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
⊢ ∀ (f_1 : G.obj Y' ⟶ unop Y),
    (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (ℱ.map f ≫ appHom α (unop Y))).toFun x) =
      (ConcreteCategory.hom (ℱ'.obj.map f_1.op)) ((ConcreteCategory.hom (appHom α (unop X) ≫ ℱ'.obj.map f)).toFun x)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x)).IsAmalgamation
    (f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x)

Tactic:
intro Y'

Goal state after:
case h
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
Y' : D
⊢ ∀ (f_1 : Y' ⟶ unop U) (h : (Sieve.coverByImage G (unop U)).arrows f_1),
    (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop Y))).map f_1.op))
        (f.unop ≫ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x) =
      pushforwardFamily (homOver α (unop Y)) (f.unop ≫ x) f_1 h
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ pullback.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1

Tactic:
have : p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = p ≫ pullback.snd _ _ ≫ pullback.fst _ _ := by
          simp [p]

Goal state after:
case refine_1.refine_2.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
this :
  p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    p ≫
      pullback.snd ((E.inter F).f i) ((E.inter F).f j) ≫
        pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst)
          (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd)
⊢ pullback.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1