mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha)) ≫
      G₀.obj.map p₁.op =
    (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hb)) ≫
      G₀.obj.map p₂.op

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha) ≫ G₀.obj.map p₁.op =
    (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hb)) ≫
      G₀.obj.map p₂.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha) ≫ G₀.obj.map p₁.op =
    (presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫ IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hb)) ≫
      G₀.obj.map p₂.op

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha) ≫ G₀.obj.map p₁.op =
    presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i hb) ≫
      IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h hb) ≫ G₀.obj.map p₂.op
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ (F.map p₁ ≫ Sieve.ofArrows.h ha) ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map (p₁ ≫ a)

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₁ ≫ Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map (p₁ ≫ a)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ (F.map p₂ ≫ Sieve.ofArrows.h hb) ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map (p₁ ≫ a)

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ W₀ : C₀
a : W₀ ⟶ X₀
ha : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows a
T₀ : C₀
b : T₀ ⟶ X₀
hb : Presieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀.arrows b
U₀ : C₀
p₁ : U₀ ⟶ W₀
p₂ : U₀ ⟶ T₀
fac : p₁ ≫ a = p₂ ≫ b
ha' : Sieve.ofArrows.h ha ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i ha) = F.map a
hb' : Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map b
⊢ F.map p₂ ≫ Sieve.ofArrows.h hb ≫ (data (F.obj X₀)).f (Sieve.ofArrows.i hb) = F.map (p₁ ≫ a)
Module: Mathlib.AlgebraicGeometry.Sites.ConstantSheaf

Goal state before:
pp: A : Type v
inst✝² : TopologicalSpace A
inst✝¹ : AddCommGroup A
inst✝ : IsTopologicalAddGroup A
⊢ Presheaf.IsSheaf Scheme.fpqcTopology (continuousMapPresheafAb A ⋙ forget Ab)

Tactic:
exact isSheaf_fpqcTopology_continuousMapPresheaf _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ (presheafObjObjIso.hom data G₀ X₀ ≫ presheafObjObjIso.inv data G₀ X₀) ≫
      presheafObjπ data G₀ (unop (op (F.obj X₀))) i =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
i : (data (unop (op (F.obj X₀)))).I₀
⊢ presheafObjObjIso.hom data G₀ X₀ ≫ presheafObjObjIso.inv data G₀ X₀ ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i =
    𝟙 ((presheaf data G₀).obj (op (F.obj X₀))) ≫ presheafObjπ data G₀ (unop (op (F.obj X₀))) i
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ (presheafMap data G₀ ((data X).f i) ≫ (presheafObjObjIso data G₀ ((data X).X i)).hom) ≫
      (presheafObjObjIso data G₀ ((data X).X i)).inv =
    presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫
      (presheafObjObjIso data G₀ ((data X).X i)).hom ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv =
    presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j =
    (presheafObjπ data G₀ X i ≫ (presheafObjObjIso data G₀ ((data X).X i)).inv) ≫
      presheafObjπ data G₀ (F.obj ((data X).X i)) j

Tactic:
assoc,

Goal state after:
C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X : C
i : (data X).I₀
j : (data (F.obj ((data X).X i))).I₀
⊢ presheafMap data G₀ ((data X).f i) ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j =
    presheafObjπ data G₀ X i ≫
      (presheafObjObjIso data G₀ ((data X).X i)).inv ≫ presheafObjπ data G₀ (F.obj ((data X).X i)) j
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ (π ≫ x₄) ≫ k = 0

Tactic:
assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
⊢ π ≫ x₄ ≫ k = 0
Module: Mathlib.CategoryTheory.Abelian.CommSq

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + (h₂.lift (-x₂) x₃ fac₃ ≫ t) ≫ r

Tactic:
assoc,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X₁ X₂ X₃ X₄ : C
t : X₁ ⟶ X₂
l : X₁ ⟶ X₃
r : X₂ ⟶ X₄
b : X₃ ⟶ X₄
h₁ : IsPushout t l r b
X₅ : C
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
k : X₄ ⟶ X₅
fac₁ : r ≫ k = r'
fac₂ : b ≫ k = b'
inst✝ : Mono r'
T₀ : C
x₄ : T₀ ⟶ X₄
hx₄ : x₄ ≫ k = 0
T₁ : C
π : T₁ ⟶ T₀
w✝ : Epi π
x₂ : T₁ ⟶ X₂
x₃ : T₁ ⟶ X₃
eq : π ≫ x₄ = x₂ ≫ r + x₃ ≫ b
fac₃ : (-x₂) ≫ r' = x₃ ≫ b'
⊢ x₂ ≫ r + x₃ ≫ b = x₂ ≫ r + h₂.lift (-x₂) x₃ fac₃ ≫ t ≫ r
Module: Mathlib.CategoryTheory.Sites.Subcanonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (F.obj.map g.op)) (J.uliftYonedaEquiv f) =
    J.uliftYonedaEquiv ((uliftYoneda.{v', v, u} J).map g ≫ f)

Tactic:
change (f.hom.app (op X) ≫ F.obj.map g.op) ⟨𝟙 X⟩ = f.hom.app (op Y) ⟨𝟙 Y ≫ g⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type (max v v'))
f : (uliftYoneda.{v', v, u} J).obj X ⟶ F
g : Y ⟶ X
⊢ (ConcreteCategory.hom (f.hom.app (op X) ≫ F.obj.map g.op)) { down := 𝟙 X } =
    (ConcreteCategory.hom (f.hom.app (op Y))) { down := 𝟙 Y ≫ g }
Module: Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
m : Y₁ ⟶ Y₂
g₁ : Y₁ ⟶ X₁
g₂ : Y₂ ⟶ X₂
h : coproducts.{w, v, u} (ofHoms g) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells g f)

Tactic:
rw [coproducts_iff] at h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
α : Type t
A B : α → C
g : (a : α) → A a ⟶ B a
X₁ X₂ : C
f : X₁ ⟶ X₂
Y₁ Y₂ : C
m : Y₁ ⟶ Y₂
g₁ : Y₁ ⟶ X₁
g₂ : Y₂ ⟶ X₂
h : ∃ J, (ofHoms g).colimitsOfShape (Discrete J) m
sq : IsPushout g₁ m f g₂
⊢ Nonempty (AttachCells g f)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ arrowMap iter.F i (Order.succ i) ⋯ ⋯ = Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩)

Tactic:
← arrowSucc_def _ _ hi,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ arrowSucc iter.F i hi = Φ.toSuccArrow (iter.F.obj ⟨i, ⋯⟩)
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j : J
iter : Φ.Iteration j
i : J
hi : i < j
⊢ Φ.prop (iter.F.map (homOfLE ⋯))

Tactic:
rw [prop_iff, ← arrowMap, ← arrowSucc_def _ _ hi, iter.arrowSucc_eq]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    ((objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv) ≫
      (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv

Tactic:
assoc,

Goal state after:
case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫
      (F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv) ≫ (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫
      (F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv) ≫ (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv

Tactic:
assoc,

Goal state after:
case inl.inl.inl
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₃ : i₃ ≤ j
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
hi₃' : i₃ < j
⊢ (objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (objIso c i₃ hi₃').inv =
    (objIso c i₁ ⋯).hom ≫
      F.map (homOfLE hi) ≫ (objIso c i₂ ⋯).inv ≫ (objIso c i₂ ⋯).hom ≫ F.map (homOfLE hi') ≫ (objIso c i₃ hi₃').inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
hj₁ : ¬IsMax j
iter₁ iter₂ : Φ.Iteration (Order.succ j)
h₀ : j ≤ Order.succ j
hj₂ : restrictionLE iter₁.F h₀ = restrictionLE iter₂.F h₀
hsucc : iter₁.F.obj ⟨j, ⋯⟩ = iter₂.F.obj ⟨j, ⋯⟩
this : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₂ : k₂ ≤ Order.succ j), k₂ ≤ j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₂
h₂ : Order.succ j ≤ Order.succ j
h : ¬Order.succ j ≤ j
h₁₂ : Order.succ j ≤ Order.succ j
h' : j < Order.succ j
⊢ MapEq iter₁.F iter₂.F (Order.succ j) (Order.succ j) h₁₂ h₂

Tactic:
rw [MapEq, arrowMap_refl, arrowMap_refl,
              obj_succ _ _ h', obj_succ _ _ h', hsucc]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Construction

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S✝ X✝ : C
πX✝ : X✝ ⟶ S✝
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX✝)) C
inst✝² : HasPushout (functorObjTop f πX✝) (functorObjLeft f πX✝)
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
this : Arrow.Hom.left τ ≫ πY = πX ≫ Arrow.Hom.right τ
⊢ (t ≫ Arrow.Hom.left τ) ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S✝ X✝ : C
πX✝ : X✝ ⟶ S✝
inst✝³ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX✝)) C
inst✝² : HasPushout (functorObjTop f πX✝) (functorObjLeft f πX✝)
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
b' : B i ⟶ T
hb' : b ≫ Arrow.Hom.right τ = b'
t' : A i ⟶ Y
ht' : t ≫ Arrow.Hom.left τ = t'
this : Arrow.Hom.left τ ≫ πY = πX ≫ Arrow.Hom.right τ
⊢ t ≫ Arrow.Hom.left τ ≫ πY = t ≫ πX ≫ Arrow.Hom.right τ
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    ((objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫
      (objIso c i₂ hi₂₃).hom ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv

Tactic:
assoc,

Goal state after:
case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    (objIso c i₁ ⋯).hom ≫
      (F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫ (objIso c i₂ hi₂₃).hom ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone

Goal state before:
pp: case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    (objIso c i₁ ⋯).hom ≫
      (F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv) ≫ (objIso c i₂ hi₂₃).hom ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv

Tactic:
assoc,

Goal state after:
case inl.inl.inr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : Type u
inst✝ : LinearOrder J
i₁ i₂ i₃ : J
hi : i₁ ≤ i₂
hi' : i₂ ≤ i₃
hi₁₂ : i₁ < i₂
hi₂₃ : i₂ < i₃
F : ↑(Set.Iio i₃) ⥤ C
c : Cocone F
hi₃ : i₃ ≤ i₃
⊢ (objIso c i₁ ⋯).hom ≫ c.ι.app ⟨i₁, ⋯⟩ ≫ (objIsoPt c).inv =
    (objIso c i₁ ⋯).hom ≫
      F.map (homOfLE hi) ≫ (objIso c i₂ hi₂₃).inv ≫ (objIso c i₂ hi₂₃).hom ≫ c.ι.app ⟨i₂, hi₂₃⟩ ≫ (objIsoPt c).inv
Module: Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    ((objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, ⋯⟩).inv) ≫
      (objIso F X ⟨i₂, ⋯⟩).hom ≫ F.map (homOfLE h₂₃) ≫ (objIso F X ⟨i₃, h₁⟩).inv

Tactic:
assoc,

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ i₃ : J
h₁₂ : i₁ ≤ i₂
h₂₃ : i₂ ≤ i₃
h : i₃ ≤ Order.succ j
h₁ : i₃ ≤ j
⊢ (objIso F X ⟨i₁, ⋯⟩).hom ≫ F.map (homOfLE ⋯) ≫ (objIso F X ⟨i₃, h₁⟩).inv =
    (objIso F X ⟨i₁, ⋯⟩).hom ≫
      (F.map (homOfLE h₁₂) ≫ (objIso F X ⟨i₂, ⋯⟩).inv) ≫
        (objIso F X ⟨i₂, ⋯⟩).hom ≫ F.map (homOfLE h₂₃) ≫ (objIso F X ⟨i₃, h₁⟩).inv