mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ (Function.Injective ⇑(algebraMap (↥S) A) ∧ ∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
and_iff_right (FaithfulSMul.algebraMap_injective _ _)

Goal state after:
A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ (∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), f a = 0 ↔ a = 0
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
this : eval₂ f (f x * z) (p.scaleRoots x) = 0
⊢ (p.scaleRoots x).IsRoot y

Tactic:
rwa [hz, Polynomial.eval₂_at_apply, hf] at this

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

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsEisensteinAt 𝓟
n : ℕ
hn : n ≠ f.natDegree
h₂ : f.natDegree < n
⊢ f.coeff n ∈ 𝓟

Tactic:
· rw [coeff_eq_zero_of_natDegree_lt h₂]
    exact Ideal.zero_mem _

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
n : ℕ
hn : ¬n = f.natDegree
hn' : ¬n < f.natDegree
⊢ f.natDegree < n

Tactic:
· simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).re = (↑x✝¹ • x✝).re

Tactic:
exact Rat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imI = (↑x✝¹ • x✝).imI

Tactic:
exact Rat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imJ = (↑x✝¹ • x✝).imJ

Tactic:
exact Rat.smul_def ..

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: case a
R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝¹ : ℚ
x✝ : ℍ[R]
⊢ (x✝¹ • x✝).imK = (↑x✝¹ • x✝).imK

Tactic:
exact Rat.smul_def ..

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

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ k * x = x ^ ↑k * x

Tactic:
← hk

Goal state after:
case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ k * x = x ^ k * x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case inl
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[k] (fun x ↦ 0) 0 = 0

Tactic:
fwdDiff_iter_eq_sum_shift,

Goal state after:
case inl
m k : ℕ
hmn : m < m + k + 1
⊢ ∑ k_1 ∈ range (k + 1), ((-1) ^ (k - k_1) * ↑(k.choose k_1)) • 0 = 0
Module: Mathlib.Algebra.Group.Translate

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
⊢ support (τ a f) = a +ᵥ support f

Tactic:
by
  ext; simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' {i | 1 < f (v i)})

Tactic:
by
  refine le_antisymm (closure_mono (image_mono <| IsMulIndecomposable.baseOf_subset_one_lt v f))
    (closure_le.mpr ?_)
  rintro - ⟨i, hi : 1 < f (v i), rfl⟩
  by_contra hi'
  let t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
  let s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
  have hne : s.Nonempty := ⟨i, hi, hi'⟩
  clear! i
  obtain ⟨i, hi⟩ := s.toFinite.exists_minimalFor (f ∘ v) s hne
  have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
  have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by
    by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le
  have hi₃ : i ∉ t := by contrapose hi₁; exact subset_closure <| mem_image_of_mem v hi₁
  obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)),
      v i = v j * v k := by
    grind [IsMulIndecomposable]
  have hj' : v j ∈ closure (v '' t) := hi₂ j hj <| by aesop
  have hk' : v k ∈ closure (v '' t) := hi₂ k hk <| by aesop
  replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'
  exact hi₁ hjk

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
· obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
· obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Goal state after:
case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr
ι : 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
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : 1 < f (v i)
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})

Tactic:
· left
    exact Submonoid.subset_closure ⟨i, by simpa⟩

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

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : v = u * y
⊢ y ∈ f.valueGroup

Tactic:
← inv_mul_eq_iff_eq_mul

Goal state after:
case refine_2
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
x✝ : ∃ a, ¬f a = 0 ∧ ∃ x, f a * ↑y = f x
a : A
ha : f a ≠ 0
x : A
hv : f x ≠ 0
v : Bˣ := ⋯.unit
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
hy : u⁻¹ * v = y
⊢ y ∈ f.valueGroup
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)

Tactic:
rw [mem_valueGroup_iff_of_comm'] at hx

Goal state after:
case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx✝ : x ∈ f.valueGroup
hx : ∃ a, f a ≠ 0 ∧ ∃ x_1, f x_1 ≠ 0 ∧ f a * ↑x = f x_1
⊢ some ⟨x, hx✝⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx✝⟩ = ↑(valueGroup.mk f r s hr hs)
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (fun x ↦ (h.inv { down := x }).down) ((fun x ↦ (h.hom { down := x }).down) a) = a

Tactic:
change ULift.down _ = _

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin X.len
⊢ (h.inv { down := (fun x ↦ (h.hom { down := x }).down) a }).down = a
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (fun x ↦ (h.hom { down := x }).down) ((fun x ↦ (h.inv { down := x }).down) a) = a

Tactic:
change ULift.down _ = _

Goal state after:
X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
a : Fin Y.len
⊢ (h.hom { down := (fun x ↦ (h.inv { down := x }).down) a }).down = a
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (kernelSubobject (X.δ i.succ)).factorThru (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ⋯ ≫
      (kernelSubobject (X.δ i.succ)).arrow ≫ X.map (SimplexCategory.δ i.succ).op ≫ f.app (op ⦋n✝⦌) =
    0

Tactic:
rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

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✝
x : SimplexCategory
⊢ f.unop.right.op ≫ ((unop Y✝).hom.app (op x)).op = ((unop X✝).hom.app (op x)).op ≫ (f.unop.left.app (op x)).op

Tactic:
simp_rw [← op_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ ((unop Y✝).hom.app (op x) ≫ f.unop.right).op = (f.unop.left.app (op x) ≫ (unop X✝).hom.app (op x)).op
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x✝¹ x✝ : SimplexCategory
f g : x✝¹ ⟶ x✝
h : skeletalFunctor.map f = skeletalFunctor.map g
⊢ f = g

Tactic:
ext : 3
    exact CategoryTheory.congr_fun h _

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✝
⊢ f.unop.op ≫ (unop Y✝).rightOpLeftOpIso.hom.op =
    (unop X✝).rightOpLeftOpIso.hom.op ≫
      Quiver.Hom.op
        { left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ }

Tactic:
simp_rw [← op_comp]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((unop Y✝).rightOpLeftOpIso.hom ≫ f.unop).op =
    ({ left := NatTrans.leftOp (NatTrans.rightOp f.unop.op.unop.left), right := f.unop.op.unop.right, w := ⋯ } ≫
        (unop X✝).rightOpLeftOpIso.hom).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.Op

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v, u_1} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ (opFunctor.obj X).σ i = opObjIso.hom ≫ X.σ i.rev ≫ opObjIso.inv

Tactic:
simp [opObjIso, SimplicialObject.σ]

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

Goal state before:
pp: 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
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) k.succ) = ↑k - j

Tactic:
σ₀Iter_coe_eq_of_ge ..

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
hk' : i ≤ k.castSucc
⊢ ↑k.succ - (j + 1) = ↑k - j
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (k.pred ⋯)) = ↑k - (i + 1)

Tactic:
σ₀Iter_coe_eq_of_ge ..

Goal state after:
case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑(k.pred ⋯) - i = ↑k - (i + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) → x ∈ X.degenerate n

Tactic:
rintro ⟨m, hm, f, hf, hx⟩

Goal state after:
case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
⊢ x ∈ X.degenerate n
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:
rintro j

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: case mp
X : SSet
x y : X.S
⊢ (∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex) → Nonempty (equivElements y ⟶ equivElements x)

pp: case mpr
X : SSet
x y : X.S
⊢ Nonempty (equivElements y ⟶ equivElements x) → ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
· rintro ⟨f, hf⟩
    exact ⟨⟨f.op, hf⟩⟩

Goal state after:
case mpr
X : SSet
x y : X.S
⊢ Nonempty (equivElements y ⟶ equivElements x) → ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
⊢ range ((A.preimage p).ι ≫ p) ≤ A

Tactic:
simp [range_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
this : Odd (i + j)
⊢ φ = ψ

Tactic:
exact False.elim <| Nat.not_even_iff_odd.2 h <| by simp_all [Nat.odd_add]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : Even n
h₀ : n ≠ 0
⊢ ∀ (Z : C) (g : Z ⟶ (HomologicalComplex.sc (alternatingConst.obj X) n).X₂),
    g ≫ (HomologicalComplex.sc (alternatingConst.obj X) n).g = 0 → g = 0

Tactic:
by cases n <;> simp_all

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

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
· exact ⟨⟨alternatingConstHomologyDataOdd X _ h⟩⟩

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ l ∈ Set.range j.succAbove

Tactic:
grind [Fin.range_succAbove, mem_compl, Fin.succAbove]

Goal state after:
Module: Mathlib.CategoryTheory.Center.NegOnePow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
n : ℤ
X : C
⊢ (↑((-1) ^ n)).app X = n.negOnePow • 𝟙 X

Tactic:
obtain ⟨n, rfl⟩ | ⟨n, rfl⟩ := Int.even_or_odd n

Goal state after:
case inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
n : ℤ
⊢ (↑((-1) ^ (n + n))).app X = (n + n).negOnePow • 𝟙 X

case inr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
n : ℤ
⊢ (↑((-1) ^ (2 * n + 1))).app X = (2 * n + 1).negOnePow • 𝟙 X
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel i₁ (c₁.next i₁)
⊢ c₁.π c₂ c (c₁.next i₁, i₂) = c.next j

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

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

Goal state before:
pp: case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ 0 = d₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
d₃_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₁

Goal state after:
case neg
C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
h₁ : ¬c₃.Rel i₃ (c₃.next i₃)
⊢ 0 = 0
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 sq.cokernelCofork
s : PushoutCocone f g
⊢ inr ≫ h.desc (CokernelCofork.ofπ (biprod.desc s.inl s.inr) ⋯) = s.inr

Tactic:
simpa using biprod.inr ≫=
                h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr)
                  (by simp [s.condition])) .one

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithFibrations C
inst✝¹ : (fibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialFibrations C).IsStableUnderRetracts

Tactic:
dsimp [trivialFibrations]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
fg : X ⟶ Z
fac : f ≫ g = fg
inst✝¹ : WeakEquivalence f
inst✝ : WeakEquivalence fg
⊢ WeakEquivalence g

Tactic:
subst fac
  exact weakEquivalence_of_precomp f g

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : cofibrations C i
hp : trivialFibrations C p
⊢ HasLiftingProperty i p

Tactic:
rw [mem_trivialFibrations_iff] at hp
    rw [← cofibration_iff] at hi
    have := hp.1
    have := hp.2
    infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
inst✝¹ : L.EssSurj
inst✝ : L.Full
W : MorphismProperty C
hW : W.IsInvertedBy L
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), L.map f₀ = L.map f₁ → ∃ P x, W P.ι
X Y : Cᵒᵖ
f₀ f₁ : X ⟶ Y
hf : L.op.map f₀ = L.op.map f₁
P : PrepathObject (Opposite.unop X)
h : P.RightHomotopy f₀.unop f₁.unop
hι : W P.ι
⊢ ∃ P x, W.op P.π

Tactic:
exact ⟨P.op, h.op, hι⟩

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
K : CochainComplex C ℤ
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj K) → CochainComplex.plus C K

Tactic:
simp only [plus, ObjectProperty.strictMap_iff]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
⊢ (∃ X, CochainComplex.plus C X ∧ (quotient C (ComplexShape.up ℤ)).obj X = (quotient C (ComplexShape.up ℤ)).obj K) →
    CochainComplex.plus C K