awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)}
this : a ≠ swap z w • a
⊢ False
have this₁ : a = z ∨ a = w
Tactic: rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at 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
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)}
this : a = z ∨ a = w
⊢ False
have refine_4 : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z w • a) a)
Tactic: refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)
-- 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
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)}
this : a = z ∨ a = w
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z w • a) a)
have refine_4 : ∀ (hzw : a ≠ w) (hσ : swap a w ∈ S)
  (hσa : swap a w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
  Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap a w • a) a)
Tactic: obtain rfl | rfl := this
Cleared hypotheses: z, hzw, hσ, hσa, 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
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)}
this : a = z ∨ a = w
refine_4 :
  ∀ (hzw : a ≠ w) (hσ : swap a w ∈ S)
    (hσa : swap a w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap a w • a) a)
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z w • a) a)
have refine_4₁ : ∀ (hzw : z ≠ a) (hσ : swap z a ∈ S)
  (hσa : swap z a • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
  Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z a • a) a)
Tactic: obtain rfl | rfl := this
Cleared hypotheses: w, hzw, hσ, hσa, 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_1 : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
f : Equiv.Perm α
hf : f ∈ S
⊢ f⁻¹ ∈ S
have refine_1 : ∀ (x y : α) (hf : swap x y ∈ S), (swap x y)⁻¹ ∈ S
Tactic: obtain ⟨x, y, -, rfl⟩ := hS f hf
Cleared hypotheses: f, 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
h : swap x y ∉ closure S
⊢ Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} y
have refine_3 : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (Equiv.refl α)
Tactic: rw [mem_setOf, swap_self]
-- 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
f : Equiv.Perm α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f ↔
    (fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
have refine_1 : ∀ (hf : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f), (fixedBy α f)ᶜ.Finite
Tactic: refine ⟨fun hf ↦ ⟨?_, fun x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩⟩, ?_⟩
-- 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
f : Equiv.Perm α
refine_1 : ∀ (hf : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f), (fixedBy α f)ᶜ.Finite
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f ↔
    (fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
have refine_2 : ((fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)) →
  Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: refine ⟨fun hf ↦ ⟨?_, fun x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩⟩, ?_⟩
-- 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
f : Equiv.Perm α
fin : (fixedBy α f)ᶜ.Finite
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
fin₁ :
  let supp := (fixedBy α f)ᶜ;
  supp.Finite
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have supp_eq : let supp := (fixedBy α f)ᶜ;
supp = (fixedBy α f)ᶜ
Tactic: set supp := (fixedBy α f)ᶜ with supp_eq
Cleared hypotheses: fin
-- 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
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α := (fixedBy α f)ᶜ
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have refine_2 : (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: suffices h : (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S from h supp_eq.symm.subset
-- 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
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α := (fixedBy α f)ᶜ
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
⊢ (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have refine_2 : ∀ (supp : Set α) (fin : supp.Finite) (supp_eq : supp = (fixedBy α f)ᶜ),
  (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: clear_value supp
Cleared hypotheses: supp, fin, supp_eq
-- 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
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α
fin : supp.Finite
⊢ (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have refine_2 : ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
  (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: revert f
Cleared hypotheses: f, 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
supp : Set α
fin : supp.Finite
⊢ ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have apply : ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
  (fixedBy α f)ᶜ ⊆ ∅ → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: apply fin.induction_on ..
-- 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
supp : Set α
fin : supp.Finite
apply :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ ∅ → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have apply₁ : ∀ {a : α} {s : Set α},
  a ∉ s →
    ∀ (hs : s.Finite),
      (∀ {f : Equiv.Perm α}
          (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
          (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f) →
        ∀ {f : Equiv.Perm α}
          (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
          (fixedBy α f)ᶜ ⊆ insert a s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
Tactic: apply fin.induction_on ..
-- 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
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have h : f = 1
Tactic: convert! (closure S).one_mem
-- 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
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ f = 1
have h : ∀ (x : α), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
Tactic: ext
-- 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
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x : α
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
have h : ∀ (h : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)), 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have refine_1 : ∀ (b : α),
  Membership.mem (α := α) (orbit (↥(closure S)) b)
    ((HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f : (a : α) → α) b : α)
Tactic: refine (mul_mem_cancel_left ((swap_mem_closure_isSwap hS).2 (hf a))).1
    (ih (fun b ↦ ?_) fun b hb ↦ ?_)
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
refine_1 :
  ∀ (b : α),
    Membership.mem (α := α) (orbit (↥(closure S)) b)
      ((HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f : (a : α) → α) b : α)
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
have refine_2 : ∀ (b : α) (hb : b ∈ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ), b ∈ s
Tactic: refine (mul_mem_cancel_left ((swap_mem_closure_isSwap hS).2 (hf a))).1
    (ih (fun b ↦ ?_) fun b hb ↦ ?_)
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b)
    ((HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f : (a : α) → α) b : α)
have refine_1 : (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
  else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
  orbit (↥(closure S)) b
Tactic: rw [Perm.mul_apply, swap_apply_def]
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
    else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
    orbit (↥(closure S)) b
have pos : ∀ (h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)), a ∈ orbit (↥(closure S)) b
Tactic: split_ifs with h1 h2
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
pos : ∀ (h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)), a ∈ orbit (↥(closure S)) b
⊢ (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
    else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
    orbit (↥(closure S)) b
have pos₁ : ∀ (h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)) (h2 : (f : (a : α) → α) b = a),
  Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) a : α)
Tactic: split_ifs with h1 h2
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
pos : ∀ (h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)), a ∈ orbit (↥(closure S)) b
pos₁ :
  ∀ (h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)) (h2 : (f : (a : α) → α) b = a),
    Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) a : α)
⊢ (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
    else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
    orbit (↥(closure S)) b
have neg : ∀ (h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)) (h2 : ¬(f : (a : α) → α) b = a),
  Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) b : α)
Tactic: split_ifs with h1 h2
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
⊢ a ∈ orbit (↥(closure S)) b
have pos : a ∈ orbit (↥(closure S)) a
Tactic: rw [← orbit_eq_iff.mpr (hf b), h1, orbit_eq_iff.mpr (hf a)]
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
h2 : (f : (a : α) → α) b = a
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) a : α)
have pos : Membership.mem (α := α) (orbit (↥(closure S)) a) ((f : (a : α) → α) a : α)
Tactic: rw [← orbit_eq_iff.mpr (hf b), h2]
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∈ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ
⊢ b ∈ s
have refine_2 : ∀ (hb : b ∉ s), b ∉ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ
Tactic: contrapose hb
Cleared hypotheses: hb
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ b ∉ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ
have refine_2 : (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
Tactic: simp_rw [notMem_compl_iff, mem_fixedBy, Perm.smul_def, Perm.mul_apply, swap_apply_def,
      apply_eq_iff_eq]
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
have pos : ∀ (hb' : (f : (a : α) → α) b = b),
  (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
Tactic: by_cases hb' : f b = b
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
pos :
  ∀ (hb' : (f : (a : α) → α) b = b),
    (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
have neg : ∀ (hb' : ¬(f : (a : α) → α) b = b),
  (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
Tactic: by_cases hb' : f b = b
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
have pos : (if b = a then a else if b = a then (f : (a : α) → α) a else b) = b
Tactic: rw [hb']
-- 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
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
⊢ (if b = a then a else if b = a then (f : (a : α) → α) a else b) = b
have pos : ∀ (h : b = a), a = b
Tactic: split_ifs with h