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

Goal state before:
pp: case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv : ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = (algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ (algebraMap R (FractionRing R)) x * ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = X

Tactic:
eq_comm,

Goal state after:
case h
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : FractionRing R
x✝ : IsIntegral R X
p : R[X]
hp₁ : p.Monic
hp₂ : Polynomial.eval₂ (algebraMap R (FractionRing R)) X p = 0
a✝ : GCDMonoid R
x y : R
hg : IsUnit (gcd x y)
he : X * (algebraMap R (FractionRing R)) y = (algebraMap R (FractionRing R)) x
this✝ : y ∣ x ^ p.natDegree
this : IsUnit y
coe_map_inv : ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹ = (algebraMap R (FractionRing R)) ↑this.unit⁻¹
⊢ X = (algebraMap R (FractionRing R)) x * ↑((Units.map ↑(algebraMap R (FractionRing R))) this.unit)⁻¹
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
by rw [add_comm, self_add_star']

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
m : Monoid M
inst✝ : (i : ι) → MulAction M (α i)
x : (i : ι) × α i
⊢ 1 • x = x

Tactic:
cases x
    rw [smul_mk, one_smul]

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
by
  rw [QuaternionAlgebra.re_star, zero_mul, add_zero]

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

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

Tactic:
rw [hn, leadingCoeff, sub_self]
      exact zero_mem _

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

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

Tactic:
simp [npow_add]

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

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

Tactic:
simp [npow_add]

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

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

Tactic:
simp [npow_add]

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
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
mem_closure_range_iff

Goal state after:
M : Type u_1
inst✝¹ : CommGroup M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.Group.Submonoid.Finsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ x ∈ closure (Set.range f) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i

Tactic:
mem_closure_range_iff

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
ι : Type u_2
f : ι → M
x : M
inst✝ : Fintype ι
⊢ (∃ a, x = a.prod fun x1 x2 ↦ f x1 ^ x2) ↔ ∃ b, x = ∏ i, f i ^ Finsupp.equivFunOnFinite.symm.symm b i
Module: Mathlib.Algebra.GroupWithZero.TransferInstance

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := e.mulZeroOneClass
x✝ : Pow α ℕ := Equiv.pow ℕ e
⊢ MonoidWithZero α

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

Goal state after:
case zero
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 0 = 0

case one
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝¹ : MulZeroOneClass α := ⋯
x✝ : Pow α ℕ := ⋯
⊢ e 1 = 1

case mul
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

case npow
α : Type u
β : Type v
e : α ≃ β
inst✝ : MonoidWithZero β
x✝² : MulZeroOneClass α := e.mulZeroOneClass
x✝¹ : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : MonoidWithZero B
f : A →*₀ B
b : Bˣ
hb : ↑b ∈ range ⇑f
⊢ b ∈ f.valueMonoid

Tactic:
by
  tauto

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : x ^ n = x ^ n * ↑u ^ n
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
eq_comm,

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : x ^ n * ↑u ^ n = x ^ n
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ x = (Units.mk0 (f r) hr)⁻¹ * Units.mk0 (f s) hs

Tactic:
rw [eq_inv_mul_iff_mul_eq]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
x : Bˣ
hx : x ∈ f.valueGroup
r : A
hr : f r ≠ 0
s : A
hs : f s ≠ 0
hrs : f r * ↑x = f s
⊢ Units.mk0 (f r) hr * x = Units.mk0 (f s) hs
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case pos
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ { down := 1 } ≤ { down := 0 }

pp: case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }

Tactic:
· exfalso
          exact h₁ (lt_of_le_of_lt h h₂)

Goal state after:
case neg
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Epi f
m : ↑B.toLinOrd
hm : ∀ (a : ↑A.toLinOrd), (ConcreteCategory.hom f) a ≠ m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : ↑B.1
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : ¬x₂ < m
⊢ { down := 1 } ≤ { down := 1 }
Module: Mathlib.CategoryTheory.Idempotents.Basic

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

Tactic:
comp_id

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

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

Tactic:
comp_id

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
h : ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
X : C
p : X ⟶ X
hp : p ≫ p = p
this : HasEqualizer (𝟙 X) p
⊢ equalizer.ι (𝟙 X) p = equalizer.ι (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ 𝟙 X = 𝟙 X
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
P Q : Karoubi C
f g h' : P ⟶ Q
⊢ (f + g + h').f = (f + (g + h')).f

Tactic:
apply add_assoc

Goal state after:
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 φ = (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j)) ≫ F.map φ

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 φ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h.left
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)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun j ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
⊢ equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ 𝟙 (F.obj j) = equalizer.ι (𝟙 (F.obj j)) (p.app j)

Tactic:
comp_id

Goal state after:
case h.left
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)
Y : J ⥤ C :=
  { obj := fun j ↦ equalizer (𝟙 (F.obj j)) (p.app j),
    map := fun {j j'} φ ↦ equalizer.lift (equalizer.ι (𝟙 (F.obj j)) (p.app j) ≫ F.map φ) ⋯, map_id := ⋯, map_comp := ⋯ }
i : Y ⟶ F := { app := fun j ↦ equalizer.ι (𝟙 (F.obj j)) (p.app j), naturality := ⋯ }
e : F ⟶ Y := { app := fun j ↦ equalizer.lift (p.app j) ⋯, naturality := ⋯ }
j : J
⊢ equalizer.ι (𝟙 (F.obj j)) (p.app j) = equalizer.ι (𝟙 (F.obj j)) (p.app j)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ δ i ≫ δ j = δ i ≫ δ (j.pred ⋯).succ

pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯

Tactic:
· rw [Fin.succ_pred]

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ i ≤ j.pred ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))

Tactic:
apply Fintype.card_congr

Goal state after:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fin (X.len + 1) ≃ Fin (Y.len + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc < i.succ

Tactic:
exact Fin.castSucc_lt_succ

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

Goal state before:
pp: n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = θ' ≫ δ i

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp hθ

Goal state after:
n : ℕ
Δ : SimplexCategory
θ : Δ ⟶ ⦋n + 1⦌
hθ : ¬Function.Surjective ⇑(Hom.toOrderHom θ)
i : Fin (⦋n + 1⦌.len + 1)
hi : ¬∃ a, (Hom.toOrderHom θ) a = i
⊢ ∃ i θ', θ = θ' ≫ δ i
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 ((image.ι f).op ≫ (factorThruImage f).op))) y = x
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)

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
this : (image f).len ≤ m
⊢ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))
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))

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

Tactic:
· rintro ⟨m, hm, f, y, hy⟩
    rw [← image.fac f, op_comp] at hy
    have : _ ≤ m := SimplexCategory.len_le_of_mono (image.ι f)
    exact ⟨(image f).len, by lia, factorThruImage f, inferInstance, by aesop⟩

Goal state after:
case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))) → x ∈ X.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.ι ≫ f) ≤ A.image f

Tactic:
rw [image_eq_range]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this : 0 < n
⊢ ∀ (d : SimplexCategory), IsConnected (CostructuredArrow (inclusion n) d)

Tactic:
intro Δ

Goal state after:
n : ℕ
inst✝ : NeZero n
this : 0 < n
Δ : SimplexCategory
⊢ IsConnected (CostructuredArrow (inclusion n) Δ)
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 : SimplexCategoryᵒᵖ
⊢ ed.s' ≫ X.hom.app (op ⦋0⦌) ≫ 𝟙 X.right = 𝟙 X.right

Tactic:
comp_id

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : SimplexCategoryᵒᵖ
⊢ ed.s' ≫ X.hom.app (op ⦋0⦌) = 𝟙 X.right
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ (Subcomplex.ofSimplex x).toSSet.Finite

Tactic:
obtain ⟨f, rfl⟩ := yonedaEquiv.surjective x

Goal state after:
X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ (Subcomplex.ofSimplex (yonedaEquiv f)).toSSet.Finite
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩ ∈ (range (toOfSimplex x)).obj m ↔
    ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩ ∈ ⊤.obj m

Tactic:
simp only [range_eq_ofSimplex, yonedaEquiv_toOfSimplex, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ⟨(ConcreteCategory.hom (X.map u)) x, ⋯⟩ ∈ (ofSimplex ⟨x, ⋯⟩).obj m
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
⊢ ExtraDegeneracy.s f S 0 ≫ f.augmentedCechNerve.left.δ 1 =
    f.augmentedCechNerve.hom.app (op ⦋0⦌) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯

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

Goal state after:
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
⊢ ExtraDegeneracy.s f S 0 ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
        ⋯ =
    (WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯
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:
dsimp [SimplicialObject.δ, SimplexCategory.δ]

Goal state after:
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 ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) i.succ) ⋯ =
    𝟙 (widePullback f.right (fun x ↦ f.left) fun x ↦ f.hom)
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 : ℕ
i : Fin (n + 2)
⊢ ExtraDegeneracy.s f S (n + 1) ≫ f.augmentedCechNerve.left.δ i.succ =
    f.augmentedCechNerve.left.δ i ≫ ExtraDegeneracy.s f S n

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

Goal state after:
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 : ℕ
i : Fin (n + 2)
⊢ ExtraDegeneracy.s f S (n + 1) ≫
      WidePullback.lift (WidePullback.base fun x ↦ f.hom)
        (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯ =
    WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1)) ⋯ ≫
      ExtraDegeneracy.s f S n
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 L M : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
e : K ≅ L
ψ : L ⟶ M
c₁₂ : ComplexShape I₁₂
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : DecidableEq I₁₂
inst✝² : K.HasTotal c₁₂
inst✝¹ : L.HasTotal c₁₂
inst✝ : M.HasTotal c₁₂
⊢ map e.hom c₁₂ ≫ map e.inv c₁₂ = 𝟙 (K.total c₁₂)

Tactic:
rw [← map_comp, e.hom_inv_id, map_id]

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 : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' n' : ℤ
ha' : a' + b = n'
hn' : n' = n + x
⊢ K.ιTotal (up ℤ) a' b n' ha' ≫
      (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv ≫ (K.totalShift₁Iso x).inv.f n =
    (K.shiftFunctor₁XXIso a x a' ⋯ b).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h

Tactic:
by
  subst hn'
  obtain rfl : a = a' - x := by lia
  dsimp [totalShift₁Iso, totalShift₁XIso, shiftFunctor₁XXIso, XXIsoOfEq]
  simp only [id_comp, ι_totalDesc]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n

Tactic:
by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
⊢ ∃ n, ∀ (j : J), (p.diag.obj j).IsStrictlyGE n

Tactic:
by
      choose n hn using p.prop_diag_obj
      exact ⟨Finset.min' (Finset.image n ⊤ ∪ {0}) ⟨0, by grind⟩, fun j ↦
        (p.diag.obj j).isStrictlyGE_of_ge _ _ (Finset.min'_le _ (n j) (by simp))⟩

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

Goal state before:
pp: case e_a
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₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := c₁.π c₂ c₁₂ (i₁, i₂)
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
⊢ 0 = d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'

Tactic:
by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
          · rw [d₂_eq _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
            dsimp [ComplexShape.r]
            intro h₄
            apply h₂
            rw [← h₄, ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃]
          · rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ h₃]

Goal state after: