awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
h3 : τ.IsSwap
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
have obtain : ∀ (x y : α) (h4 : x ≠ y) (h5 : τ = swap x y), Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
Tactic: obtain ⟨x, y, h4, h5⟩ := h3
Cleared hypotheses: h3
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
have obtain : ∀ (i : ℕ) (hi : (σ ^ i : (a : α) → α) x = y), Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
Tactic: obtain ⟨i, hi⟩ :=
    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, τ}) ⊤
have rw : Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ i : (a : α) → α) x)}) ⊤
Tactic: rw [h5, ← hi]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ i : (a : α) → α) x)}) ⊤
have refine : ∀ (h : Fintype.card α ∣ i), x = y
Tactic: refine closure_cycle_coprime_swap
    (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
h : Fintype.card α ∣ i
⊢ x = y
have obtain : ∀ (m : ℕ) (hm : i = Fintype.card α * m), x = y
Tactic: obtain ⟨m, hm⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
⊢ x = y
have rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₄ : ∀ (hi : ((σ ^ orderOf σ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₄ : ∀ (hi : ((σ ^ orderOf σ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₅ : ∀ (hi : (HPow.hPow (α := Perm α) 1 m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₄ : ∀ (hi : ((σ ^ orderOf σ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₅ : ∀ (hi : (HPow.hPow (α := Perm α) 1 m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₆ : ∀ (hi : (1 : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Closure (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₄ : ∀ (hi : ((σ ^ orderOf σ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₅ : ∀ (hi : (HPow.hPow (α := Perm α) 1 m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₆ : ∀ (hi : (1 : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y
have rwa₇ : ∀ (hi : x = y) (hm : i = Fintype.card α * m), x = y
Tactic: rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi
Cleared hypotheses: hi, hm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : Membership.mem (γ := Subgroup G) (closure S) g
⊢ (fixedBy α g)ᶜ.Finite
have refine : ∀ (g g' : G),
  Membership.mem (γ := Subgroup G) (closure S) g →
    Membership.mem (γ := Subgroup G) (closure S) g' →
      ∀ (hg : (fixedBy α g)ᶜ.Finite) (hg' : (fixedBy α g')ᶜ.Finite),
        (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
Tactic: refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
      (by simp) hg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g_1 : G
hg_1 : Membership.mem (γ := Subgroup G) (closure S) g_1
g g' : G
h_1 : Membership.mem (γ := Subgroup G) (closure S) g
h_2 : Membership.mem (γ := Subgroup G) (closure S) g'
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
have simp_rw : (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g ∩ fixedBy α g')ᶜ
Tactic: simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g_1 : G
hg_1 : Membership.mem (γ := Subgroup G) (closure S) g_1
g g' : G
h_1 : Membership.mem (γ := Subgroup G) (closure S) g
h_2 : Membership.mem (γ := Subgroup G) (closure S) g'
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
simp_rw : (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g ∩ fixedBy α g')ᶜ
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
have simp_rw₁ : fixedBy α g ∩ fixedBy α g' ⊆ fixedBy α (g * g')
Tactic: simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
have have : ∀ (b : α) (hb : b ∈ T), ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
Tactic: have ⟨b, hb⟩ := nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
have obtain : ∀ (σ : ↥(closure S)) (hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T),
  ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
Tactic: obtain ⟨σ, rfl⟩ := subset hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
have contrapose : ∀ (h : LE.le (α := Subgroup G) (closure S) (stabilizer G T)), a ∈ T
Tactic: contrapose notMem with h
Cleared hypotheses: notMem
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (hypothesis)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
have key0 : ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
Tactic: have key0 : ¬ closure S ≤ stabilizer G T := by
    have ⟨b, hb⟩ := nonempty
    obtain ⟨σ, rfl⟩ := subset hb
    contrapose notMem with h
    exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T
have contrapose! : ∀ (key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T), LE.le (α := Subgroup G) (closure S) (stabilizer G T)
Tactic: contrapose! key0
Cleared hypotheses: key0
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
⊢ LE.le (α := Subgroup G) (closure S) (stabilizer G T)
have refine : ∀ (σ : G) (hσ : σ ∈ S), σ ∈ (↑(stabilizer G T) : Set G)
Tactic: refine (closure_le _).mpr fun σ hσ ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ σ ∈ (↑(stabilizer G T) : Set G)
have simp_rw : ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T
Tactic: simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y z : α
h : Membership.mem (γ := Set α) {x, y}ᶜ z
⊢ z ∈ fixedBy α (swap x y)
have a : z ≠ x
Tactic: apply swap_apply_of_ne_of_ne
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x y z : α
h : Membership.mem (γ := Set α) {x, y}ᶜ z
a : z ≠ x
⊢ z ∈ fixedBy α (swap x y)
have a₁ : z ≠ y
Tactic: apply swap_apply_of_ne_of_ne
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
σ : Perm α
h : σ.IsSwap
⊢ (fixedBy α σ)ᶜ.Finite
have obtain : ∀ (x y : α), (fixedBy α (swap x y))ᶜ.Finite
Tactic: obtain ⟨x, y, -, rfl⟩ := h
Cleared hypotheses: σ, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
⊢ swap a c ∈ M
have inl : ∀ (hab : swap a a ∈ M) (hbc : swap a c ∈ M), swap a c ∈ M
Tactic: obtain rfl | hab' := eq_or_ne a b
Cleared hypotheses: b, hab, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
inl : ∀ (hab : swap a a ∈ M) (hbc : swap a c ∈ M), swap a c ∈ M
⊢ swap a c ∈ M
have inr : ∀ (hab' : a ≠ b), swap a c ∈ M
Tactic: obtain rfl | hab' := eq_or_ne a b
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
⊢ swap a c ∈ M
have inr : ∀ (hbc : swap b a ∈ M), swap a a ∈ M
Tactic: obtain rfl | hac := eq_or_ne a c
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
inr : ∀ (hbc : swap b a ∈ M), swap a a ∈ M
⊢ swap a c ∈ M
have inr₁ : ∀ (hac : a ≠ c), swap a c ∈ M
Tactic: obtain rfl | hac := eq_or_ne a c
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap a c ∈ M
have inr : swap b c * swap a b * swap b c ∈ M
Tactic: rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y) ↔ x ∈ orbit (↥(closure S)) y
have refine : ∀ (hf : x ∈ orbit (↥(closure S)) y), Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)
Tactic: refine ⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)
have by_contra : ∀ (h : swap x y ∉ closure S), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
⊢ False
have refine_4 : ∀
  (this :
    ∃ σ ∈ S,
      ∃ (a : α),
        Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
          σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
  False
Tactic: have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
refine_4 :
  ∀
    (this :
      ∃ σ ∈ S,
        ∃ (a : α),
          Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
            σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    False
⊢ False
have refine_1 : ∀ (f : Equiv.Perm α) (hf : f ∈ S), f⁻¹ ∈ S
Tactic: have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
refine_4 :
  ∀
    (this :
      ∃ σ ∈ S,
        ∃ (a : α),
          Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
            σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    False
refine_1 : ∀ (f : Equiv.Perm α) (hf : f ∈ S), f⁻¹ ∈ S
⊢ False
have refine_2 : ∀ (z : α)
  (hz : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} z),
  z ∈ orbit (↥(closure S)) x
Tactic: have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
refine_4 :
  ∀
    (this :
      ∃ σ ∈ S,
        ∃ (a : α),
          Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
            σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    False
refine_1 : ∀ (f : Equiv.Perm α) (hf : f ∈ S), f⁻¹ ∈ S
refine_2 :
  ∀ (z : α)
    (hz : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} z),
    z ∈ orbit (↥(closure S)) x
⊢ False
have refine_3 : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} y
Tactic: have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
this :
  ∃ σ ∈ S,
    ∃ (a : α),
      Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
        σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ False
have refine_4 : ∀ (σ : Equiv.Perm α) (hσ : σ ∈ S) (a : α)
  (ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a)
  (hσa : σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}), False
Tactic: obtain ⟨σ, hσ, a, ha, hσa⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (goal)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
σ : Equiv.Perm α
hσ : σ ∈ S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
hσa : σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ False
have refine_4 : ∀ (z w : α) (hzw : z ≠ w) (hσ : swap z w ∈ S)
  (hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}), False
Tactic: obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ
Cleared hypotheses: σ, hσ, hσa
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.ClosureSwap (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ False
have this : a ≠ swap z w • a
Tactic: have := ne_of_mem_of_not_mem ha hσa