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

Goal state before:
pp: case refine_4
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'
t₁' :
  Nonempty
    (IsColimit
      (Cofan.mk (pullback c₂.inr i) fun j ↦
        pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯))
⊢ Nonempty (IsColimit c)

Tactic:
obtain ⟨H₁⟩ := t₁'

Goal state after:
case refine_4
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 }) ⋯)
⊢ Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))

Tactic:
have eq₂ := NatTrans.naturality_apply f.hom g₂.op (t f₂ hf₂)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
eq₂ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (t f₂ hf₂))
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (left_id = left_id)

Tactic:
simp only [diagram.injEq]

Goal state after:
case left_id.left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable (right_id = right_id)

Tactic:
simp only [diagram.injEq]

Goal state after:
case right_id.right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
⊢ Decidable True
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (left j✝ = left j✝)

Tactic:
simp only [diagram.injEq]

Goal state after:
case left.left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable (right j✝ = right j✝)

Tactic:
simp only [diagram.injEq]

Goal state after:
case right.right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ : J
⊢ Decidable True
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (diagram f✝¹ = diagram f✝)

Tactic:
simp only [diagram.injEq]

Goal state after:
case diagram.diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
j✝ k✝ : J
f✝¹ f✝ : j✝ ⟶ k✝
⊢ Decidable (f✝¹ = f✝)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyCoflat F.op ↔ RepresentablyFlat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyCoflat F.op
X : D
⊢ IsCofiltered (StructuredArrow X F)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyFlat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F.op (op X))
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)
Module: Mathlib.CategoryTheory.Functor.Flat

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type v₁
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
F : C ⥤ D
inst✝ : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow := { app := fun X ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this✝ : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ hc.lift (c.extend (Hom.right g₁)) = hc.lift (c.extend (Hom.right g₂))

Tactic:
by
      congr

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ (↑(x f hf)).arrows u

Tactic:
Sieve.mem_iff_pullback_eq_top,

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
hx : x.SieveCompatible
M : Sieve X := Sieve.bind S.arrows fun Y f hf ↦ ↑(x f hf)
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
u : Z ⟶ Y
W : C
g : Z ⟶ W
f' : W ⟶ X
hf' : S.arrows f'
hg : (↑(x f' hf')).arrows g
c : g ≫ f' = u ≫ f
⊢ Sieve.pullback u ↑(x f hf) = ⊤
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ ((c X) R).arrows f

Tactic:
Sieve.mem_iff_pullback_eq_top,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
c : (X : C) → ClosureOperator (Sieve X)
hc : ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : Sieve X), (c Y) (Sieve.pullback f S) = Sieve.pullback f ((c X) S)
X : C
S : Sieve X
hS : (c X) S = ⊤
R : Sieve X
hR : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.pullback f R ∈ {S | (c Y) S = ⊤}
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f ((c X) R) = ⊤
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ F.presieve₀ ∈ J.coverings S

Tactic:
refine Precoverage.RespectsIso.of_forall_exists_iso ?_ ?_ hE

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), E.presieve₀ g → ∃ Y e, F.presieve₀ (e.hom ≫ g)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
E F : PreZeroHypercover S
e : E ≅ F
hE : E.presieve₀ ∈ J.coverings S
⊢ ∀ ⦃Z : C⦄ (g : Z ⟶ S), F.presieve₀ g → ∃ Y e, E.presieve₀ (e.hom ≫ g)
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ (E.map F).sieve₀ = Sieve.functorPushforward F E.sieve₀

Tactic:
by
  rw [PreZeroHypercover.sieve₀, Sieve.ofArrows, ← PreZeroHypercover.presieve₀,
    PreOneHypercover.map_toPreZeroHypercover, PreZeroHypercover.presieve₀_map,
    Sieve.generate_map_eq_functorPushforward]

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

Goal state before:
pp: case refine_1
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K.toGrothendieck ≤ J
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ R ∈ J.toPrecoverage.coverings X

pp: case refine_2
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
⊢ K.toGrothendieck ≤ J

Tactic:
· rw [GrothendieckTopology.mem_toPrecoverage_iff]
    exact h _ (generate_mem_toGrothendieck hR)

Goal state after:
case refine_2
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K : Precoverage C
J : GrothendieckTopology C
h : K ≤ J.toPrecoverage
⊢ K.toGrothendieck ≤ J
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
P : Sheaf K E
⊢ ((F.sheafPushforwardContinuous E J K).map
          ({ app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).unit.app P.obj }, naturality := ⋯ }.app P) ≫
        { app := fun P ↦ { hom := (Adjunction.whiskerLeft E adj.op).counit.app P.obj }, naturality := ⋯ }.app
          ((F.sheafPushforwardContinuous E J K).obj P)).hom =
    (𝟙 ((F.sheafPushforwardContinuous E J K).obj P)).hom

Tactic:
exact (adj.op.whiskerLeft _).left_triangle_components P.obj

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

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
⊢ Sieve.functorPullback F (Sieve.pullback (e.hom.app U) S) ≤ Sieve.functorPullback G S

