awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
x : α
hx : ∀ (f : Perm α) (_ : f ∈ l), (f : (a : α) → α) x = x
nil :
  ∀ (hx : ∀ (f : Perm α) (_ : Membership.mem (γ := List (Perm α)) [] f), (f : (a : α) → α) x = x),
    (List.prod [] : (a : α) → α) x = x
cons :
  ∀ (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 :: l).prod : (a : α) → α) x = x
⊢ (l.prod : (a : α) → α) x = x

Tactic:
induction l with
  | nil => rfl
  | cons f l ih =>
    rw [List.prod_cons, mul_apply, ih, hx]
    · simp only [List.mem_cons, true_or]
    grind

Premises used: Finset.cons, true_or, Equiv.Perm.mul_apply, List.mem_cons, List.prod_cons
-- 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 (pow_apply_eq_self_of_apply_eq_self h2 n)

Premises used: Iff.mpr, Equiv.Perm.mem_support, Equiv.Perm.pow_apply_eq_self_of_apply_eq_self, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
simp_rw : ∀ (a : α), a ∈ σ⁻¹.support ↔ a ∈ σ.support
simp_rw₁ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a ≠ a ↔ (σ : (a : α) → α) a ≠ a
simp_rw₂ : ∀ (a : α), (σ⁻¹ : (a : α) → α) a = a ↔ (σ : (a : α) → α) a = a
simp_rw₃ : ∀ (a : α), True
⊢ σ⁻¹.support = σ.support

Tactic:
simp_rw [Finset.ext_iff, mem_support, not_iff_not, inv_eq_iff_eq.trans eq_comm, imp_true_iff]

Premises used: not_iff_not, Equiv.Perm.mem_support, Equiv.Perm.inv_eq_iff_eq, Finset.ext_iff, eq_comm, imp_true_iff, Iff.trans
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
rw : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ x ∈ f.support
rw₁ : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
rw₂ : ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x
rw₃ :
  ¬Eq (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ ¬(f : (a : α) → α) x = x
rw₄ rw₅ : ¬(f : (a : α) → α) x = x ↔ ¬(f : (a : α) → α) x = x
⊢ Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ↔ x ∈ f.support

Tactic:
rw [mem_support, mem_support, Ne, Ne, apply_eq_iff_eq]

Premises used: Equiv.Perm.mem_support, Ne, Equiv.apply_eq_iff_eq
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
pos : ∀ (hx' : x ∈ c.support), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
neg : ∀ (hx' : x ∉ c.support), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
by_cases hx' : x ∈ c.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∈ c.support
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
simp only [hcs hx', hcs (apply_mem_support.mpr hx')]

Premises used: Iff.mpr, Equiv.Perm.apply_mem_support
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
c : Perm α
s : Finset α
hcs : c.support ≤ s
x : α
hx' : x ∉ c.support
neg neg₁ : x ∈ s ↔ x ∈ s
⊢ Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
rw [notMem_support.mp hx']

Premises used: Equiv.Perm.notMem_support, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
simp :
  (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ (ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) = c ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s),
        c.subtypePerm (p := Membership.mem s) hc' = g.subtypePerm (p := Membership.mem s) hg

Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]

Premises used: Subtype.forall, Equiv.ext_iff, Subtype.mk.injEq, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
mp :
  (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) →
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
mpr :
  (c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)) →
    ∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)
⊢ (∀ (x : α),
      Eq (α := α)
        ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
                Perm α) :
              (a : α) → α)
            x :
          α)
        ((c : (a : α) → α) x : α)) ↔
    c.support ≤ s ∧
      ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
        Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
mp : c.support ≤ s
mp₁ :
  ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
    Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
⊢ c.support ≤ s ∧
    ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
      Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ∈ c.support
mp : ∀ (ha' : a ∉ s), False
⊢ a ∈ s

Tactic:
by_contra ha'
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ∈ c.support
ha' : a ∉ s
⊢ a ≠ a

Tactic:
rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha

Premises used: Equiv.Perm.mem_support, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ∈ c.support
ha' : a ∉ s
ha₁ : a ≠ a
⊢ a ∉ s

Tactic:
rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha

Premises used: Equiv.Perm.mem_support, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ≠ a
ha' : a ∉ s
⊢ False

Tactic:
ha rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
a : α
ha : a ≠ a
ha' : a ∉ s
⊢ False

Tactic:
exact ha rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
h :
  ∀ (x : α),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          x :
        α)
      ((c : (a : α) → α) x : α)
hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s
a : α
ha : a ∈ s
mp :
  Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((g : (a : α) → α) a : α)
mp₁ :
  Eq (α := α)
    ((↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) : α) :
      α)
    ((g : (a : α) → α) a : α)
mp₂ mp₃ :
  Eq (α := α)
    ((↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((g : (a : α) → α) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) : α))
            ⋯) :
        α) :
      α)
    ((g : (a : α) → α) a : α)
⊢ Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
h :
  ∀ (hc' : ∀ (x : α), Membership.mem (α := α) s ((c : (a : α) → α) x : α) ↔ x ∈ s) (a : α) (b : a ∈ s),
    Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
a : α
⊢ ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)

Tactic:
specialize h (isInvariant_of_support_le hc)

Premises used: Equiv.Perm.isInvariant_of_support_le
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
a : α
h : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
pos :
  ∀ (ha : a ∈ s),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          a :
        α)
      ((c : (a : α) → α) a : α)
neg :
  ∀ (ha : a ∉ s),
    Eq (α := α)
      ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
              Perm α) :
            (a : α) → α)
          a :
        α)
      ((c : (a : α) → α) a : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
a : α
h : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
ha : a ∈ s
pos :
  Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((g : (a : α) → α) a : α)
pos₁ :
  Eq (α := α)
    ((↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) : α) :
      α)
    ((g : (a : α) → α) a : α)
pos₂ pos₃ :
  Eq (α := α)
    ((↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((g : (a : α) → α) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) : α))
            ⋯) :
        α) :
      α)
    ((g : (a : α) → α) a : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)

Tactic:
rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

Premises used: Equiv.Perm.ofSubtype_apply_of_mem, Equiv.Perm.subtypePerm_apply
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
a : α
h : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
ha : a ∉ s
neg : a ∉ c.support
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)

Tactic:
rw [ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha, eq_comm, ← notMem_support]

Premises used: Equiv.Perm.notMem_support, eq_comm, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
a : α
h : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
ha : a ∉ s
⊢ a ∉ c.support

Tactic:
Finset.notMem_mono hc ha

Premises used: Finset.notMem_mono
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), Membership.mem (α := α) s ((g : (a : α) → α) x : α) ↔ x ∈ s
hc : c.support ≤ s
a : α
h : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
ha : a ∉ s
⊢ a ∉ c.support

Tactic:
exact Finset.notMem_mono hc ha

Premises used: Finset.notMem_mono
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
h :
  ∀ (x : α),
    Membership.mem (γ := Finset α) (support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u)) x ↔
      x ∈ map (Embedding.subtype p) u.support
⊢ support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u) = map (Embedding.subtype p) u.support

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
x : α
h :
  (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
        Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
⊢ Membership.mem (γ := Finset α) (support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u)) x ↔
    x ∈ map (Embedding.subtype p) u.support

Tactic:
simp only [mem_support, ne_eq, Finset.mem_map, Function.Embedding.coe_subtype, Subtype.exists,
    exists_and_right, exists_eq_right, not_iff_comm, not_exists, not_not]

Premises used: Classical.not_not, Equiv.Perm.mem_support, Function.Embedding.coe_subtype, Subtype.exists, not_exists, exists_eq_right, exists_and_right, ne_eq, Finset.mem_map, not_iff_comm
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
x : α
pos :
  ∀ (hx : p x),
    (∀ (x_1 : p x),
        (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
          Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
      (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
neg :
  ∀ (hx : ¬p x),
    (∀ (x_1 : p x),
        (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
          Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
      (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
⊢ (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
        Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x

Tactic:
by_cases hx : p x
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
x : α
hx : p x
⊢ (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
        Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x

Tactic:
simp only [forall_prop_of_true hx, ofSubtype_apply_of_mem u hx, ← Subtype.coe_inj]

Premises used: Subtype.coe_inj, Equiv.Perm.ofSubtype_apply_of_mem, forall_prop_of_true
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) =
        Subtype.mk (p := fun (a : α) ↦ p a) x ⋯) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x

Tactic:
simp only [forall_prop_of_false hx, ofSubtype_apply_of_not_mem u hx]

Premises used: forall_prop_of_false, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
x : α
u : Perm (Subtype p)
⊢ Membership.mem (γ := Finset α) (support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u)) x ↔
    ∃ (hx : p x), Subtype.mk (p := p) x hx ∈ u.support

Tactic:
simp [support_ofSubtype]

Premises used: Equiv.Perm.support_ofSubtype
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s : Set α).Pairwise (Commute on f)
x : β
hx : x ∈ (s.noncommProd f comm).support
contrapose! : ∀ (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support), x ∉ (s.noncommProd f comm).support
⊢ ∃ a ∈ s, x ∈ (f a).support

Tactic:
contrapose! hx
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s : Set α).Pairwise (Commute on f)
x : β
hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support
revert :
  ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
⊢ x ∉ (s.noncommProd f comm).support

Tactic:
revert hx comm s
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
empty :
  ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
    (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support
insert :
  ∀ (a : α) (s : Finset α),
    a ∉ s →
      (∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
          x ∉ (s.noncommProd f comm).support) →
        ∀ {comm : (↑(Insert.insert a s) : Set α).Pairwise (Commute on f)}
          (hx : ∀ (a_3 : α) (_ : a_3 ∈ Insert.insert a s), x ∉ (f a_3).support),
          x ∉ ((Insert.insert a s).noncommProd f comm).support
⊢ ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support

Tactic:
apply Finset.induction
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
    (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
comm : (↑(Insert.insert a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ Insert.insert a s), x ∉ (f a_1).support
insert : x ∉ (f a * s.noncommProd f ⋯).support
⊢ x ∉ ((Insert.insert a s).noncommProd f comm).support

Tactic:
rw [Finset.noncommProd_insert_of_notMem s a f comm ha]

Premises used: Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.GroupTheory.Perm.Support
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih :
  ∀ {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
comm : (↑(Insert.insert a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ Insert.insert a s), x ∉ (f a_1).support
insert : x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support

Tactic:
apply mt (Finset.mem_of_subset (support_mul_le _ _))

Premises used: mt, Equiv.Perm.support_mul_le, Finset.mem_of_subset