awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
this : ∃ b ∈ B, b ∈ sᶜ
⊢ sᶜ ⊆ B
have obtain : ∀ (b : α) (hb : b ∈ B) (hb' : b ∈ sᶜ), sᶜ ⊆ B
Tactic: obtain ⟨b, hb, hb'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
this : ∃ (k : ↥(fixingSubgroup M s)), k • b = x
⊢ x ∈ B
have obtain : ∀ (k : M) (hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k)
  (hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ),
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ B
Tactic: obtain ⟨⟨k, hk⟩, rfl⟩ := this
Cleared hypotheses: x, hx', this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ B
have suffices : k • B = B
Tactic: suffices k • B = B from this.le (smul_mem_smul_set hb)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ k • B = B
have apply : (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k sorry • B ∩ B).Nonempty
Tactic: apply isBlock_iff_smul_eq_of_nonempty.mp hB (g := ⟨k, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
apply : (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B ∩ B).Nonempty
⊢ k • B = B
have apply₁ : k ∈ G
Tactic: apply isBlock_iff_smul_eq_of_nonempty.mp hB (g := ⟨k, ?_⟩)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ (Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B ∩ B).Nonempty
have refine : a ∈ Subtype.mk (p := fun (x : M) ↦ x ∈ G) k sorry • B
Tactic: refine ⟨a, ?_, ha⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ a ∈ Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B
have hk₁ : ∀ y ∈ s, k • y = y
Tactic: rw [mem_fixingSubgroup_iff] at hk
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hk : ∀ y ∈ s, k • y = y
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk_1 • b ∈ sᶜ
⊢ a ∈ Subtype.mk (p := fun (x : M) ↦ x ∈ G) k ⋯ • B
have rw : k • a ∈ Subtype.mk (p := fun (x : M) ↦ x ∈ G) k sorry • B
Tactic: rw [← hk a ha']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hx' : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk • b ∈ sᶜ
⊢ k ∈ G
have a₁ : Membership.mem (γ := Subgroup M) (stabilizer M s) k
Tactic: apply hG
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
⊢ x ∈ B
have suffices : ∃ (k : ↥(fixingSubgroup M s)), k • b = x
Tactic: suffices ∃ k : fixingSubgroup M s, k • b = x by
    obtain ⟨⟨k, hk⟩, rfl⟩ := this
    suffices k • B = B from this.le (smul_mem_smul_set hb)
    -- `k • B = B`
    apply isBlock_iff_smul_eq_of_nonempty.mp hB (g := ⟨k, ?_⟩)
    · refine ⟨a, ?_, ha⟩
      rw [mem_fixingSubgroup_iff] at hk
      rw [← hk a ha']
      exact Set.smul_mem_smul_set ha
    · -- `k ∈ G`
      apply hG
      exact MulAction.fixingSubgroup_le_stabilizer _ _ hk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ ∃ (k : ↥(fixingSubgroup M s)), k • b = x
have obtain : ∀ (k : ↥(fixingSubgroup M s))
  (hk :
    k •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) b hb' =
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx'),
  ∃ (k : ↥(fixingSubgroup M s)), k • b = x
Tactic: obtain ⟨k, hk⟩ := h.exists_smul_eq (⟨b, hb'⟩ : ofFixingSubgroup M s) ⟨x, hx'⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
h : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
k : ↥(fixingSubgroup M s)
hk :
  k •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) b hb' =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx'
⊢ ∃ (k : ↥(fixingSubgroup M s)), k • b = x
have hk₁ : k •
    (↑(Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) b hb') :
      α) =
  (↑(Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx') :
    α)
Tactic: rw [← Subtype.coe_inj, val_smul] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
⊢ ∃ (k : ↥(fixingSubgroup M s)), k • b = x
have suffices : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: suffices h : IsPretransitive (fixingSubgroup M s) (ofFixingSubgroup M s) by
      obtain ⟨k, hk⟩ := h.exists_smul_eq (⟨b, hb'⟩ : ofFixingSubgroup M s) ⟨x, hx'⟩
      rw [← Subtype.coe_inj, val_smul] at hk
      exact ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
inst_2 : Finite α
inst_3 : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock.{u_1, u_2} (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
⊢ IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have rw : IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 1
Tactic: rw [← is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have h1 : sᶜ.Nonempty
Tactic: have h1 : sᶜ.Nonempty := nonempty_iff_ne_empty.mpr (by aesop)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have have : ∀ (this : Fintype α), IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: have : Fintype α := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have refine : ∀ (G : Subgroup (Perm α)) (hG : stabilizer (Perm α) s < G), G = ⊤
Tactic: refine ⟨stabilizer_ne_top_of_nonempty_of_nonempty_compl h0 h1, fun G hG ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ G = ⊤
have hG' : stabilizer (Perm α) sᶜ < G
Tactic: have hG' : stabilizer (Perm α) sᶜ < G := by rwa [stabilizer_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
⊢ G = ⊤
have obtain : ∀ (g : Perm α) (hg_swap : g.IsSwap) (hg : g ∈ G), G = ⊤
Tactic: obtain ⟨g, hg_swap, hg⟩ := has_swap_mem_of_lt_stabilizer s G hG
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
⊢ G = ⊤
have apply : IsPreprimitive (↥G) α
Tactic: apply subgroup_eq_top_of_isPreprimitive_of_isSwap_mem _ g hg_swap hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
⊢ IsPreprimitive (↥G) α
have this₁ : IsPretransitive (↥G) α
Tactic: have := G.isPretransitive_of_stabilizer_lt hG exists_mem_stabilizer_smul_eq
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
⊢ IsPreprimitive (↥G) α
have isTrivialBlock_of_isBlock : ∀ {B : Set α}, IsBlock (↥G) B → IsTrivialBlock B
Tactic: apply IsPreprimitive.mk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
⊢ B.Subsingleton ∨ B = univ
have isTrivialBlock_of_isBlock : ¬B.Subsingleton → B = univ
Tactic: rw [or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ B = univ
have apply : Nat.card α < B.ncard * 2
Tactic: apply hB.eq_univ_of_card_lt
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this : sᶜ ⊆ B
⊢ Nat.card α < B.ncard * 2
have this₁ : sᶜ.ncard ≤ B.ncard
Tactic: have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this_2 : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this_3 : sᶜ ⊆ B
this : sᶜ.ncard ≤ B.ncard
⊢ Nat.card α < B.ncard * 2
have rw : s.ncard + sᶜ.ncard < B.ncard * 2
Tactic: rw [← Set.ncard_add_ncard_compl s]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ B = univ
have isTrivialBlock_of_isBlock : sᶜ ⊆ B
Tactic: suffices sᶜ ⊆ B by
    apply hB.eq_univ_of_card_lt
    have : sᶜ.ncard ≤ B.ncard := ncard_le_ncard this
    rw [← Set.ncard_add_ncard_compl s]
    lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
⊢ False
have inl : ∀ (hB' : Nat.card α < sᶜ.ncard * 2), False
Tactic: rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
inl : ∀ (hB' : Nat.card α < sᶜ.ncard * 2), False
⊢ False
have inr : ∀ (hB' : sᶜ.ncard * 2 ≤ Nat.card α), False
Tactic: rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : Nat.card α < sᶜ.ncard * 2
⊢ False
have inl : s = ∅
Tactic: apply h0.ne_empty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : Nat.card α < sᶜ.ncard * 2
⊢ s = ∅
have inl : sᶜ = univ
Tactic: rw [← compl_univ_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : sᶜ.ncard * 2 ≤ Nat.card α
⊢ False
have hB'₁ : ¬Nat.card α < sᶜ.ncard * 2
Tactic: rw [← not_lt] at hB'
Cleared hypotheses: hB'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ False
have inr : Nat.card α < sᶜ.ncard * 2
Tactic: apply hB'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
⊢ Nat.card α < sᶜ.ncard * 2
have inr : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard * 2
Tactic: rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
inr : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard * 2
⊢ Nat.card α < sᶜ.ncard * 2
have inr₁ : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard + sᶜ.ncard
Tactic: rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB'_1 : ¬B.Subsingleton
hsc : IsBlock (↥G) sᶜ
hB' : ¬Nat.card α < sᶜ.ncard * 2
inr : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard * 2
inr₁ : sᶜ.ncard + sᶜᶜ.ncard < sᶜ.ncard + sᶜ.ncard
⊢ Nat.card α < sᶜ.ncard * 2
have inr₂ : sᶜᶜ.ncard < sᶜ.ncard
Tactic: rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
⊢ sᶜ ⊆ B
have not_isBlock_sc : ¬IsBlock (↥G) sᶜ
Tactic: have not_isBlock_sc : ¬ IsBlock G sᶜ := fun hsc ↦ by
    rcases lt_or_ge (Nat.card α) (sᶜ.ncard * 2) with hB' | hB'
    · apply h0.ne_empty
      rw [← compl_univ_iff]
      exact hsc.eq_univ_of_card_lt hB'
    · rw [← not_lt] at hB'
      apply hB'
      rwa [← Set.ncard_add_ncard_compl sᶜ, mul_two, add_lt_add_iff_left, compl_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this_1 : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
⊢ sᶜ ⊆ B
have hB_not_le_sc : ∀ (B : Set α) (hB : IsBlock (↥G) B) (hBsc : B ⊆ sᶜ), B.Subsingleton
Tactic: have hB_not_le_sc (B : Set α) (hB : IsBlock G B) (hBsc : B ⊆ sᶜ) :
      B.Subsingleton :=
    -- uses Step 1
    hB.subsingleton_of_ssubset_of_stabilizer_Perm_le (hBsc.ssubset_of_ne (by lia)) hG'.le