awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α)
⊢ Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
have mp₂ : Eq (α := α)
  ((↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((g : (a : α) → α) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) : α)) sorry) :
      α) :
    α)
  ((g : (a : α) → α) a : α)
Tactic: rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
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 : α
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have h₁ : ∀ (a : α) (b : a ∈ s), Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)
Tactic: specialize h (isInvariant_of_support_le hc)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have 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 : α)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have 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 : α)
Tactic: by_cases ha : a ∈ s
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have 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 : α)
Tactic: rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have pos₁ : Eq (α := α)
  ((↑((g.subtypePerm (p := Membership.mem s) hg : (a : ↥s) → ↥s) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha)) : α) : α)
  ((g : (a : α) → α) a : α)
Tactic: rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α)
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have pos₂ : Eq (α := α)
  ((↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((g : (a : α) → α) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) : α)) sorry) :
      α) :
    α)
  ((g : (a : α) → α) a : α)
Tactic: rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ Eq (α := α)
    ((((ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm ↥s) → Perm α) (g.subtypePerm (p := Membership.mem s) hg) :
            Perm α) :
          (a : α) → α)
        a :
      α)
    ((c : (a : α) → α) a : α)
have neg : a ∉ c.support
Tactic: rw [ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha, eq_comm, ← notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
⊢ support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u) = map (Embedding.subtype p) u.support
have h : ∀ (x : α),
  Membership.mem (γ := Finset α) (support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u)) x ↔
    x ∈ map (Embedding.subtype p) u.support
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype p)
x : α
⊢ Membership.mem (γ := Finset α) (support ((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u)) x ↔
    x ∈ map (Embedding.subtype p) u.support
have h : (∀ (x_1 : p x),
    (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x sorry) =
      Subtype.mk (p := fun (a : α) ↦ p a) x sorry) ↔
  (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
u : Perm (Subtype 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
have pos : ∀ (hx : p x),
  (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x sorry) =
        Subtype.mk (p := fun (a : α) ↦ p a) x sorry) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ (∀ (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
have neg : ∀ (hx : ¬p x),
  (∀ (x_1 : p x),
      (u : (a : Subtype p) → Subtype p) (Subtype.mk (p := fun (a : α) ↦ p a) x sorry) =
        Subtype.mk (p := fun (a : α) ↦ p a) x sorry) ↔
    (((ofSubtype (p := p) : (a : Perm (Subtype p)) → Perm α) u : Perm α) : (a : α) → α) x = x
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ ∃ a ∈ s, x ∈ (f a).support
have contrapose! : ∀ (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support), x ∉ (s.noncommProd f comm).support
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ x ∉ (s.noncommProd f comm).support
have revert : ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
  x ∉ (s.noncommProd f comm).support
Tactic: revert hx comm s
Cleared hypotheses: s, comm, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_2
β : Type u_3
inst : DecidableEq β
inst_1 : Fintype β
f : α → Perm β
x : β
⊢ ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
have empty : ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
  (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
    x ∉ (s.noncommProd f comm).support
have 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 a s) : Set α).Pairwise (Commute on f)}
        (hx : ∀ (a_3 : α) (_ : a_3 ∈ insert a s), x ∉ (f a_3).support), x ∉ ((insert a s).noncommProd f comm).support
Tactic: apply Finset.induction
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ insert a s), x ∉ (f a_1).support
⊢ x ∉ ((insert a s).noncommProd f comm).support
have insert : x ∉ (f a * s.noncommProd f sorry).support
Tactic: rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ insert a s), x ∉ (f a_1).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support
have insert : x ∉ (f a).support ⊔ (s.noncommProd f sorry).support
Tactic: apply mt (Finset.mem_of_subset (support_mul_le _ _))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 a s) : Set α).Pairwise (Commute on f)
hs : ∀ (a_1 : α) (_ : a_1 ∈ insert a s), x ∉ (f a_1).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support
have insert : x ∉ (f a).support ∧ x ∉ (s.noncommProd f sorry).support
Tactic: rw [Finset.sup_eq_union, Finset.notMem_union]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ x ∉ (s.noncommProd f comm).support
have revert : ∀ {s : Finset α} {comm : (↑s : Set α).Pairwise (Commute on f)} (hx : ∀ (a : α) (_ : a ∈ s), x ∉ (f a).support),
  x ∉ (s.noncommProd f comm).support
Tactic: classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩
Cleared hypotheses: s, comm, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
have empty : ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
  (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support
Tactic: classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩
Cleared hypotheses: s, comm, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
empty :
  ∀ {comm : (↑∅ : Set α).Pairwise (Commute on f)}
    (hx : ∀ (a : α) (_ : Membership.mem (γ := Finset α) ∅ a), x ∉ (f a).support), x ∉ (noncommProd ∅ f comm).support
⊢ x ∉ (s.noncommProd f comm).support
have 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 a s) : Set α).Pairwise (Commute on f)}
        (hx : ∀ (a_3 : α) (_ : a_3 ∈ insert a s), x ∉ (f a_3).support), x ∉ ((insert a s).noncommProd f comm).support
Tactic: classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩
Cleared hypotheses: s, comm, hx
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
⊢ Eq (α := α) ((f ^ (k + 1) : (a : α) → α) x : α) ((g ^ (k + 1) : (a : α) → α) x : α)
have succ : Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
Tactic: rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
⊢ Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
have succ : Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧
  Membership.mem (α := α) g.support ((g : (a : α) → α) x : α)
Tactic: rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
succ :
  Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧
    Membership.mem (α := α) g.support ((g : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
have succ₁ : Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧ x ∈ g.support
Tactic: rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
succ :
  Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧
    Membership.mem (α := α) g.support ((g : (a : α) → α) x : α)
succ₁ : Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧ x ∈ g.support
⊢ Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
have succ₂ : Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ∧ x ∈ g.support
Tactic: rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
x : α
hx : x ∈ f.support ∩ g.support
succ :
  Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧
    Membership.mem (α := α) g.support ((g : (a : α) → α) x : α)
succ₁ : Membership.mem (α := α) f.support ((g : (a : α) → α) x : α) ∧ x ∈ g.support
succ₂ : Membership.mem (α := α) f.support ((f : (a : α) → α) x : α) ∧ x ∈ g.support
⊢ Membership.mem (α := α) (f.support ∩ g.support) ((g : (a : α) → α) x : α)
have succ₃ : x ∈ f.support ∧ x ∈ g.support
Tactic: rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
⊢ ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
have zero : ∀ x ∈ f.support ∩ g.support,
  Eq (α := α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) g 0 : (a : α) → α) x : α)
Tactic: induction k with
  | zero => simp
  | succ k hk =>
    intro x hx
    rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
    rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f : (a : α) → α) x : α) ((g : (a : α) → α) x : α)
k : ℕ
zero :
  ∀ x ∈ f.support ∩ g.support,
    Eq (α := α) ((HPow.hPow (β := ℕ) f 0 : (a : α) → α) x : α) ((HPow.hPow (β := ℕ) g 0 : (a : α) → α) x : α)
⊢ ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)
have succ : ∀ (k : ℕ) (hk : ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ k : (a : α) → α) x : α) ((g ^ k : (a : α) → α) x : α)),
  ∀ x ∈ f.support ∩ g.support, Eq (α := α) ((f ^ (k + 1) : (a : α) → α) x : α) ((g ^ (k + 1) : (a : α) → α) x : α)
Tactic: induction k with
  | zero => simp
  | succ k hk =>
    intro x hx
    rw [pow_succ, mul_apply, pow_succ, mul_apply, h _ hx, hk]
    rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ (f * g).support = f.support ∪ g.support
have refine : ∀ a ∈ f.support ∪ g.support, a ∈ (f * g).support
Tactic: refine le_antisymm (support_mul_le _ _) fun a => ?_