mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
ι : Sort u_1
S : ι → Subfunctor F
U : C
⊢ (⨆ i, S i).obj U = ⋃ i, (S i).obj U

Tactic:
by
  simp [iSup, sSup_obj]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (m₁ m₂ : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) (m₁ + m₂) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n =
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n +
        (ConcreteCategory.hom (M₁.map f)) m₂ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n

Tactic:
intro m₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m₁ : ↑(M₁.obj X)
⊢ ∀ (m₂ : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) (m₁ + m₂) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n =
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n +
        (ConcreteCategory.hom (M₁.map f)) m₂ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (m : ↑(M₁.obj X)) (n₁ n₂ : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (n₁ + n₂) =
      (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₁ +
        (ConcreteCategory.hom (M₁.map f)) m ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₂

Tactic:
intro m₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m₁ : ↑(M₁.obj X)
⊢ ∀ (n₁ n₂ : ↑(M₂.obj X)),
    (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (n₁ + n₂) =
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₁ +
        (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) n₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ ∀ (m : ↑(M₁.obj X)) (n : ↑(M₂.obj X)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (𝟙 X))) (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n) =
      (ModuleCat.Hom.hom
          ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 X))) ⋯).inv.app
            (M₁.obj X ⊗ M₂.obj X)))
        (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n)

Tactic:
intro m₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
m₁ : ↑(M₁.obj X)
⊢ ∀ (n : ↑(M₂.obj X)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (𝟙 X))) (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n) =
      (ModuleCat.Hom.hom
          ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (𝟙 X))) ⋯).inv.app
            (M₁.obj X ⊗ M₂.obj X)))
        (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X)] n)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑(M₁.obj X✝)) (n : ↑(M₂.obj X✝)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (f ≫ g))) (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n) =
      (ModuleCat.Hom.hom
          (tensorObjMap M₁ M₂ f ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
                (tensorObjMap M₁ M₂ g) ≫
              (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map g))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (f ≫ g))) ⋯).inv.app
                (M₁.obj Z✝ ⊗ M₂.obj Z✝)))
        (m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n)

Tactic:
intro m₁

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ Y✝ Z✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m₁ : ↑(M₁.obj X✝)
⊢ ∀ (n : ↑(M₂.obj X✝)),
    (ModuleCat.Hom.hom (tensorObjMap M₁ M₂ (f ≫ g))) (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n) =
      (ModuleCat.Hom.hom
          (tensorObjMap M₁ M₂ f ≫
            (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))).map
                (tensorObjMap M₁ M₂ g) ≫
              (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map f))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map g))
                      (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map (f ≫ g))) ⋯).inv.app
                (M₁.obj Z✝ ⊗ M₂.obj Z✝)))
        (m₁ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj X✝)] n)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ M₁ ◁ 𝟙 M₂ = 𝟙 (M₁ ⊗ M₂)

Tactic:
ext1 X

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (M₁ ◁ 𝟙 M₂).app X = (𝟙 (M₁ ⊗ M₂)).app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ 𝟙 x✝¹ ▷ x✝ = 𝟙 (x✝¹ ⊗ x✝)

Tactic:
ext1 X

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (𝟙 x✝¹ ▷ x✝).app X = (𝟙 (x✝¹ ⊗ x✝)).app X
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
⊢ ∀ ⦃f_1 : Z ⟶ Y⦄, (Sieve.pullback f S).arrows f_1 → Sieve.pullback f_1 (Sieve.pullback f R) ∈ J Z

Tactic:
g

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S R : Sieve X
h : J.Covers S f
k : ∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f S).arrows g → Sieve.pullback g (Sieve.pullback f R) ∈ J Z
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : ι'
u : T ⟶ X (incl (Sum.inl i))
hu : Presieve.ofArrows (Y (incl (Sum.inl i))) (g (incl (Sum.inl i))) u
⊢ Presieve.ofArrows (fun j ↦ Y (incl (Sum.inl i)) (fibincl (Sum.inl i) j))
    (fun j ↦ g (incl (Sum.inl i)) (fibincl (Sum.inl i) j)) u

Tactic:
| =>

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : ι'
u : T ⟶ X (incl (Sum.inl i))
hu : Presieve.ofArrows (Y (incl (Sum.inl i))) (g (incl (Sum.inl i))) u
⊢ Presieve.ofArrows (fun j ↦ Y (incl (Sum.inl i)) (fibincl (Sum.inl i) j))
    (fun j ↦ g (incl (Sum.inl i)) (fibincl (Sum.inl i) j)) u
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : α
u : T ⟶ X (incl (Sum.inr i))
hu : Presieve.ofArrows (Y (incl (Sum.inr i))) (g (incl (Sum.inr i))) u
⊢ Presieve.ofArrows (fun j ↦ Y (incl (Sum.inr i)) (fibincl (Sum.inr i) j))
    (fun j ↦ g (incl (Sum.inr i)) (fibincl (Sum.inr i) j)) u

Tactic:
| =>

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderComposition
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.coverings S
σ : ι → Type w'
Y : (i : ι) → σ i → C
g : (i : ι) → (j : σ i) → Y i j ⟶ X i
hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)
ι' : Type (max u v) := ↑(Presieve.ofArrows X f).uncurry
σ' : ι' → Type (max u v) :=
  fun i ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯)) (g (Presieve.ofArrows.idx ⋯))).uncurry
α : Type (max u v) := ↑(Presieve.ofArrows (fun p ↦ Y p.fst p.snd) fun x ↦ g x.fst x.snd ≫ f x.fst).uncurry
τ' : α → Type (max u v) :=
  fun a ↦ ↑(Presieve.ofArrows (Y (Presieve.ofArrows.idx ⋯).fst) (g (Presieve.ofArrows.idx ⋯).fst)).uncurry
fib : ι' ⊕ α → Type (max u v) := fun i ↦ Sum.elim (fun i ↦ σ' i) (fun i ↦ Unit ⊕ τ' i) i
incl : ι' ⊕ α → ι := fun p ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ (Presieve.ofArrows.idx ⋯).fst) p
fibincl : (i : ι' ⊕ α) → fib i → σ (incl i) :=
  fun i j ↦
    match i, j with
    | Sum.inl i, j => Presieve.ofArrows.idx ⋯
    | Sum.inr i, j => Sum.elim (fun x ↦ (Presieve.ofArrows.idx ⋯).snd) (fun i_1 ↦ Presieve.ofArrows.idx ⋯) j
i✝ : ι' ⊕ α
T : C
i : α
u : T ⟶ X (incl (Sum.inr i))
hu : Presieve.ofArrows (Y (incl (Sum.inr i))) (g (incl (Sum.inr i))) u
⊢ Presieve.ofArrows (fun j ↦ Y (incl (Sum.inr i)) (fibincl (Sum.inr i) j))
    (fun j ↦ g (incl (Sum.inr i)) (fibincl (Sum.inr i) j)) u
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = 𝟙 (F.obj Z) ≫ f
⊢ map F R f

Tactic:
Category.id_comp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve X
Z : C
g : Z ⟶ X
hg : R g
f : F.obj Z ⟶ F.obj X
x✝ : ∃ Z_1, ∃ (h : F.obj Z_1 = F.obj Z), ∃ g, R g ∧ F.map g = eqToHom h ≫ f
heq : F.map g = f
⊢ map F R f
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
⊢ ∀ (g : Z ⟶ Y) (hf : S.arrows f), x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)

Tactic:
g

Goal state after:
case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ∀ (hf : S.arrows f), x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Y Z : C
⊢ ∀ (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (secondMap P S)) x)

Tactic:
g

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : Presieve.FamilyOfElements.SieveCompatible ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x)
Y Z : C
g : Z ⟶ Y
⊢ ∀ (f : Y ⟶ X) (hf : S.arrows f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (firstMap P S)) x) =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
        ((ConcreteCategory.hom (secondMap P S)) x)
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.Compatible
⊢ (FamilyOfElements.pullback f x).Compatible

Tactic:
simp only [compatible_iff_sieveCompatible] at h ⊢
  intro W Z f₁ f₂ hf
  unfold FamilyOfElements.pullback
  rw [← h (f₁ ≫ f) f₂ hf]
  congr 1
  simp only [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
⊢ ∀ (f_1 : W ⟶ X), (ofArrows Y f).arrows f_1 → (ofObjects Y X).arrows f_1

Tactic:
g

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
X : C
f : (i : I) → Y i ⟶ X
W : C
g : W ⟶ X
⊢ (ofArrows Y f).arrows g → (ofObjects Y X).arrows g
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y Z : C
f : Y ⟶ X
⊢ ∀ (g : Z ⟶ Y) (hf : S.arrows f),
    (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
      (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)

Tactic:
g

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : FirstObj P S.arrows
t : (ConcreteCategory.hom (firstMap P S)) x = (ConcreteCategory.hom (secondMap P S)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
⊢ ∀ (hf : S.arrows f),
    (ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x (g ≫ f) ⋯ =
      (ConcreteCategory.hom (P.map g.op)) ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom) x f hf)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : Y ⟶ X
S✝ R : Sieve X
h : Y ⟶ X
S : Sieve X
Y✝ Z✝ : C
f✝ : Y✝ ⟶ Y
g : S.arrows (f✝ ≫ h)
⊢ ∀ (g : Z✝ ⟶ Y✝), S.arrows ((g ≫ f✝) ≫ h)

Tactic:
by simp [g]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
⊢ ∀ (f_1 : Z ⟶ X), S.arrows f_1 → (pushforward f (pullback f S)).arrows f_1

Tactic:
g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
g : Z ⟶ X
⊢ S.arrows g → (pushforward f (pullback f S)).arrows g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
⊢ ∀ (f_1 : Y ⟶ X) (h : R f_1),
    (ConcreteCategory.hom (Q.map f_1.op)) ((ConcreteCategory.hom (f.app (op X))) t) = x.map f f_1 h

Tactic:
g

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
f : P ⟶ Q
h : x.IsAmalgamation t
Y : C
g : Y ⟶ X
⊢ ∀ (h : R g), (ConcreteCategory.hom (Q.map g.op)) ((ConcreteCategory.hom (f.app (op X))) t) = x.map f g h
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      (ConcreteCategory.hom (firstMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) =
          (ConcreteCategory.hom (secondMap P S)) ((firstObjEqFamily P S.arrows).toEquiv.symm a) →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a

Tactic:
simp_rw [← compatible_iff]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
⊢ Presieve.IsSheafFor P S.arrows ↔
    ∀ (a : Presieve.FamilyOfElements P S.arrows),
      ((ConcreteCategory.hom (firstObjEqFamily P S.arrows).hom)
            ((firstObjEqFamily P S.arrows).toEquiv.symm a)).Compatible →
        ∃! x, (ConcreteCategory.hom (forkMap P S.arrows)) x = (firstObjEqFamily P S.arrows).toEquiv.symm a
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
⊢ ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPullback F R.arrows (g ≫ f)

Tactic:
g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve (F.obj X)
Y✝ Z✝ : C
f : Y✝ ⟶ X
hf : Presieve.functorPullback F R.arrows f
g : Z✝ ⟶ Y✝
⊢ Presieve.functorPullback F R.arrows (g ≫ f)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve (F.obj X)
Z : C
⊢ Presieve.functorPullback F R ≤ (functorPullback F (generate R)).arrows

Tactic:
g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Presieve (F.obj X)
Z : C
g : Z ⟶ X
⊢ Presieve.functorPullback F R g ≤ (functorPullback F (generate R)).arrows g
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
⊢ (ConcreteCategory.hom (P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝

Tactic:
have := Presieve.HasPairwisePullbacks.has_pullbacks fg.1.2.2 fg.2.2.2

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
fg : ((Y : C) × { f // R f }) × (Z : C) × { g // R g }
x✝ : P.obj (op X)
this : HasPullback ↑fg.1.snd ↑fg.2.snd
⊢ (ConcreteCategory.hom (P.map (↑fg.1.snd).op ≫ P.map (pullback.fst ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝ =
    (ConcreteCategory.hom (P.map (↑fg.2.snd).op ≫ P.map (pullback.snd ↑fg.1.snd ↑fg.2.snd).op)).toFun x✝
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ Z✝ : D
f : Y✝ ⟶ F.obj X
h : Presieve.functorPushforward F R.arrows f
⊢ ∀ (g : Z✝ ⟶ Y✝), Presieve.functorPushforward F R.arrows (g ≫ f)

Tactic:
g

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R✝ : Sieve X
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve X
Y✝ Z✝ : D
f : Y✝ ⟶ F.obj X
h : Presieve.functorPushforward F R.arrows f
g : Z✝ ⟶ Y✝
⊢ Presieve.functorPushforward F R.arrows (g ≫ f)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y Z : C
f : Y ⟶ X
⊢ ∀ ⦃f₂ : Z ⟶ X⦄ (h₁ : R f) (h₂ : R f₂),
    (ConcreteCategory.hom (P.map (pullback.fst f f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f f₂).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f₂ h₂)

Tactic:
g

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : FirstObj P R
t : (ConcreteCategory.hom (firstMap P R)) x = (ConcreteCategory.hom (secondMap P R)) x
Y Z : C
f : Y ⟶ X
g : Z ⟶ X
⊢ ∀ (h₁ : R f) (h₂ : R g),
    (ConcreteCategory.hom (P.map (pullback.fst f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x f h₁) =
      (ConcreteCategory.hom (P.map (pullback.snd f g).op)) ((ConcreteCategory.hom (firstObjEqFamily P R).hom) x g h₂)