awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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_1 : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) T
hT :
  ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧ R ≤ T.arrows
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT_1) :
                Sieve (F.obj U)))).arrows
have obtain : ∀ (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),
  ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT_1) :
                Sieve (F.obj U)))).arrows
Tactic: obtain ⟨R, hR, hle⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ ∃ (R : Presieve.{v_4, u_4} (F.obj U)),
    Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj U))) (K.coverings (F.obj U)) R ∧
      R ≤
        (Sieve.functorPushforward F
            (Sieve.functorPullback F
              (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                    Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                      ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                    T hT) :
                Sieve (F.obj U)))).arrows
have refine : map F (functorPullback F R) ≤
  (Sieve.functorPushforward F
      (Sieve.functorPullback F
        (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
              Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
              T hT) :
          Sieve (F.obj U)))).arrows
Tactic: refine ⟨_, H hR, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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.functorPushforward F
        (Sieve.functorPullback F
          (↑(Subtype.mk (p := fun (x : Sieve.{v_4, u_4} (F.obj U)) ↦
                Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U)))
                  ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U)) x)
                T hT) :
            Sieve (F.obj U)))).arrows
have refine : map F (functorPullback F R) ≤ functorPushforward F (functorPullback F R)
Tactic: refine le_trans ?_
      (Presieve.functorPushforward_monotone (Presieve.functorPullback_monotone hle))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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) ≤ functorPushforward F (functorPullback F R)
have rw : map F (functorPullback F R) ≤ (Sieve.generate (map F (functorPullback F R))).arrows
Tactic: rw [← Sieve.arrows_generate_map_eq_functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (hypothesis)
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))
⊢ (comap F K).toGrothendieck = F.inducedTopology K.toGrothendieck
have this : F.LocallyCoverDense K.toGrothendieck
Tactic: haveI : F.LocallyCoverDense K.toGrothendieck :=
    K.locallyCoverDense_of_map_functorPullback_mem F H
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
have refine_1 : (comap F K).toGrothendieck ≤ F.inducedTopology K.toGrothendieck
Tactic: refine le_antisymm ?_ fun X T hT ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ (comap F K).toGrothendieck = F.inducedTopology K.toGrothendieck
have 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
Tactic: refine le_antisymm ?_ fun X T hT ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (hypothesis)
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
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
have 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)
Tactic: rw [Functor.mem_inducedTopology_sieves_iff] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (hypothesis)
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)
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
have 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
Tactic: rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
have 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
Tactic: obtain ⟨R, hR, hle⟩ := hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
have refine_2 : Sieve.generate (functorPullback F R) ≤ T
Tactic: refine GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ T ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
have refine_2₁ : Sieve.generate (functorPullback F R) ∈ ((comap F K).toGrothendieck : (a : C) → Set (Sieve a)) X
Tactic: refine GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
have refine_2 : Sieve.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T
Tactic: refine le_trans (le_trans (Sieve.generate_functorPullback_le F R)
        (Sieve.functorPullback_monotone _ _ (Sieve.generate_mono hle))) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T
have refine_2 : Sieve.functorPullback F (Sieve.functorPushforward F T) ≤ T
Tactic: rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
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
⊢ Sieve.functorPullback F (Sieve.generate (Sieve.functorPushforward F T).arrows) ≤ T
have refine_2₁ : T ≤ T
Tactic: rw [Sieve.generate_sieve, Sieve.functorPullback_functorPushforward_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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
⊢ Eq (α := Functor.{v_1, v_1, u_1, u_1} Cᵒᵖ Cᵒᵖ) (shiftFunctor Cᵒᵖ n) (Functor.op (shiftFunctor C m))
have 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)))
Tactic: obtain rfl : m = -n := by lia
Cleared hypotheses: m, hnm
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
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} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw : 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} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
  (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X)
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Opposite.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
X : Cᵒᵖ
rw :
  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} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫ NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
      Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (𝟭 Cᵒᵖ) X ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X)
    (NatTrans.app (Iso.inv (shiftFunctorZero Cᵒᵖ ℤ)) X)
    (Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 ⋯)) X)
have rw₁ : 𝟙 (Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor Cᵒᵖ (A := ℤ) 0) X) =
  NatTrans.app (Iso.hom (shiftFunctorZero Cᵒᵖ ℤ)) X ≫
    Quiver.Hom.op (NatTrans.app (Iso.hom (shiftFunctorZero C ℤ)) (Opposite.unop X)) ≫
      NatTrans.app (Iso.inv (shiftFunctorOpIso C 0 0 sorry)) X
Tactic: rw [← cancel_epi ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X), Iso.hom_inv_id_app,
    shiftFunctorZero_op_hom_app, assoc, ← op_comp_assoc, Iso.hom_inv_id_app, op_id,
    id_comp, Iso.hom_inv_id_app]