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 α
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
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
⊢ (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) : (a : α) → α)
    ((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]
-- 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
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
rw₁ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) : (a : α) → α)
      ((f : (a : α) → α) a : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
⊢ (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) : (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]
-- 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
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
rw₁ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) : (a : α) → α)
      ((f : (a : α) → α) a : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
rw₂ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi) : (a : α) → α) a =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
have rw₃ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
Tactic: rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
-- 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
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
⊢ False
have hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
Tactic: have hix : x a = l[i] := by
        rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
-- 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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
have rw : (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g : (a : α) → α) a =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
Tactic: rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- 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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
rw :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g : (a : α) → α) a =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
have rw₁ : (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) : (a : α) → α)
    ((g : (a : α) → α) a : α) =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
Tactic: rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- 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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
rw :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g : (a : α) → α) a =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
rw₁ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) : (a : α) → α)
      ((g : (a : α) → α) a : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
have rw₂ : (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) : (a : α) → α) a =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
Tactic: rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- 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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
rw :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) * g : (a : α) → α) a =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
rw₁ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) : (a : α) → α)
      ((g : (a : α) → α) a : α) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
rw₂ :
  (Equiv.swap a (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj) : (a : α) → α) a =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
have rw₃ : getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj =
  getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
Tactic: rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- 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
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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
⊢ False
have hiy : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
Tactic: have hiy : x a = l[j] := by
        rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- 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
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
hix : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l i hi
hiy : (x : (a : α) → α) a = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l j hj
⊢ False
have hieqj : i = j
Tactic: have hieqj : i = j := hl'.getElem_inj_iff.1 (hix.symm.trans hiy)
-- 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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
⊢ False
have refine_4 : ∀ (x : α) (hx : x ∈ l)
  (hx' :
    Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))
      f),
  False
Tactic: let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
-- 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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
⊢ False
have refine_4 : ∀ (g : Equiv.Perm α) (hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f), 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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((f : (a : α) → α) a : α)
have rw : (Equiv.swap a x * g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) = a
Tactic: rw [hmeml hf₁, ← hg.2]
-- 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
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ False
have hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
Tactic: obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
Cleared hypotheses: a, hl, hmeml, hf₂, hx', hg
-- 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
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
⊢ False
have hmeml₁ : ∀ {f : Equiv.Perm α},
  f ∈ permsOfList l →
    Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
Tactic: obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
Cleared hypotheses: a, hl, hmeml, hf₂, hx', hg
-- 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
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml₁ :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
⊢ False
have hf₃ : Membership.mem (γ := List (Equiv.Perm α))
  (flatMap
    (fun (b : α) ↦
      List.map
        (fun (f : Equiv.Perm α) ↦
          HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
        (permsOfList l))
    l)
  f
Tactic: obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
Cleared hypotheses: a, hl, hmeml, hf₂, hx', hg
-- 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
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → (f : (a : α) → α) a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) l) f
x : α
hx : x ∈ l
hx' :
  Membership.mem (γ := List (Equiv.Perm α)) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l)) f
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
hl₁ : Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)
hmeml₁ :
  ∀ {f : Equiv.Perm α},
    f ∈ permsOfList l →
      Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((Equiv.symm g : (a : α) → α) x : α)
hf₃ :
  Membership.mem (γ := List (Equiv.Perm α))
    (flatMap
      (fun (b : α) ↦
        List.map
          (fun (f : Equiv.Perm α) ↦
            HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) b : Equiv.Perm α) f)
          (permsOfList l))
      l)
    f
⊢ False
have hx'₁ : Membership.mem (γ := List (Equiv.Perm α))
  (List.map
    (fun (f : Equiv.Perm α) ↦
      HMul.hMul (α := Equiv.Perm α) (Equiv.swap ((Equiv.symm g : (a : α) → α) x) x : Equiv.Perm α) f)
    (permsOfList l))
  f
Tactic: obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
Cleared hypotheses: a, hl, hmeml, hf₂, hx', hg