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

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ IntFractPair.stream v (n' + 1) ≠ none

Tactic:
simp [stream_nth_eq]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Type u_3
e : I → R
inst✝ : DecidableEq I
H : ∀ (i j : I), e i * e j = if i = j then e i else 0
i : I
⊢ IsIdempotentElem (e i)

Tactic:
simpa using! H i i

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
| 1 - (1 - x ^ n) ^ n - (1 - (1 - x ^ n) ^ n) ^ 2

Tactic:
rw [pow_two, ← mul_one_sub, sub_sub_cancel]

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
| (1 - (1 - x ^ n) ^ n) * (1 - x ^ n) ^ n
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
i j : n
⊢ ⇑c.ofMatrix = Relation.Map (⇑c) (fun x ↦ x i j) fun x ↦ x i j

Tactic:
ext x y
  constructor
  · intro h
    refine ⟨_,_, h i j, ?_⟩
    simp
  · rintro ⟨X, Y, h, rfl, rfl⟩ i' j'
    simpa using c.mul (c.mul (c.refl <| single i' i 1) h) (c.refl <| single j j' 1)

Goal state after:
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
⊢ matrix n I ≤ matrix n J → I ≤ J

Tactic:
intro le

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
⊢ I ≤ J
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ (trace R M) f = ∑ i ∈ hN.toFinset, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
rw [← Finset.sum_coe_sort, trace_eq_sum_trace_restrict (isInternal_ne_bot_iff.mpr h) (hf ·)]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : ι → Submodule R M
inst✝² : DecidableEq ι
inst✝¹ : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯) = ∑ i, (trace R ↥(N ↑i)) (f.restrict ⋯)
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
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f : M →ₗ[R] R
x : M
⊢ ((toMatrix (Free.chooseBasis R M) (Free.chooseBasis R M))
        (f.smulRight (∑ i, ((Free.chooseBasis R M).repr x) i • (Free.chooseBasis R M) i))).trace =
    f (∑ i, ((Free.chooseBasis R M).repr x) i • (Free.chooseBasis R M) i)

Tactic:
simp [-Basis.sum_repr, dotProduct]

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
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R N
inst✝² : Module.Finite R N
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) (g ∘ₗ f ∘ₗ h) = (trace R N) (f ∘ₗ h ∘ₗ g)

Tactic:
trace_comp_comm',

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R N
inst✝² : Module.Finite R N
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R N) ((f ∘ₗ h) ∘ₗ g) = (trace R N) (f ∘ₗ h ∘ₗ g)
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
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R P) ((g ∘ₗ f) ∘ₗ h) = (trace R M) ((h ∘ₗ g) ∘ₗ f)

Tactic:
trace_comp_comm',

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R P
inst✝ : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
⊢ (trace R M) (h ∘ₗ g ∘ₗ f) = (trace R M) ((h ∘ₗ g) ∘ₗ f)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R N) ((↑e ∘ₗ f) ∘ₗ ↑e.symm) = (trace R M) f

Tactic:
trace_comp_comm',

Goal state after:
case pos
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
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this✝² : Module.Finite R M
this✝¹ : Free R M
this✝ : Module.Finite R N
this : Free R N
⊢ (trace R M) (↑e.symm ∘ₗ ↑e ∘ₗ f) = (trace R M) f
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 : ℕ
⊢ ∑ i ∈ range n, x⁻¹ ^ i = (x - 1)⁻¹ * (x - x⁻¹ ^ n * x)

Tactic:
by
  have h₁ : x⁻¹ ≠ 1 := by rwa [inv_eq_one_div, Ne, div_eq_iff_mul_eq hx0, one_mul]
  have h₂ : x⁻¹ - 1 ≠ 0 := mt sub_eq_zero.1 h₁
  have h₃ : x - 1 ≠ 0 := mt sub_eq_zero.1 hx1
  have h₄ : x * (x ^ n)⁻¹ = (x ^ n)⁻¹ * x :=
    Nat.recOn n (by simp) fun n h => by
      rw [pow_succ', mul_inv_rev, ← mul_assoc, h, mul_assoc, mul_inv_cancel₀ hx0, mul_assoc,
        inv_mul_cancel₀ hx0]
  rw [geom_sum_eq h₁, div_eq_iff_mul_eq h₂, ← mul_right_inj' h₃, ← mul_assoc, ← mul_assoc,
    mul_inv_cancel₀ h₃]
  simp only [inv_pow, sub_eq_add_neg, mul_add, one_mul, mul_neg, add_mul, mul_inv_cancel₀ hx0,
    neg_mul, mul_assoc, mul_one, add_comm, neg_add_rev, neg_neg, h₄, add_left_comm]
  rw [add_comm _ (-x), add_assoc, add_assoc _ _ 1]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : a = 0
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝² : AddCommMonoid α
inst✝¹ : DivisionSemiring γ
inst✝ : Module γ α
h : Periodic f c
a : γ
x : α
ha : ¬a = 0
⊢ (fun x ↦ f (a • x)) (x + a⁻¹ • c) = (fun x ↦ f (a • x)) x
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
· exact Red.cons_cons ih

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
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
⊢ a ∣ b

Tactic:
by_cases ha : a = 0

Goal state after:
case pos
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
ha : a = 0
⊢ a ∣ b

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
ha : ¬a = 0
⊢ a ∣ b
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
P : R[X]
hP : P.natDegree < P.natDegree + 1
⊢ (Δ_[1]^[P.natDegree + 1] fun x ↦ eval x P) = 0

Tactic:
exact Polynomial.fwdDiff_iter_eq_zero_of_degree_lt hP

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

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a b c : α
⊢ c ≠ 0 ∧ SemiconjBy c a b ↔ c ≠ 0 ∧ c * a * c⁻¹ = b

Tactic:
exact and_congr_right (mul_inv_eq_iff_eq_mul₀ · |>.symm)

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
a b : ↑Y.1
h : φ b < φ a
H : (ConcreteCategory.hom f) (φ b) ≤ (ConcreteCategory.hom f) (φ a)
⊢ b ≤ a

Tactic:
simpa only [hφ] using H

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete (Karoubi C)

Tactic:
refine ⟨?_⟩
  intro P p hp
  simp only [hom_ext_iff, comp_f] at hp
  use ⟨P.X, p.f, hp⟩
  use ⟨p.f, by rw [comp_p p, hp]⟩
  use ⟨p.f, by rw [hp, p_comp p]⟩
  simp [hp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P.p ≫ e ≫ ((toKaroubi C).obj Y).p = e

Tactic:
by simp [Category.assoc, h₁, ← h₂]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ } ⟶ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
by exact Hom.mk f.f (by simp)

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 ≤ (j.predAbove k).castSucc

Tactic:
rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]

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

Goal state before:
pp: case last
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ j.predAbove (i.castSucc.predAbove (Fin.last ⦋n + 1 + 1⦌.len)) =
    i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))

Tactic:
simp only [len_mk, Fin.predAbove_right_last]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).map f ≫
      (((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).toSingle₀Equiv
            (SimplicialObject.Augmented.point.obj Y)).symm
        ⟨Y.hom.app (op ⦋0⦌), ⋯⟩ =
    (((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).toSingle₀Equiv
            (SimplicialObject.Augmented.point.obj X)).symm
        ⟨X.hom.app (op ⦋0⦌), ⋯⟩ ≫
      (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).map f

Tactic:
apply HomologicalComplex.to_single_hom_ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X Y : SimplicialObject.Augmented C
f : X ⟶ Y
⊢ ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).map f ≫
          (((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj Y)).symm
            ⟨Y.hom.app (op ⦋0⦌), ⋯⟩).f
      0 =
    ((((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).toSingle₀Equiv
                (SimplicialObject.Augmented.point.obj X)).symm
            ⟨X.hom.app (op ⦋0⦌), ⋯⟩ ≫
          (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C).map f).f
      0
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : ¬y₁ < y₂
⊢ (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
    (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂

Tactic:
rw [eq_of_le_of_not_lt h h']

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

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ Fin.castSucc 0 < (ConcreteCategory.hom (σ₀Iter i ⋯)) k

Tactic:
rw [Fin.lt_def, Fin.castSucc_zero, σ₀Iter_coe_eq_of_ge ..,
      Fin.coe_ofNat_eq_mod, Nat.zero_mod]

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
hk : i < ↑k
⊢ 0 < ↑k - i
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : i ≤ k.castSucc
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

Tactic:
· rw [Fin.succAbove_of_le_castSucc _ _ hk', σ₀Iter_coe_eq_of_lt ..]

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
rintro ⟨m, hm, f, y, 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 f.op)) y = x
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
by
  have := isIso_factorThruImage_g hf₁ hy₁ hy₂
  rw [← image.fac (g hf₁ f₂)]
  infer_instance

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ x₁ = y₁

Tactic:
rw [← hom.tgt_eq, hhom, hom'.tgt_eq]

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id x₁).edge = (id y₁).edge

Tactic:
rw [← hom.tgt_eq, hhom, hom'.tgt_eq]

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ face S = Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))

Tactic:
apply le_antisymm
  · rintro ⟨k⟩ x hx
    induction k using SimplexCategory.rec with | _ k
    rw [mem_face_iff] at hx
    let φ : Fin (k + 1) →o S :=
      { toFun i := ⟨x i, hx i⟩
        monotone' := (objEquiv x).toOrderHom.monotone }
    refine ⟨Quiver.Hom.op
      (SimplexCategory.Hom.mk ((e.symm.toOrderEmbedding.toOrderHom.comp φ))), ?_⟩
    ext j : 1
    simpa only [Subtype.ext_iff] using! e.apply_symm_apply ⟨_, hx j⟩
  · simp

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)
⊢ ¬↑x b < ↑x a → ¬b < a

Tactic:
intro h 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
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Epi (toOfSimplex x)

Tactic:
rw [← range_eq_top_iff]
  ext m ⟨_, u, rfl⟩
  simp only [range_eq_ofSimplex, yonedaEquiv_toOfSimplex, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
  refine ⟨u, ?_⟩
  dsimp
  ext
  rw [← yonedaEquiv.right_inv x]
  aesop

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 ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i j →
    (match i with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))) ≫
        ((truncate.obj C).augment (C.d 0 1) ⋯).d i j =
      C.d i j ≫
        match j with
        | 0 => 𝟙 (C.X 0)
        | n.succ => 𝟙 (C.X (n + 1))

Tactic:
rcases j with (_ | _ | j) <;> rcases i with - | i <;> aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
⊢ ExtraDegeneracy.s f S n ≫ f.augmentedCechNerve.left.δ 0 = 𝟙 (f.augmentedCechNerve.left _⦋n⦌)

Tactic:
by
    dsimp [SimplicialObject.δ, SimplexCategory.δ]
    cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (shiftFunctor C c).map ((↑(t.z a b)).app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
t.shift_z_app,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫
        (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom ≫
          (↑(t.z a b)).app ((shiftFunctor C c).obj ((shiftFunctor C b).obj ((shiftFunctor C a).obj X))) =
    (↑(t.z a (b + c))).app ((shiftFunctor C (a + b + c)).obj X) ≫
      (↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
        eqToHom ⋯ ≫
          ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0

Tactic:
dsimp [d₁]
  rw [shape _ _ _ h, Functor.map_zero, zero_app, Functor.map_zero, zero_app, zero_comp, smul_zero]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5} C₃
inst✝¹⁶ : Category.{v_4, u_6} C₄
inst✝¹⁵ : Category.{v_5, u_3} C₁₂
inst✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝⁹ : F₁₂.PreservesZeroMorphisms
inst✝⁸ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁷ : G.Additive
inst✝⁶ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁵ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0

Tactic:
by
  dsimp [d₂]
  rw [shape _ _ _ h, Functor.map_zero, Functor.map_zero, zero_app, zero_comp, smul_zero]

Goal state after: