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

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

Tactic:
cases s with
    | nil =>
      cases S with
      | nil => simp
      | cons x S =>
        obtain ⟨a, s⟩ := x
        simpa [map] using ⟨_, _, rfl, rfl⟩
    | cons _ s => simpa using ⟨s, S, rfl, rfl⟩

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case nil
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a : γ
⊢ (join (((a, nil), S), SS)).join = join (join ((a, nil), S), Seq.map join SS)

Tactic:
induction S using recOn with | nil => simp | cons x_1 s_2 => ?_

Goal state after:
case nil.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a : γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, nil), Seq.cons x_1 s_2), SS)).join = join (join ((a, nil), Seq.cons x_1 s_2), Seq.map join SS)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
S : Seq (Seq1 γ)
a x : γ
s_1 : Seq γ
⊢ (join (((a, Seq.cons x s_1), S), SS)).join = join (join ((a, Seq.cons x s_1), S), Seq.map join SS)

Tactic:
induction S using recOn with | nil => simp | cons x_1 s_2 => ?_

Goal state after:
case cons.cons
α : Type u
β : Type v
γ : Type w
f : α → Seq1 β
g : β → Seq1 γ
a✝ : α
s : Seq α
SS : Seq (Seq1 (Seq1 γ))
a x : γ
s_1 : Seq γ
x_1 : Seq1 γ
s_2 : Seq (Seq1 γ)
⊢ (join (((a, Seq.cons x s_1), Seq.cons x_1 s_2), SS)).join =
    join (join ((a, Seq.cons x s_1), Seq.cons x_1 s_2), Seq.map join SS)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = none
⊢ (squashSeq s n).get? m = s.get? m

Tactic:
squashSeq_eq_self_of_terminated s_succ_nth_eq

Goal state after:
case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
m : ℕ
m_lt_n : m < n
s_succ_nth_eq : s.get? (n + 1) = none
⊢ s.get? m = s.get? m
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:

Tactic:
(N' : K) ≤ (N : K) := mod_cast le_max_left _ _
      _ ≤ n := mod_cast n_ge_N
      _ ≤ fib n := mod_cast le_fib_self <| le_trans (le_max_right N' 5) n_ge_N
      _ ≤ fib (n + 1) := mod_cast fib_le_fib_succ
      _ ≤ fib (n + 1) * fib (n + 1) := mod_cast (fib (n + 1)).le_mul_self
      _ ≤ fib (n + 1) * fib (n + 2) := by gcongr; lia
      _ ≤ B * nB := by gcongr

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ ∃ x y z, (map φ P).roots = {x, y, z}

Tactic:
by
  rw [splits_iff_card_roots ha, card_eq_three]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ map φ P = { a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z), d := φ P.a * -(x * y * z) }

Tactic:
by
  apply_fun toPoly
  · rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
  · exact fun P Q ↦ (toPoly_injective P Q).mp

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
⊢ e₁ = e₂

Tactic:
have : (e₁ - e₂) ^ 3 = (e₁ - e₂) := by
    simp only [pow_succ, pow_zero, mul_sub, one_mul, sub_mul, he₁.eq, he₂.eq,
      H'.eq, mul_assoc]
    simp only [← mul_assoc, he₂.eq]
    abel

Goal state after:
R : Type u_1
inst✝ : Ring R
e₁ e₂ : R
he₁ : IsIdempotentElem e₁
he₂ : IsIdempotentElem e₂
H : IsNilpotent (e₁ - e₂)
H' : Commute e₁ e₂
this : (e₁ - e₂) ^ 3 = e₁ - e₂
⊢ e₁ = e₂
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j : n
⊢ ∀ c ∈ Finset.univ, M i c * N c j ∈ I.toAddSubmonoid

Tactic:
intro k _

Goal state after:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : Ideal R
M N : Matrix n n R
hN : N ∈ I.matrix.carrier
i j k : n
a✝ : k ∈ Finset.univ
⊢ M i k * N k j ∈ I.toAddSubmonoid
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R
H : ∀ (i j : n), M i j = 0
i✝ j✝ : n
⊢ M i✝ j✝ = 0 i✝ j✝

Tactic:
apply H

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
by
  apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)
  intro contra; apply hk
  rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra
  rw [eq_bot_iff]
  intro x hx
  rw [mem_genEigenspace] at hx
  rcases hx with ⟨l, -, hx⟩
  rwa [LinearMap.ker_eq_bot.mpr] at hx
  rw [Module.End.coe_pow (f - μ • 1) l]
  exact Function.Injective.iterate contra l

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

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
rcases hx with ⟨l, hl, hx⟩

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 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 g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0

Tactic:
replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : ↑l ≤ k
hx : ((f - μ • 1) ^ l) x = 0
h : Commute ((f - μ • 1) ^ l) g
⊢ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) (g x) = 0
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.maxGenEigenspace μ = (f.genEigenspace μ) ↑(finrank K V)

Tactic:
apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top

Goal state after:
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 μ) ⊤ ≤ (f.genEigenspace μ) ↑(finrank K V)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case insert
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 : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ↑l ≤ k ∧ y ∈ ((f - μ₂ • 1) ^ l).ker
⊢ ∃ l, ↑l ≤ k ∧ y + z ∈ ((f - μ₂ • 1) ^ l).ker

Tactic:
← exists_prop

Goal state after:
case insert
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 : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ ((f - μ₂ • 1) ^ l).ker
⊢ ∃ l, ∃ (_ : ↑l ≤ k), y + z ∈ ((f - μ₂ • 1) ^ l).ker
Module: Mathlib.SetTheory.Cardinal.Free

Goal state before:
pp: case inl
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
⊢ Nonempty (CommRing α)

Tactic:
obtain ⟨e⟩ := Fintype.truncEquivFin α

Goal state after:
case inl.mk
α : Type u
inst✝ : Nonempty α
hR : Finite α
x : Fintype α
this : NeZero (Fintype.card α)
x✝ : Trunc (α ≃ Fin (Fintype.card α))
e : α ≃ Fin (Fintype.card α)
⊢ Nonempty (CommRing α)
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i

Goal state after:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P
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
ha : ¬a = 0
⊢ a ∣ b

Tactic:
let K := FractionRing R

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
ha : ¬a = 0
K : Type u_1 := FractionRing R
⊢ a ∣ b
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
⊢ IsIntegrallyClosed S

Tactic:
let K := FractionRing R

Goal state after:
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
⊢ IsIntegrallyClosed S
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + ((a * star b).re + (b * star a).re) = normSq a + normSq b + 2 * (a * star b).re

Tactic:
by
      rw [← re_add, ← star_mul_star a b, self_add_star', re_coe]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ 0 ≤ normSq a

Tactic:
by
  rw [normSq_def']
  apply_rules [sq_nonneg, add_nonneg]

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

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
s : Set M
x y : M
⊢ y ∈ s ∪ univ * s → x • y ∈ s ∪ univ * s

Tactic:
rintro (hy | ⟨y, -, z, hz, rfl⟩)
        · exact .inr <| mul_mem_mul (mem_univ _) hy
        · simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ∪ univ * s = univ * s

Tactic:
union_eq_right

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ⊆ univ * s
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ (k + 1) = x ^ ↑(k + 1)

Tactic:
rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
⊢ v '' baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' baseOf v f

Tactic:
suffices ∀ (f : G →* S),
      v '' baseOf v (invMonoidHom.comp f) ⊆ (invMonoidHom ∘ v) '' baseOf v f by
    apply subset_antisymm (this f)
    replace this := image_mono (f := invMonoidHom) <| this (invMonoidHom.comp f)
    rw [← MonoidHom.comp_assoc, invMonoidHom_comp_invMonoidHom, MonoidHom.id_comp, image_comp,
      ← image_comp invMonoidHom invMonoidHom, ← MonoidHom.coe_comp, invMonoidHom_comp_invMonoidHom,
      ← image_comp] at this
    simpa using this

Goal state after:
ι : 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
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
⊢ ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f
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 : G₀ˣ
⊢ (inl G₀ H₀) ↑x = ↑(x, 1)

Tactic:
by
  simp [inl]

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 : G₀
⊢ (fst G₀ H₀) ((inl G₀ H₀) x) = x

Tactic:
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
  simp [WithZero.withZeroUnitsEquiv, fst, inl]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
hxy,

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
u : Mˣ
hxy : u = 1
hu : x * ↑1 = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫ f.app (op ⦋n✝ + 1⦌) ≫ Y.δ i.succ = 0

Tactic:
SimplicialObject.δ,

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n✝ : ℕ
i : Fin (n✝ + 1)
x✝ : i ∈ Finset.univ
⊢ (Finset.univ.inf fun k ↦ kernelSubobject (X.δ k.succ)).arrow ≫
      f.app (op ⦋n✝ + 1⦌) ≫ Y.map (SimplexCategory.δ i.succ).op =
    0
Module: Mathlib.Order.Category.NonemptyFinLinOrd

Goal state before:
pp: case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
⊢ b ≤ a

Tactic:
have H : f (φ b) ≤ f (φ a) := f.hom.hom.monotone (le_of_lt h)

Goal state after:
case refine_1
X Y : NonemptyFinLinOrd
f : X ⟶ Y
hf : Epi f
H✝ : ∀ (y : ↑Y.toLinOrd), Nonempty ↑(⇑(ConcreteCategory.hom f) ⁻¹' {y})
φ : ↑Y.toLinOrd → ↑X.toLinOrd := fun y ↦ ↑⋯.some
hφ : ∀ (y : ↑Y.toLinOrd), (ConcreteCategory.hom f) (φ y) = y
a b : ↑Y.1
h : φ b < φ a
H : (ConcreteCategory.hom f) (φ b) ≤ (ConcreteCategory.hom f) (φ a)
⊢ b ≤ a
Module: Mathlib.CategoryTheory.Idempotents.Karoubi

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q : Karoubi C
f : P.Hom Q
⊢ P.p ≫ f.f = f.f

Tactic:
rw [← f.comm, ← assoc, P.idem]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
by rw [comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsIdempotentComplete C
P : Karoubi C
Y : C
i : Y ⟶ P.X
e : P.X ⟶ Y
h₁ : i ≫ e = 𝟙 Y
h₂ : e ≫ i = P.p
⊢ P.p ≫ e ≫ ((toKaroubi C).obj Y).p = e

Tactic:
simp [Category.assoc, h₁, ← h₂]

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at *

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
simp at *

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : k < j
h✝ : i ≤ k
⊢ False
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsIdempotentComplete C → IsIdempotentComplete Cᵒᵖ

Tactic:
intro h
    apply isIdempotentComplete_of_isIdempotentComplete_opposite
    rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]
    exact h

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
simp at *

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : k + 1 < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.castSucc = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
simp at *

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : k < j + 1
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ k = k + 1 + 1
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at *

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : k < j
h✝ : k < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
simp at *

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
simp at *

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.castSucc.succ = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
simp at *

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : k < i
h✝² : j + 1 ≤ k
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.castSucc

Tactic:
simp at *

Goal state after:
case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² h✝¹ : k < j
h✝ : k < i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.castSucc.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.castSucc.succ

Tactic:
simp at *

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

Goal state before:
pp: case pos
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.succ.castSucc

Tactic:
simp at *

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

Goal state before:
pp: case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
H : ⟨i, isLt✝²⟩ ≤ ⟨j, isLt✝¹⟩
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
h✝³ : ¬⟨k, isLt✝⟩.castSucc < ⟨i, isLt✝²⟩
h✝² : ⟨k, isLt✝⟩.succ.castSucc < ⟨j, isLt✝¹⟩.succ
h✝¹ : ¬⟨k, isLt✝⟩.castSucc < ⟨j, isLt✝¹⟩
h✝ : ¬⟨k, isLt✝⟩.succ.castSucc < ⟨i, isLt✝²⟩.castSucc
⊢ ↑⟨k, isLt✝⟩.succ.castSucc = ↑⟨k, isLt✝⟩.succ.succ

Tactic:
simp at *

Goal state after:
case neg
n i : ℕ
isLt✝² : i < n + 2
j : ℕ
isLt✝¹ : j < n + 2
k : ℕ
isLt✝ : k < ⦋n⦌.len + 1
H : i ≤ j
h✝³ : i ≤ k
h✝² : k < j
h✝¹ : j ≤ k
h✝ : i ≤ k + 1
⊢ False