Tactic:
intro Y f (hf : S.arrows (F.map f ≫ e.hom.app U))

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F G : C ⥤ D
e : F ≅ G
inst✝ : F.IsCocontinuous J K
U : C
S : Sieve (G.obj U)
hS : S ∈ K (G.obj U)
Y : C
f : Y ⟶ U
hf : S.arrows (F.map f ≫ e.hom.app U)
⊢ (Sieve.functorPullback G S).arrows f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case e_a.e_a
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' : Y' ⟶ unop U
hf' : (Sieve.coverByImage G (unop U)).arrows f'
⊢ (ConcreteCategory.hom (appHom (homOver α (unop X)) (unop U))) x ≫ ℱ'.obj.map (Nonempty.some hf').map.op =
    (x ≫ ℱ.map (Nonempty.some hf').map.op) ≫ α.app (op (Nonempty.some hf').1)

Tactic:
exact (appHom_restrict (homOver α (unop X)) hf'.some.map.op x).trans (by simp)

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

Goal state before:
pp: case e_6
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse := ⋯
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := ⋯
⊢ (adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
      ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    (presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g

Tactic:
apply adj₁.homEquiv_naturality_left

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

Goal state before:
pp: case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      eqToHom ⋯ ≫ e.hom.h₁ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))

Tactic:
← eqToHom_naturality_assoc _ (by simp)

Goal state after:
case h
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S✝ : C
E✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
e : E ≅ F
i j : E.I₀
k : E.I₁ i j
⊢ e.inv.h₁ (e.hom.s₁ k) ≫
      e.hom.h₁ (e.inv.s₁ (e.hom.s₁ k)) ≫ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (e.hom.s₁ k)).hom =
    𝟙 (F.Y (e.hom.s₁ k))
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹) F.op

Tactic:
apply +allowSynthFailures createsLimitsOfShapeOp

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteCoproducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesColimitsOfShape (Discrete x✝¹)ᵒᵖ F
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : C ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ D
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
F : Cᵒᵖ ⥤ Dᵒᵖ
inst✝ : CreatesFiniteProducts F
x✝¹ : Type
x✝ : Fintype x✝¹
⊢ CreatesLimitsOfShape (Discrete x✝¹)ᵒᵖ F

Tactic:
exact createsLimitsOfShapeOfEquiv (Discrete.opposite _).symm _

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.fst ≫ biprod.inl + biprod.snd ≫ biprod.inr = biprod.fst ≫ biprod.inl ↔ IsZero Y

Tactic:
add_eq_left

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_2
C✝¹ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C✝¹
D✝ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁹ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁸ : Category.{v₄, u₄} D''
J✝¹ : GrothendieckTopology C✝¹
K✝ : GrothendieckTopology D✝
F✝ : C✝¹ ⥤ D✝
S✝ : Sheaf J✝¹ RingCat
R✝¹ : Sheaf K✝ RingCat
inst✝⁷ : F✝.IsContinuous J✝¹ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝¹ K✝).obj R✝¹
C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
J✝ : GrothendieckTopology C✝
K : GrothendieckTopology D
F : C✝ ⥤ D
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J✝ K
inst✝³ : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝² : Category.{v', u'} C
inst✝¹ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
x✝¹ : (Over X)ᵒᵖ
x✝ : ↑((R.over X).obj.obj x✝¹)
⊢ (RingCat.Hom.hom
        (((R.pushforwardOverMapIso f).inv.hom ≫
              (Over.map f).op.whiskerLeft (R.toPushforwardOverPullback f).hom ≫
                whiskerRight (NatTrans.op (Over.mapPullbackAdj f).unit) (R.over X).obj).app
          x✝¹))
      x✝ =
    (RingCat.Hom.hom ((𝟙 (R.over X).obj).app x✝¹)) x✝

Tactic:
simp [← Functor.map_comp, ← op_comp, Sheaf.pushforwardOverMapIso]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case pair.single
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (single i')
⊢ ∃ l,
    List.IsChain Zag ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l) ∧
      ({ left := { as := PUnit.unit }, right := Pairwise.pair i j, hom := a } :: l).getLast ⋯ =
        { left := { as := PUnit.unit }, right := single i', hom := b }

Tactic:
refine
          ⟨[{   left := ⟨⟨⟩⟩
                right := single i
                hom := ObjectProperty.homMk (homOfLE (a.hom.le.trans (by simp))) },
              { left := ⟨⟨⟩⟩
                right := pair i i'
                hom := ObjectProperty.homMk (homOfLE
                  (le_inf ((a.hom.le).trans (by simp)) b.hom.le)) }, _],
                ?_, rfl⟩
        exact
          List.IsChain.cons_cons
            (Or.inl
              ⟨{  left := 𝟙 _
                  right := left i j }⟩)
            (List.IsChain.cons_cons
              (Or.inr
                ⟨{  left := 𝟙 _
                    right := left i i' }⟩)
              (List.IsChain.cons_cons
                (Or.inl
                  ⟨{  left := 𝟙 _
                      right := right i i' }⟩)
                (List.IsChain.singleton _)))

Goal state after: