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

Goal state before:
pp: case refine_1
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
⊢ ((P : Sylow (↑⟨p, hp⟩) G) → ↥P) ≃* ↥↑(P ↑⟨p, hp⟩)

Tactic:
haveI hp' := Fact.mk (Nat.prime_of_mem_primeFactors hp)

Goal state after:
case refine_1
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
p : ℕ
hp : p ∈ ps
hp' : Fact (Nat.Prime p)
⊢ ((P : Sylow (↑⟨p, hp⟩) G) → ↥P) ≃* ↥↑(P ↑⟨p, hp⟩)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι✝ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁸ : Ring R✝
inst✝⁷ : Ring S
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R✝ M
m : Submodule R✝ M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
ι : Type u_7
inst✝² : Finite ι
R : ι → Type u_6
inst✝¹ : (i : ι) → Ring (R i)
inst✝ : ∀ (i : ι), IsSemisimpleRing (R i)
x✝ : (i : ι) → Module ((i : ι) → R i) (R i) := fun i ↦ Module.compHom (R i) (Pi.evalRingHom R i)
e : (i : ι) → R i →ₛₗ[Pi.evalRingHom R i] R i :=
  fun i ↦
    let __src := AddMonoidHom.id (R i);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing ((i : ι) → R i)

Tactic:
have (i : _) : IsSemisimpleModule (Π i, R i) (R i) :=
    ((e i).isSemisimpleModule_iff_of_bijective Function.bijective_id).mpr inferInstance

Goal state after:
ι✝ : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁸ : Ring R✝
inst✝⁷ : Ring S
M : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R✝ M
m : Submodule R✝ M
N : Type u_5
inst✝⁴ : AddCommGroup N
inst✝³ : Module R✝ N
ι : Type u_7
inst✝² : Finite ι
R : ι → Type u_6
inst✝¹ : (i : ι) → Ring (R i)
inst✝ : ∀ (i : ι), IsSemisimpleRing (R i)
x✝ : (i : ι) → Module ((i : ι) → R i) (R i) := fun i ↦ Module.compHom (R i) (Pi.evalRingHom R i)
e : (i : ι) → R i →ₛₗ[Pi.evalRingHom R i] R i :=
  fun i ↦
    let __src := AddMonoidHom.id (R i);
    { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
this : ∀ (i : ι), IsSemisimpleModule ((i : ι) → R i) (R i)
⊢ IsSemisimpleRing ((i : ι) → R i)
Module: Mathlib.Algebra.Polynomial.Module.AEval

Goal state before:
pp: R : Type u_2
A : Type u_3
M : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
a : A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
m : M
n : ℕ
⊢ X ^ n • (of R M a) m = (of R M a) (a ^ n • m)

Tactic:
by
  rw [← of_aeval_smul, aeval_X_pow]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ (map R' f) (p • q) = Polynomial.map (algebraMap R R') p • (map R' f) q

Tactic:
induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
    | monomial => rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_5
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m✝ m' m₁ m₂ m₁' m₂' : M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ((s • m).coeff.sum fun i m ↦ r ^ i • m) = (RingHom.id R) s • m.coeff.sum fun i m ↦ r ^ i • m

Tactic:
by
    refine (Finsupp.sum_smul_index' ?_).trans ?_
    · exact fun i => smul_zero _
    · simp_rw [RingHom.id_apply, Finsupp.smul_sum]
      congr
      ext i c
      rw [smul_comm]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
y : M
hy : ∃ y_1 ∈ I, y_1 • i = y
z : M
hz : z ∈ I • span R s
hyz : y + z = r • n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
rcases hy with ⟨d, _, rfl⟩

Goal state after:
case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • Quotient.mk'' x = 0
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
⊢ torsionBy R (R ⧸ R ∙ a * b) a = R ∙ (mk (R ∙ a * b)) b

Tactic:
by
  ext x; rw [mem_torsionBy_iff, Submodule.mem_span_singleton]
  obtain ⟨x, rfl⟩ := mk_surjective x; constructor <;> intro h
  · rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
    obtain ⟨c, h⟩ := h
    rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
      mul_comm] at h
    use c
    rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
  · obtain ⟨c, h⟩ := h
    rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
      (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
x : I.Cotangent
⊢ I.cotangentToQuotientSquare x ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
by rw [← range_cotangentToQuotientSquare]; exact LinearMap.mem_range_self _ _

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
S✝ : Type v
S' : Type w
inst✝¹⁴ : CommRing R
inst✝¹³ : CommSemiring S✝
inst✝¹² : Algebra S✝ R
inst✝¹¹ : CommSemiring S'
inst✝¹⁰ : Algebra S' R
inst✝⁹ : Algebra S✝ S'
inst✝⁸ : IsScalarTower S✝ S' R
I✝ : Ideal R
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra R S
I : Ideal S
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ↥I →ₗ[R] M
hf : ∀ (x y : ↥I), f (x * y) = 0
r : R
x : I.Cotangent
⊢ (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun (r • x) =
    (RingHom.id R) r • (↑(QuotientAddGroup.lift (I • ⊤).toAddSubgroup f.toAddMonoidHom ⋯)).toFun x

Tactic:
obtain ⟨x, rfl⟩ := I.toCotangent_surjective x
    exact map_smul f _ _

Goal state after:
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
⊢ ⊤.spanRank ≤ ⊤.spanRank

Tactic:
obtain ⟨s, hs_card, hs_span⟩ :=
      (⊤ : Submodule (ResidueField R) (CotangentSpace R)).exists_span_set_card_eq_spanRank
    have hs_span' : Submodule.span R s =
        Submodule.map (Submodule.mkQ (maximalIdeal R • (⊤ : Submodule R (maximalIdeal R)))) ⊤ := by
      rw [Submodule.map_top, Submodule.range_mkQ]
      change Submodule.span R s = ⊤
      rw [← Submodule.restrictScalars_span R (ResidueField R)
        Ideal.Quotient.mk_surjective, hs_span, Submodule.restrictScalars_top]
    obtain ⟨t, ht_inj, ht_image, ht_span⟩ :=
      Submodule.exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot s
        ((Submodule.fg_top (maximalIdeal R)).mpr fg)
        (IsLocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge
        hs_span'
    rw [← hs_card, ← ht_span, ← ht_image]
    exact le_of_le_of_eq (Submodule.spanRank_span_le_card t)
      (Cardinal.mk_image_eq_of_injOn _ _ ht_inj).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
φ : M₁.presheaf ⟶ M₂.presheaf
hφ :
  ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
    (ConcreteCategory.hom (φ.app X)) (r • m) = r • (ConcreteCategory.hom (φ.app X)) m
X : Cᵒᵖ
⊢ ∀ (x y : ↑(M₁.1 X)),
    (ConcreteCategory.hom (φ.app X)) (x + y) = (ConcreteCategory.hom (φ.app X)) x + (ConcreteCategory.hom (φ.app X)) y

Tactic:
by simp +instances

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

Goal state before:
pp: case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
· rw [C.shape j k hjk, comp_zero]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃
⊢ shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯ ≪≫
      isoWhiskerRight (shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯ ≪≫ (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)

Tactic:
by
  subst h₁₂ h₂₃ h₁₂₃
  ext X
  dsimp
  simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.comp_id]
  dsimp [shiftFunctorAdd']
  simp only [eqToHom_app]
  dsimp [shiftFunctorAdd, shiftFunctor]
  simp only [obj_μ_inv_app, Discrete.addMonoidal_associator, eqToIso.hom, eqToHom_map,
    eqToHom_app]
  erw [δ_μ_app_assoc, Category.assoc]
  rfl

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : c.Rel i j
⊢ C.dFrom i ≫ (C.xNextIso r).hom = C.d i j

Tactic:
by
  simp [C.dFrom_eq r]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ IsZero S.homology

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
hS : ∀ (i : ι), IsZero (S.map (eval C c i)).homology
⊢ 𝟙 S.homology = 0
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ cyclesMap (φ ≫ ψ) i = cyclesMap φ i ≫ cyclesMap ψ i

Tactic:
dsimp [cyclesMap]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
⊢ ShortComplex.cyclesMap ((shortComplexFunctor C c i).map (φ ≫ ψ)) =
    ShortComplex.cyclesMap ((shortComplexFunctor C c i).map φ) ≫
      ShortComplex.cyclesMap ((shortComplexFunctor C c i).map ψ)
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 : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
⊢ e.f 0 = dFrom P 0 ≫ 0 + (zero ≫ (xPrevIso Q ⋯).inv) ≫ dTo Q 0

Tactic:
by simpa using comm_zero

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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
⊢ e.f 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ (xNextIso P ⋯).hom ≫ zero

Tactic:
by simpa using comm_zero

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
rw [IsZero.iff_id_eq_zero]

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 ↔ Nonempty (Homotopy (𝟙 C) 0)
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
⊢ (isoAdd' ⋯ (isoAdd' hab ea eb) ec).hom.app X = (isoAdd' ⋯ ea (isoAdd' hbc eb ec)).hom.app X

Tactic:
have := NatTrans.naturality_2 ec.hom ((shiftFunctorAdd' C a b ab hab).app X)

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
F : C ⥤ D
A : Type u_4
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a b c ab bc abc : A
ea : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
eb : shiftFunctor C b ⋙ F ≅ F ⋙ shiftFunctor D b
ec : shiftFunctor C c ⋙ F ≅ F ⋙ shiftFunctor D c
hab : a + b = ab
hbc : b + c = bc
h : a + b + c = abc
X : C
this :
  (shiftFunctor C c ⋙ F).map ((shiftFunctorAdd' C a b ab hab).app X).hom ≫
      ec.hom.app ((shiftFunctor C a ⋙ shiftFunctor C b).obj X) ≫
        (F ⋙ shiftFunctor D c).map ((shiftFunctorAdd' C a b ab hab).app X).inv =
    ec.hom.app ((shiftFunctor C ab).obj X)
⊢ (isoAdd' ⋯ (isoAdd' hab ea eb) ec).hom.app X = (isoAdd' ⋯ ea (isoAdd' hbc eb ec)).hom.app X
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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₂.obj₁
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃
⊢ ∃ b, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₂ ≫ c = b ≫ T₂.mor₂

Tactic:
by
  obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (inv_rot_of_distTriang _ hT₁) (inv_rot_of_distTriang _ hT₂) (c⟦(-1 : ℤ)⟧') a (by
    dsimp
    simp only [neg_comp, comp_neg, ← Functor.map_comp_assoc, ← comm,
      Functor.map_comp, shift_shift_neg', Functor.id_obj, assoc, Iso.inv_hom_id_app, comp_id])
  refine ⟨a, ⟨ha₁, ?_⟩⟩
  dsimp only [Triangle.invRotate, Triangle.mk] at ha₂
  rw [← cancel_mono ((shiftEquiv C (1 : ℤ)).counitIso.inv.app T₂.obj₃), assoc, assoc, ← ha₂]
  simp only [shiftEquiv'_counitIso, shift_neg_shift', assoc, Iso.inv_hom_id_app_assoc]

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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₃ ↔ IsIso T.mor₁

Tactic:
refine Iff.trans ?_ (Triangle.isZero₁_iff_isIso₂ _ (inv_rot_of_distTriang _ 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
⊢ IsZero T.obj₃ ↔ IsZero T.invRotate.obj₁
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
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
y₂ : A ⟶ T'.obj₂
x₃ : A ⟶ T.obj₃
hx₃ : x₃ ≫ φ.hom₃ = y₂ ≫ T'.mor₂
x₂ : A ⟶ T.obj₂
hx₂ : x₃ = x₂ ≫ T.mor₂
⊢ (y₂ - x₂ ≫ φ.hom₂) ≫ T'.mor₂ = 0

Tactic:
rw [sub_comp, assoc, ← φ.comm₂, ← reassoc_of% hx₂, hx₃, sub_self]

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✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i, g := opcyclesMap S.g i,
      zero := ⋯ }.Exact

Tactic:
by
  have : Epi (ShortComplex.map S (eval C c i)).g := by dsimp; infer_instance
  have hj := (hS.map (HomologicalComplex.eval C c i)).gIsCokernel
  apply ShortComplex.exact_of_g_is_cokernel
  refine CokernelCofork.IsColimit.ofπ' _ _ (fun {A} k hk => by
    dsimp at k hk ⊢
    have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])
    dsimp at H
    refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
    · rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2])

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

Goal state before:
pp: case refine_1.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths p
h : W.paths (p.comp (q'.cons f))
⊢ W.paths p

Tactic:
rw [Path.comp_cons] at h

Goal state after:
case refine_1.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths p
h : W.paths ((p.comp q').cons f)
⊢ W.paths p
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_2.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths q'
h : W.paths (p.comp (q'.cons f))
⊢ W.paths (q'.cons f)

Tactic:
rw [Path.comp_cons] at h

Goal state after:
case refine_2.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths q'
h : W.paths ((p.comp q').cons f)
⊢ W.paths (q'.cons f)
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
hp : W.paths p
h : W (𝟙 X)
⊢ W (composePath p)

Tactic:
revert hp
  exact p.rec (by simpa) fun p f hp hp' ↦ W.comp_mem _ _ (hp hp'.1) hp'.2

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)
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)
X Y : C
f : { as := { obj := X } } ⟶ { as := { obj := Y } }
a✝ : ⊤ f
⊢ P f

Tactic:
simpa only [Functor.map_preimage] using! this _ _ (G.preimage f)

Goal state after: