mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ 1 ≤ ifp_succ_n.b

Tactic:
by
  obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
        ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
  rw [IntFractPair.of, le_floor, cast_one, one_le_inv₀
    ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)]
  exact (nth_stream_fr_lt_one nth_stream_eq).le

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
| (of v).dens n * (of v).dens (n + 1)

Tactic:
mul_comm

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
| (of v).dens (n + 1) * (of v).dens n
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
v : M
hv : f.HasUnifEigenvector μ 1 v
n : ℕ
⊢ (f ^ n) v = μ ^ n • v

Tactic:
induction n <;> simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

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
f : End K V
a b : K
hb : b ≠ 0
⊢ (f.genEigenspace (a * b⁻¹)) 1 = (f.genEigenspace (b⁻¹ * a)) 1

Tactic:
mul_comm

Goal state after:
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.genEigenspace (b⁻¹ * a)) 1 = (f.genEigenspace (b⁻¹ * a)) 1
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i ↦ Free.chooseBasis R ↥(N i)
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).trace = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i ↦ Free.chooseBasis R ↥(N i)
⊢ (Matrix.blockDiagonal' fun i ↦ (toMatrix (b i) (b i)) (f.restrict ⋯)).trace = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ e * r = r → r * e = r

Tactic:
intro

Goal state after:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
a✝ : e * r = r
⊢ r * e = r
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' uIcc a (a + c) = range f

Tactic:
uIcc_of_ge (add_le_of_nonpos_right hc.le),

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
h : Periodic f c
hc✝ : c ≠ 0
a : α
hc : c < 0
⊢ f '' Icc (a + c) a = range f
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case refine_2.refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : T
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) x

Tactic:
obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h

Goal state after:
case refine_2.refine_1
R : Type u_4
S : Type u_5
T : Type u_6
U : Type u_7
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : CommRing T
inst✝⁹ : CommRing U
inst✝⁸ : Algebra R T
inst✝⁷ : Algebra S T
inst✝⁶ : Algebra R U
inst✝⁵ : Algebra S U
inst✝⁴ : Algebra T U
inst✝³ : IsScalarTower S T U
inst✝² : IsScalarTower R T U
inst✝¹ : IsIntegralClosure S R T
inst✝ : IsIntegrallyClosedIn T U
x : S
h : IsIntegral R ((algebraMap S T) x)
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) ((algebraMap S T) x)
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f

Tactic:
apply toPartialEquiv_injective
  rw [toPartialEquiv_restr, PartialEquiv.restr_eq_of_source_subset hA]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
by rw [add_comm, self_add_star]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
inst✝³ : SMul M α
inst✝² : SMul N α
a✝ : M
b : α
x✝ : Option α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
a : M
x : Option α
⊢ MulOpposite.op a • x = a • x

Tactic:
cases x
    exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]

Goal state after:
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
inst✝³ : (i : ι) → SMul M (α i)
inst✝² : (i : ι) → SMul N (α i)
a✝ : M
i : ι
b✝ : α i
x : (i : ι) × α i
inst✝¹ : SMul M N
inst✝ : ∀ (i : ι), IsScalarTower M N (α i)
a : M
b : N
fst✝ : ι
snd✝ : α fst✝
⊢ (a • b) • ⟨fst✝, snd✝⟩ = a • b • ⟨fst✝, snd✝⟩

Tactic:
rw [smul_mk, smul_mk, smul_mk, smul_assoc]

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

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

Tactic:
mul_comm

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

Goal state after:
M : Type u_1
inst✝² : MulOneClass M
inst✝¹ : Pow M ℕ
inst✝ : NatPowAssoc M
x : M
m n : ℕ
⊢ x ^ (n * m) = (x ^ n) ^ m
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_2
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ f (y + n • h) = ((fwdDiffₗ M G h + 1) ^ n) f y

pp: case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y =
    (∑ m ∈ range (n + 1), fwdDiffₗ M G h ^ m * 1 ^ (n - m) * ↑(n.choose m)) f y

Tactic:
· rw [← shiftₗ_pow_apply h f, shiftₗ]

Goal state after:
case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y =
    (∑ m ∈ range (n + 1), fwdDiffₗ M G h ^ m * 1 ^ (n - m) * ↑(n.choose m)) f y
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ ∑ x_1 ∈ range P.natDegree, (P.coeff x_1 • Δ_[1]^[P.natDegree] fun i ↦ i ^ x_1) x +
      (P.coeff P.natDegree • Δ_[1]^[P.natDegree] fun i ↦ i ^ P.natDegree) x =
    P.leadingCoeff • ↑P.natDegree ! x

Tactic:
sum_eq_zero (fun i hi ↦ ?_),

Goal state after:
R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ 0 + (P.coeff P.natDegree • Δ_[1]^[P.natDegree] fun i ↦ i ^ P.natDegree) x = P.leadingCoeff • ↑P.natDegree ! x

R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
i : ℕ
hi : i ∈ range P.natDegree
⊢ (P.coeff i • Δ_[1]^[P.natDegree] fun i_1 ↦ i_1 ^ i) x = 0
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s t : Set M
⊢ #↑(s * t) ≤ #↑s * #↑t

Tactic:
rw [← image2_mul]; exact Cardinal.mk_image2_le

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
simp only [Nat.card, ← Cardinal.toNat_mul]

Goal state after:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Cardinal.toNat #↑(s * t) ≤ Cardinal.toNat (#↑s * #↑t)
Module: Mathlib.Algebra.Group.Pointwise.Set.Small

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : InvolutiveNeg α
inst✝ : Small.{u, u_1} ↑s
⊢ Small.{u, u_1} ↑((fun x ↦ -x) '' s)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝³ : CommMonoid G
inst✝² : LinearOrder G
inst✝¹ : CommMonoid G'
inst✝ : Preorder G'
e : G ≃* G'
he : StrictMono ⇑e
⊢ StrictMono ⇑e.symm

Tactic:
intro

Goal state after:
G : Type u_1
G' : Type u_2
inst✝³ : CommMonoid G
inst✝² : LinearOrder G
inst✝¹ : CommMonoid G'
inst✝ : Preorder G'
e : G ≃* G'
he : StrictMono ⇑e
a✝ : G'
⊢ ∀ ⦃b : G'⦄, a✝ < b → e.symm a✝ < e.symm b
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₂ * (x₁ * y) ∈ s

Tactic:
rwa [mul_left_comm, ← mul_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: ⊢ Skeleton.incl.IsEquivalence

Tactic:
infer_instance

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

Goal state before:
pp: case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f → Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
intro

Goal state after:
case mp
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))

Tactic:
by
      cases n <;> dsimp
      · apply top_factors
      · refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_
        rw [Category.assoc, SimplicialObject.δ, ← f.naturality,
          ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
          Category.assoc]
        rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Goal state after:
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
inst✝ : Abelian D
X✝ : D
p✝ : X✝ ⟶ X✝
a✝ : p✝ ≫ p✝ = p✝
⊢ HasKernel p✝

Tactic:
infer_instance

Goal state after:
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
⊢ AddCommGroup (P ⟶ Q)

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯

Tactic:
· simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ,
      j.succ_pred, Fin.lt_def] using! H

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 Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ f.app (op ⦋n + 1⦌) ≫ ((-1) ^ ↑x✝¹ • Y.δ x✝¹) = ((-1) ^ ↑x✝¹ • X.δ x✝¹) ≫ f.app (op ⦋n⦌)

Tactic:
comp_zsmul,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • f.app (op ⦋n + 1⦌) ≫ Y.δ x✝¹ = ((-1) ^ ↑x✝¹ • X.δ x✝¹) ≫ f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategoryᵒᵖ ⥤ C)

Tactic:
infer_instance

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
inst✝ : HasPullbacks C
X✝ Y✝ : SimplicialObject C
x✝² : X✝ ⟶ Y✝
x✝¹ : Mono x✝²
x✝ : ℕ
⊢ Mono (x✝².app (op ⦋x✝⦌))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((Truncated.sk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.lanUnit.app ((truncation n).obj X))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsRightKanExtension ((Truncated.cosk n).obj ((truncation n).obj X))
    ((SimplexCategory.Truncated.inclusion n).op.ranCounit.app ((truncation n).obj X))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ Category.{?u.6, max u v} (SimplexCategory ⥤ C)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory ⥤ C)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory ⥤ C)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h
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 : ℕ
j : Fin (i + 1)
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ ((-1) ^ ↑j.succ • X.δ j.succ) = 0

Tactic:
comp_zsmul,

