mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
⊢ e₁ * e₂ - e₁ * e₂ = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
⊢ 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 ↦ IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ f e' - f e' = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e' : R
he₂ : IsIdempotentElem e'
he : f e' ∈ f.range
he' : IsIdempotentElem (f e')
x : R
x✝ : (fun e'_1 ↦ IsIdempotentElem e'_1 ∧ f e'_1 = f e') x
hx : IsIdempotentElem x
hx' : f x = f e'
⊢ 0 = 0
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ 1 - 1 = 0

Tactic:
sub_self

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ 0 = 0
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
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ μ • v - μ • v = 0

Tactic:
sub_self

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ 0 = 0
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ (trace R ↥(f.maxGenEigenspace μ)) (restrict g hg' ∘ₗ restrict f hf') = 0

Tactic:
trace_comp_eq_mul_of_commute_of_isNilpotent μ h_comm this,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ μ * (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right
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₂)
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
Finset.mem_antidiagonal

Goal state after:
case h.right
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).1 + (i, j).2 = l₁ + l₂
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ antidiagonal n
hx1 : f.natDegree ≤ x.1
⊢ x.2 < f'.natDegree

Tactic:
by_contra!

Goal state after:
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f f' : R[X]
hf : ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
hf' : ∀ {n : ℕ}, n < f'.natDegree → f'.coeff n ∈ 𝓟
n : ℕ
hn : n < (f * f').natDegree
x : ℕ × ℕ
hx : x ∈ antidiagonal n
hx1 : f.natDegree ≤ x.1
this : f'.natDegree ≤ x.2
⊢ False
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
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (r : ↥S), (algebraMap (↥S) A) r ∈ T) ↔ ofClass S ≤ T

Tactic:
Subtype.forall,

Goal state after:
A : Type u_2
inst✝³ : CommRing A
C : Type u_5
inst✝² : SetLike C A
inst✝¹ : SubringClass C A
S : C
T : Subring A
inst✝ : IsIntegrallyClosedIn (↥T) A
⊢ (∀ (a : A) (b : a ∈ S), (algebraMap (↥S) A) ⟨a, b⟩ ∈ T) ↔ ofClass S ≤ T
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
h : MapsTo f A B
⊢ IsDecompOn (g ∘ f) A (T * S)

Tactic:
by
  rw [left_eq_inter.mpr h]
  exact hg.comp' hf

Goal state after:
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 y * star x)

Tactic:
y.mul_star_eq_coe,

Goal state after:
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 y).re * star x)
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

pp: case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

pp: case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2

Tactic:
add_eq_zero_iff_of_nonneg

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : ((a.re ^ 2 = 0 ∧ a.imI ^ 2 = 0) ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ a = 0

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : (a.re ^ 2 + a.imI ^ 2 = 0 ∧ a.imJ ^ 2 = 0) ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imI ^ 2

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 = 0 ∧ a.imK ^ 2 = 0
⊢ 0 ≤ a.imJ ^ 2

case ha
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2

case hb
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
h : a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2 = 0
⊢ 0 ≤ a.imK ^ 2
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 f.natDegree - f.coeff f.natDegree ∈ P

Tactic:
sub_self

Goal state after:
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
⊢ 0 ∈ P
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case e'_3
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : AddCommGroup G
h : M
f : M → G
n : ℕ
y : M
⊢ ∑ k ∈ range (n + 1), n.choose k • Δ_[h]^[k] f y =
    (∑ m ∈ range (n + 1), fwdDiffₗ M G h ^ m * 1 ^ (n - m) * ↑(n.choose m)) f y

Tactic:
simp [Module.End.pow_apply, coe_fwdDiffₗ]

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

Goal state before:
pp: M : Type u_3
R : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Ring R
φ : AddChar M R
x h : M
n : ℕ
⊢ Δ_[h]^[n] (⇑φ) x = (φ h - 1) ^ n * φ x

Tactic:
induction n generalizing x with
  | zero => simp
  | succ n IH =>
    simp only [pow_succ, iterate_succ_apply', fwdDiff, IH, ← mul_sub, mul_assoc]
    rw [sub_mul, ← AddChar.map_add_eq_mul, add_comm h x, one_mul]

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

Goal state before:
pp: case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ Δ_[1]^[n] (∑ i ∈ range j, j.choose i • fun r ↦ r ^ i) = 0

Tactic:
fwdDiff_iter_finsetSum

Goal state after:
case succ
R : Type u_3
inst✝ : CommRing R
n : ℕ
ih : ∀ {j : ℕ}, j < n → (Δ_[1]^[n] fun r ↦ r ^ j) = 0
j : ℕ
h : j < n + 1
this : (Δ_[1] fun r ↦ r ^ j) = ∑ i ∈ range j, j.choose i • fun r ↦ r ^ i
⊢ ∑ k ∈ range j, Δ_[1]^[n] (j.choose k • fun r ↦ r ^ k) = 0
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ : M
hx : x✝ ∈ s
⊢ ∃ y, x✝ * y ∈ s

Tactic:
exact ⟨1, by simpa⟩

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

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
hx : x ≠ 0
⊢ ((fst G₀ H₀).comp (inr G₀ H₀)) x = 1

Tactic:
fst_comp_inr,

Goal state after:
G₀ : Type u_1
H₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : GroupWithZero H₀
inst✝ : DecidablePred fun x ↦ x = 0
x : H₀
hx : x ≠ 0
⊢ 1 x = 1
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr
ι : 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
f : G →* S
i : ι
hi : f (v i) ≠ 1
hi' : v i⁻¹ = (v i)⁻¹
hj : 1 < f (v i)
⊢ v i ∈ Submonoid.closure (v '' {i | 1 < f (v i)}) ∨ (v i)⁻¹ ∈ Submonoid.closure (v '' {i | 1 < f (v i)})

Tactic:
left
    exact Submonoid.subset_closure ⟨i, by simpa⟩

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
this :
  ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S]
    [inst_2 : InvolutiveInv ι] [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (s : Set ι),
    (∀ i ∈ s, 1 < f (v i)) →
      ∀ (i : ι),
        v i ≠ 1 →
          v i⁻¹ = (v i)⁻¹ → v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s) → v i ∈ closure (v '' s) → f (v i) ≠ 1
hi : v i ∉ closure (v '' s)
hi' : (v i)⁻¹ ∈ closure (v '' s)
⊢ v i⁻¹ ∈ closure (v '' s) ∨ (v i⁻¹)⁻¹ ∈ closure (v '' s)

Tactic:
left; simpa [hv_inv]

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

Goal state before:
pp: case mp
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x) → (∃ y, f y = x) ∧ ¬x = 0

pp: case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ y, f y = x) ∧ ¬x = 0 → ∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x

Tactic:
· rintro ⟨y, hy, rfl⟩
    simp only [Units.ne_zero, not_false_eq_true, and_true, hy]

Goal state after:
case mpr
A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
x : B
⊢ (∃ y, f y = x) ∧ ¬x = 0 → ∃ x_1, (∃ y, f y = ↑x_1) ∧ ↑x_1 = x
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f → Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
intro _ a₁ a₂ h

Goal state after:
A B : NonemptyFinLinOrd
f : A ⟶ B
a✝ : Mono f
a₁ a₂ : ↑A.toLinOrd
h : (ConcreteCategory.hom f) a₁ = (ConcreteCategory.hom f) a₂
⊢ a₁ = a₂
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
by simp only [comp_id, id_comp]

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

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

Tactic:
by
  rw [δ_comp_δ]
  · rfl
  · exact H

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⦌), ⋯⟩).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

Tactic:
change f.left.app _ ≫ _ = _ ≫ ((ChainComplex.single₀ _).map f.right).f 0

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
⊢ f.left.app (op ⦋0⦌) ≫
      ((((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⦌), ⋯⟩).f
        0 ≫
      ((ChainComplex.single₀ C).map f.right).f 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ X.δ i.castSucc ≫ X.σ i = 𝟙 (X ^⦋n⦌)

Tactic:
dsimp [δ, σ]
  simp only [← X.map_comp, SimplexCategory.δ_comp_σ_self, X.map_id]

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

Goal state before:
pp: X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ X = Y

Tactic:
suffices Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1)) by
    ext
    simpa

Goal state after:
X Y : SimplexCategory
x✝ : IsIsomorphic X Y
I : X ≅ Y
⊢ Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ n < d

Tactic:
by_contra!

Goal state after:
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
d : ℕ
inst✝ : X.HasDimensionLT d
this : d ≤ n
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
m : SimplexCategory
f : ⦋n⦌ ⟶ m
y : X.obj (op m)
hy : (ConcreteCategory.hom (X.map f.op)) y = ↑x
⊢ Mono f

Tactic:
have := X.isIso_of_nonDegenerate x (factorThruImage f) (y := X.map (image.ι f).op y) (by
      rw [← comp_apply, ← Functor.map_comp, ← op_comp, image.fac f, hy])
  rw [← image.fac f]
  infer_instance

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf₁ : SplitEpi f₁
hf₁' : (SimplexCategory.Hom.toOrderHom hf₁.section_) ((SimplexCategory.Hom.toOrderHom f₁) x) = x
⊢ (SimplexCategory.Hom.toOrderHom f₁) x = (SimplexCategory.Hom.toOrderHom f₂) x

Tactic:
simpa [g, hf₁'] using (SimplexCategory.congr_toOrderHom_apply (g_eq_id hy₁ hy₂ hf₁)
      (f₁.toOrderHom x)).symm

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ face {i, j}ᶜ ≤ face {i}ᶜ

Tactic:
by simp [face_le_face_iff]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ face {i, j}ᶜ ≤ face {j}ᶜ

Tactic:
by simp [face_le_face_iff]

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₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.d₂ c₁₂ i₁ (c₂.next i₂) i₁₂'' = 0

pp: case neg
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₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.d₂ c₁₂ i₁ (c₂.next i₂) i₁₂'' = 0

Tactic:
· rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]

Goal state after:
case neg
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₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.d₂ c₁₂ i₁ (c₂.next i₂) i₁₂'' = 0
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
by_cases h₀ : c.Rel j j'

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom

case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₁ c j j' = K.flip.D₂ c j j' ≫ (K.totalFlipIsoX c j').hom
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

Tactic:
by_cases h₀ : c.Rel j j'

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom

case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : ¬c.Rel j j'
⊢ (K.totalFlipIsoX c j).hom ≫ K.D₂ c j j' = K.flip.D₁ c j j' ≫ (K.totalFlipIsoX c j').hom