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

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α ↔ IsMultiplyPreprimitive M α 1
Tactic:
constructor
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1

case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 → IsPreprimitive M α

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1
Tactic:
intro h
State after:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1

State before:
case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1
Tactic:
constructor
State after:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1

case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1
Tactic:
rw [← isPretransitive_iff_is_one_pretransitive]
State after:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsPretransitive M α

State before:
case mp.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsPretransitive M α
Tactic:
exact h.toIsPretransitive
State after:
no goals

State before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
intro s hs
State after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = ↑1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = ↑1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
simp only [Nat.cast_one] at hs
State after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)

State before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
suffices s = ∅ by
  rw [this]
  rw [isPreprimitive_of_bijective_map_iff
    (SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective M α)
    (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α)]
  exact h
State after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ s = ∅

State before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ s = ∅
Tactic:
rw [← Set.encard_eq_zero, ← Nat.cast_zero, ← WithTop.add_one_eq_coe_succ_iff]
State after:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ Set.encard s + 1 = ↑(Nat.succ 0)

State before:
case mp.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
⊢ Set.encard s + 1 = ↑(Nat.succ 0)
Tactic:
exact hs
State after:
no goals

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
Tactic:
rw [this]
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Tactic:
rw [isPreprimitive_of_bijective_map_iff
  (SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective M α)
  (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α)]
State after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive M α

State before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
s : Set α
hs : Set.encard s + 1 = 1
this : s = ∅
⊢ IsPreprimitive M α
Tactic:
exact h
State after:
no goals

State before:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
Tactic:
rintro ⟨_, h1'⟩
State after:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive M α

State before:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive M α
Tactic:
apply isPreprimitive_of_surjective_map
  (Function.Bijective.surjective
      (SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective M α))
State after:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)

State before:
case mpr.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ IsPreprimitive ↥(fixingSubgroup M ∅) ↥(SubMulAction.ofFixingSubgroup M ∅)
Tactic:
apply h1'
State after:
case mpr.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ Set.encard ∅ + 1 = ↑1

State before:
case mpr.intro.x
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
left✝ : IsMultiplyPretransitive M α 1
h1' : ∀ (s : Set α), Set.encard s + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(SubMulAction.ofFixingSubgroup M s)
⊢ Set.encard ∅ + 1 = ↑1
Tactic:
simp only [Set.encard_empty, zero_add, Nat.cast_one]
State after:
no goals