mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesLimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj (F.mapCone b.toCone)).π.app { as := WalkingPair.right } =
    (id (Iso.refl (F.obj b.pt))).hom ≫ (F.mapBinaryBicone b).toCone.π.app { as := WalkingPair.right }

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x✝ : α
⊢ x✝ ∈ ↑f.support ↔ x✝ ∈ {x | f x ≠ x}

Tactic:
simp

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

Goal state before:
pp: n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks.length = (replicate c.blocks.length 1).sum

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ f x = x

Tactic:
hf

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
x : α
hf : f x = x
hg : g x = x
⊢ x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ : ℕ
c : Composition n✝
n : ℕ
h : 0 < n
⊢ [n].sum = n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
h : 0 < n
i : Fin n
⊢ ↑(((single n h).embedding 0) i) = ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        { as := WalkingPair.left } ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesBinaryBiproduct X Y F
c : Cocone (pair X Y)
hc : IsColimit c
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).hom).obj
              (F.mapBinaryBicone (BinaryBicone.ofColimitCocone hc)).toCocone).ι.app
        { as := WalkingPair.right } ≫
      (id (Iso.refl (F.obj c.pt))).hom =
    (F.mapCocone c).ι.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ 0 < (single n hn).length

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ n ≤ (single n hn).blocksFun ⟨0, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
⊢ ∀ (j : Fin c.length), j = i

Tactic:
intro j

Goal state after:
n : ℕ
hn : 0 < n
c : Composition n
i : Fin c.length
hi : n ≤ c.blocksFun i
j : Fin c.length
⊢ j = i
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case left
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.left } ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.left }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y : C
inst✝ : PreservesColimit (pair X Y) F
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).ι.app
        { as := WalkingPair.right } ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone b.toCocone)).pt).hom =
    (F.mapBinaryBicone b).toCocone.ι.app { as := WalkingPair.right }

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
b : ↑(Set.range f)
⊢ ∀ (a : α), f a = ↑b ↔ a ∈ Finset.univ ∧ f a = ↑b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α → β
hf : Injective f
a : α
⊢ hf.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
a : α
⊢ f.invOfMemRange ⟨f a, ⋯⟩ = a

Tactic:
simp

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

Goal state before:
pp: n : ℕ
c : Composition n
m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ (c₁.blocks ++ c₂.blocks).sum = m + n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
c✝ : Composition n
m : ℕ
c : Composition n
⊢ c.blocks.reverse.sum = n

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ (ones n).reverse.blocks = (ones n).blocks

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (single n hn).reverse.blocks = (single n hn).blocks

Tactic:
simp

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

Goal state before:
pp: n m : ℕ
c₁ : Composition m
c₂ : Composition n
⊢ (c₁.append c₂).reverse.blocks = ((c₂.reverse.append c₁.reverse).cast ⋯).blocks

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x✝ : α
⊢ f.invOfMemRange ((fun a ↦ ⟨f a, ⋯⟩) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Equiv.Perm α
f : α ↪ β
x✝ : ↑(Set.range ⇑f)
⊢ (fun a ↦ ⟨f a, ⋯⟩) (f.invOfMemRange x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
f : α ↪ β
x✝ : α
⊢ ↑(f.toEquivRange x✝) = ↑((Equiv.ofInjective ⇑f ⋯) x✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
let ft : Finset α := Finset.univ.map (Function.Embedding.subtype (· ∈ t))

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
⊢ ↑(s \ t) ≃ ↑(t \ s)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons.zero
α : Type u_1
n : ℕ
ns : List ℕ
IH :
  ∀ (l : List α) {i : ℕ} (hi : i < (l.splitWrtCompositionAux ns).length),
    (l.splitWrtCompositionAux ns)[i] = drop (take i ns).sum (take (take (i + 1) ns).sum l)
l : List α
hi : 0 < (l.splitWrtCompositionAux (n :: ns)).length
⊢ (l.splitWrtCompositionAux (n :: ns))[0] = drop (take 0 (n :: ns)).sum (take (take (0 + 1) (n :: ns)).sum l)

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {comm : (↑∅).Pairwise (Commute on f)}, (∀ a ∈ ∅, x ∉ (f a).support) → x ∉ (∅.noncommProd f comm).support

Tactic:
simp

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
x✝ : α
⊢ x✝ ∈ spᶜ ↔ x✝ ∈ sq \ sp ∪ (sp ∪ sq)ᶜ

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
x✝ : α
⊢ x✝ ∉ sp ↔ x✝ ∈ sq ∧ x✝ ∉ sp ∨ x✝ ∉ sp ∧ x✝ ∉ sq
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x✝ : α
⊢ x✝ ∈ sqᶜ ↔ x✝ ∈ sp \ sq ∪ (sp ∪ sq)ᶜ

Tactic:
simp

Goal state after:
α : Type u_1
β : Type u_2
p q : α → Prop
inst✝ : Finite ↑{x | p x}
e : ↑{x | p x} ≃ ↑{x | q x}
sp : Set α := {x | p x}
sq : Set α := {x | q x}
this✝ : Fintype ↑sp := Fintype.ofFinite ↑sp
this : Fintype ↑sq := Fintype.ofEquiv (↑sp) e
h : ↑({x | p x} \ {x | q x}) ≃ ↑({x | q x} \ {x | p x})
hpc : spᶜ = sq \ sp ∪ (sp ∪ sq)ᶜ
x✝ : α
⊢ x✝ ∉ sq ↔ x✝ ∈ sp ∧ x✝ ∉ sq ∨ x✝ ∉ sp ∧ x✝ ∉ sq
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ take n l ++ drop n l = l

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
⊢ 0 ∈ {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset

Tactic:
simp

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

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
⊢ Fin.last n ∈ {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ ∀ x ∈ f.support ∩ g.support, (f ^ 0) x = (g ^ 0) x

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
h : List.Pairwise Disjoint []
⊢ [].prod.support = List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support [])

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case zero
n : ℕ
c : CompositionAsSet n
h : 0 < c.boundaries.card
⊢ (take 0 c.blocks).sum = ↑(c.boundary ⟨0, h⟩)

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
hs : (↑∅).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (∅.noncommProd k ⋯).support = ∅.biUnion fun i ↦ (k i).support

Tactic:
simp

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

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ ∀ i_1 ∈ s, (k i).Disjoint (k i_1)

Tactic:
intro j

Goal state after:
case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
⊢ j ∈ s → (k i).Disjoint (k j)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ [].prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support [])

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝¹ : List α
x✝ : α
⊢ (zipWith Equiv.swap [] x✝¹).prod x✝ ≠ x✝ → x✝ ∈ [] ∨ x✝ ∈ x✝¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x✝¹ : List α
x✝ : α
⊢ (zipWith Equiv.swap x✝¹ []).prod x✝ ≠ x✝ → x✝ ∈ x✝¹ ∨ x✝ ∈ []

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝ : (z :: l).formPerm x = y
⊢ z ∈ y :: z :: l

Tactic:
simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
h✝¹ : ¬(z :: l).formPerm x = y
h✝ : (z :: l).formPerm x = z
⊢ y ∈ y :: z :: l

Tactic:
simp

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

Goal state before:
pp: case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl

Tactic:
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩

Goal state after:
case mpr.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑(Equiv.symm σ)) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = (Equiv.symm σ) (Sum.inr r)
⊢ Sum.inr r ∈ Set.range Sum.inl
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
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:
simp

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

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

Tactic:
simp at hl

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

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

Tactic:
simp at hl

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:
simp

Goal state after:
α : 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
Module: Mathlib.Data.Fintype.Perm

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

Tactic:
simp

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
  intro x hx
  rwa [mem_support, ← eq_on_support_mem_disjoint h hl _ hx, ← mem_support]

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:
ext b

Goal state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ b ∈ (g.extendDomain f).support ↔ b ∈ map f.asEmbedding g.support
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:
simp

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:
simp

Goal state after:
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]

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case e'_3
α : Type u_1
inst✝ : DecidableEq α
x : α
l : List α
h : (x :: l).Nodup
n : ℕ
⊢ n = 0 + n

Tactic:
simp

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:
simp

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:
simp

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
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:
simp

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
    rcases hστ with hστ | hστ <;> rcases hτυ with hτυ | hτυ <;>
      (try rw [hστ, hτυ, swap_mul_self_mul]) <;>
      simp [hστ, hτυ]

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 ∈ []
⊢ ∀ g ∈ [], g.IsSwap

Tactic:
simp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
me : α ≃* β
⊢ (if h : ∀ (a b : α), me.toEquiv (a * b) = me.toEquiv a * me.toEquiv b then
      some { toEquiv := me.toEquiv, map_mul' := h }
    else none) =
    some me

Tactic:
simp

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : DecidableEq β✝
α : Type u_4
β : Type u_5
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
me : α ≃* β
⊢ { toEquiv := ↑me, map_mul' := ⋯ } = me
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : 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
⊢ g ∈ g :: l

Tactic:
simp

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
hwy : w ≠ y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z

Tactic:
rw [swap_comm y z, h hyz.symm hwy]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
hl : [].Nodup
⊢ [].formPerm = 1 ↔ [].length ≤ 1

Tactic:
simp

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

Goal state before:
pp: case nil.inl
α : Type u_1
inst✝ : DecidableEq α
hl hl' : [].Nodup
⊢ [].length ≤ 1

Tactic:
simp

Goal state after: