mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (count x) (of y) = Pi.single x 1 y

Tactic:
dsimp [count]
  rw [countP_of]
  simp [Pi.single, Function.update]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
P : Ideal R := ⋯
hP : P.IsPrime
m : ℕ
hm✝ : m ≤ p
hm : m = 0
a : R
hg_div : C a ∣ f
hgP : (C a).leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) (C a) ∣ map (algebraMap R K) q ^ p
hf : Associated (map (algebraMap R K) (C a)) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : C a = C (C a).leadingCoeff + r
hr : map (algebraMap R K) r = 0
this : (C a).natDegree = 0
⊢ IsUnit a

Tactic:
apply hf_prim

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
P : Ideal R := ⋯
hP : P.IsPrime
m : ℕ
hm✝ : m ≤ p
hm : m = 0
a : R
hg_div : C a ∣ f
hgP : (C a).leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) (C a) ∣ map (algebraMap R K) q ^ p
hf : Associated (map (algebraMap R K) (C a)) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : C a = C (C a).leadingCoeff + r
hr : map (algebraMap R K) r = 0
this : (C a).natDegree = 0
⊢ C a ∣ f
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ IsIntegrallyClosedIn R A ↔
    Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x

Tactic:
by
  constructor
  · rintro ⟨_, cl⟩
    simp_all
  · rintro ⟨inj, cl⟩
    refine ⟨inj, by simp_all, ?_⟩
    rintro ⟨y, rfl⟩
    apply isIntegral_algebraMap

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
⊢ IsIntegralClosure S R U

Tactic:
by
  refine ⟨?_, ?_⟩
  · rw [IsScalarTower.algebraMap_eq S T U]
    exact (IsIntegralClosure.algebraMap_injective T T U).comp
      (IsIntegralClosure.algebraMap_injective S R T)
  · intro x
    refine ⟨fun h ↦ ?_, ?_⟩
    · obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
      rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
      obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
      exact ⟨x, IsScalarTower.algebraMap_apply ..⟩
    · rintro ⟨x, rfl⟩
      rw [IsScalarTower.algebraMap_apply S T U]
      exact ((IsIntegralClosure.isIntegral_iff (A := S) (R := R) (B := T)).mpr ⟨x, rfl⟩).map
        (IsScalarTower.toAlgHom R T U)

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ x y : R
inst✝ : CommRing R
⊢ x • ↑y = ↑(x * y)

Tactic:
rw [coe_mul, coe_mul_eq_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ≥0
x✝ : ℍ[R]
⊢ x✝¹ • x✝ = ↑x✝¹ * x✝

Tactic:
by rw [← coe_nnratCast, coe_mul_eq_smul]; ext <;> exact NNRat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
m n : ℕ+
x : M
⊢ x ^ m * x ^ n = x ^ n * x ^ m

Tactic:
by simp only [← ppow_add, add_comm]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : CommMonoidWithZero β
⊢ CommMonoidWithZero α

Tactic:
let _ := e.monoidWithZero
  apply e.injective.commMonoidWithZero _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
j j' : J
φ : j ⟶ j'
⊢ (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j'

Tactic:
rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case hi
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)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ

Tactic:
simp_rw [S, φ, Finset.compl_filter, Finset.mem_filter_univ, Fin.val_succ,
      Fin.val_castLT] at hij ⊢

Goal state after:
case hi
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)
ij : P
hij✝ : ij ∈ {ij | ↑ij.2 ≤ ↑ij.1}
hij : ↑ij.2 ≤ ↑ij.1
⊢ ¬↑ij.1 + 1 ≤ ↑ij.2
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
rcases le_or_gt i k with (h | h)

Goal state after:
case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.N
⊢ x ≤ y ↔ ∃ f, ∃ (_ : Mono f), (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
simp only [le_iff, CategoryTheory.Subfunctor.ofSection_le_iff,
    Subcomplex.mem_ofSimplex_obj_iff]
  exact ⟨fun ⟨f, hf⟩ ↦ ⟨f, X.mono_of_nonDegenerate ⟨_, x.nonDegenerate⟩ f _ hf, hf⟩, by tauto⟩

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

Goal state before:
pp: case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x ≤ y

Tactic:
· rw [le_iff, h]

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

Goal state before:
pp: case a
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ y ≤ x

Tactic:
· rw [le_iff, h]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.down ℕ).Rel i j →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 1 0) ⋯).d i j =
      C.d i j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
by
        match i with
          | 0 | 1 | n + 2 =>
          rcases j with - | j <;> dsimp [augment, truncate] <;> simp

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

Goal state before:
pp: case a.mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : x ∈ (face S).obj (op ⦋k⦌)
⊢ x ∈
    (Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌)

Tactic:
mem_face_iff

