Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter (Jordan/Jordan.lean)

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have hts : s ∩ g • s ≤ s := Set.inter_subset_left s _
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have this : IsPretransitive (fixingSubgroup G (s ∩ g • s))
    (SubMulAction.ofFixingSubgroup G (s ∩ g • s)) :=
  isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
apply isPreprimitive_of_large_image (f := SubMulAction.ofFixingSubgroup.mapOfInclusion G hts) hs
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) <
    2 * Set.ncard (Set.range ⇑(SubMulAction.ofFixingSubgroup.mapOfInclusion G hts))

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) <
    2 * Set.ncard (Set.range ⇑(SubMulAction.ofFixingSubgroup.mapOfInclusion G hts))
Tactic:
rw [← Set.image_univ,
  Set.ncard_image_of_injective _ (SubMulAction.ofFixingSubgroup.mapOfInclusion_injective G _)]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Tactic:
have this : Set.ncard (s ∩  g • s)ᶜ < 2 * Set.ncard (sᶜ) := by
  rw [Set.compl_inter, ← Nat.add_lt_add_iff_right, Set.ncard_union_add_ncard_inter]
  rw [← Set.compl_union, two_mul, add_assoc]
  simp only [add_lt_add_iff_left]
  rw [← add_lt_add_iff_left, Set.ncard_add_ncard_compl]
  rw [MulAction.smul_set_ncard_eq, ← add_assoc, Set.ncard_add_ncard_compl]
  simp only [lt_add_iff_pos_right]
  rw [Set.ncard_pos]
  rw [Set.nonempty_compl]
  exact ha
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Tactic:
convert this
State after:
case h.e'_3
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Set.ncard (s ∩ g • s)ᶜ

case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard Set.univ = Set.ncard sᶜ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
Tactic:
rw [Set.compl_inter, ← Nat.add_lt_add_iff_right, Set.ncard_union_add_ncard_inter]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < 2 * Set.ncard sᶜ + Set.ncard (sᶜ ∩ (g • s)ᶜ)

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < 2 * Set.ncard sᶜ + Set.ncard (sᶜ ∩ (g • s)ᶜ)
Tactic:
rw [← Set.compl_union, two_mul, add_assoc]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < Set.ncard sᶜ + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < Set.ncard sᶜ + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)
Tactic:
simp only [add_lt_add_iff_left]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard (g • s)ᶜ < Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard (g • s)ᶜ < Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ
Tactic:
rw [← add_lt_add_iff_left, Set.ncard_add_ncard_compl]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Nat.card α < Set.ncard (g • s) + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Nat.card α < Set.ncard (g • s) + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)
Tactic:
rw [MulAction.smul_set_ncard_eq, ← add_assoc, Set.ncard_add_ncard_compl]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Nat.card α < Nat.card α + Set.ncard (s ∪ g • s)ᶜ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Nat.card α < Nat.card α + Set.ncard (s ∪ g • s)ᶜ
Tactic:
simp only [lt_add_iff_pos_right]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ 0 < Set.ncard (s ∪ g • s)ᶜ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ 0 < Set.ncard (s ∪ g • s)ᶜ
Tactic:
rw [Set.ncard_pos]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.Nonempty (s ∪ g • s)ᶜ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.Nonempty (s ∪ g • s)ᶜ
Tactic:
rw [Set.nonempty_compl]
State after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ s ∪ g • s ≠ Set.univ

State before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ s ∪ g • s ≠ Set.univ
Tactic:
exact ha
State after:
no goals

State before:
case h.e'_3
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Set.ncard (s ∩ g • s)ᶜ
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.Nat.card_coe_set_eq]
State after:
case h.e'_3
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Nat.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Nat.card ↑(s ∩ g • s)ᶜ

State before:
case h.e'_3
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Nat.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Nat.card ↑(s ∩ g • s)ᶜ
Tactic:
rfl
State after:
no goals

State before:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard Set.univ = Set.ncard sᶜ
Tactic:
rw [← SubMulAction.ofFixingSubgroup_carrier G]
State after:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard Set.univ = Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier

State before:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard Set.univ = Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier
Tactic:
rw [← Set.ncard_image_of_injective (Set.univ) (SubMulAction.ofFixingSubgroup G s).inclusion_injective]
State after:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier

State before:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier
Tactic:
rw [← SubMulAction.image_inclusion]
State after:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)))

State before:
case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)))
Tactic:
congr
State after:
case h.e'_4.h.e'_6.e_s
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ =
    Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s))

State before:
case h.e'_4.h.e'_6.e_s
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ =
    Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s))
Tactic:
simp only [Set.image_univ]
State after:
no goals