awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
M : A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
X Y : C
f : X ⟶ Y
inst_4 : HasFunctorEnrichedHom A F G
y : (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M)).obj (op Y)
j : Over.{v₁, u₁} X
⊢ Eq.{v₃ + 1} (α :=
    (Functor.op (Over.forget X) ⋙ tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)).obj (op j) ⟶
      (Functor.op (Over.forget X) ⋙ G).obj (op j))
    (NatTrans.app
      ((functorEnrichedHomCoyonedaObjEquiv M F G X :
          (a : M ⟶ enrichedHom A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        (y ≫
          precompEnrichedHom' A (Under.map f.op) (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ F))
            (Iso.refl (Under.map f.op ⋙ Under.forget (op Y) ⋙ G))))
      (op j))
    (NatTrans.app
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G).map f.op) :
          (a : (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G) →
            (Over.forget X).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget X).op ⋙ G)
        ((functorEnrichedHomCoyonedaObjEquiv M F G Y :
            (a : M ⟶ enrichedHom A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)) →
              (Over.forget Y).op ⋙ (F ⊗ (Functor.const Cᵒᵖ).obj M) ⟶ (Over.forget Y).op ⋙ G)
          y))
      (op j))
have w : Eq (α := tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
  (uncurry
      (y ≫
        enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
          (Functor.obj (C := Under.{v₁, u₁} (op X)) (Under.map f.op) (Under.mk j.hom.op))) :
    tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
  (uncurry
      (y ≫
        enrichedHomπ A (Under.forget (op Y) ⋙ F) (Under.forget (op Y) ⋙ G)
          (Under.mk (Y := op j.left) (f.op ≫ j.hom.op))) :
    tensorObj.{v₃, u₃} (𝒞 := inst_1) (F.obj (op j.left)) M ⟶ G.obj (op j.left))
Tactic: simp [functorEnrichedHomCoyonedaObjEquiv, presheafHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf.{v₃, v₁, u₁} J (functorEnrichedHom A F G ⋙ Functor.obj coyoneda (op M))
have rw : Presieve.IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)
Tactic: rw [Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
F G : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
hG : IsSheaf J G
inst_4 : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)
have rw : IsSheaf J (presheafHom (tensorObj (𝒞 := Functor.category) F (Functor.obj (Functor.const Cᵒᵖ) M)) G)
Tactic: rw [← isSheaf_iff_isSheaf_of_type]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
K : GrothendieckTopology.{v₂, u₂} D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.IsCoverDense J
inst_5 : G.Full
inst_6 : G.IsContinuous K J
inst_7 : Functor.EssSurj (C := Sheaf.{v₁, v₃, u₁, u₃} J A) (G.sheafPushforwardContinuous A K J)
inst_8 : MorphismProperty.IsMonoidal (C := Functor.{v₂, v₃, u₂, u₃} Dᵒᵖ A) K.W
⊢ MorphismProperty.IsMonoidal (C := Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A) J.W
have rw : MorphismProperty.IsMonoidal (C := Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A)
  (MorphismProperty.inverseImage K.W (Functor.obj (Functor.whiskeringLeft Dᵒᵖ Cᵒᵖ A) G.op))
Tactic: rw [← J.W_inverseImage_whiskeringLeft K G]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
⊢ Function.Bijective (β := tensorObj (𝒞 := Functor.category) F G₁ ⟶ H)
    fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1
have this : Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1
Tactic: have := hg _ (Presheaf.isSheaf_functorEnrichedHom F H h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this : Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1
⊢ Function.Bijective (β := tensorObj (𝒞 := Functor.category) F G₁ ⟶ H)
    fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1
have rw : Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ F ⟹ H)
  (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1)
Tactic: rw [← Function.Bijective.of_comp_iff' (f := MonoidalClosed.curry)
    ((ihom.adjunction _).homEquiv _ _).bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this : Function.Bijective (β := G₁ ⟶ functorEnrichedHom A F H) fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1
⊢ Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ F ⟹ H)
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1)
have this₁ : Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
  ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
Tactic: rw [← Function.Bijective.of_comp_iff (g := MonoidalClosed.curry) _
    ((ihom.adjunction _).homEquiv _ _).bijective] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
⊢ Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ F ⟹ H)
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1)
have h₁ : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H) →
  Eq (α := (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1 :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ functorEnrichedHom A F H))
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
e_2 : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
⊢ Eq (α := (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    (curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1 :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ F ⟹ H))
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry :
      (tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) → (G₁ ⟶ functorEnrichedHom A F H))
have h₁ : ∀ (α : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H),
  Eq (α := G₁ ⟶ F ⟹ H) ((curry ∘ fun (g_1 : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) ↦ F ◁ g ≫ g_1) α)
    (((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry) α)
Tactic: ext α : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Monoidal (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
A : Type u₃
inst_1 : Category.{v₃, u₃} A
inst_2 : MonoidalCategory.{v₃, u₃} A
inst_3 : MonoidalClosed.{v₃, u₃} A
inst_4 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasFunctorEnrichedHom A F₁ F₂
inst_5 : ∀ (F₁ F₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Functor.{v₁, v₃, u₁, u₃} Cᵒᵖ A
h : Presheaf.IsSheaf J H
this :
  Function.Bijective (α := tensorObj (𝒞 := Functor.category) F G₂ ⟶ H) (β := G₁ ⟶ functorEnrichedHom A F H)
    ((fun (g_1 : G₂ ⟶ functorEnrichedHom A F H) ↦ g ≫ g_1) ∘ curry)
e_2 : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : tensorObj (𝒞 := Functor.category) F G₂ ⟶ H
⊢ Eq (α := G₁ ⟶ F ⟹ H) (curry (F ◁ g ≫ α)) (g ≫ curry α)
have h₁ : Eq (α := G₁ ⟶ F ⟹ H) (g ≫ curry α) (g ≫ curry α)
Tactic: rw [curry_natural_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
ι : Type (max u_1 v_1)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ P.precoverage.coverings S
T : C
g_1 : T ⟶ S
W : ι → C
p₁ : (i : ι) → W i ⟶ T
p₂ : (i : ι) → W i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g_1 (f i)
Z : C
g : Z ⟶ T
hg : Presieve.ofArrows W p₁ g
⊢ P g
have obtain : ∀ ⦃Y : C⦄ (i : ι), P (p₁ i)
Tactic: obtain ⟨i⟩ := hg
Cleared hypotheses: Z, g, hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
S : C
E : P.precoverage.ZeroHypercover S
⊢ E.Small
have exists_restrictIndex_mem : ∃ (ι : Type w) (f : ι → E.I₀), PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex f) ∈ P.precoverage.coverings S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
S : C
E : P.precoverage.ZeroHypercover S
⊢ ∃ (ι : Type w) (f : ι → E.I₀),
    PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex f) ∈ P.precoverage.coverings S
have h : PreZeroHypercover.presieve₀.{w, v_1, u_1} (E.restrictIndex PEmpty.elim) ∈ P.precoverage.coverings S
Tactic: use PEmpty, PEmpty.elim
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
⊢ (P ⊓ Q).precoverage = P.precoverage ⊓ Q.precoverage
have coverings : ∀ (X : C) (R : Presieve.{v_1, u_1} X),
  R ∈ (P ⊓ Q).precoverage.coverings X ↔ R ∈ (P.precoverage ⊓ Q.precoverage).coverings X
Tactic: ext X R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
P : MorphismProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
⊢ Precoverage.comap F P.precoverage = (P.inverseImage F).precoverage
have coverings : ∀ (X : C) (R : Presieve.{v_1, u_1} X),
  R ∈ (Precoverage.comap F P.precoverage).coverings X ↔ R ∈ (P.inverseImage F).precoverage.coverings X
Tactic: ext X R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
P : MorphismProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X : C
R : Presieve.{v_1, u_1} X
⊢ R ∈ (Precoverage.comap F P.precoverage).coverings X ↔ R ∈ (P.inverseImage F).precoverage.coverings X
have coverings : ∀ (ι : Type (max u_1 v_1)) (Y : ι → C) (f : (i : ι) → Y i ⟶ X),
  Presieve.ofArrows Y f ∈ (Precoverage.comap F P.precoverage).coverings X ↔
    Presieve.ofArrows Y f ∈ (P.inverseImage F).precoverage.coverings X
Tactic: obtain ⟨ι, Y, f, rfl⟩ := R.exists_eq_ofArrows
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f
have this : S.HasPullbacks f
Tactic: have : S.HasPullbacks f := ⟨fun {W} h hh ↦ P.hasPullback _ (hS hh)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ P.precoverage.coverings Y, T.FactorsThruAlong S f
have refine : Presieve.pullbackArrows f S ∈ P.precoverage.coverings Y
Tactic: refine ⟨S.pullbackArrows f, ?_, .pullbackArrows f S⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
⊢ Presieve.pullbackArrows f S g → P g
have this₁ : ∀ (W : C) (a : W ⟶ X) (h : S a), P (X := pullback a f) (pullback.snd a f)
Tactic: ⟨W, a, h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P_1 Q P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : P.HasPullbacks
X Y : C
f : Y ⟶ X
S : Presieve.{v_1, u_1} X
hS : S ∈ P.precoverage.coverings X
this : S.HasPullbacks f
Z : C
g : Z ⟶ Y
W : C
a : W ⟶ X
h : S a
⊢ P (X := pullback a f) (pullback.snd a f)
have this₁ : HasPullback a f
Tactic: have := S.hasPullback f h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : P.IsMultiplicative
⊢ P.grothendieckTopology = Pretopology.toGrothendieck P.pretopology
have rw : P.coverage.toGrothendieck = Pretopology.toGrothendieck P.pretopology
Tactic: rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
    Pretopology.toGrothendieck_toCoverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : P.IsMultiplicative
rw : P.coverage.toGrothendieck = Pretopology.toGrothendieck P.pretopology
⊢ P.grothendieckTopology = Pretopology.toGrothendieck P.pretopology
have rw₁ : (Pretopology.toCoverage P.pretopology).toGrothendieck = Pretopology.toGrothendieck P.pretopology
Tactic: rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
    Pretopology.toGrothendieck_toCoverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : P.IsMultiplicative
rw : P.coverage.toGrothendieck = Pretopology.toGrothendieck P.pretopology
rw₁ : (Pretopology.toCoverage P.pretopology).toGrothendieck = Pretopology.toGrothendieck P.pretopology
⊢ P.grothendieckTopology = Pretopology.toGrothendieck P.pretopology
have rw₂ : Pretopology.toGrothendieck P.pretopology = Pretopology.toGrothendieck P.pretopology
Tactic: rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
    Pretopology.toGrothendieck_toCoverage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
⊢ Eq (α := Pretopology.{v_1, u_1} C) (P ⊓ Q).pretopology (P.pretopology ⊓ Q.pretopology)
have coverings : (Pretopology.toPrecoverage (P ⊓ Q).pretopology).coverings =
  (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.MorphismProperty (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
⊢ (Pretopology.toPrecoverage (P ⊓ Q).pretopology).coverings =
    (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings
have coverings : (P.precoverage ⊓ Q.precoverage).coverings = (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings
Tactic: simp only [pretopology_toPrecoverage, precoverage_inf]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x x_1 x_2 : OneCochain G U
⊢ x * x_1 * x_2 = x * (x_1 * x_2)
have ev : ∀ (x_3 x_4 : I) (x_5 : C) (x_6 : x_5 ⟶ U x_3) (x_7 : x_5 ⟶ U x_4),
  (x * x_1 * x_2).ev x_3 x_4 x_6 x_7 = (x * (x_1 * x_2)).ev x_3 x_4 x_6 x_7
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
⊢ 1 * x = x
have ev : ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2), (1 * x).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
⊢ x * 1 = x
have ev : ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2), (x * 1).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
⊢ x⁻¹ * x = 1
have ev : ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2), (x⁻¹ * x).ev x_1 x_2 x_4 x_5 = ev 1 x_1 x_2 x_4 x_5
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹
have rw : γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
Tactic: rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
    ev_refl, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
rw : γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹
have rw₁ : γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
Tactic: rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
    ev_refl, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
rw : γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₁ : γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹
have rw₂ : 1 = (γ.ev j i b a)⁻¹ * γ.ev j i b a
Tactic: rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
    ev_refl, inv_mul_cancel]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
rw : γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₁ : γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₂ : 1 = (γ.ev j i b a)⁻¹ * γ.ev j i b a
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹
have rw₃ : Eq.{w + 1} (α := (↑(G.obj (Opposite.op T)) : Type w)) 1 1
Tactic: rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
    ev_refl, inv_mul_cancel]