awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
h : IsLocallySurjective J (FA := FA) (CA := CA) f₂
⊢ IsLocallySurjective J (FA := FA) (CA := CA) f₃
have mpr : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
Tactic: rw [← fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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)
K : GrothendieckTopology.{v, u} C
hJK : J ≤ K
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f : F ⟶ G
h : IsLocallySurjective J (FA := FA) (CA := CA) f
U : C
s : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (G.obj (op U))
⊢ imageSieve (FA := FA) (CA := CA) f s ∈ (K : (a : C) → Set (Sieve a)) U
have a : imageSieve (FA := FA) (CA := CA) f s ∈ (J : (a : C) → Set (Sieve a)) U
Tactic: apply hJK
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
have rj : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
  (imageSieve (FA := FA) (CA := CA) f₁ x₁)
Tactic: apply J.intersection_covering
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
rj :
  Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (imageSieve (FA := FA) (CA := CA) f₁ x₁)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
have sj : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
  (imageSieve (FA := FA) (CA := CA) f₁ x₂)
Tactic: apply J.intersection_covering
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FA) (CD := CA) x₁ x₂)
have hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
Tactic: have hS : S ∈ J X.unop := by
      apply J.intersection_covering
      all_goals apply imageSieve_mem
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FA) (CD := CA) x₁ x₂)
have refine_1 : Sieve.bind S.arrows T ≤ equalizerSieve (FD := FA) (CD := CA) x₁ x₂
Tactic: refine J.superset_covering ?_ (J.transitive hS (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
refine_1 : Sieve.bind S.arrows T ≤ equalizerSieve (FD := FA) (CD := CA) x₁ x₂
⊢ Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X))
    (equalizerSieve (FD := FA) (CD := CA) x₁ x₂)
have refine_2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄, S.arrows f → Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: refine J.superset_covering ?_ (J.transitive hS (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
have refine_2 : T f hf ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ T f hf ∈ (J : (a : C) → Set (Sieve a)) Y
have refine_2 : Eq (α := CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
      (localPreimage (FA := FA) (CA := CA) f₁ x₁ f sorry) :
    CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f sorry) :
    CA (F₃.obj (op Y)))
Tactic: apply equalizerSieve_mem J (f₁ ≫ f₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) ((f₁ ≫ f₂).app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
      CA (F₃.obj (op Y)))
have refine_2 : Eq (α := CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
        (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
      (localPreimage (FA := FA) (CA := CA) f₁ x₁ f sorry) :
    CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
        (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f sorry) :
    CA (F₃.obj (op Y)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
X : Cᵒᵖ
x₁ x₂ : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj X)
h :
  Eq (α := CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₁ : CA (F₃.obj X))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app X) : (a : CA (F₂.obj X)) → CA (F₃.obj X)) x₂ : CA (F₃.obj X))
S : Sieve.{v, u} (unop X) := imageSieve (FA := FA) (CA := CA) f₁ x₁ ⊓ imageSieve (FA := FA) (CA := CA) f₁ x₂
hS : Membership.mem (γ := Set (Sieve.{v, u} (unop X))) ((J : (a : C) → Set (Sieve a)) (unop X)) S
T : ⦃Y : C⦄ → (f : Y ⟶ unop X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ unop X) (hf : S.arrows f) ↦
    equalizerSieve (FD := FA) (CD := CA) (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯)
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯)
Y : C
f : Y ⟶ unop X
hf : S.arrows f
⊢ Eq (α := CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
          (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₁ f ⋯) :
      CA (F₃.obj (op Y)))
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
          (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) f₁ x₂ f ⋯) :
      CA (F₃.obj (op Y)))
have refine_2 : Eq (α := CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op Y)) : (a : CA (F₂.obj (op Y))) → CA (F₃.obj (op Y)))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
          (localPreimage (FA := FA) (CA := CA) f₁ x₁ f sorry) :
        CA (F₂.obj (op Y))) :
    CA (F₃.obj (op Y)))
  ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y) ≫ f₂.app (op Y)) :
        (a : CA (F₁.obj (op Y))) → CA (F₃.obj (op Y)))
      (localPreimage (FA := FA) (CA := CA) f₁ x₂ f sorry) :
    CA (F₃.obj (op Y)))
Tactic: rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, app_localPreimage,
        app_localPreimage, NatTrans.naturality_apply, NatTrans.naturality_apply, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (hypothesis)
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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst_4 : IsLocallyInjective (FD := FA) (CD := CA) J f₃
inst_5 : IsLocallySurjective J (FA := FA) (CA := CA) f₁
⊢ IsLocallyInjective (FD := FA) (CD := CA) J f₂
have inst : IsLocallyInjective (FD := FA) (CD := CA) J (f₁ ≫ f₂)
Tactic: subst fac
Cleared hypotheses: f₃, fac, inst_4
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
⊢ imageSieve (FA := FA) (CA := CA) f₁ x ∈ (J : (a : C) → Set (Sieve a)) X
have refine_1 : Sieve.bind S.arrows T ≤ imageSieve (FA := FA) (CA := CA) f₁ x
Tactic: refine J.superset_covering ?_ (J.transitive (imageSieve_mem J (f₁ ≫ f₂) (f₂.app _ x))
      (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
refine_1 : Sieve.bind S.arrows T ≤ imageSieve (FA := FA) (CA := CA) f₁ x
⊢ imageSieve (FA := FA) (CA := CA) f₁ x ∈ (J : (a : C) → Set (Sieve a)) X
have refine_2 : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop (op X)⦄,
  Sieve.arrows
      (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
        ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
          x))
      f →
    Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: refine J.superset_covering ?_ (J.transitive (imageSieve_mem J (f₁ ≫ f₂) (f₂.app _ x))
      (Sieve.bind S.1 T) ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.LocallySurjective (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₁ F₂ F₃ : Functor.{v, v', u, u'} Cᵒᵖ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst_4 : IsLocallySurjective J (FA := FA) (CA := CA) (f₁ ≫ f₂)
inst_5 : IsLocallyInjective (FD := FA) (CD := CA) J f₂
X : C
x : ToType.{w', v', u', u_1} (FC := FA) (CC := CA) (F₂.obj (op X))
S : Sieve.{v, u} X :=
  imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
    ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve.{v, u} Y :=
  fun (Y : C) (f : Y ⟶ X) (hf : S.arrows f) ↦
    equalizerSieve.{w', v', v, u', u, u_1} (FD := FA) (CD := CA) (F := F₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₁.app (op Y)) : (a : CA (F₁.obj (op Y))) → CA (F₂.obj (op Y)))
        (localPreimage (FA := FA) (CA := CA) (f₁ ≫ f₂)
          ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X)))
            x)
          f hf))
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (F₂.map f.op) : (a : CA (F₂.obj (op X))) → CA (F₂.obj (op Y))) x)
Y : C
f : Y ⟶ unop (op X)
hf :
  Sieve.arrows
    (imageSieve (FA := FA) (CA := CA) (f₁ ≫ f₂)
      ((ConcreteCategory.hom (FC := FA) (CC := CA) (f₂.app (op X)) : (a : CA (F₂.obj (op X))) → CA (F₃.obj (op X))) x))
    f
⊢ Sieve.pullback f (Sieve.bind S.arrows T) ∈ (J : (a : C) → Set (Sieve a)) Y
have refine_2 : T f hf ∈ (J : (a : C) → Set (Sieve a)) Y
Tactic: apply J.superset_covering (Sieve.le_pullback_bind _ _ _ hf)