mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ (ConcreteCategory.hom (P.map ((pullback.fst (F.map (f i)) (F.map (f j))).op ≫ (pullbackComparison F (f i) (f j)).op)))
        (x i) =
      (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)

Tactic:
Functor.map_comp,

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this✝¹ : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
x : (i : ι) → P.obj (Opposite.op (F.obj (Y i)))
i j : ι
this✝ : PreservesLimit (cospan (f i) (f j)) F
this : HasPullback (F.map (f i)) (F.map (f j))
⊢ (ConcreteCategory.hom
          (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op ≫ P.map (pullbackComparison F (f i) (f j)).op))
        (x i) =
      (ConcreteCategory.hom (P.map (F.map (pullback.snd (f i) (f j))).op)) (x j) ↔
    (ConcreteCategory.hom (P.map (pullback.fst (F.map (f i)) (F.map (f j))).op)) (x i) =
      (ConcreteCategory.hom (P.map (pullback.snd (F.map (f i)) (F.map (f j))).op)) (x j)
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
⊢ (FamilyOfElements.functorPushforward G x).Compatible

Tactic:
rintro Z₁ Z₂ W g₁ g₂ f₁' f₂' H₁ H₂ eq
  unfold FamilyOfElements.functorPushforward
  rcases getFunctorPushforwardStructure H₁ with ⟨X₁, f₁, h₁, hf₁, rfl⟩
  rcases getFunctorPushforwardStructure H₂ with ⟨X₂, f₂, h₂, hf₂, rfl⟩
  suffices ℱ.obj.map (g₁ ≫ h₁).op (x f₁ hf₁) = ℱ.obj.map (g₂ ≫ h₂).op (x f₂ hf₂) by
    simpa using this
  apply hG.compatible ℱ h _ _ hf₁ hf₂
  simpa using eq

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
⊢ (FunctorPushforwardStructure.casesOn (getFunctorPushforwardStructure ⋯) fun Z_1 g h h₁ fac ↦
      (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁)) =
    x f hf

Tactic:
rcases getFunctorPushforwardStructure (image_mem_functorPushforward G T hf) with
    ⟨X, g, f', hg, eq⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
hG : CompatiblePreserving K G
ℱ : Sheaf K (Type w)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
h : x.Compatible
Y : C
f : Y ⟶ Z
hf : T f
X : C
g : X ⟶ Z
f' : G.obj Y ⟶ G.obj X
hg : T g
eq : G.map f = f' ≫ G.map g
⊢ (FunctorPushforwardStructure.casesOn { preobj := X, premap := g, lift := f', cover := hg, fac := eq }
      fun Z_1 g h h₁ fac ↦ (ConcreteCategory.hom (ℱ.obj.map h.op)) (x g h₁)) =
    x f hf
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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.IsCocontinuous J K
this : G.IsRightAdjoint
⊢ CoverPreserving K J G

Tactic:
← adj.isCocontinuous_iff_coverPreserving

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.IsCocontinuous J K
this : G.IsRightAdjoint
⊢ F.IsCocontinuous J K
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ Sieve.pullback f (E.sieve₁ p₁ p₂) ≤ E.sieve₁ (f ≫ p₁) (f ≫ p₂)

Tactic:
intro Z

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
⊢ ∀ (f_1 : Z ⟶ T), (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows f_1 → (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows f_1
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
⊢ E.sieve₁ (f ≫ p₁) (f ≫ p₂) ≤ Sieve.pullback f (E.sieve₁ p₁ p₂)

Tactic:
intro Z

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
T : C
f : T ⟶ W
Z : C
⊢ ∀ (f_1 : Z ⟶ T), (E.sieve₁ (f ≫ p₁) (f ≫ p₂)).arrows f_1 → (Sieve.pullback f (E.sieve₁ p₁ p₂)).arrows f_1
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₁.unit.app F ≫
      G.op.ran.map
        (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F) ≫
          (sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))

Tactic:
Functor.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    (adj₁.homEquiv F ((sheafToPresheaf J A).obj ((presheafToSheaf K A ⋙ G.sheafPushforwardContinuous A J K).obj F)))
      (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F))
Module: Mathlib.CategoryTheory.Sites.CoverLifting

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
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map
          ((sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))) ≫
        adj₁.counit.app
          ((sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F))) =
    ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₃.unit.app F) ≫
      ((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map (adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)) ≫
        adj₁.counit.app
          ((sheafToPresheaf J A).obj ((G.sheafPushforwardContinuous A J K).obj ((presheafToSheaf K A).obj F)))

Tactic:
congr 3

Goal state after:
case e_a.e_a
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
G : C ⥤ D
A : Type w
inst✝⁵ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝⁴ : G.IsCocontinuous J K
inst✝³ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F
inst✝² : G.IsContinuous J K
inst✝¹ : HasWeakSheafify J A
inst✝ : HasWeakSheafify K A
F : Dᵒᵖ ⥤ A
adj₁ : (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op ⊣ G.op.ran := G.op.ranAdjunction A
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
adj₃ : presheafToSheaf K A ⊣ sheafToPresheaf K A := sheafificationAdjunction K A
adj₄ : G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K := G.sheafAdjunctionCocontinuous A J K
eq :
  adj₁.unit.app F ≫
      G.op.ran.map (adj₂.unit.app (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj F)) ≫
        G.op.ran.map ((sheafToPresheaf J A).map (((adj₁.comp adj₂).leftAdjointUniq (adj₃.comp adj₄)).hom.app F)) =
    adj₃.unit.app F ≫ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F))
