mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
g : A
hs : Function.Surjective fun x ↦ x • g
h_ne : g ≠ 0
this :
  ∀ {A : Type u_4} [inst : AddCommGroup A] [inst_1 : LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] (g : A),
    (Function.Surjective fun x ↦ x • g) → g ≠ 0 → 0 < g → Nonempty (A ≃+o ℤ)
hg' : ¬0 < g
⊢ Function.Surjective fun x ↦ x • -g

Tactic:
by simpa using! neg_surjective.comp hs

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
⊢ IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)

Tactic:
by
  refine ⟨?_, fun ⟨e⟩ ↦ e.isAddCyclic.mpr inferInstance⟩
  rintro ⟨g, hs⟩
  have h_ne : g ≠ 0 := by
    obtain ⟨a, ha⟩ := exists_ne (0 : A)
    obtain ⟨m, rfl⟩ := hs a
    aesop
  wlog hg' : 0 < g
  · exact this (g := -g) (by simpa using! neg_surjective.comp hs) (by grind) (by grind)
  have hi : (fun n : ℤ ↦ n • g).Injective := injective_zsmul_iff_not_isOfFinAddOrder.mpr
      <| not_isOfFinAddOrder_of_isAddTorsionFree h_ne
  exact ⟨.symm { Equiv.ofBijective _ ⟨hi, hs⟩ with
    map_add' := add_zsmul g
    map_le_map_iff' := zsmul_le_zsmul_iff_left hg' }⟩

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).castSucc, (snoc s₂ x₂ hsat₂).toFun (e (Fin.last s₁.length)).succ)

Tactic:
he_last

Goal state after:
case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
x₁ x₂ : X
hsat₁ : IsMaximal (last s₁) x₁
hsat₂ : IsMaximal (last s₂) x₂
hequiv : s₁.Equivalent s₂
hlast : Iso (last s₁, x₁) (last s₂, x₂)
e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
  Trans.trans (Trans.trans finSuccEquivLast (Functor.mapEquiv Option (Exists.choose hequiv))) finSuccEquivLast.symm
he_last : e (Fin.last s₁.length) = Fin.last s₂.length
he_castSucc : ∀ (j : Fin s₁.length), e j.castSucc = ((Exists.choose hequiv) j).castSucc
i : Fin (snoc s₁ x₁ hsat₁).length
⊢ Iso ((snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).castSucc, (snoc s₁ x₁ hsat₁).toFun (Fin.last s₁.length).succ)
    ((snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).castSucc, (snoc s₂ x₂ hsat₂).toFun (Fin.last s₂.length).succ)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this : Module R S := Module.compHom S f
⊢ IsSemisimpleRing S

Tactic:
have : RingHomSurjective f := ⟨hf⟩

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
f : R →+* S
hf : Function.Surjective ⇑f
inst✝ : IsSemisimpleRing R
this✝ : Module R S := Module.compHom S f
this : RingHomSurjective f
⊢ IsSemisimpleRing S
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N = I • N ⊔ N'
⊢ N' ≤ N

Tactic:
rw [hmaple]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : N = I • N ⊔ N'
⊢ N' ≤ I • N ⊔ N'
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
⊢ ∀ (i : Subtype (Membership.mem (Finset.range n.succ))),
    (Submodule.span (↥(reesAlgebra I)) (single R ↑i '' ↑(F.N ↑i))).FG

Tactic:
rintro ⟨i, hi⟩

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
⊢ (Submodule.span (↥(reesAlgebra I)) (single R ↑⟨i, hi⟩ '' ↑(F.N ↑⟨i, hi⟩))).FG
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ ⊤.spanRank ≤ ⊤.spanRank

Tactic:
rw [← hs_card, ← ht_span, ← ht_image]

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ (Submodule.span R t).spanRank ≤ Cardinal.mk ↑(⇑(maximalIdeal R • ⊤).mkQ '' t)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
⊢ x ∈ ⊥

Tactic:
by_contra hx'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsNoetherianRing R
inst✝¹ : Module.IsTorsionFree R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
⊢ False
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' = p'

