mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
left✝¹ : C
right✝¹ : Discrete PUnit.{1}
hom✝¹ : S.obj left✝¹ ⟶ (Functor.fromPUnit T).obj right✝¹
left✝ : C
right✝ : Discrete PUnit.{1}
hom✝ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝
hl : left { left := left✝¹, right := right✝¹, hom := hom✝¹ } = left { left := left✝, right := right✝, hom := hom✝ }
hh :
  S.map (eqToHom hl) ≫ hom { left := left✝, right := right✝, hom := hom✝ } =
    hom { left := left✝¹, right := right✝¹, hom := hom✝¹ }
⊢ { left := left✝¹, right := right✝¹, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }

Tactic:
cases hl

Goal state after:
case mk.mk.refl
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
left✝ : C
right✝¹ : Discrete PUnit.{1}
hom✝¹ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝¹
right✝ : Discrete PUnit.{1}
hom✝ : S.obj left✝ ⟶ (Functor.fromPUnit T).obj right✝
hh :
  S.map (eqToHom ⋯) ≫ hom { left := left✝, right := right✝, hom := hom✝ } =
    hom { left := left✝, right := right✝¹, hom := hom✝¹ }
⊢ { left := left✝, right := right✝¹, hom := hom✝¹ } = { left := left✝, right := right✝, hom := hom✝ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

Tactic:
simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr' ⊢

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd

Tactic:
simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr' ⊢

Goal state after:
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h

Tactic:
by
    rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
⊢ Mono (lift F' ≫ F'.m)

Tactic:
simpa using! MonoFactorisation.m_mono _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv
⊢ f = 0

Tactic:
simpa using h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f
⊢ f = 0

Tactic:
simpa using h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : IsIso f
⊢ f ≫ g = 0 ↔ g = 0

Tactic:
by
  rw [← IsIso.eq_inv_comp, Limits.comp_zero]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape (Discrete ι) C

Tactic:
have : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape (Discrete (Fin n)) C
⊢ HasLimitsOfShape (Discrete ι) C
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
g₁ g₂ : Group G
h_mul : HMul.hMul = HMul.hMul
⊢ g₁ = g₂

Tactic:
have h₁ : g₁.one = g₂.one := congr_arg (·.one) (Monoid.ext h_mul)
  let f : @MonoidHom G G g₁.toMulOne g₂.toMulOne :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  exact
    Group.toDivInvMonoid_injective
      (DivInvMonoid.ext h_mul
        (funext <| @MonoidHom.map_inv G G g₁ g₂.toDivisionMonoid f))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : Y ⟶ W
h✝ : X ⟶ W
c : KernelFork h✝
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h✝
s : Fork f 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι c) hf).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι
⊢ m ≫ Fork.ι c = i.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι c

Tactic:
simpa using h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : X ⟶ Z
i : Z ≅ Y
h✝ : l ≫ i.hom = f
s✝ : KernelFork f
hs : IsLimit s✝
s : Fork l 0
m : s.pt ⟶ (KernelFork.ofι (Fork.ι s✝) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (Fork.ι s✝) ⋯) = s.ι
⊢ m ≫ Fork.ι s✝ = hs.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι s✝

Tactic:
simpa using h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ Cofork.π c ≫ m = Cofork.π c ≫ i.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
simpa using h

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h✝ : i.hom ≫ l = f
s✝ : CokernelCofork f
hs : IsColimit s✝
s : Cofork l 0
m : (CokernelCofork.ofπ (Cofork.π s✝) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s✝) ⋯) ≫ m = s.π
⊢ Cofork.π s✝ ≫ m = Cofork.π s✝ ≫ hs.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
simpa using h

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) → α
⊢ ((fun x1 x2 ↦ x1 < x2) ⇒ r) (cons a f) (cons a f) ↔ (∀ (i : Fin (n + 1)), r a (f i)) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
apply (liftFun_vecCons r).trans
    simp only [forall_iff_succ, and_congr_left_iff, iff_self_and]
    intro h r0 i
    exact _root_.trans r0 (h (by grind))

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range n) ++ [(n, n - n)]) =
    [![n]]

Tactic:
Nat.sub_self,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2))
      (map (fun i ↦ (i, n - i)) (range n) ++ [(n, 0)]) =
    [![n]]
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
n : ℕ
⊢ map { toFun := fun m a ↦ Multiset.count a ↑m, inj' := ⋯ } (s.sym n) = s.piAntidiag n

Tactic:
by
  ext f
  simp only [Sym.val_eq_coe, mem_map, mem_sym_iff, Embedding.coeFn_mk, funext_iff, Sym.exists,
    Sym.mem_mk, Sym.coe_mk, exists_and_left, exists_prop, mem_piAntidiag, ne_eq]
  constructor
  · rintro ⟨m, hm, rfl, hf⟩
    simpa [← hf, Multiset.sum_count_eq_card hm]
  · rintro ⟨rfl, hf⟩
    refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩
    · simp +contextual
    · simpa [Multiset.count_sum', Multiset.count_singleton, not_imp_comm, eq_comm (a := 0)] using hf

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

Goal state before:
pp: 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
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this : Epi (F.splitEpiBiproductComparison f).section_
⊢ PreservesBiproduct f F

Tactic:
have : IsIso (biproductComparison F f) :=
    IsIso.of_epi_section' (splitEpiBiproductComparison F f)

Goal state after:
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
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this✝ : Epi (F.splitEpiBiproductComparison f).section_
this : IsIso (F.biproductComparison f)
⊢ PreservesBiproduct f F
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ : ℕ
c✝ : Composition n✝
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n : ℕ
c : Composition n
zero : motive 0 (ones 0)
single_append : (k n : ℕ) → (c : Composition n) → motive n c → motive (k + 1 + n) ((single (k + 1) ⋯).append c)
blocks tail✝ : List ℕ
blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail✝ → 0 < i
⊢ motive (0 :: tail✝).sum { blocks := 0 :: tail✝, blocks_pos := blocks_pos, blocks_sum := ⋯ }

Tactic:
by simp at blocks_pos

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
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
x : α
⊢ x ∈ ft ↔ x ∈ t

Tactic:
simp [ft]

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
h : x ∈ [y]
⊢ [y].formPerm x ∈ [y]

Tactic:
simpa using h

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

Goal state before:
pp: case mp.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.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr

Tactic:
rintro _; exact ⟨r, rfl⟩

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
z : α
xs : List α
IH : ∀ (x y : α), (x :: (xs ++ [y])).formPerm y = x
x y : α
⊢ (x :: (z :: xs ++ [y])).formPerm y = x

Tactic:
| cons z xs IH =>

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

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

Tactic:
left
    rw [extendDomain_apply_not_subtype _ _ pb]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ i < xs.length.succ

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ (l.rotate 1).Nodup

Tactic:
simpa using h

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

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

Tactic:
by_cases hx : x ∈ l.rotate 1

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

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

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

Tactic:
(try rw [hστ, hτυ, swap_mul_self_mul])

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

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

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

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Tactic:
by
  cases nonempty_fintype α
  refine top_unique fun x _ ↦ ?_
  obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop
  rw [← h1]
  exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

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

Goal state before:
pp: case zero
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ (f ^ orderOf f) x = (f ^ 0) x

Tactic:
rw [pow_orderOf_eq_one, pow_zero]

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
hl : [].Nodup
⊢ [].formPerm = l'.formPerm ↔ [] ~r l' ∨ [].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
suffices l'.length ≤ 1 ↔ l' = nil ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff]
    refine ⟨fun h => Or.inr h, ?_⟩
    rintro (rfl | h)
    · simp
    · exact h

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (-1)

Tactic:
← signAux_swap_zero_one h2n

Goal state after:
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Surjective fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩

Tactic:
rintro ⟨y, hy⟩

Goal state after:
case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy : y ∈ σ.support
⊢ ∃ a, (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) a = ⟨y, hy⟩
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((e.symm.trans (Equiv.trans f (swap x (f x)))) x✝)) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((Equiv.trans f (swap x (f x))) (e.symm x✝))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ a ∈ closure S, ↑a.support ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
apply closure_induction

Goal state after:
case mem
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support

case one
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ↑(support 1) ⊆ ⋃ b ∈ S, ↑b.support

case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ (x y : Perm α),
    x ∈ closure S →
      y ∈ closure S →
        ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑y.support ⊆ ⋃ b ∈ S, ↑b.support → ↑(x * y).support ⊆ ⋃ b ∈ S, ↑b.support

case inv
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
⊢ ∀ x ∈ closure S, ↑x.support ⊆ ⋃ b ∈ S, ↑b.support → ↑x⁻¹.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (((e.symm.trans f).trans e) x✝))

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e ((e.symm.trans f) x✝)))

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))

Tactic:
trans_apply

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(e ((swap x (f x)) (f (e.symm x✝)))) = ↑((swap (e x) (e (f x))) (e (f (e.symm x✝))))
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n i : ℕ
h : i + 1 < n + 1
⊢ i < n

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ #(swap x (f x)).support

Tactic:
card_support_swap hx.1.symm

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : f (f x) = x
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ (b - a) = 1

Tactic:
rw [hf.pow_eq_one_iff]

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x