Theorem: MulAction.isMultiplyPreprimitive_of_higher (Jordan/MultiplePrimitivity.lean)

State before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n m : ℕ
hmn : m ≤ n
hα : ↑n ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive M α m
Tactic:
induction' n with n hrec
State after:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hmn : m ≤ Nat.zero
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
⊢ IsMultiplyPreprimitive M α m

case succ
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
⊢ IsMultiplyPreprimitive M α m

State before:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hmn : m ≤ Nat.zero
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
⊢ IsMultiplyPreprimitive M α m
Tactic:
simp only [Nat.zero_eq, nonpos_iff_eq_zero] at hmn
State after:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
hmn : m = 0
⊢ IsMultiplyPreprimitive M α m

State before:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
hmn : m = 0
⊢ IsMultiplyPreprimitive M α m
Tactic:
rw [hmn]
State after:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
hmn : m = 0
⊢ IsMultiplyPreprimitive M α 0

State before:
case zero
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m : ℕ
hα : ↑Nat.zero ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α Nat.zero
hmn : m = 0
⊢ IsMultiplyPreprimitive M α 0
Tactic:
apply isMultiplyPreprimitive_zero
State after:
no goals

State before:
case succ
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
⊢ IsMultiplyPreprimitive M α m
Tactic:
cases' Nat.eq_or_lt_of_le hmn with hmn hmn'
State after:
case succ.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn✝ : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn : m = Nat.succ n
⊢ IsMultiplyPreprimitive M α m

case succ.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α m

State before:
case succ.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn✝ : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn : m = Nat.succ n
⊢ IsMultiplyPreprimitive M α m
Tactic:
rw [hmn]
State after:
case succ.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn✝ : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn : m = Nat.succ n
⊢ IsMultiplyPreprimitive M α (Nat.succ n)

State before:
case succ.inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn✝ : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn : m = Nat.succ n
⊢ IsMultiplyPreprimitive M α (Nat.succ n)
Tactic:
exact hn
State after:
no goals

State before:
case succ.inr
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α m
Tactic:
apply hrec (Nat.lt_succ_iff.mp hmn')
State after:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ ↑n ≤ PartENat.card α

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n

State before:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ ↑n ≤ PartENat.card α

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n
Tactic:
refine' le_trans _ hα
State after:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ ↑n ≤ ↑(Nat.succ n)

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n

State before:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ ↑n ≤ ↑(Nat.succ n)

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n
Tactic:
rw [PartENat.coe_le_coe]
State after:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ n ≤ Nat.succ n

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n

State before:
case succ.inr.hα
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ n ≤ Nat.succ n

case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n
Tactic:
exact Nat.le_succ n
State after:
case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n

State before:
case succ.inr.hn
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
m n : ℕ
hrec : m ≤ n → ↑n ≤ PartENat.card α → IsMultiplyPreprimitive M α n → IsMultiplyPreprimitive M α m
hmn : m ≤ Nat.succ n
hα : ↑(Nat.succ n) ≤ PartENat.card α
hn : IsMultiplyPreprimitive M α (Nat.succ n)
hmn' : m < Nat.succ n
⊢ IsMultiplyPreprimitive M α n
Tactic:
apply isMultiplyPreprimitive_of_multiply_pretransitive_succ M α hα hn.left
State after:
no goals