-- 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 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
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.val s).arrows g
⊢ G.val.map g.op (f.val.app X (H.amalgamate t ht)) = G.val.map g.op s

Tactic:
rw [← FunctorToTypes.naturality, H.valid_glue 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
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.val s).arrows g
⊢ f.val.app (Opposite.op Y) (t g ?mp.intro.Hf) = G.val.map g.op s

case mp.intro.Hf
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
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.val s).arrows g
⊢ (Presheaf.imageSieve f.val s).arrows g

Proof state:
case a
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₂
eq₁ : f.val.app (Opposite.op W) (F.val.map g₁.op (t f₁ hf₁)) = G.val.map g₁.op (f.val.app (Opposite.op Y₁) (t f₁ hf₁))
eq₂ : f.val.app (Opposite.op W) (F.val.map g₂.op (t f₂ hf₂)) = G.val.map g₂.op (f.val.app (Opposite.op Y₂) (t f₂ hf₂))
⊢ (ConcreteCategory.hom (f.val.app (Opposite.op W))) (F.val.map g₁.op (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.val.app (Opposite.op W))) (F.val.map g₂.op (t f₂ hf₂))

Tactic:
have eq₃ := congr_arg (G.val.map g₁.op) (Presheaf.app_localPreimage f.val s _ hf₁)

Result:
case a
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₂
eq₁ : f.val.app (Opposite.op W) (F.val.map g₁.op (t f₁ hf₁)) = G.val.map g₁.op (f.val.app (Opposite.op Y₁) (t f₁ hf₁))
eq₂ : f.val.app (Opposite.op W) (F.val.map g₂.op (t f₂ hf₂)) = G.val.map g₂.op (f.val.app (Opposite.op Y₂) (t f₂ hf₂))
eq₃ :
  G.val.map g₁.op ((ConcreteCategory.hom (f.val.app (Opposite.op Y₁))) (Presheaf.localPreimage f.val s f₁ hf₁)) =
    G.val.map g₁.op ((ConcreteCategory.hom (G.val.map f₁.op)) s)
⊢ (ConcreteCategory.hom (f.val.app (Opposite.op W))) (F.val.map g₁.op (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.val.app (Opposite.op W))) (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)
X : Cᵒᵖ
⊢ IsIso (((sheafToPresheaf J (Type w)).map f).app X)

Tactic:
rw [isIso_iff_bijective]

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ᵒᵖ
⊢ Function.Bijective (((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
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)

Tactic:
intro X

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:
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
⊢ ∃ a, f.val.app X a = s

Tactic:
let t : Presieve.FamilyOfElements F.val (Presheaf.imageSieve f.val s).arrows :=
  fun Y g hg => Presheaf.localPreimage f.val s g hg

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
⊢ ∃ a, f.val.app X a = s

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)
X : Cᵒᵖ
⊢ Function.Bijective (((sheafToPresheaf J (Type w)).map f).app X)

Tactic:
exact ⟨h₁ X, this X⟩

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
⊢ IsIso f

Tactic:
suffices ∀ (X : Cᵒᵖ), Function.Surjective (f.val.app X) by
  rw [← isIso_iff_of_reflects_iso _ (sheafToPresheaf _ _), NatTrans.isIso_iff_isIso_app]
  intro X
  rw [isIso_iff_bijective]
  exact ⟨h₁ X, this X⟩

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ᵒᵖ), Function.Surjective (f.val.app X)