-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma isLocallyInjective_of_injective (hφ : ∀ (X : Cᵒᵖ), Function.Injective (φ.app X)) :
    IsLocallyInjective J φ where
  equalizerSieve_mem {X} x y h

Proof state:
case h.e'_5
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve x y = ⊤

Tactic:
ext Y f

Result:
case h.e'_5.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (equalizerSieve x y).arrows f ↔ ⊤.arrows f

Proof state:
case h.e'_5.h.a
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) x) =
    (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) y)

Tactic:
simp [h]

Result:
no goals

Proof state:
case h.e'_5.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (equalizerSieve x y).arrows f ↔ ⊤.arrows f

Tactic:
simp only [equalizerSieve_apply, op_unop, Sieve.top_apply, iff_true]

Result:
case h.e'_5.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (ConcreteCategory.hom (F₁.map f.op)) x = (ConcreteCategory.hom (F₁.map f.op)) y

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
convert J.top_mem X.unop

Result:
case h.e'_5
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ equalizerSieve x y = ⊤

Proof state:
case h.e'_5.h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (ConcreteCategory.hom (F₁.map f.op)) x = (ConcreteCategory.hom (F₁.map f.op)) y

Tactic:
apply hφ

Result:
case h.e'_5.h.a
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hφ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
Y : C
f : Y ⟶ unop X
⊢ (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) x) =
    (ConcreteCategory.hom (φ.app (op Y))) ((ConcreteCategory.hom (F₁.map f.op)) y)