mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      𝟙 (L₁.obj ((𝟭 C₁).obj (F.obj X₂))) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app ((𝟭 C₂).obj X₂) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)

Tactic:
id_comp,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : adj.unit.app (F.obj X₂) ≫ F.map (adj.counit.app X₂) = 𝟙 (F.obj X₂)
⊢ (𝟭 D₁).map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫ (CatCommSq.iso F L₂ L₁ F').hom.app ((𝟭 C₂).obj X₂) =
    (NatTrans.id (F' ⋙ 𝟭 D₁)).app (L₂.obj X₂)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
⊢ P.isoClosure.isColocal g → P.isColocal g

Tactic:
intro hg X hX
    exact hg _ (P.le_isoClosure _ hX)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : D
f : X ⟶ Y
⊢ isLocal (fun x ↦ x ∈ Set.range F.obj) f ↔ IsIso (G.map f)

Tactic:
by
  have := adj.unit.naturality f
  dsimp at this
  rw [← (isLocal (· ∈ Set.range F.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
    this, (isLocal (· ∈ Set.range F.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X),
    isLocal_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]
  exact ⟨fun _ ↦ isIso_of_fully_faithful F (G.map f), fun _ ↦ inferInstance⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr → Nonempty (IsColimit c')

Tactic:
· rintro ⟨H₁, H₂⟩
    refine ⟨IsColimit.ofIsoColimit ?_ <| (isoBinaryCofanMk _).symm⟩
    let e₁ : X' ≅ _ := H₁.isLimit.conePointUniqueUpToIso (limits _ _)
    let e₂ : Y' ≅ _ := H₂.isLimit.conePointUniqueUpToIso (limits _ _)
    have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp [e₁]
    have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp [e₂]
    rw [he₁, he₂]
    exact (BinaryCofan.mk _ _).isColimitCompRightIso e₂.hom
      ((BinaryCofan.mk _ _).isColimitCompLeftIso e₁.hom (h₂ f))

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
⊢ IsSheaf J (F.op ⋙ G)

Tactic:
intro X S hS

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : GrothendieckTopology C
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
K : GrothendieckTopology D
inst✝ : LocallySmall.{w, v_1, u_1} C
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type w) ⥤ Dᵒᵖ ⥤ Type w
adj : H ⊣ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type w)).obj F.op
h : ∀ ⦃X : C⦄ ⦃S : Sieve X⦄, S ∈ J X → K.W (H.map (Sieve.shrinkFunctor.{w, v_1, u_1} S).ι)
G : Dᵒᵖ ⥤ Type w
hG : IsSheaf K G
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsSheafFor (F.op ⋙ G) S.arrows
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: 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 α
⊢ Nonempty (IsColimit c) ↔
    ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)

Tactic:
refine ⟨?_, isUniversalColimit_extendCofan f t₁.isUniversal t₂.isUniversal c α i e hα⟩

Goal state after:
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 α
⊢ Nonempty (IsColimit c) →
    ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_3.zero
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
t₂' :
  ∀ (j : Discrete WalkingPair),
    IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).ι.app j)
      ((mapPair (α.app { as := 0 }) (Sigma.desc fun b ↦ α.app { as := b.succ } ≫ c₁.inj b)).app j) i (c₂.ι.app j)
⊢ IsPullback (c.ι.app { as := 0 }) (α.app { as := 0 }) i ((extendCofan c₁ c₂).ι.app { as := 0 })

Tactic:
exact t₂' ⟨WalkingPair.left⟩

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hd : projectiveDimension X = ⊥
⊢ HasProjectiveDimensionLE X 0

Tactic:
by simp [← projectiveDimension_le_iff, hd]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
⊢ (Hom.hom S.g).ker = (Hom.hom S'.g ∘ₛₗ ↑e2).ker

Tactic:
comm,

Goal state after:
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
⊢ (Hom.hom S.g).ker = (↑e' ∘ₛₗ Hom.hom S.g).ker
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
⊢ Presieve.IsSheaf J₁ (Functor.closedSieves J₁).toFunctor

Tactic:
intro X S hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ Presieve.IsSheafFor (Functor.closedSieves J₁).toFunctor S.arrows
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
⊢ J₁ ≤ J₂

Tactic:
intro X S hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : Presieve.IsSheaf J₁ (Functor.closedSieves J₂).toFunctor
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ S ∈ J₂ X
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreZeroHypercover S
e : E ≅ F
i : E.I₀
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
by
  obtain ⟨hs, hh⟩ := Hom.ext'_iff.mp e.hom_inv_id
  simpa using hh i

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ K.coverings X

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))

Tactic:
· rwa [← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)] at hE

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
this : F.presieve₀ = Presieve.ofArrows (fun i ↦ F.X i.fst) fun i ↦ e.inv.h₀ i.fst ≫ E.f (e.inv.s₀ i.fst)
⊢ ∀ (i : F.I₀), (Presieve.ofArrows (fun k ↦ F.X i) fun k ↦ e.inv.h₀ i) ∈ K.coverings (E.X (e.inv.s₀ i))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S

Tactic:
obtain ⟨ι, Y, f, h⟩ := E.presieve₀.exists_eq_ofArrows

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : Precoverage C
S T : C
E : J.ZeroHypercover S
ι : Type (max u v)
Y : ι → C
f : (i : ι) → Y i ⟶ S
h : E.presieve₀ = Presieve.ofArrows Y f
⊢ ∃ ι f, (E.restrictIndex f).presieve₀ ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ K.toGrothendieck ∈ {J | K ≤ J.toCoverage}

Tactic:
intro X S hS

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ K.coverings X
⊢ S ∈ K.toGrothendieck.toCoverage.coverings X
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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ J X → K.W (H'.map (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S).ι)

Tactic:
intro X S hS

Goal state after:
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
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
⊢ K.W (H'.map (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S).ι)
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)
Y : C
f : Y ⟶ U
hf : S.arrows (F.map f ≫ e.hom.app U)
this : S.arrows (e.inv.app Y ≫ F.map f ≫ e.hom.app U)
⊢ (Sieve.functorPullback G S).arrows f

Tactic:
e.hom.naturality f,

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)
this : S.arrows (e.inv.app Y ≫ e.hom.app Y ≫ G.map f)
⊢ (Sieve.functorPullback G S).arrows f
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.snd (E.f i₁) (E.f i₂) = E.p₂ k

Tactic:
pullback.lift_snd

Goal state after:
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.p₂ k = E.p₂ k
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: 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
f : E.Hom F
g : F.Hom G
⊢ ∀ {i j : E.I₀} (k : E.I₁ i j), (f.h₁ k ≫ g.h₁ (f.s₁ k)) ≫ G.p₁ ((g.s₁ ∘ f.s₁) k) = E.p₁ k ≫ (f.comp g.toHom).h₀ i

Tactic:
by simp [w₁₁, w₁₁_assoc]

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

Goal state before:
pp: 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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
⊢ ∀ (b : E.multicospanShape.R),
    (d.ι (f.s₀ (E.multicospanShape.fst b)) ≫ P.map (f.h₀ (E.multicospanShape.fst b)).op) ≫
        (E.multicospanIndex P).fst b =
      (d.ι (f.s₀ (E.multicospanShape.snd b)) ≫ P.map (f.h₀ (E.multicospanShape.snd b)).op) ≫
        (E.multicospanIndex P).snd b

Tactic:
intro (k : E.I₁')

Goal state after:
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
f : E.Hom F
P : Cᵒᵖ ⥤ A
c : Multifork (E.multicospanIndex P)
hc : IsLimit c
d : Multifork (F.multicospanIndex P)
k : E.I₁'
⊢ (d.ι (f.s₀ (E.multicospanShape.fst k)) ≫ P.map (f.h₀ (E.multicospanShape.fst k)).op) ≫ (E.multicospanIndex P).fst k =
    (d.ι (f.s₀ (E.multicospanShape.snd k)) ≫ P.map (f.h₀ (E.multicospanShape.snd k)).op) ≫ (E.multicospanIndex P).snd k
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
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
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g

Tactic:
let adj₁ := (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction

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
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 :=
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyOfIsEquivalence J K G A).map f ≫ g) =
    f ≫ (sheafifyHomEquivOfIsEquivalence J K G) g
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
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 (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
        ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
      ((presheafToSheaf J A).map (G.op.whiskerLeft f) ≫ (adj₁.homEquiv ((presheafToSheaf J A).obj (G.op ⋙ P₂)) Q) g) =
    G.op.whiskerLeft f ≫
      (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g)

Tactic:
· apply adj₂.homEquiv_naturality_left

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
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 : Dᵒᵖ ⥤ A
Q₁ Q₂ : Sheaf K A
f : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁
g : Q₁ ⟶ Q₂
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
⊢ (sheafifyHomEquivOfIsEquivalence J K G) (f ≫ g) = (sheafifyHomEquivOfIsEquivalence J K G) f ≫ g.hom

Tactic:
let adj₁ := (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction

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
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 : Dᵒᵖ ⥤ A
Q₁ Q₂ : Sheaf K A
f : (sheafifyOfIsEquivalence J K G A).obj P ⟶ Q₁
g : Q₁ ⟶ 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 :=
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
⊢ (sheafifyHomEquivOfIsEquivalence J K G) (f ≫ g) = (sheafifyHomEquivOfIsEquivalence J K G) f ≫ g.hom
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
⊢ J ≤ finestTopology Ps

Tactic:
intro X S hS

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Ps : Set (Cᵒᵖ ⥤ Type w)
J : GrothendieckTopology C
hJ : ∀ P ∈ Ps, Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ S ∈ (finestTopology Ps) X
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : Precoverage D
⊢ (comap F K).toGrothendieck ≤ F.restrictedTopology K.toGrothendieck

Tactic:
Functor.restrictedTopology

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : Precoverage D
⊢ (comap F K).toGrothendieck ≤ (comap F K.toGrothendieck.toPrecoverage).toGrothendieck
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (G.restrictedTopology K) U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)

Tactic:
Functor.restrictedTopology

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
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ (Precoverage.comap G K.toPrecoverage).toGrothendieck U✝
⊢ Sieve.functorPushforward G S✝ ∈ K (G.obj U✝)