internlm/Lean-Github huggingface dataset:
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case h.e'_3.h.e'_1.a
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype.card ↥(SubMulAction.ofStabilizer M a) = Fintype.card α - 1
Tactic:
convert Fintype.card_compl_set _
Proof state after:
case h.e'_3.h.e'_1.a.convert_5
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype ↑{a}ᶜ
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixing_subgroup_aux
Proof state before:
case h.e'_3.h.e'_1.a.convert_5
k : ℕ
hrec :
  ∀ (M : Type u_2) (α : Type u_1) [inst : Group M] [inst_1 : MulAction M α] [inst_2 : Fintype α],
    IsMultiplyPretransitive M α k →
      ∀ {s : Set α},
        Set.ncard s = k → Subgroup.index (fixingSubgroup M s) * (Fintype.card α - Set.ncard s)! = (Fintype.card α)!
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
hmk : IsMultiplyPretransitive M α (succ k)
s : Set α
hs : Set.ncard s = succ k
hGX : IsPretransitive M α
a : α
has : a ∈ s
t : Set ↥(SubMulAction.ofStabilizer M a) := Subtype.val ⁻¹' s
hat : Subtype.val '' t = s \ {a}
hat' : s = insert a (Subtype.val '' t)
hfs : fixingSubgroup M s = Subgroup.map (Subgroup.subtype (stabilizer M a)) (fixingSubgroup (↥(stabilizer M a)) t)
hscard : Set.ncard s = Set.ncard t + 1
htcard : Set.ncard t = k
this : succ k - 1 = Set.ncard t
⊢ Fintype ↑{a}ᶜ
Tactic:
exact setFintype {a}ᶜ
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup'
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)!
Tactic:
apply Nat.eq_of_mul_eq_mul_right (Nat.factorial_pos _)
Proof state after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) * ?m.226642! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * ?m.226642!

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ ℕ
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup'
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Subgroup.index (fixingSubgroup M s) * ?m.226642! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * ?m.226642!

M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ ℕ
Tactic:
rw [IsMultiplyPretransitive.index_of_fixingSubgroup M α s hMk]
Proof state after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ (Fintype.card α)! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * (Fintype.card α - Set.ncard s)!
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup'
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ (Fintype.card α)! = choose (Fintype.card α) (Set.ncard s) * (Set.ncard s)! * (Fintype.card α - Set.ncard s)!
Tactic:
rw [Nat.choose_mul_factorial_mul_factorial]
Proof state after:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Set.ncard s ≤ Fintype.card α
Theorem: MulAction.IsMultiplyPretransitive.index_of_fixingSubgroup'
Proof state before:
M : Type u_2
α : Type u_1
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : Fintype α
s : Set α
hMk : IsMultiplyPretransitive M α (Set.ncard s)
⊢ Set.ncard s ≤ Fintype.card α
Tactic:
apply Set.ncard_le_fintype_card
Proof state after:
no goals
Theorem: PartENat.lt_coe_succ_iff_le'
Proof state before:
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
by_cases hx : x = ⊤
Proof state after:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n

case neg
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : ¬x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Theorem: PartENat.lt_coe_succ_iff_le'
Proof state before:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
rw [hx]
Proof state after:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ ⊤ < ↑(succ n) ↔ ⊤ ≤ ↑n
Theorem: PartENat.lt_coe_succ_iff_le'
Proof state before:
case pos
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : x = ⊤
⊢ ⊤ < ↑(succ n) ↔ ⊤ ≤ ↑n
Tactic:
simp only [cast_succ, not_top_lt, top_le_iff, PartENat.natCast_ne_top]
Proof state after:
no goals
Theorem: PartENat.lt_coe_succ_iff_le'
Proof state before:
case neg
M : Type ?u.226745
α : Type ?u.226748
inst✝¹ : Group M
inst✝ : MulAction M α
x : PartENat
n : ℕ
hx : ¬x = ⊤
⊢ x < ↑(succ n) ↔ x ≤ ↑n
Tactic:
rw [Nat.succ_eq_add_one n, Nat.cast_add, Nat.cast_one, PartENat.lt_add_one_iff_lt hx]
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
⊢ IsPreprimitive M α
Tactic:
by_cases hα : Subsingleton α
Proof state after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : Subsingleton α
⊢ IsPreprimitive M α

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ IsPreprimitive M α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ IsPreprimitive M α
Tactic:
have hα' : 2 ≤ PartENat.card α := by
  rw [← PartENat.card_le_one_iff_subsingleton, not_le] at hα
  exact PartENat.coe_succ_le_iff.mpr hα
Proof state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPreprimitive M α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPreprimitive M α
Tactic:
have : IsPretransitive M α := by
  rw [isPretransitive_iff_is_one_pretransitive]
  apply isMultiplyPretransitive_of_higher M α h2
  norm_num
  exact hα'
Proof state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ IsPreprimitive M α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.mk
Proof state after:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
⊢ ∀ {B : Set α}, IsBlock M B → IsTrivialBlock B
Tactic:
intro B hB
Proof state after:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
⊢ IsTrivialBlock B
Tactic:
cases' B.subsingleton_or_nontrivial with h h
Proof state after:
case neg.has_trivial_blocks'.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ IsTrivialBlock B

case neg.has_trivial_blocks'.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ IsTrivialBlock B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : Subsingleton α
⊢ IsPreprimitive M α
Tactic:
apply IsPreprimitive.on_subsingleton
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
⊢ 2 ≤ PartENat.card α
Tactic:
rw [← PartENat.card_le_one_iff_subsingleton, not_le] at hα
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : 1 < PartENat.card α
⊢ 2 ≤ PartENat.card α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : 1 < PartENat.card α
⊢ 2 ≤ PartENat.card α
Tactic:
exact PartENat.coe_succ_le_iff.mpr hα
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsPretransitive M α
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
Proof state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α 1
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ IsMultiplyPretransitive M α 1
Tactic:
apply isMultiplyPretransitive_of_higher M α h2
Proof state after:
case hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ 1 ≤ 2

case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case hmn
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ 1 ≤ 2

case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Tactic:
norm_num
Proof state after:
case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case hα
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
⊢ ↑2 ≤ PartENat.card α
Tactic:
exact hα'
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inl
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ IsTrivialBlock B
Tactic:
left
Proof state after:
case neg.has_trivial_blocks'.inl.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ Set.Subsingleton B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inl.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Subsingleton B
⊢ Set.Subsingleton B
Tactic:
exact h
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ IsTrivialBlock B
Tactic:
right
Proof state after:
case neg.has_trivial_blocks'.inr.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ B = ⊤
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inr.h
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
h : Set.Nontrivial B
⊢ B = ⊤
Tactic:
obtain ⟨a, ha, b, hb, h⟩ := h
Proof state after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = ⊤
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ B = ⊤
Tactic:
rw [eq_top_iff]
Proof state after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ ⊤ ≤ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
⊢ ⊤ ≤ B
Tactic:
intro c _
Proof state after:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
⊢ c ∈ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg.has_trivial_blocks'.inr.h.intro.intro.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
⊢ c ∈ B
Tactic:
by_cases h' : a = c
Proof state after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ c ∈ B

case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ c ∈ B
Tactic:
rw [← h']
Proof state after:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ a ∈ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case pos
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ a ∈ B
Tactic:
exact ha
Proof state after:
no goals
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : IsBlock M B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
rw [IsBlock.mk_subset] at hB
Proof state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : IsMultiplyPretransitive M α 2
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
rw [is_two_pretransitive_iff] at h2
Proof state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Theorem: MulAction.IsMultiplyPretransitive.isPreprimitive_of_two
Proof state before:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
⊢ c ∈ B
Tactic:
obtain ⟨g, hga, hgb⟩ := h2 a b a c h h'
Proof state after:
case neg.intro.intro
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h2 : ∀ (a b c d : α), a ≠ b → c ≠ d → ∃ m, m • a = c ∧ m • b = d
hα : ¬Subsingleton α
hα' : 2 ≤ PartENat.card α
this : IsPretransitive M α
B : Set α
hB : ∀ {g : M} {b : α}, b ∈ B → b ∈ g • B → g • B ≤ B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : M
hga : g • a = a
hgb : g • b = c
⊢ c ∈ B