-- Mathlib/AlgebraicGeometry/Sites/Small.lean
lemma Cover.overEquiv_generate_toPresieveOver_eq_ofArrows {X : Over S} (𝒰 : Cover.{u} P X.left)
    [𝒰.Over S] : Sieve.overEquiv X (Sieve.generate 𝒰.toPresieveOver) =
      Sieve.ofArrows 𝒰.obj 𝒰.map

Proof state:
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
⊢ (Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver) = Sieve.ofArrows 𝒰.obj 𝒰.map

Tactic:
ext V f

Result:
case h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ ((Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver)).arrows f ↔ (Sieve.ofArrows 𝒰.obj 𝒰.map).arrows f

Proof state:
case h.mp.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Over S
k : 𝒰.J
h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ (𝒰.obj k).asOver S
hcomp : h ≫ Hom.asOver (𝒰.map k) S = Over.homMk f ⋯
⊢ ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

Tactic:
exact ⟨𝒰.obj k, h.left, 𝒰.map k, ⟨k⟩, congrArg CommaMorphism.left hcomp⟩

Result:
no goals

Proof state:
case h.mp
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

Tactic:
rintro ⟨U, h, g, ⟨k⟩, hcomp⟩

Result:
case h.mp.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Over S
k : 𝒰.J
h : CategoryTheory.Over.mk (f ≫ X.hom) ⟶ (𝒰.obj k).asOver S
hcomp : h ≫ Hom.asOver (𝒰.map k) S = Over.homMk f ⋯
⊢ ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

Proof state:
case h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ ((Sieve.overEquiv X) (Sieve.generate 𝒰.toPresieveOver)).arrows f ↔ (Sieve.ofArrows 𝒰.obj 𝒰.map).arrows f

Tactic:
simp only [Sieve.overEquiv_iff, Functor.const_obj_obj, Sieve.generate_apply]

Result:
case h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) ↔ ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

Proof state:
case h.mpr
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
rintro ⟨U, h, g, ⟨k⟩, hcomp⟩

Result:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Proof state:
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ h ≫ ((𝒰.obj k).asOver S).hom = (CategoryTheory.Over.mk (f ≫ X.hom)).hom

Tactic:
simp [← hcomp, this]

Result:
no goals

Proof state:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
refine ⟨(𝒰.obj k).asOver S, Over.homMk h (by simp [← hcomp, this]), (𝒰.map k).asOver S, ⟨k⟩, ?_⟩

Result:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ Over.homMk h ⋯ ≫ Hom.asOver (𝒰.map k) S = Over.homMk f ⋯

Proof state:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ Over.homMk h ⋯ ≫ Hom.asOver (𝒰.map k) S = Over.homMk f ⋯

Tactic:
ext : 1

Result:
case h.mpr.intro.intro.intro.intro.mk.h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ (Over.homMk h ⋯ ≫ Hom.asOver (𝒰.map k) S).left = (Over.homMk f ⋯).left

Proof state:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Tactic:
have : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S := comp_over (𝒰.map k) S

Result:
case h.mpr.intro.intro.intro.intro.mk
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯

Proof state:
case h.mpr.intro.intro.intro.intro.mk.h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
Y : Scheme
k : 𝒰.J
h : V ⟶ 𝒰.obj k
hcomp : h ≫ 𝒰.map k = f
this : 𝒰.map k ≫ X.hom = 𝒰.obj k ↘ S
⊢ (Over.homMk h ⋯ ≫ Hom.asOver (𝒰.map k) S).left = (Over.homMk f ⋯).left

Tactic:
simpa

Result:
no goals

Proof state:
case h
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) ↔ ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

Tactic:
constructor

Result:
case h.mp
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯) → ∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f

case h.mpr
P : MorphismProperty Scheme
S : Scheme
X : Over S
𝒰 : Cover P X.left
inst✝ : Cover.Over S 𝒰
V : Scheme
f : V ⟶ X.left
⊢ (∃ Y h g, Presieve.ofArrows 𝒰.obj 𝒰.map g ∧ h ≫ g = f) → ∃ Y h g, 𝒰.toPresieveOver g ∧ h ≫ g = Over.homMk f ⋯