awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
Z : D
U : C
iUY : U ⟶ Y
iZU : Z ⟶ G.obj U
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
⊢ Sieve.pullback iZU (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
    (K : (a : D) → Set (Sieve a)) Z
have h : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
  (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
Tactic: apply K.pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U))) ((K : (a : D) → Set (Sieve a)) (G.obj U))
    (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
have h : ∀ ⦃Y_1 : D⦄ ⦃f : Y_1 ⟶ G.obj U⦄,
  (Sieve.functorPushforward G (G.imageSieve iUW)).arrows f →
    Sieve.pullback f (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
      (K : (a : D) → Set (Sieve a)) Y_1
Tactic: apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback (iZU₁ ≫ G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))) ∈
    (K : (a : D) → Set (Sieve a)) Z
have h : Sieve.pullback iZU₁
    (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))) ∈
  (K : (a : D) → Set (Sieve a)) Z
Tactic: rw [Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
Z : D
U₁ : C
iU₁U : U₁ ⟶ U
iZU₁ : Z ⟶ G.obj U₁
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Sieve.pullback iZU₁
      (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))) ∈
    (K : (a : D) → Set (Sieve a)) Z
have h : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U₁))) ((K : (a : D) → Set (Sieve a)) (G.obj U₁))
  (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))))
Tactic: apply K.pullback_stable
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj U₁))) ((K : (a : D) → Set (Sieve a)) (G.obj U₁))
    (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S))))
have apply : Sieve.functorPushforward G (Sieve.equalizer (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX)) ≤
  Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))
Tactic: apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
      (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X Y : C
S : Sieve.{v_1, u_1} X
iYX : Y ⟶ X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
U : C
iUY : U ⟶ Y
W : C
iWX : W ⟶ X
iUW : G.obj U ⟶ G.obj W
hiWX : S.arrows iWX
e₁ : G.map iUY ≫ G.map iYX = iUW ≫ G.map iWX
U₁ : C
iU₁U : U₁ ⟶ U
iU₁W : U₁ ⟶ W
e₂ : G.map iU₁W = G.map iU₁U ≫ iUW
Z : D
U₂ : C
iU₂U₁ : U₂ ⟶ U₁
iZU₂ : Z ⟶ G.obj U₂
e₃ : iU₂U₁ ≫ iU₁U ≫ iUY ≫ iYX = iU₂U₁ ≫ iU₁W ≫ iWX
⊢ (Sieve.pullback (G.map iU₁U) (Sieve.pullback (G.map iUY) (Sieve.functorPushforward G (Sieve.pullback iYX S)))).arrows
    (iZU₂ ≫ G.map iU₂U₁)
have refine : (Sieve.pullback iYX S).arrows (iU₂U₁ ≫ iU₁U ≫ iUY)
Tactic: refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S'
have h : ∀ ⦃Y : D⦄ ⦃f : Y ⟶ G.obj X⦄,
  (Sieve.functorPushforward G S).arrows f →
    Sieve.pullback f (Sieve.functorPushforward G S') ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: apply K.transitive hS
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback (i ≫ G.map g) (Sieve.functorPushforward G S') ∈ (K : (a : D) → Set (Sieve a)) Y
have h : Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ (K : (a : D) → Set (Sieve a)) Y
Tactic: rw [Sieve.pullback_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Sieve.pullback i (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')) ∈ (K : (a : D) → Set (Sieve a)) Y
have h : Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
  (Sieve.pullback (G.map g) (Sieve.functorPushforward G S'))
Tactic: apply K.pullback_stable i
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg : S.arrows g
⊢ Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Z))) ((K : (a : D) → Set (Sieve a)) (G.obj Z))
    (Sieve.pullback (G.map g) (Sieve.functorPushforward G S'))
have h : Sieve.functorPushforward G (Sieve.pullback g S') ≤ Sieve.pullback (G.map g) (Sieve.functorPushforward G S')
Tactic: refine K.superset_covering ?_ (H' hg)
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
S : Sieve.{v_1, u_1} X
hS :
  Membership.mem (γ := Set (Sieve.{v_1, u_1} X))
    {S : Sieve.{v_1, u_1} X |
      Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj X))) ((K : (a : D) → Set (Sieve a)) (G.obj X))
        (Sieve.functorPushforward G S)}
    S
S' : Sieve.{v_1, u_1} X
H' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f →
      Membership.mem (γ := Set (Sieve.{v_1, u_1} Y))
        {S : Sieve.{v_1, u_1} Y |
          Membership.mem (γ := Set (Sieve.{v_2, u_2} (G.obj Y))) ((K : (a : D) → Set (Sieve a)) (G.obj Y))
            (Sieve.functorPushforward G S)}
        (Sieve.pullback f S')
Y : D
Z : C
g : Z ⟶ X
i : Y ⟶ G.obj Z
hg_1 : S.arrows g
W : D
Z' : C
g' : Z' ⟶ Z
i' : W ⟶ G.obj Z'
hg : (Sieve.pullback g S').arrows g'
⊢ (Sieve.pullback (G.map g) (Sieve.functorPushforward G S')).arrows (i' ≫ G.map g')
have h : (i' ≫ G.map g') ≫ G.map g = i' ≫ G.map (g' ≫ g)
Tactic: refine ⟨Z', g' ≫ g, i', hg, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
⊢ Membership.mem (γ := Set (Sieve.{v_1, u_1} (obj (Over.forget X) Y)))
    ((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y))
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
have h : Sieve.functorPushforward (Over.forget X) (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))) =
  (↑T : Sieve ((Over.forget X).obj Y))
Tactic: convert! T.property
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
⊢ Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))) =
    (↑T : Sieve ((Over.forget X).obj Y))
have h : ∀ ⦃Z : C⦄ (f : Z ⟶ obj (Over.forget X) Y),
  Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f ↔
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f
Tactic: ext Z f
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
f : Z ⟶ obj (Over.forget X) Y
⊢ Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f ↔
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f
have h : Sieve.arrows
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
    f →
  (↑T : Sieve ((Over.forget X).obj Y)).arrows f
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
D : Type u_2
inst_1 : Category.{v_2, u_2} D
G : Functor.{v_1, v_2, u_1, u_2} C D
J : GrothendieckTopology.{v_1, u_1} C
K : GrothendieckTopology.{v_2, u_2} D
A : Type v
inst_2 : Category.{u, v} A
inst_3 : G.LocallyCoverDense K
inst_4 : G.IsLocallyFull K
inst_5 : G.IsLocallyFaithful K
X : C
Y : Over.{v_1, u_1} X
T : (↑((J : (a : C) → Set (Sieve a)) (obj (Over.forget X) Y)) : Type (max u_1 v_1))
Z : C
f : Z ⟶ obj (Over.forget X) Y
h :
  Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f →
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f
⊢ Sieve.arrows
      (Sieve.functorPushforward (Over.forget X)
        (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
      f ↔
    (↑T : Sieve ((Over.forget X).obj Y)).arrows f
have h₁ : (↑T : Sieve ((Over.forget X).obj Y)).arrows f →
  Sieve.arrows
    (Sieve.functorPushforward (Over.forget X)
      (Sieve.functorPullback (Over.forget X) (↑T : Sieve ((Over.forget X).obj Y))))
    f
Tactic: constructor
-- 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 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
⊢ (comap F K).toGrothendieck ≤ F.inducedTopology K.toGrothendieck
have rw : comap F K ≤ (F.inducedTopology K.toGrothendieck).toPrecoverage
Tactic: rw [Precoverage.toGrothendieck_le_iff_le_toPrecoverage]
-- 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 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : R ∈ (comap F K).coverings X
⊢ R ∈ (F.inducedTopology K.toGrothendieck).toPrecoverage.coverings X
have hR₁ : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)
Tactic: rw [Precoverage.mem_comap_iff] at hR
Cleared hypotheses: 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 : F.IsLocallyFull K.toGrothendieck
inst_3 : F.IsLocallyFaithful K.toGrothendieck
inst_4 : F.LocallyCoverDense K.toGrothendieck
X : C
R : Presieve.{v_3, u_3} X
hR : Membership.mem (γ := Set (Presieve.{v_4, u_4} (F.obj X))) (K.coverings (F.obj X)) (map F R)
⊢ R ∈ (F.inducedTopology K.toGrothendieck).toPrecoverage.coverings X
have rw : Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj X))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj X))
  (Sieve.generate (map F R))
Tactic: rw [GrothendieckTopology.mem_toPrecoverage_iff, Functor.mem_inducedTopology_sieves_iff,
    ← Sieve.generate_map_eq_functorPushforward]
-- 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
⊢ Membership.mem (γ := Set (Sieve.{v_4, u_4} (F.obj U))) ((K.toGrothendieck : (a : D) → Set (Sieve a)) (F.obj U))
    (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))))
have rw : ∀
  (hT_1 :
    ∃ (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) :
                Sieve (F.obj U)))).arrows
Tactic: rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT ⊢