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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve Y
inst✝ : R.HasPullbacks f
⊢ (Presieve.pullbackArrows f R).FactorsThruAlong R f

Tactic:
intro Z g ⟨W, b, hb⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
R : Presieve Y
inst✝ : R.HasPullbacks f
Z : C
g : Z ⟶ X
W : C
b : W ⟶ Y
hb : R b
⊢ ∃ W_1 i e, R e ∧ i ≫ e = pullback.snd b f ≫ f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_1.transitive
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows

Tactic:
mem_iff_exists_zeroHypercover

Goal state after:
case refine_1.transitive
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
R : Presieve X
hR : ∃ 𝒰, R = Presieve.ofArrows 𝒰.X 𝒰.f
hle : R ≤ S.arrows
⊢ ∃ R ∈ J.coverings X, R ≤ T.arrows
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve (E.X i)
hR' : R' ∈ J.coverings (E.X i)
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows

Tactic:
mem_iff_exists_zeroHypercover

Goal state after:
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X✝ : C
S✝ : Sieve X✝
X : C
S T : Sieve X
hS : J.Saturate X S
hT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → J.Saturate Y (Sieve.pullback f T)
hleT : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → ∃ R ∈ J.coverings Y, R ≤ (Sieve.pullback f T).arrows
E : J.ZeroHypercover X
hle : Presieve.ofArrows E.X E.f ≤ S.arrows
i : E.I₀
R' : Presieve (E.X i)
hR' : ∃ 𝒰, R' = Presieve.ofArrows 𝒰.X 𝒰.f
hle' : R' ≤ (Sieve.pullback (E.f i) T).arrows
⊢ ∃ F, F.presieve₀ ≤ (Sieve.pullback (E.f i) T).arrows
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
F : Sheaf K A
H : Sheaf J A
f : (G.sheafPushforwardContinuous A J K).obj F ⟶ H
⊢ (G.op.ranAdjunction A).unit.app F.obj ≫
      G.op.ran.map ((G.sheafPushforwardContinuousCompSheafToPresheafIso A J K).inv.app F) ≫
        G.op.ran.map f.hom ≫ 𝟙 ((G.sheafPushforwardCocontinuous A J K).obj H).obj =
    ((G.op.ranAdjunction A).homEquiv F.obj H.obj) f.hom

Tactic:
erw [Functor.map_id, Category.comp_id, Category.id_comp,
          Adjunction.homEquiv_unit]

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
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 (Exists.choose ha) = G.map (a ≫ g)

Tactic:
rw [ha.choose_spec, Functor.map_comp_assoc, Functor.map_comp, fac]

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' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
i'' j'' : E.I₀
hii'' : i' = i''
hjj'' : j' = j''
k : E.I₁ i j
⊢ (congrIndexOneOfEq hii'' hjj'') ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) k

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j i'' j'' : E.I₀
k : E.I₁ i j
hii'' : i = i''
hjj'' : j = j''
⊢ (congrIndexOneOfEq hii'' hjj'') ((congrIndexOneOfEq ⋯ ⋯) k) = (congrIndexOneOfEq ⋯ ⋯) k
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
⊢ u₁ ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) (u₁ k)

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
k : E.I₁ i j
⊢ u₁ ((congrIndexOneOfEq ⋯ ⋯) k) = (congrIndexOneOfEq ⋯ ⋯) (u₁ 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✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i'✝ j✝ j'✝ : E✝.I₀
hii'✝ : i✝ = i'✝
hjj'✝ : j✝ = j'✝
E : PreOneHypercover S
i i' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq hii' hjj') k) = E.Y k

Tactic:
subst hii' hjj'

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✝
S : C
E✝ : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E✝.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ E.Y ((congrIndexOneOfEq ⋯ ⋯) k) = E.Y k
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' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).hom ≫ E.p₁ k = E.p₁ ((congrIndexOneOfEq hii' hjj') k) ≫ eqToHom ⋯

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ E.p₁ k = E.p₁ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯
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' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ E.p₁ ((congrIndexOneOfEq hii' hjj') k) = E.p₁ k ≫ eqToHom ⋯

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₁ ((congrIndexOneOfEq ⋯ ⋯) k) = E.p₁ k ≫ eqToHom ⋯
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' j j' : E.I₀
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ E.p₂ ((congrIndexOneOfEq hii' hjj') k) = E.p₂ k ≫ eqToHom ⋯

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
i j : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₂ ((congrIndexOneOfEq ⋯ ⋯) k) = E.p₂ k ≫ eqToHom ⋯
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✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i'✝ j✝ j'✝ : E.I₀
hii'✝ : i✝ = i'✝
hjj'✝ : j✝ = j'✝
i i' j j' : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ F.Y (u₁ i' j' ((congrIndexOneOfEq hii' hjj') k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))

Tactic:
subst hii' hjj'

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✝
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i✝ i' j✝ j' : E.I₀
hii' : i✝ = i'
hjj' : j✝ = j'
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ F.Y (u₁ i j ((congrIndexOneOfEq ⋯ ⋯) k)) = F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).hom ≫ z i j k =
    z i' j' ((congrIndexOneOfEq hii' hjj') k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).hom ≫ z i j k =
    z i j ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i i' j j' : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
