mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subobject.NoetherianObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictMono f
⊢ IsNoetherianObject X

Tactic:
dsimp only [IsNoetherianObject]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
h : ∀ (f : ℕ → Subobject X), ¬StrictMono f
⊢ isNoetherianObject.Is X
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝³ : Preadditive C
inst✝² : HasFiniteBiproducts C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ o.matrixDecomposition.toFun (w + z) = o.matrixDecomposition.toFun w + o.matrixDecomposition.toFun z

Tactic:
by
      ext
      dsimp [biproduct.components]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ eqToHom ⋯ ≫ biproduct.ι (fun a ↦ s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c =
    ∑ x,
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫ biproduct.π (fun b ↦ s (g b)) ↑x ≫ biproduct.ι (fun a ↦ s (g a)) ↑x ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c

Tactic:
conv_lhs => rw [← Category.id_comp w, ← biproduct.total]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
o : HomOrthogonal s
α β γ : Type
inst✝² : Finite α
inst✝¹ : Fintype β
inst✝ : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
w : (⨁ fun b ↦ s (g b)) ⟶ ⨁ fun c ↦ s (h c)
c : γ
a : α
j_property✝ : a ∈ f ⁻¹' {h c}
j_property : f a = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι (fun a ↦ s (f a)) a ≫
        z ≫
          ((∑ j, biproduct.π (fun b ↦ s (g b)) j ≫ biproduct.ι (fun b ↦ s (g b)) j) ≫ w) ≫
            biproduct.π (fun b ↦ s (h b)) c =
    ∑ x,
      eqToHom ⋯ ≫
        biproduct.ι (fun a ↦ s (f a)) a ≫
          z ≫ biproduct.π (fun b ↦ s (g b)) ↑x ≫ biproduct.ι (fun a ↦ s (g a)) ↑x ≫ w ≫ biproduct.π (fun b ↦ s (h b)) c
Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteBiproducts C
R : Type u_2
inst✝³ : Semiring R
inst✝² : Linear R C
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
w : R
z : (⨁ fun a ↦ s (f a)) ⟶ ⨁ fun b ↦ s (g b)
⊢ o.matrixDecompositionAddEquiv.toFun (w • z) = (RingHom.id R) w • o.matrixDecompositionAddEquiv.toFun z

Tactic:
by
      ext
      dsimp [biproduct.components]
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
f : X ⟶ Y
⊢ biprod.lift f 0 ≫ biprod.snd = (f ≫ biprod.inl) ≫ biprod.snd

Tactic:
· simp [biprod.lift_snd, Category.assoc, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
M : Mat_ C
i j : M.ι
h : i ≠ j
⊢ 𝟙 M i j = 0

Tactic:
by
  simp [id_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : Mat R
i j : M.obj
h : i ≠ j
⊢ 𝟙 M i j = 0

Tactic:
by
  simp [id_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
g₂ : Y ⟶ Z
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
h : (fun g ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁) = (fun g ↦ f ≫ g) g₂
⊢ g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁ = g₂

Tactic:
obtain ⟨j₂, g₂, rfl⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit g₂

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u'
inst✝³ : Category.{v', u'} J
inst✝² : EssentiallySmall.{w, v', u'} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ
Z : C
x✝ : W.isLocal.colimitsOfShape J Z
X Y : C
f : X ⟶ Y
hf : W f
p : W.isLocal.ColimitOfShape J Z
left✝ : IsCardinalPresentable X κ
right✝ : IsCardinalPresentable Y κ
j₁ : J
g₁ : Y ⟶ p.diag.obj j₁
j₂ : J
g₂ : Y ⟶ p.diag.obj j₂
h : (fun g ↦ f ≫ g) (g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁) = (fun g ↦ f ≫ g) (g₂ ≫ { pt := Z, ι := p.ι }.ι.app j₂)
⊢ g₁ ≫ { pt := Z, ι := p.ι }.ι.app j₁ = g₂ ≫ { pt := Z, ι := p.ι }.ι.app j₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
x✝ : IsIso (toSucc W Z)
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective fun g ↦ f ≫ g

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
⊢ IsIso (toSucc W Z)

Tactic:
· refine ⟨fun g₁ g₂ h ↦ ?_, fun g ↦ ?_⟩
    · simpa [← cancel_mono (toSucc W Z)] using
        D₂.condition f hf (g₁ := g₁ ≫ toStep W Z) (g₂ := g₂ ≫ toStep W Z)
          (by simp [reassoc_of% h])
    · have hZ := IsIso.hom_inv_id (toSucc W Z)
      simp only [Category.assoc] at hZ
      exact ⟨D₁.ιRight f hf g ≫ pushout.inl _ _ ≫ fromStep W Z ≫ inv (toSucc W Z),
        by simp [← D₁.ιLeft_comp_t_assoc, pushout.condition_assoc, hZ]⟩

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
⊢ IsIso (toSucc W Z)
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
hY' : ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
B : Set X
⊢ B ⊆ φ Y m B

Tactic:
dsimp [φ]
  split_ifs with hB
  · intro b hb
    obtain ⟨C, hC, hC'⟩ := hY' B hB ⟨{⟨b, hb⟩},
      hasCardinalLT_of_finite _ _ (IsRegular.aleph0_le Fact.out)⟩
    refine Set.subset_iUnion _ ⟨C, hC⟩ (Or.inl ?_)
    simp only [Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]
    exact ⟨hb, @hC' ⟨b, hb⟩ (by simp)⟩
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_3
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
⊢ ∀ ⦃j : J⦄, (D₂ D hι u).P j → ∀ (l₁ l₂ : j ⟶ m), (D₂ D hι u).W l₁ → (D₂ D hι u).W l₂ → l₁ = l₂

Tactic:
intro j hj l₁ l₂ hl₁ hl₂

Goal state after:
case refine_3
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
hj : (D₂ D hι u).P j
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ l₁ = l₂
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
this✝¹ : IsCardinalFiltered (DiagramWithUniqueTerminal J κ) κ
this✝ : IsFiltered J
this : IsFiltered (DiagramWithUniqueTerminal J κ)
j : J
D : DiagramWithUniqueTerminal J κ
f₁ f₂ : j ⟶ D.top
m₀ : J
t : D.top ⟶ m₀
hm₀ : IsEmpty (m₀ ⟶ D.top)
m₁ : J
u : m₀ ⟶ m₁
hu : f₁ ≫ t ≫ u = f₂ ≫ t ≫ u
h₁ : ¬D.P m₁
φ : (x : Subtype D.P) → ↑x ⟶ m₁ := fun x ↦ D.isTerminal.lift ⋯ ≫ t ≫ u
h₂ : ∀ {j : J} (hj : D.P j) {f : j ⟶ m₁}, (D₄ D φ).W f → f = φ ⟨j, hj⟩
h₃ : ∀ {f : m₁ ⟶ m₁}, (D₄ D φ).W f → f = 𝟙 m₁
l₁ l₂ : m₁ ⟶ m₁
hl₁ : (D₄ D φ).W l₁
hl₂ : (D₄ D φ).W l₂
⊢ l₁ = l₂

Tactic:
rw [h₃ hl₁, h₃ hl₂]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
x✝ : Arrow (Sheaf J A)
⊢ locallyInjective J A
    (((sheafToPresheaf J A).mapArrow.whiskerLeft
            (whiskerRight (MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).p
              (presheafToSheaf J A)) ≫
          Arrow.rightFunc.whiskerLeft (sheafificationAdjunction J A).counit).app
      x✝)

Tactic:
by
    dsimp [locallyInjective]
    rw [← isLocallyInjective_sheafToPresheaf_map_iff, Functor.map_comp,
      Presheaf.isLocallyInjective_comp_iff, isLocallyInjective_sheafToPresheaf_map_iff,
      Presheaf.isLocallyInjective_presheafToSheaf_map_iff]
    apply Presheaf.isLocallyInjective_of_injective
    apply (data.functorCategory Cᵒᵖ).hp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ (e i₁).hom ≫
      D₂.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂

Tactic:
← reassoc_of% (comm i₁ i₂),

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Adj Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
D₁ D₂ : F.DescentDataAsCoalgebra f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    D₁.hom i₁ i₂ ≫ (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) =
      (e i₁).hom ≫ D₂.hom i₁ i₂
i₁ i₂ : ι
⊢ D₁.hom i₁ i₂ ≫
      (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).hom) ≫
        (F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (e i₂).inv) =
    (e i₁).hom ≫ (e i₁).inv ≫ D₁.hom i₁ i₂
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (sq i₁ i₂).p₂.op.toLoc ≫ p.op.toLoc = f₂.op.toLoc

Tactic:
by rw [← Quiver.Hom.comp_toLoc, ← op_comp, IsPullback.lift_snd]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ (↑s (op X₂)).app (op (Over.mk (𝟙 X₂))) =
    ((Over.forget (unop (op X₁))).op ⋙ F).map (Over.homMk f ⋯).op ≫ (↑s (op X₁)).app (op (Over.mk f))

Tactic:
← s.2 f.op

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
s : ↑(presheafHom F G).sections
X₁ X₂ : C
f : X₂ ⟶ X₁
⊢ F.map (op f) ≫ ((ConcreteCategory.hom ((presheafHom F G).map f.op)) (↑s (op X₁))).app (op (Over.mk (𝟙 X₂))) =
    ((Over.forget (unop (op X₁))).op ⋙ F).map (Over.homMk f ⋯).op ≫ (↑s (op X₁)).app (op (Over.mk f))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q : Y ⟶ S') ⦃i₁ i₂ : ι'⦄ (f₁ : Y ⟶ X' i₁) (f₂ : Y ⟶ X' i₂) (hf₁ : f₁ ≫ f' i₁ = q) (hf₂ : f₂ ≫ f' i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map (D.iso (p' i₁ ≫ f (α i₁)) (p' i₁) (p'' i₁) ⋯ ⋯).hom ≫
        ((pullFunctor F w').obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F w).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map (D.iso (p' i₂ ≫ f (α i₂)) (p' i₂) (p'' i₂) ⋯ ⋯).hom

Tactic:
intro Y q j₁ j₂ f₁ f₂ hf₁ hf₂
    dsimp
    rw [pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      pullFunctorObjHom_eq _ _ _ _ _ (q ≫ p) _ _ rfl (by cat_disch) (by cat_disch),
      map_eq_pullHom_assoc _ _ (f₁ ≫ p' j₁) (f₁ ≫ p'' j₁) (by cat_disch) (by cat_disch),
      map_eq_pullHom _ _ (f₂ ≫ p' j₂) (f₂ ≫ p'' j₂) (by cat_disch) (by cat_disch)]
    simp only [Cat.Hom.hom_inv_id_toNatTrans_app_assoc, Category.assoc]
    rw [pullHom_hom _ _ _ (q ≫ p) (by rw [w, reassoc_of% hf₁]) _ _
        rfl (by cat_disch) _ _ rfl rfl, hom_comp_assoc,
      pullHom_hom _ _ _ (q ≫ p) (by rw [w, reassoc_of% hf₂]) _ _
        rfl (by cat_disch) _ _ rfl rfl, hom_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm S).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ (Sieve.overEquiv (Over.mk f)).symm S ∈ (J.over X) (Over.mk f)

Tactic:
rw [mem_over_iff, OrderIso.apply_symm_apply]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
S : Sieve (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm S).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ J (Over.mk f).left
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b) =
    shrinkYonedaObjObjEquiv.symm (𝟙 X)
⊢ shrinkYonedaObjObjEquiv.symm (b ≫ a) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b)

Tactic:
shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
Y : C
a : Y ⟶ X
ha : S.arrows a
b : X ⟶ Y
hb :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map a).app (op X))) (shrinkYonedaObjObjEquiv.symm b) =
    shrinkYonedaObjObjEquiv.symm (𝟙 X)
⊢ shrinkYonedaObjObjEquiv.symm (b ≫ a) = shrinkYonedaObjObjEquiv.symm (b ≫ a)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
S'' : C
q : S'' ⟶ S'
ι'' : Type t''
X'' : ι'' → C
f'' : (k : ι'') → X'' k ⟶ S''
β : ι'' → ι'
q' : (k : ι'') → X'' k ⟶ X' (β k)
w' : ∀ (k : ι''), q' k ≫ f' (β k) = f'' k ≫ q
r : S'' ⟶ S
r' : (k : ι'') → X'' k ⟶ X (α (β k))
hr : autoParam (q ≫ p = r) pullFunctorCompIso._auto_1
hr' : autoParam (∀ (k : ι''), q' k ≫ p' (β k) = r' k) pullFunctorCompIso._auto_3
k : ι''
⊢ r' k ≫ f (α (β k)) = f'' k ≫ r

Tactic:
rw [← hr', Category.assoc, w, reassoc_of% w', hr]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
i : ι
Y : C
i' : ι'
w✝ : X i ⟶ X' i'
fac : w✝ ≫ f' i' = f i
⊢ ∃ i' g, g ≫ f' i' = f i

Tactic:
exact ⟨i', _, fac⟩

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

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✝¹³ : 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
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
⊢ ψ ≫ g = ψ ≫ ((adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃) ≫ (Functor.commShiftIso G 1).hom.app T.obj₁

Tactic:
← cancel_mono ((Functor.commShiftIso G (1 : ℤ)).inv.app T.obj₁),

Goal state after:
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
φ : Y ⟶ G.obj T.obj₃
ψ : Y ⟶ Z
hψ : φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ = ψ ≫ g
α : Y ⟶ G.obj T.obj₃
hα : α = φ - ψ ≫ (adj.homEquiv Z T.obj₃) h
⊢ (ψ ≫ g) ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ =
    (ψ ≫ ((adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃) ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ≫
      (Functor.commShiftIso G 1).inv.app T.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : 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✝ : G.IsTriangulated
⊢ F.IsTriangulated

Tactic:
have := isTriangulated_rightAdjoint adj.op

Goal state after:
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✝ : G.IsTriangulated
this : F.op.IsTriangulated
⊢ F.IsTriangulated