mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ ∀ (x₂ : (fun X ↦ X) (G.obj X)) (x₃ : (fun X ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)),
    (ConcreteCategory.hom ((χ m).app X)) x₂ = (ConcreteCategory.hom ((truth C).app X)) x₃ →
      ∃ x₁,
        (ConcreteCategory.hom (m.app X)) x₁ = x₂ ∧
          (ConcreteCategory.hom (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X)) x₁ = x₃
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).1 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1

pp: case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2

Tactic:
·

Goal state after:
case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).1 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤ →
    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤ →
    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2

Tactic:
·

Goal state after:
case snd
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).2 =
    (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).2
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
this :
  (ConcreteCategory.hom ((Functor.sieves C).map f.op)) ((ConcreteCategory.hom (χ'.app X)) x) =
    (ConcreteCategory.hom (↾fun S ↦ Sieve.pullback f.op.unop S)) ((ConcreteCategory.hom (χ'.app X)) x)
⊢ (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
    (ConcreteCategory.hom (χ'.app (Opposite.op Y))) ((ConcreteCategory.hom (G.map f.op)) x) = ⊤
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ Presieve.FamilyOfElements.Compatible a

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ?refine_1)

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ Presieve.FamilyOfElements.Compatible a
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
⊢ (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) (⋯.amalgamate a ⋯)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case e
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J

pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))

Tactic:
·

Goal state after:
case e
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))

Tactic:
·

Goal state after:
case H
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback ((sheafToPresheaf J (Type (max u v))).map m)
    ((sheafToPresheaf J (Type (max u v))).map ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    ((sheafToPresheaf J (Type (max u v))).map (χ m)) ((sheafToPresheaf J (Type (max u v))).map (truth J))
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback (m.hom ≫ 𝟙 G.obj) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ 𝟙 G.obj ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback (m.hom ≫ 𝟙 G.obj) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ 𝟙 G.obj ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι

Tactic:
·

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ 𝟙 G.obj ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n m : ℤ
h : n + m = 0
⊢ m = -n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: case pos
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n m : ℕ
h : n ≤ m
hP : P.Nonempty
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

pp: case neg
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n m : ℕ
h : n ≤ m
hP : P = ⊥
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
·

Goal state after:
case pos
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n m : ℕ
h : n ≤ m
hP : P.Nonempty
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: case neg
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n m : ℕ
h : n ≤ m
hP : P = ⊥
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m

Tactic:
·

Goal state after:
case neg
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n m : ℕ
h : n ≤ m
hP : P = ⊥
⊢ (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n ≤
    (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter m
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

Goal state before:
pp: case right
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
⊢ Function.Surjective fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h

Tactic:
·

Goal state after:
case right
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
⊢ Function.Surjective fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) iso_hom_app._auto_1
⊢ m + n = 0

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n m : ℤ
hnm : n + m = 0
⊢ m = -n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n m : ℤ
hnm : autoParam (n + m = 0) iso_inv_app._auto_1
⊢ m + n = 0

Tactic:
by lia

Goal state after: