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

Goal state before:
pp: case refine_2
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ f (1 - e₂) * f e' = f e'

Tactic:
map_sub,

Goal state after:
case refine_2
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (f 1 - f e₂) * f e' = f e'
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * 0 = 0

Tactic:
mul_zero

Goal state after:
case refine_3
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ 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 (x - e') = 0

Tactic:
map_sub,

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'
⊢ f x - f e' = 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)) μ) ⋯)
⊢ μ * 0 = 0

Tactic:
mul_zero

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)) μ) ⋯)
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) f).trace = ((toMatrix b b) (f ∘ₗ id)).trace

Tactic:
LinearMap.comp_id

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) f).trace = ((toMatrix b b) f).trace
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
x y : A
⊢ (↑fe).1 x * (↑fe).1 y * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }
x y : A
⊢ 0 = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 1 * (↑fg).1 a = (↑fg).2 (a • 1)

Tactic:
← fg.prop.2.2,

Goal state after:
R : Type u_1
A✝ : Type u_2
B : Type u_3
A : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
fg :
  { fg //
    (∀ (x y : A), fg.2 x * fg.2 y = 0) ∧
      (∀ (r x : A), fg.2 (r • x) = fg.1 r * fg.2 x) ∧ ∀ (r x : A), fg.2 (MulOpposite.op r • x) = fg.2 x * fg.1 r }
a : A
⊢ (↑fg).2 (MulOpposite.op a • 1) = (↑fg).2 (a • 1)
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) (f ∘ₗ id)).trace = ((toMatrix c c) f).trace

Tactic:
LinearMap.comp_id

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f).trace = ((toMatrix c c) f).trace
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 : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ ∀ (s : Finset R), s.SupIndep fun x ↦ (f.genEigenspace x) k

Tactic:
Finset.supIndep_iff_disjoint_erase

Goal state after:
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 : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
⊢ ∀ (s : Finset R), ∀ i ∈ s, Disjoint ((f.genEigenspace i) k) ((s.erase i).sup fun x ↦ (f.genEigenspace x) k)
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 : End R M
⊢ (trace R M) (f * g - g * f) = 0

Tactic:
map_sub,

Goal state after:
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
⊢ (trace R M) (f * g) - (trace R M) (g * f) = 0
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
b✝ c✝ : List (α × Bool)
a✝ : Relation.ReflTransGen Red.Step (reduce L₁) b✝
H1 : Red.Step b✝ c✝
H2 : reduce L₁ = b✝
⊢ reduce L₁ = c✝

Tactic:
obtain ⟨L4, L5, x, b⟩ := H1

Goal state after:
case tail
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
a✝ : Relation.ReflTransGen Red.Step (reduce L₁) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)
H2 : reduce L₁ = L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
⊢ reduce L₁ = L₁✝ ++ L₂✝
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : FreeGroup α
⊢ x.norm = 0 ↔ x = 1

Tactic:
by
  simp only [norm, List.length_eq_zero_iff, toWord_eq_nil_iff]

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

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

Tactic:
| insert _ _ _ _ =>

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
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)

Tactic:
set P := ker (algebraMap R K)

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)
⊢ ∃ m r, g = C g.leadingCoeff * q ^ m + r ∧ map (algebraMap R K) r = 0 ∧ (m = 0 → IsUnit g)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

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

Tactic:
exact mul_mem_right (x ^ k) 𝓟 this

Goal state after:
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
⊢ (algebraMap R (FractionRing R)) (x * ↑this.unit⁻¹) = X

Tactic:
map_mul

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
⊢ (algebraMap R (FractionRing R)) x * (algebraMap R (FractionRing R)) ↑this.unit⁻¹ = X
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this✝¹ : Algebra S K := g.toAlgebra
this✝ : IsScalarTower R S K
this : IsFractionRing S K
x : K
hx : IsIntegral S x
y : R
y_mem : y ∈ M
hy : IsIntegral R (⟨y, y_mem⟩ • x)
z : R
hz : (algebraMap R K) z = ⟨y, y_mem⟩ • x
⊢ ((algebraMap R K).comp (RingHom.id R)) z = ((algebraMap R K).comp (RingHom.id R)) ↑⟨y, y_mem⟩ * x

Tactic:
rw [RingHom.comp_id, hz, ← Algebra.smul_def, Submonoid.mk_smul]

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 (x * y)).re = ↑((x * star x).re * (y * star y).re)

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

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
simp only [normSq_def, star_neg, neg_mul_neg]

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

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ ↑((n + 1).choose i) * 0 = 0

Tactic:
mul_zero

Goal state after:
R : Type u_3
inst✝ : CommRing R
n : ℕ
IH : (Δ_[1]^[n] fun r ↦ r ^ n) = ↑n !
this : (Δ_[1] fun r ↦ r ^ (n + 1)) = ∑ i ∈ range (n + 1), (n + 1).choose i • fun r ↦ r ^ i
i : ℕ
hi : i ∈ range n
⊢ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i.castSucc).op ≫ X.map (SimplexCategory.δ i).op =
    X.map (SimplexCategory.δ i.succ).op ≫ X.map (SimplexCategory.δ i).op

Tactic:
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ_self]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝¹ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F
⊢ IsLeftKanExtension ((sk n).obj X) ((skAdj n).unit.app ((truncation n).obj X))

Tactic:
by
  dsimp [sk, skAdj]
  rw [lanAdjunction_unit]
  infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) x)) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Tactic:
fin_cases x <;> rw [Fin.succAbove_of_le_castSucc]

Goal state after:
case «0»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨0, ⋯⟩))

case «0».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨0, ⋯⟩)).castSucc

case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ ↑((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).succ =
    ↑((Hom.toOrderHom (mkOfSucc i.succ)) ((fun i ↦ i) ⟨1, ⋯⟩))

case «1».h
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ j ≤ ((Hom.toOrderHom (mkOfSucc i)) ((fun i ↦ i) ⟨1, ⋯⟩)).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : (SimplicialObject.Augmented C)ᵒᵖ
f : X✝ ⟶ Y✝
x : SimplexCategory
⊢ (unop Y✝).hom.app (op x) ≫ f.unop.right = f.unop.left.app (op x) ≫ (unop X✝).hom.app (op x)

Tactic:
exact (congr_app f.unop.w (op x)).symm

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter i hi ≫ δ j)) k) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)

Tactic:
rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter i hi) (δ j), coe_δ,
    δ₀Iter_apply .., δ₀Iter_apply ..,
    Fin.succAbove_of_le_castSucc _ _ (by grind)]

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + i, ⋯⟩.succ = ↑⟨↑k + (i + 1), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
⊢ X.σ j ≫ X.δ₀Iter (i + 1) hi = X.δ₀Iter i ⋯

Tactic:
dsimp [σ, δ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.δ₀Iter_σ ..]

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂
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
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x = A.right.app x

Tactic:
refine WidePushout.hom_ext _ _ _ (fun j => ?_) ?_

Goal state after:
case h₂.refine_1
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
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

case h₂.refine_2
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
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x ↦ F.hom) ≫ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right.app x =
    (WidePushout.head fun x ↦ F.hom) ≫ A.right.app x
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
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun x ↦ X) j =
    limit.lift (Discrete.functor fun x ↦ X) (Fan.mk s.pt fun j ↦ s.π.app (some j)) ≫ Pi.π (fun x ↦ X) j

Tactic:
rw [limit.lift_π]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ᶜ fun x ↦ X,
        π :=
          {
            app := fun X_1 ↦
              Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none))
                fun i ↦ limit.π (Discrete.functor fun x ↦ X) { as := i },
            naturality := ⋯ } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        { pt := ∏ᶜ fun x ↦ X,
                π :=
                  {
                    app := fun X_1 ↦
                      Option.casesOn X_1
                        (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                        limit.π (Discrete.functor fun x ↦ X) { as := i },
                    naturality := ⋯ } }.π.app
          j =
      s.π.app j
j : ι
⊢ f ≫ Pi.π (fun x ↦ X) j = (Fan.mk s.pt fun j ↦ s.π.app (some j)).π.app { as := j }
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices

Goal state before:
pp: case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map (f ≫ section_ f ≫ f).op)) ↑y = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
IsSplitEpi.id,

Goal state after:
case refine_1
X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this✝ : IsSplitEpi f
this : Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))
⊢ (ConcreteCategory.hom (X.map (f ≫ 𝟙 ⦋m⦌).op)) ↑y = (ConcreteCategory.hom (X.map f.op)) ↑y
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: 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 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
apply congr_fun

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 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: 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 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
apply congr_fun

Goal state after:
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 ≫ δ₂ 2 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: 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 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op)) s

Tactic:
apply congr_fun

Goal state after:
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 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 1) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: 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 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op)) s

Tactic:
apply congr_fun

Goal state after:
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 ≫ δ₂ 0 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 2) ⋯ ⋯).op))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated

Goal state before:
pp: 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 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) s =
    (ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op)) s

Tactic:
apply congr_fun

Goal state after:
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 ≫ δ₂ 1 Edge._proof_2 _proof_2).op)) =
    ⇑(ConcreteCategory.hom (X.map (Hom.tr (⦋0⦌.const ⦋2⦌ 0) ⋯ ⋯).op))