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

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

Tactic:
obtain (ifp_fr_eq_zero | ifp_fr_ne_zero) := eq_or_ne ifp.fr 0

Goal state after:
case inl
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_eq_zero : ifp.fr = 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))

case inr
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
g_finite_correctness : v = GenContFract.compExactValue pred_conts conts ifp.fr
ifp_fr_ne_zero : ifp.fr ≠ 0
⊢ let g := of v;
  let B := (g.contsAux (n + 1)).b;
  let pB := (g.contsAux n).b;
  v - g.convs n = if ifp.fr = 0 then 0 else (-1) ^ n / (B * (ifp.fr⁻¹ * B + pB))
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp
g : GenContFract K := of v
conts : Pair K := g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
ifp_fr_ne_zero : ifp.fr ≠ 0
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
n_eq_zero_or_not_terminatedAt_pred_n : n = 0 ∨ ¬g.TerminatedAt (n - 1)
determinant_eq : pA * B - pB * A = (-1) ^ n
pB_ineq : ↑(fib n) ≤ pB
⊢ n + 1 ≤ 1 ∨ ¬g.TerminatedAt (n + 1 - 2)

Tactic:
rcases n_eq_zero_or_not_terminatedAt_pred_n with n_eq_zero | not_terminatedAt_pred_n
        · simp [n_eq_zero]
        · exact Or.inr not_terminatedAt_pred_n

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ IsIdempotentElem (e default) ∧ ∑ i, e i = 1 ↔ e default = 1

Tactic:
Fintype.sum_unique,

Goal state after:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ IsIdempotentElem (e default) ∧ e default = 1 ↔ e default = 1
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

Tactic:
by_cases hi : i = k

Goal state after:
case pos
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k

case neg
I : Type u_4
inst✝² : Fintype I
inst✝¹ : DecidableEq I
R : I → Type u_5
inst✝ : (i : I) → Semiring (R i)
i j : I
hij : i ≠ j
k : I
hi : ¬i = k
⊢ (Pi.single i 1 * Pi.single j 1) k = 0 k
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
I : Type u_3
e : I → R
inst✝ : Fintype I
he : CompleteOrthogonalIdempotents e
⊢ ∑ i, (⇑f ∘ e) i = 1

Tactic:
simp only [Function.comp_apply, ← map_sum, he.complete, map_one]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr.refine_2.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (1 ^ (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
⊢ MulOpposite.unop k * (a ^ n * (a * e₂)) = 0

Tactic:
ha',

Goal state after:
case inr.refine_2.succ
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
k : Rᵐᵒᵖ
n : ℕ
hn : (a - a ^ 2) ^ (n + 1) = 0
hk :
  MulOpposite.unop (1 ^ (n + 1) - MulOpposite.op (1 - a ^ (n + 1)) ^ (n + 1)) =
    MulOpposite.unop ((1 - MulOpposite.op (1 - a ^ (n + 1))) * k)
this : 1 - (1 - a ^ (n + 1)) ^ (n + 1) = MulOpposite.unop k * a ^ (n + 1)
⊢ MulOpposite.unop k * (a ^ n * 0) = 0
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
⊢ matrix n I.jacobson ≤ (matrix n I).jacobson

Tactic:
intro M MI
  rw [matrix_eq_sum_single M]
  apply sum_mem
  intro i _
  apply sum_mem
  intro j _
  apply single_mem_jacobson_matrix I _ (MI i j)

Goal state after:
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
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i ↦ Free.chooseBasis R ↥(N i)
⊢ ∑ i, ((toMatrix (b i) (b i)) (f.restrict ⋯)).trace = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
← trace_eq_matrix_trace

Goal state after:
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₂ : R
i : I
⊢ e i * (r₁ * e i * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)

Tactic:
conv in (r₁ * _ * r₂) => rw [← (he.idem i).eq]
      simp_rw [mul_assoc]

Goal state after:
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.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) } ≃ (A[ε] →ₐ[R] B)

Tactic:
by
  refine Equiv.trans ?_ TrivSqZeroExt.liftEquiv
  exact {
    toFun := fun fe => ⟨
      (fe.val.1, MulOpposite.op fe.val.2 • fe.val.1.toLinearMap),
      fun x y => show (fe.val.1 x * fe.val.2) * (fe.val.1 y * fe.val.2) = 0 by
        rw [(fe.prop.2 _).mul_mul_mul_comm, fe.prop.1, mul_zero],
      fun r x => show fe.val.1 (r * x) * fe.val.2 = fe.val.1 r * (fe.val.1 x * fe.val.2) by
        rw [map_mul, mul_assoc],
      fun r x => show fe.val.1 (x * r) * fe.val.2 = (fe.val.1 x * fe.val.2) * fe.val.1 r by
        rw [map_mul, (fe.prop.2 _).right_comm]⟩
    invFun := fun fg => ⟨
      (fg.val.1, fg.val.2 1),
      fg.prop.1 _ _,
      fun a => show fg.val.2 1 * fg.val.1 a = fg.val.1 a * fg.val.2 1 by
        rw [← fg.prop.2.1, ← fg.prop.2.2, smul_eq_mul, op_smul_eq_mul, mul_one, one_mul]⟩
    left_inv := fun fe => Subtype.ext <| Prod.ext rfl <|
      show fe.val.1 1 * fe.val.2 = fe.val.2 by
        rw [map_one, one_mul]
    right_inv := fun fg => Subtype.ext <| Prod.ext rfl <| LinearMap.ext fun x =>
      show fg.val.1 x * fg.val.2 1 = fg.val.2 x by
        rw [← fg.prop.2.1, smul_eq_mul, mul_one] }

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: case pos
R : Type u
inst✝² : CommSemiring R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : M →ₗ[R] M
H : ∃ s, Nonempty (Basis (↥s) R M)
⊢ (trace R M) (f * g) = (trace R M) (g * f)

Tactic:
let ⟨s, ⟨b⟩⟩ := H
    simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
    apply Matrix.trace_mul_comm

Goal state after:
Module: Mathlib.Algebra.Field.NegOnePow

Goal state before:
pp: case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k + 1)

Tactic:
zpow_add_one₀ (by simp),

Goal state after:
case inr
K : Type u_1
inst✝ : DivisionRing K
k : ℤ
⊢ ↑↑(2 * k + 1).negOnePow = (-1) ^ (2 * k) * -1
Module: Mathlib.Algebra.Field.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝³ : AddMonoid α
inst✝² : Neg β
inst✝¹ : GroupWithZero γ
inst✝ : DistribMulAction γ α
h : Antiperiodic f c
a : γ
ha : a ≠ 0
⊢ Antiperiodic (fun x ↦ f (a⁻¹ • x)) (a • c)

Tactic:
simpa only [inv_inv] using h.const_smul₀ (inv_ne_zero ha)

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

Goal state before:
pp: case cons.nil
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
htl : reduce tl1 = []
ih : Red tl1 []
⊢ Red (hd1 :: tl1)
    (List.rec [hd1] (fun head tail tail_ih ↦ if hd1.1 = head.1 ∧ hd1.2 = !head.2 then tail else hd1 :: head :: tail) [])

Tactic:
exact Red.cons_cons ih

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

Goal state before:
pp: case neg
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
hd1 : α × Bool
tl1 : List (α × Bool)
hd2 : α × Bool
tl2 : List (α × Bool)
htl : reduce tl1 = hd2 :: tl2
ih : Red tl1 (hd2 :: tl2)
h : ¬(hd1.1 = hd2.1 ∧ hd1.2 = !hd2.2)
⊢ Red (hd1 :: tl1) (hd1 :: hd2 :: tl2)

Tactic:
exact Red.cons_cons ih

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : FreeGroup α), reduce x.toWord = x.toWord

Tactic:
by
  rintro ⟨L⟩
  exact reduce.idem

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥((FreeAlgebra.lift R) Subtype.val).range ≤ max (max (lift.{v, u} #R) (lift.{u, v} #↑s)) ℵ₀

Tactic:
exact H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

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_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C (map (algebraMap R K) g).leadingCoeff = ↑u

Tactic:
← hu,

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_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff * q ^ m + r
u : K[X]ˣ
hu : map (algebraMap R K) q ^ m * ↑u = map (algebraMap R K) g
a : K
ha : IsUnit a
ha' : C a = ↑u
⊢ C (map (algebraMap R K) q ^ m * ↑u).leadingCoeff = ↑u
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝

Tactic:
rcases hg _ aB with ⟨δ, δ_mem, hδ⟩

Goal state after:
X : Type u_1
G : Type u_2
inst✝¹ : Monoid G
inst✝ : MulAction G X
g f : X → X
B A : Set X
T S : Finset G
hg : IsDecompOn g B T
hf : IsDecompOn f A S
a✝ : X
aA : a✝ ∈ A
aB : a✝ ∈ f ⁻¹' B
γ : G
γ_mem : γ ∈ S
hγ : f a✝ = γ • a✝
δ : G
δ_mem : δ ∈ T
hδ : g (f a✝) = δ • f a✝
⊢ ∃ g_1 ∈ T * S, (g ∘ f) a✝ = g_1 • a✝
Module: Mathlib.Algebra.Group.NatPowAssoc

Goal state before:
pp: R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

Tactic:
by
    rw [pow_zero, npow_zero, Int.cast_one]

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✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ioc a b * Ico c d) ⊆ ↑(Ioo (a * c) (b * d))

Tactic:
by simpa using Set.Ioc_mul_Ico_subset' _ _ _ _

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
inst✝ : InvolutiveInv G
s : Set G
⊢ s⁻¹.encard = s.encard

Tactic:
by
  simp [← toENat_cardinalMk]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Card

Goal state before:
pp: G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
⊢ (a • s).encard = s.encard

Tactic:
by
  simp [← toENat_cardinalMk]

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
this : ∀ (f : G →* S), v '' baseOf v (invMonoidHom.comp f) ⊆ ⇑invMonoidHom ∘ v '' baseOf v f
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)

