mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ (fun x1 x2 ↦ x1 * x2) <$> Functor.Comp.mk (traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y))

Tactic:
Functor.Comp.map_mk

Goal state after:
α β : 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✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (pure x) = Functor.Comp.mk (traverse f <$> traverse g (pure x))
ih2 : traverse (Functor.Comp.mk ∘ Functor.map f ∘ g) y = Functor.Comp.mk (traverse f <$> traverse g y)
⊢ Functor.Comp.mk ((fun x ↦ (fun x1 x2 ↦ x1 * x2) <$> x) <$> traverse f <$> traverse g (pure x)) <*>
      Functor.Comp.mk (traverse f <$> traverse g y) =
    Functor.Comp.mk (traverse f <$> ((fun x1 x2 ↦ x1 * x2) <$> traverse g (pure x) <*> traverse g y))
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ star a = ↑(2 * a.re) - a

Tactic:
by
  simpa using! QuaternionAlgebra.star_eq_two_re_sub a

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

Tactic:
by
  induction n with
  | zero => rw [npow_zero, mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]

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

Goal state before:
pp: case succ
M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
h : M
n : ℕ
IH : ∀ (x : M), Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x
x : M
⊢ Δ_[h]^[n + 1] (⇑φ) x = (φ h - 1) ^ (n + 1) * φ x

Tactic:
simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]
    rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]

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
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

Tactic:
replace hi : v i = v j⁻¹ * v k⁻¹ := by
    rwa [hv_inv, inv_eq_iff_eq_inv, mul_inv, ← hv_inv, ← hv_inv] at hi

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.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
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' v '' IsMulIndecomposable.baseOf v f' = v '' IsMulIndecomposable.baseOf v f

Tactic:
IsMulIndecomposable.image_baseOf_inv_comp_eq v hv_inv f,

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}
f' : G →* S := invMonoidHom.comp f
⊢ ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f = v '' IsMulIndecomposable.baseOf v f
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inl
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k ∈ t
⊢ False

pp: case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ False

Tactic:
· suffices ¬ IsMulIndecomposable v t i from this (hst hi)
    simp only [IsMulIndecomposable, hv_one, or_self, imp_false, not_and, not_forall, not_not]
    exact fun _ ↦ ⟨k, hk', j, h_sub hj, by simp [hk]⟩

Goal state after:
case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ False
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
⊢ SemigroupWithZero α

Tactic:
apply e.injective.semigroupWithZero _ <;> intros

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := ⋯
zero : Zero α := ⋯
⊢ e 0 = 0

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : SemigroupWithZero β
mul : Mul α := e.mul
zero : Zero α := e.zero
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case some
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
⊢ some ⟨x, hx⟩ = 0 ∨ ∃ r s, ∃ (hr : f r ≠ 0) (hs : f s ≠ 0), some ⟨x, hx⟩ = ↑(valueGroup.mk f r s hr hs)

Tactic:
· rw [mem_valueGroup_iff_of_comm'] at hx
    obtain ⟨r, hr, s, hs, hrs⟩ := hx
    refine .inr ⟨r, s, hr, hs, Option.some_inj.mpr <| by
      simp only [valueGroup.mk, Subtype.mk.injEq]
      rw [eq_inv_mul_iff_mul_eq]
      simp [← hrs, mul_comm]⟩

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

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
⊢ Monotone φ

Tactic:
intro a b

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
⊢ a ≤ b → φ a ≤ φ b
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 : ℕ
⊢ f.app (op ⦋n + 1⦌) ≫ ∑ i, (-1) ^ ↑i • Y.δ i = (∑ i, (-1) ^ ↑i • X.δ i) ≫ f.app (op ⦋n⦌)

Tactic:
rw [comp_sum, sum_comp]

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 : ℕ
⊢ ∑ j, f.app (op ⦋n + 1⦌) ≫ ((-1) ^ ↑j • Y.δ j) = ∑ j, ((-1) ^ ↑j • X.δ j) ≫ f.app (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ j ≫ X.σ i.castSucc = X.σ i ≫ X.σ j.succ

Tactic:
by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.σ_comp_σ 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
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X Y : CosimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ f.app ⦋n⦌ ≫ ∑ i, (-1) ^ ↑i • Y.δ i = (∑ i, (-1) ^ ↑i • X.δ i) ≫ f.app ⦋n + 1⦌

Tactic:
rw [comp_sum, sum_comp]

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 : ℕ
⊢ ∑ j, f.app ⦋n⦌ ≫ ((-1) ^ ↑j • Y.δ j) = ∑ j, ((-1) ^ ↑j • X.δ j) ≫ f.app ⦋n + 1⦌
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j' + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'

Tactic:
obtain rfl : j = j' := by lia

Goal state after:
case zero
n : ℕ
j : Fin (n + 1)
hi' : n + 0 = n
hj' : ↑j = ↑j + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j ≫ δ₀Iter 0 hi'
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n : ℕ
j' j : Fin (n + 1)
hi : n + 0 = n
hj : ↑j = ↑j' + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j'

Tactic:
obtain rfl : j = j' := by lia

Goal state after:
case zero
n : ℕ
j : Fin (n + 1)
hi : n + 0 = n
hj : ↑j = ↑j + 0
⊢ σ j ≫ σ₀Iter 0 hi = σ₀Iter 0 ⋯ ≫ σ j
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'
⊢ (ConcreteCategory.hom (f.app X)) x ∈ (ofSection ((ConcreteCategory.hom (f.app X)) x)).obj X

Tactic:
exact ⟨𝟙 X, by simp⟩

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

Goal state before:
pp: X : SSet
⊢ X.nonDegenerate 0 = Set.univ

Tactic:
simp [nonDegenerate]

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

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

Tactic:
simp [nonDegenerate]

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

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map f.op)) y = x
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
rw [← image.fac f, op_comp] at hy

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map ((image.ι f).op ≫ (factorThruImage f).op))) y = x
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

pp: case h₂.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x

Tactic:
· dsimp
        simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right,
          SimplexCategory.len_mk, Arrow.cechConerve_map, colimit.ι_desc,
          WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
        rfl

Goal state after:
case h₂.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
x✝ : SimplexCategoryᵒᵖ
x : Y.obj x✝
⊢ (∃ x_1 ∈ A.obj x✝, (ConcreteCategory.hom (f.app x✝)) x_1 = x) → (ConcreteCategory.hom (inv (f.app x✝))) x ∈ A.obj x✝

Tactic:
by rintro ⟨x, hx, rfl⟩; simpa

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

Goal state before:
pp: case zero
X : Type u_1
inst✝ : PartialOrder X
s : nerve X _⦋0⦌
⊢ s ∈ (nerve X).nonDegenerate 0 ↔ StrictMono s.obj

pp: case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj

Tactic:
· simpa using Subsingleton.strictMono _

Goal state after:
case succ
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
⊢ s ∈ (nerve X).nonDegenerate (n + 1) ↔ StrictMono s.obj
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 1 2 _proof_246✝ _proof_247✝)) =
    ComposableArrows.arrowEquiv.symm (Arrow.mk (ComposableArrows.map' h.simplex 1 2 _proof_246✝ _proof_247✝))

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

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

Goal state before:
pp: case inl.zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Even 0
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) 0

pp: case inl.succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) (n + 1)

Tactic:
· exact ⟨⟨alternatingConstHomologyDataZero X _ rfl⟩⟩

Goal state after:
case inl.succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
intro a b

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
h : ¬↑x b < ↑x a
h' : b < a
⊢ ↑x b < ↑x a

Tactic:
obtain h'' | h'' := (monotone_apply x.val h'.le).lt_or_eq

Goal state after:
case mp.inl
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
h : ¬↑x b < ↑x a
h' : b < a
h'' : (fun j ↦ ↑x j) b < (fun j ↦ ↑x j) a
⊢ ↑x b < ↑x a

case mp.inr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
h : ¬↑x b < ↑x a
h' : b < a
h'' : (fun j ↦ ↑x j) b = (fun j ↦ ↑x j) a
⊢ ↑x b < ↑x a
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
x✝¹ x✝ : HomologicalComplex₂ C c₁ c₂
φ₁ φ₂ : x✝¹ ⟶ x✝
h : (toGradedObjectFunctor C c₁ c₂).map φ₁ = (toGradedObjectFunctor C c₁ c₂).map φ₂
⊢ φ₁ = φ₂

Tactic:
ext i₁ i₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
x✝¹ x✝ : HomologicalComplex₂ C c₁ c₂
φ₁ φ₂ : x✝¹ ⟶ x✝
h : (toGradedObjectFunctor C c₁ c₂).map φ₁ = (toGradedObjectFunctor C c₁ c₂).map φ₂
i₁ : I₁
i₂ : I₂
⊢ (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂
Module: Mathlib.Algebra.Homology.Bifunctor

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

Tactic:
Functor.map_zero

Goal state after:
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₂
h₂ : ¬c₂.Rel i₂ i₂'
⊢ 0 = 0
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.obj (K₁.X i₁)).map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
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₂
⊢ 0 = 0
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 : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
j : J
c₂₃ : (i₂₃ : ρ₂₃.I₂₃) → (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).CofanMapObjFun ρ₂₃.p i₂₃ :=
  fun i₂₃ ↦ (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).cofanMapObj ρ₂₃.p i₂₃
h₂₃ : (i₂₃ : ρ₂₃.I₂₃) → IsColimit (c₂₃ i₂₃)
c : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).CofanMapObjFun ρ₂₃.q j :=
  (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).cofanMapObj ρ₂₃.q j
hc : IsColimit c
c₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) →
  Cocone (Discrete.functor ((((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).mapObjFun ρ₂₃.p (↑i).2) ⋙ F.obj (X₁ (↑i).1)) :=
  fun i ↦ (F.obj (X₁ (↑i).1)).mapCocone (c₂₃ (↑i).2)
hc₂₃' : (i : ↑(ρ₂₃.q ⁻¹' {j})) → IsColimit (c₂₃' i)
Z : GradedObject (I₁ × I₂ × I₃) C₄ := (((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃
p' : I₁ × I₂ × I₃ → I₁ × ρ₂₃.I₂₃ :=
  fun x ↦
    match x with
    | (i₁, i₂, i₃) => (i₁, ρ₂₃.p (i₂, i₃))
i₁ : I₁
i₂₃ : ρ₂₃.I₂₃
x✝ : ↑(p' ⁻¹' {(i₁, i₂₃)})
i₁' : I₁
i₂ : I₂
i₃ : I₃
hi : (i₁', i₂, i₃) ∈ p' ⁻¹' {(i₁, i₂₃)}
⊢ (fun x ↦
        match x with
        | ⟨(i₂, i₃), hi⟩ => ⟨(i₁, i₂, i₃), ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨(i₁', i₂, i₃), hi⟩ => ⟨(i₂, i₃), ⋯⟩)
        ⟨(i₁', i₂, i₃), hi⟩) =
    ⟨(i₁', i₂, i₃), hi⟩

Tactic:
obtain rfl : i₁ = i₁' := by cat_disch
        rfl

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₁Iso x).hom.f n ≫ (total.map f (up ℤ)).f (n + x)

Tactic:
K.ι_totalShift₁Iso_hom_f_assoc x i₁ i₂ n h _ rfl _ rfl

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₁ C x).map f).f i₁).f i₂ ≫
      (L.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
        L.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
          (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) x n (n + x) ⋯).inv =
    (K.shiftFunctor₁XXIso i₁ x (i₁ + x) ⋯ i₂).hom ≫
      K.ιTotal (up ℤ) (i₁ + x) i₂ (n + x) ⋯ ≫
        (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n (n + x) ⋯).inv ≫ (total.map f (up ℤ)).f (n + x)