internlm/Lean-Github huggingface dataset:
Theorem: Finperm.swap_mul_swap
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b * swap a b).support ⊆ {a, b}
Tactic:
refine (mul_support_subset _ _).trans ?_
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b).support ∪ (swap a b).support ⊆ {a, b}
Theorem: Finperm.swap_mul_swap
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ (swap a b).support ∪ (swap a b).support ⊆ {a, b}
Tactic:
rw [Finset.union_self, swap_support_of_ne hne]
Proof state after:
no goals
Theorem: Finperm.swap_mul_swap
Proof state before:
case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
a b : α
hne : a ≠ b
⊢ 1.support ⊆ {a, b}
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.swap_conj_eq
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
⊢ swap x y * swap y z * swap x y = swap x z
Tactic:
obtain (rfl | hxy) := eq_or_ne x y
Proof state after:
case inl
α : Type u_1
x : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz hyz : x ≠ z
⊢ swap x x * swap x z * swap x x = swap x z

case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ swap x y * swap y z * swap x y = swap x z
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ swap x y * swap y z * swap x y = swap x z
Tactic:
apply funext_support_subset (s := {x,y,z})
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y * swap y z * swap x y).support ⊆ {x, y, z}

case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x z).support ⊆ {x, y, z}

case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ ∀ i ∈ {x, y, z}, (swap x y * swap y z * swap x y) i = (swap x z) i
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ ∀ i ∈ {x, y, z}, (swap x y * swap y z * swap x y) i = (swap x z) i
Tactic:
simp only [mem_insert, mem_singleton, mul_apply, forall_eq_or_imp, swap_apply_left,
  swap_apply_right, forall_eq]
Proof state after:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y) z = z ∧ (swap x y) ((swap y z) x) = (swap x z) y ∧ (swap x y) ((swap y z) ((swap x y) z)) = x
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y) z = z ∧ (swap x y) ((swap y z) x) = (swap x z) y ∧ (swap x y) ((swap y z) ((swap x y) z)) = x
Tactic:
rw [swap_apply_of_ne_of_ne hxz.symm hyz.symm, swap_apply_of_ne_of_ne hxy hxz,
  swap_apply_of_ne_of_ne hxy.symm hyz]
Proof state after:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ z = z ∧ (swap x y) x = y ∧ (swap x y) ((swap y z) z) = x
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.h
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ z = z ∧ (swap x y) x = y ∧ (swap x y) ((swap y z) z) = x
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.swap_conj_eq
Proof state before:
case inl
α : Type u_1
x : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz hyz : x ≠ z
⊢ swap x x * swap x z * swap x x = swap x z
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x y * swap y z * swap x y).support ⊆ {x, y, z}
Tactic:
rw [mul_support_eq, mul_support_eq]
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => (swap x y * swap y z) ((swap x y) x_1) ≠ x_1)
      (filter (fun x_1 => (swap x y) ((swap y z) x_1) ≠ x_1) ((swap x y).support ∪ (swap y z).support) ∪
        (swap x y).support) ⊆
    {x, y, z}
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => (swap x y * swap y z) ((swap x y) x_1) ≠ x_1)
      (filter (fun x_1 => (swap x y) ((swap y z) x_1) ≠ x_1) ((swap x y).support ∪ (swap y z).support) ∪
        (swap x y).support) ⊆
    {x, y, z}
Tactic:
simp only [mul_apply, ne_eq, swap_support, filter_congr_decidable, if_neg hxy, if_neg hyz]
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => ¬(swap x y) ((swap y z) ((swap x y) x_1)) = x_1)
      (filter (fun x_1 => ¬(swap x y) ((swap y z) x_1) = x_1) ({x, y} ∪ {y, z}) ∪ {x, y}) ⊆
    {x, y, z}
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ filter (fun x_1 => ¬(swap x y) ((swap y z) ((swap x y) x_1)) = x_1)
      (filter (fun x_1 => ¬(swap x y) ((swap y z) x_1) = x_1) ({x, y} ∪ {y, z}) ∪ {x, y}) ⊆
    {x, y, z}
Tactic:
refine (filter_subset _ _).trans (union_subset ((filter_subset _ _).trans ?_) (by aesop))
Proof state after:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ∪ {y, z} ⊆ {x, y, z}
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.hf
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ∪ {y, z} ⊆ {x, y, z}
Tactic:
apply union_subset <;> aesop
Proof state after:
no goals
Theorem: Finperm.swap_conj_eq
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ {x, y} ⊆ {x, y, z}
Tactic:
aesop
Proof state after:
no goals
Theorem: Finperm.swap_conj_eq
Proof state before:
case inr.hg
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
z : α
hxz : x ≠ z
hyz : y ≠ z
hxy : x ≠ y
⊢ (swap x z).support ⊆ {x, y, z}
Tactic:
aesop
Proof state after:
no goals
Theorem: Finperm.support_mul_pair_subset
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
⊢ (f * swap x (f⁻¹ x)).support ⊆ erase f.support x
Tactic:
intro y hy
Proof state after:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ y ∈ erase f.support x
Theorem: Finperm.support_mul_pair_subset
Proof state before:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ y ∈ erase f.support x
Tactic:
simp only [mem_erase, ne_eq, mem_support_iff]
Proof state after:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ ¬y = x ∧ ¬f y = y
Theorem: Finperm.support_mul_pair_subset
Proof state before:
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
⊢ ¬y = x ∧ ¬f y = y
Tactic:
obtain (rfl | hne) := eq_or_ne y x
Proof state after:
case inl
α : Type u_1
y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
y : α
hx : y ∈ f.support
hy : y ∈ (f * swap y (f⁻¹ y)).support
⊢ ¬y = y ∧ ¬f y = y

case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
⊢ ¬y = x ∧ ¬f y = y
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
⊢ ¬y = x ∧ ¬f y = y
Tactic:
refine ⟨hne, fun hy' ↦ ?_⟩
Proof state after:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
hy' : f y = y
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hy : y ∈ (f * swap x (f⁻¹ x)).support
hne : y ≠ x
hy' : f y = y
⊢ False
Tactic:
simp only [mem_support_iff, mul_apply, ne_eq] at hy
Proof state after:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
⊢ False
Tactic:
obtain (rfl | hne') := eq_or_ne y (f⁻¹ x)
Proof state after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy' : f (f⁻¹ x) = f⁻¹ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
⊢ False

case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
hne' : y ≠ f⁻¹ x
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f ((swap x (f⁻¹ x)) y) = y
hne' : y ≠ f⁻¹ x
⊢ False
Tactic:
rw [swap_apply_of_ne_of_ne hne hne'] at hy
Proof state after:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f y = y
hne' : y ≠ f⁻¹ x
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr.inr
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
y : α
hne : y ≠ x
hy' : f y = y
hy : ¬f y = y
hne' : y ≠ f⁻¹ x
⊢ False
Tactic:
exact hy hy'
Proof state after:
no goals
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inl
α : Type u_1
y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
y : α
hx : y ∈ f.support
hy : y ∈ (f * swap y (f⁻¹ y)).support
⊢ ¬y = y ∧ ¬f y = y
Tactic:
simp at hy
Proof state after:
no goals
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy' : f (f⁻¹ x) = f⁻¹ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
⊢ False
Tactic:
simp only [swap_apply_right, apply_inv_apply] at hy'
Proof state after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : f⁻¹ x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Tactic:
rw [← hy'] at hne
Proof state after:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Theorem: Finperm.support_mul_pair_subset
Proof state before:
case inr.inl
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
hx : x ∈ f.support
hne : x ≠ x
hy : ¬f ((swap x (f⁻¹ x)) (f⁻¹ x)) = f⁻¹ x
hy' : x = f⁻¹ x
⊢ False
Tactic:
exact hne rfl
Proof state after:
no goals
Theorem: Finperm.swapsOf_univ_eq
Proof state before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ swapsOf Set.univ = swaps α
Tactic:
simp [swaps, swapsOf]
Proof state after:
no goals
Theorem: Finperm.swapsOf_support_subset
Proof state before:
α : Type u_1
x y : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
hf : f ∈ swapsOf t
⊢ ↑f.support ⊆ t
Tactic:
obtain ⟨i,j, hi, hj, hne, rfl⟩ := hf
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
x y : α
g : Finperm α
inst✝ : DecidableEq α
t : Set α
i j : α
hi : i ∈ t
hj : j ∈ t
hne : i ≠ j
⊢ ↑(swap i j).support ⊆ t
Theorem: Finperm.swapsOf_support_subset
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
x y : α
g : Finperm α
inst✝ : DecidableEq α
t : Set α
i j : α
hi : i ∈ t
hj : j ∈ t
hne : i ≠ j
⊢ ↑(swap i j).support ⊆ t
Tactic:
rwa [swap_support_of_ne hne, coe_insert, Set.insert_subset_iff, coe_singleton,
  Set.singleton_subset_iff, and_iff_right hi]
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
obtain (h | h) := eq_or_ne f.support ∅
Proof state after:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ f ∈ Subgroup.closure (swapsOf t)

case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support ≠ ∅
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support ≠ ∅
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
simp only [ne_eq, eq_empty_iff_forall_not_mem, mem_support_iff, not_not, not_forall] at h
Proof state after:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : ∃ x, ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : ∃ x, ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
obtain ⟨x, hx⟩ := h
Proof state after:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hx' : x ∈ f.support := by simpa
Proof state after:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
set g := f * swap x (f⁻¹ x) with hg_def
Proof state after:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hsupp : g.support ⊆ _ := support_mul_pair_subset hx'
Proof state after:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have _ : g.support.card < f.support.card := by
  exact card_lt_card <| (hsupp.trans_ssubset (erase_ssubset hx'))
Proof state after:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hg_supp : (g.support : Set α) ⊆ t
Proof state after:
case hg_supp
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ ↑g.support ⊆ t

case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hg := support_closure_aux hg_supp
Proof state after:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
Proof state after:
case hs
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)

case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hf' : f = g * (swap x (f⁻¹ x))
Proof state after:
case hf'
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
⊢ f = g * swap x (f⁻¹ x)

case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
hf' : f = g * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
hf' : f = g * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
rw [hf']
Proof state after:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
hf' : f = g * swap x (f⁻¹ x)
⊢ g * swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inr.intro
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
hf' : f = g * swap x (f⁻¹ x)
⊢ g * swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
Tactic:
exact Subgroup.mul_mem _ hg hs
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
rw [show f = 1 from (support_eq_empty_iff _).1 h]
Proof state after:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ 1 ∈ Subgroup.closure (swapsOf t)
Theorem: Finperm.support_closure_aux
Proof state before:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ 1 ∈ Subgroup.closure (swapsOf t)
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals