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

Goal state before:
pp: case cons.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c

pp: case cons.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

pp: case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
·

Goal state after:
case cons.inl.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r c c
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c

pp: case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
·

Goal state after:
case cons.inl.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = b → r b a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a b
hc : c ∈ l
⊢ r b c
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c

pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
·

Goal state after:
case cons.inr.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hb : b ∈ l
hs : (∀ (a' : α), a' ∈ l ∨ a' = c → r c a') ∧ List.Pairwise r l ∧ ∀ a ∈ l, r a c
⊢ r b c
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c

Tactic:
·

Goal state after:
case cons.inr.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
inst✝ : IsTrans α r
a : α
l : List α
a✝ : Chain r ↑l → ∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b
b c : α
hs : (∀ (a' : α), a' ∈ l ∨ a' = a → r a a') ∧ List.Pairwise r l ∧ ∀ a_1 ∈ l, r a_1 a
hb : b ∈ l
hc : c ∈ l
⊢ r b c
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case inl
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)
he : IsEmpty X
⊢ Finite (orbitRel.Quotient (↥H) X)

pp: case inr
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
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
·

Goal state after:
case inl
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)
he : IsEmpty X
⊢ Finite (orbitRel.Quotient (↥H) X)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
pp: case inr
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
⊢ Finite (orbitRel.Quotient (↥H) X)

Tactic:
·

Goal state after:
case inr
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
⊢ Finite (orbitRel.Quotient (↥H) X)
Module: Mathlib.Data.Nat.Factors

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

pp: case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []

Tactic:
·

Goal state after:
case mp
n : ℕ
h : n.primeFactorsList = []
⊢ n = 0 ∨ n = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.zero
h : primeFactorsList 0 = []
⊢ 0 = 0 ∨ 0 = 1

pp: case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
·

Goal state after:
case mp.zero
h : primeFactorsList 0 = []
⊢ 0 = 0 ∨ 0 = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1

pp: case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1

Tactic:
·

Goal state after:
case mp.succ.zero
h : (0 + 1).primeFactorsList = []
⊢ 0 + 1 = 0 ∨ 0 + 1 = 1
Module: Mathlib.Data.Nat.Factors

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

Tactic:
·

Goal state after:
case mp.succ.succ
n : ℕ
h : (n + 1 + 1).primeFactorsList = []
⊢ n + 1 + 1 = 0 ∨ n + 1 + 1 = 1
Module: Mathlib.Data.Nat.Factors

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

Tactic:
·

Goal state after:
case mpr
n : ℕ
h : n = 0 ∨ n = 1
⊢ n.primeFactorsList = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mpr.inl
⊢ primeFactorsList 0 = []

pp: case mpr.inr
⊢ primeFactorsList 1 = []

Tactic:
·

Goal state after:
case mpr.inl
⊢ primeFactorsList 0 = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case mpr.inr
⊢ primeFactorsList 1 = []

Tactic:
·

Goal state after:
case mpr.inr
⊢ primeFactorsList 1 = []
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0

pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n

Tactic:
·

Goal state after:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ∣ 0
Module: Mathlib.Data.Nat.Factors

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

Tactic:
·

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ∣ n
Module: Mathlib.Data.Nat.Factors

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

pp: case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n

Tactic:
·

Goal state after:
case inl
p : ℕ
h : p ∈ primeFactorsList 0
⊢ p ≤ 0
Module: Mathlib.Data.Nat.Factors

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

Tactic:
·

Goal state after:
case inr
n p : ℕ
h : p ∈ n.primeFactorsList
hn : n > 0
⊢ p ≤ n
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
⊢ l.prod = n.primeFactorsList.prod

pp: case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p

pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
·

Goal state after:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ l.prod = n.primeFactorsList.prod
Module: Mathlib.Data.Nat.Factors

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

pp: case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.Prime p

Tactic:
·

Goal state after:
case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ l → _root_.Prime p
Module: Mathlib.Data.Nat.Factors

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

Tactic:
·

Goal state after:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ (p : ℕ), p ∈ l → Prime p
⊢ ∀ (p : ℕ), p ∈ n.primeFactorsList → _root_.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)
Module: Mathlib.GroupTheory.GroupAction.Quotient

Goal state before:
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:
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.GroupTheory.GroupAction.Quotient

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

pp: case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1

pp: case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ n.primeFactors = ∅ → n = 0 ∨ n = 1
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b

pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p

Tactic:
·

Goal state after:
case refine_1
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.primeFactorsList ++ b.primeFactorsList).prod = a * b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ b.primeFactorsList → Prime p

Tactic:
·

Goal state after:
case refine_2
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ (p : ℕ), p ∈ a.primeFactorsList ++ 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
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ n = 0 ∨ n = 1 → n.primeFactors = ∅
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList

pp: case inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
·

Goal state after:
case inl
b : ℕ
hab : Coprime 0 b
⊢ (0 * b).primeFactorsList ~ primeFactorsList 0 ++ b.primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inl
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0

pp: case inr.inr
a b : ℕ
hab : a.Coprime b
ha : a > 0
hb : b > 0
⊢ (a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList

Tactic:
·

Goal state after:
case inr.inl
a : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ (a * 0).primeFactorsList ~ a.primeFactorsList ++ primeFactorsList 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList

pp: case succ
k : ℕ
h : k ≠ 0
hn : ℕ
⊢ (hn + 1).primeFactorsList <+ ((hn + 1) * k).primeFactorsList

Tactic:
·

Goal state after:
case zero
k : ℕ
h : k ≠ 0
⊢ primeFactorsList 0 <+ (0 * k).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0

pp: case inr
a b : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ b.primeFactorsList
hb : b > 0
⊢ a ∣ b

Tactic:
·

Goal state after:
case inl
a : ℕ
ha : a ≠ 0
h : a.primeFactorsList <+~ primeFactorsList 0
⊢ a ∣ 0
Module: Mathlib.Data.Nat.PrimeFin

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

pp: case inr
n k : ℕ
hn : n ≠ 0
⊢ (n ^ (k + 1)).primeFactors = n.primeFactors

Tactic:
·

Goal state after:
case inl
k : ℕ
⊢ (0 ^ (k + 1)).primeFactors = primeFactors 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b

pp: case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

pp: case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Tactic:
·

Goal state after:
case inr.zero
b : ℕ
hb : b > 0
ha : 0 ≠ 0
h : primeFactorsList 0 <+~ b.primeFactorsList
⊢ 0 ∣ b
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b

pp: case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : a + 1 + 1 ≠ 0
h : (a + 1 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ a + 1 + 1 ∣ b

Tactic:
·

Goal state after:
case inr.succ.zero
b : ℕ
hb : b > 0
ha : 0 + 1 ≠ 0
h : (0 + 1).primeFactorsList <+~ b.primeFactorsList
⊢ 0 + 1 ∣ b
Module: Mathlib.Data.Nat.PrimeFin

Goal state before:
pp: case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors

pp: case succ
n n✝ : ℕ
hk : n✝ + 1 ≠ 0
⊢ (n ^ (n✝ + 1)).primeFactors = n.primeFactors

Tactic:
·

Goal state after:
case zero
n : ℕ
hk : 0 ≠ 0
⊢ (n ^ 0).primeFactors = n.primeFactors
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
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b

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

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
⊢ replicate (n + 1) a <+~ b.primeFactorsList → a ^ (n + 1) ∣ b
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)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.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)
b : ℕ
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) a <+~ b.primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList

pp: case inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
·

Goal state after:
case inl
b p : ℕ
hab : Coprime 0 b
⊢ p ∈ (0 * b).primeFactorsList ↔ p ∈ primeFactorsList 0 ∪ b.primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr.inl
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0

pp: case inr.inr
a b : ℕ
hab : a.Coprime b
p : ℕ
ha : a > 0
hb : b > 0
⊢ p ∈ (a * b).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ b.primeFactorsList

Tactic:
·

Goal state after:
case inr.inl
a p : ℕ
ha : a > 0
hab : a.Coprime 0
⊢ p ∈ (a * 0).primeFactorsList ↔ p ∈ a.primeFactorsList ∪ primeFactorsList 0
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList

pp: case inr
p a b : ℕ
hpa : p ∈ a.primeFactorsList
hb : b ≠ 0
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
·

Goal state after:
case inl
p b : ℕ
hb : b ≠ 0
hpa : p ∈ primeFactorsList 0
⊢ p ∈ (0 * b).primeFactorsList
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p

pp: case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

pp: case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
·

Goal state after:
case inl.zero
n2 : 2 < 2 ^ 0
⊢ 4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p

pp: case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
·

Goal state after:
case inl.succ.zero
n2 : 2 < 2 ^ (0 + 1)
⊢ 4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p

pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
·

Goal state after:
case inl.succ.succ
k : ℕ
n2 : 2 < 2 ^ (k + 1 + 1)
⊢ 4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p
Module: Mathlib.Data.Nat.Factors

Goal state before:
pp: case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p

Tactic:
·

Goal state after:
case inr
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ 4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Injective (Quotient.map' ⇑f ⋯)

pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Injective (Quotient.map' ⇑f ⋯)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H : Subgroup G
f : G' →* G
hf : Surjective ⇑f
key : ∀ (x y : G'), (QuotientGroup.leftRel (comap f H)) x y ↔ (QuotientGroup.leftRel H) (f x) (f y)
⊢ Surjective (Quotient.map' ⇑f ⋯)
Module: Mathlib.GroupTheory.Index

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

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

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
ha : a ∉ H ∧ ∀ x ∉ H, x⁻¹ * a ∈ H
b : G
hba : b * a ∈ H
hb : b ∈ H
⊢ False
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:
·

Goal state after:
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
Module: Mathlib.GroupTheory.Index

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

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
Module: Mathlib.GroupTheory.Index

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

Goal state after:
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.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
Module: Mathlib.GroupTheory.Index

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∉ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
h : H.index = 2
a b : G
ha : a ∉ H
hb : b ∈ H
⊢ a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)