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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ (∃! t, x.IsAmalgamation t) ↔ ∃! x_1, (ConcreteCategory.hom (forkMap P R)) x_1 = (firstObjEqFamily P R).toEquiv.symm x

Tactic:
apply existsUnique_congr

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
⊢ ∀ (a : P.obj (op X)),
    x.IsAmalgamation a ↔ (ConcreteCategory.hom (forkMap P R)) a = (firstObjEqFamily P R).toEquiv.symm x
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ Nonempty (IsLimit (P.mapCone S.arrows.cocone.op)) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.Compatible → ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows f✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
U : C
S : Sieve U
Y✝ : C
f✝ : Y✝ ⟶ e.inverse.obj (e.functor.obj U)
⊢ (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f✝ ↔ (pullback (e.unitInv.app U) S).arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X : C
S : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ (𝟭 C).obj X
⊢ (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f✝ ↔ S.arrows f✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
⊢ (∀ (i : Cone (S.arrows.diagram.op ⋙ P)), Nonempty (Unique (i ⟶ P.mapCone S.arrows.cocone.op))) ↔
    ∀ (E : Aᵒᵖ) (x : FamilyOfElements (P ⋙ coyoneda.obj E) S.arrows), x.SieveCompatible → ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ Multiequalizer.ι ((unop S).index P) ((Cover.Arrow.base I).map f.unop) =
    Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I ((J.pullback f✝).map f.unop)).base

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹ : Category.{w', w} D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
X Y : C
f✝ : X ⟶ Y
S T : (J.Cover Y)ᵒᵖ
f : S ⟶ T
I : (unop ((J.pullback f✝).op.obj T)).shape.L
⊢ Multiequalizer.ι ((unop S).index P) ((Cover.Arrow.base I).map f.unop) =
    Multiequalizer.ι ((unop S).index P) (Cover.Arrow.map I ((J.pullback f✝).map f.unop)).base
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
⊢ (∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i) ↔
    ∃! x_1,
      (ConcreteCategory.hom (forkMap P X π)) x_1 =
        (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)

Tactic:
apply existsUnique_congr

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
⊢ ∀ (a : P.obj (op B)),
    (∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) a = x i) ↔
      (ConcreteCategory.hom (forkMap P X π)) a =
        (Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv.symm ((equivShrink ((j : I) → P.obj (op (X j)))) x)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case mk
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
Y✝ : C
f✝ : Y✝ ⟶ Y
hf✝ : (↑(S.pullback f)).arrows f✝
⊢ ↑x { Y := Y✝, f := f✝, hf := hf✝ }.base =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ f, hf := ⋯ }

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
Y✝ : C
f✝ : Y✝ ⟶ Y
hf✝ : (↑(S.pullback f)).arrows f✝
⊢ ↑x { Y := Y✝, f := f✝, hf := hf✝ }.base =
    ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ f, hf := ⋯ }
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
X✝ : Sheaf J A
m✝ : X✝ ⟶ terminal J hX
⊢ m✝ = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X✝.obj }

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
X✝ : Sheaf J A
m✝ : X✝ ⟶ terminal J hX
⊢ m✝ = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X✝.obj }
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
X✝ : Sheaf J A
m✝ : X✝ ⟶ terminal J hX
x✝ : Cᵒᵖ
⊢ m✝.hom.app x✝ = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X✝.obj }.hom.app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
X : A
hX : IsTerminal X
X✝ : Sheaf J A
m✝ : X✝ ⟶ terminal J hX
x✝ : Cᵒᵖ
⊢ m✝.hom.app x✝ = { hom := (Functor.isTerminalConst Cᵒᵖ hX).from X✝.obj }.hom.app x✝
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
⊢ x.IsAmalgamation (hh.lift K) ∧ ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation y → y = hh.lift K

Tactic:
;

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
h : ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))
E : A
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op E)) S.arrows
hx : x.Compatible
T : J.Cover X := ⟨S, hS⟩
hh : IsLimit (T.multifork P)
K : Multifork (T.index P) := Multifork.ofι (T.index P) E (fun I ↦ x I.f ⋯) ⋯
⊢ x.IsAmalgamation (hh.lift K) ∧ ∀ (y : E ⟶ P.obj (op X)), x.IsAmalgamation y → y = hh.lift K
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x✝¹ : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) x = y i
right✝ :
  ∀ (y_1 : (fun X ↦ X) (P.obj (op B))),
    (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = y i) y_1 → y_1 = x
x✝ : I
⊢ ↑(Arrows.toCompatible P π x) x✝ = ↑⟨y, hy⟩ x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h :
  ∀ (x : (i : I) → P.obj (op (X i))),
    Arrows.Compatible P π x → ∃! t, ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i
x✝¹ : Subtype (Arrows.Compatible P π)
y : (i : I) → P.obj (op (X i))
hy : Arrows.Compatible P π y
x : P.obj (op B)
hx : ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) x = y i
right✝ :
  ∀ (y_1 : (fun X ↦ X) (P.obj (op B))),
    (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = y i) y_1 → y_1 = x
x✝ : I
⊢ ↑(Arrows.toCompatible P π x) x✝ = ↑⟨y, hy⟩ x✝
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π ↑(Arrows.toCompatible P π y)
y' : (fun X ↦ X) (P.obj (op B))
hy' : (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = ↑(Arrows.toCompatible P π y) i) y'
x✝ : I
⊢ ↑(Arrows.toCompatible P π y') x✝ = ↑(Arrows.toCompatible P π y) x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type u_1
X : I → C
π : (i : I) → X i ⟶ B
h : Function.Bijective (Arrows.toCompatible P π)
y : P.obj (op B)
hx : Arrows.Compatible P π ↑(Arrows.toCompatible P π y)
y' : (fun X ↦ X) (P.obj (op B))
hy' : (fun t ↦ ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = ↑(Arrows.toCompatible P π y) i) y'
x✝ : I
⊢ ↑(Arrows.toCompatible P π y') x✝ = ↑(Arrows.toCompatible P π y) x✝
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (⊤.index P))
              (fun I_1 ↦ Multiequalizer.ι (⊤.index P) (I_1.map e)) ⋯ ≫
            Multiequalizer.ι ((S.pullback I.f).index P) i))
      (↑x I) =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫
          Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((Meq.equiv P S).symm x)

Tactic:
Multiequalizer.lift_ι,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          Multiequalizer.ι (⊤.index P) (Cover.Arrow.map i e)))
      (↑x I) =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫
          Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((Meq.equiv P S).symm x)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom
        (Multiequalizer.lift (⊤.index P) (P.obj (op I.Y)) (fun I_1 ↦ P.map I_1.f.op) ⋯ ≫
          Multiequalizer.ι (⊤.index P) (Cover.Arrow.map i e)))
      (↑x I) =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫
          Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((Meq.equiv P S).symm x)

Tactic:
Multiequalizer.lift_ι,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
I : S.Arrow
e : (J.pullback I.f).obj (unop (op S)) ⟶ ⊤ := homOfLE ⋯
i : (unop (op ((J.pullback I.f).obj (unop (op S))))).shape.L
⊢ (ConcreteCategory.hom (P.map (Cover.Arrow.map i e).f.op)) (↑x I) =
    (ConcreteCategory.hom
        (Multiequalizer.lift ((S.pullback I.f).index P) (multiequalizer (S.index P))
            (fun I_1 ↦ Multiequalizer.ι (S.index P) I_1.base) ⋯ ≫
          Multiequalizer.ι ((S.pullback I.f).index P) i))
      ((Meq.equiv P S).symm x)
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
⊢ ∀ (S T : (J.Cover (unop X))ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P (unop X)).map f)

Tactic:
intro S T e

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
hP : ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)
X : Cᵒᵖ
S T : (J.Cover (unop X))ᵒᵖ
e : S ⟶ T
⊢ IsIso ((J.diagram P (unop X)).map e)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_2.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑x ({ Y := Y✝, f := f✝, hf := hf✝ }.map h1.unop)

Tactic:
;

Goal state after:
case e'_2.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑x { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑x ({ Y := Y✝, f := f✝, hf := hf✝ }.map h1.unop)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: case e'_3.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑y { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑y ({ Y := Y✝, f := f✝, hf := hf✝ }.map h2.unop)

Tactic:
;

Goal state after:
case e'_3.mk
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
X : C
P : Cᵒᵖ ⥤ D
S T : J.Cover X
x : Meq P S
y : Meq P T
h : mk x = mk y
W : (J.Cover X)ᵒᵖ
h1 : op S ⟶ W
h2 : op T ⟶ W
Y✝ : C
f✝ : Y✝ ⟶ X
hf✝ : (↑(unop W)).arrows f✝
hh :
  (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h1)) ((Meq.equiv P S).symm x)) =
    (ConcreteCategory.hom (Multiequalizer.ι ((unop W).index P) { Y := Y✝, f := f✝, hf := hf✝ }))
      ((ConcreteCategory.hom ((J.diagram P X).map h2)) ((Meq.equiv P T).symm y))
e_1✝ :
  ToType (P.obj (op { Y := Y✝, f := f✝, hf := hf✝ }.Y)) = CD (((unop W).index P).left { Y := Y✝, f := f✝, hf := hf✝ })
⊢ ↑y { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f, hf := ⋯ } =
    ↑y ({ Y := Y✝, f := f✝, hf := hf✝ }.map h2.unop)