awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ Y) biprod.snd 0
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
have mpr : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (0 ≫ biprod.inr) 0
Tactic: rw [h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X Y : C
h : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ Y) biprod.snd 0
mpr : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (0 ≫ biprod.inr) 0
⊢ Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) (biprod.snd ≫ biprod.inr) 0
have mpr₁ : Eq.{v + 1} (α := biprod.{v, u} X Y ⟶ biprod.{v, u} X Y) 0 0
Tactic: rw [h, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
⊢ IsZero.{v, u} Y ∨ IsZero.{v, u} Z
have refine : ∀ (h : ¬IsZero.{v, u} Y), IsZero.{v, u} Z
Tactic: refine or_iff_not_imp_left.mpr fun h => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : ¬IsZero.{v, u} Y
⊢ IsZero.{v, u} Z
have h₁ : ¬Eq.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
Tactic: rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : ¬Eq.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
⊢ IsZero.{v, u} Z
have h₁ : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
Tactic: change biprod.inl ≠ 0 at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
⊢ IsZero.{v, u} Z
have this : Simple.{v, u} (biprod.{v, u} Y Z)
Tactic: have : Simple (Y ⊞ Z) := Simple.of_iso i.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : Ne.{v + 1} (α := Y ⟶ biprod.{v, u} Y Z) biprod.inl 0
this : Simple.{v, u} (biprod.{v, u} Y Z)
⊢ IsZero.{v, u} Z
have h₁ : IsIso.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
Tactic: rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y Z : C
i : X ≅ biprod.{v, u} Y Z
h : IsIso.{v, u} (C := C) (X := Y) (Y := biprod.{v, u} Y Z) biprod.inl
this : Simple.{v, u} (biprod.{v, u} Y Z)
⊢ IsZero.{v, u} Z
have rwa : ∀ (h : IsZero.{v, u} Z) (this : Simple.{v, u} (biprod.{v, u} Y Z)), IsZero.{v, u} Z
Tactic: rwa [Biprod.isIso_inl_iff_isZero] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : Simple.{v, u} X
a : Subobject.{v, u} X
⊢ a = ⊥ ∨ a = ⊤
have obtain : ∀ (Y : C) (i : Y ⟶ X) (w : Mono i), mk i = ⊥ ∨ mk i = ⊤
Tactic: obtain ⟨Y, i, _, rfl⟩ := Subobject.mk_surjective a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
⊢ mk i = ⊥ ∨ mk i = ⊤
have pos : ∀ (h : i = 0), mk i = ⊥ ∨ mk i = ⊤
Tactic: by_cases h : i = 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : Simple.{v, u} X
Y : C
i : Y ⟶ X
w : Mono i
pos : ∀ (h : i = 0), mk i = ⊥ ∨ mk i = ⊤
⊢ mk i = ⊥ ∨ mk i = ⊤
have neg : ∀ (h : ¬i = 0), mk i = ⊥ ∨ mk i = ⊤
Tactic: by_cases h : i = 0
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
⊢ Simple.{v, u} X
have mono_isIso_iff_nonzero : ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
have mono_isIso_iff_nonzero : IsIso f → f ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
mono_isIso_iff_nonzero : IsIso f → f ≠ 0
⊢ IsIso f ↔ f ≠ 0
have mono_isIso_iff_nonzero₁ : f ≠ 0 → IsIso f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : IsIso f
⊢ f ≠ 0
have i₁ : mk f = ⊤
Tactic: rw [Subobject.isIso_iff_mk_eq_top] at i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False
have w₁ : mk f = ⊥
Tactic: rw [← Subobject.mk_eq_bot_iff_zero] at w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
⊢ IsIso f
have mono_isIso_iff_nonzero : ∀ (h : mk f = ⊥), IsIso f
Tactic: rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
mono_isIso_iff_nonzero : ∀ (h : mk f = ⊥), IsIso f
⊢ IsIso f
have mono_isIso_iff_nonzero₁ : ∀ (h : mk f = ⊤), IsIso f
Tactic: rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Simple (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasZeroObject.{v, u} C
X : C
inst_3 : IsSimpleOrder (Subobject.{v, u} X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f
have h₁ : f = 0
Tactic: rw [Subobject.mk_eq_bot_iff_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
⊢ inv f = f⁻¹
have hom_inv_id : Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
⊢ Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)
have hom_inv_id : f⁻¹ * f = 𝟙 x
Tactic: rw [comp_as_mul, inv_mul_cancel, id_as_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
hom_inv_id : f⁻¹ * f = 𝟙 x
⊢ Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)
have hom_inv_id₁ : Eq.{u + 1} (α := x ⟶ x) 1 (𝟙 x)
Tactic: rw [comp_as_mul, inv_mul_cancel, id_as_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
G : Type u
inst : Group G
x y : SingleObj G
f : x ⟶ y
hom_inv_id : f⁻¹ * f = 𝟙 x
hom_inv_id₁ : Eq.{u + 1} (α := x ⟶ x) 1 (𝟙 x)
⊢ Eq.{u + 1} (α := x ⟶ x) (f ≫ f⁻¹) (𝟙 x)
have hom_inv_id₂ : Eq.{u + 1} (α := x ⟶ x) 1 1
Tactic: rw [comp_as_mul, inv_mul_cancel, id_as_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw₂ : f Z = f Z * (f Y)⁻¹ * f Y
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
rw₂ : f Z = f Z * (f Y)⁻¹ * f Y
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw₃ : f Z = f Z * ((f Y)⁻¹ * f Y)
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
rw₂ : f Z = f Z * (f Y)⁻¹ * f Y
rw₃ : f Z = f Z * ((f Y)⁻¹ * f Y)
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw₄ : f Z = f Z * 1
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M G : Type u
inst : Monoid M
inst_1 : Group G
N : Type v
inst_2 : Monoid N
C : Type v
inst_3 : Category.{w, v} C
f : C → G
X Y Z : C
f_1 : X ⟶ Y
g : Y ⟶ Z
rw : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * (f Y * (f X)⁻¹)
rw₁ : f Z * (f X)⁻¹ = f Z * (f Y)⁻¹ * f Y * (f X)⁻¹
rw₂ : f Z = f Z * (f Y)⁻¹ * f Y
rw₃ : f Z = f Z * ((f Y)⁻¹ * f Y)
rw₄ : f Z = f Z * 1
⊢ f Z * (f X)⁻¹ = CategoryStruct.comp (Y := ()) (f Y * (f X)⁻¹) (f Z * (f Y)⁻¹)
have rw₅ : f Z = f Z
Tactic: rw [SingleObj.comp_as_mul, ← mul_assoc, mul_left_inj, mul_assoc, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ 𝟭 (SingleObj M) = e.toMonoidHom.toFunctor ⋙ e.symm.toMonoidHom.toFunctor
have rw : MonoidHom.toFunctor (MonoidHom.id M) = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
Tactic: rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ MonoidHom.toFunctor (MonoidHom.id M) = (e.symm.toMonoidHom.comp e.toMonoidHom).toFunctor
have e_f : MonoidHom.id M = e.symm.toMonoidHom.comp e.toMonoidHom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ e.symm.toMonoidHom.toFunctor ⋙ e.toMonoidHom.toFunctor = 𝟭 (SingleObj N)
have rw : (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = MonoidHom.toFunctor (MonoidHom.id N)
Tactic: rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
-- Lean 4 proof step from Mathlib.CategoryTheory.SingleObj (goal)
Goal:
M : Type u
N : Type v
inst : Monoid M
inst_1 : Monoid N
e : M ≃* N
⊢ (e.toMonoidHom.comp e.symm.toMonoidHom).toFunctor = MonoidHom.toFunctor (MonoidHom.id N)
have e_f : e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id N
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf.{v₁, v_1, u₁, u_1} J E
⊢ Eq (α :=
    (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X).obj (P := Presheaf.IsSheaf J) ⟶
      ((composeAndSheafify J G ⋙ sheafCompose J F).obj X).obj (P := Presheaf.IsSheaf J))
    (InducedCategory.Hom.hom (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
have change : Eq (α :=
  obj (sheafToPresheaf J E) (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X) ⟶
    obj (sheafToPresheaf J E) ((composeAndSheafify J G ⋙ sheafCompose J F).obj X))
  (map (sheafToPresheaf J E) (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
  (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
    whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
Tactic: change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
inst_3 : HasWeakSheafify.{v₁, v₂, u₁, u₂} J D
inst_4 : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf.{v₁, v_1, u₁, u_1} J E
⊢ Eq (α :=
    obj (sheafToPresheaf J E) (obj (𝟭 (Sheaf.{v₁, v_1, u₁, u_1} J E)) X) ⟶
      obj (sheafToPresheaf J E) ((composeAndSheafify J G ⋙ sheafCompose J F).obj X))
    (map (sheafToPresheaf J E) (NatTrans.app (Adjunction.unit (adjunction J adj)) X))
    (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
      whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
have simp : Eq (α :=
  obj (sheafToPresheaf J E) X ⟶
    obj (sheafToPresheaf J E) ((sheafCompose J F).obj (obj (presheafToSheaf J D) (obj (sheafToPresheaf J E) X ⋙ G))))
  (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (obj (sheafToPresheaf J E) X) ≫
    whiskerRight (toSheafify J (obj (sheafToPresheaf J E) X ⋙ G)) F)
  (NatTrans.app (Adjunction.unit (Adjunction.whiskerRight Cᵒᵖ adj)) (X.obj (P := Presheaf.IsSheaf J)) ≫
    whiskerRight (toSheafify J (X.obj (P := Presheaf.IsSheaf J) ⋙ G)) F)
Tactic: simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
    Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app,
    sheafificationAdjunction_unit_app, whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app,
    Functor.comp_map, Functor.map_id, whiskerRight_id', Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
⊢ MorphismProperty.inverseImage J.W (obj (whiskeringRight Cᵒᵖ E D) G) f
have this : F.IsRightAdjoint
Tactic: have := adj.isRightAdjoint
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
⊢ Function.Bijective (β := P ⋙ G ⟶ R) fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g
have rw : Function.Bijective (α := Q ⋙ G ⟶ R) (β := P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R)
  (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
    (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
      (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
    fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
Tactic: rw [← ((adj.whiskerRight Cᵒᵖ).homEquiv P R).comp_bijective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
⊢ Function.Bijective (α := Q ⋙ G ⟶ R) (β := P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R)
    (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
      (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
      fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
have h : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R) →
  (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F) →
    Eq (α := (Q ⋙ G ⟶ R) → (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R))
      (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
        (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
        fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
      (⇑((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
            (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) sorry)) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
Tactic: convert!
      (((adj.whiskerRight Cᵒᵖ).homEquiv Q R).trans
          (hf.homEquiv (R ⋙ F) ((sheafCompose J F).obj ⟨R, hR⟩).property)).bijective
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
⊢ Eq (α := (Q ⋙ G ⟶ R) → (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R))
    (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
      (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
        (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
      fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g)
    (⇑((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
          (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯)) :
      (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
have h : ∀ (g : Q ⋙ G ⟶ R) (X : Cᵒᵖ),
  Eq.{v_1 + 1} (α := P.obj X ⟶ (obj (obj (whiskeringRight Cᵒᵖ D E) F) R).obj X)
    (NatTrans.app
      (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
        (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
        (fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g) g)
      X)
    (NatTrans.app
      (((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
            (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) sorry) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
        g)
      X)
Tactic: ext g X
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Adjunction (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : GrothendieckTopology.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v₂, v_1, u₂, u_1} D E
G : Functor.{v_1, v₂, u_1, u₂} E D
adj : G ⊣ F
P Q : Functor.{v₁, v_1, u₁, u_1} Cᵒᵖ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Functor.{v₁, v₂, u₁, u₂} Cᵒᵖ D
hR : Presheaf.IsSheaf J R
e_1 : (Q ⋙ G ⟶ R) = (obj (obj (whiskeringRight Cᵒᵖ E D) G) Q ⟶ R)
e_2 : (P ⟶ obj (obj (whiskeringRight Cᵒᵖ D E) F) R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α := P.obj X ⟶ (obj (obj (whiskeringRight Cᵒᵖ D E) F) R).obj X)
    (NatTrans.app
      (Function.comp (β := obj (obj (whiskeringRight Cᵒᵖ E D) G) P ⟶ R)
        (⇑(Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj P ⟶ R) → P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R)
        (fun (g : Q ⋙ G ⟶ R) ↦ whiskerRight f G ≫ g) g)
      X)
    (NatTrans.app
      (((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R).trans
            (ObjectProperty.isLocal.homEquiv (P := Presheaf.IsSheaf J) hf (R ⋙ F) ⋯) :
          (a : ((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R) → P ⟶ R ⋙ F)
        g)
      X)
have h : Eq (α := P.obj X ⟶ F.obj (R.obj X))
  (NatTrans.app
      ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) P R : (a : P ⋙ G ⟶ R) → P ⟶ R ⋙ F) (whiskerRight f G ≫ g))
      X :
    P.obj X ⟶ (R ⋙ F).obj X)
  (f.app X ≫
    NatTrans.app ((Adjunction.homEquiv (Adjunction.whiskerRight Cᵒᵖ adj) Q R : (a : Q ⋙ G ⟶ R) → Q ⟶ R ⋙ F) g) X)
Tactic: dsimp