mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : ↑{p | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
  { toFun := fun x ↦ { asIdeal := ↑x, isPrime := ⋯ }, invFun := fun x ↦ ⟨x.asIdeal, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }
⊢ ↑(minimalPrimes R) ≃o (↑(irreducibleComponents (PrimeSpectrum R)))ᵒᵈ

Tactic:
rw [irreducibleComponents_eq_maximals_closed]

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
e : ↑{p | p.IsPrime ∧ ⊥ ≤ p} ≃o PrimeSpectrum R :=
  { toFun := fun x ↦ { asIdeal := ↑x, isPrime := ⋯ }, invFun := fun x ↦ ⟨x.asIdeal, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
    map_rel_iff' := ⋯ }
⊢ ↑(minimalPrimes R) ≃o (↑{s | Maximal (fun x ↦ IsClosed x ∧ IsIrreducible x) s})ᵒᵈ
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
h0 : {a | orderOf a = d} = ∅
⊢ ∑ m ∈ c.divisors.erase d, #{a | orderOf a = m} ≤ ∑ m ∈ c.divisors.erase d, φ m

Tactic:
gcongr with m hm
      have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
      obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
      · simp [h1]
      · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]

Goal state after:
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg : g ∈ primaryComponent G p
hg' : g ∈ primaryComponent G p'
⊢ g = 1

Tactic:
rw [mem_primaryComponent_iff_orderOf] at hg hg'
    obtain ⟨_ | n, hn⟩ := hg
    · rwa [pow_zero, orderOf_eq_one_iff] at hn
    · obtain ⟨_, hn'⟩ := hg'
      exact absurd (eq_of_prime_pow_eq hp.out.prime hp'.out.prime n.succ_pos (hn ▸ hn')) hne

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
⊢ (↑P).Characteristic

Tactic:
refine Subgroup.characteristic_iff_map_eq.mpr fun ϕ ↦ ?_

Goal state after:
G : Type u
inst✝¹ : Group G
p : ℕ
inst✝ : Subsingleton (Sylow p G)
P : Sylow p G
ϕ : G ≃* G
⊢ Subgroup.map ϕ.toMonoidHom ↑P = ↑P
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
I J : Ideal R
hIJ : I = J
x y : ↥J
⊢ (I.toCotangent ∘ₗ ↑(LinearEquiv.ofEq J I ⋯)) (x * y) = 0

Tactic:
by
    simp [toCotangent_eq_zero, hIJ, sq, mul_mem_mul]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ (Submodule.subtype (maximalIdeal R)) x = maximalIdeal R) ↔ ∃ a, maximalIdeal R = R ∙ a

Tactic:
eq_comm (a := maximalIdeal R)

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, R ∙ (Submodule.subtype (maximalIdeal R)) x = maximalIdeal R) ↔ ∃ a, R ∙ a = maximalIdeal R
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg.zero
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
⊢ I ≤ I ^ 0

Tactic:
simp [H.pow_succ_eq]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg.succ
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
H : IsIdempotentElem I
h✝ : ¬I = ⊤
n : ℕ
⊢ I ≤ I ^ (n + 1)

Tactic:
simp [H.pow_succ_eq]

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
X✝ : Cᵒᵖ
hX✝ : Limits.IsInitial X✝
X : Cᵒᵖ
hX : Limits.IsInitial X
M N : PresheafOfModules R
f : M ⟶ N
Y Z : Cᵒᵖ
g : Y ⟶ Z
⊢ (forgetToPresheafModuleCatObj X hX M).map g ≫
      ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Z)), map_add' := ⋯, map_smul' := ⋯ } =
    ModuleCat.ofHom { toFun := ⇑(ConcreteCategory.hom (f.app Y)), map_add' := ⋯, map_smul' := ⋯ } ≫
      (forgetToPresheafModuleCatObj X hX N).map g

Tactic:
ext x
    exact naturality_apply f g x

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)

Tactic:
rw [← obj_η_app_assoc, ← Functor.map_comp]
  simp

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₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
inst✝ : IsIso f
j : ι
⊢ (inv f).f j = inv (f.f j)

Tactic:
by
  apply IsIso.eq_inv_of_inv_hom_id
  simp [← comp_f]

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩) = D a

Tactic:
refine (D.liftKaehlerDifferential_apply _).trans ?_

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D.tensorProductTo ↑⟨1 ⊗ₜ[R] a - a ⊗ₜ[R] 1, ⋯⟩ = D a
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) =
    (shiftComm X i j).hom ≫ (shiftFunctor C i).map ((shiftFunctor C j).map f) ≫ (shiftComm Y j i).hom

