awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
mpr : ∀ (x : α), p ((g : (a : α) → α) x) ↔ p x
⊢ Membership.mem (γ := Subgroup (Perm α)) (MonoidHom.range (G := Perm (Subtype p)) (ofSubtype (p := p))) g

Tactic:
refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
pos : ∀ (hx : (g : (a : α) → α) x = x), p ((g : (a : α) → α) x) ↔ p x
neg : ∀ (hx : ¬(g : (a : α) → α) x = x), p ((g : (a : α) → α) x) ↔ p x
⊢ p ((g : (a : α) → α) x) ↔ p x

Tactic:
by_cases hx : g x = x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : (g : (a : α) → α) x = x
pos pos₁ : p x ↔ p x
⊢ p ((g : (a : α) → α) x) ↔ p x

Tactic:
rw [hx]
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
⊢ p ((g : (a : α) → α) x) ↔ p x

Tactic:
iff_of_true (hg ?_) (hg ?_)

Premises used: iff_of_true
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
neg : Membership.mem (α := α) (↑g.support : Set α) ((g : (a : α) → α) x : α)
neg₁ : x ∈ (↑g.support : Set α)
⊢ p ((g : (a : α) → α) x) ↔ p x

Tactic:
refine iff_of_true (hg ?_) (hg ?_)

Premises used: iff_of_true
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
⊢ Membership.mem (α := α) (↑g.support : Set α) ((g : (a : α) → α) x : α)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
p : α → Prop
inst_2 : DecidablePred p
g : Perm α
hg : (↑g.support : Set α) ⊆ setOf p
x : α
hx : ¬(g : (a : α) → α) x = x
⊢ x ∈ (↑g.support : Set α)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
⊢ Eq.{u_1 + 1} (α := Equiv.Perm α) (formPerm []) 1

Tactic:
rfl

Premises used: List.formPerm, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
⊢ [x].formPerm = 1

Tactic:
rfl

Premises used: List.formPerm, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
⊢ (x :: y :: l).formPerm = swap x y * (y :: l).formPerm

Tactic:
rfl

Premises used: List.tail, List.formPerm, List.foldr, rfl, List.prod
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ [x, y].formPerm = swap x y

Tactic:
rfl

Premises used: Equiv.swapCore, Equiv.trans, Equiv.swap, List.formPerm, List.foldr, rfl, List.prod, ite
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
x_1 : α
⊢ ((zipWith swap [] x).prod : (a : α) → α) x_1 ≠ x_1 → Membership.mem (γ := List α) [] x_1 ∨ x_1 ∈ x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : List α
x_1 : α
⊢ ((zipWith swap x []).prod : (a : α) → α) x_1 ≠ x_1 → x_1 ∈ x ∨ Membership.mem (γ := List α) [] x_1

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l : List α
b : α
l' : List α
x : α
hx : ((zipWith swap (a :: l) (b :: l')).prod : (a : α) → α) x ≠ x
h : ((zipWith swap l l').prod : (a : α) → α) x = x
⊢ (swap a b : (a : α) → α) x ≠ x

Tactic:
simpa [h] using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
b : α
l' : List α
x : α
h : ((zipWith swap l l').prod : (a : α) → α) x = x
hx : ((zipWith swap (x :: l) (b :: l')).prod : (a : α) → α) x ≠ x
⊢ x ∈ x :: l

Tactic:
.head _

Premises used: List.Mem.head
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
b : α
l' : List α
x : α
h : ((zipWith swap l l').prod : (a : α) → α) x = x
hx : ((zipWith swap (x :: l) (b :: l')).prod : (a : α) → α) x ≠ x
⊢ x ∈ x :: l

Tactic:
exact .head _
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l l' : List α
x : α
h : ((zipWith swap l l').prod : (a : α) → α) x = x
hx : ((zipWith swap (a :: l) (x :: l')).prod : (a : α) → α) x ≠ x
⊢ x ∈ x :: l'

Tactic:
.head _

Premises used: List.Mem.head
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
a : α
l l' : List α
x : α
h : ((zipWith swap l l').prod : (a : α) → α) x = x
hx : ((zipWith swap (a :: l) (x :: l')).prod : (a : α) → α) x ≠ x
⊢ x ∈ x :: l'

Tactic:
exact .head _
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l l' : List α
x : α
h : Membership.mem (γ := Set α) {x : α | ((zipWith swap l l').prod : (a : α) → α) x ≠ x} x
⊢ x ∈ (↑(l.toFinset ⊔ l'.toFinset) : Set α)

Tactic:
simpa using mem_or_mem_of_zipWith_swap_prod_ne h

Premises used: List.mem_or_mem_of_zipWith_swap_prod_ne
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ Membership.mem (γ := Set α) {x : α | ((zipWith swap l l').prod : (a : α) → α) x ≠ x} x

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
⊢ Membership.mem (γ := Set α) {x : α | ((zipWith swap l l').prod : (a : α) → α) x ≠ x} x

Tactic:
have hx' : x ∈ { x | (zipWith swap l l').prod x ≠ x } := by simpa using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith swap l l').prod.support
hx' : Membership.mem (γ := Set α) {x : α | ((zipWith swap l l').prod : (a : α) → α) x ≠ x} x
⊢ x ∈ l.toFinset ⊔ l'.toFinset

Tactic:
simpa using zipWith_swap_prod_support' _ _ hx'

Premises used: List.zipWith_swap_prod_support'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)

Tactic:
(zipWith_swap_prod_support' l l.tail).trans ?_

Premises used: setOf, List.tail, List.zipWith_swap_prod_support', LE.le.trans
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
refine : (↑(l.toFinset ⊔ l.tail.toFinset) : Set α) ≤ (↑l.toFinset : Set α)
⊢ {x : α | (l.formPerm : (a : α) → α) x ≠ x} ≤ (↑l.toFinset : Set α)

Tactic:
refine (zipWith_swap_prod_support' l l.tail).trans ?_

Premises used: List.tail, List.zipWith_swap_prod_support', LE.le.trans
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
⊢ (↑(l.toFinset ⊔ l.tail.toFinset) : Set α) ≤ (↑l.toFinset : Set α)

Tactic:
simpa [Finset.subset_iff] using tail_subset l

Premises used: Finset.subset_iff, List.tail_subset
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
inst_1 : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x

Tactic:
simpa using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
inst_1 : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x

Tactic:
have hx' : x ∈ { x | formPerm l x ≠ x } := by simpa using hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
inst_1 : Fintype α
x : α
hx : x ∈ l.formPerm.support
hx' : Membership.mem (γ := Set α) {x : α | (l.formPerm : (a : α) → α) x ≠ x} x
⊢ x ∈ l.toFinset

Tactic:
simpa using support_formPerm_le' _ hx'

Premises used: List.support_formPerm_le'
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : (l.formPerm : (a : α) → α) x ≠ x
⊢ x ∈ l

Tactic:
simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

Premises used: or_iff_left_of_imp, List.mem_or_mem_of_zipWith_swap_prod_ne, List.mem_of_mem_tail
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∉ l
⊢ (l.formPerm : (a : α) → α) x = x

Tactic:
not_imp_comm.1 mem_of_formPerm_apply_ne h

Premises used: not_imp_comm, Iff.mp, List.mem_of_formPerm_apply_ne
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : x ∈ l
nil :
  ∀ (h : Membership.mem (γ := List α) [] x),
    Membership.mem (α := α) (γ := List α) [] ((formPerm [] : (a : α) → α) x : α)
cons :
  ∀ (y : α) (l : List α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
⊢ Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α)

Tactic:
rcases l with - | ⟨y, l⟩
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
h : Membership.mem (γ := List α) [] x
⊢ Membership.mem (α := α) (γ := List α) [] ((formPerm [] : (a : α) → α) x : α)

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
h : x ∈ [y]
⊢ Membership.mem (α := α) [y] (([y].formPerm : (a : α) → α) x : α)

Tactic:
simpa using h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
pos : ∀ (hx : x ∈ z :: l), Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
neg : ∀ (hx : x ∉ z :: l), Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)

Tactic:
by_cases hx : x ∈ z :: l
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
pos :
  (if ((z :: l).formPerm : (a : α) → α) x = y then z
    else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
    y :: z :: l
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)

Tactic:
rw [formPerm_cons_cons, mul_apply, swap_apply_def]

Premises used: Equiv.swap_apply_def, List.formPerm_cons_cons, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
pos : ((z :: l).formPerm : (a : α) → α) x = y → z ∈ y :: z :: l
pos₁ : ¬((z :: l).formPerm : (a : α) → α) x = y → ((z :: l).formPerm : (a : α) → α) x = z → y ∈ y :: z :: l
neg :
  ¬((z :: l).formPerm : (a : α) → α) x = y →
    ¬((z :: l).formPerm : (a : α) → α) x = z →
      Membership.mem (α := α) (y :: z :: l) (((z :: l).formPerm : (a : α) → α) x : α)
⊢ (if ((z :: l).formPerm : (a : α) → α) x = y then z
    else if ((z :: l).formPerm : (a : α) → α) x = z then y else ((z :: l).formPerm : (a : α) → α) x) ∈
    y :: z :: l

Tactic:
split_ifs
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h_1 : ((z :: l).formPerm : (a : α) → α) x = y
⊢ z ∈ y :: z :: l

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h_1 : ¬((z :: l).formPerm : (a : α) → α) x = y
h_2 : ((z :: l).formPerm : (a : α) → α) x = z
⊢ y ∈ y :: z :: l

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h_1 : ¬((z :: l).formPerm : (a : α) → α) x = y
h_2 : ¬((z :: l).formPerm : (a : α) → α) x = z
⊢ Membership.mem (α := α) (y :: z :: l) (((z :: l).formPerm : (a : α) → α) x : α)

Tactic:
simp [*]
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ x = y

Tactic:
replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)
x y : α
hx : x ∉ z :: l
h : x = y
⊢ Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)

Tactic:
simp [formPerm_apply_of_notMem hx, ← h]

Premises used: List.formPerm_apply_of_notMem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
cons : ∀ {x : α} (y : α) (h : x ∈ [y]), Membership.mem (α := α) [y] (([y].formPerm : (a : α) → α) x : α)
cons₁ :
  ∀ (z : α) (l : List α)
    (IH :
      ∀ {x : α} (y : α) (h : x ∈ y :: l), Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α))
    {x : α} (y : α) (h : x ∈ y :: z :: l),
    Membership.mem (α := α) (y :: z :: l) (((y :: z :: l).formPerm : (a : α) → α) x : α)
⊢ Membership.mem (α := α) (y :: l) (((y :: l).formPerm : (a : α) → α) x : α)

Tactic:
induction l generalizing x y with
  | nil => simpa using h
  | cons z l IH =>
    by_cases hx : x ∈ z :: l
    · rw [formPerm_cons_cons, mul_apply, swap_apply_def]
      split_ifs
      · simp
      · simp
      · simp [*]
    · replace h : x = y := Or.resolve_right (mem_cons.1 h) hx
      simp [formPerm_apply_of_notMem hx, ← h]

Premises used: Equiv.swap_apply_def, List.cons, List.formPerm_cons_cons, Equiv.Perm.mul_apply, List.nil
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h : Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α)
contrapose : ∀ (h : x ∉ l), ((l.formPerm : (a : α) → α) x : α) ∉ l
⊢ x ∈ l

Tactic:
contrapose h
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
h rwa rwa₁ rwa₂ rwa₃ : x ∉ l
⊢ ((l.formPerm : (a : α) → α) x : α) ∉ l

Tactic:
rwa [formPerm_apply_of_notMem h]

Premises used: List.formPerm_apply_of_notMem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x : α
⊢ Membership.mem (α := α) l ((l.formPerm : (a : α) → α) x : α) ↔ x ∈ l

Tactic:
⟨l.mem_of_formPerm_apply_mem, l.formPerm_apply_mem_of_mem⟩

Premises used: List.mem_of_formPerm_apply_mem, List.formPerm_apply_mem_of_mem, Iff.intro
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
⊢ ((x :: ([] ++ [y])).formPerm : (a : α) → α) y = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
z : α
xs : List α
IH : ∀ (x y : α), ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x
x y : α
⊢ ((x :: (z :: xs ++ [y])).formPerm : (a : α) → α) y = x

Tactic:
simp [IH]
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
xs : List α
nil : ∀ (x y : α), ((x :: ([] ++ [y])).formPerm : (a : α) → α) y = x
cons :
  ∀ (z : α) (xs : List α) (IH : ∀ (x y : α), ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x) (x y : α),
    ((x :: (z :: xs ++ [y])).formPerm : (a : α) → α) y = x
⊢ ((x :: (xs ++ [y])).formPerm : (a : α) → α) y = x

Tactic:
induction xs generalizing x y with
  | nil => simp
  | cons z xs IH => simp [IH]

Premises used: List.cons, List.nil
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
nil : ∀ (x : α), ([x].formPerm : (a : α) → α) ([x].getLast ⋯) = x
append_singleton :
  ∀ (l : List α) (a : α),
    (∀ (x : α), ((x :: l).formPerm : (a : α) → α) ((x :: l).getLast ⋯) = x) →
      ∀ (x : α), ((x :: (l ++ [a])).formPerm : (a : α) → α) ((x :: (l ++ [a])).getLast ⋯) = x
⊢ ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast ⋯) = x

Tactic:
induction xs using List.reverseRecOn generalizing x
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
⊢ ([x].formPerm : (a : α) → α) ([x].getLast ⋯) = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
a : α
h : ∀ (x : α), ((x :: l).formPerm : (a : α) → α) ((x :: l).getLast ⋯) = x
x : α
⊢ ((x :: (l ++ [a])).formPerm : (a : α) → α) ((x :: (l ++ [a])).getLast ⋯) = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
xs : List α
rw : ((x :: xs).formPerm : (a : α) → α) ((x :: xs).getLast ⋯) = x
rw₁ rw₂ : x = x
⊢ ((x :: xs).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: xs) xs.length ⋯) =
    x

Tactic:
rw [getElem_cons_length rfl, formPerm_apply_getLast]

Premises used: List.getElem_cons_length, List.formPerm_apply_getLast, rfl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
xs : List α
h : (x :: y :: xs).Nodup
⊢ ((x :: y :: xs).formPerm : (a : α) → α) x = y

Tactic:
simp [formPerm_apply_of_notMem h.notMem]

Premises used: List.formPerm_apply_of_notMem, List.Nodup.notMem
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
nil :
  ∀ (h : Nodup.{u_1} (α := α) []) (hl : 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 1 hl
cons :
  ∀ (x : α) (h : [x].Nodup) (hl : 1 < [x].length),
    ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 1 hl
cons₁ :
  ∀ (x y : α) (tl : List α) (h : (x :: y :: tl).Nodup) (hl : 1 < (x :: y :: tl).length),
    ((x :: y :: tl).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
⊢ (l.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) l 1 hl

Tactic:
rcases l with (_ | ⟨x, _ | ⟨y, tl⟩⟩)
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
h : Nodup.{u_1} (α := α) []
hl : 1 < length.{u_1} (α := α) []
⊢ (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] 1 hl

Tactic:
simp at hl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x : α
h : [x].Nodup
hl : 1 < [x].length
⊢ ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] 1 hl

Tactic:
simp at hl
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
cons :
  ((x :: y :: tl).formPerm : (a : α) → α) x =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
cons₁ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl
cons₂ : y = getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (y :: tl) 0 ⋯
cons₃ cons₄ : y = y
⊢ ((x :: y :: tl).formPerm : (a : α) → α)
      (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: tl) 1 hl

Tactic:
rw [getElem_cons_zero, formPerm_apply_head _ _ _ h, getElem_cons_succ, getElem_cons_zero]

Premises used: List.getElem_cons_zero, List.formPerm_apply_head, List.getElem_cons_succ
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
l : List α
x y : α
rw rw₁ : ((y :: l).formPerm : (a : α) → α) x = y ↔ ((y :: l).formPerm : (a : α) → α) x = y
⊢ ((y :: l).formPerm : (a : α) → α) x = y ↔
    Eq (α := α) (((y :: l).formPerm : (a : α) → α) x : α) (((y :: l).formPerm : (a : α) → α) ((y :: l).getLast ⋯) : α)

Tactic:
rw [formPerm_apply_getLast]

Premises used: List.formPerm_apply_getLast
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
xs : List α
h : xs.Nodup
hn : HAdd.hAdd (α := ℕ) 0 1 < xs.length
⊢ (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs 0 ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (HAdd.hAdd (α := ℕ) 0 1) hn

Tactic:
simpa using formPerm_apply_getElem_zero _ h _

Premises used: List.formPerm_apply_getElem_zero
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
xs : List α
h : xs.Nodup
hn : n + 1 + 1 < xs.length
succ :
  ∀ (h : Nodup.{u_1} (α := α) []) (hn : n + 1 + 1 < length.{u_1} (α := α) []),
    (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1 + 1) hn
succ₁ :
  ∀ (x : α) (h : [x].Nodup) (hn : n + 1 + 1 < [x].length),
    ([x].formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [x] (n + 1 + 1) hn
succ₂ :
  ∀ (x y : α) (l : List α) (h : (x :: y :: l).Nodup) (hn : n + 1 + 1 < (x :: y :: l).length),
    ((x :: y :: l).formPerm : (a : α) → α)
        (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1) ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) (x :: y :: l) (n + 1 + 1) hn
⊢ (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1 + 1) hn

Tactic:
rcases xs with (_ | ⟨x, _ | ⟨y, l⟩⟩)
-- Module: Mathlib.GroupTheory.Perm.List
Goal:
α : Type u_1
inst : DecidableEq α
n : ℕ
IH :
  ∀ (xs : List α) (h : xs.Nodup) (hn : n + 1 < xs.length),
    (xs.formPerm : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs n ⋯) =
      getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) xs (n + 1) hn
h : Nodup.{u_1} (α := α) []
hn : n + 1 + 1 < length.{u_1} (α := α) []
⊢ (formPerm [] : (a : α) → α) (getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1) ⋯) =
    getElem (valid := fun (as : List α) (i : ℕ) ↦ i < as.length) [] (n + 1 + 1) hn

Tactic:
simp at hn