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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
i : I
⊢ f (e' i * e' i - e' i) = 0

Tactic:
simp [he', (he.1.1 i).eq]

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

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ) ≤ (f.genEigenspace μ) ↑(finrank K V)

Tactic:
apply genEigenspace_le_genEigenspace_finrank f μ

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
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
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R M) (↑(e ≪≫ₗ e.symm) ∘ₗ f) = (trace R M) f

Tactic:
LinearEquiv.self_trans_symm,

Goal state after:
case pos
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
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R M) (↑(LinearEquiv.refl R M) ∘ₗ f) = (trace R M) 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
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ ((f - μ • 1) ^ l).ker
⊢ ∃ l, ↑l ≤ k ∧ m ∈ ((t • f - (t * μ) • 1) ^ l).ker

Tactic:
← exists_prop,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), m ∈ ((f - μ • 1) ^ l).ker
⊢ ∃ l, ∃ (_ : ↑l ≤ k), m ∈ ((t • f - (t * μ) • 1) ^ l).ker
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
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
hg : IsNilpotent (g - (algebraMap R (End R M)) μ)
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
set n := g - algebraMap R _ μ

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f
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
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ ((algebraMap R (End R M)) μ + n)) = μ * (trace R M) f

Tactic:
comp_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ (algebraMap R (End R M)) μ + f ∘ₗ n) = μ * (trace R M) f
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
⊢ Function.Bijective ⇑(algebraMap R S)

Tactic:
have : Module.Finite R S := finite_of_finrank_pos (by grind)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
this : Module.Finite R S
⊢ Function.Bijective ⇑(algebraMap R S)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right.inl
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
rw [(h.pow_pow i j).eq, Module.End.mul_apply, Module.End.pow_map_zero_of_le hi hl₁, map_zero]

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 : End R M
μ : R
⊢ (-f).HasEigenvalue μ ↔ f.HasEigenvalue (-μ)

Tactic:
by
  simp only [hasEigenvalue_iff, eigenspace_def]
  rw [← LinearMap.ker_neg]
  simp [add_comm]

Goal state after:
Module: Mathlib.Algebra.Field.ZMod

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1

Tactic:
apply coe_mul_inv_eq_one

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ k.Coprime p
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
m : M₃
hm : i₃ m = 1
⊢ m = 1

Tactic:
obtain ⟨x, rfl⟩ := (hf₂ m).mp <| by
    suffices h : i₄ (f₃ m) = 1 by rwa [map_eq_one_iff _ hi₄] at h
    simp [← show g₃ (i₃ m) = i₄ (f₃ m) by simpa using DFunLike.congr_fun hc₃ m, hm]

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
⊢ f₂ x = 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

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

Tactic:
FreeGroup.mk_toWord

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = x * y
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
a : M₁
hm : i₃ (f₂ (f₁ a)) = 1
⊢ f₂ (f₁ a) = 1

Tactic:
hf₁.apply_apply_eq_one

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
a : M₁
hm : i₃ (f₂ (f₁ a)) = 1
⊢ 1 = 1
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
⊢ Function.Surjective ⇑i₁

Tactic:
refine surjective_of_surjective_of_surjective_of_injective (0 : Unit →ₗ[R] M₁) f₁ f₂
    (0 : Unit →ₗ[R] N₁) g₁ g₂ 0 i₁ i₂ i₃ (by simp) hc₁ hc₂ hf₁ (fun y ↦ ?_) hg₁
    (fun | .unit => ⟨0, rfl⟩) hi₂ hi₃

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₂ : Function.Surjective ⇑i₂
hi₃ : Function.Injective ⇑i₃
hg₀ : Function.Injective ⇑g₁
y : N₁
⊢ g₁ y = 0 ↔ y ∈ Set.range ⇑0
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : WithOne (FreeSemigroup α)
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) x) = x

Tactic:
induction x with
    | one => simp
    | coe a => induction a with simp_all

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

Goal state before:
pp: case zero
M : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : AddCommGroup G
h : M
R : Type u_3
inst✝¹ : Monoid R
inst✝ : DistribMulAction R G
r : R
f : M → G
⊢ Δ_[h]^[0] (r • f) = r • Δ_[h]^[0] f

Tactic:
simp only [iterate_zero, id_eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ s / 0 ⊆ 0

Tactic:
simp [subset_iff, mem_div]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
s : Finset α
⊢ 0 / s ⊆ 0

Tactic:
simp [subset_iff, mem_div]

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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ closure (v '' IsMulIndecomposable.baseOf v f) = closure (v '' univ)

Tactic:
refine le_antisymm (closure_mono (image_mono <| by simp)) ((closure_le _).mpr ?_)

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
⊢ v '' univ ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
x✝ : j ∈ t
⊢ v j = v k⁻¹ * v i

Tactic:
by simp [hv_inv, hk]

Goal state after:
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
p₁ : B ⟶ Y := ofHom { toFun := fun b ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y := ofHom { toFun := fun b ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
h : (ConcreteCategory.hom p₁) m = (ConcreteCategory.hom p₂) m
⊢ False

Tactic:
simp [Y, p₁, p₂, ConcreteCategory.hom_ofHom] at h

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
h_X : P.X = Q.X
h_p : P.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ P = Q

Tactic:
cases P

Goal state after:
case mk
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Q : Karoubi C
X✝ : C
p✝ : X✝ ⟶ X✝
idem✝ : p✝ ≫ p✝ = p✝
h_X : { X := X✝, p := p✝, idem := idem✝ }.X = Q.X
h_p : { X := X✝, p := p✝, idem := idem✝ }.p ≫ eqToHom h_X = eqToHom h_X ≫ Q.p
⊢ { X := X✝, p := p✝, idem := idem✝ } = Q
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: 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' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom

Tactic:
slice_rhs 1 2 => rw [φ.hom_inv_id]

Goal state after:
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' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = (𝟙 X' ≫ p) ≫ φ.hom
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 g : P ⟶ Q
⊢ P.p ≫ (f.f ≫ Q.p + g.f ≫ Q.p) = f.f + g.f

Tactic:
comp_add,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g : P ⟶ Q
⊢ P.p ≫ f.f ≫ Q.p + P.p ≫ g.f ≫ Q.p = f.f + g.f
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ ((toKaroubi C).obj Y).p ≫ i ≫ P.p = i

Tactic:
simp [← Category.assoc, h₁, ← h₂]

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

Goal state before:
pp: case h
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ Nonempty ((toKaroubi C).obj Y ≅ P)

Tactic:
exact
      Nonempty.intro
        { hom := ⟨i, by simp [← Category.assoc, h₁, ← h₂]⟩
          inv := ⟨e, by simp [Category.assoc, h₁, ← h₂]⟩ }

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.δ₀Iter (i + 1) h = X.δ₀Iter i ⋯ ≫ X.δ 0

Tactic:
dsimp [δ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_succ' _ h]

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

Goal state before:
pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
have hy : x = y.succ := (Fin.succ_pred x _).symm

Goal state after:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
hy : x = y.succ
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : SimplexCategory
⊢ Finite (X.obj (Opposite.op n))

Tactic:
induction n using SimplexCategory.rec with | _ n

Goal state after:
case mk
X : SSet
inst✝ : X.Finite
n : ℕ
⊢ Finite (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x : X.S
y : X.N
hy : x.toN = y
⊢ ∃! f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
by
  obtain ⟨n, x, hx, rfl⟩ := x.mk_surjective
  obtain ⟨m, f, _, z, rfl⟩ := X.exists_nonDegenerate x
  obtain rfl : y = N.mk _ z.2 := by
    rw [toN_eq_iff] at hy
    rw [← N.subcomplex_injective_iff, hy]
    exact subcomplex_eq_of_epi _ _ f rfl
  refine existsUnique_of_exists_of_unique ⟨f, inferInstance, rfl⟩
    (fun f₁ f₂ ⟨_, hf₁⟩ ⟨_, hf₂⟩ ↦ unique_nonDegenerate_map _ _ _ _ hf₁.symm _ _ hf₂.symm)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ homEquiv (edgeMk f₀₁) ≫ homEquiv (edgeMk f₁₂) = homEquiv (edgeMk f₀₂)

Tactic:
convert! (nerve.nonempty_compStruct_iff _ _ _).1 ⟨h⟩ <;> apply homEquiv_edgeMk

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

Goal state before:
pp: n : SimplexCategory
⊢ (stdSimplex.obj n).Finite

Tactic:
induction n using SimplexCategory.rec with | _ n

Goal state after:
case mk
n : ℕ
⊢ Δ[n].Finite
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 * 1 = q.negOnePow * ((p + 1) * q).negOnePow

Tactic:
rw [mul_one, ← Int.negOnePow_add, add_comm q, add_mul, one_mul, Int.negOnePow_add,
      Int.negOnePow_add, mul_assoc, Int.units_mul_self, mul_one]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K ⟶ L
i : I₂
⊢ ∀ (i_1 j : I₁), c₁.Rel i_1 j → (f.f i_1).f i ≫ (L.flip.X i).d i_1 j = (K.flip.X i).d i_1 j ≫ (f.f j).f i

Tactic:
by intros; simp

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      0 =
    (((dNext 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD 0) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f 0

Tactic:
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_zero_chainComplex]
          simp [dsimp% ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
            (C := AlternatingFaceMapComplex.obj X.left), s_comp_δ₀, s₀_comp_δ₁]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Tactic:
by_cases h : c₂.Rel i₂ (c₂.next i₂)
  · simp [totalAux.d₂_eq' _ c₁₂ i₁ h]
  · simp [d₂_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

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

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.π c₁ c (i₂, i₁) = j

Tactic:
by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
x✝ : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ (L.D₁ c₁₂ i₁₂ i₁₂' + L.D₂ c₁₂ i₁₂ i₁₂') =
    (K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂') ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'

Tactic:
comp_add,

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
x✝ : c₁₂.Rel i₁₂ i₁₂'
⊢ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₁ c₁₂ i₁₂ i₁₂' +
      GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ ≫ L.D₂ c₁₂ i₁₂ i₁₂' =
    (K.D₁ c₁₂ i₁₂ i₁₂' + K.D₂ c₁₂ i₁₂ i₁₂') ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + x = n₀'
h₁ : n₁ + x = n₁'
⊢ ((shiftFunctor₁ C x).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₁XIso x n₁ n₁' h₁).hom =
    x.negOnePow • (K.totalShift₁XIso x n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
by_cases h : (up ℤ).Rel n₀ n₁
  · apply total.hom_ext
    intro p q hpq
    dsimp at h hpq
    dsimp [totalShift₁XIso]
    rw [ι_D₂_assoc, Linear.comp_units_smul, ι_totalDesc_assoc, ι_D₂,
      ((shiftFunctor₁ C x).obj K).d₂_eq _ _ rfl _ (by dsimp; lia),
      K.d₂_eq _ _ rfl _ (by dsimp; lia), smul_smul,
      Linear.units_smul_comp, Category.assoc, ι_totalDesc]
    dsimp
    congr 1
    rw [add_comm p, Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
  · rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
    grind [up_Rel]

Goal state after: