mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∏ i ∈ s✝, f i).den ∣ ∏ i ∈ s✝, (f i).den
⊢ (∏ i ∈ insert a✝ s✝, f i).den ∣ ∏ i ∈ insert a✝ s✝, (f i).den

Tactic:
simp_rw [Finset.prod_insert has]

Goal state after:
case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∏ i ∈ s✝, f i).den ∣ ∏ i ∈ s✝, (f i).den
⊢ (f a✝ * ∏ i ∈ s✝, f i).den ∣ (f a✝).den * ∏ i ∈ s✝, (f i).den
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
this : x ^ f.natDegree ∈ 𝓟
⊢ x ^ f.natDegree * x ^ k ∈ 𝓟

Tactic:
by exact mul_mem_right (x ^ k) 𝓟 this

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S) by
    intro i hi
    obtain ⟨k, hk⟩ := exists_add_of_le hi
    rw [hk, pow_add]
    exact mul_mem_right _ _ this

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
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 : T
h : IsIntegral R ((algebraMap T U) x)
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) x

Tactic:
rw [isIntegral_algebraMap_iff (IsIntegralClosure.algebraMap_injective T T U)] at h

Goal state after:
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 : T
h : IsIntegral R x
⊢ ∃ y, (algebraMap S U) y = (algebraMap T U) x
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
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hx : (algebraMap R K) b ^ n = (algebraMap R K) (a ^ n * x)
⊢ (algebraMap R K) b ^ n / (algebraMap R K) a ^ n - (algebraMap R K) x = 0

Tactic:
simp [hx, ha]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ⋯
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) = 0

Tactic:
suffices f %ₘ q = (r * s) %ₘ q by
      -- Since the coefficients of `r` and `s` are in `P`, those of `r * s` are in `P ^ 2`
      suffices h : map (Ideal.Quotient.mk (P ^ 2)) (r * s) = 0 by
        simp [this, h, map_modByMonic, hq_monic]
      ext n
      have h (x : ℕ × ℕ) : (Ideal.Quotient.mk (P ^ 2)) (r.coeff x.1 * s.coeff x.2) = 0 := by
        rw [eq_zero_iff_mem, pow_two]
        apply mul_mem_mul
        · rw [mem_ker, ← coeff_map, hr, coeff_zero]
        · rw [mem_ker, ← coeff_map, hs, coeff_zero]
      simp [-Polynomial.map_mul, coeff_mul, h]

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ f %ₘ q = r * s %ₘ q
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
inst✝ : CommRing R
r x✝ y✝ : R
a b x y : ℍ[R]
⊢ ↑(x * y * star (x * y)).re = ↑((x * star x).re * (y * star y).re)

Tactic:
conv_lhs => rw [← mul_star_eq_coe, star_mul, mul_assoc, ← mul_assoc y, y.mul_star_eq_coe,
      coe_commutes, ← mul_assoc, x.mul_star_eq_coe, ← coe_mul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
star_comm_self,

Goal state after:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ a * star a = ↑(normSq a)
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}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f)) ∧
    v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
refine ⟨le_trans ?_ (le_closure_toSubmonoid (v '' IsMulIndecomposable.baseOf v f)), ?_⟩

Goal state after:
case refine_1
ι : 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}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(Submonoid.closure (v '' IsMulIndecomposable.baseOf v f))

case refine_2
ι : 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}
⊢ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.LeftInverse (fun x ↦ (h.inv { down := x }).down) fun x ↦ (h.hom { down := x }).down

Tactic:
by
            intro a
            change ULift.down _ = _
            rw [ULift.up_down]
            change ((h.hom ≫ h.inv) _).down = _
            simp
            rfl

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

Goal state before:
pp: 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
⊢ i ≫ 𝟙 X = i ≫ p

Tactic:
comp_id,

Goal state after:
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
⊢ i = i ≫ 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 ≫ 𝟙 Y

Tactic:
exact (comp_id m).symm

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
⊢ IsIdempotentComplete C → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
intro _ X p hp
    rcases IsIdempotentComplete.idempotents_split X p hp with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
    exact
      ⟨Nonempty.intro
          { cone := Fork.ofι i (show i ≫ 𝟙 X = i ≫ p by rw [comp_id, ← h₂, ← assoc, h₁, id_comp])
            isLimit := by
              apply Fork.IsLimit.mk'
              intro s
              refine ⟨s.ι ≫ e, ?_⟩
              constructor
              · simp [h₂, ← Limits.Fork.condition s]
              · intro m hm
                rw [Fork.ι_ofι] at hm
                rw [← hm]
                simp only [assoc, h₁]
                exact (comp_id m).symm }⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ P.p ≫ P.p ≫ 𝟙 P.X = P.p

Tactic:
comp_id,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
⊢ P.p ≫ P.p = P.p
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
j j' : J
φ : j ⟶ j'
⊢ (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ 𝟙 (F.obj j') =
    (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j'

Tactic:
comp_id,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
inst✝ : IsIdempotentComplete C
F : J ⥤ C
p : F ⟶ F
hp : p ≫ p = p
hC : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
this : ∀ (j : J), HasEqualizer (𝟙 (F.obj j)) (p.app j)
j j' : J
φ : j ⟶ j'
⊢ equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ = (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ≫ p.app j'
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case i_inj
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := ⋯
S : Finset P := ⋯
φ : (ij : P) → ij ∈ S → P := ⋯
⊢ ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂

Tactic:
rintro ⟨i, j⟩ hij ⟨i', j'⟩ hij' h
    rw [Prod.mk_inj]
    exact ⟨by simpa [φ] using! congr_arg Prod.snd h,
      by simpa [φ, Fin.castSucc_castLT] using! congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h.e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
rw [CategoryTheory.SimplicialObject.δ_comp_δ'']

Goal state after:
case h.e_a.H
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
n : ℕ
⊢ X.σ₀Iter 0 ⋯ = 𝟙 (X _⦋n⦌)

Tactic:
simp [σ₀Iter]

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

Goal state before:
pp: n : ℕ
x✝ : Fin (⦋n⦌.len + 1)
⊢ ↑((Hom.toOrderHom (σ₀Iter 0 ⋯)) x✝) = ↑((Hom.toOrderHom (𝟙 ⦋n⦌)) x✝)

Tactic:
simp [σ₀Iter]

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

Goal state before:
pp: case succ
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ σ₀Iter i ⋯ ≫ σ j'.succ ≫ σ 0 = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'

Tactic:
← σ_comp_σ (by simp),

Goal state after:
case succ
i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ σ₀Iter i ⋯ ≫ σ (Fin.castSucc 0) ≫ σ j' = σ₀Iter i ⋯ ≫ σ 0 ≫ σ j'
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:
by apply WidePushout.ι _ i

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

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

Tactic:
simp only [mem_nonDegenerate_iff_notMem_degenerate,
    opObjEquiv_mem_degenerate_iff]

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

Goal state before:
pp: X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s

Tactic:
subst hd
  rfl

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

Goal state before:
pp: X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f = ⊤ ↔ range f ≤ B

Tactic:
rw [← image_top, image_le_iff, top_le_iff]

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

Goal state before:
pp: X Y : SSet
A : Y.Subcomplex
f : X ⟶ Y
inst✝ : IsIso f
⊢ A.image (inv f) = A.preimage f

Tactic:
simp [← preimage_inv]

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

Goal state before:
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:
← not_iff_not,

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.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:
by
    rw [← Functor.map_comp_apply, ← op_comp, δ₂_one_comp_σ₂_zero]
    simp

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
⊢ yonedaEquiv.symm x = const x

Tactic:
apply yonedaEquiv.injective
  simp [yonedaEquiv_const]

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

Goal state before:
pp: n : ℕ
x✝¹ : SimplexCategoryᵒᵖ
x✝ : Δ[n].obj x✝¹
⊢ x✝ ∈ (face ∅).obj x✝¹ ↔ x✝ ∈ ⊥.obj x✝¹

Tactic:
simpa using Finset.univ_neq_empty _

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

Goal state before:
pp: case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ⋯⟩ =
    ⟨S, hS⟩

Tactic:
simp [e, ← Finset.image_image, Finset.image_univ_of_surjective e.surjective]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
⊢ K.D₂ c₁₂ i₁₂ i₁₂' = 0

Tactic:
by
  ext ⟨i₁, i₂⟩ h
  simp only [totalAux.ιMapObj_D₂, comp_zero]
  by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)
  · rw [K.d₂_eq_zero' c₁₂ i₁ h₂ i₁₂']
    intro h₁
    exact h₁₂ (by simpa only [← h, ← h₁] using ComplexShape.rel_π₂ c₁ c₁₂ i₁ h₂)
  · exact d₂_eq_zero _ _ _ _ _ h₂

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

Goal state before:
pp: case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁₂.next (c₁₂.next i₁₂) = i₁₂''

Tactic:
c₁₂.next_eq' h₁,

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₃ : c₁.Rel i₁ (c₁.next i₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁₂.next i₁₂' = i₁₂''
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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
let c := (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj
    (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j

Goal state after:
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 F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
h₁₂ : (i₁₂ : ρ₁₂.I₁₂) → IsColimit (c₁₂ i₁₂)
c : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).CofanMapObjFun ρ₁₂.q j :=
  (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).cofanMapObj ρ₁₂.q j
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
Module: Mathlib.CategoryTheory.GradedObject.Associator

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_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
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₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      𝟙 (mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j) =
    ((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
        (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j

Tactic:
comp_id,

Goal state after:
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_5} C₃
inst✝⁶ : Category.{v_4, u_6} C₄
inst✝⁵ : Category.{v_5, u_3} C₁₂
inst✝⁴ : Category.{v_6, u_4} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝³ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝² : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
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₃
H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    ((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
        (mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).hom j