-- Mathlib/CategoryTheory/Sites/Coherent/LocallySurjective.lean
lemma coherentTopology.presheafIsLocallySurjective_iff {F G : Cᵒᵖ ⥤ D} (f : F ⟶ G)
    [Preregular C] [FinitaryPreExtensive C] [PreservesFiniteProducts F] [PreservesFiniteProducts G]
      [PreservesFiniteProducts (forget D)] :
        Presheaf.IsLocallySurjective (coherentTopology C) f ↔
          Presheaf.IsLocallySurjective (regularTopology C) f

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) (whiskerRight f (forget D))

Tactic:
exact regularTopology.isLocallySurjective_sheaf_of_types _

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)

Tactic:
exact (Coverage.gi _).gc.monotone_l le_sup_right

Result:
no goals

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f

Tactic:
refine Presheaf.isLocallySurjective_of_le (J := regularTopology C) ?_ _

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ coherentTopology C

Proof state:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f → Presheaf.IsLocallySurjective (regularTopology C) f

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget,
  Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)]

Result:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) (whiskerRight f (forget D)) →
    Presheaf.IsLocallySurjective (regularTopology C) (whiskerRight f (forget D))

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f ↔ Presheaf.IsLocallySurjective (regularTopology C) f

Tactic:
constructor

Result:
case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f → Presheaf.IsLocallySurjective (regularTopology C) f

case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ coherentTopology C

Tactic:
rw [← extensive_regular_generate_coherent]

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Category.{u_5, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ regularTopology C ≤ Coverage.toGrothendieck C (extensiveCoverage C ⊔ regularCoverage C)