hii' : i = i'
hjj' : j = j'
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso hii' hjj' k).inv ≫ z i' j' ((congrIndexOneOfEq hii' hjj') k) ≫ eqToHom ⋯ =
    z i j k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv

Tactic:
subst hii' hjj'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
i j : E.I₀
u₀ : E.I₀ → F.I₀
u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)
z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ z i j ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ =
    z i j k ≫ (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
⊢ PreservesColimitsOfShape J (proj B K)

Tactic:
by
  have : PreservesLimitsOfShape Jᵒᵖ (proj B K).op :=
    inferInstanceAs <| PreservesLimitsOfShape Jᵒᵖ <|
      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
  apply preservesColimitsOfShape_of_op

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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
T : C
g : T ⟶ W
j : E.I₁ i₁ i₂
h : T ⟶ E.Y j
fac₁ : g ≫ p₁ = h ≫ E.p₁ j
fac₂ : g ≫ p₂ = h ≫ E.p₂ j
⊢ c.ι i₁ ≫ F.obj.map (E.p₁ j).op ≫ F.obj.map h.op = c.ι i₂ ≫ F.obj.map (E.p₂ j).op ≫ F.obj.map h.op

Tactic:
simpa using! c.condition ⟨⟨i₁, i₂⟩, j⟩ =≫ F.obj.map h.op

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := ⋯
g₁' : W' ⟶ Y₁ := ⋯
g₂' : W' ⟶ Y₂ := ⋯
e : (Over.map f).obj W' ≅ W := ⋯
⊢ Over.Hom.left (g₁' ≫ g₁) = Over.Hom.left (g₂' ≫ g₂)

Tactic:
exact (Over.forget _).congr_map h

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

Goal state before:
pp: case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom (F.obj.map e.inv.op))
      ((ConcreteCategory.hom (((Over.map f).op ⋙ F.obj).map g₁'.op)) (x g₁ hg₁))

Tactic:
dsimp [e, W', g₁', g₂']

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₁.op)) (x g₁ hg₁) =
    (ConcreteCategory.hom (F.obj.map (Over.isoMk (Iso.refl W.left) ⋯).inv.op))
      ((ConcreteCategory.hom (F.obj.map ((Over.map f).map (Over.homMk (Over.Hom.left f₁) ⋯)).op)) (x g₁ hg₁))
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom (F.obj.map e.inv.op))
      ((ConcreteCategory.hom (((Over.map f).op ⋙ F.obj).map g₂'.op)) (x g₂ hg₂))

Tactic:
dsimp [e, W', g₁', g₂']

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X Y : C
f : X ⟶ Y
F : Sheaf (J.over Y) (Type u_1)
Z : Over X
x✝ : Presieve Z
x : Presieve.FamilyOfElements ((Over.map f).op ⋙ F.obj) x✝
hx : x.Compatible
Y₁ Y₂ : Over X
W : Over Y
f₁ : W ⟶ (Over.map f).obj Y₁
f₂ : W ⟶ (Over.map f).obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : x✝ g₁
hg₂ : x✝ g₂
h : f₁ ≫ (Over.map f).map g₁ = f₂ ≫ (Over.map f).map g₂
W' : Over X := Over.mk (Over.Hom.left f₁ ≫ Y₁.hom)
g₁' : W' ⟶ Y₁ := Over.homMk (Over.Hom.left f₁) ⋯
g₂' : W' ⟶ Y₂ := Over.homMk (Over.Hom.left f₂) ⋯
e : (Over.map f).obj W' ≅ W := Over.isoMk (Iso.refl ((Over.map f).obj W').left) ⋯
⊢ (ConcreteCategory.hom (F.obj.map f₂.op)) (x g₂ hg₂) =
    (ConcreteCategory.hom (F.obj.map (Over.isoMk (Iso.refl W.left) ⋯).inv.op))
      ((ConcreteCategory.hom (F.obj.map ((Over.map f).map (Over.homMk (Over.Hom.left f₂) ⋯)).op)) (x g₂ hg₂))
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
⊢ Function.Bijective F.sectionsPrecomp

Tactic:
by
  refine ⟨fun s₁ s₂ h ↦ ?_, fun t ↦ ?_⟩
  · ext Y
    let X : CostructuredArrow F Y := Classical.arbitrary _
    have := congr_fun (congr_arg Subtype.val h) X.left
    have h₁ := s₁.property X.hom
    have h₂ := s₂.property X.hom
    dsimp at this h₁ h₂
    rw [← h₁, this, h₂]
  · have h (Y : D) : ∃ (a : P.obj Y),
        ∀ (j : CostructuredArrow F Y), P.map j.hom (t.val j.left) = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ φ
      dsimp
      rw [← t.property φ.left]
      dsimp
      rw [← comp_apply, ← Functor.map_comp, CostructuredArrow.w]
    choose val hval using h
    refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
    · let X : CostructuredArrow F Y₁ := Classical.arbitrary _
      simp [← hval Y₁ X, ← hval Y₂ ((CostructuredArrow.map f).obj X)]
    · ext X : 2
      simpa using (hval (F.obj X) (CostructuredArrow.mk (𝟙 _))).symm

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi f

Tactic:
rw [← image.fac f]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑Y
⊢ hf.functor.obj ((map f).obj U) = hf.functor.obj ⊤ ⊓ U

Tactic:
by
  ext
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact ⟨⟨x, trivial, rfl⟩, hx⟩
  · rintro ⟨⟨x, -, rfl⟩, hx⟩
    exact ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.Sheaf

Goal state before:
pp: X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ s = t

Tactic:
refine (this.isSheafFor (.ofArrows V fun x ↦ homOfLE (hV x)) ?_).isSeparatedFor.ext ?_

Goal state after:
case refine_1
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ Sieve.generate (Presieve.ofArrows V fun x ↦ homOfLE ⋯) ∈ (Opens.grothendieckTopology ↑X) (unop U)

case refine_2
X : TopCat
A : Type u_1
inst✝⁵ : Category.{u, u_1} A
FC : A → A → Type u_2
CC : A → Type u
inst✝⁴ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory A FC
inst✝² : HasLimits A
inst✝¹ : PreservesLimits (forget A)
inst✝ : (forget A).ReflectsIsomorphisms
F : Presheaf A X
hF : F.IsSheaf
U : (Opens ↑X)ᵒᵖ
s t : ToType (F.obj U)
hst :
  ∀ x ∈ unop U,
    ∃ V,
      ∃ (hV : V ≤ unop U),
        x ∈ V ∧ (ConcreteCategory.hom (F.map (homOfLE hV).op)) s = (ConcreteCategory.hom (F.map (homOfLE hV).op)) t
this : Presieve.IsSheaf (Opens.grothendieckTopology ↑X) (F ⋙ forget A)
V : ↥(unop U) → Opens ↑X
hV : ∀ (x : ↥(unop U)), V x ≤ unop U
hxV : ∀ (x : ↥(unop U)), ↑x ∈ V x
H : ∀ (x : ↥(unop U)), (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) s = (ConcreteCategory.hom (F.map (homOfLE ⋯).op)) t
⊢ ∀ ⦃Y : Opens ↑X⦄ ⦃f : Y ⟶ unop U⦄,
    Presieve.ofArrows V (fun x ↦ homOfLE ⋯) f →
      (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) s = (ConcreteCategory.hom ((F ⋙ forget A).map f.op)) t
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case single
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i : ι
⊢ (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.single i)))) s =
    objPairwiseOfFamily sf (op (Pairwise.single i))

pp: case pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)))) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))

Tactic:
· exact h i

Goal state after:
case pair
X : TopCat
F : Presheaf (Type u_4) X
ι : Type u_5
U : ι → Opens ↑X
sf : (i : ι) → ToType (F.obj (op (U i)))
s : ToType (F.obj (op (iSup U)))
h : F.IsGluing U sf s
i j : ι
⊢ (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app (op (Pairwise.pair i j)))) s =
    objPairwiseOfFamily sf (op (Pairwise.pair i j))
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j) ↔
    F.IsSheafUniqueGluing

Tactic:
IsSheafUniqueGluing,

Goal state after:
X : TopCat
F : Presheaf (Type u_4) X
⊢ (∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X),
      ∀ s ∈ ((Pairwise.diagram U).op ⋙ F).sections,
        ∃! x,
          ∀ (j : (CategoryTheory.Pairwise ι)ᵒᵖ),
            (ConcreteCategory.hom ((Functor.mapCone F (Pairwise.cocone U).op).π.app j)) x = s j) ↔
    ∀ ⦃ι : Type x⦄ (U : ι → Opens ↑X) (sf : (i : ι) → ToType (F.obj (op (U i)))),
      F.IsCompatible U sf → ∃! s, F.IsGluing U sf s