internlm/Lean-Github huggingface dataset:
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s + 1 = ↑(Nat.succ 0 + m)
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Tactic:
rw [add_comm _ m, Nat.cast_add, ← Nat.cast_one, WithTop.add_eq_add_iff] at hs
Proof state after:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Tactic:
have : Finite s := by rw [Set.finite_coe_iff]; exact Set.finite_of_encard_eq_coe hs
Proof state after:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) 2
Tactic:
apply remaining_transitivity M α s h
Proof state after:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + Set.ncard s
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + Set.ncard s
Tactic:
unfold Set.ncard
Proof state after:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + ENat.toNat (Set.encard s)
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inr.right.intro.h2
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
this : Finite ↑s
⊢ Nat.succ n = 2 + ENat.toNat (Set.encard s)
Tactic:
rw [hs, hm, ENat.toNat_coe, ← Nat.succ_add]
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n = 0
⊢ IsMultiplyPreprimitive M α n
Tactic:
rw [hn]
Proof state after:
case inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
case inl
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0
Tactic:
apply isMultiplyPreprimitive_zero
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ Finite ↑s
Tactic:
rw [Set.finite_coe_iff]
Proof state after:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ Set.Finite s
Theorem: MulAction.isMultiplyPreprimitive_of_multiply_pretransitive_succ
Proof state before:
M : Type u_2
α : Type u_1
inst✝¹ : Group M
inst✝ : MulAction M α
n : ℕ
hα : ↑(Nat.succ n) ≤ PartENat.card α
h : IsMultiplyPretransitive M α (Nat.succ n)
hn : n > 0
m : ℕ
hm : n = Nat.succ 0 + m
s : Set α
hs : Set.encard s = ↑m
⊢ Set.Finite s
Tactic:
exact Set.finite_of_encard_eq_coe hs
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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]
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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'
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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]
Proof 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)
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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')
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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α
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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]
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof 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
Theorem: MulAction.isMultiplyPreprimitive_of_higher
Proof 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
Proof state after:
no goals
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive N β n
Tactic:
constructor
Proof state after:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive N β n

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case left
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive N β n

case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Tactic:
apply isMultiplyPretransitive_of_surjective_map hf.surjective h.left
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s : Set β), Set.encard s + 1 = ↑n → IsPreprimitive ↥(fixingSubgroup N s) ↥(SubMulAction.ofFixingSubgroup N s)
Tactic:
intro t ht
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let s := f ⁻¹' t
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
have hs' : f '' s = t := Set.image_preimage_eq t hf.surjective
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let φ' : fixingSubgroup M s → fixingSubgroup N t := fun ⟨m, hm⟩ =>
  ⟨φ m, fun ⟨y, hy⟩ => by
    rw [← hs', Set.mem_image_iff_bex] at hy
    obtain ⟨x, hx, hx'⟩ := hy
    simp only [Subtype.coe_mk]
    rw [← hx', ← map_smulₛₗ]
    apply congr_arg
    rw [mem_fixingSubgroup_iff] at hm
    exact hm x hx⟩
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Theorem: MulAction.isMultiplyPreprimitive_of_bijective_map
Proof state before:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)
Tactic:
let f' : SubMulAction.ofFixingSubgroup M s →ₑ[φ'] SubMulAction.ofFixingSubgroup N t :=
  { toFun := fun ⟨x, hx⟩ => ⟨f.toFun x, fun h => hx (Set.mem_preimage.mp h)⟩
    map_smul' := fun ⟨m, hm⟩ ⟨x, hx⟩ =>
      by
      rw [← SetLike.coe_eq_coe]
      exact f.map_smul' m x }
Proof state after:
case right
M : Type u_4
α : Type u_3
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_1
β : Type u_2
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : Set.encard t + 1 = ↑n
s : Set α := ⇑f ⁻¹' t
hs' : ⇑f '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x =>
    match x with
    | { val := m, property := hm } => { val := φ m, property := ⋯ }
f' : ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[φ'] ↥(SubMulAction.ofFixingSubgroup N t) :=
  {
    toFun := fun x =>
      match x with
      | { val := x, property := hx } => { val := f.toFun x, property := ⋯ },
    map_smul' := ⋯ }
⊢ IsPreprimitive ↥(fixingSubgroup N t) ↥(SubMulAction.ofFixingSubgroup N t)