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

Goal state before:
pp: case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : (of v).dens n = 0
⊢ 1 / ((of v).dens n * (of v).dens (n + 1)) ≤ 1 / (b * (of v).dens n * (of v).dens n)

Tactic:
simp only [hB, mul_zero, zero_mul, div_zero, le_refl]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ (x - x ^ 2) ^ n ∣
    (x - x ^ 2) ^ n *
      ((∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) * (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1)) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

pp: case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

pp: case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))

Tactic:
· exact ⟨_, rfl⟩

Goal state after:
case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute x (1 - x)

case hbc
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (∑ x_1 ∈ Finset.range n, (1 - x ^ n) ^ (n - 1 - x_1)) ((1 - x) ^ n)

case h
R : Type u_1
inst✝ : Ring R
x : R
n : ℕ
hx : (x - x ^ 2) ^ n = 0
⊢ Commute (1 - x) (∑ x_1 ∈ Finset.range n, x ^ (n - 1 - x_1))
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
I : Type u_3
inst✝ : Finite I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : OrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
val✝ : Fintype I
e' : Fin (Fintype.card I) → R
h₁ : OrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm.toEmbedding
⊢ ⇑f ∘ e' ∘ ⇑(Fintype.equivFin I).toEmbedding = e

Tactic:
by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)

Goal state after:
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
I : Type u_3
inst✝ : Fintype I
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e : I → S
he : CompleteOrthogonalIdempotents e
he' : ∀ (i : I), e i ∈ f.range
e' : Fin (Fintype.card I) → R
h₁ : CompleteOrthogonalIdempotents e'
h₂ : ⇑f ∘ e' = e ∘ ⇑(Fintype.equivFin I).symm
⊢ ⇑f ∘ e' ∘ ⇑(Fintype.equivFin I) = e

Tactic:
by ext x; simpa using congr_fun h₂ (Fintype.equivFin I x)

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Finite I
e : I → R
he : OrthogonalIdempotents e
this : Pairwise fun i j ↦ IsCoprime (Ideal.span {1 - e i}) (Ideal.span {1 - e j})
x : R
i : I
⊢ (RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i})) x i =
    (Ideal.quotientInfToPiQuotient fun i ↦ Ideal.span {1 - e i}) ((Ideal.Quotient.mk (⨅ i, Ideal.span {1 - e i})) x) i

Tactic:
simp [Ideal.quotientInfToPiQuotient]

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 : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ M ∈ (matrix n I).jacobson

Tactic:
matrix_eq_sum_single M

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M : Matrix n n R
MI : M ∈ matrix n I.jacobson
⊢ ∑ i, ∑ j, single i j (M i j) ∈ (matrix n I).jacobson
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : (matrix n c).ofMatrix x y
⊢ c x y

Tactic:
inhabit n

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
c : RingCon R
x y : R
h : (matrix n c).ofMatrix x y
inhabited_h : Inhabited n
⊢ c x y
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : c x y
i' : n
⊢ ∀ (j : n), c.ofMatrix (x i' j) (y i' j)

Tactic:
j'

Goal state after:
case mpr
R : Type u_1
n : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
c : RingCon (Matrix n n R)
x y : Matrix n n R
h : c x y
i' j' : n
⊢ c.ofMatrix (x i' j') (y i' j')
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
x : R
le : (of fun x_1 x_2 ↦ x) ∈ matrix n J
xI : x ∈ I
⊢ x ∈ J

Tactic:
simpa using le

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_1.none.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
j : I
h : none ≠ some j
⊢ Option.rec e₀ ((1 - e₀) • e') none * Option.rec e₀ ((1 - e₀) • e') (some j) = 0

Tactic:
dsimp; linear_combination - he₀.eq * e' j

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
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯)

Tactic:
apply isNilpotent_restrict_genEigenspace_nat

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
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := ⋯
hp : Nontrivial ↥p
f₁ : End R ↥p := ⋯
f₂ : End R ↥p := ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯)

Tactic:
apply isNilpotent_restrict_genEigenspace_nat

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
f : End R M
k : ℕ∞
⊢ InjOn (fun x ↦ (f.genEigenspace x) k) {μ | (f.genEigenspace μ) k ≠ ⊥}

Tactic:
rintro μ₁ _ μ₂ hμ₂ hμ₁₂
  by_contra contra
  apply hμ₂
  simpa only [hμ₁₂, disjoint_self] using f.disjoint_genEigenspace contra k k

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (⁅f, g⁆ * h) = (trace R M) (f * ⁅g, h⁆)

Tactic:
simp only [Ring.lie_def, sub_mul, mul_sub, map_sub, mul_assoc]

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g h : M →ₗ[R] M
⊢ (trace R M) (f * (g * h)) - (trace R M) (g * (f * h)) = (trace R M) (f * (g * h)) - (trace R M) (f * (h * g))
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ (f.genEigenspace μ) ↑(finrank K V + finrank K V) = (f.genEigenspace μ) ↑(finrank K V)

Tactic:
rw [genEigenspace_eq_genEigenspace_finrank_of_le]

Goal state after:
case hk
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
μ : K
⊢ finrank K V ≤ finrank K V + finrank K V
Module: Mathlib.Algebra.Field.GeomSum

Goal state before:
pp: K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)

Tactic:
← h.geom_sum₂_Ico_mul hmn,

Goal state after:
K : Type u_2
inst✝ : DivisionRing K
x y : K
h : Commute x y
hxy : x ≠ y
m n : ℕ
hmn : m ≤ n
this : x - y ≠ 0
⊢ ∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i) = (∑ i ∈ Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) / (x - y)
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: ι : Type u_1
f : ι → ℕ
s : Finset ι
hf : ∀ k ∈ s, f k ≠ 0
p : ℕ
⊢ (s.lcm f).factorization p = s.sup fun a ↦ (f a).factorization p

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]

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

Goal state before:
pp: 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 (algebraMap R K) g ∣ map (algebraMap R K) q ^ p

Tactic:
← IsUnit.dvd_mul_left _,

Goal state after:
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 (algebraMap R K) g ∣ ?m.213 * map (algebraMap R K) q ^ p

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 := ⋯
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
⊢ K[X]

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
⊢ IsUnit ?m.213
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ x ∈ Set.range ⇑(algebraMap R A)

Tactic:
Set.mem_range

Goal state after:
case mpr
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hRA : Function.Injective ⇑(algebraMap R A)
h : IsIntegrallyClosedIn R A
x : A
hx : x ∈ integralClosure R A
⊢ ∃ y, (algebraMap R A) y = x
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ x ∣ y ^ p.natDegree

Tactic:
← natDegree_scaleRoots p x,

Goal state after:
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ⇑f
p : R[X]
hp : p.Monic
x y : R
z : A
h : eval₂ f z p = 0
hz : f x * z = f y
⊢ x ∣ y ^ (p.scaleRoots x).natDegree
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) a * y

Tactic:
mul_div_cancel₀ _ ha

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsIntegrallyClosed R
n : ℕ
hn : n ≠ 0
a b : R
x✝ : a ^ n ∣ b ^ n
x : R
hx : b ^ n = a ^ n * x
K : Type u_1 := FractionRing R
ha : (algebraMap R K) a ≠ 0
y : K := (algebraMap R K) b / (algebraMap R K) a
hy : IsIntegral R y
k : R
hk : (algebraMap R K) k = y
⊢ (algebraMap R K) b = (algebraMap R K) b
Module: Mathlib.Algebra.Quaternion

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

Tactic:
rw [← star_comm_self']
  exact a.star_mul_eq_coe

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : PartialOrder α
inst✝³ : DecidableEq α
inst✝² : MulLeftStrictMono α
inst✝¹ : MulRightStrictMono α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ ↑(Iio a * Iic b) ⊆ ↑(Iio (a * b))

Tactic:
simpa using Set.Iio_mul_Iic_subset' _ _

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

Goal state before:
pp: case a
a b : ℤ
⊢ closure {a, b} ≤ zmultiples ↑(a.gcd b)

Tactic:
grind [closure_le, mem_zmultiples_iff, SetLike.mem_coe, gcd_dvd_left, gcd_dvd_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : a✝ ∈ ⋂ s ∈ f, ↑s
hy : b✝ ∈ ⋂ s ∈ f, ↑s
⊢ a✝ * b✝ ∈ ⋂ s ∈ f, ↑s

Tactic:
Set.mem_iInter₂

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
f : Set (SaturatedSubmonoid M)
a✝ b✝ : M
hx : ∀ i ∈ f, a✝ ∈ ↑i
hy : ∀ i ∈ f, b✝ ∈ ↑i
⊢ ∀ i ∈ f, a✝ * b✝ ∈ ↑i
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : GroupWithZero A
inst✝ : GroupWithZero B
f : A →*₀ B
⊢ range ⇑(restrict₀ f) = ⊤

Tactic:
rw [top_eq_univ, range_eq_univ]
  intro x
  match x with
  | 0 => use 0; simp
  | some ⟨u, hu⟩ =>
    change u ∈ (valueGroup f : Set Bˣ) at hu
    rw [← valueMonoid_eq_valueGroup'] at hu
    obtain ⟨v, hv⟩ := hu
    use v
    simp [restrict₀_apply, hv, Units.ne_zero, WithZero.coe]

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:
by
      simp only [valueGroup.mk, Subtype.mk.injEq]
      rw [eq_inv_mul_iff_mul_eq]
      simp [← hrs, mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.FintypeCat

Goal state before:
pp: X Y : Skeleton
x✝ : IsIsomorphic X Y
h : X ≅ Y
⊢ Function.RightInverse (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.inv ≫ h.hom) _).down = _
            simp
            rfl

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

Goal state before:
pp: n j l : ℕ
hjl : j + l ≤ n
⊢ diag l ≫ subinterval j l hjl = intervalEdge j l hjl

Tactic:
unfold subinterval intervalEdge diag mkOfLe

Goal state after:
n j l : ℕ
hjl : j + l ≤ n
⊢ mkHom
        {
          toFun := fun x ↦
            match x with
            | 0 => 0
            | 1 => Fin.last l,
          monotone' := ⋯ } ≫
      mkHom { toFun := fun i ↦ ⟨↑i + j, ⋯⟩, monotone' := ⋯ } =
    mkHom
      {
        toFun := fun x ↦
          match x with
          | 0 => ⟨j, ⋯⟩
          | 1 => ⟨j + l, ⋯⟩,
        monotone' := ⋯ }
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
j : J
⊢ ∀ (Y : J) (f : j ⟶ Y),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
      eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯

Tactic:
j'

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
j j' : J
⊢ ∀ (f : j ⟶ j'),
    ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
      eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case zero
n : ℕ
i i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i' = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i' = δ i ≫ δ₀Iter 0 ⋯

Tactic:
obtain rfl : i = i' := by lia

Goal state after:
case zero
n : ℕ
i : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i = ↑i + 0
⊢ δ₀Iter 0 h ≫ δ i = δ i ≫ δ₀Iter 0 ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j : Fin ((rev.obj { len := n + 1 }).len + 1)
⊢ (Hom.toOrderHom (rev.map (σ i))) j = (Hom.toOrderHom (σ i.rev)) j

Tactic:
simp [σ, Fin.predAbove_rev_right, Fin.rev_rev, rev_map_apply]

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

Goal state before:
pp: case zero
n : ℕ
i : Fin (n + 2)
hi' : 0 < ↑i
i' : Fin (n + 2)
h : n + 0 = n
hi'' : ↑i = ↑i' + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i'

Tactic:
obtain rfl : i = i' := by lia

Goal state after:
case zero
n : ℕ
i : Fin (n + 2)
hi' : 0 < ↑i
h : n + 0 = n
hi'' : ↑i = ↑i + 0
⊢ δ i ≫ σ₀Iter 0 ⋯ = σ₀Iter 0 ⋯ ≫ δ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter (i + 1) ⋯

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  ext
  rw [dsimp% ConcreteCategory.comp_apply (σ j) (σ₀Iter i), coe_σ]
  by_cases! hk : i < k.val
  · rw [σ₀Iter_coe_eq_of_ge (i + 1) ..,
      Fin.predAbove_of_castSucc_lt _ _ (by grind),
      σ₀Iter_coe_eq_of_ge ..]
    grind
  · rw [σ₀Iter_coe_eq_of_lt (i + 1) ..]
    rw [σ₀Iter_coe_eq_of_le _ _ _ ?_]
    by_cases! hk' : k ≤ j.castSucc
    · rwa [Fin.predAbove_of_le_castSucc _ _ (by lia)]
    · grind [Fin.predAbove]

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (uliftYonedaEquiv.symm x)).obj U

Tactic:
dsimp [uliftYonedaEquiv]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ Set.range fun y ↦ (ConcreteCategory.hom (F.map y.down.op)) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Simplices

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } ≤ { dim := n, simplex := x }

Tactic:
by
  rw [le_iff]
  tauto

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

Goal state before:
pp: X : SSet
⊢ Functor.Elements X → X.S

Tactic:
rintro ⟨⟨⟨n⟩⟩, x⟩

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ X.S
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

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

Tactic:
comp_apply,

Goal state after:
X : SSet
n : ℕ
x : X _⦋n⦌
m₁ m₂ : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m₁⦌
hf₁ : SplitEpi f₁
y₁ : ↑(X.nonDegenerate m₁)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m₂⦌
y₂ : X _⦋m₂⦌
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) y₂
⊢ (ConcreteCategory.hom (X.map hf₁.section_.op)) ((ConcreteCategory.hom (X.map f₂.op)) y₂) = ↑y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
A B : X.Subcomplex
h : ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op ⦋n⦌) → ↑x ∈ B.obj (Opposite.op ⦋n⦌)
s : X.N
⊢ s.subcomplex ≤ A → s.subcomplex ≤ B

pp: case refine_2
X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (Opposite.op ⦋n⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)

Tactic:
· induction s using N.induction with
    | mk n x =>
      intro hx
      simp only [Subfunctor.ofSection_le_iff, mk_simplex] at hx ⊢
      exact h _ _ hx

Goal state after:
case refine_2
X : SSet
A B : X.Subcomplex
h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
n : ℕ
x : ↑(X.nonDegenerate n)
hx : ↑x ∈ A.obj (Opposite.op ⦋n⦌)
⊢ ↑x ∈ B.obj (Opposite.op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
constructor
  · intro h
    ext x
    simp only [Set.inf_eq_inter, Set.mem_inter_iff, and_iff_right_iff_imp]
    intro hx
    simp [← A.mem_degenerate_iff ⟨x, hx⟩, h, Set.top_eq_univ, Set.mem_univ]
  · intro h
    simp only [Set.inf_eq_inter, Set.inter_eq_right] at h
    ext x
    simpa [A.mem_degenerate_iff] using h x.prop

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ StrictMono s.obj

Tactic:
obtain _ | n := n
  · simpa using Subsingleton.strictMono _
  · rw [← not_iff_not, ← SSet.mem_degenerate_iff_notMem_nonDegenerate,
      Fin.strictMono_iff_lt_succ, SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
    simp only [mem_range_nerve_σ_iff, not_forall]
    apply exists_congr
    intro i
    have := s.monotone i.castSucc_le_succ
    grind [lt_self_iff_false, LE.le.lt_or_eq]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : Even i
hj : ¬Even j
⊢ φ ≫ ψ = 0

pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : Even j
⊢ ψ ≫ φ = 0

pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ ψ ≫ ψ = 0

Tactic:
· assumption

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : Even j
⊢ ψ ≫ φ = 0

case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
this : Odd (i + j)
hi : ¬Even i
hj : ¬Even j
⊢ ψ ≫ ψ = 0