mathlib-initiative/mathlib-tactics huggingface dataset:
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
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - (b⁻¹ * a) • 1).ker = (f - b⁻¹ • a • 1).ker

Tactic:
rw [smul_smul]

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

Goal state before:
pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
rintro ⟨x, rfl⟩ i hi

Goal state after:
case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ ∃ y, ((f - μ • 1) ^ i) y = ((f - μ • 1) ^ k) x
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ↑((LinearMap.restrict (f - μ • 1) h ^ k) ⟨x, hx✝⟩) = ↑(0 ⟨x, hx✝⟩)

Tactic:
rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
    Module.End.pow_restrict, LinearMap.restrict_apply]

Goal state after:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
x : M
hx✝ : x ∈ (f.genEigenspace μ) ↑k
hx : x ∈ ((f - μ • 1) ^ k).ker
⊢ ⟨((f - μ • 1) ^ k) ↑⟨x, hx✝⟩, ⋯⟩ = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ ((toMatrix b b) 1).trace = ↑(finrank R M)

Tactic:
toMatrix_one,

Goal state after:
case inr
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Matrix.trace 1 = ↑(finrank R M)
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
l : ℕ
⊢ (((f - μ • 1) ^ l).domRestrict p).ker = Submodule.comap p.subtype ((f - μ • 1) ^ l).ker

Tactic:
LinearMap.domRestrict,

Goal state after:
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
l : ℕ
⊢ (((f - μ • 1) ^ l) ∘ₗ p.subtype).ker = Submodule.comap p.subtype ((f - μ • 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✝³ : Free R M
inst✝² : Module.Finite R M
f : M →ₗ[R] M
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
b' : Basis (Free.ChooseBasisIndex R M) A (A ⊗[R] M) := Algebra.TensorProduct.basis A b
⊢ (trace A (A ⊗[R] M)) (baseChange A f) = ↑(algebraMap R A) ((trace R M) f)

Tactic:
simp [b', trace_eq_matrix_trace R b, trace_eq_matrix_trace A b', AddMonoidHom.map_trace]

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 + -(ρ • LinearMap.id)).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)

Tactic:
← neg_smul,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ ρ : R
⊢ (f + -ρ • LinearMap.id).HasEigenvalue μ ↔ f.HasEigenvalue (μ + ρ)
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝⁴ : Applicative m
F : α → m β
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ β✝ γ✝ : Type u
f : β✝ → F✝ γ✝
g : α✝ → G✝ β✝
x✝ : FreeMagma α✝
x : α✝
⊢ traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))

Tactic:
by simp only [Function.comp_def, traverse_pure, functor_norm]

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

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

Tactic:
FreeGroup.mk_toWord,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ x * y = x * mk y.toWord
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a
α : Type u
inst✝ : Nonempty α
⊢ #(List (α × Bool)) = max #α ℵ₀

Tactic:
simp only [mk_list_eq_max_mk_aleph0, mk_prod, lift_uzero, mk_fintype, Fintype.card_bool,
      Nat.cast_ofNat, lift_ofNat]

Goal state after:
case a
α : Type u
inst✝ : Nonempty α
⊢ max (#α * 2) ℵ₀ = max #α ℵ₀
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: case hfP
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
⊢ (algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff ≠ 0

Tactic:
simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, coe_comp, Function.comp_apply, ne_eq,
      FaithfulSMul.algebraMap_eq_zero_iff]

Goal state after:
case hfP
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
⊢ ¬(Ideal.Quotient.mk P) f.leadingCoeff = 0
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x : M
⊢ x ∈ closure s ↔ x ∈ s ∨ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
by
  rw [← SetLike.mem_coe, coe_closure]
  simp [mem_mul]

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

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
⊢ (-1) ^ k * a * b = (-1) ^ k * (a * b)

Tactic:
induction k with

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ IsConj a b ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
rw [IsConj, Units.exists_iff_ne_zero (p := (SemiconjBy · a b))]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a b : α
⊢ (∃ x, x ≠ 0 ∧ SemiconjBy x a b) ↔ ∃ c, c ≠ 0 ∧ c * a * c⁻¹ = b
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : 1 < f (v i)
hi' : v i ∉ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
⊢ False

Tactic:
let s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
i : ι
hi : 1 < f (v i)
hi' : v i ∉ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
⊢ False
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
⊢ v '' univ ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
have : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1} := by ext i; simp [(hf i).symm]

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
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' univ ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ (∃ Y' i' e', i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p') → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
apply split_imp_of_iso φ.symm p' p

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X X' : C
φ : X ≅ X'
p : X ⟶ X
p' : X' ⟶ X'
hpp' : p ≫ φ.hom = φ.hom ≫ p'
⊢ p' ≫ φ.symm.hom = φ.symm.hom ≫ p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
Fin.le_castSucc_iff,

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

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

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]
    rcases le_or_gt k (j.castSucc) with (hjk | hjk)
    · rw [Fin.predAbove_of_le_castSucc _ _
      (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
      Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]
      rw [Fin.castSucc_castPred]
      exact hjk.trans_lt H
    · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]
      rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]

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

Goal state before:
pp: case cast.succ.inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj

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

Goal state before:
pp: x y : SimplexCategory
e : x ≅ y
i : Fin (y.len + 1)
⊢ (Hom.toOrderHom e.hom) ((Hom.toOrderHom e.inv) i) = i

Tactic:
simpa only using! congr_arg (fun φ => (Hom.toOrderHom φ) i) e.inv_hom_id

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 : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.map (SimplexCategory.σ₀Iter i hi).op ≫ X.map (SimplexCategory.σ j).op = X.map (SimplexCategory.σ₀Iter (i + 1) ⋯).op

Tactic:
rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]

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

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
i : Fin (n + 2)
hi : ∀ (x : Fin (Δ.len + 1)), (Hom.toOrderHom θ) x ≠ i
x : Fin (Δ.len + 1)
this : ∀ (j : Fin (n + 2)), j ≠ i → i.succAbove (((Fin.last n).predAbove i).predAbove j) = j
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom ((θ ≫ σ ((Fin.last n).predAbove i)) ≫ δ i)) x

Tactic:
by
    dsimp [δ, σ]
    exact .symm <| this _ (hi _)

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

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j

Tactic:
by_cases! hk' : i ≤ k.castSucc

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j

case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : j ≤ ↑k
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = ↑k - j
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

Tactic:
by_cases! hk' : i ≤ k.castSucc

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0
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'
⊢ ofSection x ≤ (ofSection ((ConcreteCategory.hom (f.app X)) x)).preimage f

Tactic:
ofSection_le_iff,

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 ∈ ((ofSection ((ConcreteCategory.hom (f.app X)) x)).preimage f).obj X
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStruct

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ x₁ = y₁

Tactic:
by rw [← hom.tgt_eq, hhom, hom'.tgt_eq]

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id x₁).edge = (id y₁).edge

Tactic:
by rw [← hom.tgt_eq, hhom, hom'.tgt_eq]

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

Goal state before:
pp: case right
n m : ℕ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

Tactic:
intro ⟨S, hS⟩

Goal state after:
case right
n m : ℕ
S : Finset (Fin (n + 1))
hS : S ∈ {S | #S = m + 1}
⊢ ∃ a,
    (fun x ↦
          match x with
          | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
        a =
      ⟨S, hS⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj : j ∈ ↑(nonDegenerateEquiv' x)
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj⟩

Tactic:
rw [nonDegenerateEquiv'_iff] at hj

Goal state after:
case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj✝ : j ∈ ↑(nonDegenerateEquiv' x)
hj : ∃ i, ↑x i = j
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
generalize hm : S.card = m
  obtain _ | m := m
  · obtain rfl : S = ∅ := by rwa [← Finset.card_eq_zero]
    rw [face_empty]
    infer_instance
  · rw [← hasDimensionLT_iff_of_iso
      (isoOfRepresentableBy (faceRepresentableBy S m (monoEquivOfFin S (by simpa))))]
    exact hasDimensionLT_of_le _ (m + 1) _

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₁ : I₁
i₂ : I₂
⊢ c₂.π c₁ c₁₂ (i₂, i₁) = c₁.π c₂ c₁₂ (i₁, i₂)

Tactic:
by
  apply TotalComplexShapeSymmetry.symm

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
α : F ⟶ F'
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ : GradedObject I₁ C₁
X₂ Y₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
⊢ ((mapTrifunctor F I₁ I₂ I₃).obj X₁).map φ ≫
      { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (Y₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } =
    { app := fun x x_1 ↦ ((α.app (X₁ x_1.1)).app (X₂ x_1.2.1)).app (x x_1.2.2), naturality := ⋯ } ≫
      ((mapTrifunctor F' I₁ I₂ I₃).obj X₁).map φ

Tactic:
by
        ext X₃ ⟨i₁, i₂, i₃⟩
        dsimp
        simp only [← NatTrans.comp_app, NatTrans.naturality]

Goal state after:
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₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
i₁ i₁' : I₁
i₂ i₂' : I₂
⊢ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂) ≫ (F.obj (K₁.X i₁')).map (K₂.d i₂ i₂') =
    (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.map (K₁.d i₁ i₁')).app (K₂.X i₂')

Tactic:
by
        dsimp
        rw [NatTrans.naturality]

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

Goal state before:
pp: case pos
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
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) •
      (K.flip.X i₂).d i₁ (c₁.next i₁) ≫
        K.flip.ιTotal c i₂ (c₁.next i₁) j' h₃ ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
ι_totalDesc,

Goal state after:
case pos
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
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₁.Rel i₁ (c₁.next i₁)
h₃ : c₂.π c₁ c (i₂, c₁.next i₁) = j'
h₄ : c₁.π c₂ c (c₁.next i₁, i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₁ c₂ c (i₁, i₂) • (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.ιTotal c (c₁.next i₁) i₂ j' h₄ =
    c₂.ε₂ c₁ c (i₂, i₁) •
      (K.flip.X i₂).d i₁ (c₁.next i₁) ≫ (c₁.σ c₂ c (c₁.next i₁) i₂ • K.ιTotal c (c₁.next i₁) i₂ j' ⋯)
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
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
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) •
      (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫
        K.flip.ιTotal c (c₂.next i₂) i₁ j' h₃ ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
ι_totalDesc,

Goal state after:
case pos
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
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    c₂.ε₁ c₁ c (i₂, i₁) •
      (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ (c₁.σ c₂ c i₁ (c₂.next i₂) • K.ιTotal c i₁ (c₂.next i₂) j' ⋯)
Module: Mathlib.Algebra.Homology.BifunctorFlip

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
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
⊢ K₂.HasMapBifunctor K₁ F.flip c

Tactic:
rw [hasMapBifunctor_flip_iff]
  infer_instance

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

Goal state before:
pp: case pos
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₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ ((x.negOnePow • (K.d (p + x) (p + 1 + x)).f q) ≫
      ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p + 1) q n₁ ⋯ ≫
        ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n₁' ⋯) =
    x.negOnePow • 1 • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯

Tactic:
ι_totalDesc,

Goal state after:
case pos
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₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (x.negOnePow • (K.d (p + x) (p + 1 + x)).f q) ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯ =
    x.negOnePow • 1 • (K.d (p + x) (p + 1 + x)).f q ≫ K.ιTotal (up ℤ) (p + 1 + x) q n₁' ⋯