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

Goal state before:
pp: case inr.refine_2.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (1 ^ (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
⊢ MulOpposite.unop k * (a ^ n * a * e₂) = 0

Tactic:
mul_assoc,

Goal state after:
case inr.refine_2.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (1 ^ (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
⊢ MulOpposite.unop k * (a ^ n * (a * e₂)) = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * e' * ((1 - e₂) * e') = (1 - e₂) * e'

Tactic:
mul_assoc,

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * (e' * ((1 - e₂) * e')) = (1 - e₂) * e'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * e' * e₂ = 0

Tactic:
mul_assoc,

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e' : R
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * (e' * e₂) = 0
Module: Mathlib.GroupTheory.Congruence.BigOperators

Goal state before:
pp: ι : Type u_1
β : Type u_2
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : Zero β
c : Con M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), c (h i 0) 1
hf' : ∀ (i : ι), c (h' i 0) 1
H : ∀ (i : ι), c (h i (f i)) (h' i (g i))
⊢ (f.prod fun a b ↦ c.mk' (h a b)) = g.prod fun a b ↦ c.mk' (h' a b)

Tactic:
exact Finsupp.prod_congr_of_eq_on_union
    (fun _ _ => Quotient.sound <| H _)
    (fun _ _ => Quotient.sound <| hf _) (fun _ _ => Quotient.sound <| hf' _)

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
l : ℕ
hl : ↑l ≤ ↑k
hx : x ∈ ((f - μ • 1) ^ l).ker
⊢ x ∈ ((f - μ • 1) ^ k).ker

Tactic:
simp only [Nat.cast_le] at hl

Goal state after:
case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
l : ℕ
hx : x ∈ ((f - μ • 1) ^ l).ker
hl : l ≤ k
⊢ x ∈ ((f - μ • 1) ^ k).ker
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I : TwoSidedIdeal (Matrix n n R)
i j : n
r : R
h : r ∈ ↑(equivMatrix.symm I)
⊢ single i j r ∈ I

Tactic:
simpa using! h i j

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
⊢ MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)

Tactic:
intro x hx
  simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
  rcases hx with ⟨l, hl, hx⟩
  replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
  use l, hl
  rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ True ∧ e * r * e * e = e * r * e

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
r : R
⊢ True ∧ e * (r * (e * e)) = e * (r * e)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
⊢ ∑ x, r * e x * e x = r

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
⊢ ∑ x, r * (e x * e x) = r
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun x ↦ e i * x * e i) r' = ↑(r i)
⊢ e i * r' * e i * e i = e i * r' * e i

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun x ↦ e i * x * e i) r' = ↑(r i)
⊢ e i * (r' * (e i * e i)) = e i * (r' * e i)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁴ : CommSemiring R
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Module R M
ι : Type w
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
by
  classical
  rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
    traceAux_eq R b b.reindexFinsetRange]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * g * h) = (trace R M) (h * f * g)

Tactic:
LinearMap.trace_mul_comm,

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (h * (f * g)) = (trace R M) (h * f * g)
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * x * x⁻¹ = (x ^ n)⁻¹ * x⁻¹ * x

Tactic:
mul_assoc,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * (x * x⁻¹) = (x ^ n)⁻¹ * x⁻¹ * x
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * x⁻¹ * x

Tactic:
mul_assoc,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n✝ : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
n : ℕ
h : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x ^ n)⁻¹ * 1 = (x ^ n)⁻¹ * (x⁻¹ * x)
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = f '' Icc (a + c) (a + c + -c)

Tactic:
add_neg_cancel_right

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = f '' Icc (a + c) a
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : 0 < c
⊢ f '' uIcc a (a + c) = range f

Tactic:
| inr hc =>

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

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
⊢ ∀ (b : α) (a : FreeMonoid α),
    (a = 1 ∨ ∃ y, toFreeMonoid y = a) → FreeMonoid.of b * a = 1 ∨ ∃ y, toFreeMonoid y = FreeMonoid.of b * a

Tactic:
by
    rintro b _ (rfl | ⟨y, rfl⟩)
    · exact Or.inr ⟨of b, by simp⟩
    · exact Or.inr ⟨of b * y, by simp⟩

Goal state after:
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
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (integralClosure (↥S) A).toSubring ≤ T ↔ ofClass S ≤ T

Tactic:
rw [integralClosure_le_iff, Subtype.forall, SetLike.le_def]; rfl

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

Goal state before:
pp: case right
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
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A x ⟨y, hy⟩ * (algebraMap R A) y' = (algebraMap R A) x'

Tactic:
rw [mul_comm, IsLocalization.mul_mk'_eq_mk'_of_mul]

Goal state after:
case right
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
x y : R
hy : y ∈ M
x' y' : R
hx' : x = gcd x y * x'
hy' : y = gcd x y * y'
hu : IsUnit (gcd x' y')
⊢ mk' A (y' * x) ⟨y, hy⟩ = (algebraMap R A) x'
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
s : S
x : ℍ[R,c₁,c₂,c₃]
⊢ s • x = { toFun := fun s ↦ ↑((algebraMap S R) s), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } s * x

Tactic:
by ext <;> simp [Algebra.smul_def]

Goal state after:
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 y * star x)

Tactic:
mul_assoc,

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: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a⁻¹ • b ∈ s ↔ b ∈ a • s

Tactic:
by
  rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a⁻¹ • s ↔ a • b ∈ s

Tactic:
by
  rw [← smul_mem_smul_finset_iff a, smul_inv_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #↑Set.univ = #R

Tactic:
rw [mk_univ_quaternionAlgebra, pow_four]

Goal state after:
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 : ℕ
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

Tactic:
mul_assoc,

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.GroupWithZero.Submonoid.Instances

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
y : G
hy : f y = ↑x
⊢ (↑x)⁻¹ ∈ MonoidHom.mrange f

Tactic:
use y⁻¹

Goal state after:
case h
G : Type u_1
H : Type u_2
inst✝¹ : GroupWithZero G
inst✝ : GroupWithZero H
f : G →*₀ H
x : ↥(MonoidHom.mrange f)
y : G
hy : f y = ↑x
⊢ f y⁻¹ = (↑x)⁻¹
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ˣ
y : A
hy : f y = ↑a✝⁻¹
⊢ a✝ ∈ ↑f.valueMonoid

Tactic:
use y⁻¹

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✝⁻¹
⊢ f y⁻¹ = ↑a✝
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
⊢ f.valueMonoid ≤ Submonoid.closure (↑f.valueMonoid ∪ (↑f.valueMonoid)⁻¹)

Tactic:
simp [Submonoid.closure_union]

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

Goal state before:
pp: case refine_1.mul
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y c d : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
hd : d ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
u : A
hu : f u ≠ 0
a : A
ha : f u * ↑c = f a
v : A
hv : f v ≠ 0
b : A
hb : f v * ↑d = f b
⊢ f (u * v) * ↑(c * d) = f (a * b)

Tactic:
simpa [map_mul, Units.val_mul, ← hb, ← ha] using mul_mul_mul_comm ..

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        0) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        0)

Tactic:
simp <;> lia

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
i : Fin 2
⊢ ↑((Hom.toOrderHom
          (mkHom
              {
                toFun := fun x ↦
                  match x with
                  | 0 => 0
                  | 1 => Fin.last l,
                monotone' := ⋯ } ≫
            mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ }))
        1) =
    ↑((Hom.toOrderHom
          (mkHom
            {
              toFun := fun x ↦
                match x with
                | 0 => ⟨j, ⋯⟩
                | 1 => ⟨j + l, ⋯⟩,
              monotone' := ⋯ }))
        1)

Tactic:
simp <;> lia

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

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

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

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Epi f
⊢ IsIso f ↔ n.len = m.len

Tactic:
refine ⟨fun _ ↦ len_eq_of_isIso f, fun h ↦ ?_⟩
  obtain rfl : n = m := by aesop
  rw [epi_iff_surjective] at hf
  exact isIso_of_bijective ⟨by rwa [Finite.injective_iff_surjective], hf⟩

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

Goal state before:
pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
rw [← epi_iff_surjective]
      infer_instance

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

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

Tactic:
image_eq_range

Goal state after:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.ι ≫ f) ≤ range (A.ι ≫ f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.op.N
⊢ opObjEquiv x.simplex ∈ X.nonDegenerate x.dim

Tactic:
simpa only [opObjEquiv_mem_nonDegenerate_iff] using x.nonDegenerate

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₂
x : Fin (⦋n⦌.len + 1)
hf₁ : SplitEpi f₁
hf₁' : (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x

Tactic:
dsimp at hf₁'

Goal state after:
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₂
x : Fin (⦋n⦌.len + 1)
hf₁ : SplitEpi f₁
hf₁' : (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x
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₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
hα₂ : Monotone α
⊢ SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ } ≫ f₁ = 𝟙 ⦋m⦌

Tactic:
by ext : 3; apply hα₁

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

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

Tactic:
rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]
    simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : ComposableArrows C 0
e₀₁ : Edge x₀ x₁
e₁₂ : Edge x₁ x₂
e₀₂ : Edge x₀ x₂
h : e₀₁.CompStruct e₁₂ e₀₂
⊢ homEquiv e₀₁ ≫ homEquiv e₁₂ = homEquiv e₀₂

Tactic:
by
  obtain ⟨x₀, rfl⟩ := nerveEquiv.symm.surjective x₀
  obtain ⟨x₁, rfl⟩ := nerveEquiv.symm.surjective x₁
  obtain ⟨x₂, rfl⟩ := nerveEquiv.symm.surjective x₂
  obtain ⟨f₀₁, rfl⟩ := edgeMk_surjective e₀₁
  obtain ⟨f₁₂, rfl⟩ := edgeMk_surjective e₁₂
  obtain ⟨f₀₂, rfl⟩ := edgeMk_surjective e₀₂
  convert! (nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩ <;> apply homEquiv_edgeMk

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ Monotone ![a, b]

Tactic:
Fin.monotone_iff_le_succ

Goal state after:
n : ℕ
a b : Fin (n + 1)
hab : a ≤ b
⊢ ∀ (i : Fin (unop (op ⦋1⦌)).len), ![a, b] i.castSucc ≤ ![a, b] i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ Monotone ![a, b, c]

Tactic:
Fin.monotone_iff_le_succ

Goal state after:
n : ℕ
a b c : Fin (n + 1)
hab : a ≤ b
hbc : b ≤ c
⊢ ∀ (i : Fin (unop (op ⦋2⦌)).len), ![a, b, c] i.castSucc ≤ ![a, b, c] i.succ
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₁₂
p q : ℤ
⊢ (p * q).negOnePow = (p * q).negOnePow * q.negOnePow * q.negOnePow

Tactic:
mul_assoc,

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 = (p * q).negOnePow * (q.negOnePow * q.negOnePow)
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₃)
i₁₂ : ρ₁₂.I₁₂
i₃ : I₃
x✝ : ↑(p' ⁻¹' {(i₁₂, i₃)})
i₁ : I₁
i₂ : I₂
i₃' : I₃
hi : (i₁, i₂, i₃') ∈ p' ⁻¹' {(i₁₂, i₃)}
⊢ (fun x ↦
        match x with
        | ⟨(i₁, i₂), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(i₁, i₂, i₃'), hi⟩ => ⟨(i₁, i₂), ⋯⟩)
        ⟨(i₁, i₂, i₃'), hi⟩) =
    ⟨(i₁, i₂, i₃'), hi⟩

Tactic:
obtain rfl : i₃ = i₃' := by cat_disch
        rfl

Goal state after: