-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isSheafFor_iff_generate (R : Presieve X) :
    IsSheafFor P R ↔ IsSheafFor P (generate R : Presieve X)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ IsSheafFor P R ↔ IsSheafFor P (generate R).arrows

Tactic:
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSheafFor P (generate R).arrows

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
t : P.obj (op X)
ht : x.sieveExtend.IsAmalgamation t
⊢ x.IsAmalgamation t

Tactic:
simpa [hx] using isAmalgamation_restrict (le_generate R) _ _ ht

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
rw [← isSeparatedFor_iff_generate]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSheafFor P (generate R).arrows

Tactic:
rw [← isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P (generate R).arrows ∧
      ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro q x hx

Result:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), x.sieveExtend.IsAmalgamation a → x.IsAmalgamation a

Tactic:
intro t ht

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
t : P.obj (op X)
ht : x.sieveExtend.IsAmalgamation t
⊢ x.IsAmalgamation t

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
apply Exists.imp _ (q _ (hx.restrict (le_generate R)))

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), (FamilyOfElements.restrict ⋯ x).IsAmalgamation a → x.IsAmalgamation a

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
t : P.obj (op X)
ht : (FamilyOfElements.restrict ⋯ x).IsAmalgamation t
⊢ x.IsAmalgamation t

Tactic:
simpa [hx] using isAmalgamation_sieveExtend _ _ ht

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
    ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
intro q x hx

Result:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Tactic:
apply and_congr (Iff.refl _)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
⊢ (∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
    ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t

Proof state:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∃ t, x.IsAmalgamation t

Tactic:
apply Exists.imp _ (q _ hx.sieveExtend)

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P R
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), x.sieveExtend.IsAmalgamation a → x.IsAmalgamation a

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
⊢ ∀ (a : P.obj (op X)), (FamilyOfElements.restrict ⋯ x).IsAmalgamation a → x.IsAmalgamation a

Tactic:
intro t ht

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
q : ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t
x : FamilyOfElements P (generate R).arrows
hx : x.Compatible
t : P.obj (op X)
ht : (FamilyOfElements.restrict ⋯ x).IsAmalgamation t
⊢ x.IsAmalgamation t