Tactic:
by rw [← add_left_inj p, hp, ← h, add_assoc,
            ← add_assoc m', hm, zero_add, hn]

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 E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
f₁ g₁ f₂ g₂ : C ⟶ D
h₁ : Homotopy f₁ g₁
h₂ : Homotopy f₂ g₂
i j : ι
hij : ¬c.Rel j i
⊢ (h₁.hom + h₂.hom) i j = 0

Tactic:
rw [Pi.add_apply, Pi.add_apply, h₁.zero i j hij, h₂.zero i j hij, add_zero]

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ δ n m ↑z = 0

Tactic:
← mem_iff n m h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
z : Cocycle F G n
m : ℤ
h : n + 1 = m
⊢ ↑z ∈ cocycle F G n
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
⊢ ∀ {X Y Z : C} {f f' : X ⟶ Y} (g : Y ⟶ Z), CompClosure r f f' → CompClosure r (f ≫ g) (f' ≫ g)

Tactic:
rintro a d e _ _ g ⟨b, c, f, g₁, g₂, i, h⟩
    simpa using CompClosure.intro _ _ f _ _ (i ≫ g) h

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r✝ : HomRel C
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) ≫ Quot.mk (HomRel.CompClosure r) a = 𝟙 Y✝

Tactic:
simp [CategoryStruct.comp, CategoryStruct.id]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r✝ : HomRel C
G : Type u_2
inst✝ : Groupoid G
r : HomRel G
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quot.mk (HomRel.CompClosure r) a ≫ Quotient.inv r (Quot.mk (HomRel.CompClosure r) a) = 𝟙 X✝

Tactic:
simp [CategoryStruct.comp, CategoryStruct.id]

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type ?u.8
inst✝ : Category.{v_2, ?u.8} D
F✝ : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂
F G : Quotient r ⥤ D
τ : functor r ⋙ F ⟶ functor r ⋙ G
x✝¹ x✝ : Quotient r
X Y : C
⊢ ∀ (f : { as := X } ⟶ { as := Y }),
    (F.map f ≫
        match { as := Y } with
        | { as := X } => τ.app X) =
      (match { as := X } with
        | { as := X } => τ.app X) ≫
        G.map f

Tactic:
by
    rintro ⟨f⟩
    exact τ.naturality f

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
F : C ⥤ D
inst✝ : F.Additive
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso 0).hom.app x✝).f i✝ =
    ((CommShift.isoZero (F.mapHomologicalComplex (ComplexShape.up ℤ)) ℤ).hom.app x✝).f i✝

Tactic:
CommShift.isoZero_hom_app

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
F : C ⥤ D
inst✝ : F.Additive
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ ((F.mapCochainComplexShiftIso 0).hom.app x✝).f i✝ =
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map
            ((shiftFunctorZero (HomologicalComplex C (ComplexShape.up ℤ)) ℤ).hom.app x✝) ≫
          (shiftFunctorZero (HomologicalComplex D (ComplexShape.up ℤ)) ℤ).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
      i✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ ((γ.leftShift a n' hn').leftUnshift n hn').v p q hpq = γ.v p q hpq

Tactic:
(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a (q - n') p ⋯).inv ≫ (γ.leftShift a n' hn').v (q - n') q ⋯ =
    γ.v p q hpq
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
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₁
⊢ ∀ (s : Fan T) (m : s.pt ⟶ (fan T).pt), (∀ (j : J), m ≫ (fan T).proj j = s.proj j) → m = lift T s.proj

Tactic:
intro s

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle 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₁
s : Fan T
⊢ ∀ (m : s.pt ⟶ (fan T).pt), (∀ (j : J), m ≫ (fan T).proj j = s.proj j) → m = lift T s.proj
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mpr
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
a✝ : Mono T.mor₂
⊢ T.mor₁ ≫ T.mor₂ = 0 ≫ T.mor₂

Tactic:
comp_distTriang_mor_zero₁₂ _ hT,

Goal state after:
case mpr
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
a✝ : Mono T.mor₂
⊢ 0 = 0 ≫ T.mor₂
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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
comm' : φ₂ ≫ b' = a' ≫ φ₃
⊢ φ₁ ≫ b ≫ b' = (a ≫ a') ≫ φ₃

Tactic:
rw [reassoc_of% comm, comm', assoc]

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
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map (((-↑(fst φ)).rightShift 1 0 triangle._proof_3).v n n ⋯) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)

Tactic:
Cochain.rightShift_v _ 1 0 (by lia) n n (by lia) (n + 1) (by lia)

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
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((-↑(fst φ)).v n (n + 1) ⋯ ≫ (K.shiftFunctorObjXIso 1 n (n + 1) ⋯).inv) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)
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
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X.as ⟶ Y.as
⊢ ∃ Z g h, Triangle.mk ((quotient C (ComplexShape.up ℤ)).map f) g h ∈ distinguishedTriangles C

Tactic:
exact ⟨_, _, _, ⟨_, _, f, ⟨Iso.refl _⟩⟩⟩

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

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
b : Paths V
⊢ ∀ {a : Paths V} (f : a ⟶ b), P f

Tactic:
exact induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)

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

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝ : Φ.functor.IsEquivalence
h : W₂ ≤ W₁.map Φ.functor
this : (Φ.functor ⋙ W₂.Q).IsLocalization W₁
⊢ Φ.IsLocalizedEquivalence

Tactic:
exact IsLocalizedEquivalence.of_isLocalization_of_isLocalization Φ W₂.Q

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
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
obtain ⟨β, hβ₁, hβ₂⟩ := exists_leftFraction₂ L W g₁ g₂

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
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
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
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
⊢ G.CommShift M

Tactic:
by
  letI : Localization.Lifting L₁ W₁ (Φ.functor ⋙ L₂) G := ⟨e.symm⟩
  exact Functor.commShiftOfLocalization L₁ W₁ M (Φ.functor ⋙ L₂) G

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)
inst✝⁴ : ObjectProperty.EssentiallySmall.{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)
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P.limitsClosure J)

Tactic:
by
  obtain ⟨κ, h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall J
  have : Fact κ.IsRegular := ⟨h₁⟩
  exact isEssentiallySmall_limitsClosure P J κ h₂

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
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
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ (F.shift n₀).map (T.mor₁ ≫ T.mor₂) = 0

Tactic:
comp_distTriang_mor_zero₁₂ _ hT,

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
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
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
⊢ (F.shift n₀).map 0 = 0
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
h : φ.map L ⋯ = ψ.map L ⋯
⊢ LeftFractionRel φ ψ

Tactic:
← MorphismProperty.LeftFraction.Localization.map_eq_iff

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
h : φ.map L ⋯ = ψ.map L ⋯
⊢ φ.map (Localization.Q W) ⋯ = ψ.map (Localization.Q W) ⋯
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f ≫ (commShiftIso L n).hom.app Y) ≫ (F.shiftIso n a a' h).hom.app (L.obj Y) =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y

Tactic:
rw [Functor.map_comp, induced_shiftIso_hom_app_obj, assoc, assoc]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map ((commShiftIso L n).hom.app Y) ≫
        (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
          (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: 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.IsTriangulatedClosed₁
Y Z : C
b : Y ⟶ Z
hY : P Y
hZ : P Z
X : C
a : X ⟶ Y
c : Z ⟶ (shiftFunctor C 1).obj X
h : Triangle.mk a b c ∈ distinguishedTriangles
X' : C
hX' : P X'
e : (Triangle.mk a b c).obj₁ ≅ X'
⊢ ∃ X, ∃ (_ : P X), ∃ a c, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
exact ⟨X', hX', e.inv ≫ a, c ≫ e.hom⟦1⟧', isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ e.symm (Iso.refl _) (Iso.refl _))⟩

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 : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
comp,

Goal state after:
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 : C
inst✝¹ : Preadditive C
inst✝ : ∀ (a : M), (shiftFunctor C a).Additive
a b c : M
α : ShiftedHom X Y a
β₁ β₂ : ShiftedHom Y Z b
h : b + a = c
⊢ α ≫ (shiftFunctor C a).map (β₁ + β₂) ≫ (shiftFunctorAdd' C b a c h).inv.app Z = α.comp β₁ h + α.comp β₂ h