mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ v ≫ (Iso.refl S).hom = (Iso.refl B).hom ≫ v

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ u ≫ (Iso.refl S).hom = (Iso.refl a.pt).hom ≫ u

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
⊢ IsPullback (Cofan.IsColimit.desc hd q₁) (Cofan.IsColimit.desc hd fun x ↦ q₂ x ≫ a.inj x) v u

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
i : ι
⊢ ((s i).fst ≫ a.inj i) ≫ u = (s i).snd ≫ v

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.fst =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).inj p ≫ t.fst

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
p : ι
⊢ (d.inj p ≫ e.hom) ≫ t.snd =
    (Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯).inj p ≫ t.snd

Tactic:
by

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

Goal state before:
pp: 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
Y : C
r₀ r₀' : ↑(R₀.obj (Opposite.op Y))
m₀ m₀' : ↑(M₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀'
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀'
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀ • m₀) = (ConcreteCategory.hom (φ.app (Opposite.op Y))) (r₀' • m₀')

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
iso : d ≅ Cofan.mk t.pt fun i ↦ PullbackCone.IsLimit.lift ht ((s i).fst ≫ a.inj i) (s i).snd ⋯ := Cofan.ext e ⋯
j : Discrete ι
⊢ PullbackCone.IsLimit.lift ht ((s j.as).fst ≫ a.inj j.as) (s j.as).snd ⋯ ≫ t.fst = (s j.as).fst ≫ a.inj j.as

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
s : (i : ι) → PullbackCone (f i) v
hs : (i : ι) → IsLimit (s i)
t : PullbackCone u v
ht : IsLimit t
d : Cofan fun i ↦ (s i).pt
e : d.pt ≅ t.pt
hu : ∀ (i : ι), a.inj i ≫ u = f i
he₁ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.fst = (s i).fst ≫ a.inj i
he₂ : ∀ (i : ι), d.inj i ≫ e.hom ≫ t.snd = (s i).snd
⊢ Nonempty (IsColimit d)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
i : ι
⊢ (q₁ i ≫ a.inj i) ≫ u = q₂ i ≫ v

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ u ≫ (Iso.refl S).hom = (Iso.refl a.pt).hom ≫ u

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ v ≫ (Iso.refl S).hom = (Iso.refl B).hom ≫ v

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
⊢ IsPullback (Cofan.IsColimit.desc hd fun x ↦ q₁ x ≫ a.inj x) (Cofan.IsColimit.desc hd q₂) u v

Tactic:
by

Goal state after:
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
i : ι
j : ι'
⊢ (s i j).fst ≫ f i = ((s i j).snd ≫ b.inj j) ≫ v

Tactic:
by

Goal state after:
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) ⋯
i : ι
⊢ (pullback.fst (f i) v ≫ a.inj i) ≫ u = pullback.snd (f i) v ≫ v

Tactic:
by

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

Goal state before:
pp: 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)) (r₀ • m₀)) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) (r₀' • m₀')

Tactic:
by

Goal state after:
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) ⋯
⊢ d ≅ Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1

Tactic:
by

Goal state after:
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
⊢ Nonempty (IsColimit d)

Tactic:
by

Goal state after:
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
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
p : ι × ι'
⊢ (q₁ p.1 p.2 ≫ a.inj p.1) ≫ u = (q₂ p.1 p.2 ≫ b.inj p.2) ≫ v

Tactic:
by

Goal state after:
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
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
⊢ u ≫ (Iso.refl S).hom = (Iso.refl a.pt).hom ≫ u

Tactic:
by

Goal state after:
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
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
⊢ v ≫ (Iso.refl S).hom = (Iso.refl b.pt).hom ≫ v

Tactic:
by

Goal state after:
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
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
⊢ IsPullback (Cofan.IsColimit.desc hd fun p ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N₁ N₂ : M.Submodule
h : ∀ (X : Cᵒᵖ), N₁.obj X = N₂.obj X
⊢ N₁ = N₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N : M.Submodule
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↥(N.obj X)
⊢ ↑((ConcreteCategory.hom (N.toPresheafOfModules.map f)) m) = (ConcreteCategory.hom (M.map f)) ↑m

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N : M.Submodule
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(N.toPresheafOfModules.obj X)),
    (ConcreteCategory.hom
          ({ app := fun X ↦ AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom, naturality := ⋯ }.app X))
        (r • m) =
      r •
        (ConcreteCategory.hom
            ({ app := fun X ↦ AddCommGrpCat.ofHom (N.obj X).subtype.toAddMonoidHom, naturality := ⋯ }.app X))
          m

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N N₁ N₂ : M.Submodule
hle : N₁ ≤ N₂
⊢ ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(N₁.toPresheafOfModules.obj X)),
    (ConcreteCategory.hom
          ({ app := fun X ↦ AddCommGrpCat.ofHom (Submodule.inclusion ⋯).toAddMonoidHom, naturality := ⋯ }.app X))
        (r • m) =
      r •
        (ConcreteCategory.hom
            ({ app := fun X ↦ AddCommGrpCat.ofHom (Submodule.inclusion ⋯).toAddMonoidHom, naturality := ⋯ }.app X))
          m

Tactic:
by

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

Goal state before:
pp: 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))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
a₀ : ↑(R₀.obj (Opposite.op Z)) := (ConcreteCategory.hom (R₀.map g₁.op)) a₁
b₀ : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R₀.map g₁.op))).obj (M₀.obj (Opposite.op Z))) :=
  (ConcreteCategory.hom (M₀.map g₁.op)) b₁
ha₁ : (ConcreteCategory.hom (α.app (Opposite.op Y₁))) a₁ = (ConcreteCategory.hom (R.map f₁.op)) r
ha₂ : (ConcreteCategory.hom (α.app (Opposite.op Y₂))) a₂ = (ConcreteCategory.hom (R.map f₂.op)) r
hb₁ : (ConcreteCategory.hom (φ.app (Opposite.op Y₁))) b₁ = (ConcreteCategory.hom (A.map f₁.op)) m
hb₂ : (ConcreteCategory.hom (φ.app (Opposite.op Y₂))) b₂ = (ConcreteCategory.hom (A.map f₂.op)) m
⊢ (ConcreteCategory.hom (α.app (Opposite.op Z))) a₀ = (ConcreteCategory.hom (R.map (f₁.op ≫ g₁.op))) r

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
N : M.Submodule
s : Set M.Submodule
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
⊢ ⨅ N ∈ s, N.obj X✝ ≤ Submodule.comap (M.restrictₛₗ f) (⨅ N ∈ s, N.obj Y✝)

Tactic:
by

Goal state after:
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 : HasProjectiveDimensionLT X n
i : ℕ
hi : n ≤ i
Y : C
⊢ Subsingleton (Ext X Y i)

Tactic:
by

Goal state after:
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
e₁ e₂ : Ext X Y i
⊢ e₁ = e₂

Tactic:
by

Goal state after:
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
⊢ Subsingleton (Ext X Y i)

Tactic:
by

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
hX : IsZero X
⊢ HasProjectiveDimensionLT X 0

Tactic:
by

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
inst✝ : HasProjectiveDimensionLT X 0
this : HasExt C := HasExt.standard C
⊢ 0 ≤ 0

Tactic:
by

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
inst✝ : HasProjectiveDimensionLT X 0
⊢ IsZero X

Tactic:
by

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

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
⊢ HasProjectiveDimensionLT X m

Tactic:
by

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

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

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:
· simp at hi

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: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
⊢ HasProjectiveDimensionLT X 1

Tactic:
by

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
inst✝ : HasExt C
h : Projective X
⊢ 1 ≤ 1

Tactic:
by

Goal state after: