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 α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
⊢ ∃ (g : ↥G), g • a = b
have hs' : ∀ (g : M) (hg : Membership.mem (γ := Subgroup M) (stabilizer M sᶜ) g) (hb : g • a ∈ sᶜ), ∃ (g_1 : ↥G), g_1 • a = g • a
Tactic: obtain ⟨g, hg, rfl⟩ := moves a ha b hb
Cleared hypotheses: b, hb
-- 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 α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
a : α
ha : a ∈ sᶜ
g : M
hg : Membership.mem (γ := Subgroup M) (stabilizer M sᶜ) g
hb : g • a ∈ sᶜ
⊢ ∃ (g_1 : ↥G), g_1 • a = g • a
have hg₁ : Membership.mem (γ := Subgroup M) (stabilizer M s) g
Tactic: rw [stabilizer_compl] at hg
Cleared hypotheses: hg, 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 α
G : Subgroup M
hG : stabilizer M s < G
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
⊢ Ne.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
have hM : ∀ (hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤), ¬stabilizer M s < G
Tactic: contrapose hG
Cleared hypotheses: 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
⊢ ¬stabilizer M s < G
have hM : G ≤ stabilizer M s
Tactic: apply not_lt_of_ge
-- 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
⊢ G = Subgroup.map G.subtype ⊤
have rw : G = G.subtype.range
Tactic: rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
rw : G = G.subtype.range
⊢ G = Subgroup.map G.subtype ⊤
have rw₁ : G = G
Tactic: rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
⊢ G ≤ stabilizer M s
have this : G = Subgroup.map G.subtype ⊤
Tactic: have : G = Subgroup.map G.subtype ⊤ := by
      rw [← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ G ≤ stabilizer M s
have hM : ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)
Tactic: rw [this, Subgroup.map_le_iff_le_comap]
-- 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
this : G = Subgroup.map G.subtype ⊤
⊢ ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)
have hM : LE.le.{u_1} (α := Subgroup ↥G) ⊤ (stabilizer (↥G) s)
Tactic: rw [show Subgroup.comap G.subtype (stabilizer M s) = stabilizer G s from rfl, 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 α
G : Subgroup M
moves : ∀ {s : Set α}, ∀ a ∈ s, ∀ b ∈ s, ∃ (g : M), Membership.mem (γ := Subgroup M) (stabilizer M s) g ∧ g • a = b
hG : Eq.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
this : G = Subgroup.map G.subtype ⊤
hM : LE.le.{u_1} (α := Subgroup ↥G) ⊤ (stabilizer (↥G) s)
⊢ ⊤ ≤ Subgroup.comap G.subtype (stabilizer M s)
have hM₁ : LE.le.{u_1} (α := Subgroup ↥G) ⊤ ⊤
Tactic: rw [show Subgroup.comap G.subtype (stabilizer M s) = stabilizer G s from rfl, 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ B.Subsingleton
have rw : (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)).Subsingleton
Tactic: rw [← inter_eq_self_of_subset_right (subset_of_ssubset hB_ss_sc), ← Subtype.image_preimage_val]
-- 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)).Subsingleton
have hs : Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
Tactic: apply Set.Subsingleton.image
-- 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
have apply : ¬Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
Tactic: apply Or.resolve_right 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ ¬Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
have rw : ¬{x : α | x ∈ s} ⊆ B
Tactic: rw [preimage_eq_univ_iff, Subtype.range_coe_subtype]
-- 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ Set.Subsingleton (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
have hs : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
Tactic: suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set (s : Set α)) by
    apply Or.resolve_right this
    rw [preimage_eq_univ_iff, Subtype.range_coe_subtype]
    exact not_subset_of_ssubset hB_ss_sc
-- 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
have apply : IsBlock.{u_1, u_2} ↥(stabilizer M s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
Tactic: apply this.isTrivialBlock_of_isBlock
-- 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 B : Set α
hB_ss_sc : B ⊂ s
hB : IsBlock M B
hG : Function.Surjective.{u_1 + 1, u_2 + 1} (α := ↥(stabilizer M s)) (β := Perm (↑s : Type u_2)) toPerm
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
have hs : IsPreprimitive.{u_1, u_2} ↥(stabilizer M s) (↑s : Type u_2)
Tactic: suffices IsPreprimitive (stabilizer M (s : Set α)) (s : Set α) by
    apply this.isTrivialBlock_of_isBlock
    let φ' : stabilizer M (s : Set α) → M := Subtype.val
    let f' : (s : Set α) →ₑ[φ'] α := {
      toFun := Subtype.val
      map_smul' _ _ := rfl }
    exact hB.preimage f'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
⊢ B.Subsingleton
have apply : Function.Surjective.{u_2 + 1, u_2 + 1} (α := ↥(stabilizer (↥G) s)) (β := Perm (↑s : Type u_2)) toPerm
Tactic: apply hB.subsingleton_of_ssubset_of_stabilizer_le hB_ss_sc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
g : Perm (↑s : Type u_2)
⊢ ∃ (a : ↥(stabilizer (↥G) s)), toPerm a = g
have obtain : ∀ (k : Perm α) (hk : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) k),
  ∃ (a : ↥(stabilizer (↥G) s)),
    Eq (α := Perm (↑s : Type u_2)) (toPerm a)
      (toPerm
        (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) x) k hk))
Tactic: obtain ⟨⟨k, hk⟩, rfl⟩ := stabilizer.surjective_toPerm s g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
k : Perm α
hk : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) k
h : ↥G := Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) k ⋯
⊢ ∃ (a : ↥(stabilizer (↥G) s)),
    Eq (α := Perm (↑s : Type u_2)) (toPerm a)
      (toPerm
        (Subtype.mk (p := fun (x : Perm α) ↦ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) x) k hk))
have this : Membership.mem (γ := Subgroup ↥G) (stabilizer (↥G) s) h
Tactic: have : h ∈ stabilizer G s := by aesop
-- 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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ B.Subsingleton
have inl : ∀ (hB' : Set.Subsingleton (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)), B.Subsingleton
Tactic: rcases this with hB' | hB'
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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
inl : ∀ (hB' : Set.Subsingleton (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)), B.Subsingleton
⊢ B.Subsingleton
have inr : ∀ (hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ), B.Subsingleton
Tactic: rcases this with hB' | hB'
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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Set.Subsingleton (α := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
⊢ B.Subsingleton
have inl : (Set.image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)).Subsingleton
Tactic: rw [← inter_eq_self_of_subset_right hBs, ← Subtype.image_preimage_val]
-- 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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
⊢ B.Subsingleton
have hBs' : B = s
Tactic: have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
-- 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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
⊢ B.Subsingleton
have inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
Tactic: subst hBs'
Cleared hypotheses: s, inst_2, hB_not_le_sc, hG, hBs, hB', hBs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
⊢ B.Subsingleton
have hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
Tactic: subst hBs'
Cleared hypotheses: s, inst_3, hB_not_le_sc, hG, hBs, hB', hBs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
⊢ B.Subsingleton
have hG₁ : stabilizer M B < G
Tactic: subst hBs'
Cleared hypotheses: s, inst_3, hB_not_le_sc, hG, hBs, hB', hBs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG₁ : stabilizer M B < G
⊢ B.Subsingleton
have hBs₁ : B ⊆ B
Tactic: subst hBs'
Cleared hypotheses: s, inst_3, hB_not_le_sc, hG, hBs, hB', hBs'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst_1 : Group M
inst_2 : MulAction M α
s B : Set α
G : Subgroup M
inst_3 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Eq (α := Set (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B) Set.univ
hBs' : B = s
inst : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc₁ : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG₁ : stabilizer M B < G
hBs₁ : B ⊆ B
⊢ B.Subsingleton
have hB'₁ : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
Tactic: subst hBs'
Cleared hypotheses: s, inst_3, hB_not_le_sc, hG, hBs, hB', hBs'
-- 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 α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
⊢ B.Subsingleton
have inr : ∀ (g' : M) (hg' : g' ∈ G) (hg's : g' ∉ stabilizer M B), B.Subsingleton
Tactic: obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG
-- 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 α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
⊢ B.Subsingleton
have h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
Tactic: have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
-- 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 α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
⊢ B.Subsingleton
have inr : (g' • B).Subsingleton
Tactic: suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B 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 α
B : Set α
G : Subgroup M
hB : IsBlock.{u_1, u_2} (↥G) B
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) B) (↑B : Type u_2)
hB_not_le_sc : ∀ (B_1 : Set α), IsBlock.{u_1, u_2} (↥G) B_1 → B_1 ⊆ Bᶜ → B_1.Subsingleton
hG : stabilizer M B < G
hBs : B ⊆ B
hB' : Eq (α := Set (↑B : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ B) ⁻¹' B) Set.univ
g' : M
hg' : g' ∈ G
hg's : g' ∉ stabilizer M B
h : _root_.Disjoint (Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B) B
⊢ (g' • B).Subsingleton
have inr : Subtype.mk (p := fun (x : M) ↦ x ∈ G) g' hg' • B ⊆ Bᶜ
Tactic: apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)
-- 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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
⊢ B.Subsingleton
have suffices : IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
Tactic: suffices IsTrivialBlock (Subtype.val ⁻¹' B : Set s) by
    rcases this with hB' | hB'
    · -- trivial case
      rw [← inter_eq_self_of_subset_right hBs, ← Subtype.image_preimage_val]
      apply Set.Subsingleton.image hB'
    · -- `Subtype.val ⁻¹' B = s`
      have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)
      subst hBs'
      obtain ⟨g', hg', hg's⟩ := SetLike.exists_of_lt hG
      have h := (isBlock_iff_smul_eq_or_disjoint.mp hB ⟨g', hg'⟩).resolve_left hg's
      suffices (g' • B).Subsingleton by
        exact subsingleton_of_image (MulAction.injective g') B this
      apply hB_not_le_sc (⟨g', hg'⟩ • B) (hB.translate _)
      exact Disjoint.subset_compl_right h
-- 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 B : Set α
G : Subgroup M
inst_2 : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
hB : IsBlock.{u_1, u_2} (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock.{u_1, u_2} (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
this : IsPreprimitive.{u_1, u_2} ↥(stabilizer (↥G) s) (↑s : Type u_2)
⊢ IsTrivialBlock (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
have apply : IsBlock.{u_1, u_2} ↥(stabilizer (↥G) s) (X := (↑s : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' B)
Tactic: apply this.isTrivialBlock_of_isBlock
-- 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
⊢ sᶜ ⊆ B
have this : ∃ a ∈ B, a ∈ s
Tactic: have : ∃ a : α, a ∈ B ∧ a ∈ s := by grind
-- 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
this : ∃ a ∈ B, a ∈ s
⊢ sᶜ ⊆ B
have obtain : ∀ (a : α) (ha : a ∈ B) (ha' : a ∈ s), sᶜ ⊆ B
Tactic: obtain ⟨a, ha, ha'⟩ := this
Cleared hypotheses: this
-- 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
⊢ sᶜ ⊆ B
have this : ∃ b ∈ B, b ∈ sᶜ
Tactic: have : ∃ b : α, b ∈ B ∧ b ∈ sᶜ := by grind