mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_1
α : 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
⊢ (permsOfList l).Nodup

pp: case refine_2
α : 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
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

pp: case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

pp: case refine_4
α : 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
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
·

Goal state after:
case refine_1
α : 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
⊢ (permsOfList l).Nodup
Module: Mathlib.GroupTheory.Perm.Support

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

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
⊢ f.IsSwap
Module: Mathlib.GroupTheory.Perm.Finite

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

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b
Module: Mathlib.GroupTheory.Perm.List

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

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

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
·

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
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
⊢ f a = (swap x y) a

pp: case neg
α : 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
⊢ f a = (swap x y) a

Tactic:
·

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
⊢ f a = (swap x y) a
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_2
α : 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
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

pp: case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

pp: case refine_4
α : 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
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
·

Goal state after:
case refine_2
α : 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
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
·

Goal state after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
w : (x :: xs).Nodup
h : xs.length < (x :: xs).length
this : xs.length ≤ xs.length
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = (x :: xs)[(xs.length + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : 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
⊢ f a = (swap x y) a

Tactic:
·

Goal state after:
case neg
α : 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
⊢ f a = (swap x y) a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
·

Goal state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.Support

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

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

Tactic:
·

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.IsSwap
⊢ #f.support = 2
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

pp: case refine_4
α : 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
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
·

Goal state after:
case refine_3
α : 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),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]
Module: Mathlib.GroupTheory.Perm.List

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

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

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ {x | l.formPerm x ≠ x} ⊆ ↑l.toFinset
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)

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
·

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
·

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : ∀ (x : α), l ≠ [x]
⊢ ↑l.toFinset ⊆ {x | l.formPerm x ≠ x}
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ { x // x ∈ ↑(σ * τ).support } ≃ { x // x ∈ ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support }

pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ ∀ (x : α) (hx : x ∈ ↑(σ * τ).support),
    ↑(?intro.refine_1 ⟨(σ * τ) x, ⋯⟩) = (f * σ * f⁻¹ * (g * τ * g⁻¹)) ↑(?intro.refine_1 ⟨x, hx⟩)

Tactic:
·

Goal state after:
case intro.refine_1
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
⊢ { x // x ∈ ↑(σ * τ).support } ≃ { x // x ∈ ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support }
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:
rw [Nat.lt_sub_iff_add_lt, ← Nat.lt_sub_iff_add_lt', ← Finset.card_compl, Finset.compl_filter]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < #{x | ¬σ x = x}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
⊢ False

pp: case a.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ < l.length
⊢ False

Tactic:
·

Goal state after:
case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
⊢ False
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ < l.length
⊢ False

Tactic:
·

Goal state after:
case a.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ < l.length
⊢ False
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∈ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ (l.rotate 1).formPerm (l.rotate 1)[k] = l.formPerm (l.rotate 1)[k]

Tactic:
rw [formPerm_apply_getElem _ h', getElem_rotate l, getElem_rotate l, formPerm_apply_getElem _ h]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
k : ℕ
hk : k < (l.rotate 1).length
hx : (l.rotate 1)[k] ∈ l.rotate 1
⊢ l[((k + 1) % (l.rotate 1).length + 1) % l.length] = l[((k + 1) % l.length + 1) % l.length]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
h' : (l.rotate 1).Nodup
x : α
hx : x ∉ l.rotate 1
⊢ (l.rotate 1).formPerm x = l.formPerm x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx✝ : x ∈ ↑(σ * τ).support
hx : x ∈ ↑σ.support ∨ x ∈ ↑τ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

Tactic:
rcases hx with hxσ | hxτ

Goal state after:
case intro.refine_2.inl
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : x ∈ ↑σ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

case intro.refine_2.inr
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : x ∈ ↑τ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : x ∈ ↑σ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

pp: case intro.refine_2.inr
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : x ∈ ↑τ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

Tactic:
·

Goal state after:
case intro.refine_2.inl
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : x ∈ ↑σ.support
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.hl
α : 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n).length = (x' :: y' :: l').length

pp: case h.h
α : 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ∀ (i : ℕ) (h₁ : i < ((x :: y :: l).rotate n).length) (h₂ : i < (x' :: y' :: l').length),
    ((x :: y :: l).rotate n)[i] = (x' :: y' :: l')[i]

Tactic:
·

Goal state after:
case h.hl
α : 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'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n).length = (x' :: y' :: l').length