awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
i : I
g : X ⟶ Y i
Z : C
h : Z ⟶ X
⊢ arrows (ofObjects Y X) h ↔ arrows ⊤ h
have h₁ : arrows (ofObjects Y X) h
Tactic: simp only [top_apply, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
I : Type u_1
X : I → C
Y Z : C
f : Z ⟶ Y
⊢ pullback f (ofObjects X Y) = ofObjects X Z
have h : ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Z), (pullback f (ofObjects X Y)).arrows f_1 ↔ arrows (ofObjects X Z) f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
R : Sieve.{v₁, u₁} Z
W : C
h : W ⟶ X
h_1 : (pushforward f (pushforward g R)).arrows h
y : W ⟶ Y
hy : y ≫ f = h
z : W ⟶ Z
hR : z ≫ g = y
hz : R.arrows z
⊢ z ≫ g ≫ f = h ∧ R.arrows z
have rw : y ≫ f = h ∧ R.arrows z
Tactic: rw [← Category.assoc, hR]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
S : Presieve.{v₁, u₁} X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve.{v₁, u₁} Y
f : Y ⟶ X
h : S f
⊢ R h ≤ pullback f (bind S R)
have rw : pushforward f (R h) ≤ bind S R
Tactic: rw [← galoisConnection f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : Mono f
⊢ GaloisCoinsertion (pushforward f) (pullback f)
have apply : ∀ (b : Sieve.{v₁, u₁} Y), pullback f (pushforward f b) ≤ b
Tactic: apply (galoisConnection f).toGaloisCoinsertion
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z_1 : C
f_1 : Y ⟶ X
S_1 R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : Mono f
S : Sieve.{v₁, u₁} Y
Z : C
g g₁ : Z ⟶ Y
hf : g₁ ≫ f = g ≫ f
hg₁ : S.arrows g₁
⊢ S.arrows g
have hf₁ : g₁ = g
Tactic: rw [cancel_mono f] at hf
Cleared hypotheses: hf, hg₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R : Sieve.{v₁, u₁} X
f : Y ⟶ X
inst_2 : IsSplitEpi f
⊢ GaloisInsertion (pushforward f) (pullback f)
have apply : ∀ (b : Sieve.{v₁, u₁} X), b ≤ pushforward f (pullback f b)
Tactic: apply (galoisConnection f).toGaloisInsertion
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)
have h : ∀ ⦃W : C⦄ (g : W ⟶ Y), (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
Tactic: ext W g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
have h : (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W : C
g : W ⟶ Y
h : (generate (Presieve.pullbackArrows f R)).arrows g → (pullback f (generate R)).arrows g
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
have h₁ : (pullback f (generate R)).arrows g → (generate (Presieve.pullbackArrows f R)).arrows g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)
have this : HasPullback g f
Tactic: have := R.hasPullback f hg
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y_1 : C
f : Y_1 ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 Y W : C
g : W ⟶ X
hg : R g
h : W_1 ⟶ Limits.pullback g f
this : HasPullback g f
⊢ (pullback f (generate R)).arrows (h ≫ pullback.snd g f)
have h₁ : (generate R).arrows ((h ≫ pullback.fst g f) ≫ g)
Tactic: rw [Sieve.pullback_apply, assoc, ← pullback.condition, ← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve.{v₁, u₁} X
inst_1 : R.HasPullbacks f
W_1 : C
g : W_1 ⟶ Y
W : C
h : W_1 ⟶ W
k : W ⟶ X
hk : R k
comm : h ≫ k = g ≫ f
⊢ (generate (Presieve.pullbackArrows f R)).arrows g
have this : HasPullback k f
Tactic: have := R.hasPullback f hk
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₂, u₂} (F.obj X)
Y_1 Z_1 : C
f : Y_1 ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z_1 ⟶ Y_1
⊢ R.arrows (F.map (g ≫ f))
have rw : R.arrows (F.map g ≫ F.map f)
Tactic: rw [F.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Sieve.{v₁, u₁} X
⊢ functorPullback (𝟭 C) R = R
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), arrows (functorPullback (𝟭 C) R) f ↔ R.arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₃, u₃} ((F ⋙ G).obj X)
⊢ functorPullback (F ⋙ G) R = functorPullback F (functorPullback G R)
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), (functorPullback (F ⋙ G) R).arrows f ↔ (functorPullback F (functorPullback G R)).arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Presieve.{v₂, u₂} (F.obj X)
⊢ generate (Presieve.functorPullback F R) ≤ functorPullback F (generate R)
have rw : Presieve.functorPullback F R ≤ (functorPullback F (generate R)).arrows
Tactic: rw [generate_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : X ⟶ Y
S : Sieve.{v₂, u₂} (F.obj Y)
⊢ functorPullback F (pullback (F.map f) S) = pullback f (functorPullback F S)
have h : ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ X),
  (functorPullback F (pullback (F.map f) S)).arrows f_1 ↔ (pullback f (functorPullback F S)).arrows f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Presieve.{v₁, u₁} X
⊢ Presieve.functorPushforward F (generate R).arrows = Presieve.functorPushforward F R
have h : ∀ (Y : D),
  Eq (α := (Y ⟶ F.obj X) → Prop) (Presieve.functorPushforward F (generate R).arrows) (Presieve.functorPushforward F R)
Tactic: funext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Presieve.{v₁, u₁} X
Y : D
⊢ Eq (α := (Y ⟶ F.obj X) → Prop) (Presieve.functorPushforward F (generate R).arrows) (Presieve.functorPushforward F R)
have h : ∀ (f : Y ⟶ F.obj X), Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f
Tactic: ext f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
⊢ Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f
have h : Presieve.functorPushforward F (generate R).arrows f → Presieve.functorPushforward F R f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
h : Presieve.functorPushforward F (generate R).arrows f → Presieve.functorPushforward F R f
⊢ Presieve.functorPushforward F (generate R).arrows f ↔ Presieve.functorPushforward F R f
have h₁ : Presieve.functorPushforward F R f → Presieve.functorPushforward F (generate R).arrows f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : C
f_1 : Y ⟶ X
S R_1 : Sieve.{v₁, u₁} X
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₁, u₁} X
Y_1 Z_1 : D
f : Y_1 ⟶ F.obj X
h : Presieve.functorPushforward F R.arrows f
g : Z_1 ⟶ Y_1
⊢ Presieve.functorPushforward F R.arrows (g ≫ f)
have obtain : ∀ (X_1 : C) (α : X_1 ⟶ X) (β : Y_1 ⟶ F.obj X_1) (hα : R.arrows α),
  Presieve.functorPushforward F R.arrows (g ≫ β ≫ F.map α)
Tactic: obtain ⟨X, α, β, hα, rfl⟩ := h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
s : Presieve.{v₁, u₁} X
⊢ generate (Presieve.map F s) = functorPushforward F (generate s)
have h : ∀ ⦃Y : D⦄ (f : Y ⟶ F.obj X), (generate (Presieve.map F s)).arrows f ↔ (functorPushforward F (generate s)).arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
s : Presieve.{v₁, u₁} X
Y : D
f : Y ⟶ F.obj X
⊢ (generate (Presieve.map F s)).arrows f ↔ (functorPushforward F (generate s)).arrows f
have h : Presieve.functorPushforward F s f ↔ (functorPushforward F (generate s)).arrows f
Tactic: rw [arrows_generate_map_eq_functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ functorPushforward F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
have rw : generate (Presieve.map F (Presieve.ofArrows Y f)) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
Tactic: rw [← generate_map_eq_functorPushforward, Presieve.map_ofArrows]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
rw : generate (Presieve.map F (Presieve.ofArrows Y f)) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
⊢ functorPushforward F (ofArrows Y f) = ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)
have rw₁ : Eq (α := Sieve.{v₂, u₂} (F.obj X)) (generate (Presieve.ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i)))
  (ofArrows (fun (i : ι) ↦ F.obj (Y i)) fun (i : ι) ↦ F.map (f i))
Tactic: rw [← generate_map_eq_functorPushforward, Presieve.map_ofArrows]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
R : Sieve.{v₁, u₁} X
⊢ functorPushforward (𝟭 C) R = R
have h : ∀ ⦃X_1 : C⦄ (f : X_1 ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X), arrows (functorPushforward (𝟭 C) R) f ↔ R.arrows f
Tactic: ext X f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
⊢ arrows (functorPushforward (𝟭 C) R) f ↔ R.arrows f
have h : arrows (functorPushforward (𝟭 C) R) f → R.arrows f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
h : arrows (functorPushforward (𝟭 C) R) f → R.arrows f
⊢ arrows (functorPushforward (𝟭 C) R) f ↔ R.arrows f
have h₁ : R.arrows f → arrows (functorPushforward (𝟭 C) R) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X_1 : C
R : Sieve.{v₁, u₁} X_1
X : C
f : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_1
hf : arrows (functorPushforward (𝟭 C) R) f
⊢ R.arrows f
have h : ∀ (X_2 : C) (g : X_2 ⟶ X_1) (h : X ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X_2) (hg : R.arrows g),
  R.arrows (h ≫ Functor.map (𝟭 C) g)
Tactic: obtain ⟨X, g, h, hg, rfl⟩ := hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
R : Sieve.{v₁, u₁} X
⊢ functorPushforward (F ⋙ G) R = functorPushforward G (functorPushforward F R)
have h : ∀ ⦃Y : E⦄ (f : Y ⟶ (F ⋙ G).obj X),
  (functorPushforward (F ⋙ G) R).arrows f ↔ (functorPushforward G (functorPushforward F R)).arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Sieve.{v₁, u₁} X
S : Sieve.{v₂, u₂} (F.obj X)
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S
have mp : functorPushforward F R ≤ S → R ≤ functorPullback F S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
R : Sieve.{v₁, u₁} X
S : Sieve.{v₂, u₂} (F.obj X)
mp : functorPushforward F R ≤ S → R ≤ functorPullback F S
⊢ functorPushforward F R ≤ S ↔ R ≤ functorPullback F S
have mpr : R ≤ functorPullback F S → functorPushforward F R ≤ S
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
⊢ (functorPullback F S).arrows f
have mp : (functorPushforward F R).arrows (F.map f)
Tactic: apply hle
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
⊢ (functorPushforward F R).arrows (F.map f)
have mp : F.map f = 𝟙 (F.obj X) ≫ F.map f
Tactic: refine ⟨X, f, 𝟙 _, hf, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : functorPushforward F R ≤ S
X : C
f : X ⟶ X_1
hf : R.arrows f
⊢ F.map f = 𝟙 (F.obj X) ≫ F.map f
have mp : F.map f = F.map f
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 : C
R : Sieve.{v₁, u₁} X_1
S : Sieve.{v₂, u₂} (F.obj X_1)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X_1
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (h ≫ F.map g)
have mpr : S.arrows (F.map g)
Tactic: apply Sieve.downward_closed S
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (functorPushforward F ⊤) ⊤
have refine : Eq (α := Sieve.{v₂, u₂} (F.obj X)) (generate (arrows (functorPushforward F ⊤))) ⊤
Tactic: refine (generate_sieve _).symm.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Eq (α := Sieve.{v₂, u₂} (F.obj X)) (generate (arrows (functorPushforward F ⊤))) ⊤
have apply : arrows (functorPushforward F ⊤) (𝟙 (F.obj X))
Tactic: apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
⊢ functorPushforward F (pullback f S) ≤ pullback (F.map f) (functorPushforward F S)
have rw : pullback f S ≤ pullback f (functorPullback F (functorPushforward F S))
Tactic: rw [Sieve.functorPushforward_le_iff_le_functorPullback, Sieve.functorPullback_pullback]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
f : Y ⟶ X
S : Sieve.{v₁, u₁} X
⊢ pullback f S ≤ pullback f (functorPullback F (functorPushforward F S))
have a : S ≤ functorPullback F (functorPushforward F S)
Tactic: apply Sieve.pullback_monotone
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y Z : C
f : Y ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
⊢ GaloisInsertion (α := Sieve.{v₁, u₁} X) (functorPushforward F) (functorPullback F)
have apply : ∀ (b : Sieve.{v₂, u₂} (F.obj X)), b ≤ functorPushforward F (functorPullback F b)
Tactic: apply (functor_galoisConnection F X).toGaloisInsertion
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.EssSurj
inst_4 : F.Full
X : C
S : Sieve.{v₂, u₂} (F.obj X)
Y : D
f : Y ⟶ F.obj X
hf : S.arrows f
⊢ (functorPushforward F (functorPullback F S)).arrows f
have refine : (functorPullback F S).arrows (Y := F.objPreimage Y) (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)) ∧
  f =
    CategoryStruct.comp (Y := F.obj (F.objPreimage Y)) (Iso.inv (F.objObjPreimageIso Y))
      (F.map (F.preimage (Iso.hom (F.objObjPreimageIso Y) ≫ f)))
Tactic: refine ⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y Z : C
f : Y ⟶ X_1
S R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
⊢ GaloisCoinsertion (α := Sieve.{v₁, u₁} X) (functorPushforward F) (functorPullback F)
have apply : ∀ (b : Sieve.{v₁, u₁} X), functorPullback F (functorPushforward F b) ≤ b
Tactic: apply (functor_galoisConnection F X).toGaloisCoinsertion
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = h ≫ F.map g
⊢ S.arrows f
have h₃ : F.map f = F.map (F.preimage h ≫ g)
Tactic: rw [← F.map_preimage h, ← F.map_comp] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y_1 Z_1 : C
f_1 : Y_1 ⟶ X_1
S_1 R : Sieve.{v₁, u₁} X_1
E : Type u₃
inst_2 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : F.Full
inst_4 : F.Faithful
X : C
S : Sieve.{v₁, u₁} X
Y : C
f : Y ⟶ X
Z : C
g : Z ⟶ X
h : F.obj Y ⟶ F.obj Z
h₁ : S.arrows g
h₂ : F.map f = F.map (F.preimage h ≫ g)
⊢ S.arrows f
have rw : S.arrows (F.preimage h ≫ g)
Tactic: rw [F.map_injective h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ functorPushforward e.functor S = functorPullback e.inverse (pullback (e.unitInv.app X) S)
have h : ∀ ⦃Y : D⦄ (iYX : Y ⟶ e.functor.obj X),
  (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
Tactic: ext Y iYX
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
have h : (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
S : Sieve.{v₁, u₁} X
e : Equivalence.{v₁, v₂, u₁, u₂} C D
Y : D
iYX : Y ⟶ e.functor.obj X
h : (functorPushforward e.functor S).arrows iYX → (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ (functorPushforward e.functor S).arrows iYX ↔ (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
have h₁ : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX → (functorPushforward e.functor S).arrows iYX
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
U : C
S : Sieve.{v₁, u₁} U
⊢ functorPushforward e.inverse (functorPushforward e.functor S) = pullback (e.unitInv.app U) S
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ e.inverse.obj (e.functor.obj U)),
  (functorPushforward e.inverse (functorPushforward e.functor S)).arrows f ↔ (pullback (e.unitInv.app U) S).arrows f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Sieves (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : Equivalence.{v₁, v₂, u₁, u₂} C D
X : C
S : Sieve.{v₁, u₁} X
⊢ pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S)) = S
have h : ∀ ⦃Y : C⦄ (f : Y ⟶ Functor.obj.{v₁, v₁, u₁, u₁} (𝟭 C) X),
  (pullback (e.unit.app X) (functorPushforward e.inverse (functorPushforward e.functor S))).arrows f ↔ S.arrows f
Tactic: ext