mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
x : α
hx : x ∈ (zipWith Equiv.swap l l').prod.support
⊢ x ∈ {x | (zipWith Equiv.swap l l').prod x ≠ x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
⊢ (swap x y).support = {x, y} ↔ x ≠ y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
⊢ (zipWith Equiv.swap l l').prod.support ⊆ l.toFinset ⊔ l'.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
⊢ {x | l.formPerm x ≠ x} ⊆ ↑l.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
x : α
hx : x ∈ l.formPerm.support
⊢ x ∈ {x | l.formPerm x ≠ x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
l : List α
inst✝ : Fintype α
⊢ l.formPerm.support ⊆ l.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.boundaries = c.boundaries

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
c : Composition n
⊢ (fun c ↦ c.toComposition) ((fun c ↦ c.toCompositionAsSet) c) = c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun c ↦ c.toCompositionAsSet) ((fun c ↦ c.toComposition) c) = c

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
⊢ Fintype.card (Composition n) = 2 ^ (n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : [x, y, z].Nodup
⊢ (swap x y * swap y z).support = {x, y, z}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
⊢ f.support \ {x, y} ⊆ (swap x y * f).support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : x ∈ l
⊢ l.formPerm x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
⊢ ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ∈ l
⊢ x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
⊢ (x :: (xs ++ [y])).formPerm y = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm ((x :: xs).getLast ⋯) = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
h : (x :: y :: xs).Nodup
⊢ (x :: y :: xs).formPerm x = y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (permsOfList (a :: l)).length = (a :: l).length !

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
⊢ (swap x (f x) * f).support = f.support \ {x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x (f x) * f).support
⊢ y ∈ f.support ∧ y ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
⊢ ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
hl : 1 < l.length
⊢ l.formPerm l[0] = l[1]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).Disjoint (swap z t)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
⊢ (y :: l).formPerm x = y ↔ (y :: l).formPerm x = (y :: l).formPerm ((y :: l).getLast ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this✝ : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
this : f ∈ permsOfList l ∨ ∃ b ∈ l, ∃ g ∈ permsOfList l, Equiv.swap a b * g = f
⊢ f ∈ permsOfList (a :: l)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ l
⊢ f ∈ permsOfList l

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ ∀ x ∈ f.support, f x = l.prod x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : x = a
⊢ x ∈ a :: l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ⊆ f.support
hg : y.support ⊆ g.support
⊢ x.Disjoint y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : x = y
⊢ x ∈ l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
l : List (Perm α)
h : f ∈ l
hl : List.Pairwise Disjoint l
⊢ f.support ⊆ l.prod.support

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ g x ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝ : [].Nodup
⊢ (permsOfList []).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ (g.extendDomain f).support = map f.asEmbedding g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
⊢ #(g.extendDomain f).support = #g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ σ ∈ (sumCongrHom m n).range

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 0 ↔ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f ≠ 1
⊢ 1 < #f.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support ≤ 1 ↔ f = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hx : f x ≠ x
h : f.support ⊆ (swap x (f x) * f).support
⊢ ¬(swap x (f x) * f) x ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (x ::ₘ y ::ₘ 0).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ (swap x y).support = { val := x ::ₘ y ::ₘ 0, nodup := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
h : xs.Nodup
n : ℕ
hn : n + 1 < xs.length
⊢ xs.formPerm xs[n] = xs[n + 1]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ.extendDomain f).Disjoint (τ.extendDomain f)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ f b ≠ b ↔ ?m.105 b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i ≤ xs.length

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ a = (swap x y) a

Tactic:
swap_apply_of_ne_of_ne ha'.1 ha'.2

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a : α
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = y
ha : f a = a
ha' : ¬a = x ∧ ¬a = y
⊢ a = a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < xs.length
⊢ xs.formPerm xs[i] = xs[(i + 1) % xs.length]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 2 ↔ f.IsSwap

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #f.support + #g.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
h : List.Pairwise Disjoint l
⊢ #l.prod.support = (List.map (card ∘ support) l).sum

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), f x ∈ s ↔ x ∈ s
⊢ (f.subtypePerm h).support = {x | f ↑x ≠ ↑x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} < Fintype.card α - 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ (σ * τ * σ⁻¹).support = map (Equiv.toEmbedding σ) τ.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ #(σ * τ * σ⁻¹).support = #τ.support

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x | l.formPerm x ≠ x} = ↑l.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: x : ℤ
⊢ IsUnit x ↔ |x| = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: a : ℤ
ha : IsUnit a
⊢ a ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u * u = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u⁻¹ = u

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u₁ u₂ : ℤˣ
⊢ u₁ / u₂ = u₁ * u₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑u * ↑u = 1

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: n : ℕ
⊢ (-1) ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ l.formPerm.support = l.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).formPerm = l.formPerm

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
⊢ (l.rotate n).formPerm = l.formPerm

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l l' : List α
hd : l.Nodup
h : l ~r l'
⊢ l.formPerm = l'.formPerm

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
a b : α
⊢ (x :: y :: l ++ [a, b]).formPerm = (x :: y :: l ++ [a]).formPerm * Equiv.swap a b

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (a :: b :: l).reverse.formPerm = (a :: b :: l).formPerm⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
w : l.Nodup
n i : ℕ
h : i < l.length
⊢ (l.formPerm ^ n) l[i] = l[(i + n) % l.length]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ ((x :: l).formPerm ^ n) x = (x :: l)[n % (x :: l).length]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ (x :: y :: l).formPerm x' ≠ x'

Tactic:
h x',

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ (x' :: y' :: l').formPerm x' ≠ x'
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ x' ∈ {z | (x :: y :: l).formPerm z ≠ z}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ x' ∈ x :: y :: l

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ ∀ (x_1 : α), x :: y :: l ≠ [x_1]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ ∀ (x : α), x' :: y' :: l' ≠ [x]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ (x :: y :: l).length = (x' :: y' :: l').length

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : 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
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
⊢ x a = l[i]

Tactic:
by

Goal state after:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : 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
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ x a = l[j]

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ : Perm α
h✝ : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
⊢ τ = swap i j * σ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
try rw [hστ, hτυ, swap_mul_self_mul]

Goal state after:
case inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inl.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ

Tactic:
try rw [hστ, hτυ, swap_mul_self_mul]

Goal state after:
case inl.inr
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : 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
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f ((Equiv.symm g) x) = f a

Tactic:
by

Goal state after: