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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
⊢ Nat.Prime (Nat.card α)

Tactic:
have hα : Nontrivial α := IsSimpleGroup.toNontrivial
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  replace hα : Nat.card α ≠ 1 := by contrapose! hα; exact (Nat.card_eq_one_iff_unique.mp hα).1
  rw [← orderOf_eq_card_of_forall_mem_zpowers hg] at hα ⊢
  have h (n : ℕ) : orderOf g ∣ n ∨ n.Coprime (orderOf g) := by
    refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
    · simp [orderOf_dvd_iff_pow_eq_one]
    · simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn
  apply Nat.prime_of_coprime
  · refine Nat.one_lt_iff_ne_zero_and_ne_one.mpr ⟨?_, hα⟩
    contrapose! h
    exact ⟨37, by simp [h]⟩
  · intro n hn hn0
    exact ((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup {a | IsAtom a} = ⊤

Tactic:
rw [eq_top_iff, ← h', ← hu₂]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (a : i ∈ s), f i = sSup (t i a)
ht' : ∀ (i : ι) (a : i ∈ s), ∀ a_1 ∈ t i a, IsAtom a_1
u : Set α := ⋃ i, ⋃ (hi : i ∈ s), t i hi
hu₁ : u ⊆ {a | IsAtom a}
hu₂ : sSup u = ⨆ i ∈ s, f i
⊢ sSup u ≤ sSup {a | IsAtom a}
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
⊢ ∃ y, 0 ≠ y

Tactic:
have h : (⊥ : Submodule R M) ≠ ⊤ := bot_ne_top

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSimpleModule R M
h : ⊥ ≠ ⊤
⊢ ∃ y, 0 ≠ y
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ torsionOf R M 0 = ⊤

Tactic:
simp [torsionOf]

Goal state after:
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 • x ∈ torsion R M
⊢ x ∈ torsion R M

Tactic:
obtain ⟨b, h⟩ := 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 b : ↥R⁰
h : b • a • x = 0
⊢ x ∈ torsion R M
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ a • (mk (R ∙ a * b)) x = 0

Tactic:
· 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.Nakayama

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
N N' : Submodule R M
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hmaple : map (I • N).mkQ N ≤ map (I • N).mkQ N'
⊢ Monotone (comap (I • N).mkQ)

Tactic:
apply Submodule.comap_mono

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ I • ⊤ ⊔ f.range = ⊤

Tactic:
← Submodule.map_mkQ_eq_top,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
I : Ideal R
Ile : I ≤ ⊥.jacobson
surj : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
⊢ Submodule.map (I • ⊤).mkQ f.range = ⊤
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp.refine_1
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
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ single R i '' ↑(F.N i) ⊆ ⋃ i, ⋃ (_ : i ≤ m), single R i '' ↑(F.N i)

Tactic:
refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_

Goal state after:
case mp.refine_1
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
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_1
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
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ ↥I₁ →ₗ[R] ↥I₂

pp: case refine_2
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
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ Submodule.restrictScalars R (I₁ • ⊤) ≤ Submodule.comap ?refine_1 (Submodule.restrictScalars R (I₂ • ⊤))

Tactic:
· exact f.toLinearMap.restrict (p := I₁.restrictScalars R) (q := I₂.restrictScalars R) h

Goal state after:
case refine_2
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
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ Submodule.restrictScalars R (I₁ • ⊤) ≤
    Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))
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 R (maximalIdeal R)).exists_span_set_card_eq_spanRank
    have hs_span' : Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ := by
      rw [← Submodule.restrictScalars_eq_top_iff R,
        Submodule.restrictScalars_span R (ResidueField R) Ideal.Quotient.mk_surjective,
        ← Submodule.map_span, hs_span, Submodule.map_top, Ideal.toCotangent_range]
    rw [← hs_card, ← hs_span']
    grw [Submodule.spanRank_span_le_card, Cardinal.mk_image_le]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
⊢ ∀ {M N : Type v} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] [inst_2 : Module R M] [inst_3 : Module R N]
    (f : M →ₗ[R] N) (g : ↑P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g

Tactic:
intro _

Goal state after:
R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
M✝ : Type v
⊢ ∀ {N : Type v} [inst : AddCommGroup M✝] [inst_1 : AddCommGroup N] [inst_2 : Module R M✝] [inst_3 : Module R N]
    (f : M✝ →ₗ[R] N) (g : ↑P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    (succ
        { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
          X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
          g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).fst

Tactic:
rw [← mk_congr_succ_X₃ succ
      (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)]
    rfl

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cone F
hs : (i : ι) → IsLimit ((eval C c i).mapCone s)
t : Cone F
m : t.pt ⟶ s.pt
hm : ∀ (j : J), m ≫ s.π.app j = t.π.app j
i : ι
j : J
⊢ m.f i ≫ (s.π.app j).f i = (t.π.app j).f i

Tactic:
simp only [← comp_f, hm]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
m : s.pt ⟶ t.pt
hm : ∀ (j : J), s.ι.app j ≫ m = t.ι.app j
i : ι
j : J
⊢ (s.ι.app j).f i ≫ m.f i = (t.ι.app j).f i

Tactic:
simp only [← comp_f, hm]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : ↥(ideal R S)
⊢ ∃ a, (D R S).tensorProductTo a = (ideal R S).toCotangent x

Tactic:
exact ⟨x, KaehlerDifferential.D_tensorProductTo x⟩

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
i j : A
⊢ (shiftFunctor C j).map ((shiftFunctor C i).map f) =
    (shiftFunctor C j).map ((shiftFunctor C i).map f) ≫
      (shiftFunctorComm C i j).hom.app Y ≫ (shiftFunctorComm C i j).inv.app Y

Tactic:
simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
C : Type u_2
D : Type u_3
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
inst✝¹ : Linear R C
inst✝ : Linear R D
ι : Type u_4
c : ComplexShape ι
X✝ Y✝ X Y : HomologicalComplex C c
x✝² x✝¹ : R
x✝ : X ⟶ Y
i✝ : ι
⊢ ((x✝² + x✝¹) • x✝).f i✝ = (x✝² • x✝ + x✝¹ • x✝).f i✝

Tactic:
apply add_smul

Goal state after:
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 : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.opcyclesIsoSc' i j k hi hk).inv ≫ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles

Tactic:
simp only [← cancel_epi (K.sc' i j k).pOpcycles, pOpcycles_opcyclesIsoSc'_inv_assoc,
    p_fromOpcycles, ShortComplex.p_fromOpcycles, shortComplexFunctor'_obj_g]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
⊢ f = g ↔ biprod.inl.f i ≫ f = biprod.inl.f i ≫ g ∧ biprod.inr.f i ≫ f = biprod.inr.f i ≫ g

Tactic:
refine ⟨by rintro rfl; simp, fun ⟨h₁, h₂⟩ ↦ ?_⟩
  rw [← cancel_epi (𝟙 _)]
  simp [← biprod_total_f, h₁, h₂]

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

Goal state before:
pp: J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
⊢ (MorphismProperty.pi W).IsInvertedBy (Functor.pi F)

Tactic:
intro _

Goal state after:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ : (j : J) → C j
⊢ ∀ ⦃Y : (j : J) → C j⦄ (f : X✝ ⟶ Y), MorphismProperty.pi W f → IsIso ((Functor.pi F).map f)
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F : C ⥤ D
⊢ W.isoClosure.IsInvertedBy F ↔ W.IsInvertedBy F

Tactic:
by
  constructor
  · intro h X Y f hf
    exact h _ (W.le_isoClosure _ hf)
  · intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
    simp only [Arrow.iso_w' e, F.map_comp]
    have := h _ hf'
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
⊢ (isomorphisms C).IsInvertedBy F

Tactic:
intro _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), isomorphisms C f → IsIso (F.map f)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
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)
x : B ⊗[A] Ω[A⁄R]
hx : x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker
⊢ x ∈ (kerCotangentToTensor R A B).range

Tactic:
obtain ⟨x, rfl⟩ := LinearMap.rTensor_surjective Ω[A⁄R] (g := Algebra.linearMap A B) h x

Goal state after:
case mpr
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)
x : A ⊗[A] Ω[A⁄R]
hx : (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B)) x ∈ Submodule.restrictScalars A (mapBaseChange R A B).ker
⊢ (LinearMap.rTensor Ω[A⁄R] (Algebra.linearMap A B)) x ∈ (kerCotangentToTensor R A B).range
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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
⊢ (φ ≫ inr φ).f j =
    (((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) +
        (prevD j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) +
      Hom.f 0 j

Tactic:
obtain ⟨i, hij⟩ := hc j
    rw [prevD_eq _ hij, dif_pos hij]
    by_cases hj : c.Rel j (c.next j)
    · simp only [comp_f, homotopyCofiber_d, zero_f, add_zero,
        inlX_d φ i j _ hij hj, dNext_eq _ hj, dif_pos hj,
        add_neg_cancel_left, inr_f]
    · rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d,
        inlX_d' _ _ _ _ hj, comp_f, inr_f]

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 k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap' h).f k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

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

Goal state after:
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 : ι
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

Tactic:
by
  by_cases hi : c.Rel i (c.next i)
  · simp [mapHomologicalComplexObjXIso, dif_pos hi, ← Functor.map_comp]
  · dsimp [mapHomologicalComplexObjXIso, XIso, inrX]
    simp [dif_neg hi]

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 : ι
C D E : HomologicalComplex V c
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy ((f.hom ≫ g.hom) ≫ g.inv ≫ f.inv) (𝟙 C)

Tactic:
by simpa using
    ((g.homotopyHomInvId.compRightId f.inv).compLeft f.hom).trans f.homotopyHomInvId

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ Φ.map f ≍ Quot.liftOn f (fun f ↦ Φ.map ((functor r).map f)) ⋯

Tactic:
refine Quot.inductionOn f fun _ ↦ ?_

Goal state after:
case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ Φ.map (Quot.mk (HomRel.CompClosure r) x✝) ≍
    (Quot.mk (HomRel.CompClosure r) x✝).liftOn (fun f ↦ Φ.map ((functor r).map f)) ⋯
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((Functor.commShiftIso (functor r) 0).inv.app X) ≫ (Functor.commShiftIso F 0).hom.app X =
    (Functor.CommShift.isoZero (lift r F hF) A).hom.app ((functor r).obj X)

Tactic:
(functor r).commShiftIso_zero,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((Functor.CommShift.isoZero (functor r) A).inv.app X) ≫ (Functor.commShiftIso F 0).hom.app X =
    (Functor.CommShift.isoZero (lift r F hF) A).hom.app ((functor r).obj X)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
⊢ δ n m (γ.shift a) = a.negOnePow • (δ n m γ).shift a

Tactic:
ext p q hpq
    dsimp
    simp only [shift_v', shiftFunctor_obj_d',
      δ_v n m hnm _ p q hpq (q - 1) (p + 1) rfl rfl,
      δ_v n m hnm _ (p + a) (q + a) (by lia) (q - 1 + a) (p + 1 + a)
        (by lia) (by lia),
      smul_add, Linear.units_smul_comp, Linear.comp_units_smul, add_right_inj]
    rw [smul_comm]

Goal state after:
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'
⊢ (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a

Tactic:
by
  ext p q hpq
  simp only [rightShift_v _ a n hn' p q hpq (q + a) (by lia),
    leftShift_v _ a n' hn' p (q + a) (by lia) (p + a) (by lia), units_smul_v, shift_v']
  dsimp
  rw [id_comp, comp_id]

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₃ ↔ T.mor₂ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (rot_of_distTriang _ hT)).trans ?_

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
⊢ T.rotate.mor₁ = 0 ∧ T.rotate.mor₂ = 0 ↔ T.mor₂ = 0 ∧ T.mor₃ = 0
Module: Mathlib.CategoryTheory.PathCategory.Basic

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

Tactic:
intro _

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

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

Tactic:
induction f with
    | nil =>
      simp only [Category.comp_id]
      apply Functor.map_id
    | cons p f' ih =>
      simp only [Category.comp_id, Category.id_comp] at ih ⊢
      -- Porting note: Had to do substitute `p.cons f'` and `f'.toPath` by their fully qualified
      -- versions in this `have` clause (elsewhere too).
      have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
        convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')
      rw [this, ih]

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.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap S.f i ≫ HomologicalComplex.homologyMap S.g i = 0

Tactic:
← HomologicalComplex.homologyMap_comp,

Goal state after:
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.ShortExact
i j : ι
hij : c.Rel i j
⊢ HomologicalComplex.homologyMap (S.f ≫ S.g) i = 0
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
X Y : C
w : X ⟶ Y
hw : W w
⊢ (Paths.of (LocQuiver W)).obj { obj := Y } ⟶ (Paths.of (LocQuiver W)).obj { obj := X }

Tactic:
dsimp; exact (Paths.of _).map (Sum.inr ⟨w, hw⟩)

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

Goal state before:
pp: case inl
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 : LocQuiver W
f : X.obj ⟶ Y.obj
⊢ G.obj X.obj ⟶ G.obj Y.obj

Tactic:
exact G.map f

Goal state after: