mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case a
α : Type u
inst✝ : Nonempty α
⊢ max #α ℵ₀ ≤ #(FreeGroup α)

Tactic:
apply max_le
    · exact mk_le_of_injective FreeGroup.of_injective
    · simp

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
⊢ Associated (a ^ n) (b ^ n) ↔ Associated a b

Tactic:
simp_rw [← dvd_dvd_iff_associated, pow_dvd_pow_iff hn]

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

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
⊢ ∀ ⦃a₂ : Equidecomp X G⦄,
    { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂.toPartialEquiv →
      { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂

Tactic:
_

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
a₂✝ : Equidecomp X G
⊢ { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂✝.toPartialEquiv →
    { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂✝
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
a₂✝ : Equidecomp X G
⊢ { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂✝.toPartialEquiv →
    { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂✝

Tactic:
_

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
toPartialEquiv✝ : PartialEquiv X X
w✝ : Finset G
h✝ : IsDecompOn (↑toPartialEquiv✝) toPartialEquiv✝.source w✝
a₂✝ : Equidecomp X G
a✝ : { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ }.toPartialEquiv = a₂✝.toPartialEquiv
⊢ { toPartialEquiv := toPartialEquiv✝, isDecompOn' := ⋯ } = a₂✝
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

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

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

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
⊢ #↑Set.univ = #R ^ 4

Tactic:
by
  rw [mk_univ, mk_quaternionAlgebra]

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 ^ m) ^ n

Tactic:
induction n with
  | one => rw [ppow_one, mul_one]
  | succ k hk => rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ s ∈ f, ↑s
hy : b✝ ∈ ⋂ s ∈ f, ↑s
⊢ a✝ * b✝ ∈ ⋂ s ∈ f, ↑s

Tactic:
by rw [Set.mem_iInter₂] at *; exact fun s hs ↦ mul_mem (hx s hs) (hy s hs)

Goal state after:
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✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
⊢ v i ∈ ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
refine ⟨i⁻¹, ⟨by simpa [hv_inv] using hi, fun j hj k hk hi ↦ ?_⟩, by simp [hv_inv]⟩

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
i : ι
hi✝ : i ∈ {i | 1 < (invMonoidHom.comp f) (v i)}
hi' :
  ∀ j ∈ {i | 1 < (invMonoidHom.comp f) (v i)},
    ∀ k ∈ {i | 1 < (invMonoidHom.comp f) (v i)}, v i = v j * v k → v j = 1 ∨ v k = 1
j : ι
hj : j ∈ {i | 1 < f (v i)}
k : ι
hk : k ∈ {i | 1 < f (v i)}
hi : v i⁻¹ = v j * v k
⊢ v j = 1 ∨ v k = 1
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : G₀
⊢ (fst G₀ H₀) ((inl G₀ H₀) x) = x

Tactic:
by
  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  simp [WithZero.withZeroUnitsEquiv, fst, inl]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
r₁ s₁ r₂ s₂ : A
hr₁ : f r₁ ≠ 0
hs₁ : f s₁ ≠ 0
hr₂ : f r₂ ≠ 0
hs₂ : f s₂ ≠ 0
⊢ mk f r₁ s₁ hr₁ hs₁ = mk f r₂ s₂ hr₂ hs₂ ↔ f (r₁ * s₂) = f (r₂ * s₁)

Tactic:
simp only [mk, Subtype.mk.injEq, map_mul]
  rw [inv_mul_eq_inv_mul_iff_mul_eq_mul, eq_comm]
  simp [Units.ext_iff, mul_comm (f r₂), mul_comm (f s₂)]

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

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

Tactic:
refine ⟨?_, ConcreteCategory.mono_of_injective f⟩
  intro _ a₁ a₂ h
  let X := of (ULift (Fin 1))
  let g₁ : X ⟶ A := ofHom ⟨fun _ => a₁, fun _ _ _ => by rfl⟩
  let g₂ : X ⟶ A := ofHom ⟨fun _ => a₂, fun _ _ _ => by rfl⟩
  change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
  have eq : g₁ ≫ f = g₂ ≫ f := by
    ext
    exact h
  rw [cancel_mono] at eq
  rw [eq]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
⊢ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
X

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
⊢ ∀ (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ (Fork.ofι i ⋯).pt
hm : m ≫ i = s.ι
⊢ m = (m ≫ i) ≫ e

Tactic:
simp only [assoc, h₁]

Goal state after:
case right
C : Type u_1
inst✝ : Category.{v_1, u_1} C
a✝ : IsIdempotentComplete C
X : C
p : X ⟶ X
hp : p ≫ p = p
Y : C
i : Y ⟶ X
e : X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = p
s : Fork (𝟙 X) p
m : s.pt ⟶ (Fork.ofι i ⋯).pt
hm : m ≫ i = s.ι
⊢ m = m ≫ 𝟙 Y
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mp
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), p ≫ p = p → HasKernel p

Tactic:
X

Goal state after:
case mp
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), p ≫ p = p → HasKernel p
Module: Mathlib.CategoryTheory.Idempotents.Basic

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

Tactic:
X

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
X : C
⊢ ∀ (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : (toOrderHom f) 0 = (toOrderHom g) 0
h1 : (toOrderHom f) 1 = (toOrderHom g) 1
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Tactic:
match i with
  | 0 => exact h0 ▸ rfl
  | 1 => exact h1 ▸ rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Epi f
Z✝ : Karoubi C
g h : (toKaroubi C).obj Y✝ ⟶ Z✝
eq : (toKaroubi C).map f ≫ g = (toKaroubi C).map f ≫ h
⊢ g = h

Tactic:
ext
    rw [← cancel_epi f]
    simpa using eq

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

Tactic:
exact H.trans_lt hjk

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

Goal state before:
pp: n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑((Hom.toOrderHom (δ ⟨i, hi⟩.castSucc ≫ σ ⟨i, hi⟩)) ⟨j, hj⟩) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) ⟨j, hj⟩)

Tactic:
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]

Goal state after:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ ↑(if h : ⟨i, ⋯⟩ < if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩ then
        (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).pred ⋯
      else (if ⟨j, ⋯⟩ < ⟨i, ⋯⟩ then ⟨j, ⋯⟩ else ⟨j + 1, ⋯⟩).castPred ⋯) =
    j
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ : C ⥤ D
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { app := fun A ↦ { left := whiskerLeft (drop.obj A) (x✝¹ ≫ x✝), right := (x✝¹ ≫ x✝).app (point.obj A), w := ⋯ },
      naturality := ⋯ } =
    { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝¹, right := x✝¹.app (point.obj A), w := ⋯ },
        naturality := ⋯ } ≫
      { app := fun A ↦ { left := whiskerLeft (drop.obj A) x✝, right := x✝.app (point.obj A), w := ⋯ }, naturality := ⋯ }

Tactic:
by ext <;> rfl

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

Goal state before:
pp: Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e✝ : Δ ⟶ Δ'
inst✝¹ : Epi e✝
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e✝ ≫ i = φ
this : StrongEpi e✝
e : Δ' ≅ image φ := ⋯
⊢ (image φ).len = Δ'.len

Tactic:
exact le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x ↦ f✝.right) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x ↦ g.right) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (n.len + 1)
⊢ g.right ⟶ g.cechConerve.obj n

Tactic:
apply WidePushout.ι _ i

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:
rw [isIso_iff_bijective]

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
x : X _⦋m⦌
⊢ ofSimplex ((ConcreteCategory.hom (X.map f.op)) x) ≤ ofSimplex x

Tactic:
simp only [Subfunctor.ofSection_le_iff]
  exact ⟨f.op, by simp⟩

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
inst✝ : Epi f
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ IsIso f

Tactic:
by
  obtain ⟨x, hx⟩ := x
  induction m using SimplexCategory.rec with | _ m
  rw [mem_nonDegenerate_iff_notMem_degenerate] at hx
  by_contra hf
  refine hx ⟨_, not_le.1 (fun h ↦ hf ?_), f, y, hy⟩
  rw [SimplexCategory.isIso_iff_of_epi]
  exact le_antisymm h (SimplexCategory.len_le_of_epi f)

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
⊢ Mono f

Tactic:
have := X.isIso_of_nonDegenerate x (factorThruImage f) (y := X.map (image.ι f).op y) (by
      rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy])

Goal state after:
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 f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case neg
X : SSet
inst✝ : X.Finite
this : Fintype X.N
φ : X.N → ℕ := fun x ↦ x.dim
h : ¬(Finset.image φ ⊤).Nonempty
⊢ ∃ d, ∀ s ∈ Finset.image φ ⊤, s < d

Tactic:
· rw [Finset.not_nonempty_iff_eq_empty] at h
      simp only [h]
      exact ⟨0, by simp⟩

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

Goal state before:
pp: case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 2 Edge._proof_2 _proof_2).op ≫ (δ₂ 1 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 2 Edge._proof_2 _proof_2).op ≫ (δ₂ 0 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 0 Edge._proof_2 _proof_2).op ≫ (δ₂ 1 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 0 Edge._proof_2 _proof_2).op ≫ (δ₂ 0 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 1 Edge._proof_2 _proof_2).op ≫ (δ₂ 1 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
← Functor.map_comp_apply,

Goal state after:
case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map ((δ₂ 1 Edge._proof_2 _proof_2).op ≫ (δ₂ 0 Edge._proof_1 _proof_3).op))) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    (id x).edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 0 _proof_2 Edge._proof_2).op ≫ (δ₂ 2 Edge._proof_2 _proof_2).op))) e.edge =
    (id x).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 0 _proof_2 Edge._proof_2).op ≫ (δ₂ 0 Edge._proof_2 _proof_2).op))) e.edge = e.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 0 _proof_2 Edge._proof_2).op ≫ (δ₂ 1 Edge._proof_2 _proof_2).op))) e.edge = e.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 1 _proof_2 Edge._proof_2).op ≫ (δ₂ 2 Edge._proof_2 _proof_2).op))) e.edge = e.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    (id y).edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 1 _proof_2 Edge._proof_2).op ≫ (δ₂ 0 Edge._proof_2 _proof_2).op))) e.edge =
    (id y).edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op))
      ((ConcreteCategory.hom (X.map (σ₂ 1 _proof_2 Edge._proof_2).op)) e.edge) =
    e.edge

Tactic:
← Functor.map_comp_apply,

Goal state after:
X Y : Truncated 2
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge._proof_1 })
e : Edge x y
⊢ (ConcreteCategory.hom (X.map ((σ₂ 1 _proof_2 Edge._proof_2).op ≫ (δ₂ 1 Edge._proof_2 _proof_2).op))) e.edge = e.edge
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.left e.edge = nerveEquiv x

Tactic:
simp only [← e.src_eq]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.left e.edge = nerveEquiv ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) e.edge)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ ComposableArrows.arrowEquiv.symm
      (Arrow.mk (ComposableArrows.map' h'.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝)) =
    ComposableArrows.arrowEquiv.symm
      (Arrow.mk (ComposableArrows.map' h.simplex 0 1 ComposableArrows.homMk₁._proof_4 _proof_246✝))

Tactic:
by simp [-Edge.CompStruct.d₂, h'₂, ← h₂]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ Even i → ψ = φ

Tactic:
intro hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
hi : Even i
⊢ ψ = φ
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
⊢ ¬Even i → φ = ψ

Tactic:
intro hi

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Odd j
hi : ¬Even i
⊢ φ = ψ