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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'

Tactic:
rw [heq_iff_eq] at hxy

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x = y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
l₁ l₂ : List α
h : (IsRotated.setoid α) l₁ l₂
h₁ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₁)
h₂ : Nodup (Quot.mk (⇑(IsRotated.setoid α)) l₂)
_he : h₁ ≍ h₂
x y : α
hxy : x ≍ y
hm : x ∈ Quot.mk (⇑(IsRotated.setoid α)) l₁
hm' : y ∈ Quot.mk (⇑(IsRotated.setoid α)) l₂
he' : hm ≍ hm'
⊢ l₁.prev x hm = l₂.prev y hm'

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.reverse.next ⋯ x ⋯ = s.prev hs x hx

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.reverse.Nodup
x : α
hx : x ∈ s.reverse
⊢ s.reverse.next hs x hx = s.prev ⋯ x ⋯

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.next hs x hx ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
x : α
hx : x ∈ s
⊢ s.prev hs x hx ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
x✝ : ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
p : R
k : ℕ
hp : Prime p
hk : 0 < k
hn : p ^ k = n
⊢ p ^ (k - 1 + 1) = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoidWithZero R
inst✝ : IsReduced R
⊢ ¬IsPrimePow 0

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
n : R
hn✝ : IsPrimePow n
k : ℕ
hk : k ≠ 0
p : R
k' : ℕ
hp : Prime p
hk' : 0 < k'
hn : p ^ k' = n
⊢ p ^ (k * k') = n ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ p, p ≤ n ∧ ∃ k, k ≤ n ∧ Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n : ℕ
⊢ IsPrimePow n ↔ ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: n m : ℕ
hn : IsPrimePow n
hm : m ∣ n
hm₁ : m ≠ 1
⊢ IsPrimePow m

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod ↔ ∃ a, a ∈ L ∧ p ∣ a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
p : M
hp : Prime p
L : List M
hL : ∀ (q : M), q ∈ L → Prime q
hpL : p ∣ L.prod
⊢ p ∈ L

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ Chain r Cycle.nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ Chain r ↑[a] ↔ r a a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
⊢ a ∣ (a :: l₁).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
hl₁' : ∀ (p : M), p ∈ l₁ → Prime p
hl₂' : ∀ (p : M), p ∈ (b :: l₂).erase a → Prime p
ha : a ∈ b :: l₂
hb : b :: l₂ ~ a :: (b :: l₂).erase a
⊢ a * l₁.prod = a * ((b :: l₂).erase a).prod

Tactic:
by

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : IsCancelMulZero M
inst✝ : Subsingleton Mˣ
a : M
l₁ : List M
b : M
l₂ : List M
h : (a :: l₁).prod = (b :: l₂).prod
hl₁ : ∀ (p : M), p ∈ a :: l₁ → Prime p
hl₂ : ∀ (p : M), p ∈ b :: l₂ → Prime p
⊢ a :: l₁ ~ b :: l₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
l : List α
⊢ ∀ (l : List α) (a : α),
    (∀ (hl : l ≠ []), Chain r ↑l ↔ IsChain r (l.getLast hl :: l)) →
      ∀ (hl : l ++ [a] ≠ []), Chain r ↑(l ++ [a]) ↔ IsChain r ((l ++ [a]).getLast hl :: (l ++ [a]))

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
l : List β
⊢ Chain r (map f ⟦l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦l⟧

Tactic:
by

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ Chain r ↑(range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ s
⊢ Chain r₂ s

Tactic:
by

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:
by

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
Ha : a ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ b ∈ ↑(a :: l)

Tactic:
by

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
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l ++ [a]
⊢ r a b

Tactic:
by

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
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c ∈ [a]
⊢ r b c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
⊢ (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s

Tactic:
by

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
x✝³ x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
by

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
b : ↥(normalizer ↑H).op
c x✝¹ : G
x✝ : c⁻¹ * x✝¹ ∈ H
⊢ (b • c)⁻¹ * b • x✝¹ ∈ H

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
⊢ Chain r s → ∀ a ∈ s, ∀ b ∈ s, r a b

Tactic:
by

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
hH : H.Normal
x✝³ : Gᵐᵒᵖ
x✝² x✝¹ : G
x✝ : x✝²⁻¹ * x✝¹ ∈ H
⊢ (x✝³ • x✝²)⁻¹ * x✝³ • x✝¹ ∈ H

Tactic:
by

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:
by

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

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
h : Chain r s
⊢ s = Cycle.nil

Tactic:
by

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : Chain r s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
by

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

Goal state before:
pp: G : Type u
X : Type v
inst✝⁴ : Group G
H : Subgroup G
inst✝³ : H.Normal
inst✝² : SMul G X
inst✝¹ : MulAction (G ⧸ H) X
inst✝ : IsScalarTower G (G ⧸ H) X
g : G
x : X
⊢ ↑g • x = g • x

Tactic:
by

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
g : G ⧸ stabilizer G x
g1 g2 : G
H : (leftRel (stabilizer G x)) g1 g2
⊢ g1 • (g1⁻¹ * g2) • x = g2 • x

Tactic:
by

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

Goal state before:
pp: ⊢ primeFactorsList 0 = []

Tactic:
by

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

Goal state before:
pp: ⊢ primeFactorsList 1 = []

Tactic:
by

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

Goal state before:
pp: ⊢ primeFactorsList 2 = [2]

Tactic:
by

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
y₁ y₂ : G ⧸ stabilizer G x
g₁ g₂ : G
H : g₁ • x = g₂ • x
⊢ (leftRel (stabilizer G x)) g₁ g₂

Tactic:
by

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✝ b : X
x y : G ⧸ stabilizer G b
hxy : (fun g ↦ ⟨ofQuotientStabilizer G b g, ⋯⟩) x = (fun g ↦ ⟨ofQuotientStabilizer G b g, ⋯⟩) y
⊢ ofQuotientStabilizer G b x = ofQuotientStabilizer G b y

Tactic:
by

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
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList

Tactic:
by

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:
by

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:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ stabilizer G ↑1 = H

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
inst✝² : Fintype G
inst✝¹ : (g : G) → Fintype ↑(fixedBy X g)
inst✝ : Fintype (Quotient (orbitRel G X))
⊢ ∑ g, Fintype.card ↑(fixedBy X g) = Fintype.card (Quotient (orbitRel G X)) * Fintype.card G

Tactic:
by

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
⊢ False

Tactic:
by

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
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ∀ (x y : G ⧸ H), ∃ g, g • x = y

Tactic:
by

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

Goal state before:
pp: ⊢ ¬BddAbove {p | Prime p}

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
⊢ p.primeFactorsList = [p]

Tactic:
by

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
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : g₁ * g₂⁻¹ ∈ H
⊢ ⟨g₁ * g₂⁻¹, r⟩ • g₂ • b = g₁ • b

Tactic:
by

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
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
b : X
h' : Finite (Quotient (rightRel H))
a : Quotient (rightRel H)
g₁ g₂ : G
r : (rightRel H) g₁ g₂
⊢ ⟦g₁ • b⟧ = ⟦g₂ • b⟧

Tactic:
by

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
inst✝¹ : IsPretransitive G X
H : Subgroup G
inst✝ : Finite (G ⧸ H)
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
by

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:
by

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
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
x : ↑(orbitRel.Quotient.orbit ω)
⊢ ↑x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω}

Tactic:
by

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

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

Tactic:
by

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
ω : Quotient (orbitRel G X)
q : orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω)
a b : ↑(orbitRel.Quotient.orbit ω)
h : (orbitRel ↥H ↑(orbitRel.Quotient.orbit ω)) a b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ (n + 2).primeFactorsList = (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList

Tactic:
by

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
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
x : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
⊢ ↑x ∈ orbitRel.Quotient.orbit ω

Tactic:
by

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
ω : Quotient (orbitRel G X)
q : Quotient (Setoid.comap Subtype.val (orbitRel (↥H) X))
a b : { x // x ∈ Quotient.mk (orbitRel G X) ⁻¹' {ω} }
h : (Setoid.comap Subtype.val (orbitRel (↥H) X)) a b
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
by

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
ω : Quotient (orbitRel G X)
⊢ LeftInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
simp only [LeftInverse]
    intro q
    induction q using Quotient.inductionOn'
    rfl

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
ω : Quotient (orbitRel G X)
⊢ LeftInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
by

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
ω : Quotient (orbitRel G X)
⊢ RightInverse (fun q ↦ q.liftOn' (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯) fun q ↦ Quotient.liftOn' q (fun x ↦ ⟦⟨↑x, ⋯⟩⟧) ⋯

Tactic:
by

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:
by

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

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList = [] ↔ n = 0 ∨ n = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ n.primeFactorsList ≠ [] ↔ 1 < n

Tactic:
by

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

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
h : a.primeFactorsList ~ b.primeFactorsList
⊢ a = b

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
y₂ : X
g : ↥H
this : ⋯.choose = ⋯.choose * ↑g⁻¹
⊢ ⋯.choose⁻¹ * ⋯.choose ∈ H

Tactic:
by

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

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ∣ n

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactorsList ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : orbitRel.Quotient (↥H) X
⊢ ∀ (a b : X), (orbitRel (↥H) X) a b → ↑⋯.choose = ↑⋯.choose

Tactic:
by

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

Goal state before:
pp: n p : ℕ
h : p ∈ n.primeFactorsList
⊢ p ≤ n

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
g₁ g₂ : G
h : g₁⁻¹ * g₂ ∈ H
⊢ (fun m ↦ m • g₂⁻¹ • x) ⟨g₁⁻¹ * g₂, h⟩ = g₁⁻¹ • x

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
q : G ⧸ H
⊢ ∀ (a b : G), (leftRel H) a b → ⟦a⁻¹ • x⟧ = ⟦b⁻¹ • x⟧

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
y : orbitRel.Quotient (↥H) X
⊢ (fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) ((fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) y) = y

Tactic:
by

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

Goal state before:
pp: case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ (fun x y ↦ x⁻¹ * y ∈ H) ⋯.choose g

Tactic:
simp only

Goal state after:
case h
G : Type u
X : Type v
inst✝³ : Group G
inst✝² : MulAction G X
x : X
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G
⊢ ⋯.choose⁻¹ * g ∈ H
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hn : n ≠ 0
⊢ p ∈ n.primeFactors ↔ Prime p ∧ p ∣ n

Tactic:
by

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

Goal state before:
pp: n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l ~ n.primeFactorsList

Tactic:
by

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
inst✝¹ : IsPretransitive G X
inst✝ : IsCancelSMul G X
H : Subgroup G
g : G ⧸ H
⊢ (fun q ↦ Quotient.liftOn' q (fun y ↦ ↑⋯.choose) ⋯) ((fun q ↦ Quotient.liftOn' q (fun g ↦ ⟦g⁻¹ • x⟧) ⋯) g) = g

Tactic:
by

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

Goal state before:
pp: m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ m.primeFactors ⊆ n.primeFactors

Tactic:
by

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

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primeFactors ↔ p ∈ n.primeFactorsList

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ (p ^ n).primeFactorsList = replicate n p

Tactic:
by

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
⊢ (p ^ n).primeFactorsList = replicate n p

Tactic:
by
  symm
  rw [← List.replicate_perm]
  apply Nat.primeFactorsList_unique (List.prod_replicate n p)
  intro q hq
  rwa [eq_of_mem_replicate hq]

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

Goal state before:
pp: ⊢ primeFactors 0 = ∅

Tactic:
by

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

Goal state before:
pp: ⊢ primeFactors 1 = ∅

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
g : G
inst✝¹ : Fintype ↑(ConjClasses.mk g).carrier
inst✝ : Fintype ↥(MulAction.stabilizer (ConjAct G) g)
⊢ Fintype.card ↑(ConjClasses.mk g).carrier = Fintype.card G / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
by

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

Goal state before:
pp: n p : ℕ
hpos : n ≠ 0
h : ∀ {d : ℕ}, Prime d → d ∣ n → d = p
⊢ n = p ^ n.primeFactorsList.length

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker

Tactic:
by

Goal state after: