awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
⊢ ∃ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
    R = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [Precoverage.mem_iff_exists_zeroHypercover] at hR

Premises used: CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  ∃ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
    R = Presieve.ofArrows 𝒰.X 𝒰.f
obtain :
  ∀ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
    ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = R

Tactic:
obtain ⟨𝒰, rfl⟩ := hR

Premises used: rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
i : 𝒰.I₀
⊢ Over.Hom.left (𝒰.f i) ≫ X.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    Comma.hom
      (Comma.toComma (P := P) (Q := ⊤) (W := ⊤) ((fun (i : 𝒰.I₀) ↦ (Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯ : P.Over ⊤ S)) i))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
refine_2 : ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
refine_1 : ∀ (i : 𝒰.I₀), P (𝒰.X i).hom
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
let 𝒱 : PreZeroHypercover X :=
    ⟨𝒰.I₀, fun i ↦ Over.mk _ (𝒰.X i).hom ?_, fun i ↦ Over.homMk (𝒰.f i).left (by simp) trivial⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯,
    f := fun (i : 𝒰.I₀) ↦ Over.homMk (P := P) (Q := ⊤) (Over.Hom.left (𝒰.f i)) ⋯ trivial }
h : Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
use 𝒱.presieve₀

Premises used: CategoryTheory.PreZeroHypercover.presieve₀
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯,
    f := fun (i : 𝒰.I₀) ↦ Over.homMk (P := P) (Q := ⊤) (Over.Hom.left (𝒰.f i)) ⋯ trivial }
h :
  (Presieve.ofArrows (fun (i : 𝒱.I₀) ↦ Functor.obj (Over.forget P ⊤ S) (𝒱.X i)) fun (i : 𝒱.I₀) ↦
      Functor.map (Over.forget P ⊤ S) (𝒱.f i)) =
    Presieve.ofArrows 𝒰.X 𝒰.f
⊢ Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rw [Presieve.map_ofArrows]

Premises used: CategoryTheory.Presieve.map_ofArrows
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯,
    f := fun (i : 𝒰.I₀) ↦ Over.homMk (P := P) (Q := ⊤) (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ (Presieve.ofArrows (fun (i : 𝒱.I₀) ↦ Functor.obj (Over.forget P ⊤ S) (𝒱.X i)) fun (i : 𝒱.I₀) ↦
      Functor.map (Over.forget P ⊤ S) (𝒱.f i)) =
    Presieve.ofArrows 𝒰.X 𝒰.f

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
i : 𝒰.I₀
refine_1 : P (Over.Hom.left (𝒰.f i) ≫ (Functor.obj (Over.forget P ⊤ S) X).hom)
⊢ P (𝒰.X i).hom

Tactic:
rw [← CategoryTheory.Over.w (𝒰.f i)]

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Over.w, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
i : 𝒰.I₀
⊢ P (Over.Hom.left (𝒰.f i) ≫ (Functor.obj (Over.forget P ⊤ S) X).hom)

Tactic:
P.comp_mem _ _ (H _ 𝒰.mem₀ ⟨⟨i⟩⟩) X.prop

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Presieve.map.of
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
i : 𝒰.I₀
⊢ P (Over.Hom.left (𝒰.f i) ≫ (Functor.obj (Over.forget P ⊤ S) X).hom)

Tactic:
exact P.comp_mem _ _ (H _ 𝒰.mem₀ ⟨⟨i⟩⟩) X.prop

Premises used: CategoryTheory.Presieve.ofArrows.mk, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Precoverage.ZeroHypercover.mem₀, CategoryTheory.Presieve.map.of
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
rw :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)

Tactic:
rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]

Premises used: CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
H₁ :
  ∀ {S_1 : P.Over ⊤ S} {R : Presieve (Functor.obj (Over.forget P ⊤ S) S_1)},
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1)) R →
      Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1))
        (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck

Tactic:
apply Precoverage.locallyCoverDense_of_map_functorPullback_mem

Premises used: CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
H₁ :
  ∀ (R : Presieve X)
    (hR :
      Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
        (Presieve.map (Over.forget P ⊤ S) R)),
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
      (Presieve.map (Over.forget P ⊤ S)
        (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) R)))
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))

Tactic:
obtain ⟨R, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve _ H hR

Premises used: CategoryTheory.MorphismProperty.exists_map_eq_of_presieve, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve X
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) R)
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S)
      (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) R)))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
rw : Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck

Tactic:
rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]

Premises used: CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)

Tactic:
MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H

Premises used: CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)

Tactic:
exact MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H

Premises used: CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck

Tactic:
have : (Over.forget P ⊤ S).LocallyCoverDense
      (K.comap (CategoryTheory.Over.forget S)).toGrothendieck := by
    rw [← over_toGrothendieck_eq_toGrothendieck_comap_forget]
    exact MorphismProperty.locallyCoverDense_forget_of_le (S := S) K H
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
rw :
  Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck (Precoverage.comap (Over.forget P ⊤ S ⋙ CategoryTheory.Over.forget S) K))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))

Tactic:
rw [Precoverage.comap_comp]

Premises used: CategoryTheory.Precoverage.comap_comp
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
simp_rw :
  Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck)
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (K.toGrothendieck.over S))

Tactic:
simp_rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]

Premises used: CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
H₁ :
  ∀ {S_1 : P.Over ⊤ S} {R : Presieve (Functor.obj (Over.forget P ⊤ S) S_1)},
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1)) R →
      Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1))
        (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
⊢ Eq (α := GrothendieckTopology (P.Over ⊤ S))
    (Precoverage.toGrothendieck
      (Precoverage.comap (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K)))
    (Functor.inducedTopology (Over.forget P ⊤ S) (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck)

Tactic:
apply Precoverage.toGrothendieck_comap_eq_inducedTopology

Premises used: CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
H₁ :
  ∀ (T : Presieve X)
    (hR :
      Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
        ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
        (Presieve.map (Over.forget P ⊤ S) T)),
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
      (Presieve.map (Over.forget P ⊤ S)
        (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) T)))
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))

Tactic:
obtain ⟨T, rfl⟩ := MorphismProperty.exists_map_eq_of_presieve K H hR

Premises used: CategoryTheory.MorphismProperty.exists_map_eq_of_presieve, rfl
-- Module: Mathlib.CategoryTheory.MorphismProperty.CommaSites
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
this :
  Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
X : P.Over ⊤ S
T : Presieve X
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S) T)
⊢ Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X))
    (Presieve.map (Over.forget P ⊤ S)
      (Presieve.functorPullback (Over.forget P ⊤ S) (Presieve.map (Over.forget P ⊤ S) T)))

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
X : C
⊢ W (𝟙 X)

Tactic:
ContainsIdentities.id_mem X

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} C
inst_2 : W.ContainsIdentities
⊢ ContainsIdentities.{v, u} (C := Cᵒᵖ) W.op

Tactic:
⟨fun X => W.id_mem X.unop⟩

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.mk, CategoryTheory.MorphismProperty.id_mem, Opposite.unop
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
W : MorphismProperty.{v, u} Cᵒᵖ
inst_2 : ContainsIdentities.{v, u} (C := Cᵒᵖ) W
⊢ W.unop.ContainsIdentities

Tactic:
⟨fun X => W.id_mem (Opposite.op X)⟩

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.mk, Opposite.op, CategoryTheory.MorphismProperty.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : ContainsIdentities.{v, u} (C := Cᵒᵖ) W.op
⊢ W.ContainsIdentities

Tactic:
(inferInstance : W.op.unop.ContainsIdentities)

Premises used: CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, inferInstance, CategoryTheory.MorphismProperty.op
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} Cᵒᵖ
inst_1 : W.unop.ContainsIdentities
⊢ ContainsIdentities.{v, u} (C := Cᵒᵖ) W

Tactic:
(inferInstance : W.unop.op.ContainsIdentities)

Premises used: Quiver.Hom.op, CategoryTheory.MorphismProperty.unop, Quiver.Hom.unop, inferInstance, CategoryTheory.MorphismProperty.op
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x y : C
h : x = y
subst : W (CategoryTheory.eqToHom ⋯)
⊢ W (CategoryTheory.eqToHom h)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x : C
rw : W (𝟙 x)
⊢ W (CategoryTheory.eqToHom ⋯)

Tactic:
rw [eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Tactic:
id_mem x

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.id_mem
-- Module: Mathlib.CategoryTheory.MorphismProperty.Composition
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
inst_1 : W.ContainsIdentities
x : C
⊢ W (𝟙 x)

Tactic:
exact id_mem x

Premises used: CategoryTheory.MorphismProperty.ContainsIdentities.id_mem