mathlib-initiative/mathlib-tactics huggingface dataset:
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:
(he.idem i).eq

Goal state after:
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 j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ e i * e j * r' * e j * e i = 0

Tactic:
he.ortho ne.symm,

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 j : I
a✝ : j ∈ Finset.univ
ne : j ≠ i
r' : R
eq : (fun x ↦ e j * x * e j) r' = ↑(r j)
⊢ 0 * r' * e j * e i = 0
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₂ : R
i : I
⊢ e i * r₁ * r₂ * e i = e i * e i * r₁ * r₂ * e i

Tactic:
(he.idem i).eq

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x ↦
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite R ↥(N' i)
_i2 : ∀ (i : ↥s), Free R ↥(N' i)
⊢ ∑ i, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) = ∑ i ∈ s, (trace R ↥(N i)) (restrict f ⋯)

Tactic:
← s.sum_coe_sort

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : ι → Submodule R M
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
s : Finset ι
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
p : Submodule R M
hp : p = ⨆ i ∈ s, N i
hp' : MapsTo ⇑f ↑p ↑p
N' : ↥s → Submodule R ↥p := fun i ↦ Submodule.comap p.subtype (N ↑i)
h : IsInternal N'
hf' : ∀ (i : ↥s), MapsTo ⇑(restrict f hp') ↑(N' i) ↑(N' i)
e : (i : ↥s) → ↥(N' i) ≃ₗ[R] ↥(N ↑i) :=
  fun x ↦
    match x with
    | ⟨i, hi⟩ => Submodule.comapSubtypeEquivOfLe ⋯
_i1 : ∀ (i : ↥s), Module.Finite R ↥(N' i)
_i2 : ∀ (i : ↥s), Free R ↥(N' i)
⊢ ∑ i, (trace R ↥(N' i)) ((restrict f hp').restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (restrict f ⋯)
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
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
this : IsNilpotent (f₂ - f₁)
x✝ : ↥p
⊢ ↑((f₂ - f₁) x✝) = ↑(((algebraMap R (End R ↥p)) (μ₁ - μ₂)) x✝)

Tactic:
simp [f₁, f₂]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (mk [(a, true)] ^ n).toWord = List.replicate n (a, true)

Tactic:
pow_mk,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ (mk (List.replicate n [(a, true)]).flatten).toWord = List.replicate n (a, true)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (x * y).toWord

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
this : x * y = mk (x.toWord ++ y.toWord)
⊢ Red (x.toWord ++ y.toWord) (mk (x.toWord ++ y.toWord)).toWord
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
have hX := mk_freeMonoid X

Goal state after:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: α : Type u
⊢ #(FreeRing α) = max #α ℵ₀

Tactic:
by
  cases isEmpty_or_nonempty α <;> simp [FreeRing]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : n = 0
⊢ IsUnit g ∨ IsUnit h

Tactic:
right; exact hn0 hn

Goal state after:
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⟩
    refine ⟨inj, by simp_all, ?_⟩
    rintro ⟨y, rfl⟩
    apply isIntegral_algebraMap

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
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
⊢ IsUnit y

Tactic:
isUnit_iff_dvd_one,

Goal state after:
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
⊢ y ∣ 1
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
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ⟨y, y_mem⟩ • x = ↑⟨y, y_mem⟩ • x

Tactic:
Submonoid.mk_smul

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
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ y • x = ↑⟨y, y_mem⟩ • x
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ ↑(closure s) = s ∪ univ * s

Tactic:
rw [this]

Goal state after:
M : Type u_1
inst✝ : Semigroup M
s : Set M
I : SemigroupIdeal M := { carrier := s ∪ univ * s, smul_mem' := ⋯ }
this : closure s = I
⊢ ↑I = s ∪ univ * s
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)

Tactic:
ppow_add,

Goal state after:
case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ k * (x ^ m) ^ 1
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * k + m * 1) = (x ^ m) ^ k * x ^ m

Tactic:
ppow_add,

Goal state after:
case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * k) * x ^ (m * 1) = (x ^ m) ^ k * x ^ m
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 + 1) = x ^ ↑(k + 1)

Tactic:
ppow_add,

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 ^ 1 = x ^ ↑(k + 1)
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 + ↑1)

Tactic:
pow_add,

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 ^ ↑1
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
ih : x ^ (m * n) = (x ^ m) ^ n
⊢ x ^ (m * (n + 1)) = (x ^ m) ^ (n + 1)

Tactic:
rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i

Tactic:
exact fun s hs ↦ mul_mem (hx s hs) (hy s hs)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : GroupWithZero α
inst✝ : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (s.PairwiseDisjoint fun x ↦ x • t) ↔ Set.InjOn (fun p ↦ p.1 • p.2) (s ×ˢ ↑t)

Tactic:
by
  simp_rw [← pairwiseDisjoint_coe, coe_smul_finset]
  exact Set.pairwiseDisjoint_image_right_iff (fun a ha => MulAction.injective₀ (hs a ha))

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ mk f r₁ s₁ hr₁ hs₁ = mk f r₂ s₂ hr₂ hs₂ ↔ f (r₁ * s₂) = f (r₂ * s₁)

Tactic:
simp only [mk, Subtype.mk.injEq, map_mul]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ (Units.mk0 (f r₁) hr₁)⁻¹ * Units.mk0 (f s₁) hs₁ = (Units.mk0 (f r₂) hr₂)⁻¹ * Units.mk0 (f s₂) hs₂ ↔
    f r₁ * f s₂ = f r₂ * f s₁
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ HasKernel p

Tactic:
convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ p = 𝟙 X - (𝟙 X - p)
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ (eqToHom ⋯).f = P.p ≫ eqToHom ⋯

Tactic:
simp only [eqToHom_refl, Karoubi.id_f, comp_id]

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

Goal state before:
pp: case h.left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map i ≫ ε.functor.map e = 𝟙 (ε.functor.obj Y)

pp: case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom

Tactic:
· rw [← ε.functor.map_comp, h₁, ε.functor.map_id]

Goal state after:
case h.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ⋯
Y : C
i : Y ⟶ ε.inverse.obj X'
e : ε.inverse.obj X' ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = ε.inverse.map p
⊢ ε.functor.map e ≫ ε.functor.map i = φ.inv ≫ p ≫ φ.hom
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

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

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

Goal state before:
pp: case a
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ∃ x x_1, (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) x_1 ∧ ¬x = x_1
x y : Fin (n + 2)
h₁ : (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y
h₂ : x < y
⊢ (Hom.toOrderHom θ) (x.castPred ⋯).succ ≤ (Hom.toOrderHom θ) (x.castPred ⋯).castSucc

Tactic:
· rw [Fin.castSucc_castPred, h₁]
    exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective σ

Tactic:
by
  intro i j hij
  rw [← Fin.predAbove_left_inj]
  ext k : 1
  exact congr($hij k)

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

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

Tactic:
Fin.lt_def

Goal state after:
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : m + j = n),
    j < ↑i → ↑i = ↑i' + j → δ i ≫ σ₀Iter j ⋯ = σ₀Iter j ⋯ ≫ δ i'
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : m + (j + 1) = n
hi' : j + 1 < ↑i
hi'' : ↑i = ↑i' + (j + 1)
⊢ ↑(Fin.castSucc 0) < ↑i'
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ x ∈ ((ofSection ((ConcreteCategory.hom (f.app X)) x)).preimage f).obj X

Tactic:
preimage_obj,

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ x ∈ ⇑(ConcreteCategory.hom (f.app X)) ⁻¹' (ofSection ((ConcreteCategory.hom (f.app X)) x)).obj X
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
⊢ y ∈ (ofSimplex x).obj m ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) x = y

Tactic:
by
  dsimp [ofSimplex, Subfunctor.ofSection]
  aesop

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

