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
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this✝ : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
not_terminatedAt_pred_n : ¬g.TerminatedAt (n - 1)
not_terminatedAt_ppred_n : ¬g.TerminatedAt (n - 2)
ppred_nth_fib_le_ppconts_B : ↑(fib n) ≤ ppconts.b
this : ↑(fib (n + 1)) ≤ gp.b * pconts.b
⊢ ↑(fib n) + ↑(fib (n + 1)) ≤ ppconts.b + gp.b * pconts.b

Tactic:
by gcongr

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
⊢ P.toPoly.natDegree = 0

Tactic:
rw [of_c_eq_zero ha hb hc, natDegree_C]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z

Tactic:
← map_ne_zero φ,

Goal state after:
F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ φ P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inl
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 : (of v).dens n = 0
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

pp: case inr
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
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
· simp only [hB, mul_zero, zero_mul, div_zero, le_refl]

Goal state after:
case inr
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
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
le : matrix n I ≤ matrix n J
⊢ I ≤ J

Tactic:
x

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
le : matrix n I ≤ matrix n J
x : R
⊢ x ∈ I → x ∈ J
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ ∃ e', (CompleteOrthogonalIdempotents fun t ↦ Option.rec e₀ e' t) ∧ e = ⇑f ∘ e'

Tactic:
refine ⟨(1 - e₀) • e', ⟨⟨Option.rec he₀ fun i ↦ ?_, ?_⟩, ?_⟩, ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ Pairwise fun x1 x2 ↦ Option.rec e₀ ((1 - e₀) • e') x1 * Option.rec e₀ ((1 - e₀) • e') x2 = 0

case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ ∑ i, Option.rec e₀ ((1 - e₀) • e') i = 1

case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
⊢ e = ⇑f ∘ ((1 - e₀) • e')

case refine_4
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i : I
⊢ IsIdempotentElem (Option.rec e₀ ((1 - e₀) • e') (some i))
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)
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
κ : ι → Type u_3 := fun i ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := fun i ↦ Free.chooseBasis R ↥(N ↑i)
h : IsInternal fun i ↦ N ↑i
⊢ ∀ i ∉ s, N i = ⊥

Tactic:
by simp [s]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
⊢ (fun r ↦ ∑ i, ↑(r i)) ((fun r i ↦ ⟨(fun x ↦ e i * x * e i) r, ⋯⟩) r) = r

Tactic:
simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]

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

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
geom_sum_eq h₁,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x : K
hx1 : x ≠ 1
hx0 : x ≠ 0
n : ℕ
h₁ : x⁻¹ ≠ 1
h₂ : x⁻¹ - 1 ≠ 0
h₃ : x - 1 ≠ 0
h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x
⊢ (x⁻¹ ^ n - 1) / (x⁻¹ - 1) = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)
Module: Mathlib.Algebra.Ring.MinimalAxioms

Goal state before:
pp: R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
⊢ a + b = b + a

Tactic:
have h₂ : (1 + 1 : R) * (a + b) = a + (b + a) + b := by
      rw [right_distrib]
      simp only [left_distrib, one_mul, add_assoc]

Goal state after:
R : Type u
inst✝⁴ : Add R
inst✝³ : Mul R
inst✝² : Neg R
inst✝¹ : Zero R
inst✝ : One R
add_assoc : ∀ (a b c : R), a + b + c = a + (b + c)
zero_add : ∀ (a : R), 0 + a = a
neg_add_cancel : ∀ (a : R), -a + a = 0
mul_assoc : ∀ (a b c : R), a * b * c = a * (b * c)
one_mul : ∀ (a : R), 1 * a = a
mul_one : ∀ (a : R), a * 1 = a
left_distrib : ∀ (a b c : R), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : R), (a + b) * c = a * c + b * c
this : AddGroup R := AddGroup.ofLeftAxioms add_assoc zero_add neg_add_cancel
a b : R
h₁ : (1 + 1) * (a + b) = a + (a + b) + b
h₂ : (1 + 1) * (a + b) = a + (b + a) + b
⊢ a + b = b + a
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α * 2 = #α

Tactic:
Cardinal.mul_eq_left hα _ (by simp)

Goal state after:
case a.inr
α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ #α = #α

α : Type u
inst✝ : Nonempty α
hα : ℵ₀ ≤ #α
⊢ 2 ≤ #α
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ (if y = x then 1 else 0) = Pi.single x 1 y

Tactic:
simp [Pi.single, Function.update]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
A : Type v
inst✝ : CommSemiring A
φ : R →+* A
⊢ (Polynomial.map φ f).IsWeaklyEisensteinAt (Ideal.map φ 𝓟)

Tactic:
by
  refine (isWeaklyEisensteinAt_iff _ _).2 fun hn => ?_
  rw [coeff_map]
  exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn natDegree_map_le))

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
⊢ integralClosure R A ≤ ⊥

Tactic:
x

Goal state after:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
⊢ x ∈ integralClosure R A → x ∈ ⊥
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_4
K : Type u_5
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : FaithfulSMul R K
inst✝ : IsIntegrallyClosedIn R K
⊢ IsIntegrallyClosed R

Tactic:
have : IsDomain R := (FaithfulSMul.algebraMap_injective R K).isDomain _
  let f : FractionRing R →ₐ[R] K := IsFractionRing.liftAlgHom (g := Algebra.ofId _ _)
    (FaithfulSMul.algebraMap_injective R K)
  rw [isIntegrallyClosed_iff (K := FractionRing R)]
  intro x hx
  convert! (IsIntegralClosure.isIntegral_iff (A := R)).mp (hx.map f)
  simp [← f.toRingHom.injective.eq_iff]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
inst✝¹ : CommRing R
inst✝ : StrongRankCondition R
⊢ Module.rank R ℍ[R,c₁,c₂,c₃] = 4

Tactic:
by
  rw [rank_eq_card_basis (basisOneIJK c₁ c₂ c₃), Fintype.card_fin]
  norm_num

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
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x✝ : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
x : α ⊕ β
⊢ (a • b) • x = a • b • x

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

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
a✝ b✝ : Bˣ
hb : a✝ ∈ Units.val ⁻¹' range ⇑f
hb' : b✝ ∈ Units.val ⁻¹' range ⇑f
⊢ a✝ * b✝ ∈ Units.val ⁻¹' range ⇑f

Tactic:
by
    obtain ⟨y, hy⟩ := hb
    obtain ⟨y', hy'⟩ := hb'
    use y * y'
    rw [map_mul, hy, hy', Units.val_mul]

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

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
a₁

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ : ↑A.toLinOrd
⊢ ∀ ⦃a₂ : (fun X ↦ ↑X.toLinOrd) A⦄, (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂ → a₁ = a₂
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) (𝟙 X - p)
⊢ p = 𝟙 X - (𝟙 X - p)

Tactic:
rw [sub_sub_cancel]

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

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ k.castSucc.pred ⋯

Tactic:
Fin.le_pred_iff,

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i.succ ≤ k.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
⊢ δ₀Iter i hi ≫ δ j = δ₀Iter (i + 1) ⋯

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter i hi) (δ j), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..,
    Fin.succAbove_of_le_castSucc _ _ (by grind)]
  simp [add_assoc]

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

Goal state before:
pp: X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ opObjEquiv x ∈ X.degenerate n ↔ x ∈ X.op.degenerate n

Tactic:
simp only [mem_degenerate_iff]

Goal state after:
X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), opObjEquiv x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) ↔
    ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.op.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁✝ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁✝
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂✝ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂✝
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
this : y₂ ≤ y₁
⊢ False

Tactic:
by simp [show y₁ = y₂ by lia] at h'

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.nonDegenerate n ⊆ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)

Tactic:
x

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.nonDegenerate n → x ∈ (⨆ x, ofSimplex ↑x.snd).obj (op ⦋n⦌)
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).map f ≫
        (HomologicalComplex.Hom.isoOfComponents
            (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj Y).X x)) ⋯).hom =
      (HomologicalComplex.Hom.isoOfComponents
            (fun x ↦ Iso.refl (((Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C).obj X).X x)) ⋯).hom ≫
        ChainComplex.alternatingConst.map f

Tactic:
by intros; ext; simp

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

Goal state after:
case zero
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 : ℕ
s : ¬(ComplexShape.up ℕ).Rel i 0
⊢ (match i, 0 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.zero
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 : ℕ
s : ¬(ComplexShape.up ℕ).Rel i (0 + 1)
⊢ (match i, 0 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0

case succ.succ
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 + 1 + 1)
⊢ (match i, j + 1 + 1 with
    | 0, 1 => f
    | i.succ, j.succ => C.d i j
    | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
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 : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j 0
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
rcases j with (_ | _ | j)

Goal state after:
case zero.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 0
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case zero.succ.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) 0
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case zero.succ.succ
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) 0
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero
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 : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hjk : (ComplexShape.up ℕ).Rel j (0 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
rcases j with (_ | _ | j)

Goal state after:
case succ.zero.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 (0 + 1)
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero.succ.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (0 + 1)
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.zero.succ.succ
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (0 + 1)
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ
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 : ℕ
hij : (ComplexShape.up ℕ).Rel i j
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel j (k + 1 + 1)
⊢ ((match i, j with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
rcases j with (_ | _ | j)

Goal state after:
case succ.succ.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hij : (ComplexShape.up ℕ).Rel i 0
hjk : (ComplexShape.up ℕ).Rel 0 (k + 1 + 1)
⊢ ((match i, 0 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ.succ.zero
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hij : (ComplexShape.up ℕ).Rel i (0 + 1)
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
⊢ ((match i, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

case succ.succ.succ.succ
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 : ℕ
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k j : ℕ
hij : (ComplexShape.up ℕ).Rel i (j + 1 + 1)
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
⊢ ((match i, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ (Subcomplex.ofSimplex (yonedaEquiv f)).toSSet.Finite

Tactic:
← Subcomplex.range_eq_ofSimplex

Goal state after:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ (Subcomplex.range f).toSSet.Finite