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 α
f g : Perm α
h : f.Disjoint g
a : α
⊢ a ∈ f.support ∪ g.support → a ∈ (f * g).support
have rw : (f : (a : α) → α) ((g : (a : α) → α) a : α) = a → (f : (a : α) → α) a = a ∧ (g : (a : α) → α) a = a
Tactic: rw [mem_union, mem_support, mem_support, mem_support, mul_apply, ← not_and_or, not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl :
  ∀ (h : List.Pairwise Disjoint tl),
    tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : List.Pairwise Disjoint (hd :: tl)
⊢ (hd :: tl).prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
have h₁ : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
Tactic: rw [List.pairwise_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl :
  ∀ (h : List.Pairwise Disjoint tl),
    tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
h : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ (hd :: tl).prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
have this : hd.Disjoint tl.prod
Tactic: have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ l.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)
have nil : ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
  Eq.{u_1 + 1} (α := Finset α) (support (List.prod []))
    (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
nil :
  ∀ (h : List.Pairwise.{u_1} (α := Perm α) Disjoint []),
    Eq.{u_1 + 1} (α := Finset α) (support (List.prod []))
      (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
⊢ l.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)
have cons : ∀ (hd : Perm α) (tl : List (Perm α))
  (hl :
    ∀ (h : List.Pairwise Disjoint tl),
      tl.prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl))
  (h : List.Pairwise Disjoint (hd :: tl)),
  (hd :: tl).prod.support = List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.pairwise_cons] at h
    have : Disjoint hd tl.prod := disjoint_prod_right _ h.left
    simp [this.support_mul, hl h.right]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun (i : ι) ↦ (k i).support
have hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
Tactic: have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun (i : ι) ↦ (k i).support
have insert : (k i * s.noncommProd k sorry).support = (k i).support ∪ s.biUnion fun (i : ι) ↦ (k i).support
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (k i * s.noncommProd k ⋯).support = (k i).support ∪ s.biUnion fun (i : ι) ↦ (k i).support
have insert : (k i).Disjoint (s.noncommProd k sorry)
Tactic: rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)
have insert : ∀ i_1 ∈ s, (k i).Disjoint (k i_1)
Tactic: apply disjoint_noncommProd_right
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)
have apply : i ∈ (↑(insert i s) : Set ι)
Tactic: apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
hs' : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
apply : i ∈ (↑(insert i s) : Set ι)
⊢ (k i).Disjoint (k j)
have apply₁ : j ∈ (↑(insert i s) : Set ι)
Tactic: apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
have empty : ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
  (noncommProd ∅ k sorry).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (noncommProd ∅ k ⋯).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
⊢ (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (hrec :
    ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
      (s.noncommProd k sorry).support = s.biUnion fun (i : ι) ↦ (k i).support)
  (hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
  ((insert i s).noncommProd k sorry).support = (insert i s).biUnion fun (i : ι) ↦ (k i).support
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
⊢ (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
have empty : ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
  (noncommProd ∅ k sorry).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)
empty :
  ∀ (hs : (↑∅ : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
    (noncommProd ∅ k ⋯).support = Finset.biUnion ∅ fun (i : ι) ↦ (k i).support
⊢ (s.noncommProd k ⋯).support = s.biUnion fun (i : ι) ↦ (k i).support
have insert : ∀ (i : ι) (s : Finset ι) (hi : i ∉ s)
  (hrec :
    ∀ (hs : (↑s : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
      (s.noncommProd k sorry).support = s.biUnion fun (i : ι) ↦ (k i).support)
  (hs : (↑(insert i s) : Set ι).Pairwise fun (i j : ι) ↦ (k i).Disjoint (k j)),
  ((insert i s).noncommProd k sorry).support = (insert i s).biUnion fun (i : ι) ↦ (k i).support
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
have cons : hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)
Tactic: refine (support_mul_le hd tl.prod).trans ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
⊢ l.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)
have nil : LE.le.{u_1} (α := Finset α) (support (List.prod []))
  (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.map_cons, List.foldr_cons]
    refine (support_mul_le hd tl.prod).trans ?_
    exact sup_le_sup le_rfl hl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
nil :
  LE.le.{u_1} (α := Finset α) (support (List.prod []))
    (List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support []))
⊢ l.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support l)
have cons : ∀ (hd : Perm α) (tl : List (Perm α))
  (hl : tl.prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support tl)),
  (hd :: tl).prod.support ≤ List.foldr (fun (x1 x2 : Finset α) ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.map_cons, List.foldr_cons]
    refine (support_mul_le hd tl.prod).trans ?_
    exact sup_le_sup le_rfl hl
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y : α
⊢ (swap x y).support = {x, y} ↔ x ≠ y
have refine : ∀ (h : (swap x y).support = {x, y}), x ≠ y
Tactic: refine ⟨fun h => ?_, fun h => support_swap h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : [x, y, z].Nodup
⊢ (swap x y * swap y z).support = {x, y, z}
have h₁ : ¬(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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)
⊢ (swap x y * swap y z).support = {x, y, z}
have h₁ : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 = {x, y, z}
have a : (swap x y * swap y z).support ≤ {x, y, z}
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
⊢ (swap x y * swap y z).support = {x, y, z}
have a₁ : {x, y, z} ≤ (swap x y * swap y z).support
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 ≤ {x, y, z}
have h₁ : {x, y, z} = (swap x y).support ⊔ (swap y z).support
Tactic: convert! support_mul_le (swap x y) (swap y z) using 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} = (swap x y).support ⊔ (swap y z).support
have h₁ : Eq (α := Finset α) {x, y, z} ({x, y} ⊔ {y, z})
Tactic: rw [support_swap h.left.left, support_swap h.right.left]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
x_1 : α
⊢ Membership.mem (γ := Finset α) {x, y, z} x_1 → x_1 ∈ (swap x y * swap y z).support
have a : x_1 = x ∨ x_1 = y ∨ x_1 = z → x_1 ∈ (swap x y * swap y z).support
Tactic: simp only [mem_insert, mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
⊢ x_1 ∈ f.support \ {x, y} → x_1 ∈ (swap x y * f).support
have simp : ¬(f : (a : α) → α) x_1 = x_1 → ¬(x_1 = x ∨ x_1 = y) → ¬(swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) = x_1
Tactic: simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
    mem_singleton]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y x_1 : α
⊢ ¬(f : (a : α) → α) x_1 = x_1 → ¬(x_1 = x ∨ x_1 = y) → ¬(swap x y : (a : α) → α) ((f : (a : α) → α) x_1 : α) = x_1
have push : (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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (hypothesis)
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
⊢ False
have H₁ : (f : (a : α) → α) x_1 = x_1
Tactic: rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x : α
h : (f : (a : α) → α) ((f : (a : α) → α) x : α) ≠ x
⊢ (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
have pos : ∀ (hx : (f : (a : α) → α) x = x), (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
⊢ (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
have neg : ∀ (hx : ¬(f : (a : α) → α) x = x), (swap x ((f : (a : α) → α) x) * f).support = f.support \ {x}
Tactic: by_cases hx : f x = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
have neg : ∀ (z : α), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: ext z
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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 : α
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
have pos : ∀ (hzx : z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzx : z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
have neg : ∀ (hzx : ¬z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzx : z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
have pos : ∀ (hzf : z = (f : (a : α) → α) x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzf : z = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
have neg : ∀ (hzf : ¬z = (f : (a : α) → α) x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzf : z = f x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
have pos : ∀ (hzfx : (f : (a : α) → α) z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzfx : f z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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}
⊢ z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
have neg : ∀ (hzfx : ¬(f : (a : α) → α) z = x), z ∈ (swap x ((f : (a : α) → α) x) * f).support ↔ z ∈ f.support \ {x}
Tactic: by_cases hzfx : f z = x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x ((f : (a : α) → α) x) * f).support
⊢ y ∈ f.support ∧ y ≠ x
have 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
Tactic: simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Support (goal)
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
⊢ Eq (α := α) ((f : (a : α) → α) x : α) (((hd :: tl).prod : (a : α) → α) x : α)
have 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 : α)
Tactic: rw [List.pairwise_cons] at hl
Cleared hypotheses: hl, x, hx