-- 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
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)

Tactic:
refine K.superset_covering (Sieve.functorPushforward_monotone H _ ?_)
  (hH.cover_preserve <| equalizerSieve_mem J (whiskerLeft H.op f)
    (F.map map.op a) (F.map map.op b) ?_)

Result:
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
⊢ equalizerSieve ((ConcreteCategory.hom (F.map map.op)) a) ((ConcreteCategory.hom (F.map map.op)) b) ≤
    Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))

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 ((whiskerLeft H.op f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map map.op)) a) =
    (ConcreteCategory.hom ((whiskerLeft H.op f).app (Opposite.op Z))) ((ConcreteCategory.hom (F.map map.op)) b)

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 g (equalizerSieve a b) ∈ K Y

Tactic:
rw [← fac, Sieve.pullback_comp]

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
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

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
⊢ equalizerSieve ((ConcreteCategory.hom (F.map map.op)) a) ((ConcreteCategory.hom (F.map map.op)) b) ≤
    Sieve.functorPullback H (Sieve.pullback map (equalizerSieve a b))

Tactic:
intro W q hq

Result:
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