-- Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
lemma Functor.isCoverDense_of_generate_singleton_functor_π_mem (G : C ⥤ D)
    (K : GrothendieckTopology D)
    (h : ∀ B, ∃ (X : C) (f : G.obj X ⟶ B), Sieve.generate (Presieve.singleton f) ∈ K B) :
    G.IsCoverDense K where
  is_cover B

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝¹ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f✝ : G.obj X ⟶ B
h✝ : Sieve.generate (Presieve.singleton f✝) ∈ K B
Y : D
f : Y ⟶ B
Z : D
g : Y ⟶ Z
w✝ : Z ⟶ B
h : Presieve.singleton f✝ w✝
w : g ≫ w✝ = f
⊢ (Sieve.coverByImage G B).arrows f

Tactic:
cases h

Result:
case intro.intro.mk
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f✝ : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f✝) ∈ K B
Y : D
f : Y ⟶ B
g : Y ⟶ G.obj X
w : g ≫ f✝ = f
⊢ (Sieve.coverByImage G B).arrows f

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.coverByImage G B ∈ K B

Tactic:
refine K.superset_covering ?_ h

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
⊢ Sieve.coverByImage G B ∈ K B

Tactic:
obtain ⟨X, f, h⟩ := h B

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.coverByImage G B ∈ K B

Proof state:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f) ∈ K B
⊢ Sieve.generate (Presieve.singleton f) ≤ Sieve.coverByImage G B

Tactic:
intro Y f ⟨Z, g, _, h, w⟩

Result:
case intro.intro
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝¹ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f✝ : G.obj X ⟶ B
h✝ : Sieve.generate (Presieve.singleton f✝) ∈ K B
Y : D
f : Y ⟶ B
Z : D
g : Y ⟶ Z
w✝ : Z ⟶ B
h : Presieve.singleton f✝ w✝
w : g ≫ w✝ = f
⊢ (Sieve.coverByImage G B).arrows f

Proof state:
case intro.intro.mk
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_5, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
h✝ : ∀ (B : D), ∃ X f, Sieve.generate (Presieve.singleton f) ∈ K B
B : D
X : C
f✝ : G.obj X ⟶ B
h : Sieve.generate (Presieve.singleton f✝) ∈ K B
Y : D
f : Y ⟶ B
g : Y ⟶ G.obj X
w : g ≫ f✝ = f
⊢ (Sieve.coverByImage G B).arrows f

Tactic:
exact ⟨⟨_, g, _, w⟩⟩

Result:
no goals