⊢ (sheafToPresheaf K A).map (adj₄.unit.app ((presheafToSheaf K A).obj F)) =
    adj₁.unit.app ((presheafToSheaf K A ⋙ sheafToPresheaf K A).obj F)
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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ Exists.choose ha) =
    G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ Exists.choose ha')

Tactic:
Functor.map_comp,

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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map (Exists.choose ha) =
    G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ Exists.choose ha')
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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map (Exists.choose ha) =
    G.map ({ Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ Exists.choose ha')

Tactic:
Functor.map_comp,

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
G : C ⥤ D
A : Type u_4
inst✝¹ : Category.{v_4, u_4} A
inst✝ : IsDenseSubsite J K G
F : Sheaf J A
X Y : C
f : G.obj X ⟶ G.obj Y
W₀ : C
a : W₀ ⟶ X
ha : (↑⟨G.imageSieve f, ⋯⟩).arrows a
W₀' : C
a' : W₀' ⟶ X
ha' : (↑⟨G.imageSieve f, ⋯⟩).arrows a'
T₀ : C
p₁ : T₀ ⟶ { Y := W₀, f := a, hf := ha }.Y
p₂ : T₀ ⟶ { Y := W₀', f := a', hf := ha' }.Y
fac : p₁ ≫ { Y := W₀, f := a, hf := ha }.f = p₂ ≫ { Y := W₀', f := a', hf := ha' }.f
⊢ G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₁ ≫ G.map (Exists.choose ha) =
    G.map { Z := T₀, g₁ := p₁, g₂ := p₂, w := fac }.g₂ ≫ G.map (Exists.choose ha')
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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map a ≫ G.map p ≫ f = G.map (a ≫ g)

Tactic:
Functor.map_comp,

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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ G.map a ≫ G.map p ≫ f = G.map a ≫ G.map g
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)
k : E.I₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map ((F.p₁ (f.s₁ k.snd)).op ≫ (f.h₁ k.snd).op) =
    d.ι (f.s₀ k.fst.2) ≫ P.map (f.h₁ k.snd ≫ F.p₂ (f.s₁ k.snd)).op

Tactic:
Functor.map_comp,

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₁'
heq : d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op = d.ι (f.s₀ k.fst.2) ≫ P.map (F.p₂ (f.s₁ k.snd)).op
⊢ d.ι (f.s₀ k.fst.1) ≫ P.map (F.p₁ (f.s₁ k.snd)).op ≫ P.map (f.h₁ k.snd).op =
    d.ι (f.s₀ k.fst.2) ≫ P.map (f.h₁ k.snd ≫ F.p₂ (f.s₁ k.snd)).op
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback (𝟙 Y) (Sieve.pullback (f ≫ g) R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
rw [pullback_id, pullback_comp] at this

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
this : Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
⊢ imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a) ≤
    Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))

Tactic:
intro W q ⟨x, h⟩

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
hh :
  Sieve.functorPushforward H (imageSieve (H.op.whiskerLeft f) ((ConcreteCategory.hom (G.map m.op)) a)) ∈
    K (H.obj (Opposite.unop (Opposite.op Z)))
W : C
q : W ⟶ Z
x : ToType ((H.op ⋙ F).obj (Opposite.op W))
h :
  (ConcreteCategory.hom ((H.op.whiskerLeft f).app (Opposite.op W))) x =
    (ConcreteCategory.hom ((H.op ⋙ G).map q.op)) ((ConcreteCategory.hom (G.map m.op)) a)
⊢ (Sieve.functorPullback H (Sieve.pullback m (imageSieve f a))).arrows q
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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = g.h₁ k ≫ F.p₁ (f.s₁ k, g.s₁ k).2 ≫ F.f (__spread✝⁻⁰.s₀ i✝).2

Tactic:
g.w₁₁_assoc k

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 : PreOneHypercover S
F : PreOneHypercover S
G✝ : PreOneHypercover S
inst✝¹ : ∀ (i : E.I₀) (j : F.I₀), HasPullback (E.f i) (F.f j)
inst✝ : ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), HasPullback (E.p₁ k ≫ E.f i) (F.p₁ l ≫ F.f a)
G : PreOneHypercover S
f : G.Hom E
g : G.Hom F
i✝ j✝ : G.I₀
k : G.I₁ i✝ j✝
⊢ G.p₁ k ≫ f.h₀ i✝ ≫ E.f (__spread✝⁻⁰.s₀ i✝).1 = G.p₁ k ≫ g.h₀ i✝ ≫ F.f (__spread✝⁻⁰.s₀ i✝).2
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
⊢ functorPullback F ((overEquiv ((Over.post F).obj U)) S) ≤ (overEquiv U) (functorPullback (Over.post F) S)

Tactic:
intro Z

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
⊢ ∀ (f : Z ⟶ U.left),
    (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows f →
      ((overEquiv U) (functorPullback (Over.post F) S)).arrows f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
· intro h
    rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h
    rw [h, zero_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cocone F
⊢ c.pt ∈ upperBounds (Set.range F.obj)

Tactic:
intro x ⟨i, p⟩; rw [← p]; exact (c.ι.app i).le

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

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
⊢ ∀ b ∈ Set.range F.obj, s.pt ≤ b

Tactic:
rintro _ ⟨j, rfl⟩

Goal state after:
α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cone F
j : J
⊢ s.pt ≤ F.obj j
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cocone F
⊢ ∀ b ∈ Set.range F.obj, b ≤ s.pt

Tactic:
rintro _ ⟨j, rfl⟩

Goal state after:
α : Type u
inst✝¹ : CompleteLattice α
J : Type w
inst✝ : Category.{w', w} J
F : J ⥤ α
s : Cocone F
j : J
⊢ F.obj j ≤ s.pt
Module: Mathlib.CategoryTheory.Sites.Spaces

Goal state before:
pp: case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1

Tactic:
obtain ⟨i, hi⟩ := hU (x := x)
    exact ⟨U i, ⟨homOfLE le_top, ⟨i, ⟨𝟙 _⟩⟩⟩, hi⟩

Goal state after: