mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left X✝.hom

Tactic:
rw [← Over.w κ]

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left (Hom.left κ ≫ Y✝.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ W₁.comp W₂ f

Tactic:
simp only [h, top_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
⊢ ∀ {m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt},
    m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst → m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l

Tactic:
intro m hm₁ hm₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt
hm₁ : m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst
hm₂ : m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd
⊢ m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: i j : WalkingParallelPairᵒᵖ
f : i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
induction i with | _ i
       =>  _ 

Goal state after:
case op
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
⊢ ∀ {m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt},
    (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl → (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l

Tactic:
intro m hm₁ hm₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt
hm₁ : (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl
hm₂ : (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr
⊢ m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ f = default

Tactic:
rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
apply IsLimit.postcomposeInvEquiv h c (isLimitOfReflects F _)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : ReflectsLimit K₁ F
c : Cone K₂
t : IsLimit (F.mapCone c)
⊢ IsLimit (F.mapCone ((Cone.postcompose h.inv).obj c))
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : X ⟶ W
⊢ (leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom) ((rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom).toFun x) = x

Tactic:
by
      simp only [Iso.symm_hom, LinearMap.toFun_eq_coe, LinearMap.coe_comp, Function.comp_apply,
        leftComp_apply, rightComp_apply, Category.assoc, Iso.hom_inv_id, Category.comp_id,
        Iso.hom_inv_id_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m✝ : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m✝ = s.π
⊢ m✝ = i.desc (cokernelCoforkOfCofork s)

Tactic:
by
      apply Cofork.IsColimit.hom_ext i; cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m✝ : (cokernelCoforkOfCofork c).pt ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m✝ = s.π
⊢ m✝ = i.desc (coforkOfCokernelCofork s)

Tactic:
by
      apply Cofork.IsColimit.hom_ext i; cat_disch

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u_1
m₁ m₂ : DivInvMonoid M
h_mul : HMul.hMul = HMul.hMul
h_inv : Inv.inv = Inv.inv
⊢ m₁ = m₂

Tactic:
by
  have h_mon := Monoid.ext h_mul
  have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
  let f : @MonoidHom M M m₁.toMulOne m₂.toMulOne :=
    @MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁)
      (fun x y => congr_fun (congr_fun h_mul x) y)
  have : m₁.zpow = m₂.zpow := by
    ext m x
    exact @MonoidHom.map_zpow' M M m₁ m₂ f (congr_fun h_inv) x m
  have : m₁.div = m₂.div := by
    ext a b
    exact (@div_eq_mul_inv _ m₁ a b).trans
      (((congr_fun (congr_fun h_mul a) _).trans
        (congr_arg _ (congr_fun h_inv b))).trans (@div_eq_mul_inv _ m₂ a b).symm)
  rcases m₁ with @⟨_, ⟨_⟩, ⟨_⟩, ⟨_⟩⟩
  congr

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

Goal state before:
pp: case inl
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
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
⊢ (if i ≠ i then 𝟙 (f i) else 0) ≫ ι f i ≫ s.π = ι f i ≫ s.π

Tactic:
rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]

Goal state after:
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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) =
    𝟙 (binaryBiconeOfIsSplitMonoOfCokernel i).pt

Tactic:
dsimp only [binaryBiconeOfIsSplitMonoOfCokernel_pt]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
X✝ Y✝ : C
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ retraction f ≫ (binaryBiconeOfIsSplitMonoOfCokernel i).inl +
      Cofork.π c ≫
        (isColimitCoforkOfCokernelCofork (isCokernelEpiComp i (retraction f) ⋯)).desc
          (Cofork.ofπ (𝟙 Y - retraction f ≫ f) ⋯) =
    𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = desc b.ι

Tactic:
by
  classical
  refine biproduct.hom_ext' _ _ fun j => hb.isLimit.hom_ext fun j' => ?_
  rw [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp, Bicone.toCone_π_app,
    biproduct.bicone_π, biproduct.ι_desc, biproduct.ι_π, b.toCone_π_app, b.ι_π]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgCat R)).map f)
i : (forget (AlgCat R)).obj X ≅ (forget (AlgCat R)).obj Y := asIso ((forget (AlgCat R)).map f)
⊢ IsIso f

Tactic:
let e : X ≃ₐ[R] Y := { f.hom, i.toEquiv with }

Goal state after:
R : Type u
inst✝ : CommRing R
X₁ X₂ : Type v
X Y : AlgCat R
f : X ⟶ Y
x✝ : IsIso ((forget (AlgCat R)).map f)
i : (forget (AlgCat R)).obj X ≅ (forget (AlgCat R)).obj Y := asIso ((forget (AlgCat R)).map f)
e : ↑X ≃ₐ[R] ↑Y :=
  let __src := Hom.hom f;
  let __src_1 := i.toEquiv;
  { toFun := (↑↑__src.toRingHom).toFun, invFun := __src_1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
⊢ IsIso f
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mp.refine_1
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
f : ι →₀ μ
hsupp : f.support ⊆ insert a s
⊢ f = (Finsupp.erase a f).update a (f a)

Tactic:
rw [update_erase_eq_update, Finsupp.update_self]

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

Goal state before:
pp: α : Type u_1
f g : Perm α
⊢ f⁻¹.Disjoint g ↔ f.Disjoint g

Tactic:
by
  refine ⟨fun h => ?_, Disjoint.inv_left⟩
  convert! h.inv_left

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

Goal state before:
pp: case e'_1
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
⊢ k + 1 + n = n + (k + 1)

pp: case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)

Tactic:
· apply add_comm

Goal state after:
case e'_2
n✝¹ : ℕ
c✝¹ : Composition n✝¹
m : ℕ
motive : (n : ℕ) → Composition n → Sort u_1
n✝ : ℕ
c✝ : Composition n✝
zero : motive 0 (ones 0)
append_single : (k n : ℕ) → (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (single (k + 1) ⋯))
k n : ℕ
c : Composition n
ih : motive n c.reverse
e_1✝ : k + 1 + n = n + (k + 1)
⊢ ((single (k + 1) ⋯).append c).reverse ≍ c.reverse.append (single (k + 1) ⋯)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support

Tactic:
Finset.sup_eq_union,

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ∪ (s.noncommProd f ⋯).support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ (x :: y :: tl).formPerm x = (x :: y :: tl)[1]

Tactic:
formPerm_apply_head _ _ _ h,

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
tl : List α
h : (x :: y :: tl).Nodup
hl : 1 < (x :: y :: tl).length
⊢ y = (x :: y :: tl)[1]
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ Equiv.refl α * f = f

Tactic:
← one_def,

Goal state after:
α : Type u
inst✝ : DecidableEq α
β : Type v
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
m : { l // l.prod = swap x (f x) * f ∧ ∀ g ∈ l, g.IsSwap } := swapFactorsAux l (swap x (f x) * f) ⋯
⊢ 1 * f = f
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
⊢ ∀ a ∈ finPairsLT n,
    (if (f * g) a.fst ≤ (f * g) a.snd then -1 else 1) =
      (if f (g.signBijAux a).fst ≤ f (g.signBijAux a).snd then -1 else 1) *
        if g⁻¹ (g.signBijAux a).fst ≤ g⁻¹ (g.signBijAux a).snd then -1 else 1

Tactic:
rintro ⟨a, b⟩ hab

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) ⟨a, b⟩.fst ≤ (f * g) ⟨a, b⟩.snd then -1 else 1) =
    (if f (g.signBijAux ⟨a, b⟩).fst ≤ f (g.signBijAux ⟨a, b⟩).snd then -1 else 1) *
      if g⁻¹ (g.signBijAux ⟨a, b⟩).fst ≤ g⁻¹ (g.signBijAux ⟨a, b⟩).snd then -1 else 1
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:
zpow_apply_comm σ m 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σ)) = ((fun x ↦ σ ^ x) n) ((σ ^ i) (Classical.choose hσ))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux (Equiv.refl (Fin n)) = signAux2 [] (Equiv.refl α)

