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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
⊢ e * f = 0 ∧ e + f = 1 → (s = ↑(basicOpen f) ↔ s = zeroLocus {e})

Tactic:
intro ⟨mul, add⟩

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
e f : R
mul : e * f = 0
add : e + f = 1
⊢ s = ↑(basicOpen f) ↔ s = zeroLocus {e}
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x✝¹ x✝ : { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 }
x : R × R
hx : x.1 * x.2 = 0 ∧ x.1 + x.2 = 1
y : R × R
hy : y.1 * y.2 = 0 ∧ y.1 + y.2 = 1
eq :
  (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨x, hx⟩ =
    (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) ⟨y, hy⟩
⊢ (↑⟨x, hx⟩).1 = (↑⟨y, hy⟩).1

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s

Tactic:
· exact basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
          (IsIdempotentElem.of_mul_add hy.1 hy.2).1 <| SetLike.ext' (congr_arg (·.1) eq)

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Clopens (PrimeSpectrum R)
⊢ ∃ a, (fun e ↦ { carrier := ↑(basicOpen (↑e).1), isClopen' := ⋯ }) a = s
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : (Nat.card ↥H).Coprime H.index
⊢ P ≤ H ∨ Disjoint H P

Tactic:
by_cases h1 : Nat.card H = 0
  · rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop
    rw [h_cop]
    exact Or.inl le_top
  by_cases h2 : H.index = 0
  · rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop
    rw [h_cop]
    exact Or.inr disjoint_bot_left
  have : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← H.card_mul_index]
    exact mul_ne_zero h1 h2
  have h3 : (Nat.card H).Coprime (Nat.card P) ∨ H.index.Coprime (Nat.card P) := by
    obtain ⟨k, hk⟩ := hP.exists_card_eq
    refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_
    contrapose! h_cop
    exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩
  refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)
  · rw [← Subgroup.relIndex_eq_one]
    exact Nat.eq_one_of_dvd_coprimes h4 (H.relIndex_dvd_index_of_normal P)
      (Subgroup.relIndex_dvd_card H P)
  · exact Subgroup.disjoint_of_coprime_natCard h4

Goal state after:
Module: Mathlib.Algebra.Module.ZMod

Goal state before:
pp: n : ℕ
M : Type u_1
M₁ : Type u_2
inst✝¹ : NeZero n
inst✝ : AddCommMonoid M
h : ∀ (x : M), n • x = 0
c : ℕ
x : M
this : (c % n + c / n * n) • x = c • x
⊢ (c % n) • x = c • x

Tactic:
rwa [add_nsmul, mul_nsmul, h, add_zero] at this

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

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic G'
f : G →* G'
hf : f.ker ≤ center G
a b : G
x : G'
y : G
hxy : f y = x
hx : ∀ (a : ↥f.range), a ∈ zpowers ⟨x, ⋯⟩
m : ℤ
hm✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) m = ⟨f a, ⋯⟩
n : ℤ
hn✝ : (fun x_1 ↦ ⟨x, ⋯⟩ ^ x_1) n = ⟨f b, ⋯⟩
hm : x ^ m = f a
hn : x ^ n = f b
ha : y ^ (-m) * a ∈ center G
⊢ y ^ (-n) * b ∈ f.ker

Tactic:
by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel]

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

Goal state before:
pp: case h.left
G : Type u_2
inst✝¹ : CommGroup G
inst✝ : IsSimpleGroup G
g : G
hg : zpowers g = ⊤
⊢ Nat.Prime (Nat.card G)

Tactic:
exact IsSimpleGroup.prime_card

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
x : G
⊢ (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) (map N.subtype ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ ↑(map N.subtype ↑P)

Tactic:
map_map,

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
x : G
⊢ (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈
      map ((MulEquiv.toMonoidHom (MulAut.conj (↑n * g))).comp N.subtype) ↑P ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ ↑(map N.subtype ↑P)
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: case refine_1
ι : Type u_1
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a : α
x✝ : ↑(Iic a)
s : Set α
hs : ∀ x ∈ s, IsCompactElement x
hx✝ : sSup s ≤ a
hx : ∀ b ∈ s, b ≤ a
f : ↑s → ↑(Iic a) := fun y ↦ ⟨↑y, ⋯⟩
⊢ ∀ x ∈ range f, IsCompactElement x

Tactic:
rintro - ⟨⟨y, hy⟩, hy', rfl⟩
    exact isCompactElement (hs _ hy)

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

Goal state before:
pp: case refine_1
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ 1 - 1 ∈ I

Tactic:
rw [sub_self]

Goal state after:
case refine_1
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
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ 0 ∈ I
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ f ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))

Tactic:
rw [← f.ofCoeff_coeff, ← f.coeff.sum_single, ofCoeff_finsuppSum]

Goal state after:
case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ (f.coeff.sum fun i n ↦ { coeff := Finsupp.single i n }) ∈ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
⊢ α - β = 0

Tactic:
have : ⊤ ≤ LinearMap.ker (α - β).hom := by
    rw [← KaehlerDifferential.span_range_derivation, Submodule.span_le]
    rintro _ ⟨y, rfl⟩
    rw [SetLike.mem_coe, LinearMap.mem_ker, ModuleCat.hom_sub, LinearMap.sub_apply, sub_eq_zero]
    apply h

Goal state after:
A B : CommRingCat
f : A ⟶ B
M : ModuleCat ↑B
α β : KaehlerDifferential f ⟶ M
h : ∀ (b : ↑B), (ConcreteCategory.hom α) (d b) = (ConcreteCategory.hom β) (d b)
this : ⊤ ≤ (ModuleCat.Hom.hom (α - β)).ker
⊢ α - β = 0
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mp
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
⊢ F.submodule.FG → ∃ n₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))

pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ (∃ n₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))) → F.submodule.FG

Tactic:
· rintro H
    refine H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_
    · intro n m e
      rw [Submodule.span_le, Set.iUnion₂_subset_iff]
      intro i hi
      refine Set.Subset.trans ?_ Submodule.subset_span
      refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
      exact hi.trans e
    · dsimp
      rw [← Submodule.span_iUnion, ← submodule_span_single]
      simp [Set.biUnion_le_eq_iUnion]

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

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
hs_span' : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤
⊢ ⊤.spanRank ≤ ⊤.spanRank

Tactic:
rw [← hs_card, ← hs_span']

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
hs_span' : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤
⊢ (Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s)).spanRank ≤ Cardinal.mk ↑s
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
⊢ h₁ = h₂

Tactic:
suffices ∀ {M' : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)}
      (d' : M'.Derivation φ), h₁.desc d' = h₂.desc d' by
        cases h₁
        cases h₂
        simp only [Universal.mk.injEq]
        ext : 2
        apply this
    intro M' d'
    apply h₁.postcomp_injective
    simp

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
⊢ 1 ⊗ₜ[R] 1 - 1 ⊗ₜ[R] 1 = 0

Tactic:
rw [sub_self]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ F.map (d (n + 1)) ≫ F.map (d n) = 0

Tactic:
rw [← F.map_comp, sq n, Functor.map_zero]

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
i i' : ι
x✝ : c.Rel i i'
j : J
eq :
  ∀ (k : ι) (j : J),
    ((eval C c k).mapCocone s).ι.app j ≫ (hs k).desc ((eval C c k).mapCocone t) = ((eval C c k).mapCocone t).ι.app j
⊢ ((eval C c i).mapCocone s).ι.app j ≫ (hs i).desc ((eval C c i).mapCocone t) ≫ t.pt.d i i' =
    ((eval C c i).mapCocone s).ι.app j ≫ s.pt.d i i' ≫ (hs i').desc ((eval C c i').mapCocone t)

Tactic:
simp only [Functor.mapCocone_ι_app, eval_map] at eq

Goal state after:
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
i i' : ι
x✝ : c.Rel i i'
j : J
eq : ∀ (k : ι) (j : J), (s.ι.app j).f k ≫ (hs k).desc ((eval C c k).mapCocone t) = (t.ι.app j).f k
⊢ ((eval C c i).mapCocone s).ι.app j ≫ (hs i).desc ((eval C c i).mapCocone t) ≫ t.pt.d i i' =
    ((eval C c i).mapCocone s).ι.app j ≫ s.pt.d i i' ≫ (hs i').desc ((eval C c i').mapCocone t)
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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun i j hij ↦ hom i j hij ≫ g.f j

Tactic:
rw [nullHomotopicMap', nullHomotopicMap_comp]

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
⊢ (nullHomotopicMap fun i j ↦ (dite (c.Rel j i) (hom i j) fun x ↦ 0) ≫ g.f j) =
    nullHomotopicMap' fun i j hij ↦ hom i j hij ≫ g.f j
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 φ
K : CochainComplex C ℤ
d e f : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = f
⊢ (Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0

Tactic:
obtain rfl : e = f := by lia

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
d e : ℤ
γ : Cochain F K d
he : 1 + d = e
hf : 0 + e = e
⊢ (Cochain.ofHom (inr φ)).comp ((↑(fst φ)).comp γ he) hf = 0
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 l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (nullHomotopicMap fun i j ↦ dite (c.Rel j i) (h i j) fun x ↦ 0).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]

Goal state after:
ι : 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 l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
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 φ
K : CochainComplex C ℤ
d : ℤ
γ : Cochain G K d
he : 0 + d = d
⊢ (Cochain.ofHom (inr φ)).comp ((snd φ).comp γ he) ⋯ = γ

Tactic:
rw [← Cochain.comp_assoc_of_first_is_zero_cochain, inr_snd, Cochain.id_comp]

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

Goal state before:
pp: case mpr
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
A : C
f g : A ⟶ (mappingCone φ).X i
⊢ f ≫ (↑(fst φ)).v i j hij = g ≫ (↑(fst φ)).v i j hij ∧ f ≫ (snd φ).v i i ⋯ = g ≫ (snd φ).v i i ⋯ → f = g

Tactic:
· rintro ⟨h₁, h₂⟩
    exact ext_to φ i j hij 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
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫
        (z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
          (n₂ + 1).negOnePow • G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯) +
      n₂.negOnePow • (δ n₁ (n₁ + 1) z₁).v p (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯

Tactic:
δ_v n₁ (n₁ + 1) rfl z₁ p (p + n₁ + 1) (by lia) (p + n₁) _ (by lia) rfl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
p q : ℤ
hpq : p + (n₁ + n₂ + 1) = q
⊢ (z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q +
      (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ =
    z₁.v p (p + n₁) ⋯ ≫
        (z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q +
          (n₂ + 1).negOnePow • G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯) +
      n₂.negOnePow •
        (z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) +
            (n₁ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯) ≫
          z₂.v (p + n₁ + 1) q ⋯
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ f.f j =
    (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

Tactic:
apply ext_from_X φ _ _ hj

Goal state after:
case pos.h₁
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hj ≫ f.f j =
    inlX φ (c.next j) j hj ≫
      (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

case pos.h₂
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inrX φ j ≫ f.f j =
    inrX φ j ≫
      (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j
Module: Mathlib.CategoryTheory.Quotient

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

Tactic:
exact τ.naturality f

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 ι
⊢ ∀ ⦃X Y : HomologicalComplex V c⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y),
    homotopic V c f₁ f₂ → homotopic V c g₁ g₂ → homotopic V c (f₁ + g₁) (f₂ + g₂)

Tactic:
rintro _ _ _ _ _ _ ⟨h⟩ ⟨h'⟩
    exact ⟨Homotopy.add h h'⟩

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
⊢ (γ₁ + γ₂).rightShift a n' hn' = γ₁.rightShift a n' hn' + γ₂.rightShift a n' hn'

Tactic:
by
  ext p q hpq
  dsimp
  simp only [rightShift_v _ a n' hn' p q hpq _ rfl, add_v, add_comp]

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' = γ₁.leftShift a n' hn' + γ₂.leftShift a n' hn'

Tactic:
by
  ext p q hpq
  dsimp
  simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), add_v, comp_add, smul_add]

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
inst✝⁹ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁸ : AddMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : HasShift C A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift C B
inst✝² : HasShift D B
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
⊢ ((shiftFunctor C 0).associator F G).symm ≪≫
      isoWhiskerRight (commShiftIso F 0) G ≪≫
        F.associator (shiftFunctor D 0) G ≪≫
          F.isoWhiskerLeft (commShiftIso G 0) ≪≫ (F.associator G (shiftFunctor E 0)).symm =
    isoZero (F ⋙ G) A

Tactic:
by
    ext X
    dsimp
    simp only [id_comp, comp_id, commShiftIso_zero, isoZero_hom_app, ← Functor.map_comp_assoc,
      assoc, Iso.inv_hom_id_app, id_obj, comp_map, comp_obj]

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map ((i a).inv.app X) ≫
          (s b).map ((i a).hom.app X) ≫
            (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
rw [← Functor.map_comp_assoc, Iso.inv_hom_id_app]

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X