mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀'

Tactic:
·

Goal state after:
case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀'
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
p : ι × ι'
⊢ (d.inj p ≫ e.hom) ≫ t.snd = (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj p ≫ t.snd

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
p : ι × ι'
⊢ (d.inj p ≫ e.hom) ≫ t.snd = (Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj p ≫ t.snd
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
⊢ Nonempty (IsColimit d)

Tactic:
let iso : d ≅ Cofan.mk c'.pt fun p : ι × ι' ↦ (c p.1).inj p.2 ≫ c'.inj _ := by
    refine Cofan.ext e <| fun p ↦ PullbackCone.IsLimit.hom_ext ht ?_ ?_
    · simp [c', c, he₁]
    · simp [c', c, he₂]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
iso : d ≅ Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1 := Cofan.ext e ⋯
⊢ Nonempty (IsColimit d)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
iso : d ≅ Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1 := Cofan.ext e ⋯
⊢ Nonempty (IsColimit c')

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝ : ∀ (i : ι), HasPullback (f i) v
s : (i : ι) → (j : ι') → PullbackCone (f i) (g j)
hs : (i : ι) → (j : ι') → IsLimit (s i j)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun p ↦ (s p.1 p.2).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
he₁ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.fst = (s (i, j).1 (i, j).2).fst ≫ a.inj (i, j).1
he₂ : ∀ (i : ι) (j : ι'), d.inj (i, j) ≫ e.hom ≫ t.snd = (s (i, j).1 (i, j).2).snd ≫ b.inj (i, j).2
c : (i : ι) → Cofan fun j ↦ (s i j).pt :=
  fun i ↦ Cofan.mk (pullback (f i) v) fun j ↦ pullback.lift (s i j).fst ((s i j).snd ≫ b.inj j) ⋯
c' : Cofan fun i ↦ (c i).pt :=
  Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht (pullback.fst (f i) v ≫ a.inj i) (pullback.snd (f i) v) ⋯
iso : d ≅ Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1 := Cofan.ext e ⋯
⊢ Nonempty (IsColimit c')
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback u v ≅ d.pt

Tactic:
exact hc.coconePointUniqueUpToIso hd

Goal state after:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₁ p.1 p.2 ≫ a.inj p.1

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ (Iso.refl b.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₁ p.1 p.2 ≫ a.inj p.1
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ (Iso.refl b.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ (Iso.refl b.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X : C
n : ℕ
hX : ∀ (i : ℕ), n ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0
i : ℕ
hi : n ≤ i
Y : C
this✝ : Subsingleton (Ext X Y i)
this : HasExt C := HasExt.standard C
⊢ Subsingleton (Ext X Y i)

Tactic:
exact Ext.chgUniv.{max u v, w}.symm.subsingleton

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ n ≤ i

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : HasProjectiveDimensionLT X n
k : ℕ
⊢ n ≤ n + k

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : HasProjectiveDimensionLT X n
k : ℕ
⊢ n ≤ k + n

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
Y : C
hi : 1 ≤ 0
e : Ext X Y 0
⊢ e = 0

pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext X Y (i + 1)
⊢ e = 0

Tactic:
·

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
Y : C
hi : 1 ≤ 0
e : Ext X Y 0
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext X Y (i + 1)
⊢ e = 0

Tactic:
·

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
Y : C
i : ℕ
hi : 1 ≤ i + 1
e : Ext X Y (i + 1)
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
hi : n + 1 ≤ 0
Y : C
x₃ : Ext S.X₃ Y 0
⊢ x₃ = 0

pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
⊢ x₃ = 0

Tactic:
·

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
hi : n + 1 ≤ 0
Y : C
x₃ : Ext S.X₃ Y 0
⊢ x₃ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
⊢ x₃ = 0

Tactic:
·

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
⊢ x₃ = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext S.X₁ Y i
⊢ n ≤ i

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₁ : Ext S.X₁ Y i
⊢ n + 1 ≤ i + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₂ : HasProjectiveDimensionLT S.X₂ n
h₃ : HasProjectiveDimensionLT S.X₃ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₂ : Ext S.X₂ Y i
⊢ n ≤ i

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : projectiveDimension X < ↑n
⊢ HasProjectiveDimensionLT X n

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑n

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : projectiveDimension X < ↑n
⊢ HasProjectiveDimensionLT X n
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑n

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X n
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑n
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasProjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑0

pp: case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑(n + 1)

Tactic:
·

Goal state after:
case refine_2.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasProjectiveDimensionLT X 0
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑(n + 1)

Tactic:
·

Goal state after:
case refine_2.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
⊢ ∃ a ∈ {n | ∀ (i : ℕ), n < ↑i → HasProjectiveDimensionLT X i}, a < ↑(n + 1)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case coe.coe
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
d : ℕ
hd : projectiveDimension X = ↑↑d
⊢ ∃ n, HasProjectiveDimensionLE X n

Tactic:
exact ⟨d, by simpa only [← projectiveDimension_le_iff] using! hd.le⟩

Goal state after: