mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)

Tactic:
· rw [zpow_add_one₀ (by simp), zpow_mul, zpow_ofNat]
    simp

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

Goal state before:
pp: case cons.cons
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail)
      (hd2 :: tl2))

Tactic:
dsimp only
      split_ifs with h
      · cases hd1
        cases hd2
        cases h
        dsimp at *
        subst_vars
        apply Red.trans (Red.cons_cons ih)
        exact Red.Step.cons_not_rev.to_red
      · exact Red.cons_cons ih

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 g : 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 : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
set r := g - C g.leadingCoeff * q ^ m

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 g : 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 : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
⊢ IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A

Tactic:
rintro ⟨inj, cl⟩

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_2
B : Type u_3
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
inj : Function.Injective ⇑(algebraMap R B)
cl : ∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap R B) y = x
⊢ IsIntegrallyClosedIn R A
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

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

Tactic:
rintro ⟨inj, cl⟩

Goal state after:
case mpr
R : Type u_1
inst✝² : CommRing R
A : Type u_2
inst✝¹ : CommRing A
inst✝ : Algebra R A
inj : Function.Injective ⇑(algebraMap R A)
cl : ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
⊢ IsIntegrallyClosedIn R A
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ IsIntegrallyClosed S

Tactic:
have : IsScalarTower R S K := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝ : Algebra S K := g.toAlgebra
this : IsScalarTower R S K
⊢ IsIntegrallyClosed S
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
⊢ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
have h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)} := by simp [f']

Goal state after:
case refine_2
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
h₁ : ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f
h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)}
⊢ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
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 h
    refine ⟨?_⟩
    intro X p hp
    have : HasEqualizer (𝟙 X) p := h X p hp
    refine ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
      equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), ?_, equalizer.lift_ι _ _⟩
    ext
    simp only [assoc, limit.lift_π,
      Fork.ofι_π_app, id_comp]
    rw [← equalizer.condition, comp_id]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.map (SimplexCategory.σ j.succ).op ≫ X.map (SimplexCategory.δ i.castSucc).op =
    X.map (SimplexCategory.δ i).op ≫ X.map (SimplexCategory.σ j).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
A : Augmented C
⊢ (𝟭 (SimplicialObject D)).map (whiskerLeft (drop.obj A) η) ≫ ((whiskeringObj C D Y✝).obj A).hom =
    ((whiskeringObj C D X✝).obj A).hom ≫ (const D).map (η.app (point.obj A))

Tactic:
by
            ext n
            dsimp
            rw [Category.comp_id, Category.comp_id, η.naturality]

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

Goal state before:
pp: case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ₀Iter (j + 1) h ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯

Tactic:
δ₀Iter_succ'_assoc ..,

Goal state after:
case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ₀Iter (j + 1) ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

Tactic:
by_cases! hk : j ≤ k.val

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)

case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) ((ConcreteCategory.hom (δ i)) k)) =
    ↑((ConcreteCategory.hom (σ₀Iter j ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
A : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj (op ⦋i⦌)

Tactic:
by
  simp [← top_le_iff, le_iff_of_hasDimensionLT ⊤ A d]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
⊢ ∀ (j : Fin (x.len + 1)), F.hom ≫ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j) = Arrow.Hom.left G ≫ X.hom.app x

Tactic:
by
            rintro j
            rw [← Arrow.w_assoc G]
            have t := X.hom.naturality (SimplexCategory.const ⦋0⦌ x j)
            dsimp at t ⊢
            simp only [Category.id_comp] at t
            rw [← t]

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ Epi (A.toImage f)

Tactic:
rw [← range_eq_top_iff]
  apply le_antisymm (by simp)
  rintro m ⟨_, ⟨y, hy, rfl⟩⟩ _
  exact ⟨⟨y, hy⟩, rfl⟩

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
⊢ Finite X.N

Tactic:
have (i : Fin d) : Finite (X.nonDegenerate i) := h i.1 i.2

Goal state after:
X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
h : ∀ i < d, Finite ↑(X.nonDegenerate i)
this : ∀ (i : Fin d), Finite ↑(X.nonDegenerate ↑i)
⊢ Finite X.N
Module: Mathlib.AlgebraicTopology.SimplexCategory.Truncated

Goal state before:
pp: n m : ℕ
inst✝ : NeZero n
hm : n ≤ m
this : (incl n m hm ⋙ inclusion m).Initial
⊢ (incl n m ⋯).Initial

Tactic:
apply Functor.initial_of_comp_full_faithful _ (inclusion m)

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 ℕ
⊢ {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
        comm' := ⋯ } ≫
      {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)),
        comm' := ⋯ } =
    𝟙 ((truncate.obj C).augment (C.d 1 0) ⋯)

Tactic:
by
    ext i
    cases i <;> simp

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 ℕ
⊢ {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (C.X 0)
          | n.succ => 𝟙 (C.X (n + 1)),
        comm' := ⋯ } ≫
      {
        f := fun x ↦
          match x with
          | 0 => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X 0)
          | n.succ => 𝟙 (((truncate.obj C).augment (C.d 1 0) ⋯).X (n + 1)),
        comm' := ⋯ } =
    𝟙 C

Tactic:
by
    ext i
    cases i <;> simp

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

Goal state before:
pp: n d : ℕ
A : Δ[n].Subcomplex
x : ↑(Δ[n].nonDegenerate d)
⊢ ↑(nonDegenerateEquiv'.symm (nonDegenerateEquiv' x)) ∈ A.obj (op ⦋d⦌) ↔ face ↑(nonDegenerateEquiv' x) ≤ A

Tactic:
rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]

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

Goal state before:
pp: case zero
n d : ℕ
hd : #∅ ≤ d
hm : #∅ = 0
⊢ (face ∅).toSSet.HasDimensionLT d

Tactic:
face_empty

Goal state after:
case zero
n d : ℕ
hd : #∅ ≤ d
hm : #∅ = 0
⊢ ⊥.toSSet.HasDimensionLT d
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } =
    𝟙 (truncate.obj (C.augment f w))

Tactic:
by
    ext i
    cases i <;> simp

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ { f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ } = 𝟙 C

Tactic:
by
    ext i
    cases i <;> simp

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
⊢ ∀ (i₁ : ℤ) {i₂ i₂' : ℤ},
    (up ℤ).Rel i₂ i₂' →
      (i₁ * i₂).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (i₁, i₂) = (up ℤ).ε₁ (up ℤ) (up ℤ) (i₂, i₁) * (i₁ * i₂').negOnePow

Tactic:
rintro p q _ rfl

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow * (up ℤ).ε₂ (up ℤ) (up ℤ) (p, q) = (up ℤ).ε₁ (up ℤ) (up ℤ) (q, p) * (p * (q + 1)).negOnePow
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.π c₂ c₁₂ (c₁.next (c₁.next i₁), i₂) = i₁₂''

Tactic:
← ComplexShape.next_π₁ c₂ c₁₂ h₄,

Goal state after:
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁₂.next (c₁.π c₂ c₁₂ (c₁.next i₁, i₂)) = i₁₂''
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
C₂₃ : Type u_6
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₁₂
inst✝² : Category.{v_6, u_6} 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₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
hc : IsColimit c
c₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) →
  Cocone
    (Discrete.functor ((((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).mapObjFun ρ₁₂.p (↑i).1) ⋙ G.flip.obj (X₃ (↑i).2)) :=
  fun i ↦ (G.flip.obj (X₃ (↑i).2)).mapCocone (c₁₂ (↑i).1)
hc₁₂' : (i : ↑(ρ₁₂.q ⁻¹' {j})) → IsColimit (c₁₂' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → ρ₁₂.I₁₂ × I₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (ρ₁₂.p (i₁, i₂), i₃)
e : (i₁₂ : ρ₁₂.I₁₂) → (i₃ : I₃) → ↑(p' ⁻¹' {(i₁₂, i₃)}) ≃ ↑(ρ₁₂.p ⁻¹' {i₁₂}) :=
  fun i₁₂ i₃ ↦
    {
      toFun := fun x ↦
        match x with
        | ⟨(i₁, i₂, i₃'), hi⟩ => ⟨(i₁, i₂), ⋯⟩,
      invFun := fun x ↦
        match x with
        | ⟨(i₁, i₂), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }
x✝ : ↑(ρ₁₂.q ⁻¹' {j})
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
hi : (i₁₂, i₃) ∈ ρ₁₂.q ⁻¹' {j}
⊢ Z.CofanMapObjFun p' ((↑⟨(i₁₂, i₃), hi⟩).1, (↑⟨(i₁₂, i₃), hi⟩).2)

Tactic:
by
      refine (Cocone.precompose (Iso.hom ?_)).obj ((Cocone.whiskeringEquivalence
        (Discrete.equivalence (e i₁₂ i₃))).functor.obj (c₁₂' ⟨⟨i₁₂, i₃⟩, hi⟩))
      refine (Discrete.natIso (fun ⟨⟨i₁, i₂, i₃'⟩, hi⟩ =>
        (G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).mapIso (eqToIso ?_)))
      obtain rfl : i₃' = i₃ := congr_arg _root_.Prod.snd hi
      rfl

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₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂))

Tactic:
ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄

Goal state after:
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₂)
⊢ c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = c₁.π c₂ c₁₂ (i₁, c₂.next i₂)
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
rw [K.d₂_eq_zero _ _ _ _ h₂, K.flip.d₁_eq_zero _ _ _ _ h₂, smul_zero, zero_comp]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to Y)

Tactic:
Subsingleton.elim (initial.to Y) (initial.to X ≫ i)

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
inst✝¹ : (cofibrations C).IsStableUnderComposition
X Y : C
i : X ⟶ Y
inst✝ : Cofibration i
hX : Cofibration (initial.to X)
⊢ Cofibration (initial.to X ≫ i)
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ (P.trans P').p = ψ ≫ prod.map P.p₀ (𝟙 A)

Tactic:
simp [PrepathObject.p, ψ]

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

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
inst✝² : Preadditive D
A : Type u_3
inst✝¹ : Category.{v_3, u_3} A
inst✝ : Abelian A
a : ℤ
X Y : Plus A
f : X ⟶ Y
⊢ (quasiIso A).inverseImage (shiftFunctor (Plus A) a) f ↔
    HomotopyCategory.quasiIso A (ComplexShape.up ℤ)
      ((shiftFunctor (HomotopyCategory A (ComplexShape.up ℤ)) a).map f.hom)

Tactic:
exact (HomotopyCategory.quasiIso _ _).arrow_mk_iso_iff
      (Arrow.isoOfNatIso ((ι A).commShiftIso a) (Arrow.mk f))

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (B.inverseImage A.ι).trW f ↔ (A ⊓ B).trW f.hom

Tactic:
simp only [trW_iff]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk f.hom g h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) Z