-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
theorem compatiblePreservingOfDownwardsClosed (F : C ⥤ D) [F.Full] [F.Faithful]
    (hF : ∀ {c : C} {d : D} (_ : d ⟶ F.obj c), Σc', F.obj c' ≅ d) : CompatiblePreserving K F

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ CompatiblePreserving K F

Tactic:
constructor

Result:
case compatible
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (F.op ⋙ ℱ.val) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂), f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ F.map (F.preimage (e.hom ≫ f₁) ≫ g₁) = F.map (F.preimage (e.hom ≫ f₂) ≫ g₂)

Tactic:
simpa using he

Result:
no goals

Proof state:
case compatible.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
apply (ℱ.1.mapIso e.op).toEquiv.injective

Result:
case compatible.mk.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ (ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₁.op (x g₁ hg₁)) = (ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₂.op (x g₂ hg₂))

Proof state:
case compatible
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
⊢ ∀ (ℱ : Sheaf K (Type u_1)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (F.op ⋙ ℱ.val) T},
    x.Compatible →
      ∀ {Y₁ Y₂ : C} {X : D} (f₁ : X ⟶ F.obj Y₁) (f₂ : X ⟶ F.obj Y₂) {g₁ : Y₁ ⟶ Z} {g₂ : Y₂ ⟶ Z} (hg₁ : T g₁)
        (hg₂ : T g₂), f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂ → ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
introv hx he

Result:
case compatible
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Proof state:
case compatible.mk.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ (ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₁.op (x g₁ hg₁)) = (ℱ.val.mapIso e.op).toEquiv (ℱ.val.map f₂.op (x g₂ hg₂))

Tactic:
simp only [Iso.op_hom, Iso.toEquiv_fun, ℱ.1.mapIso_hom, ← FunctorToTypes.map_comp_apply]

Result:
case compatible.mk.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map (f₁.op ≫ e.hom.op) (x g₁ hg₁) = ℱ.val.map (f₂.op ≫ e.hom.op) (x g₂ hg₂)

Proof state:
case compatible.mk.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map (f₁.op ≫ e.hom.op) (x g₁ hg₁) = ℱ.val.map (f₂.op ≫ e.hom.op) (x g₂ hg₂)

Tactic:
simpa using
  hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂
    (F.map_injective <| by simpa using he)

Result:
no goals

Proof state:
case compatible
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
obtain ⟨X', e⟩ := hF f₁

Result:
case compatible.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)