Goal state after:
case a.mk
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
k : ℕ
x : Δ[n] _⦋k⦌
hx : ∀ (i : Fin (k + 1)), x i ∈ S
⊢ x ∈
    (Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))).obj
      (op ⦋k⦌)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₁_assoc, comp_zero]
      by_cases h₃ : c₁.Rel i₁ (c₁.next i₁)
      · rw [totalAux.d₁_eq K c₁₂ h₃ i₂ i₁₂']; swap
        · rw [← ComplexShape.next_π₁ c₂ c₁₂ h₃ i₂, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₁]
        by_cases h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
        · rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₁ c₂ c₁₂ h₄, ← ComplexShape.next_π₁ c₂ c₁₂ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₁_eq_zero _ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₁_eq_zero c₁₂ _ _ _ h₃, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₂.Rel i₂ (c₂.next i₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = i₁₂''

Tactic:
rw [← c₁₂.next_eq' h₂, ← ComplexShape.next_π₁ c₂ c₁₂ h₃, h₅]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : ¬c₁.Rel i₁ (c₁.next i₁)
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, zero_comp]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      c₁.ε₂ c₂ c (i₁, i₂) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
        ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
          (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).ιTotal c i₁' i₂' (c.next j) ⋯ ≫
            hom₁ h₁ f₂ F c (c.next j) j)

Tactic:
ιMapBifunctor_hom₁ _ _ _ _ _ _ _ _ _ _ (c₁.prev_eq' hi₁),

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ c₁.ε₁ c₂ c (i₁, i₂) •
      c₁.ε₂ c₂ c (i₁, i₂) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
            ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).X i₁).d i₂ i₂' ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    -(c₁.ε₂ c₂ c (i₁', i₂) •
        ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).X i₁').d i₂ i₂' ≫
          (c₁.ε₁ c₂ c (i₁, i₂') •
            (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂') ≫
              (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂' j))
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 : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫
      (total.map ((shiftFunctor₁ C x).map f) (up ℤ)).f n ≫ (L.totalShift₁Iso x).hom.f n =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
rw [ιTotal_map_assoc, L.ι_totalShift₁Iso_hom_f x i₁ i₂ n h _ rfl _ rfl,
    K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫ (total.map f (up ℤ)).f (n + x)
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: case h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ biprod.inr ≫ biprod.desc inl inr ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ =
    biprod.inr ≫ s.π

Tactic:
simp only [biprod.inr_desc_assoc]
          apply PushoutCocone.IsColimit.inr_desc h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ Cofork.π sq.cokernelCofork ≫ PushoutCocone.IsColimit.desc h (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) ⋯ = s.π

Tactic:
dsimp
        ext
        · simp only [biprod.inl_desc_assoc]
          apply PushoutCocone.IsColimit.inl_desc h
        · simp only [biprod.inr_desc_assoc]
          apply PushoutCocone.IsColimit.inr_desc h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n : ℕ
⊢ (limitSequence φ hφ x₀).EqUpTo (↑(sequence φ x₀ n)) (p₀ + ↑n)

Tactic:
by
  intro p q hpq hp
  exact sequence_eqUpTo φ hφ _ _ _ (by lia) _ _ _ (by lia)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
hf : L.map f₁ = L.map f₂
⊢ f₁ = f₂

pp: case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = g

Tactic:
· rw [MorphismProperty.map_eq_iff_postcomp L P.trW] at hf
    obtain ⟨Z, s, hs, eq⟩ := hf
    exact (hX _ hs).1 eq

Goal state after:
case refine_2
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
g : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = g
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
n : ℤ
⊢ (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))

Tactic:
exact ObjectProperty.prop_of_iso _
    (((HomotopyCategory.quotient C (.up ℤ)).commShiftIso n).symm.app L)
    ((HomotopyCategory.subcategoryAcyclic C).rightOrthogonal.le_shift n _ hL)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
a : ℕ
ha : n₁ - n₀ = ↑a
⊢ t.le n₀ ≤ t.le n₁

Tactic:
obtain rfl : n₁ = n₀ + a := by lia

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.le n ≤ t.le (n + ↑a)
this : ∀ (a : ℕ), H a
n₀ : ℤ
a : ℕ
h : n₀ ≤ n₀ + ↑a
ha : n₀ + ↑a - n₀ = ↑a
⊢ t.le n₀ ≤ t.le (n₀ + ↑a)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ n₁ : ℤ
h : n₀ ≤ n₁
a : ℕ
ha : n₁ - n₀ = ↑a
⊢ t.ge n₁ ≤ t.ge n₀

Tactic:
obtain rfl : n₁ = n₀ + a := by lia

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
this : ∀ (a : ℕ), H a
n₀ : ℤ
a : ℕ
h : n₀ ≤ n₀ + ↑a
ha : n₀ + ↑a - n₀ = ↑a
⊢ t.ge (n₀ + ↑a) ≤ t.ge n₀
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
⊢ t.IsGE ((shiftFunctor C a).obj X) n' → t.IsGE X n

Tactic:
intro
    exact t.isGE_of_shift X n a n' hn'

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ WeakEquivalence f ↔ WeakEquivalence f.hom

Tactic:
by
  simp only [weakEquivalence_iff]
  rfl

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : Fibration (terminal.from Y)
⊢ Fibration prod.fst

Tactic:
rw [fibration_iff] at hY ⊢

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithFibrations C
inst✝² : HasTerminal C
X Y : C
inst✝¹ : (fibrations C).IsStableUnderBaseChange
inst✝ : HasBinaryProduct X Y
hY : fibrations C (terminal.from Y)
⊢ fibrations C prod.fst
Module: Mathlib.CategoryTheory.Localization.OfQuotient

Goal state before:
pp: case h_obj
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (X : Quotient r), F₁.obj X = F₂.obj X

Tactic:
rintro ⟨X⟩

Goal state after:
case h_obj
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
X : C
⊢ F₁.obj { as := X } = F₂.obj { as := X }
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
⊢ (t.truncGT n).Additive

Tactic:
dsimp only [truncGT]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
⊢ (t.truncGE (n + 1)).Additive