mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ equivMatrix I ≤ equivMatrix J ↔ I ≤ J

Tactic:
by
    simp only [equivMatrix_apply]
    constructor
    · intro le x xI
      specialize @le (of fun _ _ => x) (by simp [xI])
      simpa using le
    · intro IJ M MI i j
      exact IJ <| MI i j

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α✝ β✝ : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α✝ → m β✝
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η : ApplicativeTransformation F✝ G✝
α β : Type u
f : α → F✝ β
x✝ : FreeMagma α
x : α
⊢ (fun {α} ↦ η.app α) (traverse f (pure x)) = traverse ((fun {α} ↦ η.app α) ∘ f) (pure x)

Tactic:
by simp only [traverse_pure, functor_norm, Function.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Mul β
f g : FreeSemigroup α →ₙ* β
h : ⇑f ∘ of = ⇑g ∘ of
x✝ : FreeSemigroup α
x : α
y : FreeSemigroup α
hx : f (of x) = g (of x)
hy : f y = g y
⊢ f (of x * y) = g (of x * y)

Tactic:
by simp only [map_mul, *]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
x✝ : FreeGroup α
L : List (α × Bool)
⊢ mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L

Tactic:
exact reduce.self

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ R[x], (algebraMap R S) p * y = (algebraMap R S) p * (-1 * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
refine
    ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩

Goal state after:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (R ∙ p)
φ : ℕ → R
hx : x ^ (Polynomial.map (algebraMap R S) f).natDegree = -∑ i, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ -1 * ∑ i, (algebraMap R S) (φ ↑i) * x ^ ↑i ∈ R[x]
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this : y ∣ x ^ p.natDegree
⊢ y ∣ 1

Tactic:
← one_pow

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this : y ∣ x ^ p.natDegree
⊢ y ∣ 1 ^ ?m.126

R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this : y ∣ x ^ p.natDegree
⊢ ℕ
Module: Mathlib.Algebra.Group.Action.Option

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b✝ : α
x✝ : Option α
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N α
a : M
b : N
x : Option α
⊢ (a • b) • x = a • b • x

Tactic:
cases x
    exacts [rfl, congr_arg some (smul_assoc _ _ _)]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : DecidableEq γ
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : SMulCommClass α β γ
s : Finset α
t : Finset β
u : Finset γ
⊢ ↑(s • t • u) = ↑(t • s • u)

Tactic:
simp_rw [coe_smul, smul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
⊢ comap φ M < K → K = ⊤

Tactic:
hK

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
K : Subgroup G
hK : comap φ M < K
⊢ K = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x : M
⊢ x ∈ s.saturation ↔ ∃ c, x * c ∈ s

Tactic:
mem_saturation_iff

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ False

Tactic:
suffices ¬ IsMulIndecomposable v t j from this (hst hj)

Goal state after:
case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ ¬IsMulIndecomposable v t j
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C

Tactic:
· intro _ X p hp
    rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
    exact
      ⟨Nonempty.intro
          { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
            isLimit := by
              apply Fork.IsLimit.mk'
              intro s
              refine ⟨s.ι ≫ e, ?_⟩
              constructor
              · simp [h₂, ← Limits.Fork.condition s]
              · intro m hm
                rw [Fork.ι_ofι] at hm
                rw [← hm]
                simp only [assoc, h₁]
                exact (comp_id m).symm }⟩

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → IsIdempotentComplete C
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Abelian D
⊢ IsIdempotentComplete D

Tactic:
by
  rw [isIdempotentComplete_iff_idempotents_have_kernels]
  intros
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc

Tactic:
simpa [S] using! hij

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (CosimplicialObject.const Cᵒᵖ).map f.unop.right.op ≫ (unop Y✝).rightOp.hom =
    (unop X✝).rightOp.hom ≫ (𝟭 (CosimplicialObject Cᵒᵖ)).map (NatTrans.rightOp f.unop.left)

Tactic:
by
        ext x
        dsimp
        simp_rw [← op_comp]
        congr 1
        exact (congr_app f.unop.w (op x)).symm

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
this : Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
⊢ X = Y

Tactic:
by
    ext
    simpa

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (X.map (section_ f).op)) ((ConcreteCategory.hom (X.map f.op)) x) = x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A

Tactic:
← Category.comp_id A.right

Goal state after:
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ Arrow.Hom.right A ≫ X.right.map (⦋0⦌.const ⦋0⦌ 0) = Arrow.Hom.right A ≫ 𝟙 (Augmented.toArrow.obj X).right
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (X.map (section_ f).op)) x.simplex = y.simplex

Tactic:
by simp [← hf, ← Functor.map_comp_apply, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ ⇑(ConcreteCategory.hom (f.app (op ⦋n⦌))) '' X.degenerate n ⊆ Y.degenerate n

Tactic:
by
  simpa using degenerate_le_preimage f n

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_3 _proof_1).op)) x) =
    x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_3 _proof_1).op)) x) =
    x

Tactic:
simp [← Functor.map_comp_apply, ← op_comp]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.δ i)) = face {i}ᶜ

Tactic:
exact ofSimplex_yonedaEquiv_δ i

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ ExtraDegeneracy.s f S n ≫ f.augmentedCechNerve.left.δ 0 = 𝟙 (f.augmentedCechNerve.left _⦋n⦌)

Tactic:
dsimp [SimplicialObject.δ, SimplexCategory.δ]
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j =
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
dsimp [mapBifunctorComp₁₂MapObjIso]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} C₃
inst✝⁴ : Category.{v_4, u_4} C₄
inst✝³ : Category.{v_5, u_5} C₁₂
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝² : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝¹ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
inst✝ : ((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (CofanMapObjFun.iso (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)).inv =
    ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
⊢ ((K.totalDesc fun p q hpq ↦
        (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) =
    𝟙 ((K.total (up ℤ)).X n')

Tactic:
ext
    dsimp
    simp only [ι_totalDesc_assoc, Category.assoc, ι_totalDesc, XXIsoOfEq_inv_ιTotal, comp_id]

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

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((shiftFunctor₂ C y).obj K).d₁ (up ℤ) p q n₁ ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    (y.negOnePow * (p * y).negOnePow) • K.d₁ (up ℤ) p (q + y) n₁'

Tactic:
((shiftFunctor₂ C y).obj K).d₁_eq _ rfl _ _ (by dsimp; lia),

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (((up ℤ).ε₁ (up ℤ) (up ℤ) (p, q) •
        (((shiftFunctor₂ C y).obj K).d p (p + 1)).f q ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯) ≫
      ((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n₁' ⋯) =
    (y.negOnePow * (p * y).negOnePow) • K.d₁ (up ℤ) p (q + y) n₁'
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n

Tactic:
choose n hn using p.prop_diag_obj

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : J → ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE (n j)
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n

Tactic:
choose n hn using p.prop_diag_obj

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : J → ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE (n j)
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : c.Rel i (c.next i)
⊢ (K.extendXIso e ⋯).hom ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv = (dNext (e.f i)) (extend.hom e h.hom)

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (K.extendXIso e ⋯).hom ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv = (dNext (e.f i)) (extend.hom e h.hom)

Tactic:
· have hi' : c'.Rel (e.f i) (e.f (c.next i)) := by rwa [e.rel_iff]
          simp [dNext_eq _ hi, dNext_eq _ hi', extend.hom_eq _ _ rfl rfl,
            extend_d_eq _ _ rfl rfl]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (K.extendXIso e ⋯).hom ≫ (dNext i) h.hom ≫ (L.extendXIso e ⋯).inv = (dNext (e.f i)) (extend.hom e h.hom)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'

Tactic:
· obtain ⟨i, rfl⟩ := hi'
    by_cases hj' : ∃ j, e.f j = j'
    · obtain ⟨j, rfl⟩ := hj'
      simp [extend_hom_eq _ e rfl rfl, ofExtend_hom]
    · exact (isZero_extend_X _ _ _ (by tauto)).eq_of_tgt _ _

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (h.ofExtend.extend e).hom i' j' = h.hom i' j'
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: 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.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero (homotopyCofiber.X (biprod.lift (𝟙 K.op) (-𝟙 K.op)) i)

Tactic:
refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ IsZero.op (h₂ _ hj))

Goal state after:
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.HasPathObject
i : α
h₁ : IsZero (K.X i)
h₂ : ∀ (j : α), c.Rel j i → IsZero (K.X j)
⊢ IsZero ((K.op ⊞ K.op).X i)
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
a b : ℤ
inst✝¹ : X.IsGE a
inst✝ : X.IsLE b
K : CochainComplex C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Q.obj K
⊢ K.IsGE a

Tactic:
rw [← isGE_Q_obj_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
a b : ℤ
inst✝¹ : X.IsGE a
inst✝ : X.IsLE b
K : CochainComplex C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Q.obj K
⊢ (Q.obj K).IsGE a
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
A : C
inst✝⁷ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁶ : HasBinaryCoproduct A A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : HasInitial C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).IsStableUnderCobaseChange
inst✝¹ : IsCofibrant A
inst✝ : P.IsGood
⊢ Cofibration P.i₁

Tactic:
by
  rw [← P.inr_i]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : Cylinder X
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
by
  induction h
  grind [weakEquivalence_precomp_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty Cᵒᵖ
inst✝ : P.IsStableUnderShift ℤ
n : ℤ
X : C
hX : P.unop X
⊢ P.unop.shift n X

Tactic:
obtain ⟨m, rfl⟩ : ∃ m, n = -m := ⟨-n , by simp⟩
        exact P.le_shift m _ hX

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ IsStrictlyGE (cylinder K) (n - 1)

Tactic:
CochainComplex.isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((cylinder K).X i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ IsStrictlyGE (pathObject K) (n - 1)

Tactic:
CochainComplex.isStrictlyGE_iff

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ (i : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((pathObject K).X i)