awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
h : ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → f.Disjoint g
⊢ f.Disjoint (List.prod [])

Tactic:
disjoint_one_right _

Premises used: Equiv.Perm.disjoint_one_right, List.foldr, List.prod
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
h : ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → f.Disjoint g
⊢ f.Disjoint (List.prod [])

Tactic:
exact disjoint_one_right _

Premises used: Equiv.Perm.disjoint_one_right
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : ∀ (h : ∀ g ∈ l, f.Disjoint g), f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)

Tactic:
(h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Premises used: List.mem_cons_of_mem, Equiv.Perm.Disjoint.mul_right, List.mem_cons_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f g : Perm α
l : List (Perm α)
ih : ∀ (h : ∀ g ∈ l, f.Disjoint g), f.Disjoint l.prod
h : ∀ g_1 ∈ g :: l, f.Disjoint g_1
⊢ f.Disjoint (g * l.prod)

Tactic:
exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Premises used: List.mem_cons_of_mem, Equiv.Perm.Disjoint.mul_right, List.mem_cons_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
l : List (Perm α)
h : ∀ g ∈ l, f.Disjoint g
nil : ∀ (h : ∀ (g : Perm α), Membership.mem (γ := List (Perm α)) [] g → f.Disjoint g), f.Disjoint (List.prod [])
cons :
  ∀ (g : Perm α) (l : List (Perm α)) (ih : ∀ (h : ∀ g ∈ l, f.Disjoint g), f.Disjoint l.prod)
    (h : ∀ g_1 ∈ g :: l, f.Disjoint g_1), f.Disjoint (g :: l).prod
⊢ f.Disjoint l.prod

Tactic:
induction l with
  | nil => exact disjoint_one_right _
  | cons g l ih =>
    rw [List.prod_cons]
    exact (h _ List.mem_cons_self).mul_right (ih fun g hg => h g (List.mem_cons_of_mem _ hg))

Premises used: Finset.cons, Equiv.Perm.disjoint_one_right, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
g : Perm α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ Commute (k i) (k j)
hg : ∀ i ∈ s, g.Disjoint (k i)
⊢ g.Disjoint (s.noncommProd k hs)

Tactic:
noncommProd_induction s k hs g.Disjoint (fun _ _ ↦ Disjoint.mul_right) (disjoint_one_right g) hg

Premises used: Finset.noncommProd_induction, Equiv.Perm.disjoint_one_right, Equiv.Perm.Disjoint.mul_right, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
l₁ l₂ : List (Perm α)
hl : List.Pairwise Disjoint l₁
hp : l₁ ~ l₂
⊢ l₁.prod = l₂.prod

Tactic:
hp.prod_eq' <| hl.imp Disjoint.commute

Premises used: Equiv.Perm.Disjoint.commute, List.Pairwise.imp, List.Perm.prod_eq'
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
l : List (Perm α)
h1 : 1 ∉ l
h2 : List.Pairwise Disjoint l
⊢ l.Nodup

Tactic:
grind [List.Pairwise.imp_of_mem, disjoint_refl_iff]

Premises used: Equiv.Perm.disjoint_refl_iff, List.Pairwise.imp_of_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : (f ^ n * f : (a : α) → α) x = x
rw₁ : (f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw₂ : (f ^ n : (a : α) → α) x = x
rw₃ rw₄ : x = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x

Tactic:
rw [pow_succ, mul_apply, hfx, pow_apply_eq_self_of_apply_eq_self hfx n]

Premises used: pow_succ, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hfx : (f : (a : α) → α) x = x
n : ℕ
rw : ((f ^ (n + 1))⁻¹ : (a : α) → α) x = x
rw₁ : x = (f ^ (n + 1) : (a : α) → α) x
rw₂ rw₃ : x = x
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

Premises used: zpow_negSucc, Equiv.Perm.inv_eq_iff_eq, Equiv.Perm.pow_apply_eq_self_of_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : (f ^ n : (a : α) → α) x = x
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
rw₁ : Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)
rw₂ rw₃ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f ^ (n + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [pow_succ', mul_apply, h]

Premises used: Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
h : Eq (α := α) ((f ^ n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
rw : (f * f ^ n : (a : α) → α) x = x
rw₁ : (f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) = x
rw₂ : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
rw₃ rw₄ : x = x
⊢ (f ^ (n + 1) : (a : α) → α) x = x

Tactic:
rw [pow_succ', mul_apply, h, hffx]

Premises used: Equiv.Perm.mul_apply, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
rw :
  (f ^ (n + 1 + 1) : (a : α) → α) x = x ∨ Eq (α := α) ((f ^ (n + 1 + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ (f ^ Int.negSucc n : (a : α) → α) x = x ∨
    Eq (α := α) ((f ^ Int.negSucc n : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, ← f.injective.eq_iff, ← mul_apply, ← pow_succ', eq_comm,
      inv_eq_iff_eq, ← mul_apply, ← pow_succ, @eq_comm _ x, or_comm]

Premises used: zpow_negSucc, pow_succ, Equiv.Perm.inv_eq_iff_eq, Function.Injective.eq_iff, eq_comm, Equiv.Perm.mul_apply, Equiv.injective, or_comm, pow_succ'
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
⊢ (f ^ (n + 1 + 1) : (a : α) → α) x = x ∨ Eq (α := α) ((f ^ (n + 1 + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
pow_apply_eq_of_apply_apply_eq_self hffx _

Premises used: Equiv.Perm.pow_apply_eq_of_apply_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
x : α
hffx : (f : (a : α) → α) ((f : (a : α) → α) x : α) = x
n : ℕ
⊢ (f ^ (n + 1 + 1) : (a : α) → α) x = x ∨ Eq (α := α) ((f ^ (n + 1 + 1) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
exact pow_apply_eq_of_apply_apply_eq_self hffx _

Premises used: Equiv.Perm.pow_apply_eq_of_apply_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
rw : (σ : (a : α) → α) ((τ : (a : α) → α) a : α) = a
rw₁ : (σ : (a : α) → α) a = a
rw₂ rw₃ : a = a
⊢ (σ * τ : (a : α) → α) a = a

Tactic:
rw [mul_apply, h.2, h.1]

Premises used: And.right, And.left, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
refine : ∀ (h : (σ * τ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
⊢ (σ * τ : (a : α) → α) a = a ↔ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
refine ⟨fun h => ?_, fun h => by rw [mul_apply, h.2, h.1]⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
inl : ∀ (hσ : (σ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
inr : ∀ (hτ : (τ : (a : α) → α) a = a), (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
rcases hστ a with hσ | hτ
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
hσ : (σ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
⟨hσ, σ.injective (h.trans hσ.symm)⟩

Premises used: And.intro, Equiv.injective, Eq.symm, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
hσ : (σ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
exact ⟨hσ, σ.injective (h.trans hσ.symm)⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
hτ : (τ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
⟨(congr_arg σ hτ).symm.trans h, hτ⟩

Premises used: congr_arg, And.intro, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ : (a : α) → α) a = a
hτ : (τ : (a : α) → α) a = a
⊢ (σ : (a : α) → α) a = a ∧ (τ : (a : α) → α) a = a

Tactic:
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
simp_rw :
  (∀ (x : α), Eq (α := α) ((σ * τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ↔
    (∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)) ∧
      ∀ (x : α), Eq (α := α) ((τ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
simp_rw₁ :
  (∀ (x : α), (σ * τ : (a : α) → α) x = x) ↔ (∀ (x : α), (σ : (a : α) → α) x = x) ∧ ∀ (x : α), (τ : (a : α) → α) x = x
simp_rw₂ :
  (∀ (x : α), (σ : (a : α) → α) x = x ∧ (τ : (a : α) → α) x = x) ↔
    (∀ (x : α), (σ : (a : α) → α) x = x) ∧ ∀ (x : α), (τ : (a : α) → α) x = x
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Tactic:
simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]

Premises used: Equiv.Perm.Disjoint.mul_apply_eq_iff, Equiv.Perm.ext_iff, Equiv.Perm.one_apply, forall_and
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
m n : ℤ
⊢ (σ ^ m).Disjoint (τ ^ n)

Tactic:
fun x =>
  Or.imp (fun h => zpow_apply_eq_self_of_apply_eq_self h m)
    (fun h => zpow_apply_eq_self_of_apply_eq_self h n) (hστ x)

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, Or.imp, Equiv.Perm.Disjoint
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
m n : ℕ
⊢ (σ ^ m).Disjoint (τ ^ n)

Tactic:
hστ.zpow_disjoint_zpow m n

Premises used: Equiv.Perm.Disjoint.zpow_disjoint_zpow, Nat.cast, zpowRec
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
x y : Subtype p
⊢ (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) (swap x y) = swap (↑x : α) (↑y : α)

Tactic:
grind [ofSubtype_apply_of_mem, ofSubtype_apply_of_not_mem]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy :
  Subtype.mk (p := p) x hx ≠ Subtype.mk (p := p) y hy ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
⊢ ¬x = y ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)

Tactic:
simp only [Ne, Subtype.ext_iff] at hxy

Premises used: Ne, Subtype.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
⊢ x ≠ y

Tactic:
hxy.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy : ¬x = y ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
⊢ x ≠ y

Tactic:
exact hxy.1

Premises used: And.left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
p : α → Prop
inst_1 : DecidablePred p
f : Perm (Subtype p)
h : f.IsSwap
x : α
hx : p x
y : α
hy : p y
hxy :
  Subtype.mk (p := p) x hx ≠ Subtype.mk (p := p) y hy ∧ f = swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)
rw :
  (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) (swap (Subtype.mk (p := p) x hx) (Subtype.mk (p := p) y hy)) =
    swap x y
rw₁ rw₂ : swap (↑(Subtype.mk (p := p) x hx) : α) (↑(Subtype.mk (p := p) y hy) : α) = swap x y
⊢ (ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) f = swap x y

Tactic:
rw [hxy.2, ofSubtype_swap_eq]

Premises used: And.right, Equiv.Perm.ofSubtype_swap_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
x y : α
hy : (swap x ((f : (a : α) → α) x) * f : (a : α) → α) y ≠ y
⊢ (if (f : (a : α) → α) y = x then (f : (a : α) → α) x else if y = x then x else (f : (a : α) → α) y) ≠ y

Tactic:
simp only [swap_apply_def, mul_apply, f.injective.eq_iff] at *

Premises used: Function.Injective.eq_iff, Equiv.swap_apply_def, Equiv.Perm.mul_apply, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
f : Perm α
x y : α
hy : (if (f : (a : α) → α) y = x then (f : (a : α) → α) x else if y = x then x else (f : (a : α) → α) y) ≠ y
⊢ (f : (a : α) → α) y ≠ y ∧ y ≠ x

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p : Perm α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) {x : α | (Equiv.symm p : (a : α) → α) x ≠ x} x ↔
      Membership.mem (γ := Set α) {x : α | (p : (a : α) → α) x ≠ x} x
⊢ Eq.{u_1 + 1} (α := Set α) {x : α | (Equiv.symm p : (a : α) → α) x ≠ x} {x : α | (p : (a : α) → α) x ≠ x}

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p : Perm α
x : α
⊢ Membership.mem (γ := Set α) {x : α | (Equiv.symm p : (a : α) → α) x ≠ x} x ↔
    Membership.mem (γ := Set α) {x : α | (p : (a : α) → α) x ≠ x} x

Tactic:
simp [eq_symm_apply, eq_comm]

Premises used: eq_comm, Equiv.eq_symm_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p : Perm α
a : α
⊢ Membership.mem (α := α) (γ := Set α) {x : α | (p : (a : α) → α) x ≠ x} ((p : (a : α) → α) a : α) ↔
    Membership.mem (γ := Set α) {x : α | (p : (a : α) → α) x ≠ x} a

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n : (a : α) → α) x = x
H : (p : (a : α) → α) x = x
⊢ False

Tactic:
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx

Premises used: Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p q : Perm α
simp :
  Subset.{u_1} (α := Set α) {x : α | comp (β := α) (⇑p : (a : α) → α) (⇑q : (a : α) → α) x ≠ x}
    ({x : α | (p : (a : α) → α) x ≠ x} ∪ {x : α | (q : (a : α) → α) x ≠ x})
⊢ Subset.{u_1} (α := Set α) {x : α | (p * q : (a : α) → α) x ≠ x}
    ({x : α | (p : (a : α) → α) x ≠ x} ∪ {x : α | (q : (a : α) → α) x ≠ x})

Tactic:
simp only [coe_mul]

Premises used: Equiv.Perm.coe_mul
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
p q : Perm α
⊢ Subset.{u_1} (α := Set α) {x : α | comp (β := α) (⇑p : (a : α) → α) (⇑q : (a : α) → α) x ≠ x}
    ({x : α | (p : (a : α) → α) x ≠ x} ∪ {x : α | (q : (a : α) → α) x ≠ x})

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
n : ℕ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₂ :
  Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
rw₃ rw₄ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x

Tactic:
rw [← mul_apply, Commute.self_pow f, mul_apply, apply_eq_iff_eq]

Premises used: Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq, Commute.self_pow
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
f : Perm α
n : ℤ
x : α
rw : Eq (α := α) ((f * f ^ n : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₁ : Eq (α := α) ((f ^ n * f : (a : α) → α) x : α) ((f ^ n : (a : α) → α) x : α) ↔ (f : (a : α) → α) x = x
rw₂ :
  Eq (α := α) ((f ^ n : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x
rw₃ rw₄ : (f : (a : α) → α) x = x ↔ (f : (a : α) → α) x = x
⊢ Eq (α := α) ((f : (a : α) → α) ((f ^ n : (a : α) → α) x : α) : α) ((f ^ n : (a : α) → α) x : α) ↔
    (f : (a : α) → α) x = x

Tactic:
rw [← mul_apply, Commute.self_zpow f, mul_apply, apply_eq_iff_eq]

Premises used: Commute.self_zpow, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
rw : Membership.mem (γ := Finset α) {x : α | (f : (a : α) → α) x ≠ x} x ↔ (f : (a : α) → α) x ≠ x
rw₁ : Membership.mem (γ := Finset α) univ x ∧ (f : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
rw₂ rw₃ : (f : (a : α) → α) x ≠ x ↔ (f : (a : α) → α) x ≠ x
⊢ x ∈ f.support ↔ (f : (a : α) → α) x ≠ x

Tactic:
rw [support, mem_filter, and_iff_right (mem_univ x)]

Premises used: Finset.mem_univ, Equiv.Perm.support, and_iff_right, Finset.mem_filter
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ x ∉ f.support ↔ (f : (a : α) → α) x = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : ∀ (x : α), x ∈ (↑f.support : Set α) ↔ Membership.mem (γ := Set α) {x : α | (f : (a : α) → α) x ≠ x} x
⊢ (↑f.support : Set α) = {x : α | (f : (a : α) → α) x ≠ x}

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
⊢ x ∈ (↑f.support : Set α) ↔ Membership.mem (γ := Set α) {x : α | (f : (a : α) → α) x ≠ x} x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
simp_rw : (∀ (a : α), a ∈ σ.support ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
simp_rw₁ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ Membership.mem (γ := Finset α) ∅ a) ↔ σ = 1
simp_rw₂ : (∀ (a : α), (σ : (a : α) → α) a ≠ a ↔ False) ↔ σ = 1
simp_rw₃ : (∀ (a : α), ¬(σ : (a : α) → α) a ≠ a) ↔ σ = 1
simp_rw₄ : (∀ (a : α), (σ : (a : α) → α) a = a) ↔ σ = 1
simp_rw₅ :
  (∀ (a : α), (σ : (a : α) → α) a = a) ↔ ∀ (x : α), Eq (α := α) ((σ : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ σ.support = ∅ ↔ σ = 1

Tactic:
simp_rw [Finset.ext_iff, mem_support, Finset.notMem_empty, iff_false, not_not,
    Equiv.Perm.ext_iff, one_apply]

Premises used: iff_false, Classical.not_not, Equiv.Perm.mem_support, Equiv.Perm.ext_iff, Finset.ext_iff, Finset.notMem_empty, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
rw rw₁ : Eq.{u_1 + 1} (α := Perm α) 1 1
⊢ Eq.{u_1 + 1} (α := Finset α) (support 1) ∅

Tactic:
rw [support_eq_empty_iff]

Premises used: Equiv.Perm.support_eq_empty_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
⊢ support (Equiv.refl α) = ∅

Tactic:
support_one

Premises used: Equiv.Perm.support_one
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.support ⊆ g.support
h' : ∀ x ∈ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
⊢ f = g

Tactic:
grind [notMem_support]

Premises used: Equiv.Perm.notMem_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
simp : Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
⊢ Membership.mem (α := α) c.support ((g : (a : α) → α) x : α) ↔ x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not, ← mul_apply]

Premises used: not_iff_not, Equiv.Perm.mem_support, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
hgc : Commute g c
x : α
rw : Eq (α := α) ((g * c : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
rw₁ : Eq (α := α) ((g : (a : α) → α) ((c : (a : α) → α) x : α) : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x
rw₂ rw₃ : (c : (a : α) → α) x = x ↔ (c : (a : α) → α) x = x
⊢ Eq (α := α) ((c * g : (a : α) → α) x : α) ((g : (a : α) → α) x : α) ↔ (c : (a : α) → α) x = x

Tactic:
rw [← hgc, mul_apply, Equiv.apply_eq_iff_eq]

Premises used: Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
x : α
rw : (f : (a : α) → α) x = x ∧ (g : (a : α) → α) x = x → (f : (a : α) → α) ((g : (a : α) → α) x : α) = x
⊢ x ∈ (f * g).support → x ∈ f.support ∪ g.support

Tactic:
rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]

Premises used: Equiv.Perm.mem_support, not_and_or, Finset.mem_union, Equiv.Perm.mul_apply, not_imp_not
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
x : α
hf : (f : (a : α) → α) x = x
hg : (g : (a : α) → α) x = x
rw : (f : (a : α) → α) x = x
rw₁ rw₂ : x = x
⊢ (f : (a : α) → α) ((g : (a : α) → α) x : α) = x

Tactic:
rw [hg, hf]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : x ∈ l.prod.support
contrapose! : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), x ∉ f.support), x ∉ l.prod.support
⊢ ∃ f ∈ l, x ∈ f.support

Tactic:
contrapose! hx
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α) (_ : f ∈ l), x ∉ f.support
simp_rw : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
⊢ x ∉ l.prod.support

Tactic:
simp_rw [mem_support, not_not] at hx ⊢

Premises used: Classical.not_not, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
hx : ∀ (f : Perm α) (_ : Membership.mem (γ := List (Perm α)) [] f), (f : (a : α) → α) x = x
⊢ (List.prod [] : (a : α) → α) x = x

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x
cons : f ∈ f :: l
cons₁ : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x
⊢ ((f :: l).prod : (a : α) → α) x = x

Tactic:
rw [List.prod_cons, mul_apply, ih, hx]

Premises used: Equiv.Perm.mul_apply, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x
⊢ f ∈ f :: l

Tactic:
simp only [List.mem_cons, true_or]

Premises used: true_or, List.mem_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
f : Perm α
l : List (Perm α)
ih : ∀ (hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x), (l.prod : (a : α) → α) x = x
hx : ∀ (f_1 : Perm α) (_ : f_1 ∈ f :: l), (f_1 : (a : α) → α) x = x
⊢ ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x

Tactic:
grind