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
⊢ (trace R M) (g ∘ₗ f) = 0

Tactic:
have hfg : ∀ μ,
      MapsTo (g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) :=
    fun μ ↦ (f.mapsTo_maxGenEigenspace_of_comm h_comm μ).comp
      (f.mapsTo_maxGenEigenspace_of_comm rfl μ)

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 μ)
⊢ (trace R M) (g ∘ₗ f) = 0
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 : ℕ∞
⊢ Disjoint (⨆ l, (f.genEigenspace μ₁) ↑↑l) (⨆ l_1, (f.genEigenspace μ₂) ↑↑l_1)

Tactic:
simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]

Goal state after:
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 : ℕ∞
⊢ ∀ (i : { l // ↑l ≤ k }) (i_1 : { l_1 // ↑l_1 ≤ l }), Disjoint ((f.genEigenspace μ₁) ↑↑i) ((f.genEigenspace μ₂) ↑↑i_1)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ (f.toLinearMap ∘ₗ ↑R (inrHom A A)) a = (g.toLinearMap ∘ₗ ↑R (inrHom A A)) a

Tactic:
change f (inr a) = g (inr a)

Goal state after:
R : Type u_1
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f g : A[ε] →ₐ[R] B
hinl : f.comp (inlAlgHom R A A) = g.comp (inlAlgHom R A A)
hinr :
  f.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε) = g.toLinearMap ∘ₗ ↑R (LinearMap.toSpanSingleton A A[ε] ε)
a : A
⊢ f (inr a) = g (inr a)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
⊢ f = g

Tactic:
by
  let : Algebra R R' := by
    letI := f.toAlgebra
    exact Algebra.compHom _ (algebraMap R R[ε])
  let f' : R[ε] →ₐ[R] R' :=
    { toRingHom := f
      commutes' _ := rfl }
  let g' : R[ε] →ₐ[R] R' :=
    { toRingHom := g
      commutes' r := (DFunLike.congr_fun h₀ r).symm }
  exact congr_arg AlgHom.toRingHom (show f' = g' from algHom_ext hε)

Goal state after:
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 (MulOpposite.op a • 1) = (↑fg).2 (a • 1)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 (MulOpposite.op a • 1) = (↑fg).2 (a * 1)
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).2 (x • 1) = (↑fg).2 x

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
x : A
⊢ (↑fg).2 (x * 1) = (↑fg).2 x
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
k : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ iSupIndep fun x ↦ (f.genEigenspace x) k

Tactic:
by
    simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]
    exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)

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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ (∃ l, ↑l ≤ k ∧ p.subtype x ∈ (f.genEigenspace μ) ↑l) ↔ ∃ l, ↑l ≤ k ∧ p.subtype x ∈ ((f - μ • 1) ^ l).ker

Tactic:
mem_genEigenspace_nat

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
V : Type u_7
W : Type u_8
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup W
inst✝² : Module K W
F : Type u_9
inst✝¹ : EquivLike F (End K V) (End K W)
inst✝ : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w✝ : V ≃ₗ[K] W
h : ↑f = LinearEquiv.conjAlgEquiv K w✝
⊢ ?m.65

Tactic:
simpa using congr($h x)

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: K : Type u_6
m : Type u_7
n : Type u_8
inst✝⁶ : Field K
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
F : Type u_9
inst✝¹ : EquivLike F (Matrix m m K) (Matrix n n K)
inst✝ : AlgEquivClass F K (Matrix m m K) (Matrix n n K)
f : F
x : Matrix m m K
⊢ (f x).trace = x.trace

Tactic:
by
  simpa [toMatrixAlgEquiv', Matrix.toLinAlgEquiv'] using
    LinearMap.trace_map ((Matrix.toLinAlgEquiv'.symm.trans
      (AlgEquivClass.toAlgEquiv f)).trans Matrix.toLinAlgEquiv') x.toLin'

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

Goal state before:
pp: G : Type u
inst✝² : Mul G
inst✝¹ : Inv G
inst✝ : One G
assoc : ∀ (a b c : G), a * b * c = a * (b * c)
mul_one : ∀ (a : G), a * 1 = a
mul_inv_cancel : ∀ (a : G), a * a⁻¹ = 1
a : G
⊢ a⁻¹ * a * 1 = a⁻¹ * a * (a⁻¹ * a * (a⁻¹ * a)⁻¹)

Tactic:
rw [mul_inv_cancel]

Goal state after:
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₄
⊢ Function.Injective ⇑i₃

Tactic:
injective_iff_map_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₃), i₃ a = 1 → a = 1
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ IsReduced L

Tactic:
IsReduced,

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) L
Module: Mathlib.Algebra.Free

Goal state before:
pp: α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ (toFreeSemigroup (x * y)).length = (x * y).length

Tactic:
rw [map_mul, FreeSemigroup.length_mul, hx, hy]

Goal state after:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + y.length = (x * y).length
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : IsEmpty X
⊢ #(FreeAlgebra R X) = Cardinal.lift.{v, u} #R

Tactic:
by
  simp [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq,
    MonoidAlgebra.cardinalMk_eq_lift_of_fintype]

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

Goal state before:
pp: α : Type u_1
⊢ Function.Injective ⇑toFreeMonoid

Tactic:
rintro ⟨x, xs⟩ ⟨y, ys⟩ h
  simp only [toFreeMonoid_mk_eq_cons, Equiv.apply_eq_iff_eq] at h
  simpa using h

Goal state after:
Module: Mathlib.Algebra.Group.Action.Sum

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
m : Monoid M
inst✝¹ : MulAction M α
inst✝ : MulAction M β
a b : M
x : α ⊕ β
⊢ (a * b) • x = a • b • x

Tactic:
by
    cases x
    exacts [congr_arg inl (mul_smul _ _ _), congr_arg inr (mul_smul _ _ _)]

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

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

Tactic:
by_cases hn' : n < f.natDegree
      · exact hfP _ (coe_lt_degree.mpr hn')
      · rw [f.coeff_eq_zero_of_natDegree_lt]
        · exact P.zero_mem
        · simp [Nat.lt_iff_le_and_ne, ← Nat.not_lt, hn', Ne.symm hn]

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

Goal state before:
pp: 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
n : ℕ
⊢ Δ_[h]^[n] (r • f) = r • Δ_[h]^[n] f

Tactic:
by
  induction n generalizing f with
  | zero => simp only [iterate_zero, id_eq]
  | succ n IH => simp only [iterate_succ_apply, fwdDiff_const_smul, IH]

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

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

Tactic:
rw [mul_comm]
  exact npow_mul x n m

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
⊢ i < n

Tactic:
have := mem_range.1 hi

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this✝ : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range j
this : i < j
⊢ i < n
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ i < n

Tactic:
have := mem_range.1 hi

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this✝ : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
this : i < n
⊢ i < n
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] (Δ_[1]^[P.natDegree] fun x ↦ eval x P)) x = 0 x

Tactic:
P.fwdDiff_iter_degree_eq_factorial,

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
j : ℕ
hP : P.natDegree < P.natDegree + j + 1
⊢ Δ_[1]^[j] (Δ_[1] (P.leadingCoeff • ↑P.natDegree !)) x = 0 x
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset

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

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

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

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

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

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
y : Bˣ
⊢ y ∈ f.valueGroup ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x

Tactic:
rw [mem_valueGroup_iff_of_comm]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y : Bˣ
⊢ (∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑y = f x) ↔ ∃ a, f a ≠ 0 ∧ ∃ x, f x ≠ 0 ∧ f a * ↑y = f x
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ (Fin.castSucc 0) ≫ X.δ i.succ = 0

Tactic:
← X.δ_comp_δ (Fin.zero_le i.succ)

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ i.succ.succ ≫ X.δ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ : SimplexCategory
f g : Δ ⟶ ⦋0⦌
⊢ f = g

Tactic:
by ext : 3; apply Subsingleton.elim (α := Fin 1)

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}
⊢ ∑ x ∈ Finset.univ ×ˢ Finset.univ, ((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1) = 0

Tactic:
rw [Finset.univ_product_univ, ← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero,
    ← Finset.sum_neg_distrib]

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}
⊢ ∑ 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.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
Fin.predAbove_of_le_castSucc _ _ hjk,

Goal state after:
case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (k.castPred ⋯).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k = i.succAbove (j.predAbove k)

Tactic:
Fin.predAbove_of_le_castSucc _ _ hjk,

Goal state after:
case inl.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ k = i.succAbove (k.castPred ⋯)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.σ i ≫ X.δ i.castSucc = 𝟙 (X _⦋n⦌)

Tactic:
dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_self, op_id, X.map_id]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X✝ Y✝ : Augmented C
η : X✝ ⟶ Y✝
n✝ : SimplexCategoryᵒᵖ
⊢ ((𝟭 (SimplicialObject D)).map (whiskerRight η.left F) ≫
          { left := ((whiskering C D).obj F).obj (drop.obj Y✝), right := F.obj (point.obj Y✝),
              hom := whiskerRight Y✝.hom F ≫ (constComp SimplexCategoryᵒᵖ Y✝.right F).hom }.hom).app
      n✝ =
    ({ left := ((whiskering C D).obj F).obj (drop.obj X✝), right := F.obj (point.obj X✝),
              hom := whiskerRight X✝.hom F ≫ (constComp SimplexCategoryᵒᵖ X✝.right F).hom }.hom ≫
          (const D).map (F.map η.right)).app
      n✝

Tactic:
simp [← Functor.map_comp, w_app]

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

Goal state before:
pp: X : NonemptyFinLinOrd
aux : Fintype.card ↑X.toLinOrd = Fintype.card ↑X.toLinOrd - 1 + 1
f : Fin (Fintype.card ↑X.toLinOrd - 1 + 1) ≃o ↑X.toLinOrd := monoEquivOfFin (↑X.toLinOrd) aux
hf : StrictMono ⇑(Finset.univ.orderEmbOfFin aux)
⊢ InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f, monotone' := ⋯ }) ≫
      InducedCategory.homMk (LinOrd.ofHom { toFun := ⇑f.symm, monotone' := ?m.113 }) =
    𝟙 (skeletalFunctor.obj ⦋Fintype.card ↑X.toLinOrd - 1⦌)

Tactic:
by ext; apply f.symm_apply_apply

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

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

Tactic:
Fin.predAbove_of_le_castSucc i x h'

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (x.castPred ⋯))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case h
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
i : Fin (n + 2)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = θ' ≫ δ i
this✝ : Mono (θ' ≫ δ i)
this : Mono θ'
⊢ θ = δ i

Tactic:
rw [h, eq_id_of_mono θ', Category.id_comp]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
k : Fin (n + 1)
⊢ i.succAbove k = j.succAbove k

Tactic:
exact congr($hij k)

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
k : Fin (n + 1 + 1)
⊢ i.predAbove k = j.predAbove k

Tactic:
exact congr($hij k)

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: 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'
⊢ (ofSection x).image f = ofSection ((ConcreteCategory.hom (f.app X)) x)

Tactic:
apply le_antisymm
  · rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]
    exact ⟨𝟙 X, by simp⟩
  · simp only [ofSection_le_iff, image_obj, Set.mem_image]
    exact ⟨x, mem_ofSection_obj x, rfl⟩

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

Goal state before:
pp: X : SSet
x y : X.N
h : x < y
⊢ x.dim < y.dim

Tactic:
obtain h' | h' := (dim_le_of_le h.le).lt_or_eq

Goal state after:
case inl
X : SSet
x y : X.N
h : x < y
h' : x.dim < y.dim
⊢ x.dim < y.dim

case inr
X : SSet
x y : X.N
h : x < y
h' : x.dim = y.dim
⊢ x.dim < y.dim
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.preimage (inv f) = A.image f

Tactic:
ext _ x

Goal state after:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
⊢ x ∈ (A.preimage (inv f)).obj x✝ ↔ x ∈ (A.image f).obj x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
trans N.mk x hx = N.mk y hy
  · exact (N.ext_iff (N.mk x hx) (N.mk y hy)).symm
  · simp only [le_antisymm_iff]
    rfl

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

Tactic:
by
  rw [← degenerate_iff_of_isIso (Subcomplex.toRange f) x,
    Subcomplex.mem_degenerate_iff]
  simp

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

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
simp_all [-Nat.not_even_iff_odd]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i j : ℕ
hij : (ComplexShape.down ℕ).Rel i j
h✝ : ¬Even i
⊢ f ≫ (HomologicalComplex.alternatingConst Y ⋯ ⋯ ⋯).d i j = (HomologicalComplex.alternatingConst X ⋯ ⋯ ⋯).d i j ≫ f

Tactic:
simp_all [-Nat.not_even_iff_odd]

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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow = q.negOnePow * ((p + 1) * q).negOnePow

Tactic:
← Int.negOnePow_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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow = (q + (p + 1) * q).negOnePow