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

Goal state before:
pp: case pos
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ s.length' ≤ ↑n ↔ s.TerminatedAt n

Tactic:
simpa [length'_of_terminates h] using length_le_iff

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h)[(s.toList h).length - 1]? = s.get? (s.length h - 1)

Tactic:
getElem?_toList,

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
⊢ s.get? ((s.toList h).length - 1) = s.get? (s.length h - 1)
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
ca : Computation α
cb : Computation β
ma : a ∈ ca
mb : b ∈ cb
ab : R a b
b' : β
mb' : b' ∈ cb
⊢ ∃ a, a ∈ ca ∧ R a b'

Tactic:
by
    rw [mem_unique mb' mb]; exact ⟨a, ma, ab⟩

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

Goal state before:
pp: case succ.zero
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
hx : x ∈ (Seq.cons hd tl).get? 0
h_ij : 0 < k + 1
⊢ R x y

Tactic:
simp only [get?_cons_zero, Option.mem_def, Option.some.injEq] at hx

Goal state after:
case succ.zero
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h_hd : ∀ x ∈ tl, R hd x
h_tl : ∀ (i j : ℕ), i < j → ∀ x ∈ tl.get? i, ∀ y ∈ tl.get? j, R x y
x y : α
k : ℕ
hy : y ∈ tl.get? k
h_ij : 0 < k + 1
hx : hd = x
⊢ R x y
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
hx : x ∈ tl
⊢ R hd x

Tactic:
rw [mem_iff_exists_get?] at hx

Goal state after:
α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : ∀ (i j : ℕ), i < j → ∀ x ∈ (Seq.cons hd tl).get? i, ∀ y ∈ (Seq.cons hd tl).get? j, R x y
x : α
hx : ∃ i, some x = tl.get? i
⊢ R hd x
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (m : ℕ), fib (m + n + 1) = fib m * fib n + fib (m + 1) * fib (n + 1)
m : ℕ
⊢ fib (m + (n + 1) + 1) = fib m * fib (n + 1) + fib (m + 1) * fib (n + 1 + 1)

Tactic:
specialize ih (m + 1)
    rw [add_assoc m 1 n, add_comm 1 n] at ih
    simp only [fib_add_two, ih]
    ring

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

Goal state before:
pp: case succ
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
ih : b.drop m ≠ nil → motive (a.drop m) (b.drop m)
hb : (b.drop m).tail ≠ nil
⊢ motive (a.drop m).tail (b.drop m).tail

Tactic:
generalize b.drop m = tb at *

Goal state after:
case succ
α : Type u
β : Type v
a : Seq α
b : Seq β
motive : Seq α → Seq β → Prop
base : motive a b
step :
  ∀ (a : Seq α) (b : Seq β),
    motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl
m : ℕ
tb : Seq β
ih : tb ≠ nil → motive (a.drop m) tb
hb : tb.tail ≠ nil
⊢ motive (a.drop m).tail tb.tail
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a b : α
s : Seq α
S : Seq (Seq1 α)
⊢ join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

Tactic:
dsimp [join]; rw [destruct_cons]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries

Goal state before:
pp: K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
⊢ ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs' n = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n

Tactic:
of_convs_eq_convs'

Goal state after:
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
⊢ ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs' n = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs' n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.leadingCoeff = c

Tactic:
simp [hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.degree = 1

Tactic:
simp [hc]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
c d : R
inst✝ : Semiring R
hc : c ≠ 0
⊢ { a := 0, b := 0, c := c, d := d }.toPoly.natDegree = 1

Tactic:
simp [hc]

Goal state after:
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
ifp_fr_eq_zero : ifp.fr = 0
this : v - g.convs n = 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))

Tactic:
simpa [ifp_fr_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: 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

Tactic:
simp [hi]

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₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * (e₂ * e₁) - (e₂ * (e₂ * e₁) - e₂)) = e₁ - e₂

Tactic:
simp only [← mul_assoc, he₂.eq]

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₂
⊢ e₁ - e₂ * e₁ - (e₂ * e₁ - e₂ * e₁) - (e₂ * e₁ - e₂ * e₁ - (e₂ * e₁ - e₂)) = e₁ - e₂
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: case inr
ι : Type u_1
inst✝⁹ : DecidableEq ι
R : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
N₁ : ι → Submodule R M₁
h₁ : IsInternal N₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
N₂ : ι → Submodule R M₂
h₂ : IsInternal N₂
κ₁ : ι → Type u_7
κ₂ : ι → Type u_8
inst✝³ : (i : ι) → Fintype (κ₁ i)
inst✝² : ∀ (i : ι), Finite (κ₂ i)
inst✝¹ : (i : ι) → DecidableEq (κ₁ i)
inst✝ : Fintype ι
b₁ : (i : ι) → Basis (κ₁ i) R ↥(N₁ i)
b₂ : (i : ι) → Basis (κ₂ i) R ↥(N₂ i)
f : M₁ →ₗ[R] M₂
hf : ∀ (i : ι), MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)
i : ι
snd✝¹ : κ₂ i
j : ι
snd✝ : κ₁ j
hij : i ≠ j
⊢ ((h₂.collectedBasis b₂).repr (f ((h₁.collectedBasis b₁) ⟨j, snd✝⟩))) ⟨i, snd✝¹⟩ =
    if h : i = j then ((b₂ i).repr ((f.restrict ⋯) ((b₁ i) (cast ⋯ snd✝)))) snd✝¹ else 0

Tactic:
simp [hij, h₂.collectedBasis_repr_of_mem_ne _ hij.symm (hf _ (Subtype.mem _))]

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)
s : Finset M
b : Basis (↥s) R M
⊢ ((toMatrix b b) f * (toMatrix b b) g).trace = ((toMatrix b b) g * (toMatrix b b) f).trace

Tactic:
apply Matrix.trace_mul_comm

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

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
s : Finset R
⊢ μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)

Tactic:
induction s using Finset.induction_on with

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
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ (LinearMap.trace R ↥p) id + (LinearMap.trace R ↥f.ker) 0 = ↑(finrank R ↥p)

Tactic:
trace_id,

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst✝³ : Free R ↥p
inst✝² : Module.Finite R ↥p
inst✝¹ : Free R ↥f.ker
inst✝ : Module.Finite R ↥f.ker
⊢ ↑(finrank R ↥p) + (LinearMap.trace R ↥f.ker) 0 = ↑(finrank R ↥p)
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
⊢ (-f).HasEigenvalue μ ↔ f.HasEigenvalue (-μ)

Tactic:
simp only [hasEigenvalue_iff, eigenspace_def]
  rw [← LinearMap.ker_neg]
  simp [add_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ k.Coprime p

Tactic:
apply Nat.Coprime.symm

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ p.Coprime k
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ x y : FreeMagma α✝
ih1 : id <$> x = x
ih2 : id <$> y = y
⊢ id <$> (x * y) = x * y

Tactic:
rw [map_mul', ih1, ih2]

Goal state after:
Module: Mathlib.Algebra.Free

Goal state before:
pp: α β α✝ : Type u
x✝ : FreeSemigroup α✝
x : α✝
y : FreeSemigroup α✝
ih1 : id <$> pure x = pure x
ih2 : id <$> y = y
⊢ id <$> (pure x * y) = pure x * y

Tactic:
rw [map_mul', ih1, ih2]

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.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
y : M₃
⊢ 1 y = 1 ↔ y ∈ Set.range ⇑f₂

Tactic:
simpa using hf₂ y

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ (countP p) (of x) = if p x then 1 else 0

Tactic:
rw [countP_apply, toList_of, List.countP_singleton]
  simp only [decide_eq_true_eq]

Goal state after:
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.Injective ⇑i₂
hf₂ : Function.Surjective ⇑f₂
y : M₃
⊢ 0 y = 0 ↔ y ∈ Set.range ⇑f₂

Tactic:
simpa using hf₂ y

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

Goal state before:
pp: ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ (∑ i ∈ s, f i).den ∣ s.lcm fun i ↦ (f i).den

Tactic:
induction s using Finset.induction_on with

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

Goal state before:
pp: ι : Type u_3
s : Finset ι
f : ι → ℚ
⊢ (∏ i ∈ s, f i).den ∣ ∏ i ∈ s, (f i).den

Tactic:
induction s using Finset.induction_on with

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 : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.restr A = f.toPartialEquiv

Tactic:
PartialEquiv.restr_eq_of_source_subset hA

Goal state after:
X : Type u_1
G : Type u_2
inst✝ : SMul G X
f : Equidecomp X G
A : Set X
hA : f.source ⊆ A
⊢ f.toPartialEquiv = f.toPartialEquiv
Module: Mathlib.Algebra.Quaternion

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

Tactic:
by rw [h, re_coe]

Goal state after:
Module: Mathlib.Algebra.Quaternion

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

Tactic:
by
  simpa using! QuaternionAlgebra.self_add_star' a

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

Goal state before:
pp: case hfP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ (algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff ≠ 0

pp: case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    C ((algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff) * map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

pp: case hfmodP2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (Ideal.Quotient.mk (ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2)) (f %ₘ X) ≠ 0

Tactic:
· simp only [IsScalarTower.algebraMap_eq R (R ⧸ P) (FractionRing (R ⧸ P)),
      Quotient.algebraMap_eq, coe_comp, Function.comp_apply, ne_eq,
      FaithfulSMul.algebraMap_eq_zero_iff]
    rw [Ideal.Quotient.eq_zero_iff_mem]
    exact hfl

Goal state after:
case hfmodP
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (algebraMap R (FractionRing (R ⧸ P))) f =
    C ((algebraMap R (FractionRing (R ⧸ P))) f.leadingCoeff) * map (algebraMap R (FractionRing (R ⧸ P))) X ^ f.natDegree

case hfmodP2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0 : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
⊢ map (Ideal.Quotient.mk (ker (algebraMap R (FractionRing (R ⧸ P))) ^ 2)) (f %ₘ X) ≠ 0
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b ↦ 1 • b) s = s

Tactic:
one_smul,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : DecidableEq γ
inst✝³ : DecidableEq β
inst✝² : DecidableEq α
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Finset β
⊢ image (fun b ↦ b) s = s
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a • a⁻¹ • b ∈ a • s ↔ b ∈ a • s

Tactic:
smul_inv_smul

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ b ∈ a • s ↔ b ∈ a • s
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a • b ∈ a • a⁻¹ • s ↔ a • b ∈ s

Tactic:
smul_inv_smul

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s : Finset β
a : α
b : β
⊢ a • b ∈ s ↔ a • b ∈ s
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq β
inst✝² : Group α
inst✝¹ : MulAction α β
s : Finset β
a : α
inst✝ : Fintype β
⊢ a • s = univ ↔ s = univ

Tactic:
rw [smul_eq_iff_eq_inv_smul, smul_finset_univ]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ closure s ↔ ∃ y, ∃ z ∈ s, y * z = x

Tactic:
rw [← SetLike.mem_coe, coe_closure']

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
⊢ x ∈ univ * s ↔ ∃ y, ∃ z ∈ s, y * z = x
Module: Mathlib.Algebra.Group.ForwardDiff

Goal state before:
pp: case inl
m k : ℕ
hmn : m < m + k + 1
⊢ ∑ x ∈ range (k + 1), 0 = 0

Tactic:
sum_const_zero

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Order

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : M ≠ ⊤
⊢ comap φ M ≠ ⊤

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤

Tactic:
· rwa [← (comap_injective hφ).ne_iff, comap_top] at hM

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
φ : G →* H
hφ : Function.Surjective ⇑φ
M : Subgroup H
hM✝ : IsCoatom M
hM : ∀ (b : Subgroup H), M < b → b = ⊤
⊢ ∀ (b : Subgroup G), comap φ M < b → b = ⊤
Module: Mathlib.Algebra.Group.Submonoid.Support

Goal state before:
pp: G : Type u_1
inst✝ : Group G
M : Submonoid G
h : M.mulSupport = ⊥
x : G
⊢ x ∈ M → x⁻¹ ∈ M → x = 1

Tactic:
apply_fun (x ∈ ·) at h

Goal state after:
G : Type u_1
inst✝ : Group G
M : Submonoid G
x : G
h : (x ∈ M.mulSupport) = (x ∈ ⊥)
⊢ x ∈ M → x⁻¹ ∈ M → x = 1
Module: Mathlib.Algebra.Group.Submonoid.Saturation

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
s : Submonoid M
x x✝ : M
hx : x✝ ∈ s
⊢ ∃ y, x✝ * y ∈ s

Tactic:
| mem _ hx =>

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: case inr
ι : Type u_1
G : Type u_3
inst✝¹ : CommGroup G
inst✝ : InvolutiveInv ι
v : ι → G
hv_one : ∀ (i : ι), v i ≠ 1
hv_inv : ∀ (i : ι), v i⁻¹ = (v i)⁻¹
s t : Set ι
hst : s ⊆ {i | IsMulIndecomposable v t i}
hv_t : ∀ (i : ι), i ∈ t ∨ i⁻¹ ∈ t
h_sub : s ⊆ t
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
k : ι
hk : v k = v i / v j
hk' : k⁻¹ ∈ t
⊢ False

Tactic:
suffices ¬ IsMulIndecomposable v t j from this (hst hj)
    simp only [IsMulIndecomposable, hv_one, or_self, imp_false, not_and, not_forall, not_not]
    exact fun _ ↦ ⟨k⁻¹, hk', i, h_sub hi, by simp [hv_inv, 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
s : Set ι
hst : s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}
i : ι
hf : v i = 1
⊢ f (v i) = 1

Tactic:
by simp [hf]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

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

pp: case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X

Tactic:
· intro X Y f
    ext j
    simp

Goal state after:
case h_obj
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ ∀ (X : J ⥤ C),
    (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X =
      ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (1 • X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
one_smul,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + (-1) ^ ↑1 • X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + -(1 • X.left.δ 1)) ≫ X.hom.app (op ⦋0⦌) = 0

Tactic:
one_smul,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : SimplicialObject.Augmented C
⊢ (X.left.δ 0 + -X.left.δ 1) ≫ X.hom.app (op ⦋0⦌) = 0
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 : ℕ
h : n + (i + 1) = m
⊢ X.σ₀Iter (i + 1) h = X.σ 0 ≫ X.σ₀Iter i ⋯

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

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

Goal state before:
pp: n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(Hom.toOrderHom θ)
⊢ ∃ i θ', θ = σ i ≫ θ'

Tactic:
simp only [Function.Injective, exists_prop, not_forall] at hθ
  -- as θ is not injective, there exists `x<y` such that `θ x = θ y`
  -- and then, `θ x = θ (x+1)`
  have hθ₂ : ∃ x y : Fin (n + 2), (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) y ∧ x < y := by
    rcases hθ with ⟨x, y, ⟨h₁, h₂⟩⟩
    by_cases h : x < y
    · exact ⟨x, y, ⟨h₁, h⟩⟩
    · refine ⟨y, x, ⟨h₁.symm, ?_⟩⟩
      lia
  rcases hθ₂ with ⟨x, y, ⟨h₁, h₂⟩⟩
  use x.castPred ((Fin.le_last _).trans_lt' h₂).ne
  apply eq_σ_comp_of_not_injective'
  apply le_antisymm
  · exact θ.toOrderHom.monotone (le_of_lt Fin.castSucc_lt_succ)
  · rw [Fin.castSucc_castPred, h₁]
    exact θ.toOrderHom.monotone ((Fin.succ_castPred_le_iff _).mpr h₂)

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
⊢ i.succAbove = j.succAbove

Tactic:
ext k : 1

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : δ i = δ j
k : Fin (n + 1)
⊢ i.succAbove k = j.succAbove k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
⊢ i.predAbove = j.predAbove

Tactic:
ext k : 1

Goal state after:
n : ℕ
i j : Fin (n + 1)
hij : σ i = σ j
k : Fin (n + 1 + 1)
⊢ i.predAbove k = j.predAbove k
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ (wideCospan ι X).obj none)

Tactic:
dsimp [wideCospan]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ ⊤_ C)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
⊢ (stdSimplex.obj n).Finite

Tactic:
induction n using SimplexCategory.rec with | _ n
  exact finite_of_hasDimensionLT _ (n + 1) inferInstance

Goal state after: