awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fintype.Perm
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
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)
⊢ (permsOfList (a :: l)).Nodup

Tactic:
rw [permsOfList, List.nodup_append', List.nodup_flatMap, pairwise_iff_getElem]

Premises used: List.pairwise_iff_getElem, List.nodup_flatMap, List.nodup_append', permsOfList
-- Module: Mathlib.Data.Fintype.Perm
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 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:
⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩

Premises used: And.intro
-- Module: Mathlib.Data.Fintype.Perm
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)
refine_4 :
  (permsOfList l).Disjoint
    (flatMap (fun (b : α) ↦ List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a b * f) (permsOfList l)) 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)

Tactic:
refine ⟨?_, ⟨⟨?_,?_ ⟩, ?_⟩⟩
-- Module: Mathlib.Data.Fintype.Perm
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 l).Nodup

Tactic:
hln'
-- Module: Mathlib.Data.Fintype.Perm
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 l).Nodup

Tactic:
exact hln'
-- Module: Mathlib.Data.Fintype.Perm
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
⊢ ∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))

Tactic:
fun _ _ => hln'.map fun _ _ => mul_left_cancel

Premises used: mul_left_cancel, List.Nodup.map
-- Module: Mathlib.Data.Fintype.Perm
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
⊢ ∀ x ∈ l, Nodup (α := Equiv.Perm α) (List.map (fun (f : Equiv.Perm α) ↦ Equiv.swap a x * f) (permsOfList l))

Tactic:
exact fun _ _ => hln'.map fun _ _ => mul_left_cancel

Premises used: mul_left_cancel, List.Nodup.map
-- Module: Mathlib.Data.Fintype.Perm
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
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
⊢ False

Tactic:
let ⟨f, hf⟩ := List.mem_map.1 hx₁
-- Module: Mathlib.Data.Fintype.Perm
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
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
⊢ False

Tactic:
let ⟨g, hg⟩ := List.mem_map.1 hx₂
-- Module: Mathlib.Data.Fintype.Perm
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
rw₃ 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
⊢ (x : (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]

Premises used: And.right, And.left, Equiv.Perm.mul_apply, Equiv.swap_apply_left
-- Module: Mathlib.Data.Fintype.Perm
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

Tactic:
have hix : x a = l[i] := by
        rw [← hf.2, mul_apply, hmeml hf.1, swap_apply_left]
-- Module: Mathlib.Data.Fintype.Perm
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
rw₃ 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
⊢ (x : (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]

Premises used: And.right, And.left, Equiv.Perm.mul_apply, Equiv.swap_apply_left
-- Module: Mathlib.Data.Fintype.Perm
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

Tactic:
have hiy : x a = l[j] := by
        rw [← hg.2, mul_apply, hmeml hg.1, swap_apply_left]
-- Module: Mathlib.Data.Fintype.Perm
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
⊢ i = j

Tactic:
have hieqj : i = j := hl'.getElem_inj_iff.1 (hix.symm.trans hiy)
-- Module: Mathlib.Data.Fintype.Perm
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
hieqj : i = j
⊢ False

Tactic:
absurd hieqj (_root_.ne_of_lt hij)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Data.Fintype.Perm
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
hieqj : i = j
⊢ False

Tactic:
exact absurd hieqj (_root_.ne_of_lt hij)

Premises used: absurd, ne_of_lt
-- Module: Mathlib.Data.Fintype.Perm
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
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
⊢ False

Tactic:
let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
-- Module: Mathlib.Data.Fintype.Perm
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
refine_4 : ∀ (g : Equiv.Perm α) (hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f), False
⊢ False

Tactic:
let ⟨g, hg⟩ := List.mem_map.1 hx'
-- Module: Mathlib.Data.Fintype.Perm
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
rw : (Equiv.swap a x * g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) = a
⊢ Eq (α := α) ((f : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) : α) ((f : (a : α) → α) a : α)

Tactic:
rw [hmeml hf₁, ← hg.2]

Premises used: And.right
-- Module: Mathlib.Data.Fintype.Perm
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
⊢ (Equiv.swap a x * g : (a : α) → α) ((Equiv.symm g : (a : α) → α) x : α) = a

Tactic:
simp
-- Module: Mathlib.Data.Fintype.Perm
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
⊢ Nodup (α := α) ((Equiv.symm g : (a : α) → α) x :: l : List α)

Tactic:
obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp

Premises used: Equiv.injective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Data.Fintype.Perm
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 α)
⊢ ∀ {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

Premises used: Equiv.injective, Equiv.symm, DFunLike.coe, rfl
-- Module: Mathlib.Data.Fintype.Perm
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 : α)
⊢ 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

Premises used: Equiv.injective, Equiv.symm, DFunLike.coe, rfl