Tactic:
erw [← shiftComm_symm Y i j, ← ((shiftFunctorComm C i j).hom.naturality_assoc f)]
  dsimp
  simp only [Iso.hom_inv_id_app, Functor.comp_obj, Category.comp_id]

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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : Ω[S⁄R]
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential x) =
    x

Tactic:
obtain ⟨x, rfl⟩ := KaehlerDifferential.linearCombination_surjective R S x

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
x : S →₀ S
⊢ ((kerTotal R S).liftQ (linearCombination S ⇑(D R S)) ⋯).toFun
      ((derivationQuotKerTotal R S).liftKaehlerDifferential ((linearCombination S ⇑(D R S)) x)) =
    (linearCombination S ⇑(D R S)) x
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e_p
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ (x.sum fun i a ↦ a • (map R S A B) ((D R A) i)) = 0 ↔
    ((mapDomain (⇑(algebraMap A B)) x).sum fun a b ↦ (Algebra.linearMap A B) b • (D S B) a) = 0

pp: case e_p
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (a : B), 0 • (D S B) a = 0

Tactic:
Finsupp.sum_mapDomain_index

Goal state after:
case e_p
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ (x.sum fun i a ↦ a • (map R S A B) ((D R A) i)) = 0 ↔
    (x.sum fun a m ↦ (Algebra.linearMap A B) m • (D S B) ((algebraMap A B) a)) = 0

case e_p.h_zero
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (b : B), (Algebra.linearMap A B) 0 • (D S B) b = 0

case e_p.h_add
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (b : B) (m₁ m₂ : A),
    (Algebra.linearMap A B) (m₁ + m₂) • (D S B) b =
      (Algebra.linearMap A B) m₁ • (D S B) b + (Algebra.linearMap A B) m₂ • (D S B) b

case e_p
R : Type u
S : Type v
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing S
inst✝⁹ : Algebra R S
A : Type u_2
B : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra A B
inst✝⁴ : Algebra S B
inst✝³ : Algebra R B
inst✝² : IsScalarTower R A B
inst✝¹ : IsScalarTower R S B
inst✝ : SMulCommClass S A B
x : A →₀ A
⊢ ∀ (a : B), 0 • (D S B) a = 0
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
inst✝ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
⊢ IsIso ((F ⋙ G).map f)

Tactic:
have := hF f hf

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
inst✝ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
hF : W.IsInvertedBy F
G : C₂ ⥤ C₃
X Y : C₁
f : X ⟶ Y
hf : W f
this : IsIso (F.map f)
⊢ IsIso ((F ⋙ G).map f)
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
i j : ι
hij : c.Rel i j
inst✝ : HasBinaryBiproduct (F.X j) (G.X i)
⊢ X φ i = (F.X j ⊞ G.X i)

Tactic:
by
    obtain rfl := c.next_eq' hij
    apply dif_pos hij

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₃ n₁₂ n₂₃ n₁₂₃ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₁₂ : n₁ + n₂ = n₁₂
h₂₃ : n₂ + n₃ = n₂₃
h₁₂₃ : n₁ + n₂ + n₃ = n₁₂₃
⊢ (z₁.comp z₂ h₁₂).comp z₃ ⋯ = z₁.comp (z₂.comp z₃ h₂₃) ⋯

Tactic:
by
  subst h₁₂ h₂₃ h₁₂₃
  ext p q hpq
  rw [comp_v _ _ rfl p (p + n₁ + n₂) q (add_assoc _ _ _).symm (by lia),
    comp_v z₁ z₂ rfl p (p + n₁) (p + n₁ + n₂) (by lia) (by lia),
    comp_v z₁ (z₂.comp z₃ rfl) (add_assoc n₁ n₂ n₃).symm p (p + n₁) q (by lia) (by lia),
    comp_v z₂ z₃ rfl (p + n₁) (p + n₁ + n₂) q (by lia) (by lia), assoc]

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

Goal state before:
pp: case neg
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
hc : ∀ (j : ι), ∃ i, c.Rel i j
i j : ι
hij : ¬c.Rel j i
⊢ (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j

Tactic:
· simp only [Homotopy.zero _ _ _ hij, zero_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  (inl φ).comp (Cochain.ofHom f₁) ⋯ = δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + (inl φ).comp (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ Cochain.ofHom f₁ = δ (-1) 0 (descCochain φ γ₁ γ₂ descHomotopy._proof_1) + Cochain.ofHom f₂

Tactic:
simp only [Cochain.ofHom_comp] at h₂

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v, u_1} C
inst✝³ : Category.{v', u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  (inl φ).comp (Cochain.ofHom f₁) ⋯ = δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + (inl φ).comp (Cochain.ofHom f₂) ⋯
h₂ : (Cochain.ofHom (inr φ)).comp (Cochain.ofHom f₁) ⋯ = δ (-1) 0 γ₂ + (Cochain.ofHom (inr φ)).comp (Cochain.ofHom f₂) ⋯
⊢ Cochain.ofHom f₁ = δ (-1) 0 (descCochain φ γ₁ γ₂ descHomotopy._proof_1) + Cochain.ofHom f₂
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_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.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
i : (quotient V c).obj C ≅ (quotient V c).obj D
⊢ (quotient V c).map (Quot.out i.hom ≫ Quot.out i.inv) = (quotient V c).map (𝟙 C)

Tactic:
by rw [quotient_map_out_comp_out, i.hom_inv_id, (quotient V c).map_id]

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 ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn' : n' + a = n
⊢ (γ.rightUnshift n hn').rightShift a n' hn' = γ

Tactic:
by
  ext p q hpq
  simp only [(γ.rightUnshift n hn').rightShift_v a n' hn' p q hpq (p + n) rfl,
    γ.rightUnshift_v n hn' p (p + n) rfl q hpq,
    shiftFunctorObjXIso, assoc, Iso.hom_inv_id, comp_id]

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 ℤ
a n' : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
⊢ δ n m (γ.rightUnshift n hn) = a.negOnePow • (δ n' m' γ).rightUnshift m hm'

Tactic:
obtain ⟨γ', rfl⟩ := (rightShiftAddEquiv K L n a n' hn).surjective γ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' n : ℤ
hn : n' + a = n
m m' : ℤ
hm' : m' + a = m
γ' : Cochain K L n
⊢ δ n m (((rightShiftAddEquiv K L n a n' hn) γ').rightUnshift n hn) =
    a.negOnePow • (δ n' m' ((rightShiftAddEquiv K L n a n' hn) γ')).rightUnshift m hm'
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₃
⊢ T₁.invRotate.mor₁ ≫ a = (shiftFunctor C (-1)).map c ≫ T₂.invRotate.mor₁

Tactic:
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]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem : Triangle.mk inl snd 0 ∈ distinguishedTriangles
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
⊢ HasBinaryBiproduct X₁ X₃

Tactic:
refine ⟨⟨binaryBiproductData _ mem rfl inr inr_snd.symm fst ?_⟩⟩

Goal state after:
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
X₁ X₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem : Triangle.mk inl snd 0 ∈ distinguishedTriangles
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
fst : X₂ ⟶ X₁
hfst : 𝟙 X₂ - snd ≫ inr = fst ≫ inl
⊢ fst ≫ (Triangle.mk inl snd 0).mor₁ + (Triangle.mk inl snd 0).mor₂ ≫ inr = 𝟙 (Triangle.mk inl snd 0).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
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
h₁ : e.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
h₂ : Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
⊢ T₁ ≅ T₂

Tactic:
have h₄ := (shiftFunctorCompIsoId C (-1 : ℤ) 1 (by simp)).inv.naturality e₃.hom

Goal state after:
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
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
h₁ : e.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
h₂ : Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom = e.hom.hom₂
h₃ : T₁.invRotate.mor₃ ≫ (shiftFunctor C 1).map e.hom.hom₁ = e.hom.hom₃ ≫ T₂.invRotate.mor₃
h₄ :
  (𝟭 C).map e₃.hom ≫ (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₂.obj₃ =
    (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₁.obj₃ ≫
      (shiftFunctor C (-1) ⋙ shiftFunctor C 1).map e₃.hom
⊢ T₁ ≅ T₂
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ F.shiftIso mn a a'' ⋯ =
    isoWhiskerRight (shiftFunctorAdd' C m n mn hnm) (F.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (F.shift a) ≪≫
        (shiftFunctor C m).isoWhiskerLeft (F.shiftIso n a a' ha') ≪≫ F.shiftIso m a' a'' ha''

Tactic:
subst hnm
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

Goal state after:
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
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
· rintro X Y f
    dsimp [lift]
    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.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr.cons.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr ⟨g, hg⟩)))

Tactic:
apply hP₂

Goal state after: