-- Mathlib/CategoryTheory/Sites/Sieves.lean
lemma mem_functorPushforward_iff_of_full [F.Full] {X Y : C} (R : Sieve X) (f : F.obj Y ⟶ F.obj X) :
    (R.arrows.functorPushforward F) f ↔ ∃ (g : Y ⟶ X), F.map g = f ∧ R g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
⊢ Presieve.functorPushforward F R.arrows f ↔ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
refine ⟨fun ⟨Z, g, h, hg, hcomp⟩ ↦ ?_, fun ⟨g, hcomp, hg⟩ ↦ ?_⟩

Result:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
⊢ ∃ g, F.map g = f ∧ R.arrows g

case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f

Proof state:
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ f = 𝟙 (F.obj Y) ≫ F.map g

Tactic:
simp [hcomp]

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ R.arrows (h' ≫ g)

Tactic:
apply R.downward_closed hg

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f

Tactic:
use Y, g, 𝟙 _, hg

Result:
case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ f = 𝟙 (F.obj Y) ≫ F.map g

Proof state:
case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
⊢ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
obtain ⟨h', hh'⟩ := F.map_surjective h

Result:
case refine_1.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ ∃ g, F.map g = f ∧ R.arrows g

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)

Tactic:
simp only [Functor.map_comp, hh', hcomp, true_and]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ R.arrows (h' ≫ g)

Proof state:
case refine_1.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ ∃ g, F.map g = f ∧ R.arrows g

Tactic:
use h' ≫ g

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : Presieve.functorPushforward F R.arrows f
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
hg : R.arrows g
hcomp : f = h ≫ F.map g
h' : Y ⟶ Z
hh' : F.map h' = h
⊢ F.map (h' ≫ g) = f ∧ R.arrows (h' ≫ g)