awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
neg₁ : Equiv.trans (Equiv.swap a ((f : (a : α) → α) a)) (Equiv.swap a ((f : (a : α) → α) a)) * f = f
neg₂ : Equiv.refl α * f = f
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
have neg₃ : 1 * f = f
Tactic: rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l
hfa : ¬(f : (a : α) → α) a = a
hfa' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) a : α) : α) ((f : (a : α) → α) a : α)
this : ∀ (x : α), (Equiv.swap a ((f : (a : α) → α) a) * f : (a : α) → α) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
neg : Equiv.swap a ((f : (a : α) → α) a) * Equiv.swap a ((f : (a : α) → α) a) * f = f
neg₁ : Equiv.trans (Equiv.swap a ((f : (a : α) → α) a)) (Equiv.swap a ((f : (a : α) → α) a)) * f = f
neg₂ : Equiv.refl α * f = f
neg₃ : 1 * f = f
⊢ Equiv.swap a ((f : (a : α) → α) a) * (Equiv.swap a ((f : (a : α) → α) a) * f) = f
have neg₄ : f = f
Tactic: rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l
⊢ f ∈ permsOfList l
have nil : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x),
  Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
Tactic: induction l generalizing f with
  | nil =>
    simp only [not_mem_nil] at h
    exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)
  | cons a l IH =>
  by_cases hfa : f a = a
  · refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
    split_ifs at hx with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]
  refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
Cleared hypotheses: l, f, h
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
f : Equiv.Perm α
h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l
nil :
  ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → Membership.mem (γ := List α) [] x),
    Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
⊢ f ∈ permsOfList l
have cons : ∀ (a : α) (l : List α) (IH : ∀ {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ l), f ∈ permsOfList l)
  {f : Equiv.Perm α} (h : ∀ (x : α), (f : (a : α) → α) x ≠ x → x ∈ a :: l), f ∈ permsOfList (a :: l)
Tactic: induction l generalizing f with
  | nil =>
    simp only [not_mem_nil] at h
    exact List.mem_singleton.2 (Equiv.ext fun x => Decidable.byContradiction <| h x)
  | cons a l IH =>
  by_cases hfa : f a = a
  · refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))
    rintro rfl
    exact hx hfa
  have hfa' : f (f a) ≠ f a := mt (fun h => f.injective h) hfa
  have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
    intro x hx
    have hxa : x ≠ a := by
      rintro rfl
      apply hx
      simp only [mul_apply, swap_apply_right]
    refine List.mem_of_ne_of_mem hxa (h x fun h => ?_)
    simp only [mul_apply, swap_apply_def, mul_apply, Ne, apply_eq_iff_eq] at hx
    split_ifs at hx with h_1
    exacts [hxa (h.symm.trans h_1), hx h]
  suffices f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f by
    simpa only [permsOfList, exists_prop, List.mem_map, mem_append, List.mem_flatMap]
  refine or_iff_not_imp_left.2 fun _hfl => ⟨f a, ?_, Equiv.swap a (f a) * f, IH this, ?_⟩
  · exact mem_of_ne_of_mem hfa (h _ hfa')
  · rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← Perm.one_def, one_mul]
Cleared hypotheses: l, f, h
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
⊢ (f : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq
have this : f = 1
Tactic: have : f = 1 := by simpa [permsOfList] using h
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f : Equiv.Perm α
h : Membership.mem (γ := List (Equiv.Perm α)) (permsOfList []) f
heq_iff_eq : α
this : f = 1
⊢ (f : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq
have rw : (1 : (a : α) → α) heq_iff_eq ≠ heq_iff_eq → Membership.mem (γ := List α) [] heq_iff_eq
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (g : (a : α) → α) x ≠ x
have rw : (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
Tactic: rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have pos : (f : (a : α) → α) x = a → y ≠ x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
pos : (f : (a : α) → α) x = a → y ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
pos : (f : (a : α) → α) x = a → y ≠ x
pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have neg : ¬(f : (a : α) → α) x = a → ¬(f : (a : α) → α) x = y → (f : (a : α) → α) x ≠ x
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have neg : ¬(f : (a : α) → α) x = a → (if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
Tactic: split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
neg : ¬(f : (a : α) → α) x = a → (if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have pos : (f : (a : α) → α) x = a → y ≠ x
Tactic: split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
neg : ¬(f : (a : α) → α) x = a → (if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
pos : (f : (a : α) → α) x = a → y ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
Tactic: split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h_1 : f ∈ permsOfList (a :: l)
x : α
h :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
hx : (f : (a : α) → α) x ≠ x
y : α
hy : y ∈ l
hy' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a y * f) (permsOfList l)) f
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
neg : ¬(f : (a : α) → α) x = a → (if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
pos : (f : (a : α) → α) x = a → y ≠ x
pos₁ : ¬(f : (a : α) → α) x = a → (f : (a : α) → α) x = y → a ≠ x
⊢ (if (f : (a : α) → α) x = a then y else if (f : (a : α) → α) x = y then a else (f : (a : α) → α) x) ≠ x
have neg₁ : ¬(f : (a : α) → α) x = a → ¬(f : (a : α) → α) x = y → (f : (a : α) → α) x ≠ x
Tactic: split_ifs <;> [exact Ne.symm hxy; exact Ne.symm hxa; exact hx]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
⊢ (permsOfList (a :: l)).Nodup
have hl' : l.Nodup
Tactic: have hl' : l.Nodup := hl.of_cons
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
⊢ (permsOfList (a :: l)).Nodup
have hln' : (permsOfList l).Nodup
Tactic: have hln' : (permsOfList l).Nodup := nodup_permsOfList hl'
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
⊢ (permsOfList (a :: l)).Nodup
have hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
Tactic: have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
      not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
⊢ (permsOfList (a :: l)).Nodup
have rw : (permsOfList l).Nodup ∧
  ((∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))) ∧
      ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
        onFun (β := List (Equiv.Perm α)) List.Disjoint
          (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
          (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
          (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)) ∧
    (permsOfList l).Disjoint
      (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l)
Tactic: rw [permsOfList, List.nodup_append', List.nodup_flatMap, pairwise_iff_getElem]
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
refine_1 : (permsOfList l).Nodup
⊢ (permsOfList l).Nodup ∧
    ((∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
          onFun (β := List (Equiv.Perm α)) List.Disjoint
            (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)) ∧
      (permsOfList l).Disjoint
        (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l)
have refine_2 : ∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))
Tactic: refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
refine_1 : (permsOfList l).Nodup
refine_2 : ∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))
⊢ (permsOfList l).Nodup ∧
    ((∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
          onFun (β := List (Equiv.Perm α)) List.Disjoint
            (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)) ∧
      (permsOfList l).Disjoint
        (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l)
have refine_3 : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
  onFun (β := List (Equiv.Perm α)) List.Disjoint
    (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
    (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)
Tactic: refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
refine_1 : (permsOfList l).Nodup
refine_2 : ∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))
refine_3 :
  ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
    onFun (β := List (Equiv.Perm α)) List.Disjoint
      (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)
⊢ (permsOfList l).Nodup ∧
    ((∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))) ∧
        ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length) (_hij : i < j),
          onFun (β := List (Equiv.Perm α)) List.Disjoint
            (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l))
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i _hi)
            (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j _hj)) ∧
      (permsOfList l).Disjoint
        (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l)
have refine_4 : (permsOfList l).Disjoint
  (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l)
Tactic: refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi))
    x
hx₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj))
    x
⊢ False
have refine_3 : ∀ (f : Equiv.Perm α)
  (hf : f ∈ permsOfList l ∧ Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) * f = x),
  False
Tactic: let ⟨f, hf⟩ := List.mem_map.1 hx₁
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi))
    x
hx₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj))
    x
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) * f = x
⊢ False
have refine_3 : ∀ (g : Equiv.Perm α)
  (hg : g ∈ permsOfList l ∧ Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g = x),
  False
Tactic: let ⟨g, hg⟩ := List.mem_map.1 hx₂
-- Lean 4 proof step from Mathlib.Data.Fintype.Perm (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi))
    x
hx₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    ((fun (b : α) ↦ (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l) : List (Equiv.Perm α)))
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj))
    x
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g = x
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
have rw : (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) * f : (a : α) → α) a =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
Tactic: rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]