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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf✝ : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
span_eq : Ideal.span (Set.range f) = ⊤
hf : ∀ (a : ↑(Set.range f)), ↑(basicOpen ↑a) = {e.symm a}
a b : ↑(Set.range f)
⊢ (IsLocalization.Away.awayToAwayRight ↑a ↑b) ((algE a) (x (e.symm a))) =
    (IsLocalization.Away.awayToAwayLeft ↑b ↑a) ((algE b) (x (e.symm b)))

Tactic:
obtain rfl | ne := eq_or_ne a b; · rfl
      have nil : IsNilpotent (a * b : R) := (basicOpen_eq_bot_iff _).mp <| by
        simp_rw [basicOpen_mul, SetLike.ext'_iff, TopologicalSpace.Opens.coe_inf, hf]
        exact bot_unique (fun _ ⟨ha, hb⟩ ↦ ne <| e.symm.injective (ha.symm.trans hb))
      apply (IsLocalization.subsingleton (M := .powers (a * b : R)) nil).elim

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s✝ : Set (PrimeSpectrum R)
x✝ : ∃ t, (zeroLocus ↑t)ᶜ = s✝
s : Finset R
e : (zeroLocus ↑s)ᶜ = s✝
⊢ (zeroLocus ↑(Ideal.span ↑s))ᶜ = s✝

Tactic:
by simpa using e

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
⊢ ∃ n, Nat.card G ∣ p ^ n

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Goal state after:
case inl
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup 0 G
⊢ ∃ n, Nat.card G ∣ 0 ^ n

case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
⊢ ∃ n, Nat.card G ∣ p ^ n
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
hqp : Nat.Prime q
hqdvd : q ∣ Nat.card G
right✝ : Nat.card G ≠ 0
⊢ q ∈ p.primeFactors

Tactic:
have ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q (hp := ⟨hqp⟩) hqdvd

Goal state after:
case inr
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
h : IsPGroup p G
hp : p ≠ 0
q : ℕ
hq : q ∈ (Nat.card G).primeFactors
hqp : Nat.Prime q
hqdvd : q ∣ Nat.card G
right✝ : Nat.card G ≠ 0
g : G
hg : orderOf g = q
⊢ q ∈ p.primeFactors
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑(Ideal.span ↑s))ᶜ

Tactic:
rw [zeroLocus_span]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Finset R
⊢ IsRetrocompact (zeroLocus ↑s)ᶜ
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g.1 ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1.1

Tactic:
Prod.fst_one,

Goal state after:
case refine_1.fst
M₁ : Type u_1
M₂ : Type u_2
inst✝¹ : Monoid M₁
inst✝ : Monoid M₂
g : M₁ × M₂
⊢ g.1 ^ GCDMonoid.lcm (exponent M₁) (exponent M₂) = 1
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsMulTorsion G
h : H
⊢ IsOfFinOrder h

Tactic:
by
  obtain ⟨g, rfl⟩ := hf h
  exact f.isOfFinOrder (tG g)

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝¹ : Finite α
this✝ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this : orderOf g ∈ (p ^ 2).divisors
⊢ orderOf g = p

Tactic:
have : ∃ a < 3, p ^ a = orderOf g := by
    simpa [Nat.divisors_prime_pow hp 2] using this

Goal state after:
α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝² : Finite α
this✝¹ : Nontrivial α
h_cyc : ¬IsCyclic α
g : α
hg : g ≠ 1
this✝ : orderOf g ∈ (p ^ 2).divisors
this : ∃ a < 3, p ^ a = orderOf g
⊢ orderOf g = p
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ (powMonoidHom d).range.index = (Nat.card G).gcd d

Tactic:
Subgroup.index_range,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
⊢ Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
⊢ g ^ Classical.choose ⋯ = g ^ Classical.choose ⋯ * g ^ Classical.choose ⋯

Tactic:
simp only [fun x ↦ Classical.choose_spec <| mem_zpowers_iff.mp <| hg x]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
⊢ Nat.card ↥(normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]

Tactic:
by
  have : H.subgroupOf (normalizer H) ≃ H := (subgroupOfEquivOfLe le_normalizer).toEquiv
  rw [card_eq_card_quotient_mul_card_subgroup H,
    card_eq_card_quotient_mul_card_subgroup (H.subgroupOf (normalizer H)), Nat.card_congr this,
    hH, pow_succ']
  exact (card_quotient_normalizer_modEq_card_quotient hH).mul_right' _

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}
⊢ ⨆ i, ⨆ (i_1 : i ∈ s), sSup (t i i_1) = ⨆ i ∈ s, f i

Tactic:
biSup_congr' ht

Goal state after:
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
⊢ IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨I, ⟨coatom⟩, ⟨equiv⟩⟩ ↦ ?_⟩
  · have := IsSimpleModule.nontrivial R M
    have ⟨m, hm⟩ := exists_ne (0 : M)
    exact ⟨_, ker_toSpanSingleton_isMaximal R hm,
      ⟨(LinearMap.quotKerEquivOfSurjective _ <| toSpanSingleton_surjective R hm).symm⟩⟩
  · convert! congr equiv; rwa [isSimpleModule_iff_isCoatom]

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

Goal state before:
pp: R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ p ∈ annihilator R[X] (AEval R M a) ↔ p ∈ RingHom.ker (aeval a)

Tactic:
simp_rw [mem_annihilator, RingHom.mem_ker]

Goal state after:
R : Type u_3
A : Type u_1
M : Type u_2
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
inst✝ : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : AEval R M a), p • m = 0) ↔ (aeval a) p = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion ℕ M
x : M
⊢ IsOfFinAddOrder x

Tactic:
isOfFinAddOrder_iff_nsmul_eq_zero

Goal state after:
case refine_2
M : Type u_2
inst✝ : AddCommMonoid M
h : IsTorsion ℕ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion ℤ M
x : M
⊢ IsOfFinAddOrder x

Tactic:
isOfFinAddOrder_iff_nsmul_eq_zero

Goal state after:
case refine_2
M : Type u_2
inst✝ : AddCommGroup M
h : IsTorsion ℤ M
x : M
⊢ ∃ n, 0 < n ∧ n • x = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ F.N (n + 1 + n₀) ≤ F'.N (n + 1)

Tactic:
add_right_comm,

Goal state after:
case h.succ
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
n : ℕ
hn : F.N (n + n₀) ≤ F'.N n
⊢ F.N (n + n₀ + 1) ≤ F'.N (n + 1)
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ Module.rank (ResidueField R) (CotangentSpace R) = Submodule.spanRank (maximalIdeal R)

Tactic:
by
  rw [Submodule.rank_eq_spanRank_of_free, ← Submodule.spanRank_top (maximalIdeal R)]
  apply le_antisymm
  · 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]
  · 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.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
⊢ ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)} (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d'

Tactic:
intro M' d'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
h₁ h₂ : d.Universal
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation φ
⊢ h₁.desc d' = h₂.desc d'
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
⊢ Derivation.postcomp (derivation' φ') { app := fun X ↦ (d'.app X).desc, naturality := ⋯ } = d'

Tactic:
ext X b

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
d' : M'.Derivation' φ'
X : Dᵒᵖ
b : ↑(R.obj X)
⊢ (Derivation.postcomp (derivation' φ') { app := fun X ↦ (d'.app X).desc, naturality := ⋯ }).d b = d'.d b
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : S →ₐ[R] S ⊗[R] S ⧸ ideal R S ^ 2
x : S
e₁ :
  (TensorProduct.lmul' R).kerSquareLift (f x) =
    (quotientCotangentIdealRingEquiv R S) ((Ideal.Quotient.mk (ideal R S).cotangentIdeal) (f x))
e₂ :
  x =
    (quotientCotangentIdealRingEquiv R S)
      ((IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x)
⊢ ((TensorProduct.lmul' R).kerSquareLift.comp f) x = (AlgHom.id R S) x →
    ((Ideal.Quotient.mkₐ R (ideal R S).cotangentIdeal).comp f) x =
      (IsScalarTower.toAlgHom R S ((S ⊗[R] S ⧸ ideal R S ^ 2) ⧸ (ideal R S).cotangentIdeal)) x

Tactic:
intro e; apply (KaehlerDifferential.quotientCotangentIdealRingEquiv R S).injective
    exact e₁.symm.trans (e.trans e₂)

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 L M : HomologicalComplex C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst✝ : K.HasHomology i
⊢ Mono (K.homologyι i)

Tactic:
dsimp only [homologyι]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : R
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (k • z₂) h = k • z₁.comp z₂ h

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), smul_v, Linear.comp_smul]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : q + 1 = p
⊢ (inl φ).v p q ⋯ ≫ (↑(fst φ)).v q p hpq = 𝟙 (F.X p)

Tactic:
simp [inl, fst]

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

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

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

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m x✝⁵ x✝⁴ x✝³ : ℤ
x✝² : (ComplexShape.up ℤ).Rel x✝⁵ x✝⁴
x✝¹ : (ComplexShape.up ℤ).Rel x✝⁴ x✝³
x✝ : ↑(AddCommGrpCat.of (Cochain F G x✝⁵))
p✝ q✝ : ℤ
hpq✝ : p✝ + x✝³ = q✝
⊢ Cochain.v
      ((AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁵ x✝⁴) ≫ AddCommGrpCat.ofHom ↑(δ_hom ℤ F G x✝⁴ x✝³)))
        x✝)
      p✝ q✝ hpq✝ =
    Cochain.v ((AddCommGrpCat.Hom.hom 0) x✝) p✝ q✝ hpq✝

Tactic:
simp [δ_δ]

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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

Tactic:
exact homotopyCofiber.ext_from_X' (biprod.lift (𝟙 K) (-𝟙 K)) _ hi (inrX_nullHomotopy_f _ hc _)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
⊢ ((shiftFunctor C 0).isoWhiskerLeft e.symm ≪≫ commShiftIso F 0 ≪≫ isoWhiskerRight e (shiftFunctor D 0)).hom.app X =
    (isoZero G A).hom.app X

Tactic:
simp [F.commShiftIso_zero, ← NatTrans.naturality]

Goal state after:
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
⊢ Epi T.mor₂ → T.mor₃ = 0

Tactic:
· intro
    rw [← cancel_epi T.mor₂, comp_distTriang_mor_zero₂₃ _ hT, comp_zero]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ -(σ p).s ≫ S.g.f p ≫ S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) +
      S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r ≫ S.f.f (p + 2) =
    0

Tactic:
reassoc_of% (s_g p),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ -S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) +
      S.X₃.d p (p + 1) ≫ (σ (p + 1)).s ≫ S.X₂.d (p + 1) (p + 2) ≫ (σ (p + 2)).r ≫ S.f.f (p + 2) =
    0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this : IsIso φ.hom₁
⊢ ∃ e', e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom

Tactic:
have : IsIso φ.hom₂ := by dsimp [φ]; infer_instance

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 : Arrow.mk T₁.mor₁ ≅ Arrow.mk T₂.mor₁
φ : T₁ ⟶ T₂ := completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ (Arrow.Hom.left e.hom) (Arrow.Hom.right e.hom) ⋯
this✝ : IsIso φ.hom₁
this : IsIso φ.hom₂
⊢ ∃ e', e'.hom.hom₁ = Arrow.Hom.left e.hom ∧ e'.hom.hom₂ = Arrow.Hom.right e.hom
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
⊢ opcyclesMap S.f i ≫ opcyclesMap S.g i = 0

Tactic:
← opcyclesMap_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.Exact
inst✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ opcyclesMap (S.f ≫ S.g) i = 0
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''
X : C
⊢ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X =
    (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X) ≫ (F.shiftIso mn a a'' ⋯).hom.app X

Tactic:
by
  rw [F.shiftIso_add'_hom_app n m mn hnm a a' a'' ha' ha'', ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.map_id, id_comp]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_4
inst✝¹ : Category.{v_4, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ L'.IsLocalization W

Tactic:
by
  have h : W.IsInvertedBy L' := by
    rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]
    exact MorphismProperty.IsInvertedBy.of_comp W L (Localization.inverts L W) eq.functor
  let F₁ := Localization.Construction.lift L (Localization.inverts L W)
  let F₂ := Localization.Construction.lift L' h
  let e' : F₁ ⋙ eq.functor ≅ F₂ := liftNatIso W.Q W (L ⋙ eq.functor) L' _ _ e
  exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso e' }

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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
⊢ φ.add.map F hF = φ.fst.map F hF + φ.snd.map F hF

Tactic:
have := hF φ.s φ.hs
  rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]

Goal state after: