awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s : Set α
⊢ IsPreprimitive.{u_2, u_2} ↥(stabilizer (Perm α) s) (↑s : Type u_2)

Tactic:
isPreprimitive_stabilizer_of_surjective s (stabilizer.surjective_toPerm s)

Premises used: MulAction.isPreprimitive_stabilizer_of_surjective, Equiv.Perm.stabilizer.surjective_toPerm
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
hs : s.Nonempty
hsc : sᶜ.Nonempty
obtain : ∀ (a : α) (ha : a ∈ s), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
hsc : sᶜ.Nonempty
a : α
ha : a ∈ s
obtain : ∀ (b : α) (hb : b ∈ sᶜ), Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤

Tactic:
obtain ⟨b, hb⟩ := hsc
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ b ∉ s

Tactic:
rw [Set.mem_compl_iff] at hb

Premises used: Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ sᶜ
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
hb₁ : b ∉ s
⊢ Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤

Tactic:
rw [Set.mem_compl_iff] at hb

Premises used: Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
apply : b ∈ s
⊢ False

Tactic:
apply hb
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b)

Tactic:
have hg : swap a b ∈ stabilizer (Perm α) s := by simp_all
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
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)
⊢ swap a b • s = s

Tactic:
rw [mem_stabilizer_iff] at hg

Premises used: MulAction.mem_stabilizer_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∉ s
h : Eq (α := Subgroup (Perm α)) (stabilizer (Perm α) s) ⊤
hg : swap a b • s = s
rw : ∃ y ∈ s, swap a b • y = b
⊢ b ∈ s

Tactic:
rw [← hg, Set.mem_smul_set]

Premises used: Set.mem_smul_set
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
s : Set α
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:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
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
⊢ Ne (α := Subgroup (Perm α)) (stabilizer (Perm α) 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

Premises used: Set.mem_smul_set, MulAction.mem_stabilizer_iff, Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
t : Set α
ht : 1 < t.encard
⊢ ∃ (a : α) (b : α), a ∈ t ∧ b ∈ t ∧ a ≠ b

Tactic:
rw [Set.one_lt_encard_iff] at ht

Premises used: Set.one_lt_encard_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
obtain :
  ∀ (a b : α) (ha : a ∈ t) (hb : b ∈ t) (h : a ≠ b),
    ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g

Tactic:
obtain ⟨a, b, ha, hb, h⟩ := ht
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
right : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) (swap a b)
⊢ ∃ (g : Perm α), g.IsSwap ∧ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) t) g

Tactic:
use swap a b, Perm.swap_isSwap_iff.mpr h, swap_mem_stabilizer ha hb

Premises used: Iff.mpr, Equiv.swap, Equiv.Perm.swap_mem_stabilizer, Equiv.Perm.swap_isSwap_iff
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
Goal:
α : Type u_2
inst : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr : ∀ (h1' : s.encard ≤ 1), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
rcases lt_or_ge 1 s.encard with h1 | h1'

Premises used: Set.encard, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inl :
  ∀ (g : Perm α) (hg : g.IsSwap) (hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g),
    ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
obtain ⟨g, hg, hg'⟩ := this s h1
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α
hg : g.IsSwap
hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
⟨g, hg, hG.le hg'⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α
hg : g.IsSwap
hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
exact ⟨g, hg, hG.le hg'⟩
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr₁ : ∀ (h1c' : sᶜ.encard ≤ 1), ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
rcases lt_or_ge 1 sᶜ.encard with h1c | h1c'

Premises used: Set.encard, Compl.compl, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
inr :
  ∀ (g : Perm α) (hg : g.IsSwap) (hg' : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g),
    ∃ (g : Perm α), g.IsSwap ∧ g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
obtain ⟨g, hg, hg'⟩ := this sᶜ h1c

Premises used: Compl.compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
right : g ∈ G
⊢ ∃ (g : Perm α), g.IsSwap ∧ g ∈ G

Tactic:
use g, hg
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g

Tactic:
rw [stabilizer_compl] at hg'

Premises used: stabilizer_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

Tactic:
hG.le hg'

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

Tactic:
exact hG.le hg'

Premises used: LT.lt.le
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
rw : s.encard + sᶜ.encard = 2
⊢ encard.{u_2} (α := α) univ = 2

Tactic:
rw [← Set.encard_add_encard_compl s]

Premises used: Set.encard_add_encard_compl
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ HAdd.hAdd (α := ℕ∞) 1 1 = 2

Tactic:
norm_num
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ HAdd.hAdd (α := ℕ∞) 1 1 = 2

Tactic:
have : (1 + 1 : ENat) = 2 := by norm_num
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ HAdd.hAdd (α := ℕ∞) 1 1 = 2

Tactic:
this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
h₁ : sᶜ.encard = 1
⊢ s.encard + sᶜ.encard = 2

Tactic:
convert! this
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
h₁ : 1 ≤ s.encard
⊢ s.encard = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 ≤ 1

Tactic:
assumption
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 ≠ ∅
⊢ 1 ≤ s.encard

Tactic:
rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty, Set.one_le_encard_iff_nonempty
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 ≠ ∅

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
h₁ : 1 ≤ sᶜ.encard
⊢ sᶜ.encard = 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 ≤ 1

Tactic:
assumption
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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ᶜ ≠ ∅
⊢ 1 ≤ sᶜ.encard

Tactic:
rw [one_le_encard_iff_nonempty, Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty, Set.one_le_encard_iff_nonempty
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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ᶜ ≠ ∅

Tactic:
aesop
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

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
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
rw : Nonempty.{u_2 + 1} (Fintype α)
⊢ Finite α

Tactic:
rw [finite_iff_nonempty_fintype]

Premises used: finite_iff_nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α)

Tactic:
univ_finite_iff_nonempty_fintype.mp ?_

Premises used: Iff.mp, Set.univ_finite_iff_nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
refine : Set.Finite.{u_2} (α := α) univ
⊢ Nonempty.{u_2 + 1} (Fintype α)

Tactic:
refine univ_finite_iff_nonempty_fintype.mp ?_

Premises used: Iff.mp, Set.univ_finite_iff_nonempty_fintype
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ Set.Finite.{u_2} (α := α) univ

Tactic:
finite_of_encard_eq_coe hα

Premises used: Set.finite_of_encard_eq_coe
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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
⊢ Set.Finite.{u_2} (α := α) univ

Tactic:
exact finite_of_encard_eq_coe hα

Premises used: Set.finite_of_encard_eq_coe
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α

Tactic:
have _ : Finite α := by
    rw [finite_iff_nonempty_fintype]
    refine univ_finite_iff_nonempty_fintype.mp ?_
    exact finite_of_encard_eq_coe hα
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α
⊢ 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α

Premises used: Nat.card_coe_set_eq, ENat.card_coe_set_eq, Set.ncard_univ, ENat.card_eq_coe_natCard
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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 α
hα₁ : Eq (α := ℕ∞) (↑(Nat.card α) : ℕ∞) 2
⊢ Finite α

Tactic:
rw [← ENat.card_coe_set_eq, ENat.card_eq_coe_natCard, Nat.card_coe_set_eq, ncard_univ] at hα

Premises used: Nat.card_coe_set_eq, ENat.card_coe_set_eq, Set.ncard_univ, ENat.card_eq_coe_natCard
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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α : Eq (α := ℕ∞) (↑(Nat.card α) : ℕ∞) 2
h : Finite α
⊢ Nat.card α = 2

Tactic:
ENat.coe_inj.mp hα

Premises used: ENat.coe_inj, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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α : Eq (α := ℕ∞) (↑(Nat.card α) : ℕ∞) 2
h : Finite α
⊢ Nat.card α = 2

Tactic:
exact ENat.coe_inj.mp hα

Premises used: ENat.coe_inj, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.MaximalSubgroups
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

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α