mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite :=
      WellFoundedGT.finite_ne_bot_of_iSupIndep f.independent_maxGenEigenspace

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
this : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) ((g ∘ₗ f).restrict ⋯) = 0
hds : IsInternal f.maxGenEigenspace
h_fin : {μ | f.maxGenEigenspace μ ≠ ⊥}.Finite
⊢ (trace R M) (g ∘ₗ f) = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst ∈ (inlAlgHom R A A).range ⊔ R[ ε]

pp: case refine_2
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.snd ∈ (inlAlgHom R A A).range ⊔ R[ ε]

pp: case refine_3
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
· exact le_sup_left (α := Subalgebra R _) <| Set.mem_range_self x.fst

Goal state after:
case refine_2
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.snd ∈ (inlAlgHom R A A).range ⊔ R[ ε]

case refine_3
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ ε ∈ (inlAlgHom R A A).range ⊔ R[ ε]

Tactic:
· refine le_sup_right (α := Subalgebra R _) <| subset_adjoin <| Set.mem_singleton ε

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
classical
  by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)
  · obtain ⟨s, ⟨b⟩⟩ := hM
    have := Module.Finite.of_basis b
    have := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
    have := Module.Finite.of_basis (b.map e)
    have := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
    rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
  · rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ ∀ (x y : ℍ[DualNumber R]),
    ({ re := TrivSqZeroExt.fst (x + y).re, imI := TrivSqZeroExt.fst (x + y).imI, imJ := TrivSqZeroExt.fst (x + y).imJ,
          imK := TrivSqZeroExt.fst (x + y).imK },
        { re := TrivSqZeroExt.snd (x + y).re, imI := TrivSqZeroExt.snd (x + y).imI,
          imJ := TrivSqZeroExt.snd (x + y).imJ, imK := TrivSqZeroExt.snd (x + y).imK }) =
      ({ re := TrivSqZeroExt.fst x.re, imI := TrivSqZeroExt.fst x.imI, imJ := TrivSqZeroExt.fst x.imJ,
            imK := TrivSqZeroExt.fst x.imK },
          { re := TrivSqZeroExt.snd x.re, imI := TrivSqZeroExt.snd x.imI, imJ := TrivSqZeroExt.snd x.imJ,
            imK := TrivSqZeroExt.snd x.imK }) +
        ({ re := TrivSqZeroExt.fst y.re, imI := TrivSqZeroExt.fst y.imI, imJ := TrivSqZeroExt.fst y.imJ,
            imK := TrivSqZeroExt.fst y.imK },
          { re := TrivSqZeroExt.snd y.re, imI := TrivSqZeroExt.snd y.imI, imJ := TrivSqZeroExt.snd y.imJ,
            imK := TrivSqZeroExt.snd y.imK })

Tactic:
intros
    rfl

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

Tactic:
by
  rw [countP_apply, toList_of, List.countP_singleton, apply_ite (Multiplicative.ofAdd)]
  simp only [decide_eq_true_eq]

Goal state after:
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
inst✝¹ : GCDMonoid R
M : Submonoid R
inst✝ : IsLocalization M A
z : A
⊢ ∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a

Tactic:
obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq M z
  obtain ⟨x', y', hx', hy', hu⟩ := extract_gcd x y
  use x', y', hu
  rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]
  convert! IsLocalization.mk'_mul_cancel_left (M := M) (S := A) _ _ using 2
  grind

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.IntegrallyClosed

Goal state before:
pp: case h
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
this : IsUnit y
⊢ (algebraMap R (FractionRing R)) x * (algebraMap R (FractionRing R)) ↑this.unit⁻¹ = X

Tactic:
have coe_map_inv :=
      Units.coe_map_inv ((algebraMap R (FractionRing R) : R →* FractionRing R)) this.unit

Goal state after:
case h
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
this : IsUnit y
coe_map_inv :
  ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = ↑(algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ (algebraMap R (FractionRing R)) x * (algebraMap R (FractionRing R)) ↑this.unit⁻¹ = X
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| x * y * star (x * y)

Tactic:
star_mul,

Goal state after:
S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
| x * y * (star y * star x)
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✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b ↦ 1 • b) s = s

Tactic:
by simp_rw [one_smul, image_id']

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

Goal state before:
pp: case hfmodP2
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
⊢ eval 0 f ∉ ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2

Tactic:
← coeff_zero_eq_eval_zero

Goal state after:
case hfmodP2
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
⊢ f.coeff 0 ∉ ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝ : fwdDiffₗ M G h = shiftₗ M G h - 1
this : Commute (shiftₗ M G h) (-1)
k : ℕ
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y

Tactic:
have : ((-1) ^ (n - k) * n.choose k : Module.End ℤ (M → G))
              = ↑((-1) ^ (n - k) * n.choose k : ℤ) := by norm_cast

Goal state after:
case e'_3.e_f
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
this✝¹ : fwdDiffₗ M G h = shiftₗ M G h - 1
this✝ : Commute (shiftₗ M G h) (-1)
k : ℕ
this : (-1) ^ (n - k) * ↑(n.choose k) = ↑((-1) ^ (n - k) * ↑(n.choose k))
⊢ ((-1) ^ (n - k) * ↑(n.choose k)) • f (y + k • h) = (shiftₗ M G h ^ k * (-1) ^ (n - k) * ↑(n.choose k)) f y
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ ∑ c ∈ range (P.natDegree + 1), (P.coeff c • Δ_[1]^[P.natDegree] fun i ↦ i ^ c) x = P.leadingCoeff • ↑P.natDegree ! x

Tactic:
sum_range_succ,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ ∑ x_1 ∈ range P.natDegree, (P.coeff x_1 • Δ_[1]^[P.natDegree] fun i ↦ i ^ x_1) x +
      (P.coeff P.natDegree • Δ_[1]^[P.natDegree] fun i ↦ i ^ P.natDegree) x =
    P.leadingCoeff • ↑P.natDegree ! x
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Cardinal.toNat #↑(s * t) ≤ Cardinal.toNat (#↑s * #↑t)

Tactic:
refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_

Goal state after:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ #↑s * #↑t < ℵ₀
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑((fun x ↦ x⁻¹) '' s) = #↑s

Tactic:
Cardinal.mk_image_eq_of_injOn _ _ inv_injective.injOn

Goal state after:
G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ #↑s = #↑s
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
⊢ (⇑invMonoidHom ∘ v) i⁻¹ = v i

Tactic:
simp [hv_inv]

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ v j = 1 ∨ v k = 1

Tactic:
specialize hi' j⁻¹ (by simpa [hv_inv]) k⁻¹ (by simpa [hv_inv]) hi

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hi' : v j⁻¹ = 1 ∨ v k⁻¹ = 1
hk : k ∈ {i | 1 < f (v i)}
hi : v i = v j⁻¹ * v k⁻¹
⊢ v j = 1 ∨ v k = 1
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹⁻¹ = (v i⁻¹)⁻¹

Tactic:
simp [hv_inv]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ (if h : f 1 = 0 then 0 else ↑⟨Units.mk0 (f 1) h, ⋯⟩) = 1

Tactic:
simp [← WithZero.coe_one]

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

Goal state before:
pp: case h₁
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a✝ : Bˣ
⊢ a✝ ∈ (↑f.valueMonoid)⁻¹ → a✝ ∈ ↑f.valueMonoid

Tactic:
⟨y, hy⟩

Goal state after:
case h₁
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
a✝ : Bˣ
y : A
hy : f y = ↑a✝⁻¹
⊢ a✝ ∈ ↑f.valueMonoid
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
hy : f a * ↑y = ↑v
hv₀ : f x = ↑v
u : Bˣ := ⋯.unit
ha₀ : f a = ↑u
⊢ y ∈ f.valueGroup

Tactic:
ha₀

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
hy : ↑u * ↑y = ↑v
ha₀ : f a = ↑u
⊢ y ∈ f.valueGroup
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f : P ⟶ Q
⊢ -f + f = 0

Tactic:
by
    ext
    apply neg_add_cancel

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ P.p ≫ p.f ≫ { X := P.X, p := p.f, idem := hp }.p = p.f

Tactic:
rw [hp, p_comp p]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: 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}
⊢ ∑ i ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) =
    ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)

Tactic:
let φ : ∀ ij : P, ij ∈ S → P := fun ij hij =>
    (Fin.castLT ij.2 (lt_of_le_of_lt (Finset.mem_filter.mp hij).right (Fin.is_lt ij.1)), ij.1.succ)

Goal state after:
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 ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) =
    ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)
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
⊢ toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C = (Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)

Tactic:
apply Functor.ext
  · intro X Y f
    ext j
    simp
  · intro X
    apply Functor.ext
    · intro j j' φ
      ext
      simp
    · intro j
      rfl

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

Goal state before:
pp: case last
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.last ⦋n + 1 + 1⦌.len)) =
    i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))

Tactic:
| last =>

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map (SimplexCategory.δ₀Iter i ⋯).op ≫ X.map (SimplexCategory.δ 0).op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.δ₀Iter (i + 1) h).op = X.map ((SimplexCategory.δ₀Iter i ⋯).op ≫ (SimplexCategory.δ 0).op)
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.δ j).op ≫ X.map (SimplexCategory.δ₀Iter i hi).op = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map ((SimplexCategory.δ j).op ≫ (SimplexCategory.δ₀Iter i hi).op) = X.map (SimplexCategory.δ₀Iter (i + 1) ⋯).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ j).op ≫ X.map (SimplexCategory.δ₀Iter (i + 1) hi).op = X.map (SimplexCategory.δ₀Iter i ⋯).op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.map ((SimplexCategory.σ j).op ≫ (SimplexCategory.δ₀Iter (i + 1) hi).op) = X.map (SimplexCategory.δ₀Iter i ⋯).op
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op = X.map (SimplexCategory.σ 0).op ≫ X.map (SimplexCategory.σ₀Iter i ⋯).op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
h : n + (i + 1) = m
⊢ X.map (SimplexCategory.σ₀Iter (i + 1) h).op = X.map ((SimplexCategory.σ 0).op ≫ (SimplexCategory.σ₀Iter i ⋯).op)
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op

Tactic:
← Functor.map_comp,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map ((SimplexCategory.σ₀Iter i hi).op ≫ (SimplexCategory.σ j).op) = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
s t : X.S
x✝ : ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
h₁ : s.dim = t.dim
h₂ : (s.cast h₁).simplex = t.simplex
⊢ s = t

Tactic:
by
    obtain ⟨_, _, rfl⟩ := s.mk_surjective
    obtain ⟨_, _, rfl⟩ := t.mk_surjective
    aesop

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ (ConcreteCategory.hom (X.map (image.ι f).op ≫ X.map (factorThruImage f).op)) y = ↑x

Tactic:
← Functor.map_comp,

Goal state after:
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ (ConcreteCategory.hom (X.map ((image.ι f).op ≫ (factorThruImage f).op))) y = ↑x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map f₁.op ≫ X.map hf₁.section_.op)) ↑y₁ = ↑y₁

Tactic:
← Functor.map_comp,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map (f₁.op ≫ hf₁.section_.op))) ↑y₁ = ↑y₁
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:
by
    have (i : Fin d) : Finite (X.nonDegenerate i) := h i.1 i.2
    refine Finite.of_surjective (α := Σ (i : Fin d), X.nonDegenerate i)
      (f := fun ⟨i, x⟩ ↦ N.mk _ x.property) (fun x ↦ ?_)
    by_cases hj : x.dim < d
    · exact ⟨⟨⟨_, hj⟩, ⟨_, x.nonDegenerate⟩⟩, rfl⟩
    · have := x.nonDegenerate
      simp [X.nonDegenerate_eq_empty_of_hasDimensionLT d x.dim (by simpa using hj)] at this

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x : X.N
⊢ (fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯)
      ((fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯) x) =
    x

Tactic:
by simp [N.ext_iff, S.ext_iff']

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : Y.N
⊢ (fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯)
      ((fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯) x✝) =
    x✝

Tactic:
by simp [N.ext_iff, S.ext_iff']

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
⊢ f₁ = f₂

Tactic:
by
  ext x : 3
  suffices ∃ (hf₁ : SplitEpi f₁), hf₁.section_.toOrderHom (f₁.toOrderHom x) = x by
    obtain ⟨hf₁, hf₁'⟩ := this
    dsimp at hf₁'
    simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm
  obtain ⟨⟨hf⟩⟩ := isSplitEpi_of_epi f₁
  let α (y : Fin (m + 1)) : Fin (n + 1) :=
    if y = f₁.toOrderHom x then x else hf.section_.toOrderHom y
  have hα₁ (y : Fin (m + 1)) : f₁.toOrderHom (α y) = y := by
    dsimp [α]
    split_ifs with hy
    · rw [hy]
    · apply SimplexCategory.congr_toOrderHom_apply hf.id
  have hα₂ : Monotone α := by
    rintro y₁ y₂ h
    by_contra! h'
    suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'
    simpa only [hα₁] using f₁.toOrderHom.monotone h'.le
  exact ⟨{ section_ := SimplexCategory.Hom.mk ⟨α, hα₂⟩, id := by ext : 3; apply hα₁ },
    by simp [α]⟩

Goal state after: