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

Goal state before:
pp: case mp
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)

pp: case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)

Tactic:
<;>

Goal state after:
case mp
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)

case mpr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (⇑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
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:
ext1
    exact c.toCompositionAsSet_blocks

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

Goal state before:
pp: case a.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
y z x✝ : α
h : (x✝ ≠ y ∧ x✝ ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ x✝ ∈ (swap x✝ y * swap y z).support

pp: case a.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x z x✝ : α
h : (x ≠ x✝ ∧ x ≠ z ∧ True) ∧ x✝ ≠ z ∧ True
⊢ x✝ ∈ (swap x x✝ * swap x✝ z).support

pp: case a.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ z ∈ (swap x y * swap y z).support

Tactic:
<;>

Goal state after:
case a.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
y z x✝ : α
h : (x✝ ≠ y ∧ x✝ ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ x✝ ∈ (swap x✝ y * swap y z).support

case a.inr.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x z x✝ : α
h : (x ≠ x✝ ∧ x ≠ z ∧ True) ∧ x✝ ≠ z ∧ True
⊢ x✝ ∈ (swap x x✝ * swap x✝ z).support

case a.inr.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ z ∈ (swap x y * swap y z).support
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
  intro
  simp only [and_imp, Perm.coe_mul, Function.comp_apply, Ne, mem_support, mem_insert, mem_sdiff,
    mem_singleton]
  push Not
  rintro ha ⟨hx, hy⟩ H
  rw [swap_apply_eq_iff, swap_apply_of_ne_of_ne hx hy] at H
  exact ha H

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ [x].formPerm ([x].getLast ⋯) = x

pp: case append_singleton
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
a✝¹ : α
a✝ : ∀ (x : α), (x :: l✝).formPerm ((x :: l✝).getLast ⋯) = x
x : α
⊢ (x :: (l✝ ++ [a✝¹])).formPerm ((x :: (l✝ ++ [a✝¹])).getLast ⋯) = x

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x : α
⊢ [x].formPerm ([x].getLast ⋯) = x

case append_singleton
α : Type u_1
inst✝ : DecidableEq α
l✝ : List α
a✝¹ : α
a✝ : ∀ (x : α), (x :: l✝).formPerm ((x :: l✝).getLast ⋯) = x
x : α
⊢ (x :: (l✝ ++ [a✝¹])).formPerm ((x :: (l✝ ++ [a✝¹])).getLast ⋯) = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y

Tactic:
<;>

Goal state after:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case pos.refine_1
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ σ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (σ.extendDomain f) b = b

pp: case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (τ.extendDomain f) b = b

Tactic:
<;>

Goal state after:
case pos.refine_1
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ σ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (σ.extendDomain f) b = b

case pos.refine_2
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ τ (f.symm ⟨b, pb⟩) = f.symm ⟨b, pb⟩ → (τ.extendDomain f) b = b
Module: Mathlib.GroupTheory.Perm.Support

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

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

Tactic:
<;>

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

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.IsSwap → #f.support = 2
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]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
⊢ l[n] ∈ {x | l.formPerm x ≠ x}

Tactic:
rw [Set.mem_ofPred_eq, formPerm_apply_getElem _ h]

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

Goal state before:
pp: case intro.refine_1.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
a : α
⊢ a ∈ ↑σ.support ↔ f a ∈ ↑(f * σ * f⁻¹).support

pp: case intro.refine_1.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
a : α
⊢ a ∈ ↑τ.support ↔ g a ∈ ↑(g * τ * g⁻¹).support

Tactic:
<;>

Goal state after:
case intro.refine_1.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
a : α
⊢ a ∈ ↑σ.support ↔ f a ∈ ↑(f * σ * f⁻¹).support

case intro.refine_1.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
a : α
⊢ a ∈ ↑τ.support ↔ g a ∈ ↑(g * τ * g⁻¹).support
Module: Mathlib.GroupTheory.Perm.Sign

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

pp: case 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 inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = τ
⊢ σ = υ ∨ σ = swap i j * υ

case 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.Sign

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

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

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

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 inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

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

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

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.Sign

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

Tactic:
hστ,

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:
hστ,

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.GroupTheory.Perm.Sign

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

Tactic:
hστ,

Goal state after:
case inr.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ swap i j * τ = υ ∨ swap i j * τ = swap i j * υ
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:
hστ,

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 * τ = υ ∨ swap i j * τ = swap i j * υ
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 * υ

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

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

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 inl.inl
α : Type u
inst✝ : DecidableEq α
β : Type v
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ

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

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

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.Sign

Goal state before:
pp: case pos
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
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

pp: case neg
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
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

pp: case pos
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
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

pp: case neg
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
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

Tactic:
<;>

Goal state after:
case pos
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
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case neg
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
this : ¬b₁ < b₂
h✝¹ : f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₁, f a₂⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case pos
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
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₁, f b₂⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩

case neg
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
this : ¬b₁ < b₂
h✝¹ : ¬f a₂ < f a₁
h✝ : ¬f b₂ < f b₁
h : ⟨f a₂, f a₁⟩ = ⟨f b₂, f b₁⟩
⊢ ⟨a₁, a₂⟩ = ⟨b₁, b₂⟩
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg.inl
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
hf : f (g ⟨a, b⟩.snd) < f (g ⟨a, b⟩.fst)
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

pp: case neg.inr
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
hf : f (g ⟨a, b⟩.fst) < f (g ⟨a, b⟩.snd)
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
<;>

Goal state after:
case neg.inl
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
hf : f (g ⟨a, b⟩.snd) < f (g ⟨a, b⟩.fst)
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

case neg.inr
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
hf : f (g ⟨a, b⟩.fst) < f (g ⟨a, b⟩.snd)
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.mpr
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm hd = hd → (hd :: tl).formPerm = 1

Tactic:
intro h
      simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h
      simp [h]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝¹ : y = x
h✝ : a = x
ha : y ≠ a
⊢ y = a

pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : y = x
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ y = a

pp: case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : y = x
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ y = a

pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : ¬y = x
h✝¹ : y = y
h✝ : a = x
ha : y ≠ a
⊢ x = a

pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : y = y
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ x = a

pp: case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ x = a

pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : ¬y = x
h✝¹ : ¬y = y
h✝ : a = x
ha : y ≠ a
⊢ y = a

pp: case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ y = a

pp: case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ y = a

Tactic:
<;>

Goal state after:
case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝¹ : y = x
h✝ : a = x
ha : y ≠ a
⊢ y = a

case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : y = x
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ y = a

case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : y = x
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ y = a

case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : ¬y = x
h✝¹ : y = y
h✝ : a = x
ha : y ≠ a
⊢ x = a

case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : y = y
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ x = a

case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ x = a

case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝² : ¬y = x
h✝¹ : ¬y = y
h✝ : a = x
ha : y ≠ a
⊢ y = a

case pos
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : a = y
ha : x ≠ a
⊢ y = a

case neg
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
hya : ¬y = a
h✝³ : ¬y = x
h✝² : ¬y = y
h✝¹ : ¬a = x
h✝ : ¬a = y
ha : a ≠ a
⊢ y = a
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : n.Coprime (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ (σ ^ n).support = σ.support

Tactic:
exact
    le_antisymm (support_pow_le σ n)
      (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝ : f⁻¹ ((Equiv.symm f) b) = x
⊢ (Equiv.symm f) x ≠ (Equiv.symm f) b

pp: case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝¹ : ¬f⁻¹ ((Equiv.symm f) b) = x
h✝ : f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x
⊢ x ≠ (Equiv.symm f) b

pp: case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝¹ : ¬f⁻¹ ((Equiv.symm f) b) = x
h✝ : ¬f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x
⊢ f⁻¹ ((Equiv.symm f) b) ≠ (Equiv.symm f) b

Tactic:
<;>

Goal state after:
case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝ : f⁻¹ ((Equiv.symm f) b) = x
⊢ (Equiv.symm f) x ≠ (Equiv.symm f) b

case pos
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝¹ : ¬f⁻¹ ((Equiv.symm f) b) = x
h✝ : f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x
⊢ x ≠ (Equiv.symm f) b

case neg
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
h✝¹ : ¬f⁻¹ ((Equiv.symm f) b) = x
h✝ : ¬f⁻¹ ((Equiv.symm f) b) = (Equiv.symm f) x
⊢ f⁻¹ ((Equiv.symm f) b) ≠ (Equiv.symm f) b