Goal state before:
pp: case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ x ∈ ((ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).preimage f).obj (Opposite.op ⦋n⦌)

Tactic:
preimage_obj,

Goal state after:
case a
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ x ∈
    ⇑(ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) ⁻¹'
      (ofSimplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)).obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.op.N
⊢ { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk (opObjEquiv x.simplex) ⋯, invFun := fun y ↦ mk (opObjEquiv.symm y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
dsimp
    simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
    constructor
    · rintro ⟨f, hf⟩
      exact ⟨SimplexCategory.rev.map f, by simp [op_map, dsimp% hf]⟩
    · rintro ⟨f, hf⟩
      exact ⟨SimplexCategory.rev.map f, by simp [op_map, ← hf]⟩

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
⊢ Y.Finite

Tactic:
have := hasDimensionLT_of_epi f d

Goal state after:
X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
⊢ Y.Finite
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: case right.inl
n : ℕ
j : Fin (n + 2)
hj✝ : j ∈ {0}ᶜ
hj : ¬j = 0
⊢ ∃ a, (fun a ↦ ⟨(succAboveOrderEmb 0) a, ⋯⟩) a = ⟨j, hj✝⟩

pp: case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩

Tactic:
· exact ⟨j.pred hj, by simp⟩

Goal state after:
case right.inr
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ ∃ a, (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ yonedaEquiv (const x) = x

Tactic:
simp [yonedaEquiv, uliftYonedaEquiv]

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

Goal state before:
pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : j.succAbove m ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨j.succAbove m, hl⟩

Tactic:
obtain ⟨k, hk⟩ : m ∈ Set.range (i.castPred (Fin.ne_last_of_lt h)).succAbove := by
        grind [Fin.range_succAbove, compl_insert, Fin.succAbove, Fin.castPred]

Goal state after:
case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : j.succAbove m ∈ {i, j}ᶜ
k : Fin n
hk : (i.castPred ⋯).succAbove k = m
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨j.succAbove m, hl⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
⊢ Fin n ≃ ↥{i, j}ᶜ

Tactic:
by
    refine Equiv.ofBijective
      (fun k ↦ ⟨j.succAbove ((i.castPred (Fin.ne_last_of_lt h)).succAbove k), ?_⟩)
        ⟨fun _ _ hk ↦ ?_, fun ⟨l, hl⟩ ↦ ?_⟩
    · grind [compl_insert, mem_compl, Fin.succAbove, Fin.castPred]
    · exact ((Fin.succAboveOrderEmb (i.castPred (Fin.ne_last_of_lt h))).trans
        (Fin.succAboveOrderEmb j)).injective (by rwa [Subtype.ext_iff] at hk)
    · obtain ⟨m, rfl⟩ : l ∈ Set.range j.succAbove := by
        grind [Fin.range_succAbove, mem_compl, Fin.succAbove]
      obtain ⟨k, hk⟩ : m ∈ Set.range (i.castPred (Fin.ne_last_of_lt h)).succAbove := by
        grind [Fin.range_succAbove, compl_insert, Fin.succAbove, Fin.castPred]
      exact ⟨k, by simp [hk]⟩

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

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
· rintro ⟨j, hj⟩
      rw [nonDegenerateEquiv'_iff] at hj
      aesop

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
q : ℕ
⊢ (-1) ^ q = -(-1) ^ (q + 1)

Tactic:
pow_add,

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₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
q : ℕ
⊢ (-1) ^ q = -((-1) ^ q * (-1) ^ 1)
Module: Mathlib.Algebra.Homology.TotalComplex

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

Tactic:
· rw [K.D₂_shape c₁₂ _ _ h₂, comp_zero]

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

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

Tactic:
rw [K.D₁_shape c₁₂ _ _ h₁, K.D₂_shape c₁₂ _ _ h₁, zero_comp, zero_comp, neg_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c) * ↑(t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c)) * ↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
← Units.val_mul,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c * t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c)) * ↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom