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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₁ ≅ (contractibleTriangle 0).obj₁

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₂ ≅ (contractibleTriangle 0).obj₂

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₃ ≅ (contractibleTriangle 0).obj₃

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
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₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
⊢ f ≫ T'.mor₃ = 0

Tactic:
rw [← cancel_mono (φ'.hom₁⟦1⟧'), zero_comp, assoc, φ'.comm₃, reassoc_of% hf, zero_comp]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
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₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ := fun j ↦ ⋯.choose
hα : ∀ (j : J), g ≫ Pi.π (fun j ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
hg''' : g = Pi.lift α ≫ T'.mor₁
⊢ f = 0

Tactic:
rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]

Goal state after:
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.mk (F.map X✝.mor₁) (F.map X✝.mor₂) (F.map X✝.mor₃ ≫ (commShiftIso F 1).hom.app X✝.obj₁)).mor₃ ≫
      (shiftFunctor D 1).map (F.map f.hom₁) =
    F.map f.hom₃ ≫
      (Triangle.mk (F.map Y✝.mor₁) (F.map Y✝.mor₂) (F.map Y✝.mor₃ ≫ (commShiftIso F 1).hom.app Y✝.obj₁)).mor₃

Tactic:
dsimp [Functor.comp]

Goal state after:
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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (F.map X✝.mor₃ ≫ (commShiftIso F 1).hom.app X✝.obj₁) ≫ (shiftFunctor D 1).map (F.map f.hom₁) =
    F.map f.hom₃ ≫ F.map Y✝.mor₃ ≫ (commShiftIso F 1).hom.app Y✝.obj₁
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ Int.negOnePow 2 = 1

Tactic:
rfl

Goal state after:
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✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : F.Additive
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
T : Triangle C
⊢ (F₁.map T.mor₃ ≫ (commShiftIso F₁ 1).hom.app T.obj₁) ≫ (shiftFunctor D 1).map (e.hom.app T.obj₁) =
    e.hom.app T.obj₃ ≫ F₂.map T.mor₃ ≫ (commShiftIso F₂ 1).hom.app T.obj₁

Tactic:
simp only [assoc, NatTrans.shift_app_comm e.hom (1 : ℤ) T.obj₁,
        NatTrans.naturality_assoc]

Goal state after:
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hij : c.Rel i j
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ Mono
    ((composableArrows₃ K i j).map' 0 1 instMonoMap'ComposableArrows₃OfNatNat._proof_1
      instMonoMap'ComposableArrows₃OfNatNat._proof_3)

Tactic:
by
  dsimp
  infer_instance

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

Goal state before:
pp: case nil
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ Quiver.Path.nil) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f

Tactic:
rfl

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

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
X : V
⊢ (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Tactic:
rfl

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

Goal state before:
pp: case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X : Paths V
⊢ Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ (𝟭 (Quotient (pathsHomRel C))).obj { as := as✝ } ≅ (quotientPathsTo C ⋙ toQuotientPaths C).obj { as := as✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
as✝ : Paths C
⊢ Quot.liftOn (𝟙 { as := as✝ }) (fun f ↦ composePath f) ⋯ = 𝟙 as✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
⊢ Quiver.homOfEq ((he X Y) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯ = Quiver.homOfEq ((he X Y) f) ⋯ ⋯

Tactic:
rfl

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'
  refine Paths.ext_functor ?_ ?_
  · ext X
    cases X
    apply Functor.congr_obj h
  · rintro ⟨X⟩ ⟨Y⟩ (f | ⟨w, hw⟩)
    · simpa only using! Functor.congr_hom h f
    · have hw : W.Q.map w = (wIso w hw).hom := rfl
      have hw' := Functor.congr_hom h w
      simp only [Functor.comp_map, hw] at hw'
      refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'
      all_goals apply Functor.congr_obj h

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 : C ⥤ D
hG : W.IsInvertedBy G
X : C
⊢ W.Q.obj ((fun X ↦ X.as.obj) { as := { obj := X } }) = { as := { obj := X } }

Tactic:
rfl

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

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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
⊢ W.Q = W.Q ⋙ 𝟭 W.Localization

Tactic:
rfl

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

Goal state before:
pp: case mk
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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
hW : W ≤ MorphismProperty.isomorphisms C
obj✝ : C → E
map✝ : {X Y : C} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
hF : W.IsInvertedBy { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
⊢ 𝟭 C ⋙ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } =
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
rfl

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

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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
⊢ MorphismProperty.isomorphisms C ≤ MorphismProperty.isomorphisms C

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : W f
⊢ (wIso f hf).hom = (isoOfHom W.Q W f hf).hom

Tactic:
rfl

Goal state after:
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
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ Quiver.Path.cons p' g = p' ≫ g.toPath

Tactic:
rfl

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

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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) = ((whiskeringLeftFunctor L W E).map τ).hom.app x✝

Tactic:
rfl

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
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X

Tactic:
rfl

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

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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))

Tactic:
rfl

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

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift L₂ h
⊢ L₂.IsLocalization W

Tactic:
exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

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✝ : C ⥤ D
hG : W.IsInvertedBy G✝
G : W.FunctorsInverting D
X : C
⊢ (𝟙 G).hom.app X = 𝟙 ((lift G.obj ⋯).obj (W.Q.obj X))

Tactic:
rfl

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 : C ⥤ D
hG : W.IsInvertedBy G
X✝ Y✝ Z✝ : W.FunctorsInverting D
τ₁ : X✝ ⟶ Y✝
τ₂ : Y✝ ⟶ Z✝
X : C
⊢ (τ₁ ≫ τ₂).hom.app X = τ₁.hom.app X ≫ τ₂.hom.app X

Tactic:
rfl

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
X Y : Cᵒᵖ
w : X ⟶ Y
hw : W.op w
⊢ (isoOfHom L.op W.op w hw).unop.hom = (isoOfHom L W w.unop hw).hom

Tactic:
rfl

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
⊢ φ.symm.add = φ.add

Tactic:
grind

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

Goal state before:
pp: case mp
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
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac' : (t₂ ≫ α.f ≫ u) ≫ u' = (t₂' ≫ α.s ≫ u) ≫ u'
⊢ LeftFraction₂Rel φ ψ

Tactic:
simp only [Category.assoc] at fac fac'

Goal state after:
case mp
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
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ LeftFraction₂Rel φ ψ
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (L₁.map f)

Tactic:
rw [← isIso_iff_of_reflects_iso  _ F]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁸ : Category.{v₁, u₁} C₁
inst✝⁷ : Category.{v₂, u₂} C₂
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : Φ.IsLocalizedFullyFaithful
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
L₁ : C₁ ⥤ D₁
F : D₁ ⥤ D₂
iso : Φ.functor ⋙ L₂ ≅ L₁ ⋙ F
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : L₁.EssSurj
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso (F.map (L₁.map f))
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : Φ.IsInduced
⊢ W₂.arrow.inverseImage Φ.functor.mapArrow = (W₂.inverseImage Φ.functor).arrow

Tactic:
rfl

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
⊢ Φ.inv.functor.IsEquivalence

Tactic:
by
  dsimp
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
A : Type w
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : W.IsCompatibleWithShift A
X Y : C
f : X ⟶ Y
a : A
⊢ W ((shiftFunctor C a).map f) ↔ W.inverseImage (shiftFunctor C a) f

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝³ : SupSet I
φ : I → I
J : Type w
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
i₀ : I
j : J
hj : ¬IsMax j
⊢ (φ ∘ SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) fun y x h ↦ ⨆ x, h ↑x ⋯)
      i₀ =
    φ
      (SuccOrder.limitRecOn j (motive := fun x ↦ I → I) (fun x x_1 ↦ id) (fun x x_1 g ↦ φ ∘ g) (fun y x h ↦ ⨆ x, h ↑x ⋯)
        i₀)

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isMin
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
hk : IsMin ⊥
hkj : ⊥ ≤ ⊥
⊢ (fun j ↦ transfiniteIterate φ j i₀) ⊥ ≤ (fun j ↦ transfiniteIterate φ j i₀) ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case succ.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k' : J
hk' : ¬IsMax k'
hkk' : Order.succ k' ≤ k' → (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) k'
hkj : Order.succ k' ≤ Order.succ k'
⊢ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k') ≤ (fun j ↦ transfiniteIterate φ j i₀) (Order.succ k')

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isSuccLimit.inr
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk' : Order.IsSuccLimit k
a✝ : ∀ b < k, k ≤ b → (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) b
hkj : k ≤ k
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) k

Tactic:
rfl

Goal state after: