awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
n : ℤ
⊢ (σ ^ n).support ≤ σ.support

Tactic:
fun _ h1 =>
  mem_support.mpr fun h2 => mem_support.mp h1 (zpow_apply_eq_self_of_apply_eq_self h2 n)

Premises used: Iff.mpr, Equiv.Perm.mem_support, Equiv.Perm.zpow_apply_eq_self_of_apply_eq_self, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
h : x ≠ y
⊢ (swap x y).support = {x, y}

Tactic:
grind [support]

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
⊢ (swap x y).support = {x, y} ↔ x ≠ y

Tactic:
⟨fun h => ?_, fun h => support_swap h⟩

Premises used: Iff.intro, Equiv.Perm.support_swap
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
refine : ∀ (h : (swap x y).support = {x, y}), x ≠ y
⊢ (swap x y).support = {x, y} ↔ x ≠ y

Tactic:
refine ⟨fun h => ?_, fun h => support_swap h⟩
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x : α
h : (swap x x).support = {x, x}
⊢ False

Tactic:
simp [Finset.ext_iff] at h

Premises used: Finset.ext_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : [x, y, z].Nodup
⊢ ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)

Tactic:
simp only [List.not_mem_nil, and_true, List.mem_cons, not_false_iff, List.nodup_cons,
    and_self_iff, List.nodup_nil] at h

Premises used: and_true, List.nodup_nil, List.nodup_cons, and_self_iff, List.mem_cons, not_false_iff, List.not_mem_nil
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
a : (swap x y * swap y z).support ≤ {x, y, z}
a₁ : {x, y, z} ≤ (swap x y * swap y z).support
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ (swap x y * swap y z).support ≤ (swap x y).support ⊔ (swap y z).support

Tactic:
support_mul_le (swap x y) (swap y z)

Premises used: Equiv.swap, Equiv.Perm.support_mul_le
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
h₁ : {x, y, z} = (swap x y).support ⊔ (swap y z).support
⊢ (swap x y * swap y z).support ≤ {x, y, z}

Tactic:
convert! support_mul_le (swap x y) (swap y z) using 1

Premises used: Equiv.swap, Equiv.Perm.support_mul_le
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
h₁ : Eq (α := Finset α) {x, y, z} ({x, y} ⊔ {y, z})
⊢ {x, y, z} = (swap x y).support ⊔ (swap y z).support

Tactic:
rw [support_swap h.left.left, support_swap h.right.left]

Premises used: And.right, And.left, Equiv.Perm.support_swap
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ Eq (α := Finset α) {x, y, z} ({x, y} ⊔ {y, z})

Tactic:
simp [-Finset.union_singleton]

Premises used: Finset.union_singleton
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
x_1 : α
a : x_1 = x ∨ x_1 = y ∨ x_1 = z → x_1 ∈ (swap x y * swap y z).support
⊢ Membership.mem (γ := Finset α) {x, y, z} x_1 → x_1 ∈ (swap x y * swap y z).support

Tactic:
simp only [mem_insert, mem_singleton]

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
y z x : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ x ∈ (swap x y * swap y z).support

Tactic:
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.right, And.left, And.symm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x z x_1 : α
h : (x ≠ x_1 ∧ x ≠ z ∧ True) ∧ x_1 ≠ z ∧ True
⊢ x_1 ∈ (swap x x_1 * swap x_1 z).support

Tactic:
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.right, And.left, And.symm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ z ∈ (swap x y * swap y z).support

Tactic:
simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

Premises used: Ne.symm, Equiv.swap_apply_of_ne_of_ne, And.right, And.left, And.symm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
simp : ¬(f : (a : α) → α) x_1 = x_1 → ¬(x_1 = x ∨ x_1 = y) → ¬(swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) = x_1
⊢ x_1 ∈ f.support \ {x, y} → x_1 ∈ (swap x y * f).support

Tactic:
simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
    mem_singleton]

Premises used: Finset.mem_singleton, Equiv.Perm.coe_mul, and_imp, Equiv.Perm.mem_support, Finset.mem_insert, Ne, Finset.mem_sdiff, Function.comp_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
push : (f : (a : α) → α) x_1 ≠ x_1 → x_1 ≠ x ∧ x_1 ≠ y → (swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) ≠ x_1
⊢ ¬(f : (a : α) → α) x_1 = x_1 → ¬(x_1 = x ∨ x_1 = y) → ¬(swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) = x_1

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
ha : (f : (a : α) → α) x_1 ≠ x_1
hx : x_1 ≠ x
hy : x_1 ≠ y
H : (swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) = x_1
⊢ (f : (a : α) → α) x_1 = x_1

Tactic:
rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H

Premises used: Equiv.swap_apply_of_ne_of_ne, Equiv.swap_apply_eq_iff
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
ha : (f : (a : α) → α) x_1 ≠ x_1
hx : x_1 ≠ x
hy : x_1 ≠ y
H : (f : (a : α) → α) x_1 = x_1
⊢ False

Tactic:
ha H
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
ha : (f : (a : α) → α) x_1 ≠ x_1
hx : x_1 ≠ x
hy : x_1 ≠ y
H : (f : (a : α) → α) x_1 = x_1
⊢ False

Tactic:
exact ha H
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
pos : ∀ (hx : (f : (a : α) → α) x = x), (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
⊢ (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}

Tactic:
by_cases hx : f x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : (f : (a : α) → α) x = x
⊢ (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}

Tactic:
simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem, pull_end]

Premises used: Iff.mpr, Finset.sdiff_singleton_eq_erase, Equiv.Perm.notMem_support, Finset.erase_eq_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
neg : ∀ (z : α), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
⊢ (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}

Tactic:
ext z
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
pos : ∀ (hzx : z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
neg : ∀ (hzx : ¬z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
by_cases hzx : z = x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : z = x
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
simp [hzx]
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : ¬z = x
pos : ∀ (hzf : z = (f : (a : α) → α) x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
neg : ∀ (hzf : ¬z = (f : (a : α) → α) x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
by_cases hzf : z = f x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : ¬z = x
hzf : z = (f : (a : α) → α) x
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
simp [hzf, hx, h, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : ¬z = x
hzf : ¬z = (f : (a : α) → α) x
pos : ∀ (hzfx : (f : (a : α) → α) z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
neg : ∀ (hzfx : ¬(f : (a : α) → α) z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
by_cases hzfx : f z = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : ¬z = x
hzf : ¬z = (f : (a : α) → α) x
hzfx : (f : (a : α) → α) z = x
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]

Premises used: Ne.symm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
hx : ¬(f : (a : α) → α) x = x
z : α
hzx : ¬z = x
hzf : ¬z = (f : (a : α) → α) x
hzfx : ¬(f : (a : α) → α) z = x
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
simp [hzx, hzfx, f.injective.ne hzx, swap_apply_of_ne_of_ne]

Premises used: Function.Injective.ne, Equiv.swap_apply_of_ne_of_ne, Equiv.injective
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x ((f : (a : α) → α) x) * f).support
simp :
  ∀ (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
⊢ y ∈ f.support ∧ y ≠ x

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

Premises used: Equiv.Perm.mem_support, 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 α
inst_1 : Fintype α
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
inst : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
x_1 : α
⊢ (swap x y : (a : α) → α) x_1 = x_1 ∨ (swap z t : (a : α) → α) x_1 = x_1

Tactic:
grind
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
x : α
hx : x ∈ f.support
⊢ x ∉ g.support

Tactic:
disjoint_left.mp h.disjoint_support hx

Premises used: Equiv.Perm.Disjoint.disjoint_support, Iff.mp, Finset.disjoint_left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : Membership.mem (γ := List (Perm α)) [] f
hl : List.Pairwise.{u_1} (α := Perm α) Disjoint []
⊢ ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((List.prod [] : (a : α) → α) x : α)

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
x : α
hx : x ∈ f.support
cons :
  ∀ (hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl) (x : α) (hx : x ∈ f.support),
    Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)

Tactic:
rw [List.pairwise_cons] at hl

Premises used: List.pairwise_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f ∈ hd :: tl
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
cons :
  ∀ (h : f = hd ∨ f ∈ tl) (hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl) (x : α) (hx : x ∈ f.support),
    Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)

Tactic:
rw [List.mem_cons] at h

Premises used: List.mem_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
h : f = hd ∨ f ∈ tl
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
cons :
  ∀ (hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl),
    Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)
cons₁ : ∀ (h : f ∈ tl), Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
cons : Eq (α := α) ((f : (a : α) → α) x : α) ((f * tl.prod : (a : α) → α) x : α)
cons₁ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) ((tl.prod : (a : α) → α) x : α) : α)
cons₂ cons₃ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((f :: tl).prod : (a : α) → α) x : α)

Tactic:
rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]

Premises used: Equiv.Perm.Disjoint.mem_imp, Equiv.Perm.notMem_support, Equiv.Perm.disjoint_prod_right, And.left, Iff.mp, Equiv.Perm.mul_apply, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
cons : ((f : (a : α) → α) x : α) ∉ hd.support
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)

Tactic:
rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]

Premises used: Equiv.Perm.notMem_support, eq_comm, And.right, Equiv.Perm.mul_apply, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ ((f : (a : α) → α) x : α) ∉ hd.support

Tactic:
(hl.left _ h).symm.mem_imp ?_

Premises used: Equiv.Perm.Disjoint.mem_imp, Equiv.Perm.Disjoint.symm, And.left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
cons : Membership.mem (α := α) f.support ((f : (a : α) → α) x : α)
⊢ ((f : (a : α) → α) x : α) ∉ hd.support

Tactic:
refine (hl.left _ h).symm.mem_imp ?_

Premises used: Equiv.Perm.Disjoint.mem_imp, Equiv.Perm.Disjoint.symm, And.left
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f hd : Perm α
tl : List (Perm α)
IH :
  ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α)
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α)

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
nil :
  ∀ (h : Membership.mem (γ := List (Perm α)) [] f) (hl : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((List.prod [] : (a : α) → α) x : α)
cons :
  ∀ (hd : Perm α) (tl : List (Perm α))
    (IH :
      ∀ (h : f ∈ tl) (hl : List.Pairwise Disjoint tl),
        ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((tl.prod : (a : α) → α) x : α))
    (h : f ∈ hd :: tl) (hl : List.Pairwise Disjoint (hd :: tl)),
    ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
⊢ ∀ x ∈ f.support, Eq (α := α) ((f : (a : α) → α) x : α) ((l.prod : (a : α) → α) x : α)

Tactic:
induction l with
  | nil => simp at h
  | cons hd tl IH =>
    intro x hx
    rw [List.pairwise_cons] at hl
    rw [List.mem_cons] at h
    rcases h with (rfl | h)
    · rw [List.prod_cons, mul_apply,
        notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)]
    · rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]
      refine (hl.left _ h).symm.mem_imp ?_
      simpa using hx

Premises used: Equiv.Perm.notMem_support, Finset.cons, eq_comm, List.pairwise_cons, Equiv.Perm.mul_apply, List.mem_cons, List.prod_cons, rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ≤ f.support
hg : y.support ≤ g.support
rw :
  ∀ (h : _root_.Disjoint f.support g.support) (hf : x.support ≤ f.support) (hg : y.support ≤ g.support),
    _root_.Disjoint x.support y.support
⊢ x.Disjoint y

Tactic:
rw [disjoint_iff_disjoint_support] at h ⊢

Premises used: Equiv.Perm.disjoint_iff_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g x y : Perm α
h : _root_.Disjoint f.support g.support
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ _root_.Disjoint x.support y.support

Tactic:
h.mono hf hg

Premises used: Disjoint.mono
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g x y : Perm α
h : _root_.Disjoint f.support g.support
hf : x.support ≤ f.support
hg : y.support ≤ g.support
⊢ _root_.Disjoint x.support y.support

Tactic:
exact h.mono hf hg

Premises used: Disjoint.mono
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
x : α
hx : x ∈ f.support
rwa : (l.prod : (a : α) → α) x ≠ x
rwa₁ : (f : (a : α) → α) x ≠ x
rwa₂ rwa₃ rwa₄ rwa₅ : x ∈ f.support
⊢ x ∈ l.prod.support

Tactic:
rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

Premises used: Equiv.Perm.eq_on_support_mem_disjoint, Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
h : ∀ (b : β), b ∈ (g.extendDomain (p := p) f).support ↔ b ∈ map (f.asEmbedding (p := p)) g.support
⊢ (g.extendDomain (p := p) f).support = map (f.asEmbedding (p := p)) g.support

Tactic:
ext b
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
h :
  ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
⊢ b ∈ (g.extendDomain (p := p) f).support ↔ b ∈ map (f.asEmbedding (p := p)) g.support

Tactic:
simp only [mem_map, Ne,
    mem_support]

Premises used: Equiv.Perm.mem_support, Ne, Finset.mem_map
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
β : Type u_2
inst_2 : DecidableEq β
inst_3 : Fintype β
p : β → Prop
inst_4 : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
b : β
pos :
  ∀ (pb : p b),
    ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
      ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
neg :
  ∀ (pb : ¬p b),
    ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
      ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b
⊢ ¬(g.extendDomain (p := p) f : (a : β) → β) b = b ↔
    ∃ (a : α), ¬(g : (a : α) → α) a = a ∧ (f.asEmbedding (p := p) : (a : α) → β) a = b

Tactic:
by_cases pb : p b