awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
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 γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ 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))
have rw : HMul.hMul (β := (↑(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))
    ((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)) =
  HMul.hMul (β := (↑(G.obj (Opposite.op T)) : Type w))
    (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)))
    ((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: rw [← mul_left_inj (G.map b.op (α j)), mul_assoc, ← h i j a b,
    mul_assoc, Cochain₀.inv_apply, map_inv, inv_mul_cancel_left,
    Cochain₀.inv_apply, map_inv, inv_mul_cancel, mul_one]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
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
⊢ 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))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 (goal)
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
⊢ 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))
have rw : HMul.hMul (α := (↑(G.obj (Opposite.op T)) : Type w)) (β := (↑(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))
      ((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 * α j) :
      (↑(G.obj (Opposite.op T)) : Type w))
Tactic: rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
    h₂₃ i j a b, mul_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
have refine : ∀ (Z : C) (g : Z ⟶ Functor.obj (Over.forget X) Y) (hg : R g), map (Over.forget X) (functorPullback (Over.forget X) R) g
Tactic: refine le_antisymm (map_functorPullback _) fun Z g hg ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve Y
⊢ (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
have 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
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have 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
Tactic: dsimp [Presieve.functorPullback, Presieve.functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ (∃ (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
have 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: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ b ≫ W.hom = Z.hom
have rw : b ≫ W.hom = Over.Hom.left g ≫ Y.hom
Tactic: rw [← Over.w g, w, assoc, Over.w a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ b ≫ W.hom = Z.hom
have rw₁ : b ≫ W.hom = (b ≫ Over.Hom.left a) ≫ Y.hom
Tactic: rw [← Over.w g, w, assoc, Over.w a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ b ≫ W.hom = Z.hom
have rw₂ : b ≫ W.hom = b ≫ Over.Hom.left a ≫ Y.hom
Tactic: rw [← Over.w g, w, assoc, Over.w a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ b ≫ W.hom = Z.hom
have rw₃ : b ≫ W.hom = b ≫ W.hom
Tactic: rw [← Over.w g, w, assoc, Over.w a]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 ⋯
⊢ g = c ≫ a
have h₁ : Over.Hom.left g = Over.Hom.left (c ≫ a)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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 g
have h₁ : S.arrows (c ≫ a)
Tactic: rw [show g = c ≫ a by ext; exact w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
S : Sieve.{v, u} Y.left
⊢ (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
have 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
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ 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
have 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
Tactic: dsimp [Presieve.functorPullback, Presieve.functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Eq (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) ⊤
have h : ∀ ⦃Z : C⦄ (g : Z ⟶ Y.left), arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g ↔ arrows ⊤ g
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g ↔ arrows ⊤ g
have h : arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g
Tactic: simp only [top_apply, iff_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
Z : C
g : Z ⟶ Y.left
⊢ arrows ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) ⊤) g
have h : ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y) (h : Z ⟶ Z_1.left), ⊤ g_1 ∧ g = h ≫ Over.Hom.left g_1
Tactic: dsimp [overEquiv, Presieve.functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
⊢ Eq (α := Sieve Y) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ⊥) ⊥
have rw : Eq (α := Sieve Y)
  ((Equiv.symm
        { toFun := fun (S : Sieve Y) ↦ functorPushforward (Over.forget X) S,
          invFun := fun (S' : Sieve.{v, u} Y.left) ↦ functorPullback (Over.forget X) S', left_inv := sorry,
          right_inv := sorry } :
      (a : Sieve Y.left) → Sieve Y)
    ⊥)
  ⊥
Tactic: rw [overEquiv, Equiv.coe_fn_symm_mk, functorPullback_bot]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
rw :
  Eq (α := Sieve Y)
    ((Equiv.symm
          { toFun := fun (S : Sieve Y) ↦ functorPushforward (Over.forget X) S,
            invFun := fun (S' : Sieve.{v, u} Y.left) ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
            right_inv := ⋯ } :
        (a : Sieve Y.left) → Sieve Y)
      ⊥)
    ⊥
⊢ Eq (α := Sieve Y) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ⊥) ⊥
have rw₁ : Eq (α := Sieve Y) (functorPullback (Over.forget X) ⊥) ⊥
Tactic: rw [overEquiv, Equiv.coe_fn_symm_mk, functorPullback_bot]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
rw :
  Eq (α := Sieve Y)
    ((Equiv.symm
          { toFun := fun (S : Sieve Y) ↦ functorPushforward (Over.forget X) S,
            invFun := fun (S' : Sieve.{v, u} Y.left) ↦ functorPullback (Over.forget X) S', left_inv := ⋯,
            right_inv := ⋯ } :
        (a : Sieve Y.left) → Sieve Y)
      ⊥)
    ⊥
rw₁ : Eq (α := Sieve Y) (functorPullback (Over.forget X) ⊥) ⊥
⊢ Eq (α := Sieve Y) (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ⊥) ⊥
have rw₂ : Eq (α := Sieve Y) ⊥ ⊥
Tactic: rw [overEquiv, Equiv.coe_fn_symm_mk, functorPullback_bot]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
⊢ LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
      ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left) ↔
    R₁ ≤ R₂
have refine : ∀
  (h :
    LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
      ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left)),
  R₁ ≤ R₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y : Over.{v, u} X
R₁ R₂ : Sieve Y
h :
  LE.le (α := Sieve.{v, u} Y.left) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁ : Sieve.{v, u} Y.left)
    ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂ : Sieve.{v, u} Y.left)
⊢ R₁ ≤ R₂
have h₁ : LE.le (α := Sieve Y)
  (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₁) : Sieve Y)
  (((overEquiv Y).symm : (a : Sieve Y.left) → Sieve Y) ((overEquiv Y : (a : Sieve Y) → Sieve Y.left) R₂) : Sieve Y)
Tactic: replace h : (overEquiv Y).symm (R₁.overEquiv Y) ≤ (overEquiv Y).symm (R₂.overEquiv Y) :=
    Sieve.functorPullback_monotone _ _ h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
⊢ (overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S) =
    pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)
have h : ∀ ⦃Z : C⦄ (g : Z ⟶ Y₁.left),
  arrows ((overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S)) g ↔
    (pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)).arrows g
Tactic: ext Z g
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ arrows ((overEquiv Y₁ : (a : Sieve Y₁) → Sieve Y₁.left) (pullback f S)) g ↔
    (pullback (Over.Hom.left f) ((overEquiv Y₂ : (a : Sieve Y₂) → Sieve Y₂.left) S)).arrows g
have h : (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ 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 g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
Tactic: dsimp [overEquiv, Presieve.functorPushforward]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
⊢ (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ 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 g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
have h : (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ 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 g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
h :
  (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ 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 g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
⊢ (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ 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 g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1
have h₁ : (∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₂) (h : Z ⟶ Z_1.left),
    S.arrows g_1 ∧ g ≫ Over.Hom.left f = h ≫ Over.Hom.left g_1) →
  ∃ (Z_1 : Over.{v, u} X) (g_1 : Z_1 ⟶ Y₁) (h : Z ⟶ Z_1.left), S.arrows (g_1 ≫ f) ∧ g = h ≫ Over.Hom.left g_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = T.hom
have dsimp : g ≫ Y₁.hom = b ≫ W.hom
Tactic: dsimp [T]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
⊢ g ≫ Y₁.hom = b ≫ W.hom
have rw : g ≫ Y₁.hom = b ≫ Over.Hom.left a ≫ Y₂.hom
Tactic: rw [← Over.w a, ← reassoc_of% w, Over.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
rw : g ≫ Y₁.hom = b ≫ Over.Hom.left a ≫ Y₂.hom
⊢ g ≫ Y₁.hom = b ≫ W.hom
have rw₁ : g ≫ Y₁.hom = g ≫ Over.Hom.left f ≫ Y₂.hom
Tactic: rw [← Over.w a, ← reassoc_of% w, Over.w f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Sites.Over (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : C
Y₁ Y₂ : Over.{v, u} X
f : Y₁ ⟶ Y₂
S : Sieve Y₂
Z : C
g : Z ⟶ Y₁.left
W : Over.{v, u} X
a : W ⟶ Y₂
b : Z ⟶ W.left
h : S.arrows a
w : g ≫ Over.Hom.left f = b ≫ Over.Hom.left a
T : Over.{v, u} X := Over.mk (b ≫ W.hom)
rw : g ≫ Y₁.hom = b ≫ Over.Hom.left a ≫ Y₂.hom
rw₁ : g ≫ Y₁.hom = g ≫ Over.Hom.left f ≫ Y₂.hom
⊢ g ≫ Y₁.hom = b ≫ W.hom
have rw₂ : g ≫ Y₁.hom = g ≫ Y₁.hom
Tactic: rw [← Over.w a, ← reassoc_of% w, Over.w f]