mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Int.Order.Units

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
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[((k + 1) % (l.rotate 1).length + 1) % l.length] = l[((k + 1) % l.length + 1) % l.length]

Tactic:
]

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
⊢ x = 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
⊢ x ∉ l

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
⊢ x ∉ l
Module: Mathlib.GroupTheory.Perm.List

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

pp: case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup

Tactic:
]

Goal state after:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup
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:
]

Goal state after:
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, ⋯⟩)))
Module: Mathlib.GroupTheory.Perm.List

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

pp: case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r ?m.32

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

Tactic:
]

Goal state after:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ Nodup ?m.32

case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r ?m.32

α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ List α
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 ~r x' :: y' :: l'

Tactic:
]

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 ~r x' :: y' :: l'
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
⊢ y' ≠ x'

Tactic:
]

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
⊢ y' ≠ 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
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card

Tactic:
]

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
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
⊢ (x :: y :: l).toFinset.card = (x' :: y' :: l').toFinset.card
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 ≠ x
⊢ ↑((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 ≠ x
⊢ ↑((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: α : 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).formPerm x_1 ≠ x_1} = {x | (x' :: y' :: l').formPerm x ≠ x}

Tactic:
]

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
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).formPerm x_1 ≠ x_1} = {x | (x' :: y' :: l').formPerm x ≠ x}
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
⊢ l[i] = l[i]

Tactic:
]

Goal state after:
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').length = (x' :: y' :: l').length

Tactic:
]

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]
⊢ l[j] = l[j]

Tactic:
]

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 * τ
⊢ τ = τ

Tactic:
]

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

Goal state before:
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
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]

Tactic:
]

Goal state after:
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
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.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 ≠ x
h : g (τ ((Equiv.symm g) (f x))) = f x
⊢ τ x = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))

Tactic:
]

Goal state after:
case intro.refine_2.inl.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 ≠ x
h : g (τ ((Equiv.symm g) (f x))) = f x
⊢ τ x = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))
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
⊢ (Equiv.swap a x * g) ((Equiv.symm g) x) = a

Tactic:
]

Goal state after:
α : 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
⊢ (Equiv.swap a x * g) ((Equiv.symm g) x) = a
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
]

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

Goal state before:
pp: case intro.refine_2.inl.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 ≠ x
h : g (τ ((Equiv.symm g) (f x))) = f x
⊢ x = x

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ 1 x = f x

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ []
x : α
⊢ 1 x = f x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.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 : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ¬σ x = x

Tactic:
]

Goal state after:
case intro.refine_2.inl.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 : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ¬σ x = x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ f = f

Tactic:
]

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

Goal state before:
pp: case intro.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α), (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (swap x y * l.prod)

Tactic:
]

Goal state after:
case intro.cons
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
motive : Perm α → Prop
one : motive 1
swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)
val✝ : Fintype α
g : Perm α
l : List (Perm α)
ih : ∀ (f : Perm α), (l.prod = f ∧ ∀ g ∈ l, g.IsSwap) → motive f
f : Perm α
hl : (g :: l).prod = f ∧ ∀ g_1 ∈ g :: l, g_1.IsSwap
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ motive (swap x y * l.prod)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}

Tactic:
]

Goal state after:
case intro
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : (↑x.truncSwapFactors.out).prod = x
h2 : ∀ g ∈ ↑x.truncSwapFactors.out, g.IsSwap
⊢ (↑x.truncSwapFactors.out).prod ∈ Submonoid.closure {σ | σ.IsSwap}
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
⊢ {σ | σ.IsSwap} ⊆ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
]

Goal state after:
n : ℕ
⊢ {σ | σ.IsSwap} ⊆ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.ha
α : 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 ≠ x
⊢ σ x ≠ x

Tactic:
]

Goal state after:
case intro.refine_2.inl.ha
α : 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 ≠ x
⊢ σ x ≠ x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap j i ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
]

Goal state after:
case inr
n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
this : ∀ (i j : Fin (n + 1)), i ≠ j → i < j → swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
lt : ¬i < j
⊢ swap j i ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ)
lts : i < j.castSucc
⊢ swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
]

Goal state after:
case succ.inr
n : ℕ
i : Fin (n + 1)
j : Fin n
ih :
  i ≠ j.castSucc → i < j.castSucc → swap i j.castSucc ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
ne : i ≠ j.succ
lt : i < j.succ
mem : swap j.castSucc j.succ ∈ Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ)
lts : i < j.castSucc
⊢ swap j.castSucc j.succ * swap i j.castSucc * swap j.castSucc j.succ ∈
    ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap y z = swap y z

Tactic:
]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
⊢ swap z y = swap z y

Tactic:
]

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

Goal state before:
pp: n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
]

Goal state after:
n : ℕ
f : Perm (Fin n)
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩.snd < ⟨a₁, a₂⟩.fst
b₁ b₂ : Fin n
hb : ⟨b₁, b₂⟩.snd < ⟨b₁, b₂⟩.fst
h : (if f a₂ < f a₁ then ⟨f a₁, f a₂⟩ else ⟨f a₂, f a₁⟩) = if f b₂ < f b₁ then ⟨f b₁, f b₂⟩ else ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