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

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).s.get? (n + 1) = none

Tactic:
← terminatedAt_iff_s_none,

Goal state after:
case inr.inl
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n = none
⊢ (of v).TerminatedAt (n + 1)
Module: Mathlib.Algebra.DirectSum.AddChar

Goal state before:
pp: ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
⊢ Injective directSum

Tactic:
refine toAddMonoidHomEquiv.symm.injective.comp <| DirectSum.toAddMonoid_injective.comp ?_

Goal state after:
ι : Type u_1
R : Type u_2
G : ι → Type u_3
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommGroup (G i)
inst✝ : CommMonoid R
⊢ Injective fun ψ i ↦ toAddMonoidHomEquiv (ψ i)
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ Q.toPoly.coeff 1 = Q.c

Tactic:
coeff_eq_c

Goal state after:
R : Type u_1
P Q : Cubic R
inst✝ : Semiring R
h : P.toPoly = Q.toPoly
⊢ Q.c = Q.c
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ P.a = 1

Tactic:
ha

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 1
a✝ : Nontrivial R
⊢ 1 = 1
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
x : M
⊢ x ∈ (f.genEigenspace μ) 0 ↔ x = 0

Tactic:
← Nat.cast_zero,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f.genEigenspace μ) ↑0 ↔ x = 0
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
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝ : Fintype { i // N i ≠ ⊥ } := hN.fintype
⊢ (trace R M) f = ∑ i ∈ hN.toFinset, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
let _ : Fintype {i | N i ≠ ⊥} := hN.fintype

Goal state after:
ι : 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
hN : {i | N i ≠ ⊥}.Finite
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
x✝¹ : Fintype { i // N i ≠ ⊥ } := hN.fintype
x✝ : Fintype ↑{i | N i ≠ ⊥} := hN.fintype
⊢ (trace R M) f = ∑ i ∈ hN.toFinset, (trace R ↥(N i)) (f.restrict ⋯)
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
e✝ : R
I : Type u_2
inst✝¹ : Fintype I
e : I → R
inst✝ : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
⊢ (fun r ↦ ∑ i, ↑(r i)) ((fun r i ↦ ⟨(fun x ↦ e i * x * e i) r, ⋯⟩) r) = r

Tactic:
by
    simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g

Tactic:
have h := LinearMap.ext_iff.1 (trace_prodMap R M N) (f, g)

Goal state after:
R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h : (trace R (M × N) ∘ₗ prodMapLinear R M N M N R) (f, g) = (id.coprod id ∘ₗ (trace R M).prodMap (trace R N)) (f, g)
⊢ (trace R (M × N)) (f.prodMap g) = (trace R M) f + (trace R N) g
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_3
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ (trace R (M ⊗[R] N)) (map f g) = (trace R M) f * (trace R N) g

Tactic:
by
  have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_tensorProduct R M N) f) g
  simp only [compr₂_apply, mapBilinear_apply, compl₁₂_apply, lsmul_apply,
    smul_eq_mul] at h
  exact h

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case neg.cons
α : Type u_1
inst✝ : DecidableEq α
p : Prop
x : α
b : Bool
L1 L3 : List (α × Bool)
x' : α
b' : Bool
tail : List (α × Bool)
y : α
c : Bool
r : reduce L1 = (y, c) :: tail
h : ¬(x = y ∧ b = !c)
a : α × Bool
L2 : List (α × Bool)
H : (x, b) :: (y, c) :: tail = a :: L2 ++ (x', b') :: (x', !b') :: L3
⊢ p

Tactic:
· refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
⊢ Function.Bijective ⇑i₃

Tactic:
refine ⟨injective_of_surjective_of_injective_of_right_exact f₁ f₂ g₁ g₂ i₁ i₂ i₃
    hc₁ hc₂ hf₁ hg₁ hi₁ hi₂.1 hf₂, fun y ↦ ?_⟩

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝⁵ : Group M₁
inst✝⁴ : Group M₂
inst✝³ : Group M₃
inst✝² : Group N₁
inst✝¹ : Group N₂
inst✝ : Group N₃
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hf₁ : Function.MulExact ⇑f₁ ⇑f₂
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : N₃
⊢ ∃ a, i₃ a = y
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
⊢ Function.Bijective ⇑i₃

Tactic:
refine ⟨injective_of_surjective_of_injective_of_right_exact f₁ f₂ g₁ g₂ i₁ i₂ i₃
    hc₁ hc₂ hf₁ hg₁ hi₁ hi₂.1 hf₂, fun y ↦ ?_⟩

Goal state after:
R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_7
N₂ : Type u_8
N₃ : Type u_9
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : AddCommGroup M₂
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : AddCommGroup N₂
inst✝³ : AddCommGroup N₃
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
hc₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
hc₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
hf₁ : Function.Exact ⇑f₁ ⇑f₂
hg₁ : Function.Exact ⇑g₁ ⇑g₂
hi₁ : Function.Surjective ⇑i₁
hi₂ : Function.Bijective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
hg₂ : Function.Surjective ⇑g₂
y : N₃
⊢ ∃ a, i₃ a = y
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : FreeMonoid α
⊢ x ∈ Set.range ⇑toFreeMonoid ↔ x ∈ {1}ᶜ

Tactic:
grind [eq_one_or_toFreeMonoid x]

Goal state after:
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✝ : AddCommGroup R
⊢ AddCommGroup ℍ[R,c₁,c₂,c₃]

Tactic:
apply (equivProd c₁ c₂ c₃).injective.addCommGroup <;> intros <;> rfl

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

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
⊢ a ∈ A' → ∃ g ∈ S, f' a = g • a

Tactic:
ha

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f f' : X → X
A A' : Set X
S : Finset G
h : IsDecompOn f A S
hA' : A' ⊆ A
hf' : EqOn f f' A'
a : X
ha : a ∈ A'
⊢ ∃ g ∈ S, f' a = g • a
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
A B C : Set X
inst✝¹ : Monoid G
inst✝ : MulAction G X
⊢ IsDecompOn (↑(PartialEquiv.refl X)) (PartialEquiv.refl X).source {1}

Tactic:
simp [IsDecompOn]

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✝ y✝ : M
hx✝ : x✝ ∈ s.saturation
hy✝ : y✝ ∈ s.saturation
ih₁ : ∃ y, x✝ * y ∈ s
ih₂ : ∃ y, y✝ * y ∈ s
y₁ : M
h₁ : x✝ * y₁ ∈ s
y₂ : M
h₂ : y✝ * y₂ ∈ s
⊢ x✝ * y✝ * (y₁ * y₂) ∈ s

Tactic:
rw [mul_mul_mul_comm]; exact mul_mem h₁ h₂

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
⊢ x ∈ ⊥ ↔ IsUnit x

Tactic:
by
  simp_rw [bot_def, Submonoid.mem_saturation_iff, Submonoid.mem_bot, isUnit_iff_exists_inv]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: case inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
hs : (s.erase 0).Nonempty
⊢ #s ≤ #(s * s)

Tactic:
obtain ⟨a, ha⟩ := hs

Goal state after:
case inr
α : Type u_1
inst✝³ : Mul α
inst✝² : Zero α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : IsLeftCancelMulZero α
a : α
ha : a ∈ s.erase 0
⊢ #s ≤ #(s * s)
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
⊢ i ∉ t

Tactic:
contrapose hi₁

Goal state after:
ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₂ : ∀ (k : ι), 1 < f (v k) → f (v k) < f (v i) → v k ∈ closure (v '' t)
hi₁ : i ∈ t
⊢ v i ∈ closure (v '' t)
Module: Mathlib.Algebra.GroupWithZero.ProdHom

Goal state before:
pp: G₀ : Type u_1
H₀ : Type u_2
inst✝¹ : GroupWithZero G₀
inst✝ : GroupWithZero H₀
⊢ Function.Surjective ⇑(snd G₀ H₀)

Tactic:
exact Function.HasRightInverse.surjective ⟨inr .., fun _ ↦ by simp⟩

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : MulZeroOneClass G
inst✝¹ : MulZeroOneClass H
inst✝ : Nontrivial H
f : G →*₀ H
⊢ 1 ≠ 0

Tactic:
by simp [Subtype.ext_iff]

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

Goal state before:
pp: case refine_1.mem
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y x✝ : Bˣ
h : x✝ ∈ ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑x✝ = f x

Tactic:
| mem _ h =>

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 g : P ⟶ Q
⊢ f + g = g + f

Tactic:
ext
    apply add_comm

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

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

Tactic:
comp_p p,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Karoubi C
p : P ⟶ P
hp : p.f ≫ p.f = p.f
⊢ { X := P.X, p := p.f, idem := hp }.p ≫ p.f = p.f
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ {ij | ↑ij.2 ≤ ↑ij.1}
⊢ φ ij hij ∈ {ij | ↑ij.2 ≤ ↑ij.1}ᶜ

Tactic:
φ,

Goal state after:
case hi
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := {ij | ↑ij.2 ≤ ↑ij.1}
φ : (ij : P) → ij ∈ S → P := fun ij hij ↦ (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ij ∈ {ij | ↑ij.2 ≤ ↑ij.1}
⊢ (ij.2.castLT ⋯, ij.1.succ) ∈ {ij | ↑ij.2 ≤ ↑ij.1}ᶜ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl.h.inl
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : k ≤ j.castSucc
⊢ i ≤ (j.predAbove k).castSucc

pp: case inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
· rwa [Fin.predAbove_of_le_castSucc _ _ hjk, Fin.castSucc_castPred]

Goal state after:
case inl.h.inr
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case zero
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ 0
⊢ (Hom.toOrderHom (factor_δ f 0 ≫ δ 0)) k = (Hom.toOrderHom f) k

Tactic:
simp_all [factor_δ, δ, σ]

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

Goal state before:
pp: case succ
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
k : Fin (⦋m⦌.len + 1)
i✝ : Fin (n + 1)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f) k ≠ i✝.succ
⊢ (Hom.toOrderHom (factor_δ f i✝.succ ≫ δ i✝.succ)) k = (Hom.toOrderHom f) k

Tactic:
simp_all [factor_δ, δ, σ]

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ∃ i, θ = δ i

Tactic:
by
  obtain ⟨i, θ', h⟩ := eq_comp_δ_of_not_surjective θ (by
    rw [← epi_iff_surjective]
    grind [→ le_of_epi])
  use i
  have : Mono (θ' ≫ δ i) := by
    rw [← h]
    infer_instance
  have := CategoryTheory.mono_of_mono θ' (δ i)
  rw [h, eq_id_of_mono θ', Category.id_comp]

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

Goal state before:
pp: X : SSet
d✝ d : ℕ
w✝ : X _⦋d⦌
hd : { dim := d, simplex := w✝ }.dim = d✝
⊢ { dim := d, simplex := w✝ }.cast hd = { dim := d, simplex := w✝ }

Tactic:
obtain rfl := hd

Goal state after:
X : SSet
d : ℕ
w✝ : X _⦋d⦌
⊢ { dim := d, simplex := w✝ }.cast ⋯ = { dim := d, simplex := w✝ }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: case mk
X : SSet
inst✝ : X.Finite
n : ℕ
⊢ Finite (X _⦋n⦌)

Tactic:
let φ : (Σ (m : Fin (n + 1)) (f : ⦋n⦌ ⟶ ⦋m.1⦌),
    X.nonDegenerate m.1) → X _⦋n⦌ := fun ⟨m, f, x⟩ ↦ X.map f.op x.1

Goal state after:
case mk
X : SSet
inst✝ : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋↑m⦌) × ↑(X.nonDegenerate ↑m) → X _⦋n⦌ :=
  fun x ↦
    match x with
    | ⟨m, ⟨f, x⟩⟩ => (ConcreteCategory.hom (X.map f.op)) ↑x
⊢ Finite (X _⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ⇑s ↔ Mono (objEquiv s)

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ⇑s ↔ Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ Δ[n].nonDegenerate d ↔ Mono (objEquiv s)

Tactic:
by
  rw [mem_nonDegenerate_iff_strictMono,
    SimplexCategory.mono_iff_injective]
  refine ⟨fun h ↦ h.injective, fun h ↦ ?_⟩
  rw [Fin.strictMono_iff_lt_succ]
  intro i
  obtain h' | h' := (stdSimplex.monotone_apply s i.castSucc_le_succ).lt_or_eq
  · exact h'
  · simpa [Fin.ext_iff] using h h'

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

Goal state before:
pp: n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : Mono (objEquiv x)
⊢ #(Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ) = m + 1

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
n m : ℕ
x✝ : { x // x ∈ Δ[n].nonDegenerate m }
x : Δ[n] _⦋m⦌
hx : Function.Injective ⇑(Hom.toOrderHom (objEquiv x))
⊢ #(Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ) = m + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ Mono (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)))

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ Function.Injective
    ⇑(Hom.toOrderHom (objEquiv (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Mono (objEquiv ↑x)
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Mono (objEquiv ↑x)
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b

Tactic:
SimplexCategory.mono_iff_injective

Goal state after:
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
⊢ ∀ {a b : Fin (d + 1)},
    (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) a ≤ (Equiv.ofBijective (fun i ↦ ⟨↑x i, ⋯⟩) ⋯) b ↔ a ≤ b
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: Δ : SimplexCategory
n : ℕ
i : Fin (n + 2)
⊢ (↾fun f ↦ objEquiv.symm (shift (objEquiv f))) ≫ (stdSimplex.obj Δ).left.δ i.succ =
    (stdSimplex.obj Δ).left.δ i ≫ ↾fun f ↦ objEquiv.symm (shift (objEquiv f))

Tactic:
ext φ
    apply objEquiv.injective
    apply SimplexCategory.Hom.ext
    ext j : 2
    dsimp [SimplicialObject.δ, SimplexCategory.δ, SSet.stdSimplex,
      objEquiv, Equiv.ulift, uliftFunctor]
    cases j using Fin.cases <;> simp

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
x✝¹ x✝ : HomologicalComplex₂ C c₁ c₂
φ₁ φ₂ : x✝¹ ⟶ x✝
h : (toGradedObjectFunctor C c₁ c₂).map φ₁ = (toGradedObjectFunctor C c₁ c₂).map φ₂
i₁ : I₁
i₂ : I₂
⊢ (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂

Tactic:
exact congr_fun h ⟨i₁, i₂⟩

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 : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) = 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃)

Tactic:
ext j i₁ i₂ i₃ h

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 : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃) j
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 : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ Y₃ Z₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
ψ : Y₃ ⟶ Z₃
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (φ ≫ ψ) =
    mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ

Tactic:
ext j i₁ i₂ i₃ h

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 : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ Y₃ Z₃ : GradedObject I₃ C₃
φ : X₃ ⟶ Y₃
ψ : Y₃ ⟶ Z₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (φ ≫ ψ) j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ ≫ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) ψ) j