mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J
⊢ (𝟭 (WidePullbackShape J)).obj j ≅
    ((wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)) ⋙
          wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)).obj
      j

Tactic:
by cases j <;> exact eqToIso (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePullbackShape J'
⊢ ((wideCospan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.term (h.invFun j)) ⋙
          wideCospan none (fun j ↦ some (h j)) fun j ↦ Hom.term (h j)).obj
      j ≅
    (𝟭 (WidePullbackShape J')).obj j

Tactic:
by cases j <;> exact eqToIso (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J
⊢ (𝟭 (WidePushoutShape J)).obj j ≅
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      j

Tactic:
by cases j <;> exact eqToIso (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
j : WidePushoutShape J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      j ≅
    (𝟭 (WidePushoutShape J')).obj j

Tactic:
by cases j <;> exact eqToIso (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso c.fst

Tactic:
rintro ⟨H⟩
    obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
    exact
      ⟨⟨l,
          BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
            (h.hom_ext _ _),
          hl⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.map f g ≫ prod.fst)) (F.map (prod.map f g) ≫ F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))

Tactic:
prod.map_fst,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.map f g) ≫ F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Over X
f g : U ⟶ V
h : Hom.left f = Hom.left g
⊢ f = g

Tactic:
let ⟨_,b,_⟩ := f
  let ⟨_,e,_⟩ := g
  congr
  simp only [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J := Classical.arbitrary J
⊢ (liftCocone D s c p hp).pt.hom ≫ hc.desc ((forget X).mapCocone t) = t.pt.hom

Tactic:
simp [← dsimp% (t.ι.app j).w, ← dsimp% (hp j), dsimp% hc.fac ((forget X).mapCocone t)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ f = e✝ ≫ Fm'

Tactic:
Ffac'

Goal state after:
case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ f = f
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
rw [Functor.isZero_iff] at hG
    exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y
X : C
f : X ⟶ X
hf : f ≫ f = f
c : Cofork (𝟙 X) f
i : IsColimit c
this : Epi c.π := epi_of_isColimit_cofork i
⊢ 𝟙 X ≫ c.π = c.π

Tactic:
exact Category.id_comp _

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X Y : C
hY : P Y
e : X ≅ Y
⊢ ⊤.map P.ι X

Tactic:
exact ⟨⟨Y, hY⟩, by simp, ⟨e.symm⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j) ≫ F.map (b.π j') = if h : j = j' then eqToHom ⋯ else 0

Tactic:
← F.map_comp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
⊢ F.map (b.ι j ≫ b.π j') = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ F.map (b.ι j ≫ b.π j) = eqToHom ⋯

Tactic:
simp only [bicone_ι_π_self, CategoryTheory.Functor.map_id, eqToHom_refl]

Goal state after:
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ 𝟙 (F.obj (f j)) = 𝟙 ((F.obj ∘ f) j)
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ x, F.map (b✝.π x) ≫ F.map (b✝.ι x) = 𝟙 (F.mapBicone b✝).pt

Tactic:
← F.map_comp

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
J : Type
x✝ : Finite J
val✝ : Fintype J
f✝ : J → C
b✝ : Bicone f✝
hb : b✝.IsBilimit
⊢ ∑ x, F.map (b✝.π x ≫ b✝.ι x) = 𝟙 (F.mapBicone b✝).pt
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → f j ⟶ T
j : J
⊢ ι f j ≫ desc g = ι f j ≫ ∑ j, π f j ≫ g j

Tactic:
simp [comp_sum, biproduct.ι_π_assoc, dite_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd

Tactic:
simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_right, ←
      BinaryBicone.toCocone_ι_app_right]
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
⊢ (matrix fun j k ↦ components m j k) = m

Tactic:
ext
  simp [biproduct.components]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
h : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
r0 : r a (f 0)
⊢ ∀ (i : Fin n), r a (f i.succ)

Tactic:
i

Goal state after:
α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
h : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
r0 : r a (f 0)
i : Fin n
⊢ r a (f i.succ)
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsColimit b.inrCokernelCofork
T : C
f : X ⟶ T
g : Y ⟶ T
m : b.toCocone.pt ⟶ T
h₁ : BinaryCofan.inl b.toCocone ≫ m = f
h₂ : BinaryCofan.inr b.toCocone ≫ m = g
⊢ m = b.fst ≫ f + b.snd ≫ g

Tactic:
by
      dsimp at m
      have h₁' : b.inl ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₁
      have h₂' : b.inr ≫ (m - (b.fst ≫ f + b.snd ≫ g)) = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : X ⟶ T, hq : b.fst ≫ q = m - (b.fst ≫ f + b.snd ≫ g)⟩ :=
        CokernelCofork.IsColimit.desc' hb _ h₂'
      rw [← sub_eq_zero, ← hq, ← Category.id_comp q, ← b.inl_fst, Category.assoc, hq, h₁',
        comp_zero]

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g

Tactic:
congr! 2

Goal state after:
case e'_4
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

case e'_6
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms

case e'_7
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
e_4✝ : (X ⊞ X) = (X ⊞ X)
⊢ preadditiveHasZeroMorphisms = preadditiveHasZeroMorphisms
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∃ y, s.sum y = m ∧ (∀ (i : ι), y i ≠ 0 → i ∈ s) ∧ n • y = f

Tactic:
refine ⟨fun i ↦ f i / n, ?_⟩

Goal state after:
case mpr
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
this : ∀ (i : ι), n ∣ f i
⊢ ∑ i ∈ s, f i / n = m ∧ (∀ (i : ι), (fun i ↦ f i / n) i ≠ 0 → i ∈ s) ∧ (n • fun i ↦ f i / n) = f
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.length ≤ n

Tactic:
conv_rhs => rw [← c.blocks_sum]

Goal state after:
n : ℕ
c : Composition n
⊢ c.length ≤ c.blocks.sum
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g : Perm α
⊢ f.Disjoint g → g.Disjoint f

Tactic:
simp only [Disjoint, or_comm, imp_self]

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

Goal state before:
pp: case inr
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : (σ * τ) a = a
hτ : τ a = a
⊢ σ a = a ∧ τ a = a

Tactic:
exact ⟨(congr_arg σ hτ).symm.trans h, hτ⟩

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

Goal state before:
pp: α : Type u_1
l : List α
c : Composition l.length
i : ℕ
⊢ (take i (map length (l.splitWrtComposition c))).sum = c.sizeUpTo i

Tactic:
congr
  exact map_length_splitWrtComposition l c

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
u : Perm (Subtype p)
x : α
hx : ¬p x
⊢ (∀ (x_1 : p x), u ⟨x, ⋯⟩ = ⟨x, ⋯⟩) ↔ (ofSubtype u) x = x

Tactic:
· simp only [forall_prop_of_false hx, ofSubtype_apply_of_not_mem u hx]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd :: tl).prod.support ⊆ List.foldr (fun x1 x2 ↦ x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
rw [List.prod_cons, List.map_cons, List.foldr_cons]
    refine (support_mul_le hd tl.prod).trans ?_
    exact sup_le_sup le_rfl hl

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

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

Tactic:
swap_inv,

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

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

Tactic:
simp [formPerm_append_pair, Equiv.swap_comm, ← formPerm_reverse (b::l)]

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

Tactic:
swap_inv,

Goal state after:
α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z
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 w y * swap x z * swap w x * (swap x z * (swap w y)⁻¹) = swap y z

Tactic:
swap_inv,

Goal state after:
α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap x z * swap w y) = swap y z
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₂⟩

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

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

Goal state before:
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:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Goal state after:
case neg
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₁ < f b₂
h✝ : f b₁ ≤ f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂
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₂⟩

Tactic:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

Goal state after:
case pos
n : ℕ
f : Perm (Fin n)
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : f b₂ ≤ f b₁
h✝ : f b₂ < f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
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:
simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x ((Equiv.symm f) y) ↔ f.SameCycle x y

Tactic:
← sameCycle_apply_right,

Goal state after:
α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x (f ((Equiv.symm f) y)) ↔ f.SameCycle x y
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).formPerm hd = hd
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
swap_inv,

Goal state after:
case e'_2
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹ * (f⁻¹ * swap x (f x)) ^ i) (f x) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ k * f ^ n) z = (f ^ k) (1 z)

Tactic:
(Commute.pow_pow_self _ _ _).eq,

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ n * f ^ k) z = (f ^ k) (1 z)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ sign σ = 1 ∨ sign σ = -1 ↔ σ ∈ univ

Tactic:
Int.units_eq_one_or,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ True ↔ σ ∈ univ
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ s.toList.formPerm.IsCycleOn ↑s

Tactic:
convert! s.nodup_toList.isCycleOn_formPerm

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ ↑s = {a | a ∈ s.toList}
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h : ¬f.SameCycle x y
⊢ (ofSubtype (f.subtypePerm ⋯)) y = y

Tactic:
apply ofSubtype_apply_of_not_mem
    exact h

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
k : ℤ
⊢ f.SameCycle x ((f ^ k) x)

Tactic:
· exact ⟨k, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #{c | #(↑c).support = n}

Tactic:
Finset.univ_eq_attach,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ (Multiset.filter (fun x ↦ n = x) (Multiset.map (Finset.card ∘ support) σ.cycleFactorsFinset.val)).card =
    #({c ∈ σ.cycleFactorsFinset.attach | #(↑c).support = n})
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c ^ n = ofSubtype (g.subtypePerm hg) → c.subtypePerm ⋯ ^ n = g.subtypePerm hg

pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
· intro h
    ext ⟨x, hx⟩
    simpa [Perm.congr_fun h _] using ofSubtype_subtypePerm_of_mem _ hx

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ IsConj (σ * π) τ

Tactic:
have h' : #σ.support ∈ τ.cycleType := by
      simp [← h, hc.cycleType]

Goal state after:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
⊢ IsConj (σ * π) τ