-- Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean
theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S : Sieve X) :
    K _ (S.functorPushforward G) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S

Proof state:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
hS : K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
intro hS

Result:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
hS : K (G.obj X) (Sieve.functorPushforward G S)
⊢ ∃ T, Sieve.functorPullback G ↑T = S

Proof state:
case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → K (G.obj X) (Sieve.functorPushforward G S)

Tactic:
rintro ⟨T, rfl⟩

Result:
case mpr.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
T : ↑(K (G.obj X))
⊢ K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ K (G.obj X) (Sieve.functorPushforward G S) ↔ ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ K (G.obj X) (Sieve.functorPushforward G S) → ∃ T, Sieve.functorPullback G ↑T = S

case mpr
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ (∃ T, Sieve.functorPullback G ↑T = S) → K (G.obj X) (Sieve.functorPushforward G S)

Proof state:
case mpr.intro
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
D : Type u_2
inst✝³ : Category.{u_4, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
T : ↑(K (G.obj X))
⊢ K (G.obj X) (Sieve.functorPushforward G (Sieve.functorPullback G ↑T))

Tactic:
exact LocallyCoverDense.functorPushforward_functorPullback_mem T

Result:
no goals