mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case succ.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
hb : (cons tb_hd tb_tl).tail ≠ nil
ih : motive (a.drop m) (cons tb_hd tb_tl)
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail

Tactic:
obtain ⟨a_hd, a_tl, ha, h_tail⟩ := step (a.drop m) (.cons tb_hd tb_tl) ih _ _ rfl

Goal state after:
case succ.cons
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb_hd : β
tb_tl : Seq β
hb : (cons tb_hd tb_tl).tail ≠ nil
ih : motive (a.drop m) (cons tb_hd tb_tl)
a_hd : α
a_tl : Seq α
ha : a.drop m = cons a_hd a_tl
h_tail : motive a_tl tb_tl
⊢ motive (a.drop m).tail (cons tb_hd tb_tl).tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.cons
α : Type u
β : Type v
f : α → β
S✝ : Seq (Seq1 α)
x : Seq1 α
S : Seq (Seq1 α)
⊢ BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (Seq.map f S.join) ∧ s2 = s.append (Seq.map (map f) S).join)
    (nil.append (Seq.map f (Seq.cons x S).join)).destruct (nil.append (Seq.map (map f) (Seq.cons x S)).join).destruct

Tactic:
obtain ⟨a, s⟩ := x
        simpa [map] using ⟨_, _, rfl, rfl⟩

Goal state after:
Module: Mathlib.Algebra.DirectSum.Idempotents

Goal state before:
pp: R : Type u_1
I : Type u_2
inst✝³ : Semiring R
inst✝² : DecidableEq I
V : I → Ideal R
inst✝¹ : Decomposition V
inst✝ : Fintype I
i j : I
hij : i ≠ j
⊢ (fun x1 x2 ↦ idempotent V x1 * idempotent V x2 = 0) i j

Tactic:
simp only
    rw [← decompose_eq_mul_idempotent, idempotent, decompose_coe,
      of_eq_of_ne (h := hij.symm), Submodule.coe_zero]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ P.toPoly.degree = 2

Tactic:
rw [of_a_eq_zero ha, degree_quadratic hb]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
⊢ (matrix n I).jacobson ≤ matrix n I.jacobson

Tactic:
intro M Mmem p q
  simp only [zero_apply, ← mem_iff]
  rw [mem_jacobson_iff]
  replace Mmem := mul_mem_right _ _ (single q p 1) Mmem
  rw [mem_jacobson_iff] at Mmem
  intro y
  specialize Mmem (y • single p p 1)
  have ⟨N, NxMI⟩ := Mmem
  use N p p
  simpa [mul_apply, single, ite_and] using! NxMI p p

Goal state after:
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
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
⊢ (trace R M) f = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
let b : (i : ι) → Basis _ R (N i) := fun i ↦ Module.Free.chooseBasis R (N i)
  simp_rw [trace_eq_matrix_trace R (h.collectedBasis b),
    toMatrix_directSum_collectedBasis_eq_blockDiagonal' h h b b hf, Matrix.trace_blockDiagonal',
    ← trace_eq_matrix_trace]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
⊢ IsNilpotent (LinearMap.restrict (f - μ • 1) h)

Tactic:
use k
  ext ⟨x, hx⟩
  rw [mem_genEigenspace_nat] at hx
  rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
    Module.End.pow_restrict, LinearMap.restrict_apply]
  ext
  simpa

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.some.some
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
I : Type u_3
inst✝ : Fintype I
f : R →+* S
e₀ : R
he₀ : IsIdempotentElem e₀
hfe₀ : RingHom.ker f = Ideal.span {e₀}
e : I → S
he : CompleteOrthogonalIdempotents e
e' : I → R
he' : ∀ (i : I), f (e' i) = e i
k : I → R
hk : ∀ (i : I), e' i * e' i - e' i = e₀ * k i
i j : I
h : some i ≠ some j
⊢ Option.rec e₀ ((1 - e₀) • e') (some i) * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

Tactic:
· obtain ⟨k, hk⟩ := Ideal.mem_span_singleton.mp
        (hfe₀.le (show f (e' i * e' j) = 0 by simp [he', he.1.2 (by simpa using h)]))
      dsimp
      rw [mul_mul_mul_comm, hk, he₀.one_sub.eq, ← mul_assoc, he₀.one_sub_mul_self, zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (h * (f * g)) = (trace R M) (h * f * g)

Tactic:
← mul_assoc

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (h * f * g) = (trace R M) (h * f * g)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this✝ : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal (l₁ + l₂)
this : ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
⊢ ((l₁ + l₂).choose (i, j).1 • ((f₁ - μ₁ • 1) ^ (i, j).1 * (f₂ - μ₂ • 1) ^ (i, j).2)) m = 0

Tactic:
by
    rw [LinearMap.smul_apply, this, smul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : IsDomain R
inst✝³ : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
⊢ μ (x + y) = μ x + μ y

Tactic:
by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))
  simp only [g, map_add]
  exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

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

Goal state before:
pp: K : Type u_1
inst✝ : Semifield K
a b c p : K
hc : c ≠ 0
⊢ c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]

Tactic:
simp [mul_comm c, hc]

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

Goal state before:
pp: 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 := 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
hm : m = 0
⊢ IsUnit g

Tactic:
isPrimitive_iff_isUnit_of_C_dvd

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 : ∀ (r : R), C r ∣ f → IsUnit r
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
hm : m = 0
⊢ IsUnit g
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ IsIntegrallyClosedIn (↥S) A ↔ ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S

Tactic:
isIntegrallyClosedIn_iff,

Goal state after:
A : Type u_2
inst✝² : CommRing A
C : Type u_5
inst✝¹ : SetLike C A
inst✝ : SubringClass C A
S : C
⊢ (Function.Injective ⇑(algebraMap (↥S) A) ∧ ∀ {x : A}, IsIntegral (↥S) x → ∃ y, (algebraMap (↥S) A) y = x) ↔
    ∀ ⦃x : A⦄, IsIntegral (↥S) x → x ∈ S
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✝² : CommRing R
inst✝¹ : CommSemiring S
inst✝ : Algebra S R
⊢ ↑((algebraMap S R) 0) = 0

Tactic:
by simp only [map_zero, coe_zero]

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

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : α
⊢ (a • b) • inl val✝ = a • b • inl val✝

pp: case inr
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a✝ : M
b✝ : α
c : β
x : α ⊕ β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
a : M
b : N
val✝ : β
⊢ (a • b) • inr val✝ = a • b • inr val✝

Tactic:
exacts [congr_arg inl (smul_assoc _ _ _), congr_arg inr (smul_assoc _ _ _)]

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

Goal state before:
pp: 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
⊢ ker (algebraMap R (FractionRing (R ⧸ P))) = P

Tactic:
IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P))

Goal state after:
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
⊢ ker ((algebraMap (R ⧸ P) (FractionRing (R ⧸ P))).comp (algebraMap R (R ⧸ P))) = P
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a b : ℍ[R]
x✝ : ℚ
⊢ ↑x✝ = ↑x✝.num / ↑x✝.den

Tactic:
rw [← coe_ratCast, Rat.cast_def, coe_div, coe_intCast, coe_natCast]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #↑Set.univ = #R

Tactic:
mk_univ_quaternionAlgebra,

Goal state after:
R : Type u_1
c₁ c₂ c₃ : R
inst✝ : Infinite R
⊢ #R ^ 4 = #R
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ s⁻¹.ncard = s.ncard

Tactic:
by simp [ncard]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ (a • s).ncard = s.ncard

Tactic:
by simp [ncard]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Goal state before:
pp: R : Type u_4
inst✝ : Ring R
r : R
k : ℤ
⊢ ↑k * r ∈ zmultiples r

Tactic:
by
  simpa only [← zsmul_eq_mul] using zsmul_mem_zmultiples r k

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * (x₂ * y) ∈ s

Tactic:
← mul_assoc

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x₁ x₂ : M
hxy✝ : x₁ * x₂ ∈ s.saturation
ih : ∃ y, x₁ * x₂ * y ∈ s
y : M
h : x₁ * x₂ * y ∈ s
⊢ x₁ * x₂ * y ∈ s
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ (if h : f 1 = 0 then 0 else ↑⟨Units.mk0 (f 1) h, ⋯⟩) = 1

Tactic:
by simp [← WithZero.coe_one]

Goal state after:
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, hx⟩ = valueGroup.mk f r s hr hs

Tactic:
simp only [valueGroup.mk, Subtype.mk.injEq]
      rw [eq_inv_mul_iff_mul_eq]
      simp [← hrs, mul_comm]

Goal state after:
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 : P ⟶ Q
⊢ f + 0 = f

Tactic:
by
    ext
    apply add_zero

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ X.δ i ≫ X.σ j = X.σ (j.castLT ⋯) ≫ X.δ (i.pred ⋯)

Tactic:
dsimp [δ, σ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_σ_of_gt' H]

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

Goal state before:
pp: case neg
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
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) (i.succ.succAbove y)

Tactic:
rw [Fin.succAbove_of_le_castSucc i.succ _]

Goal state after:
case neg
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.succ ≤ y.castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

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

Tactic:
rw [σ₀Iter_coe_eq_of_lt .., coe_σ]
    obtain hk | rfl := hk.lt_or_eq
    · grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_lt]
    · grind [Fin.predAbove_of_le_castSucc, Fin.coe_castPred, σ₀Iter_coe_eq_of_ge, tsub_self]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
⊢ Function.RightInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)

Tactic:
by
    intro A
    ext
    · rfl
    · dsimp
      rw [WidePushout.ι_desc]
      nth_rw 2 [← Category.comp_id A.right]
      congr 1
      convert! X.right.map_id _
      ext ⟨a, ha⟩
      simp

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ T ≤ ((fun S ↦ S.image f) T).preimage f

Tactic:
by rw [← image_le_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x ↦ (Arrow.mk (terminal.from X)).left) fun x ↦
    (Arrow.mk (terminal.from X)).hom

Tactic:
cases nonempty_fintype ι
  exact ⟨⟨wideCospan.limitCone ι X⟩⟩

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

Goal state before:
pp: X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ∃ x₀ x₁ x₂ e₀₁ e₁₂ e₀₂ h, h.simplex = s

Tactic:
refine ⟨X.map (Hom.tr (SimplexCategory.const _ _ 0)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 1)).op s,
    X.map (Hom.tr (SimplexCategory.const _ _ 2)).op s,
    .mk _ ?_ ?_, .mk _ ?_ ?_, .mk _ ?_ ?_, .mk s rfl rfl rfl, rfl⟩

Goal state after:
case refine_1
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

case refine_2
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 2 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

case refine_3
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

case refine_4
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

case refine_5
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

case refine_6
X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 Edge._proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (δ₂ 1 Edge._proof_2 _proof_2).op)) s) =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ j.succAbove ((i.castPred ⋯).succAbove k) ∈ {i, j}ᶜ

Tactic:
grind [compl_insert, mem_compl, Fin.succAbove, Fin.castPred]

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
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 F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
⊢ (mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
      { app := fun X₃ x ↦ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } =
    { app := fun X₃ x ↦ ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } ≫
      (mapTrifunctorObj F Y₁ I₂ I₃).map ψ

Tactic:
ext X₃ x

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 F' : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
x : I₁ × I₂ × I₃
⊢ ((mapTrifunctorObj F X₁ I₂ I₃).map ψ ≫
          { app := fun X₃ x ↦ ((F.map (φ x.1)).app (Y₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ }).app
      X₃ x =
    ({ app := fun X₃ x ↦ ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2), naturality := ⋯ } ≫
          (mapTrifunctorObj F Y₁ I₂ I₃).map ψ).app
      X₃ x
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : Augmented C
ed : X.ExtraDegeneracy
i : ℕ
⊢ (AlternatingFaceMapComplex.ε.app X ≫
          ((AlternatingFaceMapComplex.obj (drop.obj X)).fromSingle₀Equiv (point.obj X)).symm ed.s').f
      i =
    (((dNext i) fun i ↦ Pi.single (i + 1) (-ed.s i)) + (prevD i) fun i ↦ Pi.single (i + 1) (-ed.s i)) +
      (𝟙 (AlternatingFaceMapComplex.obj (drop.obj X))).f i

Tactic:
by
        cases i with
        | zero =>
          rw [Homotopy.prevD_chainComplex, Homotopy.dNext_zero_chainComplex]
          simp [dsimp% ChainComplex.fromSingle₀Equiv_symm_apply_f_zero
            (C := AlternatingFaceMapComplex.obj X.left), s_comp_δ₀, s₀_comp_δ₁]
        | succ i =>
          rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]
          simp [Fin.sum_univ_succ (n := i + 2), s_comp_δ₀, Preadditive.sum_comp,
            Preadditive.comp_sum,
            s_comp_δ, pow_succ]

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₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
⊢ ∀ (i : I₁ × I₂) (hij : c₁.π c₂ c₁₂ i = i₁₂),
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ f = K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) i i₁₂ hij ≫ g

Tactic:
rintro ⟨i₁, i₂⟩ hi

Goal state after:
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₁₂
A : C
i₁₂ : I₁₂
f g : (K.total c₁₂).X i₁₂ ⟶ A
h :
  ∀ (i₁ : I₁) (i₂ : I₂) (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂), K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g
i₁ : I₁
i₂ : I₂
hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ f =
    K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂) i₁₂ hi ≫ g
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₁₂
⊢ (HomologicalComplex.forget C c₁₂).map (map (𝟙 K) c₁₂) = (HomologicalComplex.forget C c₁₂).map (𝟙 (K.total c₁₂))

Tactic:
apply GradedObject.mapMap_id

Goal state after: