awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
mp : IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f → IsIso f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f ↔ IsIso f
have mpr : IsIso f → IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsIso f
have mp : IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f) ∧
  IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
Tactic: rw [← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)),
      ← isLocallyBijective_iff_isIso']
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
⊢ IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f) ∧
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
have mp : IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
  (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
left : IsLocallyInjective (FD := FA) (CD := CA) f
right : IsLocallySurjective (FA := FA) (CA := CA) f
mp :
  IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
    (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
⊢ IsLocallyInjective (FD := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f) ∧
    IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
      (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
have mp₁ : IsLocallySurjective (FA := TypeCat.Fun) (F₁ := Functor.obj (sheafCompose J (forget A (FC := FA) (CC := CA))) F)
  (Functor.map (sheafCompose J (forget A (FC := FA) (CC := CA))) f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
h : IsIso f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f
have mpr : IsLocallyInjective (FD := FA) (CD := CA) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
F G : Sheaf.{v, v', u, u'} J A
f : F ⟶ G
inst_4 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_5 : GrothendieckTopology.HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
h : IsIso f
mpr : IsLocallyInjective (FD := FA) (CD := CA) f
⊢ IsLocallyInjective (FD := FA) (CD := CA) f ∧ IsLocallySurjective (FA := FA) (CA := CA) f
have mpr₁ : IsLocallySurjective (FA := FA) (CA := CA) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
X Y : Functor.{v, v', u, u'} Cᵒᵖ A
f : X ⟶ Y
inst_5 : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f
inst_6 : Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f
have rw : Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [W_iff_isLocallyBijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_6 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_7 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
inst_8 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw : IsIso (X := Functor.obj (presheafToSheaf J A) P) (Functor.map (presheafToSheaf J A) f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
      ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
      Presheaf.comp_isLocallySurjective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_6 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_7 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
inst_8 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
rw :
  IsIso (X := Functor.obj (presheafToSheaf J A) P) (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₁ : Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ∧
    Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
      ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
      Presheaf.comp_isLocallySurjective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_6 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_7 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
inst_8 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
rw :
  IsIso (X := Functor.obj (presheafToSheaf J A) P) (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₂ : Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ∧
    Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
      (f ≫ CategoryTheory.toSheafify J Q) ∧
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
Tactic: rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
      ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
      Presheaf.comp_isLocallySurjective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : Functor.ReflectsIsomorphisms.{v', u', w', w' + 1} (forget A (FC := FA) (CC := CA))
inst_6 : HasSheafCompose.{v, v', w', u, u', w' + 1} J (forget A (FC := FA) (CC := CA))
inst_7 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
inst_8 :
  ∀ (P : Functor.{v, v', u, u'} Cᵒᵖ A),
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J P)
      (CategoryTheory.toSheafify J P)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
f : P ⟶ Q
rw :
  IsIso (X := Functor.obj (presheafToSheaf J A) P) (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₁ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
rw₂ :
  Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ∧
      Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
        (Functor.map (presheafToSheaf J A) f) ↔
    Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
        (f ≫ CategoryTheory.toSheafify J Q) ∧
      Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
⊢ J.W f ↔ Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J f ∧ Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) f
have rw₃ : Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ∧
    Sheaf.IsLocallySurjective (FA := FA) (CA := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) f) ↔
  Presheaf.IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := CategoryTheory.sheafify J Q)
      (f ≫ CategoryTheory.toSheafify J Q) ∧
    Presheaf.IsLocallySurjective J (FA := FA) (CA := CA) (G := CategoryTheory.sheafify J Q)
      (f ≫ CategoryTheory.toSheafify J Q)
Tactic: rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A),
      ← Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      ← Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q),
      CategoryTheory.toSheafify_naturality, Presheaf.comp_isLocallyInjective_iff,
      Presheaf.comp_isLocallySurjective_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
have rw : IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
    (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallyInjective (FD := FA) (CD := CA) J φ
Tactic: rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
have rw₁ : IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
    (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
Tactic: rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
rw₁ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
have rw₂ : IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
Tactic: rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallyBijective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst_2 : (X Y : A) → FunLike.{u_1 + 1, w' + 1, w' + 1} (FA X Y) (CA X) (CA Y)
inst_3 : ConcreteCategory.{w', v', u', u_1} A FA (CC := CA)
inst_4 : HasWeakSheafify.{v, v', u, u'} J A
inst_5 : GrothendieckTopology.WEqualsLocallyBijective.{w', v', v, u', u, u_1} J A (FA := FA) (CA := CA)
P Q : Functor.{v, v', u, u'} Cᵒᵖ A
φ : P ⟶ Q
rw :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
rw₁ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₁ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) P))
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ)) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
rw₂ :
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
      Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
      (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
        (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (φ ≫ toSheafify J Q)
⊢ Sheaf.IsLocallyInjective (FD := FA) (CD := CA) (F₁ := Functor.obj (presheafToSheaf J A) P)
      (Functor.map (presheafToSheaf J A) φ) ↔
    IsLocallyInjective (FD := FA) (CD := CA) J φ
have rw₃ : IsLocallyInjective (FD := FA) (CD := CA) J (F₂ :=
    Functor.obj (sheafToPresheaf J A) (Functor.obj (presheafToSheaf J A) Q))
    (CategoryStruct.comp (Y := sheafify J P) (toSheafify J P)
      (Functor.map (sheafToPresheaf J A) (Functor.map (presheafToSheaf J A) φ))) ↔
  IsLocallyInjective (FD := FA) (CD := CA) J (F₂ := sheafify J Q) (toSheafify J P ≫ sheafifyMap J φ)
Tactic: rw [← Sheaf.isLocallyInjective_sheafToPresheaf_map_iff,
    ← isLocallyInjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallyInjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]