awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
inst_1 : P.IsStableUnderBaseChange
inst_2 : HasPullbacks.{v_1, u_1} C
inst_3 : P.IsMultiplicative
rw : P.coverage.toGrothendieck = Pretopology.toGrothendieck P.pretopology
rw₁ : (Pretopology.toCoverage P.pretopology).toGrothendieck = Pretopology.toGrothendieck P.pretopology
rw₂ rw₃ : Pretopology.toGrothendieck P.pretopology = Pretopology.toGrothendieck P.pretopology
⊢ P.grothendieckTopology = Pretopology.toGrothendieck P.pretopology

Tactic:
rw [grothendieckTopology, coverage_eq_toCoverage_pretopology,
    Pretopology.toGrothendieck_toCoverage]

Premises used: CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology, CategoryTheory.MorphismProperty.grothendieckTopology, CategoryTheory.Pretopology.toGrothendieck_toCoverage
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
hPQ : P ≤ Q
⊢ LE.le (α := Pretopology.{v_1, u_1} C) P.pretopology Q.pretopology

Tactic:
precoverage_monotone hPQ

Premises used: CategoryTheory.MorphismProperty.precoverage_monotone
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
coverings :
  (Pretopology.toPrecoverage (P ⊓ Q).pretopology).coverings =
    (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings
⊢ Eq (α := Pretopology.{v_1, u_1} C) (P ⊓ Q).pretopology (P.pretopology ⊓ Q.pretopology)

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
coverings :
  (P.precoverage ⊓ Q.precoverage).coverings = (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings
⊢ (Pretopology.toPrecoverage (P ⊓ Q).pretopology).coverings =
    (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings

Tactic:
simp only [pretopology_toPrecoverage, precoverage_inf]

Premises used: CategoryTheory.MorphismProperty.pretopology_toPrecoverage, CategoryTheory.MorphismProperty.precoverage_inf
-- Module: Mathlib.CategoryTheory.Sites.MorphismProperty
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
P Q : MorphismProperty.{v_1, u_1} C
inst_2 : P.IsMultiplicative
inst_3 : P.IsStableUnderBaseChange
inst_4 : Q.IsMultiplicative
inst_5 : Q.IsStableUnderBaseChange
⊢ (P.precoverage ⊓ Q.precoverage).coverings = (Pretopology.toPrecoverage (P.pretopology ⊓ Q.pretopology)).coverings

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
i : I
⊢ Eq.{w + 1} (α := (↑(G.obj (Opposite.op (U i))) : Type w)) (1 i) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : ZeroCochain G U
i : I
⊢ γ⁻¹ i = (γ i)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : ZeroCochain G U
i : I
⊢ (γ₁ * γ₂) i = γ₁ i * γ₂ i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ Eq.{w + 1} (α := (↑(G.obj (Opposite.op T)) : Type w)) (ev 1 i j a b) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (γ₁ * γ₂).ev i j a b = γ₁.ev i j a b * γ₂.ev i j a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCochain G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ⁻¹.ev i j a b = (γ.ev i j a b)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x x_1 x_2 : OneCochain G U
ev :
  ∀ (x_3 x_4 : I) (x_5 : C) (x_6 : x_5 ⟶ U x_3) (x_7 : x_5 ⟶ U x_4),
    (x * x_1 * x_2).ev x_3 x_4 x_6 x_7 = (x * (x_1 * x_2)).ev x_3 x_4 x_6 x_7
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x x_1 x_2 : OneCochain G U
x_3 x_4 : I
x_5 : C
x_6 : x_5 ⟶ U x_3
x_7 : x_5 ⟶ U x_4
⊢ (x * x_1 * x_2).ev x_3 x_4 x_6 x_7 = (x * (x_1 * x_2)).ev x_3 x_4 x_6 x_7

Tactic:
apply mul_assoc

Premises used: mul_assoc
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
ev :
  ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2), (1 * x).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5
⊢ 1 * x = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
x_1 x_2 : I
x_3 : C
x_4 : x_3 ⟶ U x_1
x_5 : x_3 ⟶ U x_2
⊢ (1 * x).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5

Tactic:
apply one_mul

Premises used: one_mul
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
ev :
  ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2), (x * 1).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5
⊢ x * 1 = x

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
x_1 x_2 : I
x_3 : C
x_4 : x_3 ⟶ U x_1
x_5 : x_3 ⟶ U x_2
⊢ (x * 1).ev x_1 x_2 x_4 x_5 = x.ev x_1 x_2 x_4 x_5

Tactic:
apply mul_one

Premises used: mul_one
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
ev :
  ∀ (x_1 x_2 : I) (x_3 : C) (x_4 : x_3 ⟶ U x_1) (x_5 : x_3 ⟶ U x_2),
    (x⁻¹ * x).ev x_1 x_2 x_4 x_5 = OneCochain.ev 1 x_1 x_2 x_4 x_5
⊢ x⁻¹ * x = 1

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
x : OneCochain G U
x_1 x_2 : I
x_3 : C
x_4 : x_3 ⟶ U x_1
x_5 : x_3 ⟶ U x_2
⊢ (x⁻¹ * x).ev x_1 x_2 x_4 x_5 = ev 1 x_1 x_2 x_4 x_5

Tactic:
apply inv_mul_cancel

Premises used: inv_mul_cancel
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
⊢ Eq (α := OneCochain G U) (toOneCochain 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i : I
T : C
a : T ⟶ U i
⊢ γ.ev i i a a = 1

Tactic:
simpa using γ.ev_trans i i i a a a

Premises used: CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCocycle G U
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
rw : γ.ev i j a b * γ.ev j i b a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₁ : γ.ev i i a a = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₂ : 1 = (γ.ev j i b a)⁻¹ * γ.ev j i b a
rw₃ rw₄ : Eq.{w + 1} (α := (↑(G.obj (Opposite.op T)) : Type w)) 1 1
⊢ γ.ev i j a b = (γ.ev j i b a)⁻¹

Tactic:
rw [← mul_left_inj (γ.ev j i b a), γ.ev_trans i j i a b a,
    ev_refl, inv_mul_cancel]

Premises used: inv_mul_cancel, CategoryTheory.PresheafOfGroups.OneCocycle.ev_trans, mul_left_inj, CategoryTheory.PresheafOfGroups.OneCocycle.toOneCochain, CategoryTheory.PresheafOfGroups.OneCochain.ev, CategoryTheory.PresheafOfGroups.OneCocycle.ev_refl
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ : OneCochain G U
x x_1 : I
x_2 : C
x_3 : x_2 ⟶ U x
x_4 : x_2 ⟶ U x_1
⊢ HMul.hMul (α := (↑(G.obj (Opposite.op x_2)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map x_3.op) :
            (a : (↑(G.obj (Opposite.op (U x))) : Type w)) → (↑(G.obj (Opposite.op x_2)) : Type w))
          (1 x) :
        (↑(G.obj (Opposite.op x_2)) : Type w))
      (γ.ev x x_1 x_3 x_4) =
    HMul.hMul (β := (↑(G.obj (Opposite.op x_2)) : Type w)) (γ.ev x x_1 x_3 x_4)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map x_4.op) :
            (a : (↑(G.obj (Opposite.op (U x_1))) : Type w)) → (↑(G.obj (Opposite.op x_2)) : Type w))
          (1 x_1) :
        (↑(G.obj (Opposite.op x_2)) : Type w))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
dsimp :
  HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (β i * α i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (γ₁.ev i j a b) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₃.ev i j a b)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          (β j * α j) :
        (↑(G.obj (Opposite.op T)) : Type w))
⊢ HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map a.op) :
            (a : (↑(G.obj (Opposite.op (U i))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          ((β * α) i) :
        (↑(G.obj (Opposite.op T)) : Type w))
      (γ₁.ev i j a b) =
    HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w)) (γ₃.ev i j a b)
      ((ConcreteCategory.hom (FC := fun (x1 x2 : GrpCat.{w}) ↦ (↑x1 : Type w) →* (↑x2 : Type w)) (CC := GrpCat.carrier)
              (G.map b.op) :
            (a : (↑(G.obj (Opposite.op (U j))) : Type w)) → (↑(G.obj (Opposite.op T)) : Type w))
          ((β * α) j) :
        (↑(G.obj (Opposite.op T)) : Type w))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
⊢ γ₂.IsCohomologous γ₁

Tactic:
⟨_, h.symm⟩

Premises used: CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous, Exists.intro, CategoryTheory.PresheafOfGroups.OneCohomologyRelation.symm
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂.toOneCochain α
⊢ γ₂.IsCohomologous γ₁

Tactic:
exact ⟨_, h.symm⟩
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂_1 γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂_1.toOneCochain α
β : ZeroCochain G U
h' : OneCohomologyRelation γ₂_1.toOneCochain γ₂.toOneCochain β
⊢ γ₁.IsCohomologous γ₂

Tactic:
⟨_, h.trans h'⟩

Premises used: CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous, Exists.intro, CategoryTheory.PresheafOfGroups.OneCohomologyRelation.trans
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂_1 γ₂ : OneCocycle G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁.toOneCochain γ₂_1.toOneCochain α
β : ZeroCochain G U
h' : OneCohomologyRelation γ₂_1.toOneCochain γ₂.toOneCochain β
⊢ γ₁.IsCohomologous γ₂

Tactic:
exact ⟨_, h.trans h'⟩
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
⊢ γ₁.class = γ₂.class ↔ γ₁.IsCohomologous γ₂

Tactic:
(equivalence_isCohomologous _ _).quot_mk_eq_iff _ _

Premises used: CategoryTheory.PresheafOfGroups.H1, CategoryTheory.PresheafOfGroups.OneCocycle.class, Equivalence.quot_mk_eq_iff, CategoryTheory.PresheafOfGroups.OneCocycle.equivalence_isCohomologous
-- Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
Goal:
C : Type u
inst : Category.{v, u} C
G : Functor.{v, w, u, w + 1} Cᵒᵖ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCocycle G U
h : γ₁.IsCohomologous γ₂
⊢ γ₁.class = γ₂.class

Tactic:
Quot.sound h

Premises used: Quot.sound, CategoryTheory.PresheafOfGroups.H1, CategoryTheory.PresheafOfGroups.OneCocycle.class
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
⊢ map (Over.forget X) (functorPullback (Over.forget X) R) = R

Tactic:
le_antisymm (map_functorPullback _) fun Z g hg ↦ ?_

Premises used: CategoryTheory.Presieve.map_functorPullback, le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
refine :
  ∀ (Z : C) (g : Z ⟶ Functor.obj (Over.forget X) Y) (hg : R g),
    map (Over.forget X) (functorPullback (Over.forget X) R) g
⊢ map (Over.forget X) (functorPullback (Over.forget X) R) = R

Tactic:
refine le_antisymm (map_functorPullback _) fun Z g hg ↦ ?_

Premises used: CategoryTheory.Presieve.map_functorPullback, le_antisymm
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
hg : R g
g' : Over.mk (g ≫ Y.hom) ⟶ Y := Over.homMk g ⋯
⊢ map (Over.forget X) (functorPullback (Over.forget X) R) g

Tactic:
Presieve.map.of (u := g') hg

Premises used: CategoryTheory.Presieve.map.of
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R : Presieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
hg : R g
g' : Over.mk (g ≫ Y.hom) ⟶ Y := Over.homMk g ⋯
⊢ map (Over.forget X) (functorPullback (Over.forget X) R) g

Tactic:
exact Presieve.map.of (u := g') hg

Premises used: CategoryTheory.Presieve.map.of
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
h :
  ∀ ⦃Z : Over.{v, u} X⦄ (g : Z ⟶ Y),
    arrows
        ((fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y))
          ((fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
            S))
        g ↔
      S.arrows g
⊢ (fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y))
      ((fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y))) S) =
    S

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z.left ⟶ Z_1.left),
      S.arrows g_1 ∧ Over.Hom.left g = h ≫ Over.Hom.left g_1) ↔
    S.arrows g
⊢ arrows
      ((fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y))
        ((fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y))) S))
      g ↔
    S.arrows g

Tactic:
dsimp [Presieve.functorPullback, Presieve.functorPushforward]

Premises used: CategoryTheory.Presieve.functorPullback, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z.left ⟶ Z_1.left),
      S.arrows g_1 ∧ Over.Hom.left g = h ≫ Over.Hom.left g_1) →
    S.arrows g
h₁ :
  S.arrows g →
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z.left ⟶ Z_1.left),
      S.arrows g_1 ∧ Over.Hom.left g = h ≫ Over.Hom.left g_1
⊢ (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z.left ⟶ Z_1.left),
      S.arrows g_1 ∧ Over.Hom.left g = h ≫ Over.Hom.left g_1) ↔
    S.arrows g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
rw : b ≫ W.hom = Over.Hom.left g ≫ Y.hom
rw₁ : b ≫ W.hom = (b ≫ Over.Hom.left a) ≫ Y.hom
rw₂ : b ≫ W.hom = b ≫ Over.Hom.left a ≫ Y.hom
rw₃ rw₄ : b ≫ W.hom = b ≫ W.hom
⊢ b ≫ W.hom = Z.hom

Tactic:
rw [← Over.w g, w, assoc, Over.w a]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Over.w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
h₁ : Over.Hom.left g = Over.Hom.left (c ≫ a)
⊢ g = c ≫ a

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
⊢ Over.Hom.left g = Over.Hom.left (c ≫ a)

Tactic:
w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
⊢ Over.Hom.left g = Over.Hom.left (c ≫ a)

Tactic:
exact w
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
h₁ : S.arrows (c ≫ a)
⊢ S.arrows g

Tactic:
rw [show g = c ≫ a by ext; exact w]
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
⊢ S.arrows (c ≫ a)

Tactic:
S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
W : Over.{v, u} X
a : W ⟶ Y
b : Z.left ⟶ W.left
h : S.arrows a
w : Over.Hom.left g = b ≫ Over.Hom.left a
c : Z ⟶ W := Over.homMk b ⋯
⊢ S.arrows (c ≫ a)

Tactic:
exact S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
h : S.arrows g
⊢ Over.Hom.left g = 𝟙 Z.left ≫ Over.Hom.left g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
Z : Over.{v, u} X
g : Z ⟶ Y
h : S.arrows g
⊢ ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z.left ⟶ Z_1.left),
    S.arrows g_1 ∧ Over.Hom.left g = h ≫ Over.Hom.left g_1

Tactic:
exact ⟨Z, g, 𝟙 _, h, by simp⟩
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
h :
  ∀ ⦃Z : C⦄ (g : Z ⟶ Functor.obj (Over.forget X) Y),
    arrows
        ((fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
          ((fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y)) S))
        g ↔
      S.arrows g
⊢ (fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
      ((fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y)) S) =
    S

Tactic:
ext Z g
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left),
      S.arrows (Over.Hom.left g_1) ∧ g = h ≫ Over.Hom.left g_1) ↔
    S.arrows g
⊢ arrows
      ((fun (S : Sieve Y) ↦ (functorPushforward (Over.forget X) S : Sieve.{v, u} (Functor.obj (Over.forget X) Y)))
        ((fun (S' : Sieve.{v, u} Y.left) ↦ (functorPullback (Over.forget X) S' : Sieve Y)) S))
      g ↔
    S.arrows g

Tactic:
dsimp [Presieve.functorPullback, Presieve.functorPushforward]

Premises used: CategoryTheory.Presieve.functorPullback, CategoryTheory.Presieve.functorPushforward
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : C
g : Z ⟶ Functor.obj (Over.forget X) Y
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left),
      S.arrows (Over.Hom.left g_1) ∧ g = h ≫ Over.Hom.left g_1) →
    S.arrows g
h₁ :
  S.arrows g →
    ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left), S.arrows (Over.Hom.left g_1) ∧ g = h ≫ Over.Hom.left g_1
⊢ (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left),
      S.arrows (Over.Hom.left g_1) ∧ g = h ≫ Over.Hom.left g_1) ↔
    S.arrows g

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : C
W : Over.{v, u} X
a : W ⟶ Y
b : Z ⟶ W.left
h : S.arrows (Over.Hom.left a)
⊢ S.arrows (b ≫ Over.Hom.left a)

Tactic:
S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed
-- Module: Mathlib.CategoryTheory.Sites.Over
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
Z : C
W : Over.{v, u} X
a : W ⟶ Y
b : Z ⟶ W.left
h : S.arrows (Over.Hom.left a)
⊢ S.arrows (b ≫ Over.Hom.left a)

Tactic:
exact S.downward_closed h _

Premises used: CategoryTheory.Sieve.downward_closed