-- Mathlib/CategoryTheory/Sites/LocallyBijective.lean
/-- A morphism of sheaves of types is locally bijective iff it is an isomorphism.
(This is generalized below as `isLocallyBijective_iff_isIso`.) -/
private lemma isLocallyBijective_iff_isIso' :
    IsLocallyInjective f ∧ IsLocallySurjective f ↔ IsIso f

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
intro

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
a✝ : IsIso f
⊢ IsLocallyInjective f ∧ IsLocallySurjective f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
⊢ t.Compatible

Tactic:
intro Y₁ Y₂ W g₁ g₂ f₁ f₂ hf₁ hf₂ w

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.val s).arrows f₁
hf₂ : (Presheaf.imageSieve f.val s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.val.map g₁.op (t f₁ hf₁) = F.val.map g₂.op (t f₂ hf₂)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective (f.val.app X)
⊢ IsIso f

Tactic:
rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
this : ∀ (X : Cᵒᵖ), Function.Surjective (f.val.app X)
⊢ ∀ (X : Cᵒᵖ), IsIso (((sheafToPresheaf J (Type w)).map f).app X)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective f ∧ IsLocallySurjective f ↔ IsIso f

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective f ∧ IsLocallySurjective f → IsIso f

case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso f → IsLocallyInjective f ∧ IsLocallySurjective f

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsLocallyInjective f ∧ IsLocallySurjective f → IsIso f

Tactic:
rintro ⟨h₁, _⟩

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : IsLocallyInjective f
right✝ : IsLocallySurjective f
⊢ IsIso f

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
a✝ : IsIso f
⊢ IsLocallyInjective f ∧ IsLocallySurjective f

Tactic:
constructor <;> infer_instance

Result:
no goals

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
ht : t.Compatible
⊢ ∃ a, f.val.app X a = s

Tactic:
refine ⟨H.amalgamate t ht, ?_⟩

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
ht : t.Compatible
⊢ f.val.app X (H.amalgamate t ht) = s

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
ht : t.Compatible
⊢ f.val.app X (H.amalgamate t ht) = s

Tactic:
apply (Presieve.isSeparated_of_isSheaf _ _
  ((isSheaf_iff_isSheaf_of_type J G.val).1 G.cond) _
  (Presheaf.imageSieve_mem J f.val s)).ext

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
ht : t.Compatible
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ Opposite.unop X⦄,
    (Presheaf.imageSieve f.val s).arrows f_1 → G.val.map f_1.op (f.val.app X (H.amalgamate t ht)) = G.val.map f_1.op s

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
⊢ ∃ a, f.val.app X a = s

Tactic:
have ht : t.Compatible := by
  intro Y₁ Y₂ W g₁ g₂ f₁ f₂ hf₁ hf₂ w
  apply h₁
  have eq₁ := FunctorToTypes.naturality _ _ f.val g₁.op (t f₁ hf₁)
  have eq₂ := FunctorToTypes.naturality _ _ f.val g₂.op (t f₂ hf₂)
  have eq₃ := congr_arg (G.val.map g₁.op) (Presheaf.app_localPreimage f.val s _ hf₁)
  have eq₄ := congr_arg (G.val.map g₂.op) (Presheaf.app_localPreimage f.val s _ hf₂)
  refine eq₁.trans (eq₃.trans (Eq.trans ?_ (eq₄.symm.trans eq₂.symm)))
  erw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
  simp only [← op_comp, w]

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.val.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.val.obj X
H : Presieve.IsSheafFor F.val (Presheaf.imageSieve f.val s).arrows
t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg
ht : t.Compatible
⊢ ∃ a, f.val.app X a = s