Tactic:
← one_def,

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux 1 = signAux2 [] (Equiv.refl α)
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a.support ⊔ b.support) ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
Finset.sup_eq_union,

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a.support ∪ b.support) ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
h3 : τ.IsSwap
⊢ closure {σ, τ} = ⊤

Tactic:
by
  obtain ⟨x, y, h4, h5⟩ := h3
  obtain ⟨i, hi⟩ :=
    h1.exists_pow_eq (mem_support.mp ((Finset.ext_iff.mp h2 x).mpr (Finset.mem_univ x)))
      (mem_support.mp ((Finset.ext_iff.mp h2 y).mpr (Finset.mem_univ y)))
  rw [h5, ← hi]
  refine closure_cycle_coprime_swap
    (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x
  obtain ⟨m, hm⟩ := h
  rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi

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

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ n) x = x
h : (f ^ n).support = f.support
⊢ f ^ n = 1

Tactic:
rw [← mem_support, ← h, mem_support] at hx
        contradiction

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

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
a : α
hf : f.IsCycleOn s
hs : s.Nontrivial
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
hba : (f ^ n) a ≠ a
⊢ f a ≠ a

Tactic:
exact fun h => hba (IsFixedPt.perm_zpow h n)

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ Finset.univ.noncommProd (fun i ↦ (ϕ i) (1 i)) ⋯ = 1

Tactic:
apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)

Goal state after:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
⊢ ∀ x ∈ Finset.univ, (ϕ x) (1 x) = 1
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))) a = (f ^ n) a

Tactic:
sub_eq_iff_eq_add'.1 hk,

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) * k)) a = (f ^ n) a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x y : α
⊢ (f.cycleOf x) y = if f.SameCycle x y then f y else y

Tactic:
by
  dsimp only [cycleOf]
  split_ifs with h
  · apply ofSubtype_apply_of_mem
    exact h
  · apply ofSubtype_apply_of_not_mem
    exact h

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

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
this : (f.cycleOf x) x ≠ x
y : α
h : y ≠ y
hxy : ¬f.SameCycle x y
⊢ (f.cycleOf x).SameCycle x y

Tactic:
exact (h rfl).elim

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
case neg =>
        have : Nonempty α := ⟨x⟩
        rw [notMem_support] at hx
        exact ⟨0, Fintype.card_pos, hxy.eq_of_left hx⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : Option α
⊢ Option.map (⇑(removeNone σ)) x = (swap none (σ none)) (σ x)

Tactic:
obtain - | x := x

Goal state after:
case none
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
⊢ Option.map (⇑(removeNone σ)) none = (swap none (σ none)) (σ none)

case some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x : α
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (σ (some x))
Module: Mathlib.GroupTheory.Perm.Option

Goal state before:
pp: case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
hn : σ (some x) ≠ none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (some val✝)

Tactic:
have hσn : σ (some x) ≠ σ none := σ.injective.ne (by simp)

Goal state after:
case some.some
α : Type u_1
inst✝ : DecidableEq α
σ : Perm (Option α)
x val✝ : α
h : σ (some x) = some val✝
hn : σ (some x) ≠ none
hσn : σ (some x) ≠ σ none
⊢ Option.map (⇑(removeNone σ)) (some x) = (swap none (σ none)) (some val✝)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_2
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

Tactic:
by_cases h : i = e x

Goal state after:
case pos
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ

case neg
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = e x
⊢ (decomposeFin.symm (i.succ, e)) x.succ = (swap 0 i.succ) (e x).succ
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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
⊢ (g ^ n) x = x ↔ r = 0

Tactic:
← div_euc.1,

Goal state after:
α : 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
⊢ (g ^ (↑m + ↑(orderOf g) * q)) x = x ↔ r = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ Commute g (g.cycleOf x)

Tactic:
commute_iff_eq

Goal state after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ¬g.SameCycle x y ∧ ¬y = g y
⊢ g * g.cycleOf x = g.cycleOf x * g
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_4
inst✝ : Finite α
l₁ l₂ : List (Perm α)
h₀ : l₁.prod = l₂.prod
h₁l₁ : ∀ σ ∈ l₁, σ.IsCycle
h₁l₂ : ∀ σ ∈ l₂, σ.IsCycle
h₂l₁ : List.Pairwise Disjoint l₁
h₂l₂ : List.Pairwise Disjoint l₂
σ : Perm α
hσ : ¬σ.IsCycle
⊢ σ ∈ l₁ ↔ σ ∈ l₂

Tactic:
· exact iff_of_false (mt (h₁l₁ σ) hσ) (mt (h₁l₂ σ) hσ)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ (↑v).head * (↑v).tail.toList.prod = 1

Tactic:
rw [← List.prod_cons, ← Vector.toList_cons, v.1.cons_head_tail]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : ↑(vectorsProdEqOne G (n + 1))
⊢ (↑v).toList.prod = 1
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i : Fin n
⊢ Perm.sign (i.cycleIcc i) = 1

Tactic:
sign_cycleIcc_of_le (Fin.ge_of_eq rfl),

Goal state after:
n : ℕ
i : Fin n
⊢ (-1) ^ (↑i - ↑i) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ IsConj σ τ ↔ σ.partition = τ.partition

Tactic:
isConj_iff_cycleType_eq

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
⊢ σ.cycleType = τ.cycleType ↔ σ.partition = τ.partition