Tactic:
replace this := image_mono (f := invMonoidHom) <| this (invMonoidHom.comp f)

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
this :
  ⇑invMonoidHom '' v '' baseOf v (invMonoidHom.comp (invMonoidHom.comp f)) ⊆
    ⇑invMonoidHom '' ⇑invMonoidHom ∘ v '' baseOf v (invMonoidHom.comp f)
⊢ ⇑invMonoidHom ∘ v '' baseOf v f ⊆ v '' baseOf v (invMonoidHom.comp f)
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✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | 1 < f (v i)} ∪ v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))

Tactic:
union_subset_iff

Goal state after:
ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder S
inst✝³ : Finite ι
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
f : G →* S
hf : ∀ (i : ι), f (v i) ≠ 1
this : univ = {i | 1 < f (v i)} ∪ {i | f (v i) < 1}
⊢ v '' {i | 1 < f (v i)} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f)) ∧
    v '' {i | f (v i) < 1} ⊆ ↑(closure (v '' IsMulIndecomposable.baseOf v f))
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
hxy : x ^ n = y ^ n
u : Mˣ
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y

Tactic:
← hu,

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 : x ^ n = (x * ↑u) ^ n
hu : x * ↑u = y
hx : IsLeftRegular (x ^ n)
⊢ x = y
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: case a.a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom ≫ φ.inv

pp: case a.a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p

pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom

Tactic:
φ.hom_inv_id

Goal state after:
case a.a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| 𝟙 X'

case a.a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| p

case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
| φ.hom
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
φ : X' ≅ (ε.inverse ⋙ ε.functor).obj X' := ε.counitIso.symm.app X'
⊢ p ≫ φ.hom = φ.hom ≫ φ.inv ≫ p ≫ φ.hom

Tactic:
slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f = h.f

Tactic:
← cancel_mono f

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
Z✝ : Karoubi C
g h : Z✝ ⟶ (toKaroubi C).obj X✝
eq : g ≫ (toKaroubi C).map f = h ≫ (toKaroubi C).map f
⊢ g.f ≫ f = h.f ≫ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

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

Tactic:
Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
      (hjk.trans Fin.castSucc_lt_succ).le),

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

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

Tactic:
· simp [δ, Fin.succAbove_of_castSucc_lt _ _ h]

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

Goal state before:
pp: case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : ↑j = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero
        (by rintro rfl; dsimp at hj'; lia)

Goal state after:
case succ.succ
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m),
    ↑j = ↑j' + i → δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : ↑j.succ = ↑j' + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f✝ g f : X ⟶ Y
n : ℕ
⊢ (X.σ 0 ≫ f.app (op ⦋n + 1⦌)) ≫ Y.δ 0 = f.app (op ⦋n⦌)

Tactic:
have := Y.δ_comp_σ_self (n := n) (i := 0)
    dsimp at this
    simp only [SimplicialObject.σ_naturality, Category.assoc, this, Category.comp_id]

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

Goal state before:
pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)

Tactic:
by_cases h'' : y = i

Goal state after:
case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)

case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : ¬y = i
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) y)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = ↑((ConcreteCategory.hom (σ₀Iter (i + 1) ⋯)) k)

Tactic:
σ₀Iter_coe_eq_of_lt (i + 1) ..

Goal state after:
case neg
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : ↑k ≤ i
⊢ ↑((ConcreteCategory.hom (σ₀Iter i ⋯)) (j.predAbove k)) = 0
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ ofSection ((ConcreteCategory.hom (f.app X)) x) ≤ (ofSection x).image f

Tactic:
simp only [ofSection_le_iff, image_obj, Set.mem_image]
    exact ⟨x, mem_ofSection_obj x, rfl⟩

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.subcomplex ≤ y.subcomplex

Tactic:
simp only [Subcomplex.ofSimplex_le_iff]
  exact ⟨_, hf⟩

Goal state after: