mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (traceAux R ⋯.some) f = ((toMatrix b b) f).trace

Tactic:
← traceAux_def

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (traceAux R ⋯.some) f = (traceAux R b) f
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
⊢ (trace R M) f = ((toMatrix b b) f).trace

Tactic:
have : ∃ s : Finset M, Nonempty (Basis s R M) := ⟨s, ⟨b⟩⟩
  rw [trace, dif_pos this, ← traceAux_def]
  congr 1
  apply traceAux_eq

Goal state after:
Module: Mathlib.Algebra.DualNumber

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

Tactic:
← x.inl_fst_add_inr_snd_eq,

Goal state after:
R : Type u_1
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : TrivSqZeroExt A A
⊢ inl x.fst + inr x.snd ∈ (inlAlgHom R A A).range ⊔ R[ ε]
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case refine_2
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 : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ (g ^ l) (y + z) ∈ ↑(s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

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₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
h : Commute f₁ f₂
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
⊢ f₁ + f₂ - (μ₁ • 1 + μ₂ • 1) = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)

Tactic:
exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1)

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : traverse pure x = pure x
ih2 : traverse pure y = pure y
⊢ traverse pure (x * y) = pure (x * y)

Tactic:
by
        rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝ : Applicative m
F : α → m β
α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse pure (of x) = pure (of x)
ih2 : traverse pure y = pure y
⊢ traverse pure (of x * y) = pure (of x * y)

Tactic:
by
        rw [traverse_mul, ih1, ih2, seq_pure, map_pure, map_pure]

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
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
⊢ IsUnit g ∨ IsUnit h

Tactic:
by_cases hn : n = 0

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

case neg
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
Module: Mathlib.Algebra.Group.Action.Sigma

Goal state before:
pp: case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
fst✝ : ι
snd✝ : α fst✝
⊢ ⟨fst✝, (a * b) • snd✝⟩ = ⟨⟨fst✝, b • snd✝⟩.fst, a • ⟨fst✝, b • snd✝⟩.snd⟩

Tactic:
mul_smul

Goal state after:
case mk
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
a b : M
fst✝ : ι
snd✝ : α fst✝
⊢ ⟨fst✝, a • b • snd✝⟩ = ⟨⟨fst✝, b • snd✝⟩.fst, a • ⟨fst✝, b • snd✝⟩.snd⟩
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfmodP.e_a
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 : ℕ
⊢ f.coeff n - (C f.leadingCoeff * X ^ f.natDegree).coeff n ∈ P

Tactic:
simp only [coeff_C_mul, coeff_X_pow, mul_ite, mul_one, mul_zero, sub_ite, sub_zero]

Goal state after:
case hfmodP.e_a
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 : ℕ
⊢ (if n = f.natDegree then f.coeff n - f.leadingCoeff else f.coeff n) ∈ P
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:
induction n generalizing f with

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

Goal state before:
pp: case h.h_add
M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
v : ι →₀ ℕ
hx : (v.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hx' : ∃ a, (v.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
w : ι →₀ ℕ
hy : (w.prod fun x1 x2 ↦ f x1 ^ x2) ∈ closure (Set.range f)
hy' : ∃ a, (w.prod fun x1 x2 ↦ f x1 ^ x2) = a.prod fun x1 x2 ↦ f x1 ^ x2
⊢ ∀ a ∈ v.support ∪ w.support, ∀ (b₁ b₂ : ℕ), f a ^ (b₁ + b₂) = f a ^ b₁ * f a ^ b₂

Tactic:
· simp [pow_add]

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

Goal state before:
pp: G : Type u_5
H : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
a : G
f : G → H
x✝ : G
⊢ x✝ ∈ support (τ a f) ↔ x✝ ∈ a +ᵥ support f

Tactic:
simp [mem_vadd_set_iff_neg_vadd_mem, sub_eq_neg_add]

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

Goal state before:
pp: case refine_2
ι : 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
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
· let f' : G →* S := invMonoidHom.comp f
    have h₁ : (invMonoidHom ∘ v) '' IsMulIndecomposable.baseOf v f' =
        v '' IsMulIndecomposable.baseOf v f := by
      rw [image_comp, IsMulIndecomposable.image_baseOf_inv_comp_eq v hv_inv f, image_comp,
        ← image_comp]
      simp
    have h₂ : v '' {i | f (v i) < 1} = v '' {i | 1 < f' (v i)} := by simp [f']
    rw [h₂, ← h₁, image_comp, coe_invMonoidHom, image_inv_eq_inv, closure_inv]
    refine le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f'))
    simp [Submonoid.closure_image_isMulIndecomposable_baseOf]

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X : FintypeCat
f : X.obj → X.obj
⊢ f = id → homMk f = 𝟙 X

Tactic:
rintro rfl
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: case mpr
X Y Z : FintypeCat
f : X.obj → Y.obj
g : Y.obj → Z.obj
h : X.obj → Z.obj
⊢ h = g ∘ f → homMk h = homMk f ≫ homMk g

Tactic:
rintro rfl
    rfl

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

Goal state before:
pp: case pos
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))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

Tactic:
exfalso
          exact h₁ (lt_of_le_of_lt h h₂)

Goal state after:
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 : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0

Tactic:
rcases n with _ | n

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ objD X (0 + 1) ≫ objD X 0 = 0

case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1 + 1) ≫ objD X (n + 1) = 0
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
  constructor
  · intro h X p hp
    have : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
    rw [sub_sub_cancel]
  · intro h X p hp
    have : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    apply Preadditive.hasEqualizer_of_hasKernel

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ∀ (X : Karoubi C) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
intro P p hp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
⊢ IsIdempotentComplete Cᵒᵖ

Tactic:
by
  rwa [isIdempotentComplete_iff_opposite]

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
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((alternatingFaceMapComplex A).obj X).d (i + 1) i =
    ((normalizedMooreComplex A).obj X).d (i + 1) i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
by
  /- we have to show the compatibility of the differentials on the alternating
           face map complex with those defined on the normalized Moore complex:
           we first get rid of the terms of the alternating sum that are obviously
           zero on the normalized_Moore_complex -/
  simp only [normalizedMooreComplex, NormalizedMooreComplex.obj, alternatingFaceMapComplex,
    AlternatingFaceMapComplex.obj, ChainComplex.of_d, AlternatingFaceMapComplex.objD, comp_sum]
  rw [Fin.sum_univ_succ, Fintype.sum_eq_zero]
  swap
  · intro j
    rw [NormalizedMooreComplex.objX_add_one, comp_zsmul,
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ _ (Finset.mem_univ j)),
      Category.assoc, kernelSubobject_arrow_comp, comp_zero, smul_zero]
  -- finally, we study the remaining term which is induced by X.δ 0
  rw [add_zero, Fin.val_zero, pow_zero, one_zsmul]
  dsimp [NormalizedMooreComplex.objD, NormalizedMooreComplex.objX]
  cases i <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (f.right.app (unop x)).unop ≫ (X✝.hom.app (unop x)).unop = (Y✝.hom.app (unop x)).unop ≫ f.left.unop

Tactic:
← unop_comp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : CosimplicialObject.Augmented Cᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategoryᵒᵖ
⊢ (X✝.hom.app (unop x) ≫ f.right.app (unop x)).unop = (f.left ≫ Y✝.hom.app (unop x)).unop
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image.ι φ = i

Tactic:
have := strongEpi_of_epi e
  rw [← image.isoStrongEpiMono_hom_comp_ι e i fac,
    SimplexCategory.eq_id_of_isIso (image.isoStrongEpiMono e i fac).hom, Category.id_comp]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
G : Subfunctor F
hx : ofSection x ≤ G
⊢ x ∈ G.obj X

Tactic:
exact hx _ (mem_ofSection_obj x)

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
⊢ x ∈ (ofSimplex ((ConcreteCategory.hom (X.map f.op)) x)).obj (Opposite.op ⦋m⦌)

Tactic:
have := isSplitEpi_of_epi f

Goal state after:
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f
x : X _⦋m⦌
this : IsSplitEpi f
⊢ x ∈ (ofSimplex ((ConcreteCategory.hom (X.map f.op)) x)).obj (Opposite.op ⦋m⦌)
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:
by
    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.NonDegenerateSimplices

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ y.simplex ∈ x.subcomplex.obj (Opposite.op ⦋y.dim⦌)

Tactic:
have := isSplitEpi_of_epi f

Goal state after:
X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
this : IsSplitEpi f
⊢ y.simplex ∈ x.subcomplex.obj (Opposite.op ⦋y.dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
⊢ (N.mk ↑y ⋯).simplex ∈
    { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex.obj (Opposite.op ⦋(N.mk ↑y ⋯).dim⦌)

Tactic:
have := isSplitEpi_of_epi f

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ (N.mk ↑y ⋯).simplex ∈
    { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑y }.subcomplex.obj (Opposite.op ⦋(N.mk ↑y ⋯).dim⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case mpr
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
hx : (ConcreteCategory.hom (X.map f.op)) y ∈ A.obj (op ⦋n⦌)
⊢ y ∈ A.obj (op ⦋m⦌)

Tactic:
have := isSplitEpi_of_epi f

Goal state after:
case mpr
X : SSet
A : X.Subcomplex
n m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
hx : (ConcreteCategory.hom (X.map f.op)) y ∈ A.obj (op ⦋n⦌)
this : IsSplitEpi f
⊢ y ∈ A.obj (op ⦋m⦌)
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j : ℕ
s : ¬(ComplexShape.up ℕ).Rel i j
⊢ (match i, j with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

Tactic:
rcases j with (_ | _ | j) <;> cases i <;> simp_all

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

Goal state before:
pp: n d : ℕ
S : ↑{S | #S = d + 1}
A : Δ[n].Subcomplex
⊢ ↑(nonDegenerateEquiv'.symm S) ∈ A.obj (op ⦋d⦌) ↔ face ↑S ≤ A

Tactic:
obtain ⟨x, rfl⟩ := nonDegenerateEquiv'.{u}.surjective S
  rw [face_nonDegenerateEquiv' x, Equiv.symm_apply_apply, Subcomplex.ofSimplex_le_iff]

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

Goal state before:
pp: case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      c₁.ε₁ c₂ c₁₂ (c₁.next i₁, i₂) •
        (K.d i₁ (c₁.next i₁)).f i₂ ≫
          (K.d (c₁.next i₁) (c₁.next (c₁.next i₁))).f i₂ ≫
            K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next (c₁.next i₁), i₂) i₁₂'' ?pos✝ =
    0

pp: case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.π c₂ c₁₂ (c₁.next (c₁.next i₁), i₂) = i₁₂''

Tactic:
d_f_comp_d_f_assoc,

Goal state after:
case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      c₁.ε₁ c₂ c₁₂ (c₁.next i₁, i₂) •
        0 ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (c₁.next (c₁.next i₁), i₂) i₁₂'' ?pos✝ =
    0

case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.π c₂ c₁₂ (c₁.next (c₁.next i₁), i₂) = i₁₂''
Module: Mathlib.Algebra.Homology.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D
inst✝⁴ : HasZeroMorphisms C₁
inst✝³ : HasZeroMorphisms C₂
inst✝² : HasZeroMorphisms D
F : C₁ ⥤ C₂ ⥤ D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
K₁ K₁' : HomologicalComplex C₁ c₁
f : K₁ ⟶ K₁'
K₂ : HomologicalComplex C₂ c₂
⊢ ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁, i₂) ≫
          (((F.mapBifunctorHomologicalComplexObj c₂ K₁').obj K₂).d i₁ i₁').f i₂ =
        (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).d i₁ i₁').f i₂ ≫
          ((GradedObject.mapBifunctor F I₁ I₂).map f.f).app K₂.X (i₁', i₂)

Tactic:
intros
          dsimp
          simp only [← NatTrans.comp_app, ← F.map_comp, f.comm]

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

Goal state before:
pp: case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.d₁ c₁₂ (c₁.next i₁) i₂ i₁₂'' = 0

Tactic:
rw [totalAux.d₁_eq K c₁₂ h₄ i₂ i₁₂'', Linear.comp_units_smul,
            d_f_comp_d_f_assoc, zero_comp, smul_zero, smul_zero]

Goal state after:
case pos
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₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁.π c₂ c₁₂ (c₁.next (c₁.next i₁), i₂) = i₁₂''