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

Goal state before:
pp: case one
C : Type u
X Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y✝
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
Y : WalkingParallelPair
f : one ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases Y

Goal state after:
case one.zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : one ⟶ zero
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

case one.one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : one ⟶ one
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M : SemimoduleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0

Tactic:
simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]

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

Goal state before:
pp: case mk.mk.e_4
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ comp_zero✝¹ ≍ comp_zero✝

pp: case mk.mk.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ zero_comp✝¹ ≍ zero_comp✝

Tactic:
· apply proof_irrel_heq

Goal state after:
case mk.mk.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ zero_comp✝¹ ≍ zero_comp✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case mk.mk.e_5
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ zero_comp✝¹ ≍ zero_comp✝

Tactic:
· apply proof_irrel_heq

Goal state after:
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
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map (0 ≫ F.preimage 0) = 0

Tactic:
rw [F.map_comp, F.map_preimage, comp_zero]

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✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 * f = 0

Tactic:
dsimp [mul]; exact HasZeroMorphisms.comp_zero f _

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : WalkingParallelPair
⊢ x ∈ [zero, one].toFinset

Tactic:
cases x <;> simp

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

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
h : ¬some j' = j
⊢ Finset (j ⟶ some j')

Tactic:
exact ∅

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

Goal state before:
pp: case neg
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
h : ¬some j = j'
⊢ Finset (some j ⟶ j')

Tactic:
exact ∅

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
x : WalkingPair
⊢ x ∈ {WalkingPair.left, WalkingPair.right}

Tactic:
cases x <;> simp

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
inst✝¹ : HasZeroObject C
inst✝ : Epi f
x✝ : Cofork f 0
⊢ Cofork.π (zeroCokernelCofork f) ≫ 0 = x✝.π

Tactic:
simp [zero_of_epi_comp f _]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cocone (Discrete.functor f)
j : Discrete J
⊢ b.toCocone.ι.app j ≫ ∑ j, b.π j ≫ s.ι.app { as := j } = s.ι.app j

Tactic:
classical
        cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        simp

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
P Q P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ BinaryCofan.inr ((Cocone.precompose (mapPairIso eP eQ).inv).obj b.toCocone) ≫
      (Iso.refl ((Cocone.precompose (mapPairIso eP eQ).inv).obj b.toCocone).pt).hom =
    BinaryCofan.inr (b.ofIso eP eQ).toCocone

Tactic:
simp [BinaryCofan.inr]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0

Tactic:
simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr.hx
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ Function.update (⇑g) a n1 a = n1

Tactic:
Function.update_self

Goal state after:
case mpr.hx
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ n1 = n1
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
h : (f ^ n) x = x
⊢ (f ^ (n + 1)) x = f x

Tactic:
rw [pow_succ', mul_apply, h]

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

Goal state before:
pp: case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = f.extendSubtype x

pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ x ∉ ↑σ.support

Tactic:
Classical.not_not.1 ((not_congr mem_support).mp hx)

Goal state after:
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype x = f.extendSubtype x

α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ x ∉ ↑σ.support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)

Tactic:
have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]

Goal state after:
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
i : ℕ
hi : i < c.boundaries.card
H : (take i c.blocks).sum = ↑j
this : c.boundary ⟨i, hi⟩ = j
⊢ j = ↑((c.boundaries.orderIsoOfFin ⋯) ⟨i, hi⟩)
Module: Mathlib.GroupTheory.Perm.List

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

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
⊢ (y :: l).formPerm x ∈ y :: l

Tactic:
· simp at h

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
l : List α
h : x ∈ y :: l
⊢ (y :: l).formPerm x ∈ y :: l
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg.refine_1
α : 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
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ f a ∈ l

pp: case neg.refine_2
α : 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
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f

Tactic:
· exact mem_of_ne_of_mem hfa (h _ hfa')

Goal state after:
case neg.refine_2
α : 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
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a (f a) * (Equiv.swap a (f a) * f) = f
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
· simp at h

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
i : ℤ
hy : ¬σ ((σ ^ i) (Classical.choose hσ)) = (σ ^ i) (Classical.choose hσ)
⊢ ↑⟨(fun x ↦ σ ^ x) m, ⋯⟩ ((σ ^ i) (Classical.choose hσ)) = ↑⟨(fun x ↦ σ ^ x) n, ⋯⟩ ((σ ^ i) (Classical.choose hσ))

Tactic:
rw [Subtype.coe_mk, Subtype.coe_mk, zpow_apply_comm σ m i, zpow_apply_comm σ n i]

Goal state after:
case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
i : ℤ
hy : ¬σ ((σ ^ i) (Classical.choose hσ)) = (σ ^ i) (Classical.choose hσ)
⊢ (σ ^ i) ((σ ^ m) (Classical.choose hσ)) = (σ ^ i) ((σ ^ n) (Classical.choose hσ))
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
⊢ closure {σ, swap x (σ x)} = ⊤

Tactic:
by
  let H := closure ({σ, swap x (σ x)} : Set (Perm α))
  have h3 : σ ∈ H := subset_closure (Set.mem_insert σ _)
  have h4 : swap x (σ x) ∈ H := subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
  have step1 : ∀ n : ℕ, swap ((σ ^ n) x) ((σ ^ (n + 1) : Perm α) x) ∈ H := by
    intro n
    induction n with
    | zero => exact subset_closure (Set.mem_insert_of_mem _ (Set.mem_singleton _))
    | succ n ih =>
      convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)
      simp_rw [mul_swap_eq_swap_mul, mul_inv_cancel_right, pow_succ', coe_mul, comp_apply]
  have step2 : ∀ n : ℕ, swap x ((σ ^ n) x) ∈ H := by
    intro n
    induction n with
    | zero =>
      simp only [pow_zero, coe_one, id_eq, swap_self]
      convert! H.one_mem
    | succ n ih =>
      by_cases h5 : x = (σ ^ n) x
      · rw [pow_succ', mul_apply, ← h5]
        exact h4
      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
      · rw [← h6, swap_self]
        exact H.one_mem
      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)
  have step3 : ∀ y : α, swap x y ∈ H := by
    intro y
    have hx : x ∈ univ := Finset.mem_univ x
    rw [← h2, mem_support] at hx
    have hy : y ∈ univ := Finset.mem_univ y
    rw [← h2, mem_support] at hy
    obtain ⟨n, hn⟩ := IsCycle.exists_pow_eq h1 hx hy
    rw [← hn]
    exact step2 n
  have step4 : ∀ y z : α, swap y z ∈ H := by
    intro y z
    by_cases h5 : z = x
    · rw [h5, swap_comm]
      exact step3 y
    by_cases h6 : z = y
    · rw [h6, swap_self]
      exact H.one_mem
    rw [← swap_mul_swap_mul_swap h5 h6, swap_comm z x]
    exact H.mul_mem (H.mul_mem (step3 y) (step3 z)) (step3 y)
  rw [eq_top_iff, ← closure_isSwap, closure_le]
  rintro τ ⟨y, z, _, h6⟩
  rw [h6]
  exact step4 y z

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

Goal state before:
pp: case inr
α : 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
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
refine ⟨-i, (swap x (f⁻¹ x) * f⁻¹).injective ?_⟩

Goal state after:
case inr
α : 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⁻¹) (((swap x (f x) * f) ^ (-i)) (f x)) = (swap x (f⁻¹ x) * f⁻¹) b
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ (-1) ^ (↑l).length = sign (List.map ⇑ofSubtype ↑l).prod

Tactic:
sign_prod_list_swap hl',

Goal state after:
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out
hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap
hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f
⊢ (-1) ^ (↑l).length = (-1) ^ (List.map ⇑ofSubtype ↑l).length
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mp
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support → ¬f ^ n = 1

pp: case mpr
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ ¬f ^ n = 1 → (f ^ n).support = f.support

Tactic:
· intro h H
    refine hf.ne_one ?_
    rw [← support_eq_empty_iff, ← h, H, support_one]

Goal state after:
case mpr
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ ¬f ^ n = 1 → (f ^ n).support = f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
rw [pow_apply_eq_self_of_apply_eq_self hz, one_apply]

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

Goal state before:
pp: case cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, b)

Tactic:
| cons a' l ih =>

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

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f ^ Int.negSucc n) a = a ↔ ↑(#s) ∣ Int.negSucc n

Tactic:
rw [zpow_negSucc, ← inv_pow]

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
⊢ (f⁻¹ ^ (n + 1)) a = a ↔ ↑(#s) ∣ Int.negSucc n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ ↑(n % ↑(#s)).toNat) a = (f ^ n) a

Tactic:
Int.toNat_of_nonneg (Int.emod_nonneg _ <| Nat.cast_ne_zero.2
      (Nonempty.card_pos ⟨a, ha⟩).ne'),

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ (n % ↑(#s))) a = (f ^ n) a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : f⁻¹.SameCycle x y
h✝ : f.SameCycle x (f⁻¹ y)
⊢ y = f (f⁻¹ y)

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Goal state after:
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
h✝ : ¬f.SameCycle x (f⁻¹ y)
⊢ y = f⁻¹ y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

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

Goal state before:
pp: case pos
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
h✝¹ : ¬f⁻¹.SameCycle x y
h✝ : f.SameCycle x y
⊢ y = f y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

Goal state after:
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
h✝ : ¬f.SameCycle x y
⊢ y = y

Tactic:
simp_all [sameCycle_inv, sameCycle_symm_apply_right]

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

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
h : f x = x
y : α
hy : ¬f y = y
⊢ ¬(f x = x ↔ f y = y)

Tactic:
by tauto

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
⊢ Pairwise fun i_1 j ↦ ∀ (x : H ↑i_1) (y : H ↑j), Commute ((ϕ ↑i_1) x) ((ϕ ↑j) y)

Tactic:
intro _ _ hj

Goal state after:
case intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
f : G
hxi : f ∈ Set.range ⇑(ϕ i)
hxp : f ∈ ↑(⨆ x, (ϕ ↑x).range)
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute ((ϕ ↑i✝) x) ((ϕ ↑j✝) y)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ (-(-1) ^ a ::ₘ Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)

Tactic:
Multiset.prod_cons,

Goal state after:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ ((a ::ₘ s).sum + (a ::ₘ s).card)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
simp only [hm0, iff_false]
    exact pow_ne_one_of_lt_orderOf hm0 div_euc.2

Goal state after:
Module: Mathlib.Data.FunLike.Group

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : MulOne F
inst✝² : MulOneClass β
inst✝¹ : IsOneApply F α β
inst✝ : IsMulApply F α β
⊢ Function.Injective ⇑(coeMonoidHom F α β)

Tactic:
by
  rw [coe_coeMonoidHom]
  exact DFunLike.coe_injective

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

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.cycleRange (i.succAbove j) = j.succ

pp: case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.cycleRange (i.succAbove j) = j.succ

Tactic:
· rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]

Goal state after:
case inr
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.cycleRange (i.succAbove j) = j.succ