awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₂ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₃ obtain₄ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₅ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), b ∈ s
obtain₆ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
    (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)), b ∈ s
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₇ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
  (hg : swap a b • s = s), b ∈ s
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₁ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
obtain₂ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∈ sᶜ) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₃ obtain₄ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), False
obtain₅ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤), b ∈ s
obtain₆ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
    (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)), b ∈ s
obtain₇ :
  ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
    (hg : swap a b • s = s), b ∈ s
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
have obtain₈ : ∀ (a : α) (ha : a ∈ s) (b : α) (hb : b ∉ s) (h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤)
  (hg : swap a b • s = s), ∃ y ∈ s, swap a b • y = b
Tactic: classical
  obtain ⟨a, ha⟩ := hs
  obtain ⟨b, hb⟩ := hsc
  intro h
  rw [Set.mem_compl_iff] at hb; apply hb
  have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
  rw [mem_stabilizer_iff] at hg
  rw [← hg, Set.mem_smul_set]
  aesop
Cleared hypotheses: hs, hsc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < t.encard
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
have ht₁ : ∃ (a : α) (b : α), a ∈ t ∧ b ∈ t ∧ a ≠ b
Tactic: rw [Set.one_lt_encard_iff] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : ∃ (a : α) (b : α), a ∈ t ∧ b ∈ t ∧ a ≠ b
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
have obtain : ∀ (a b : α) (ha : a ∈ t) (hb : b ∈ t) (h : a ≠ b),
  ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
Tactic: obtain ⟨a, b, ha, hb, h⟩ := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
have w : Perm α
Tactic: use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
w : Perm α
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
have left : (swap a b).IsSwap
Tactic: use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
a b : α
ha : a ∈ t
hb : b ∈ t
h : a ≠ b
w : Perm α
left : (swap a b).IsSwap
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
have right : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) (swap a b)
Tactic: use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have this : ∀ (t : Set α),
  1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
Tactic: have : ∀ (t : Set α) (_ : 1 < t.encard), ∃ (g : Perm α),
      g.IsSwap ∧ g ∈ stabilizer (Perm α) t := by
    intro t ht
    rw [Set.one_lt_encard_iff] at ht
    obtain ⟨a, b, ha, hb, h⟩ := ht
    use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inl : ∀ (h1 : 1 < s.encard), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: rcases lt_or_ge 1 s.encard with h1 | h1'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
inl : ∀ (h1 : 1 < s.encard), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr : ∀ (h1' : s.encard ≤ 1), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: rcases lt_or_ge 1 s.encard with h1 | h1'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1 : 1 < s.encard
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inl : ∀ (g : Perm α) (hg : g.IsSwap) (hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g),
  ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: obtain ⟨g, hg, hg'⟩ := this s h1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr : ∀ (h1c : 1 < sᶜ.encard), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: rcases lt_or_ge 1 sᶜ.encard with h1c | h1c'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
inr : ∀ (h1c : 1 < sᶜ.encard), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr₁ : ∀ (h1c' : sᶜ.encard ≤ 1), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: rcases lt_or_ge 1 sᶜ.encard with h1c | h1c'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c : 1 < sᶜ.encard
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr : ∀ (g : Perm α) (hg : g.IsSwap) (hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g),
  ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
Tactic: obtain ⟨g, hg, hg'⟩ := this sᶜ h1c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c : 1 < sᶜ.encard
g : Perm α
hg : g.IsSwap
hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have right : g ∈ G
Tactic: use g, hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c : 1 < sᶜ.encard
g : Perm α
hg : g.IsSwap
hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g
⊢ g ∈ G
have hg'₁ : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
Tactic: rw [stabilizer_compl] at hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
⊢ encard.{u_2} (α := α) univ = 2
have rw : s.encard + sᶜ.encard = 2
Tactic: rw [← Set.encard_add_encard_compl s]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
⊢ s.encard + sᶜ.encard = 2
have this₁ : HAdd.hAdd (α := ℕ∞) 1 1 = 2
Tactic: have : (1 + 1 : ENat) = 2 := by norm_num
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
⊢ s.encard + sᶜ.encard = 2
have h : s.encard = 1
Tactic: convert! this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
h : s.encard = 1
⊢ s.encard + sᶜ.encard = 2
have h₁ : sᶜ.encard = 1
Tactic: convert! this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
h : s.encard ≤ 1
⊢ s.encard = 1
have h₁ : 1 ≤ s.encard
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
⊢ 1 ≤ s.encard
have h : s ≠ ∅
Tactic: rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
h : sᶜ.encard ≤ 1
⊢ sᶜ.encard = 1
have h₁ : 1 ≤ sᶜ.encard
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this_1 :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
this : HAdd.hAdd (α := ℕ∞) 1 1 = 2
⊢ 1 ≤ sᶜ.encard
have h : sᶜ ≠ ∅
Tactic: rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have hα : encard.{u_2} (α := α) univ = 2
Tactic: have hα : Set.encard (_root_.Set.univ : Set α) = 2 := by
    rw [← Set.encard_add_encard_compl s]
    have : (1 + 1 : ENat) = 2 := by norm_num
    convert! this <;>
    · apply le_antisymm
      · assumption
      rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]
      aesop
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : encard.{u_2} (α := α) univ = 2
⊢ Finite α
have rw : Nonempty.{u_2 + 1} (Fintype α)
Tactic: rw [finite_iff_nonempty_fintype]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : encard.{u_2} (α := α) univ = 2
⊢ Nonempty.{u_2 + 1} (Fintype α)
have refine : Set.Finite.{u_2} (α := α) univ
Tactic: refine univ_finite_iff_nonempty_fintype.mp ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : encard.{u_2} (α := α) univ = 2
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have x : Finite α
Tactic: have _ : Finite α := by
    rw [finite_iff_nonempty_fintype]
    refine univ_finite_iff_nonempty_fintype.mp ?_
    exact finite_of_encard_eq_coe hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : encard.{u_2} (α := α) univ = 2
h : Finite α
⊢ Nat.card α = 2
have hα₁ : Eq (α := ℕ∞) (↑(Nat.card α) : ℕ∞) 2
Tactic: rw [← ENat.card_coe_set_eq, ENat.card_eq_coe_natCard, Nat.card_coe_set_eq, ncard_univ] at hα
Cleared hypotheses: hα, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα : encard.{u_2} (α := α) univ = 2
h : Finite α
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have hα₁ : Nat.card α = 2
Tactic: have hα : Nat.card α = 2 := by
    rw [← ENat.card_coe_set_eq, ENat.card_eq_coe_natCard, Nat.card_coe_set_eq, ncard_univ] at hα
    exact ENat.coe_inj.mp hα
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
have out : Nat.Prime (Nat.card.{u_2} (Perm α))
Tactic: apply Fact.mk
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ Nat.Prime (Nat.card.{u_2} (Perm α))
have out : Nat.Prime 2
Tactic: rw [Nat.card_perm, hα, Nat.factorial_two]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
Tactic: have hα2 : Fact (Nat.card (Perm α)).Prime := by
    apply Fact.mk
    rw [Nat.card_perm, hα, Nat.factorial_two]
    exact Nat.prime_two
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊥
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊤
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have inr : ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) (α := Set α) univ) g
Tactic: rw [h, ← stabilizer_univ_eq_top (Perm α) α]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (goal)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h_1 : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
h : G = ⊤
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) (α := Set α) univ) g
have inr : 1 < encard.{u_2} (α := α) univ
Tactic: apply this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.MaximalSubgroups (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this :
  ∀ (t : Set α),
    1 < t.encard → ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα_1 : encard.{u_2} (α := α) univ = 2
h : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card.{u_2} (Perm α)))
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
have x : G = ⊥ ∨ G = ⊤
Tactic: cases G.eq_bot_or_eq_top_of_prime_card with
  | inl h =>
    exfalso; exact ne_bot_of_gt hG h
  | inr h =>
    rw [h, ← stabilizer_univ_eq_top (Perm α) α]
    apply this
    simp_all
-- 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
⊢ IsPretransitive.{u_1, u_2} (↥G) α
have hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : ↥G), g • a = b
Tactic: apply IsPretransitive.of_partition (s := 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 α
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
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : ↥G), g • a = b
⊢ IsPretransitive.{u_1, u_2} (↥G) α
have hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : ↥G), g • a = b
Tactic: apply IsPretransitive.of_partition (s := 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 α
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
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ (g : ↥G), g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ (g : ↥G), g • a = b
⊢ IsPretransitive.{u_1, u_2} (↥G) α
have hM : Ne.{u_1 + 1} (α := Subgroup ↥G) (stabilizer (↥G) s) ⊤
Tactic: apply IsPretransitive.of_partition (s := 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 α
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