mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.restrictScalars A (kerTotal R B))) =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker

Tactic:
← kerTotal_map' R A B h,

Goal state after:
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
h : Function.Surjective ⇑(algebraMap A B)
⊢ Submodule.map (linearCombination A ⇑(D R A))
      (Submodule.comap (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
        (Submodule.map (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B))
          (kerTotal R A ⊔ Submodule.span A (Set.range fun x ↦ single ((algebraMap R A) x) 1)))) =
    Submodule.map (linearCombination A ⇑(D R A))
      (mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j

Tactic:
by
  apply ext_to_X φ j k hjk
  · simp [d_fstX φ _ _ _ hij hjk]
  · simp [d_sndX φ _ _ hij]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
simp only [nullHomotopicMap']
  rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]
  split_ifs
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
⊢ γ₁ = γ₂ ↔
    (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯

Tactic:
constructor
  · rintro rfl
    tauto
  · rintro ⟨h₁, h₂⟩
    ext p q hpq
    rw [ext_from_iff φ (p + 1) p rfl]
    replace h₁ := Cochain.congr_v h₁ (p + 1) q (by lia)
    replace h₂ := Cochain.congr_v h₂ p q (by lia)
    simp only [Cochain.comp_v (inl φ) _ _ (p + 1) p q (by lia) hpq] at h₁
    simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v] at h₂
    exact ⟨h₁, h₂⟩

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

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
F G K L : CochainComplex C ℤ
n m : ℤ
z : Cocycle F G 0
i : ℤ
⊢ (↑z).v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ (↑z).v (i + 1) (i + 1) ⋯

Tactic:
rcases z with ⟨z, hz⟩

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
F G K L : CochainComplex C ℤ
n m i : ℤ
z : Cochain F G 0
hz : z ∈ cocycle F G 0
⊢ (↑⟨z, hz⟩).v i i ⋯ ≫ G.d i (i + 1) = F.d i (i + 1) ≫ (↑⟨z, hz⟩).v (i + 1) (i + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
⊢ H.map (inrX φ i) ≫ (mapHomologicalComplexObjXIso φ H i).hom = inrX ((H.mapHomologicalComplex c).map φ) i

Tactic:
← inrX_mapHomologicalComplexObjXIso_inv_assoc,

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫
      (mapHomologicalComplexObjXIso φ H i).inv ≫ (mapHomologicalComplexObjXIso φ H i).hom =
    inrX ((H.mapHomologicalComplex c).map φ) i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
subst h
      by_cases h : p'' = p'
      · subst h
        obtain rfl : p = p'' + 1 := by lia
        simp
      · rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]
        lia

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

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
· subst hm
    by_cases h : q'' = q
    · subst h
      by_cases h : p'' = p'
      · subst h
        obtain rfl : p = p'' + 1 := by lia
        simp
      · rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero, comp_zero, smul_zero]
        lia
    · simp [single_v_eq_zero' _ _ _ _ _ h]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.hom ≫ f.inv) = (quotient V c).map (𝟙 C)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.inv ≫ (quotient V c).map f.hom = 𝟙 ((quotient V c).obj D)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map (f.inv ≫ f.hom) = (quotient V c).map (𝟙 D)
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), a + 0 = a

Tactic:
rintro ⟨_⟩; exact congr_arg (functor r).map (add_zero _)

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f))
⊢ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f)) =
    r •
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
        (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y

Tactic:
← h₂

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
X Y : HomologicalComplex C (ComplexShape.up ℤ)
r : R
f : X ⟶ Y
h₁ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map f)
h₂ :
  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map ((quotient C (ComplexShape.up ℤ)).map (r • f))
⊢ (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
      (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map (r • f)) ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y =
    r •
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).inv.app X ≫
        (quotient C (ComplexShape.up ℤ)).map ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).map f) ≫
          (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) n).hom.app Y
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₃

Tactic:
by
        subst h
        dsimp
        rw [Linear.units_smul_comp, Linear.comp_units_smul, Functor.map_units_smul,
          Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, assoc, Functor.map_comp, assoc,
          ← dsimp% (CategoryTheory.shiftFunctorAdd' C a b (a + b) rfl).hom.naturality_assoc]
        simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Int.negOnePow_add,
          shiftFunctorComm_hom_app_comp_shift_shiftFunctorAdd_hom_app, add_comm a]

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
h : T.mor₃ = 0
X : C
g : T.obj₃ ⟶ X
⊢ T.mor₂ ≫ g = 0 → g = 0

Tactic:
hg

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
X : C
g : T.obj₃ ⟶ X
hg : T.mor₂ ≫ g = 0
⊢ g = 0
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
h : T.mor₁ = 0
X : C
g : X ⟶ T.obj₂
⊢ g ≫ T.mor₂ = 0 → g = 0

Tactic:
hg

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
X : C
g : X ⟶ T.obj₂
hg : g ≫ T.mor₂ = 0
⊢ g = 0
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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : IsZero T.obj₁
h₃ : IsZero T.obj₃
⊢ IsZero T.obj₂

Tactic:
T.isZero₂_iff hT

Goal state after:
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₁ : IsZero T.obj₁
h₃ : IsZero T.obj₃
⊢ T.mor₁ = 0 ∧ T.mor₂ = 0
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
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁴ : H.CommShift ℤ
inst✝³ : H.IsTriangulated
inst✝² : F.IsTriangulated
inst✝¹ : F.mapArrow.EssSurj
inst✝ : NatTrans.CommShift e.hom ℤ
⊢ G.IsTriangulated

Tactic:
by
  have := (isTriangulated_iff_of_iso e).2 inferInstance
  exact isTriangulated_of_precomp F G

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

Goal state before:
pp: case mpr
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₁ : Paths (LocQuiver W)
⊢ ∀ (X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)

Tactic:
X₂

Goal state after:
case mpr
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₂ : Paths (LocQuiver W)
⊢ ∀ (f : X₁ ⟶ X₂), P (G.map f)
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✝
⊢ ((whiskeringLeft W.Localization D E).obj (equivalenceFromModel L W).functor ⋙
            (Construction.whiskeringLeftEquivalence W E).functor).map
        τ ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (whiskeringLeftFunctor L W E).map τ

Tactic:
ext
        dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
        rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]
        dsimp
        rw [comp_id, id_comp]
        rfl

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| (commShiftOfLocalization.iso L W F F' b).hom.app (L.obj ((shiftFunctor C a).obj X)) ≫
    (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
      (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
        (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
          (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))

Tactic:
commShiftOfLocalization.iso_hom_app,

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| (F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
      (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
        (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
          (shiftFunctor E b).map ((Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X))) ≫
    (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
      (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
        (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
          (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
⊢ (Cocone.precompose p.diag.uniqueFromEmpty.inv).obj { pt := X, ι := p.ι } ≅ asEmptyCocone X

Tactic:
exact Cocone.ext (Iso.refl _) (by rintro ⟨⟨⟩⟩)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ : C
⊢ ∀ (X₂ : C), PreservesLimit (pair X₁ X₂) F

Tactic:
X₂

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
⊢ PreservesLimit (pair X₁ X₂) F
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ LeftFractionRel φ ψ

Tactic:
by
  constructor
  · intro h
    rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]
    apply map_eq_of_map_eq _ _ _ _ h
  · intro h
    simp only [← Localization.Hom.map_mk _ L (Localization.inverts _ _)]
    congr 1
    exact Quot.sound h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
by
  simp only [comp, assoc, Functor.map_comp,
    shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
    ← NatTrans.naturality_assoc, Functor.comp_map]

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
x✝ : HomologicalComplex C c
⊢ quasiIso C c (𝟙 x✝)

Tactic:
rw [mem_quasiIso_iff]
    infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ W✝ : HomologicalComplex C c
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h : RetractArrow f✝ g✝
hg : quasiIso C c g✝
⊢ quasiIso C c f✝

Tactic:
rw [mem_quasiIso_iff] at hg ⊢
    exact quasiIso_of_retractArrow h

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X) →
    ∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1

Tactic:
· rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : HomotopyCategory C c
⊢ quasiIso C c (𝟙 K)

Tactic:
rw [mem_quasiIso_iff]
    infer_instance

Goal state after: