awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
g p : Perm α
hp : Membership.mem (γ := Subgroup (Perm α)) (Subgroup.centralizer {g}) p
x : α
⊢ p * g = g * p

Tactic:
simp only [Subgroup.mem_centralizer_singleton_iff] at hp

Premises used: Subgroup.mem_centralizer_singleton_iff
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
rw : Eq (α := α) ((g * p : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₁ : Eq (α := α) ((p * g : (a : α) → α) x : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₂ : Eq (α := α) ((p : (a : α) → α) ((g : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x
rw₃ rw₄ : (g : (a : α) → α) x = x ↔ (g : (a : α) → α) x = x
⊢ Eq (α := α) ((g : (a : α) → α) ((p : (a : α) → α) x : α) : α) ((p : (a : α) → α) x : α) ↔ (g : (a : α) → α) x = x

Tactic:
rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

Premises used: EmbeddingLike.apply_eq_iff_eq, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x),
    (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x =
        x ∨
      (g : (a : α) → α) x = x
neg :
  ∀ (hx : x ∉ fixedPoints (⇑g : (a : α) → α)),
    (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                  (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
                u :
              Perm α) :
            (a : α) → α)
          x =
        x ∨
      (g : (a : α) → α) x = x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x

Tactic:
by_cases hx : x ∈ Function.fixedPoints g

Premises used: Function.fixedPoints, DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x
pos : (g : (a : α) → α) x = x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x

Tactic:
right
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x
⊢ (g : (a : α) → α) x = x

Tactic:
hx

Premises used: Set.Mem, setOf, Function.fixedPoints, Function.IsFixedPt
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x
⊢ (g : (a : α) → α) x = x

Tactic:
exact hx
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : x ∉ fixedPoints (⇑g : (a : α) → α)
neg :
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
            u :
          Perm α) :
        (a : α) → α)
      x =
    x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
                (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
              u :
            Perm α) :
          (a : α) → α)
        x =
      x ∨
    (g : (a : α) → α) x = x

Tactic:
left
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
g : Perm α
u : Perm (↑(fixedPoints (⇑g : (a : α) → α)) : Type u)
x : α
hx : x ∉ fixedPoints (⇑g : (a : α) → α)
neg neg₁ : x = x
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑g : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑g : (a : α) → α) }) → Perm α)
            u :
          Perm α) :
        (a : α) → α)
      x =
    x

Tactic:
rw [ofSubtype_apply_of_not_mem u hx]

Premises used: Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
obtain : ∀ (m : ℕ) (hm : (σ ^ n) ^ m = σ), (σ ^ n).support = σ.support
⊢ (σ ^ n).support = σ.support

Tactic:
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h

Premises used: exists_pow_eq_self_of_coprime
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = σ.support

Tactic:
le_antisymm (support_pow_le σ n)
      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Premises used: Equiv.Perm.support, Equiv.Perm.support_pow_le, ge_of_eq, congr_arg, le_antisymm, HPow.hPow, le_trans
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = σ.support

Tactic:
exact
    le_antisymm (support_pow_le σ n)
      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Premises used: Equiv.Perm.support, Equiv.Perm.support_pow_le, ge_of_eq, congr_arg, le_antisymm, HPow.hPow, le_trans
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
rw :
  ∀ (a : α),
    Membership.mem (γ := Finset α)
        (support
          ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x))
        a →
      ∀ b ∈ σ.support, a ≠ b
⊢ _root_.Disjoint
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    σ.support

Tactic:
rw [Finset.disjoint_iff_ne]

Premises used: Finset.disjoint_iff_ne
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  Membership.mem (γ := Finset α)
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    a
hb : a ∈ σ.support
⊢ (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x :
          Perm α) :
        (a : α) → α)
      a ≠
    a

Tactic:
rw [mem_support] at ha hb

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  Membership.mem (γ := Finset α)
    (support
      ((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
          (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
        x))
    a
hb : a ∈ σ.support
ha₁ :
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x :
          Perm α) :
        (a : α) → α)
      a ≠
    a
⊢ (σ : (a : α) → α) a ≠ a

Tactic:
rw [mem_support] at ha hb

Premises used: Equiv.Perm.mem_support
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x :
          Perm α) :
        (a : α) → α)
      a ≠
    a
hb : (σ : (a : α) → α) a ≠ a
⊢ False

Tactic:
ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

Premises used: Function.mem_fixedPoints_iff, mt, Iff.mp, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ : Perm α
x : Perm (↑(fixedPoints (⇑σ : (a : α) → α)) : Type u)
a : α
ha :
  (((ofSubtype (p := fun (x : α) ↦ Membership.mem (γ := Set α) (fixedPoints (⇑σ : (a : α) → α)) x) :
              (a : Perm { x : α // x ∈ fixedPoints (⇑σ : (a : α) → α) }) → Perm α)
            x :
          Perm α) :
        (a : α) → α)
      a ≠
    a
hb : (σ : (a : α) → α) a ≠ a
⊢ False

Tactic:
exact ha (ofSubtype_apply_of_not_mem x (mt Function.mem_fixedPoints_iff.mp hb))

Premises used: Function.mem_fixedPoints_iff, mt, Iff.mp, Equiv.Perm.ofSubtype_apply_of_not_mem
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
rw : H ⊓ K ≤ ⊥
⊢ _root_.Disjoint H K

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
this :
  ∀ (hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))) (hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))),
    Membership.mem (γ := Subgroup (Perm α)) ⊥ x
⊢ x ∈ H ⊓ K → Membership.mem (γ := Subgroup (Perm α)) ⊥ x

Tactic:
⟨hx1, hx2⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
⊢ _root_.Disjoint x.support x.support

Tactic:
specialize h x hx1 x hx2
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
H K : Subgroup (Perm α)
x : Perm α
hx1 : x ∈ (↑H.toSubmonoid : Set (Perm α))
hx2 : x ∈ (↑K.toSubmonoid : Set (Perm α))
h : _root_.Disjoint x.support x.support
rwa : ∀ (h : x.support = ⊥), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
rwa₁ : ∀ (h : x.support = ∅), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : x = 1), Membership.mem (γ := Subgroup (Perm α)) ⊥ x
⊢ Membership.mem (γ := Subgroup (Perm α)) ⊥ x

Tactic:
rwa [disjoint_self, Finset.bot_eq_empty, support_eq_empty_iff] at h

Premises used: Finset.bot_eq_empty, Equiv.Perm.support_eq_empty_iff, disjoint_self
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
mem : ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
one : (↑(support 1) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
mul :
  ∀ (x y : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x)
    (hy : Membership.mem (γ := Subgroup (Perm α)) (closure S) y),
    (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) →
      (↑y.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑(x * y).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
inv :
  ∀ (x : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x),
    (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑x⁻¹.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a → (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
apply closure_induction
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
⊢ ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl

Premises used: Set.subset_iUnion₂_of_subset, subset_rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
⊢ ∀ (x : Perm α) (hx : x ∈ S), (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
exact fun x hx ↦ Set.subset_iUnion₂_of_subset x hx subset_rfl

Premises used: Set.subset_iUnion₂_of_subset, subset_rfl
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
⊢ (↑(support 1) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑(a * b).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
(Finset.coe_subset.mpr (support_mul_le a b)).trans ?_

Premises used: Iff.mpr, setOf, HasSubset.Subset.trans, Equiv.Perm.support_mul_le, Finset.coe_subset
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
mul : (↑(a.support ⊔ b.support) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑(a * b).support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
refine (Finset.coe_subset.mpr (support_mul_le a b)).trans ?_

Premises used: Iff.mpr, HasSubset.Subset.trans, Equiv.Perm.support_mul_le, Finset.coe_subset
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
mul : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) ∧ (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑(a.support ⊔ b.support) : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]

Premises used: Set.union_subset_iff, Finset.sup_eq_union, Finset.coe_union
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) ∧ (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
⟨hc, hd⟩

Premises used: And.intro
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
a b : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
hb : Membership.mem (γ := Subgroup (Perm α)) (closure S) b
hc : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
hd : (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) ∧ (↑b.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
exact ⟨hc, hd⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S : Set (Perm α)
⊢ ∀ (x : Perm α) (hx : Membership.mem (γ := Subgroup (Perm α)) (closure S) x),
    (↑x.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α) → (↑x⁻¹.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
simp only [support_inv, imp_self, implies_true]

Premises used: Equiv.Perm.support_inv, imp_self, implies_true
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
⊢ (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)

Tactic:
have key1 := support_closure_subset_union S a ha
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
⊢ (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)

Tactic:
have key2 := support_closure_subset_union T b hb
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
⊢ ∀ (h : _root_.Disjoint.{u} (α := Set α) (⋃ b ∈ S, (↑b.support : Set α)) (⋃ b ∈ T, (↑b.support : Set α))),
    _root_.Disjoint (↑a.support : Set α) (↑b.support : Set α)

Tactic:
have key := Set.disjoint_of_subset key1 key2
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
key :
  ∀ (h : _root_.Disjoint.{u} (α := Set α) (⋃ b ∈ S, (↑b.support : Set α)) (⋃ b ∈ T, (↑b.support : Set α))),
    _root_.Disjoint (↑a.support : Set α) (↑b.support : Set α)
⊢ ∀ (h : ∀ (i : Perm α) (i_1 : i ∈ S) (i_2 : Perm α) (i_3 : i_2 ∈ T), _root_.Disjoint i.support i_2.support),
    _root_.Disjoint a.support b.support

Tactic:
simp_rw [Set.disjoint_iUnion_left, Set.disjoint_iUnion_right, Finset.disjoint_coe] at key

Premises used: Finset.disjoint_coe, Set.disjoint_iUnion_left, Set.disjoint_iUnion_right
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
key :
  ∀ (h : ∀ (i : Perm α) (i_1 : i ∈ S) (i_2 : Perm α) (i_3 : i_2 ∈ T), _root_.Disjoint i.support i_2.support),
    _root_.Disjoint a.support b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
key h
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
a : Perm α
ha : Membership.mem (γ := Subgroup (Perm α)) (closure S) a
b : Perm α
hb : Membership.mem (γ := Subgroup (Perm α)) (closure T) b
key1 : (↑a.support : Set α) ⊆ ⋃ b ∈ S, (↑b.support : Set α)
key2 : (↑b.support : Set α) ⊆ ⋃ b ∈ T, (↑b.support : Set α)
key :
  ∀ (h : ∀ (i : Perm α) (i_1 : i ∈ S) (i_2 : Perm α) (i_3 : i_2 ∈ T), _root_.Disjoint i.support i_2.support),
    _root_.Disjoint a.support b.support
⊢ _root_.Disjoint a.support b.support

Tactic:
exact key h
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
h₁ :
  ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a →
      ∀ (b : Perm α), Membership.mem (γ := Subgroup (Perm α)) (closure T) b → _root_.Disjoint a.support b.support
⊢ _root_.Disjoint (α := Subgroup (Perm α)) (closure S) (closure T)

Tactic:
apply disjoint_of_disjoint_support

Premises used: Equiv.Perm.disjoint_of_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h h₁ : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ (a : Perm α),
    Membership.mem (γ := Subgroup (Perm α)) (closure S) a →
      ∀ (b : Perm α), Membership.mem (γ := Subgroup (Perm α)) (closure T) b → _root_.Disjoint a.support b.support

Tactic:
apply disjoint_support_closure_of_disjoint_support

Premises used: Equiv.Perm.disjoint_support_closure_of_disjoint_support
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support

Tactic:
h
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
S T : Set (Perm α)
h : ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support
⊢ ∀ a ∈ S, ∀ b ∈ T, _root_.Disjoint a.support b.support

Tactic:
exact h
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
mp :
  Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g →
    (↑g.support : Set α) ⊆ setOf p
mpr :
  (↑g.support : Set α) ⊆ setOf p →
    Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g ↔
    (↑g.support : Set α) ⊆ setOf p

Tactic:
constructor
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
k : Perm (Subtype p)
x : α
mp : (∃ (hx : p x), Subtype.mk (p := p) x hx ∈ k.support) → p x
⊢ x ∈ (↑(support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) k)) : Set α) → x ∈ setOf p

Tactic:
simp only [Finset.mem_coe, mem_support_ofSubtype, Set.mem_setOf_eq]

Premises used: Equiv.Perm.mem_support_ofSubtype, Set.mem_setOf_eq, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
k : Perm (Subtype p)
x : α
⊢ (∃ (hx : p x), Subtype.mk (p := p) x hx ∈ k.support) → p x

Tactic:
fun ⟨hx, _⟩ ↦ hx

Premises used: _private.0.Equiv.Perm.mem_range_ofSubtype_iff.match_2
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
k : Perm (Subtype p)
x : α
⊢ (∃ (hx : p x), Subtype.mk (p := p) x hx ∈ k.support) → p x

Tactic:
exact fun ⟨hx, _⟩ ↦ hx
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g

Tactic:
⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩

Premises used: Iff.mpr, Set.Mem, Equiv.Perm.mem_support, setOf, Equiv.Perm.subtypePerm, Equiv.Perm.ofSubtype_subtypePerm, Exists.intro, Set.range