-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem toGrothendieck_eq_sInf (K : Coverage C) : toGrothendieck _ K =
    sInf {J | K ≤ ofGrothendieck _ J }

Proof state:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ K.covering X
⊢ S ∈ (ofGrothendieck C (toGrothendieck C K)).covering X

Tactic:
apply Saturate.of _ _ hS

Result:
no goals

Proof state:
case a.a.top
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
X✝ : C
⊢ ⊤ ∈ J X✝

Tactic:
apply J.top_mem

Result:
no goals

Proof state:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ ∀ b ∈ {J | K ≤ ofGrothendieck C J}, toGrothendieck C K ≤ b

Tactic:
intro J hJ

Result:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
⊢ toGrothendieck C K ≤ J

Proof state:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
⊢ toGrothendieck C K ≤ J

Tactic:
intro X S hS

Result:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ (toGrothendieck C K) X
⊢ S ∈ J X

Proof state:
case a.a.of.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.covering X
⊢ S ∈ K.covering X

Tactic:
assumption

Result:
no goals

Proof state:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ∈ {J | K ≤ ofGrothendieck C J}

Tactic:
intro X S hS

Result:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
X : C
S : Presieve X
hS : S ∈ K.covering X
⊢ S ∈ (ofGrothendieck C (toGrothendieck C K)).covering X

Proof state:
case a.a.of
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.covering X
⊢ Sieve.generate S ∈ J X

Tactic:
apply hJ

Result:
case a.a.of.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
hS : S ∈ K.covering X
⊢ S ∈ K.covering X

Proof state:
case a.a.transitive
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
a✝¹ : K.Saturate X R
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → K.Saturate Y (Sieve.pullback f S)
H1 : R ∈ J X
H2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → Sieve.pullback f S ∈ J Y
⊢ S ∈ J X

Tactic:
exact J.transitive H1 _ H2

Result:
no goals

Proof state:
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K

Tactic:
apply sInf_le

Result:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ∈ {J | K ≤ ofGrothendieck C J}

Proof state:
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}

Tactic:
apply le_sInf

Result:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ ∀ b ∈ {J | K ≤ ofGrothendieck C J}, toGrothendieck C K ≤ b

Proof state:
case a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ ofGrothendieck C J}
X : C
S : Sieve X
hS : S ∈ (toGrothendieck C K) X
⊢ S ∈ J X

Tactic:
induction hS with
| of X S hS => apply hJ; assumption
| top => apply J.top_mem
| transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K = sInf {J | K ≤ ofGrothendieck C J}

Tactic:
apply le_antisymm

Result:
case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ toGrothendieck C K ≤ sInf {J | K ≤ ofGrothendieck C J}

case a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
K : Coverage C
⊢ sInf {J | K ≤ ofGrothendieck C J} ≤ toGrothendieck C K