Goal state after:
case h
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 : ℕ
j : Fin (i + 1)
⊢ (-1) ^ ↑j.succ • (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ X.δ j.succ = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasLimitsOfShape J C
⊢ HasLimitsOfShape J (SimplexCategory.Truncated n ⥤ C)

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
J : Type v
inst✝¹ : SmallCategory J
inst✝ : HasColimitsOfShape J C
⊢ HasColimitsOfShape J (SimplexCategory.Truncated n ⥤ C)

Tactic:
infer_instance

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 Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ f.app ⦋n⦌ ≫ ((-1) ^ ↑x • Y.δ x) = ((-1) ^ ↑x • X.δ x) ≫ f.app ⦋n + 1⦌

Tactic:
comp_zsmul,

Goal state after:
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 Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
x : Fin (n + 2)
x✝ : x ∈ Finset.univ
⊢ (-1) ^ ↑x • f.app ⦋n⦌ ≫ Y.δ x = ((-1) ^ ↑x • X.δ x) ≫ f.app ⦋n + 1⦌
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
θ : ⦋n + 1⦌ ⟶ ⦋n⦌
inst✝ : Epi θ
i : Fin (n + 1)
θ' : ⦋n⦌ ⟶ ⦋n⦌
h : θ = σ i ≫ θ'
⊢ Epi θ

Tactic:
infer_instance

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

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

Tactic:
infer_instance

Goal state after:
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 ((ConcreteCategory.hom (f.app X)) x) ≤ (ofSection x).image f

Tactic:
· simp only [ofSection_le_iff, image_obj, Set.mem_image]
    exact ⟨x, mem_ofSection_obj x, rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
Y Y' : Arrow C
f : Augmented.toArrow.obj X ⟶ Y
g : Y ⟶ Y'
⊢ { toFun := equivalenceLeftToRight X Y', invFun := equivalenceRightToLeft X Y', left_inv := ⋯, right_inv := ⋯ }
      (f ≫ g) =
    { toFun := equivalenceLeftToRight X Y, invFun := equivalenceRightToLeft X Y, left_inv := ⋯, right_inv := ⋯ } f ≫
      augmentedCechNerve.map g

Tactic:
change equivalenceLeftToRight X Y' (f ≫ g) =
          equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
Y Y' : Arrow C
f : Augmented.toArrow.obj X ⟶ Y
g : Y ⟶ Y'
⊢ equivalenceLeftToRight X Y' (f ≫ g) = equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: case mp
X : SSet
m : ℕ
x : X _⦋m⦌
inst✝ : Mono (𝟙 ⦋m⦌)
h : { dim := m, simplex := (ConcreteCategory.hom (X.map (𝟙 ⦋m⦌).op)) x } = { dim := m, simplex := x }
⊢ IsIso (𝟙 ⦋m⦌)

Tactic:
infer_instance

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

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ ∀ (X : SimplexCategoryᵒᵖ), IsIso (f.app X)

Tactic:
intro

Goal state after:
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ IsIso (f.app X✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: case left
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Mono (f.app X✝)

Tactic:
infer_instance

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

Goal state before:
pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Epi (f.app X✝)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
this : IsIso (factorThruImage f)
⊢ Mono (factorThruImage f ≫ image.ι f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ ⊤_ C)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map (hf₁.section_ ≫ f₁).op)) ↑y₁ = ↑y₁

Tactic:
SplitEpi.id,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map (𝟙 ⦋m₁⦌).op)) ↑y₁ = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
this : IsIso (factorThruImage (g hf₁ f₂))
⊢ Mono (factorThruImage (g hf₁ f₂) ≫ image.ι (g hf₁ f₂))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this✝ : Y.HasDimensionLT d
i : ℕ
hi : i < d
this : Finite (Y _⦋i⦌)
⊢ Finite ↑(Y.nonDegenerate i)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ Mono (X.map f.op)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
⊢ ⨆ x, ofSimplex ↑x.snd = ⊤

Tactic:
by
  rw [eq_top_iff_contains_nonDegenerate]
  intro n x hx
  simp only [Subfunctor.iSup_obj, Set.mem_iUnion, Sigma.exists,
    Subtype.exists, exists_prop]
  exact ⟨n, x, hx, mem_ofSimplex_obj x⟩

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

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi : i ∈ S₁
⊢ i ∈ S₂

Tactic:
simp only [← obj₀Equiv_symm_mem_face_iff.{u}] at hi ⊢

Goal state after:
n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
h : face S₁ ≤ face S₂
i : Fin (n + 1)
hi : obj₀Equiv.symm i ∈ (face S₁).obj (op ⦋0⦌)
⊢ obj₀Equiv.symm i ∈ (face S₂).obj (op ⦋0⦌)
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:
by
    rcases j with (_ | _ | j) <;> cases i <;> simp_all

Goal state after: