mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ q = p + (n + a)

Tactic:
hn',

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ q = p + n'
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (x y : R) (b : T₁ ⟶ T₂), (x * y) • b = x • y • b

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (b : T₁ ⟶ T₂), 1 • b = b

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (a : R), a • 0 = 0

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (a : R) (x y : T₁ ⟶ T₂), a • (x + y) = a • x + a • y

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (r s : R) (x : T₁ ⟶ T₂), (r + s) • x = r • x + s • x

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝⁴ : Preadditive C
R : Type u_1
inst✝³ : Semiring R
inst✝² : Linear R C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), Functor.Linear R (shiftFunctor C n)
⊢ ∀ (x : T₁ ⟶ T₂), 0 • x = 0

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
inst✝⁴ : HasProduct fun j ↦ (T j).obj₁
inst✝³ : HasProduct fun j ↦ (T j).obj₂
inst✝² : HasProduct fun j ↦ (T j).obj₃
inst✝¹ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
⊢ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle T).mor₁ = 0

Tactic:
have : HasProduct (fun j => (T j).obj₂⟦(1 : ℤ)⟧) :=
    ⟨_, isLimitFanMkObjOfIsLimit (shiftFunctor C (1 : ℤ)) _ _
      (productIsProduct (fun j => (T j).obj₂))⟩
  dsimp
  change _ ≫ (Pi.lift (fun j => Pi.π _ j ≫ (T j).mor₁))⟦(1 : ℤ)⟧' = 0
  rw [assoc, ← cancel_mono (piComparison _ _), zero_comp, assoc, assoc]
  ext j
  simp [h j]

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

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 → IsIso T.mor₂

Tactic:
intro ⟨h₁, h₃⟩

Goal state after:
case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
⊢ IsIso T.mor₂
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ inr φ₁ ≫ mapOfHomotopy H = b ≫ inr φ₂

Tactic:
by
  simp [mapOfHomotopy]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ) ≅
    triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) (n.negOnePow • Iso.refl _) (shiftIso φ n) ?_ ?_ ?_

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₁ ≫
      (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom =
    (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₁

case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom =
    (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂

case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁰ : Category.{v_1, u_1} C
inst✝¹⁹ : Category.{v_2, u_2} D
inst✝¹⁸ : Category.{v_3, u_3} E
inst✝¹⁷ : HasShift C ℤ
inst✝¹⁶ : HasShift D ℤ
inst✝¹⁵ : HasShift E ℤ
F : C ⥤ D
inst✝¹⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝¹³ : G.CommShift ℤ
inst✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X Y : C
h₁ : 0 = 0 ≫ 𝟙 0 ≫ 0
h₂ : 𝟙 (F.obj 0) = 0
⊢ F.map 0 = 0

Tactic:
rw [h₁, F.map_comp, F.map_comp, F.map_id, h₂, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (lift φ).map f.toPath = φ.map f

Tactic:
dsimp [Quiver.Hom.toPath, lift]

Goal state after:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ 𝟙 (φ.obj X) ≫ φ.map f = φ.map f
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case id
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ : C
X Y : Paths (LocQuiver W)
⊢ (liftToPathCategory G hG).map (ψ₁ W (𝟙 X✝)) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))

Tactic:
aesop

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

Goal state before:
pp: case comp
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝¹ : C
X Y : Paths (LocQuiver W)
Y✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Y✝¹
⊢ (liftToPathCategory G hG).map (ψ₁ W (f✝ ≫ g✝)) = (liftToPathCategory G hG).map (ψ₁ W f✝ ≫ ψ₁ W g✝)

Tactic:
aesop

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

Goal state before:
pp: case Winv₁
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝ : C
X Y : Paths (LocQuiver W)
Y✝ : C
w✝ : X✝ ⟶ Y✝
hw✝ : W w✝
⊢ (liftToPathCategory G hG).map (ψ₁ W w✝ ≫ ψ₂ W w✝ hw✝) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝))

Tactic:
aesop

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

Goal state before:
pp: case Winv₂
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X✝¹ : C
X Y : Paths (LocQuiver W)
X✝ : C
w✝ : X✝ ⟶ X✝¹
hw✝ : W w✝
⊢ (liftToPathCategory G hG).map (ψ₂ W w✝ hw✝ ≫ ψ₁ W w✝) = (liftToPathCategory G hG).map (𝟙 (ιPaths W X✝¹))

Tactic:
aesop

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ G₁ = G₂

Tactic:
suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂ by
    refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this✝ : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f

Tactic:
rcases X with ⟨⟨X⟩⟩
      rcases Y with ⟨⟨Y⟩⟩
      simpa only [Functor.map_preimage] using! this _ _ (G.preimage f)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Equivalence

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
⊢ L₂.IsLocalization W₂

Tactic:
have : (E.functor ⋙ L₂).IsLocalization W₁ :=
    of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_4, u_4} D₁
inst✝² : Category.{v_5, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
this : (E.functor ⋙ L₂).IsLocalization W₁
⊢ L₂.IsLocalization W₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows

Goal state before:
pp: case succ
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D (n + 1)
⊢ (L.mapComposableArrows (n + 1)).essImage Y

Tactic:
obtain ⟨Y, Z, f, rfl⟩ := ComposableArrows.precomp_surjective Y

Goal state after:
case succ
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
n : ℕ
hn : ∀ (Y : ComposableArrows D n), (L.mapComposableArrows n).essImage Y
Y : ComposableArrows D n
Z : D
f : Z ⟶ Y.left
⊢ (L.mapComposableArrows (n + 1)).essImage (Y.precomp f)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
⊢ LeftFractionRel z₁ z₃

Tactic:
have eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄ := by
    simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
⊢ LeftFractionRel z₁ z₃
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ (z₁.comp₀ z₂ z₃).f ≫ z₄.f ≫ t = (z₁.comp₀ z₂ z₃').f ≫ z₄.s ≫ t

pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ W ((z₁.comp₀ z₂ z₃).s ≫ z₄.f ≫ t)

Tactic:
· simp only [comp₀, assoc, fac']

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y✝ Z : C
z₁ : W.LeftFraction X Y✝
z₂ : W.LeftFraction Y✝ Z
z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f
z₄ : W.LeftFraction z₃.Y' z₃'.Y'
fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f
eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s
Y : C
t : z₄.Y' ⟶ Y
ht : W t
fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t
⊢ W ((z₁.comp₀ z₂ z₃).s ≫ z₄.f ≫ t)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ f' = ψ.snd.map L ⋯

Tactic:
rw [← cancel_mono (L.map (φ'.s ≫ α.s)), hφ']
    nth_rw 1 [L.map_comp]
    rw [LeftFraction.map_comp_map_s_assoc, LeftFraction.map_comp_map_s,
      L.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝¹² : Category.{v_1, u_1} C₁
inst✝¹¹ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type u_3
inst✝¹⁰ : AddMonoid M
inst✝⁹ : HasShift C₁ M
inst✝⁸ : HasShift C₂ M
inst✝⁷ : Φ.functor.CommShift M
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{v_3, u_4} D₁
inst✝⁵ : Category.{v_4, u_5} D₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : HasShift D₁ M
inst✝² : HasShift D₂ M
inst✝¹ : L₁.CommShift M
inst✝ : L₂.CommShift M
G : D₁ ⥤ D₂
e : Φ.functor ⋙ L₂ ≅ L₁ ⋙ G
this : G.CommShift M := Φ.commShift M L₁ L₂ G e
m : M
X : C₁
⊢ ((Functor.commShiftIso (Φ.functor ⋙ L₂) m).hom ≫ Functor.whiskerRight e.hom (shiftFunctor D₂ m)).app X =
    ((shiftFunctor C₁ m).whiskerLeft e.hom ≫ (Functor.commShiftIso (L₁ ⋙ G) m).hom).app X

Tactic:
simp [Functor.commShiftIso_comp_hom_app, commShift_iso_hom_app, ← Functor.map_comp_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
← cancel_mono (G.map (L.objObjPreimageIso Y).inv),

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✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map (L.objObjPreimageIso X).hom ≫ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv =
    G.map (L.objObjPreimageIso X).hom ≫ (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
⊢ G.map (f + g) ≫ G.map (L.objObjPreimageIso Y).inv = (G.map f + G.map g) ≫ G.map (L.objObjPreimageIso Y).inv
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ ∧ HasCardinalLT PUnit.{1} κ ↔ HasCardinalLT X κ

Tactic:
and_iff_left_iff_imp

Goal state after:
X : Type u
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
⊢ HasCardinalLT X κ → HasCardinalLT PUnit.{1} κ
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst✝ : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT (↑(S i)) κ
⊢ ⋃ i, S i = Set.ofPred (⨆ i, S i)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝¹¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝¹⁰ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁹ : LinearOrder β
inst✝⁸ : OrderBot β
inst✝⁷ : SuccOrder β
inst✝⁶ : WellFoundedLT β
inst✝⁵ : ObjectProperty.Small.{w, v, u} P
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : Small.{w, t} α
inst✝² : ∀ (a : α), Small.{w, u'} (J a)
inst✝¹ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
b✝ : β
hb₀ : Small.{w, w'} ↑(Set.Iio b✝)
b c : β
hbc : b ≤ c
inst✝ : Small.{w, w'} ↑(Set.Iio c)
x✝² x✝¹ : ↑(Set.Iio b)
x✝ : (fun x ↦ ⟨↑x, ⋯⟩) x✝² = (fun x ↦ ⟨↑x, ⋯⟩) x✝¹
⊢ x✝² = x✝¹

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
E : Type u_3
inst✝² : Category.{v_2, u_3} E
inst✝¹ : HasShift E A
a : A
inst✝ : P.IsStableUnderShiftBy a
⊢ P.isoClosure ≤ P.isoClosure.shift a

Tactic:
rintro X ⟨Y, hY, ⟨e⟩⟩

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
E : Type u_3
inst✝² : Category.{v_2, u_3} E
inst✝¹ : HasShift E A
a : A
inst✝ : P.IsStableUnderShiftBy a
X Y : C
hY : P Y
e : X ≅ Y
⊢ P.isoClosure.shift a X
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.IsStableUnderShift A
X Y : C
a : A
i : X ≅ (shiftFunctor C a).obj Y
hY : P Y
⊢ P X

Tactic:
exact P.prop_of_iso i.symm (P.le_shift a Y hY)

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : P.IsClosedUnderIsomorphisms
h : P.shiftClosure A = P
⊢ P.IsStableUnderShift A

Tactic:
by rw [← h]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteProducts C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
this✝ : P.IsClosedUnderIsomorphisms
this : HasFiniteProducts P.FullSubcategory
⊢ P.IsClosedUnderFiniteProducts

Tactic:
have := PreservesFiniteProducts.of_preserves_binary_and_terminal P.ι

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasFiniteProducts C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
this✝¹ : P.IsClosedUnderIsomorphisms
this✝ : HasFiniteProducts P.FullSubcategory
this : PreservesFiniteProducts P.ι
⊢ P.IsClosedUnderFiniteProducts