-- Mathlib/CategoryTheory/Sites/Coverage.lean
theorem isSheaf_sup (K L : Coverage C) (P : Cᵒᵖ ⥤ Type*) :
    (Presieve.IsSheaf ((K ⊔ L).toGrothendieck C)) P ↔
    (Presieve.IsSheaf (K.toGrothendieck C)) P ∧ (Presieve.IsSheaf (L.toGrothendieck C)) P

Proof state:
case inr
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ L.covering X
⊢ IsSheafFor P R

Tactic:
exact h.2 R hR

Result:
no goals

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
⊢ IsSheaf (toGrothendieck C (K ⊔ L)) P ↔ IsSheaf (toGrothendieck C K) P ∧ IsSheaf (toGrothendieck C L) P

Tactic:
refine ⟨fun h ↦ ⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
    Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩, fun h ↦ ?_⟩

Result:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : IsSheaf (toGrothendieck C K) P ∧ IsSheaf (toGrothendieck C L) P
⊢ IsSheaf (toGrothendieck C (K ⊔ L)) P

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
⊢ IsSheaf (toGrothendieck C (K ⊔ L)) P

Tactic:
rw [isSheaf_coverage]

Result:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
⊢ ∀ {X : C}, ∀ R ∈ (K ⊔ L).covering X, IsSheafFor P R

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
⊢ ∀ {X : C}, ∀ R ∈ (K ⊔ L).covering X, IsSheafFor P R

Tactic:
intro X R hR

Result:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ (K ⊔ L).covering X
⊢ IsSheafFor P R

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ (K ⊔ L).covering X
⊢ IsSheafFor P R

Tactic:
rcases hR with hR | hR

Result:
case inl
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ K.covering X
⊢ IsSheafFor P R

case inr
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ L.covering X
⊢ IsSheafFor P R

Proof state:
case inl
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ K.covering X
⊢ IsSheafFor P R

Tactic:
exact h.1 R hR

Result:
no goals

Proof state:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : IsSheaf (toGrothendieck C K) P ∧ IsSheaf (toGrothendieck C L) P
⊢ IsSheaf (toGrothendieck C (K ⊔ L)) P

Tactic:
rw [isSheaf_coverage, isSheaf_coverage] at h

Result:
C : Type u_2
inst✝ : Category.{u_3, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.covering X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.covering X, IsSheafFor P R
⊢ IsSheaf (toGrothendieck C (K ⊔ L)) P