mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
exact h

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)
⊢ (trace R M) (g ∘ₗ f) = (trace R N) (f ∘ₗ g)

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : Ring β
h : Antiperiodic f c
n : ℕ
⊢ f (↑n * c - x) = (-1) ^ n * f (-x)

Tactic:
by
  simpa only [nsmul_eq_mul, zsmul_eq_mul, Int.cast_pow, Int.cast_neg,
    Int.cast_one] using h.nsmul_sub_eq n

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Injective ⇑i₂
hi₄ : Function.Injective ⇑i₄
x : M₂
hm : i₃ (f₂ x) = 1
a : M₁
hy : g₁ (i₁ a) = i₂ x
⊢ g₁ (i₁ a) = i₂ (f₁ a)

Tactic:
simpa using DFunLike.congr_fun hc₁ a

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x✝ y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝³ : SMul S R
inst✝² : SMul T R
s✝ : S
inst✝¹ : SMul S T
inst✝ : IsScalarTower S T R
s : S
t : T
x : ℍ[R,c₁,c₂,c₃]
⊢ (s • t) • x = s • t • x

Tactic:
by ext <;> exact smul_assoc _ _ _

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]

Tactic:
apply (equivProd c₁ c₂ c₃).injective.addCommGroup <;> intros

Goal state after:
case zero
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
⊢ (equivProd c₁ c₂ c₃) 0 = 0

case add
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ + y✝) = (equivProd c₁ c₂ c₃) x✝ + (equivProd c₁ c₂ c₃) y✝

case neg
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (-x✝) = -(equivProd c₁ c₂ c₃) x✝

case sub
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ y✝ : ℍ[R,c₁,c₂,c₃]
⊢ (equivProd c₁ c₂ c₃) (x✝ - y✝) = (equivProd c₁ c₂ c₃) x✝ - (equivProd c₁ c₂ c₃) y✝

case nsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℕ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝

case zsmul
S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroup R
x✝ : ℍ[R,c₁,c₂,c₃]
n✝ : ℤ
⊢ (equivProd c₁ c₂ c₃) (n✝ • x✝) = n✝ • (equivProd c₁ c₂ c₃) x✝
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
use m, r, hg, hr

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : f.IsPrimitive
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ⋯
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
⊢ m = 0 → IsUnit g
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 : U
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = x

pp: case refine_2.refine_2
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 : U
⊢ (∃ y, (algebraMap S U) y = x) → IsIntegral R x

Tactic:
· obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := T) (A := T)).mp h.tower_top
      rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h
      obtain ⟨x, rfl⟩ := (IsIntegralClosure.isIntegral_iff (R := R) (A := S)).mp h
      exact ⟨x, IsScalarTower.algebraMap_apply ..⟩

Goal state after:
case refine_2.refine_2
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 : U
⊢ (∃ y, (algebraMap S U) y = x) → IsIntegral R x
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) (a * k)

Tactic:
rw [map_mul, hk, mul_div_cancel₀ _ ha]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ a • s = univ ↔ s = univ

Tactic:
by
  rw [smul_eq_iff_eq_inv_smul, smul_finset_univ]

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

Goal state before:
pp: M : Type u_1
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Mul (α i)
inst✝¹ : (i : ι) → Pow (α i) ℕ+
inst✝ : ∀ (i : ι), PNatPowAssoc (α i)
x✝³ x✝² : ℕ+
x✝¹ : (i : ι) → α i
x✝ : ι
⊢ (x✝¹ ^ (x✝³ + x✝²)) x✝ = (x✝¹ ^ x✝³ * x✝¹ ^ x✝²) x✝

Tactic:
simp [ppow_add]

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

Goal state before:
pp: case fst
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).1 = (x✝ ^ x✝² * x✝ ^ x✝¹).1

Tactic:
simp [ppow_add]

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

Goal state before:
pp: case snd
M : Type u_1
N : Type u_2
inst✝⁵ : Mul M
inst✝⁴ : Pow M ℕ+
inst✝³ : PNatPowAssoc M
inst✝² : Mul N
inst✝¹ : Pow N ℕ+
inst✝ : PNatPowAssoc N
x✝² x✝¹ : ℕ+
x✝ : M × N
⊢ (x✝ ^ (x✝² + x✝¹)).2 = (x✝ ^ x✝² * x✝ ^ x✝¹).2

Tactic:
simp [ppow_add]

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

Goal state before:
pp: case inr.inr
m n : ℕ
hnm : n < m
⊢ Δ_[1]^[n] (fun x ↦ ↑(x.choose m)) 0 = if n = m then 1 else 0

Tactic:
rcases Nat.exists_eq_add_of_lt hnm with ⟨k, rfl⟩
    simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
x : R
⊢ Δ_[1]^[P.natDegree] (fun x ↦ eval x P) x = (P.leadingCoeff • ↑P.natDegree !) x

Tactic:
simp_rw [P.eval_eq_sum_range, ← sum_apply _ _ (fun i x ↦ P.coeff i * x ^ i),
    fwdDiff_iter_finsetSum, ← smul_eq_mul, ← Pi.smul_def, fwdDiff_iter_const_smul, Pi.smul_apply]
  rw [sum_apply, sum_range_succ, sum_eq_zero (fun i hi ↦ ?_), zero_add,
    fwdDiff_iter_eq_factorial, leadingCoeff, Pi.smul_apply]
  rw [fwdDiff_iter_pow_eq_zero_of_lt (mem_range.mp hi), smul_zero, Pi.zero_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommGroup M
ι : Type u_2
f : ι → M
x : M
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤

Tactic:
rwa [← (comap_injective hφ).ne_iff, comap_top] at hM

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
hx : x ∈ closure (Set.range f)
⊢ ∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2

Tactic:
induction hx using closure_induction with

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 i = v j⁻¹ * v k⁻¹

Tactic:
mul_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 i = v j⁻¹ * v k⁻¹
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ range ⇑(restrict₀ f) = univ

Tactic:
range_eq_univ

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ Function.Surjective ⇑(restrict₀ f)
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
x✝ : ↑X.toLinOrd
⊢ (LinOrd.Hom.hom (g₁ ≫ f).hom) x✝ = (LinOrd.Hom.hom (g₂ ≫ f).hom) x✝

Tactic:
exact h

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

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }

Tactic:
have eq : g₁ ≫ f = g₂ ≫ f := by
    ext
    exact h

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun x ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun x ↦ a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ (ConcreteCategory.hom g₁) { down := 0 } = (ConcreteCategory.hom g₂) { down := 0 }
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : IsIdempotentComplete C
⊢ IsIdempotentComplete C

Tactic:
exact h

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

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

Tactic:
rcases le_or_gt k i with (hik | hik)

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

case inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n
x✝ : SimplexCategoryᵒᵖ
⊢ f.app x✝ = g.app x✝

Tactic:
apply h

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ X : SimplicialObject C
X₀ : C
f : X _⦋0⦌ ⟶ X₀
w : ∀ (i : SimplexCategory) (g₁ g₂ : ⦋0⦌ ⟶ i), X.map g₁.op ≫ f = X.map g₂.op ≫ f
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f_1 : X_1 ⟶ Y),
    ((𝟭 (SimplicialObject C)).obj X).map f_1 ≫ X.map (⦋0⦌.const (unop Y) 0).op ≫ f =
      (X.map (⦋0⦌.const (unop X_1) 0).op ≫ f) ≫ ((const C).obj X₀).map f_1

Tactic:
by
        intro i j g
        dsimp
        rw [← g.op_unop]
        simpa only [← X.map_comp, ← Category.assoc, Category.comp_id, ← op_comp] using w _ _ _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : CosimplicialObject C
f g : X ⟶ Y
h : ∀ (n : SimplexCategory), f.app n = g.app n
x✝ : SimplexCategory
⊢ f.app x✝ = g.app x✝

Tactic:
apply h

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨2, ?_⟩
    ext i : 3
    match i with
    | 0 => exact e0
    | 1 => exact e1

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

Goal state before:
pp: x✝² x✝¹ : SimplexCategory
f g : x✝² ⟶ x✝¹
h : skeletalFunctor.map f = skeletalFunctor.map g
x✝ : Fin (x✝².len + 1)
⊢ (Hom.toOrderHom f) x✝ = (Hom.toOrderHom g) x✝

Tactic:
exact CategoryTheory.congr_fun h _

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Monotone fun S ↦ S.image f

Tactic:
by
  intro S T h
  rw [image_le_iff]
  exact h.trans (by rw [← image_le_iff])

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

Goal state before:
pp: case mk
X : SSet
inst✝ : X.Finite
n : ℕ
⊢ Finite (X _⦋n⦌)

Tactic:
| _ n
   => 

Goal state after:
case mk
X : SSet
inst✝ : X.Finite
n : ℕ
⊢ Finite (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: case inr
X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
h : Function.Injective s.obj
i j : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
hij : i < j
h' : s.obj i = s.obj j
⊢ s.obj i < s.obj j

Tactic:
· exact ((h h').not_lt hij).elim

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

Goal state before:
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 ⟨⟨alternatingConstHomologyDataEvenNEZero X _ h (by simp)⟩⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ h ed (Fin.last n) ≫ X.left.δ (Fin.last (n + 1)) = (X.hom ≫ ed.section_).app (op ⦋n⦌)

Tactic:
dsimp
    rw [h_eq_assoc _ _ 0, X.left.σ₀Iter_δ' _ _ 1 (by grind),
      ed.s₀_comp_δ₁_assoc, X.δ₀Iter_hom_app_assoc _ (by grind)]
    simp

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ stdSimplex.δ (i.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i

Tactic:
obtain ⟨i, rfl⟩ := i.eq_castSucc_of_ne_last (Fin.ne_last_of_lt h)

Goal state after:
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
h : i.castSucc < j
⊢ stdSimplex.δ (i.castSucc.castPred ⋯) ≫ stdSimplex.δ j = stdSimplex.δ (j.pred ⋯) ≫ stdSimplex.δ i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

Tactic:
constructor
  · rintro ⟨x₁, h₁⟩ ⟨x₂, h₂⟩ h₃
    obtain ⟨f₁, rfl⟩ := objEquiv.symm.surjective x₁
    obtain ⟨f₂, rfl⟩ := objEquiv.symm.surjective x₂
    simp only [mem_nonDegenerate_iff_mono, Equiv.apply_symm_apply,
      SimplexCategory.mono_iff_injective, SimplexCategory.len_mk] at h₁ h₂
    simp only [Set.mem_ofPred_eq, SimplexCategory.len_mk, Equiv.apply_symm_apply,
      Subtype.mk.injEq, EmbeddingLike.apply_eq_iff_eq] at h₃ ⊢
    apply SimplexCategory.Hom.ext
    rw [← OrderHom.range_eq_iff h₁ h₂]
    ext x
    simpa using congr_fun (congrArg Membership.mem h₃) x
  · intro ⟨S, hS⟩
    dsimp at hS
    let e := monoEquivOfFin S (k := m + 1) (by simpa using hS)
    refine ⟨⟨objMk ((OrderHom.Subtype.val _).comp e.toOrderEmbedding.toOrderHom), ?_⟩, ?_⟩
    · rw [mem_nonDegenerate_iff_mono, SimplexCategory.mono_iff_injective]
      intro a b h
      grind [e.injective, dsimp% h]
    · simp [e, ← Finset.image_image, Finset.image_univ_of_surjective e.surjective]

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

Tactic:
apply h

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

Goal state before:
pp: case mk
n : ℕ
⊢ Δ[n].Finite

Tactic:
| _ n
   => 

Goal state after:
case mk
n : ℕ
⊢ Δ[n].Finite
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc

Tactic:
rw [h_eq_assoc _ _ k, h_eq _ _ (k + 1),
      X.left.σ_δ₀Iter'_assoc _ _ ⟨l, by grind⟩
        (by grind),
      ← ed.s_comp_σ_assoc,
      X.left.σ₀Iter_σ' j i.succ ⟨l + 1, by grind⟩ (by grind)]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ X.left.δ₀Iter ↑j ⋯ ≫
      ed.s ↑k ≫
        X.left.σ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_43 n i j k hk l hl⟩ ≫
          X.left.σ₀Iter ↑j ⋯ =
    X.left.δ₀Iter (↑j.castSucc)
        (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_32 n j k hk) ≫
      ed.s ↑k ≫
        X.left.σ
            ⟨l, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_41 n i j k hk l hl⟩.succ ≫
          X.left.σ₀Iter ↑j.castSucc ⋯
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
rw [← mul_assoc, ComplexShape.σ_ε₂ c₁ c₁₂ i₁ h₂, mul_comm, ← mul_assoc,
      Int.units_mul_self, one_mul, mul_comm, ← mul_assoc, Int.units_mul_self, one_mul]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
Y : C₄
j : J
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
φ φ' : mapTrifunctorMapObj F p X₁ X₂ X₃ j ⟶ Y
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : p (i₁, i₂, i₃) = j),
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ = ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ φ'
i₁ : I₁
i₂ : I₂
i₃ : I₃
hi : p (i₁, i₂, i₃) = j
⊢ ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j hi ≫ φ =
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p (i₁, i₂, i₃) j hi ≫ φ'

Tactic:
apply h

Goal state after: