mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ a :: l₂' ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁ ++ t :: a :: l₂' ++ ts

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r Cycle.nil ↔ ∀ n < 0, r (f^[n] x) (f^[n + 1] x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
⊢ ↑(centralizer R s) ∪ ↑(centralizer R s) = ↑(Subalgebra.centralizer R (s ∪ star s))

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
s t : List α
⊢ [].permutations' ~ [].permutations'

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ (n % period m a) • a = m ^ n • a

Tactic:
pow_mod_period_smul

Goal state after:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
n : ℕ
m : M
a : α
⊢ m ^ n • a = m ^ n • a
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
h : x ∉ []
⊢ ([] ++ [x]).nextOr x d = d

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : Set (StarSubalgebra R A)
⊢ ↑(sInf S).toSubalgebra = ↑(sInf (toSubalgebra '' S))

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ (n % period a b) • b = a ^ n • b

Tactic:
pow_mod_period_smul

Goal state after:
α : Type v
G : Type u
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
b : α
n : ℕ
⊢ a ^ n • b = a ^ n • b
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i).toSubalgebra = ↑(⨅ i, (S i).toSubalgebra)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ (y :: l).nextOr x ((y :: l).get ⟨0, ⋯⟩) = l.nextOr x (l.get ⟨0, ⋯⟩)

Tactic:
nextOr_cons_of_ne _ _ _ _ hy,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l.dropLast
y : α
hy : x ≠ y
⊢ l.nextOr x ((y :: l).get ⟨0, ⋯⟩) = l.nextOr x (l.get ⟨0, ⋯⟩)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : x ∈ y :: l ++ [x]
⊢ (y :: l ++ [x]).get ⟨0, ⋯⟩ = y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons.zero
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = s.insertIdx n x
hn : 0 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[0] = (y :: s).insertIdx 0 x

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
⊢ count (x :: l) (permutations'Aux x l) = (takeWhile (fun x_1 ↦ decide (x = x_1)) l).length + 1

Tactic:
induction l generalizing x with

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x : α
⊢ (permutations'Aux x []).length = [].length + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x s).length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
x : α
hx : ¬x ∈ []
⊢ (permutations'Aux x []).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : Semiring B
inst✝³ : Algebra R B
inst✝² : StarRing B
inst✝¹ : StarModule R A
inst✝ : StarModule R B
φ : A →⋆ₐ[R] B
x : B
a : A
ha : (↑φ).toRingHom a = x
⊢ a ∈ ↑⊤.toSubsemiring

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case cons
α : Type u_1
x y : α
s : List α
IH : ¬x ∈ s → (permutations'Aux x s).Nodup
hx : ¬x = y ∧ ¬x ∈ s
⊢ Injective (cons y)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
y : α
k : ℕ
hd : α
tl : List α
hl : Function.Injective (hd :: tl).get
h✝ : (y :: hd :: tl).getLast ⋯ ∈ hd :: tl
h : (y :: hd :: tl).getLast ⋯ ∈ y :: hd :: tl
hy : (y :: hd :: tl).getLast ⋯ ≠ y
H : (y :: hd :: tl).getLast ⋯ ∈ (y :: hd :: tl).dropLast
hk : k + 1 < (y :: hd :: tl).dropLast.length
hk' : (y :: hd :: tl).dropLast[k + 1] = (y :: hd :: tl).getLast ⋯
⊢ tl.length < (hd :: tl).length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case nil
α : Type u_1
s : List α
⊢ [].permutations'.Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x hd : α
h : x ∈ [hd]
⊢ [hd].prev x h ∈ [hd]

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d : α
hl : [] ≠ []
h : [].getLast hl ∉ [].dropLast
⊢ [].nextOr ([].getLast hl) d = d

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
d head✝ : α
hl : [head✝] ≠ []
h : [head✝].getLast hl ∉ [head✝].dropLast
⊢ [head✝].nextOr ([head✝].getLast hl) d = d

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
⊢ (a :: tail).prev a ha = (a :: tail)[(idxOf a (a :: tail) + ((a :: tail).length - 1)) % (a :: tail).length]

Tactic:
simp

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
tail : List α
ha : a ∈ a :: tail
⊢ (a :: tail).getLast ⋯ = (a :: tail)[tail.length]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) + (head :: tail).length - 1) % (head :: tail).length

pp: case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length

Tactic:
Nat.sub_add_comm,

Goal state after:
case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ idxOf a (head :: tail) - 1 = (idxOf a (head :: tail) - 1 + (head :: tail).length) % (head :: tail).length

case neg.e_i
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ idxOf a (head :: tail)

case neg.e_i.h
α : Type u_1
inst✝ : DecidableEq α
a head : α
tail : List α
ha : a ∈ head :: tail
ha₀ : ¬a = head
⊢ 1 ≤ (head :: tail).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.next l ⋯).length = (l.rotate 1).length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case hl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (pmap l.prev l ⋯).length = (l.rotate (l.length - 1)).length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
x✝ : List α
⊢ (reverse (Quot.mk (⇑(IsRotated.setoid α)) x✝)).reverse = Quot.mk (⇑(IsRotated.setoid α)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
induction s using Quot.inductionOn with

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk (⇑(IsRotated.setoid α)) l → ∀ ⦃y : α⦄, y ∈ Quot.mk (⇑(IsRotated.setoid α)) l → x = y
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.inl
α : Type u_1
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [] → x = y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.inr
α : Type u_1
z : α
⊢ ∀ ⦃x : α⦄, x ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → ∀ ⦃y : α⦄, y ∈ Quot.mk ⇑(IsRotated.setoid α) [z] → x = y

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
by
  induction s using Quot.inductionOn with | _ l
  simp only [length_subsingleton_iff, length_coe, mk_eq_coe, le_iff_lt_or_eq, Nat.lt_add_one_iff,
    length_eq_zero_iff, length_eq_one_iff, Nat.not_lt_zero, false_or] at h
  rcases h with (rfl | ⟨z, rfl⟩) <;> simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (hd = hd ∨ hd = hd' ∨ hd ∈ tl) ∧ (hd' = hd ∨ hd' = hd' ∨ hd' ∈ tl)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
x y : α
hxy : x ≠ y
hx : x ∈ s
hy : y ∈ s
⊢ 2 ≤ s.length

Tactic:
induction s using Quot.inductionOn with

Goal state after:
case h
α : Type u_1
x y : α
hxy : x ≠ y
l : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
h : s.Subsingleton
⊢ s.Nodup

Tactic:
induction s using Quot.inductionOn with

Goal state after:
case h
α : Type u_1
l : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) l)
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) l)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), (toMultiset (Quotient.mk'' a)).card = length (Quotient.mk'' a)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
⊢ ∀ (a : List α), toMultiset (Quotient.mk'' a) = 0 ↔ Quotient.mk'' a = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Cycle α
⊢ ∀ (a : List α), map f (Quotient.mk'' a) = nil ↔ Quotient.mk'' a = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Cycle α
⊢ ∀ (a : List α), b ∈ map f (Quotient.mk'' a) ↔ ∃ a_1 ∈ Quotient.mk'' a, f a_1 = b

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑l.cyclicPermutations ↔ ↑l✝ = Quotient.mk'' l

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ x ∈ ↑(x :: y :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : ¬x = y
⊢ y ∈ ↑(x :: y :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x✝ : { s // s.Nodup }
hs✝ : List α
hs : Nodup (Quotient.mk'' hs✝)
⊢ (fun l ↦ ⟨↑↑l, ⋯⟩) ⟨hs✝, hs⟩ = ⟨Quotient.mk'' hs✝, hs⟩

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ∀ (x : Cycle α),
    x ∈ Finset.filter Nontrivial (Finset.map (Function.Embedding.subtype fun s ↦ s.Nodup) Finset.univ) ↔
      x.Nodup ∧ x.Nontrivial

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
⊢ ∀ (a : List α), toFinset (Quotient.mk'' a) = ∅ ↔ Quotient.mk'' a = nil

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
x : R
n : ℕ
_hn : 0 < n
hx : x ^ n = 0
⊢ ¬Prime 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
p : R
hp : Prime p
⊢ p ^ 1 = p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k = Nat.log 2 (2 ^ k)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inl
⊢ (∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ p, p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
· dsimp only
        obtain ⟨n, hn⟩ := hab
        induction n generalizing a b l m with
        | zero =>
          simp only [rotate_zero, cons.injEq] at hn
          rw [hn.1, hn.2]
        | succ d hd =>
          rcases l with - | ⟨c, s⟩
          · simp only [rotate_cons_succ, nil_append, rotate_singleton, cons.injEq] at hn
            rw [hn.1, hn.2]
          · rw [Nat.add_comm, ← rotate_rotate, rotate_cons_succ, rotate_zero, cons_append] at hn
            rw [← hd c _ _ _ hn]
            simp [and_comm]

Goal state after:
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
⊢ a ∈ ↑(a :: l)

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : Monoid X
inst✝¹ : MulAction X G
H : Subgroup G
inst✝ : QuotientAction X H
b : X
q : G ⧸ H
⊢ ↑(b • Quotient.out q) = b • q

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ (Quotient.out q)⁻¹ * g ^ minimalPeriod (fun x ↦ g • x) q * Quotient.out q ∈ H

Tactic:
by
  rw [mul_assoc, ← QuotientGroup.eq, QuotientGroup.out_eq', ← smul_eq_mul, Quotient.mk_smul_out,
    eq_comm, pow_smul_eq_iff_minimalPeriod_dvd]

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 0 → Prime p

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {p : ℕ}, p ∈ primeFactorsList 1 → Prime p

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k p : ℕ
h : p ∈ (k + 2).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : p = m ∨ p ∈ ((k + 2) / m).primeFactorsList
h₂ : p = m
⊢ k + 2 ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
inst✝³ : MulAction G X
b : X
inst✝² : Fintype G
inst✝¹ : Fintype ↑(orbit G b)
inst✝ : Fintype ↥(stabilizer G b)
⊢ Fintype.card ↑(orbit G b) * Fintype.card ↥(stabilizer G b) = Fintype.card G

Tactic:
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup G b)]

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ 0 ≠ 0 → (primeFactorsList 0).prod = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: ⊢ 1 ≠ 0 → (primeFactorsList 1).prod = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 0 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n : ℕ
⊢ ∀ {a : ℕ}, (∀ (p : ℕ), Prime p → p ∣ 1 → a ≤ p) → List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: primeFactorsList 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ ¬k + 2 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
H : Subgroup G
inst✝¹ : Finite (orbitRel.Quotient G X)
inst✝ : Finite (G ⧸ H)
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
rw [(equivSubgroupOrbits X H).finite_iff]
  infer_instance

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: a✝ : ℕ
⊢ a✝ ∈ primeFactors 0 ↔ a✝ ∈ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mpr.inl
⊢ primeFactors 0 = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mpr.inr
⊢ primeFactors 1 = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case inr.zero
n : ℕ
hn : n ≠ 0
⊢ (n ^ (0 + 1)).primeFactors = n.primeFactors

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case zero
a : ℕ
ha : Prime a
b : ℕ
hb : b ≠ 0
⊢ replicate 0 a <+~ b.primeFactorsList ↔ a ^ 0 ∣ b

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hb : b ∉ H
⊢ b * a ∈ H

pp: case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

pp: case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H

Tactic:
· exact inv_inv b ▸ ha.2 _ (mt (inv_mem_iff (x := b)).1 hb)

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
⊢ a ∉ H

case refine_4
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : ∀ (b : G), b * a ∈ H ↔ b ∉ H
b : G
hb : b ∉ H
⊢ b⁻¹ * a ∈ H
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: case zero
k : ℕ
⊢ ↑k = 0 ↔ 0 ∣ k

Tactic:
simp

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

Goal state before:
pp: p n q : ℕ
h : n ≤ n + q
⊢ ↑(p ^ n) * ↑p ^ q = 0

Tactic:
simp

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

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddGroupWithOne R
n✝ : ℕ
⊢ (match (motive := (x : ℕ) → ZMod x → R) n✝ + 1 with
      | 0 => Int.cast
      | n.succ => fun i ↦ ↑i.val)
      0 =
    0

Tactic:
simp

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

Goal state before:
pp: case zero
a b : ZMod 0
⊢ (a + b).cast = if ↑0 ≤ a.cast + b.cast then a.cast + b.cast - ↑0 else a.cast + b.cast

Tactic:
simp

Goal state after:
case zero
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast
Module: Mathlib.Data.ZMod.Basic

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ cast 1 = 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a + b).cast = a.cast + b.cast

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a * b).cast = a.cast * b.cast

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a b : ZMod n
⊢ (a - b).cast = a.cast - b.cast

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
a : ZMod n
k : ℕ
⊢ (a ^ k).cast = a.cast ^ k

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℕ
⊢ (↑k).cast = ↑k

Tactic:
simp

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

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (↑k).cast = ↑k

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index ≠ 0
a : G
⊢ ∃ n, 0 < n ∧ n ≤ H.index ∧ a ^ n ∈ H

Tactic:
by
  suffices ∃ n₁ n₂, n₁ < n₂ ∧ n₂ ≤ H.index ∧ ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hlt, hle, he⟩
    refine ⟨n₂ - n₁, by lia, by lia, ?_⟩
    rw [eq_comm, QuotientGroup.eq, ← zpow_natCast, ← zpow_natCast, ← zpow_neg, ← zpow_add,
        add_comm] at he
    rw [← zpow_natCast]
    convert! he
    lia
  suffices ∃ n₁ n₂, n₁ ≠ n₂ ∧ n₁ ≤ H.index ∧ n₂ ≤ H.index ∧
      ((a ^ n₂ : G) : G ⧸ H) = ((a ^ n₁ : G) : G ⧸ H) by
    rcases this with ⟨n₁, n₂, hne, hle₁, hle₂, he⟩
    rcases hne.lt_or_gt with hlt | hlt
    · exact ⟨n₁, n₂, hlt, hle₂, he⟩
    · exact ⟨n₂, n₁, hlt, hle₁, he.symm⟩
  by_contra hc
  simp_rw [not_exists] at hc
  let f : (Set.Icc 0 H.index) → G ⧸ H := fun n ↦ (a ^ (n : ℕ) : G)
  have hf : Function.Injective f := by
    rintro ⟨n₁, h₁, hle₁⟩ ⟨n₂, h₂, hle₂⟩ he
    have hc' := hc n₁ n₂
    dsimp only [f] at he
    simpa [hle₁, hle₂, he] using hc'
  have := (fintypeOfIndexNeZero h).finite
  have hcard := Nat.card_le_card_of_injective f hf
  simp [← index_eq_card] at hcard

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

Goal state before:
pp: case zero
⊢ ↑(-1) = 0

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
⊢ ↑(-1) = ↑0 - 1

Tactic:
simp

Goal state after: