-- Mathlib/CategoryTheory/Sites/PreservesLocallyBijective.lean
lemma isLocallyInjective_of_whisker (hH : CoverPreserving J K H)
    [H.IsCoverDense K] [IsLocallyInjective J (whiskerLeft H.op f)] : IsLocallyInjective K f where
  equalizerSieve_mem {X} a b h

Proof state:
case h.hS.refine_1
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
W : C
q : W ⟶ Z
hq : (equalizerSieve ((ConcreteCategory.hom (F.map map.op)) a) ((ConcreteCategory.hom (F.map map.op)) b)).arrows q
⊢ (Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))).arrows q

Tactic:
simpa using hq

Result:
no goals

Proof state:
case h
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
⊢ Sieve.pullback lift (Sieve.pullback map (equalizerSieve a b)) ∈ K Y

Tactic:
apply K.pullback_stable

Result:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
⊢ Sieve.pullback map (equalizerSieve a b) ∈ K (H.obj Z)

Proof state:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
⊢ equalizerSieve a b ∈ K (Opposite.unop X)

Tactic:
apply K.transitive (H.is_cover_of_isCoverDense K X.unop)

Result:
case h
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
⊢ ∀ ⦃Y : D⦄ ⦃f : Y ⟶ Opposite.unop X⦄,
    (Sieve.coverByImage H (Opposite.unop X)).arrows f → Sieve.pullback f (equalizerSieve a b) ∈ K Y

Proof state:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
⊢ Sieve.pullback map (equalizerSieve a b) ∈ K (H.obj Z)

Tactic:
refine K.superset_covering (Sieve.functorPullback_pushforward_le H _) ?_

Result:
case h.hS
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
⊢ Sieve.functorPushforward H (Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))) ∈ K (H.obj Z)

Proof state:
case h.hS.refine_2
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{u_6, u_1} C
inst✝⁵ : Category.{u_7, u_2} D
inst✝⁴ : Category.{u_8, 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✝ : IsLocallyInjective J (whiskerLeft H.op f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
map : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ map = g
⊢ (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map map.op)) a) =
    (ConcreteCategory.hom (f.app (Opposite.op (H.obj Z)))) ((ConcreteCategory.hom (F.map map.op)) b)

Tactic:
rw [NatTrans.naturality_apply, NatTrans.naturality_apply, h]

Result:
no goals