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

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
constructor
State after:
case left
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m

case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s_1 : Set ↥(SubMulAction.ofFixingSubgroup M s)),
    Set.encard s_1 + 1 = ↑m →
      IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) s_1)
        ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) s_1)

State before:
case left
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive (↥(fixingSubgroup M s)) (↥(SubMulAction.ofFixingSubgroup M s)) m
Tactic:
apply remaining_transitivity M α s h.left hs
State after:
no goals

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
⊢ ∀ (s_1 : Set ↥(SubMulAction.ofFixingSubgroup M s)),
    Set.encard s_1 + 1 = ↑m →
      IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) s_1)
        ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) s_1)
Tactic:
intro t ht
State after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
let t' : Set α := Subtype.val '' t
State after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
have htt' : t = Subtype.val ⁻¹' t' := by
  apply symm
  apply Set.preimage_image_eq
  exact Subtype.coe_injective
State after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) t)
Tactic:
rw [htt']
State after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
    ↥(SubMulAction.ofFixingSubgroup (↥(fixingSubgroup M s)) (Subtype.val ⁻¹' t'))
Tactic:
apply isPreprimitive_of_surjective_map
    (SubMulAction.OfFixingSubgroupUnion.map_bijective M s t').surjective
State after:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∪ t')) ↥(SubMulAction.ofFixingSubgroup M (s ∪ t'))

State before:
case right
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ IsPreprimitive ↥(fixingSubgroup M (s ∪ t')) ↥(SubMulAction.ofFixingSubgroup M (s ∪ t'))
Tactic:
apply h.right
State after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard (s ∪ t') + 1 = ↑n

State before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard (s ∪ t') + 1 = ↑n
Tactic:
rw [Set.encard_union_eq _]
State after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard s + Set.encard t' + 1 = ↑n

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Disjoint s t'

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ t = Subtype.val ⁻¹' t'
Tactic:
apply symm
State after:
case a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Subtype.val ⁻¹' t' = t

State before:
case a
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Subtype.val ⁻¹' t' = t
Tactic:
apply Set.preimage_image_eq
State after:
case a.h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Function.Injective Subtype.val

State before:
case a.h
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
⊢ Function.Injective Subtype.val
Tactic:
exact Subtype.coe_injective
State after:
no goals

State before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.encard s + Set.encard t' + 1 = ↑n
Tactic:
rw [Subtype.coe_injective.encard_image, add_assoc, ht, hs, add_comm, Nat.cast_add]
State after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ ↑m + Set.encard s = ↑m + ↑(Set.ncard s)

State before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ ↑m + Set.encard s = ↑m + ↑(Set.ncard s)
Tactic:
rw [Set.Finite.cast_ncard_eq]
State after:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.Finite s

State before:
case right.x
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Set.Finite s
Tactic:
exact Set.toFinite s
State after:
no goals

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ Disjoint s t'
Tactic:
rw [Set.disjoint_iff]
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s ∩ t' ⊆ ∅

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s ∩ t' ⊆ ∅
Tactic:
intro a
State after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
a : α
⊢ a ∈ s ∩ t' → a ∈ ∅

State before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
a : α
⊢ a ∈ s ∩ t' → a ∈ ∅
Tactic:
rintro ⟨hbs, ⟨b, _, rfl⟩⟩
State after:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ ↑b ∈ ∅

State before:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ ↑b ∈ ∅
Tactic:
exfalso
State after:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ False

State before:
case intro.intro.intro
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
m n : ℕ
s : Set α
inst✝ : Finite ↑s
hs : n = m + Set.ncard s
h : IsMultiplyPreprimitive M α n
t : Set ↥(SubMulAction.ofFixingSubgroup M s)
ht : Set.encard t + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
b : ↥(SubMulAction.ofFixingSubgroup M s)
left✝ : b ∈ t
hbs : ↑b ∈ s
⊢ False
Tactic:
exact b.prop hbs
State after:
no goals