mathlib-initiative/mathlib-tactics huggingface dataset:
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 • q = b • q

Tactic:
]

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
⊢ minimalPeriod (fun x ↦ g • x) q ∣ minimalPeriod (fun x ↦ g • x) q

Tactic:
]

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 : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b

Tactic:
]

Goal state after:
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝¹ : IsTrans α r
inst✝ : Std.Antisymm r
hs : ∀ a ∈ s, ∀ b ∈ s, r a b
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b
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:
]

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
⊢ g2 • x = g2 • x

Tactic:
]

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

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

Tactic:
]

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
⊢ g₁⁻¹ * g₂ ∈ stabilizer G x

Tactic:
]

Goal state after:
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
⊢ g₁⁻¹ * g₂ ∈ stabilizer G x
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
⊢ x = x

Tactic:
]

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

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

Tactic:
]

Goal state after:
n k p : ℕ
h : p ∈ (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ p ∈ m :: ((k + 2) / m).primeFactorsList
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 G = Fintype.card G

Tactic:
]

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

Tactic:
]

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
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))
⊢ Fintype.card (Quotient (orbitRel G X) × G) = Fintype.card (Quotient (orbitRel G X) × G)

Tactic:
]

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

Tactic:
rw [zero_mul] at this

Goal state after:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
Module: Mathlib.Data.Nat.Prime.Infinite

Goal state before:
pp: ⊢ ∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y

Tactic:
]

Goal state after:
⊢ ∀ (x : ℕ), ∃ y ∈ {p | Prime p}, x < y
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
⊢ k + 2 = k + 2

Tactic:
]

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

Goal state before:
pp: p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (p - 2 + 2).minFac :: ((p - 2 + 2) / (p - 2 + 2).minFac).primeFactorsList = [p - 2 + 2]
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₁ • b⟧ = ⟦g₂ • b⟧

Tactic:
]

Goal state after:
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₁ • b⟧ = ⟦g₂ • b⟧
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
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)

Tactic:
]

Goal state after:
n k a : ℕ
h : ∀ (p : ℕ), Prime p → p ∣ k + 2 → a ≤ p
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (a :: (k + 2).minFac :: ((k + 2) / (k + 2).minFac).primeFactorsList)
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 ω)
hx : Quotient.mk'' ↑x = ω
⊢ ⟦↑x⟧ = ω

Tactic:
]

Goal state after:
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 ω)
hx : Quotient.mk'' ↑x = ω
⊢ ⟦↑x⟧ = ω
Module: Mathlib.Data.Nat.Factors

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

Tactic:
]

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) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ ⟦↑x⟧ = ω

Tactic:
]

Goal state after:
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) ⁻¹' {ω} }
hx : ⟦↑x⟧ = ω
⊢ ⟦↑x⟧ = ω
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 : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧

Tactic:
]

Goal state after:
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 : ⟦↑a⟧ = ⟦↑b⟧
⊢ ⟦⟨↑a, ⋯⟩⟧ = ⟦⟨↑b, ⋯⟩⟧
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
]

Goal state after:
case mp.succ.succ
n : ℕ
h : (n + 2).minFac :: ((n + 2) / (n + 2).minFac).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
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 ((ω : Quotient (orbitRel G X)) × orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω))

Tactic:
]

Goal state after:
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 ((ω : Quotient (orbitRel G X)) × orbitRel.Quotient ↥H ↑(orbitRel.Quotient.orbit ω))
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₁ y₂ : X
h : (orbitRel (↥H) X) y₁ y₂
⊢ ↑⋯.choose = ↑⋯.choose

Tactic:
orbitRel_apply

Goal state after:
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₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ ↑⋯.choose = ↑⋯.choose
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₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ ↑⋯.choose = ↑⋯.choose

Tactic:
]

Goal state after:
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₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ ↑⋯.choose = ↑⋯.choose
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₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ (fun x y ↦ x⁻¹ * y ∈ H) ⋯.choose ⋯.choose

Tactic:
]

Goal state after:
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₁ y₂ : X
h : y₁ ∈ orbit (↥H) y₂
⊢ (fun x y ↦ x⁻¹ * y ∈ H) ⋯.choose ⋯.choose
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∈ n.primeFactorsList

Tactic:
]

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∈ n.primeFactorsList
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
⊢ x = (⋯.choose * ↑g⁻¹) • g • y₂

Tactic:
Subgroup.smul_def,

Goal state after:
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
⊢ x = (⋯.choose * ↑g⁻¹) • ↑g • y₂
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
⊢ x = x

Tactic:
]

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

Goal state before:
pp: case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0

Tactic:
]

Goal state after:
case inl
p : ℕ
h : p ∈ []
⊢ p ≤ 0
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
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧

Tactic:
]

Goal state after:
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
⊢ ⟦g₁⁻¹ • x⟧ = ⟦g₂⁻¹ • x⟧
Module: Mathlib.Data.Nat.Factors

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

Tactic:
]

Goal state after:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ n = n.primeFactorsList.prod
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
⊢ (orbitRel (↥H) X) (g₁⁻¹ • x) (g₂⁻¹ • x)

Tactic:
orbitRel_apply

Goal state after:
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
⊢ g₁⁻¹ • x ∈ orbit (↥H) (g₂⁻¹ • x)
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
⊢ g₁⁻¹ • x ∈ orbit (↥H) (g₂⁻¹ • x)

Tactic:
]

Goal state after:
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
⊢ g₁⁻¹ • x ∈ orbit (↥H) (g₂⁻¹ • x)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False

Tactic:
]

Goal state after:
case refine_1
l : List ℕ
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
h₁ : 0 ∈ l
⊢ False
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
a✝ : X
⊢ (orbitRel (↥H) X) (⋯.choose⁻¹ • x) a✝

Tactic:
orbitRel_apply

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
a✝ : X
⊢ ⋯.choose⁻¹ • x ∈ orbit (↥H) a✝
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
a✝ : X
⊢ ⋯.choose⁻¹ • x ∈ orbit (↥H) a✝

Tactic:
]

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
a✝ : X
⊢ ⋯.choose⁻¹ • x ∈ orbit (↥H) a✝
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case e'_5
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
a✝ : X
⊢ x = x

Tactic:
]

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

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
⊢ (fun x y ↦ x⁻¹ * y ∈ H) ⋯.choose g
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
⊢ g⁻¹ • x = g⁻¹ • x

Tactic:
]

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

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

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
⊢ replicate n p ~ (p ^ n).primeFactorsList
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 (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
]

Goal state after:
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 (ConjAct G) / Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime p

Tactic:
]

Goal state after:
p : ℕ
hp : Prime p
n q : ℕ
hq : q ∈ replicate n p
⊢ Prime p
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 ↑(MulAction.orbit (ConjAct G) g)

pp: case H
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)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)

Tactic:
]

Goal state after:
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 ↑(MulAction.orbit (ConjAct G) g)

case H
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)
⊢ 0 < Fintype.card ↥(MulAction.stabilizer (ConjAct G) g)
Module: Mathlib.Data.Nat.Factors

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

Tactic:
]

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

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b = a * b

Tactic:
]

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

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H

Tactic:
]

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ H.normalCore
q : G ⧸ H
g' : G
⊢ g'⁻¹ * g⁻¹ * g'⁻¹⁻¹ ∈ H
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p

Tactic:
]

Goal state after:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList
⊢ Prime p
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1

Tactic:
]

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hg : g ∈ (MulAction.toPermHom G (G ⧸ H)).ker
⊢ ↑(g * 1) = ↑1
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: n : ℕ
⊢ n = 0 ∨ n = 1 ↔ n = 0 ∨ n = 1

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod

Tactic:
]

Goal state after:
case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = (a + 1 + 1).primeFactorsList.prod * (b.primeFactorsList.diff a.succ.succ.primeFactorsList).prod
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ n.primeFactors = n.primeFactors

Tactic:
]

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

Goal state before:
pp: case h
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ b = b

Tactic:
]

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

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ (∃ l, l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b

Tactic:
]

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
⊢ (∃ l, l ~ b.primeFactorsList ∧ replicate (n + 1) a <+ l) → a ^ (n + 1) ∣ b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod

Tactic:
]

Goal state after:
case succ.mp
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
b : ℕ
hb : b ≠ 0
u : List ℕ
hu1 : u ~ b.primeFactorsList
hu2 : replicate (n + 1) a <+ u
⊢ (replicate (n + 1) a).prod ∣ u.prod
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList

Tactic:
]

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ replicate (n + 1) a <+~ (a ^ (n + 1) * c).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c

Tactic:
]

Goal state after:
case succ.mpr
a : ℕ
ha : Prime a
n : ℕ
ih : ∀ {b : ℕ}, b ≠ 0 → (replicate n a <+~ b.primeFactorsList ↔ a ^ n ∣ b)
c : ℕ
hb : ¬a = 0 ∧ ¬a ^ n * c = 0
⊢ a ^ n ∣ a ^ n * c
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)

Tactic:
]

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ Prime p ∧ p ∣ a * b ↔ Prime p ∧ (p ∣ a ∨ p ∣ b)
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q

Tactic:
]

Goal state after:
a b : ℕ
hab : a.Coprime b
q : ℕ
hqa : q ∈ a.primeFactorsList
hqb : q ∈ b.primeFactorsList
⊢ Prime q
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList ↔ p ∈ a.primeFactorsList ∨ p ∈ b.primeFactorsList

Tactic:
]

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

Goal state before:
pp: p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Tactic:
]

Goal state after:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
x y : G'
⊢ (f x)⁻¹ * f y = (f x)⁻¹ * f y

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
K : Subgroup G'
⊢ H.relIndex (map f K) = H.relIndex (map f K)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
hf : Injective ⇑f
⊢ H.relIndex K = H.relIndex K

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
H K : Subgroup G
⊢ (map f H).relIndex (map f K) = (map f H).relIndex (map f K)

Tactic:
]

Goal state after: