awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
⊢ map F (functorPullback F R) ≤ (Sieve.generate (map F (functorPullback F R))).arrows

Tactic:
Sieve.le_generate _

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
U : C
x : (↑((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) : Type (max u_4 v_4))
T : Sieve.{v_4, u_4} (F.obj U)
hT : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
R : Presieve.{v_4, u_4} (F.obj U)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R
hle : R ≤ T.arrows
⊢ map F (functorPullback F R) ≤ (Sieve.generate (map F (functorPullback F R))).arrows

Tactic:
exact Sieve.le_generate _

Premises used: CategoryTheory.Sieve.le_generate
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
⊢ F.LocallyCoverDense K.toGrothendieck

Tactic:
haveI : F.LocallyCoverDense K.toGrothendieck :=
    K.locallyCoverDense_of_map_functorPullback_mem F H
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck = F.inducedTopology K.toGrothendieck

Tactic:
le_antisymm ?_ fun X T hT ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
refine_1 : (comap F K).toGrothendieck ≤ F.inducedTopology K.toGrothendieck
refine_2 :
  ∀ (X : C) (T : Sieve.{v_3, u_3} X) (hT : T ∈ (F.inducedTopology K.toGrothendieck : (a : C) → Set (Sieve a)) X),
    T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ (comap F K).toGrothendieck = F.inducedTopology K.toGrothendieck

Tactic:
refine le_antisymm ?_ fun X T hT ↦ ?_

Premises used: le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck ≤ F.inducedTopology K.toGrothendieck

Tactic:
apply toGrothendieck_comap_le_inducedTopology

Premises used: CategoryTheory.Precoverage.toGrothendieck_comap_le_inducedTopology
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
hT : T ∈ (F.inducedTopology K.toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
    (Sieve.functorPushforward F T)

Tactic:
rw [Functor.mem_inducedTopology_sieves_iff] at hT

Premises used: CategoryTheory.Functor.mem_inducedTopology_sieves_iff
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
hT :
  Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
    (Sieve.functorPushforward F T)
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj X)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R ∧
      R ≤ (Sieve.functorPushforward F T).arrows

Tactic:
rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT

Premises used: CategoryTheory.Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
hT :
  ∃ (R : Presieve.{v_4, u_4} (F.obj X)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R ∧
      R ≤ (Sieve.functorPushforward F T).arrows
refine_2 :
  ∀ (R : Presieve.{v_4, u_4} (F.obj X))
    (hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R)
    (hle : R ≤ (Sieve.functorPushforward F T).arrows), T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
obtain ⟨R, hR, hle⟩ := hT
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
refine_2 : Sieve.generate (functorPullback F R) ≤ T
refine_2₁ : Sieve.generate (functorPullback F R) ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
refine GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_

Premises used: CategoryTheory.GrothendieckTopology.superset_covering
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ≤ T

Tactic:
le_trans (le_trans (Sieve.generate_functorPullback_le F R)
        (Sieve.functorPullback_monotone _ _ (Sieve.generate_mono hle))) ?_

Premises used: CategoryTheory.Sieve.generate_mono, CategoryTheory.Sieve.generate_functorPullback_le, CategoryTheory.Sieve.functorPullback_monotone, le_trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
refine_2 : Sieve.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T
⊢ Sieve.generate (functorPullback F R) ≤ T

Tactic:
refine le_trans (le_trans (Sieve.generate_functorPullback_le F R)
        (Sieve.functorPullback_monotone _ _ (Sieve.generate_mono hle))) ?_

Premises used: CategoryTheory.Sieve.generate_mono, CategoryTheory.Sieve.generate_functorPullback_le, CategoryTheory.Sieve.functorPullback_monotone, le_trans
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
refine_2 : Sieve.functorPullback F (Sieve.functorPushforward F T) ≤ T
refine_2₁ refine_2₂ : T ≤ T
⊢ Sieve.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T

Tactic:
rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]

Premises used: CategoryTheory.Sieve.generate_sieve, CategoryTheory.Sieve.functorPullback_functorPushforward_eq
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
Precoverage.generate_mem_toGrothendieck (H hR)

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Goal:
C : Type u_3
D : Type u_4
inst : Category.{v_3, u_3} C
inst_1 : Category.{v_4, u_4} D
F : Functor.{v_3, v_4, u_3, u_4} C D
K : Precoverage.{v_4, u_4} D
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
inst_6 : F.Faithful
inst_7 : F.Full
H :
  ∀ {S : C} {R : Presieve.{v_4, u_4} (F.obj S)},
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) R →
      Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj S))) (K.coverings (F.obj S)) (map F (functorPullback F R))
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve.{v_3, u_3} X
R : Presieve.{v_4, u_4} (F.obj X)
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) R
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X

Tactic:
exact Precoverage.generate_mem_toGrothendieck (H hR)

Premises used: CategoryTheory.Precoverage.generate_mem_toGrothendieck
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
a b : ℤ
⊢ -(a + b) = -a + -b

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
n : ℤ
⊢ Functor.Additive.{v_1, u_1, v_1, u_1} (C := Cᵒᵖ) (shiftFunctor Cᵒᵖ n)

Tactic:
inferInstanceAs <| (shiftFunctor (OppositeShiftAux C) n).Additive

Premises used: _private.0.CategoryTheory.Pretriangulated.Opposite.instAdditiveOppositeShiftFunctorInt._proof_1
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n m : ℤ
hnm : n + m = 0
obtain :
  ∀ (hnm : n + -n = 0),
    Eq (α := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ) (shiftFunctor Cᵒᵖ n) (Functor.op (shiftFunctor C (-n)))
⊢ Eq (α := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ) (shiftFunctor Cᵒᵖ n) (Functor.op (shiftFunctor C m))

Tactic:
obtain rfl : m = -n := by lia

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
n : ℤ
hnm : n + -n = 0
⊢ Eq (α := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ) (shiftFunctor Cᵒᵖ n) (Functor.op (shiftFunctor C (-n)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorOpIso C 0 0 ⋯)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.inv (shiftFunctorZero C ℤ)) (Opposite.unop X)))

Tactic:
rfl

Premises used: CategoryTheory.Functor.op, Quiver.Hom.op, CategoryTheory.shiftFunctor, Int.neg, rfl, Int.negOfNat
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ + b₂ = b₃

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
dsimp : b₁ = -a₁
⊢ b₁ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₁

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ = -a₁

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
dsimp : b₂ = -a₂
⊢ b₂ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₂ = -a₂

Tactic:
lia
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
dsimp : b₃ = -a₃
⊢ b₃ = (AddMonoidHom.mk' (fun (n : ℤ) ↦ -n) OppositeShiftAux._proof_1 : (a : ℤ) → ℤ) a₃

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₃ = -a₃

Tactic:
lia