mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
⊢ m₁ = m₂

Tactic:
have h₁ : m₁.one = m₂.one := congr_arg (·.one) this

Goal state after:
M : Type u
m₁ m₂ : Monoid M
h_mul : HMul.hMul = HMul.hMul
this : m₁.toMulOneClass = m₂.toMulOneClass
h₁ : One.one = One.one
⊢ m₁ = m₂
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteLimits F
⊢ leftExactFunctor C D F

Tactic:
by simpa

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteColimits F
⊢ rightExactFunctor C D F

Tactic:
by simpa

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
⊢ s.ι ≫ h = 0

Tactic:
simp [← hfg]

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
⊢ h ≫ s.π = 0

Tactic:
simp [← hfg]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ additiveFunctor C D F

Tactic:
by simpa

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
T : C
f : X ⟶ T
g : Y ⟶ T
⊢ desc f g = fst ≫ f + snd ≫ g

Tactic:
by ext <;> simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
Subsingleton.elim x (0 : M)

Goal state after:
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : X ⟶ M
x : ↑X
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
subsingleton

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

Goal state before:
pp: case h₀
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 X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.fst = 𝟙 (X ⊞ Y) ≫ biprod.fst

Tactic:
simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]

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

Goal state before:
pp: case h₁
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 X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ (biprod.fst ≫ biprod.inl) ≫ biprod.snd = 𝟙 (X ⊞ Y) ≫ biprod.snd

Tactic:
simp only [Category.assoc, biprod.inl_fst, Category.comp_id, Category.id_comp, biprod.inl_snd,
        comp_zero]

Goal state after:
case h₁
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 X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero Y
⊢ 0 = biprod.snd
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

Goal state after:
α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
⊢ r a (f 0) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f ↔ (∀ (i : Fin (n + 1)), r a (f i)) ∧ ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
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
⊢ preadditiveHasZeroMorphisms = inst✝¹

Tactic:
subsingleton

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
⊢ preadditiveHasZeroMorphisms = inst✝¹

Tactic:
subsingleton

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

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

Tactic:
subsingleton

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

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

Tactic:
subsingleton

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

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

Tactic:
subsingleton

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

Goal state before:
pp: k : ℕ
⊢ map (fun x ↦ Fin.cons (0, 0).1 x) (antidiagonalTuple k (0, 0).2) = [0]

Tactic:
antidiagonalTuple_zero_right k,

Goal state after:
k : ℕ
⊢ map (fun x ↦ Fin.cons (0, 0).1 x) [0] = [0]
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
this : m ∈ p.parts → m ≠ 0
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
by simpa

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ ∃ a, True ∧ c.boundary.toEmbedding a = Fin.last n

Tactic:
exact ⟨Fin.last c.length, And.intro True.intro c.boundary_last⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
this : ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0
⊢ ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0

Tactic:
by simpa

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ f ∈ (insert a s).finsuppAntidiag n ↔
    f ∈
      (antidiagonal n).biUnion fun p ↦
        map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach

Tactic:
mem_finsuppAntidiag_insert h,

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    f ∈
      (antidiagonal n).biUnion fun p ↦
        map { toFun := fun f ↦ (↑f).update a p.1, inj' := ⋯ } (s.finsuppAntidiag p.2).attach
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n,
      ∃ a_2 ∈ (s.finsuppAntidiag a_1.2).attach, { toFun := fun f ↦ (↑f).update a a_1.1, inj' := ⋯ } a_2 = f

Tactic:
mem_attach,

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n, ∃ a_2, True ∧ { toFun := fun f ↦ (↑f).update a a_1.1, inj' := ⋯ } a_2 = f
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ i = c.index j → j ∈ Set.range ⇑(c.embedding i)

Tactic:
intro h
    rw [h]
    exact c.mem_range_embedding j

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

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : σ a = a ∧ τ a = a
⊢ σ a = a

Tactic:
h.1

Goal state after:
α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
a : α
h : σ a = a ∧ τ a = a
⊢ a = a
Module: Mathlib.Data.Fintype.Inv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
hp : ∃! a, p a
⊢ ∃! a, a ∈ univ ∧ p a

Tactic:
by simpa

Goal state after:
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)
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
⊢ motive (k + 1 + n) ((single (k + 1) ⋯).append c).reverse

Tactic:
convert! append_single k n c.reverse ih using 1
    · apply add_comm
    · rw [reverse_append, reverse_single]
      apply cast_heq

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

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

Tactic:
apply disjoint_noncommProd_right

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

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

Tactic:
rintro _; exact ⟨l, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
⊢ (permsOfList (a :: l)).Nodup

Tactic:
have hmeml : ∀ {f : Perm α}, f ∈ permsOfList l → f a = a := fun {f} hf =>
      not_not.1 (mt (mem_of_mem_permsOfList hf) (nodup_cons.1 hl).1)

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList (a :: l)).Nodup
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

Tactic:
intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

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

Goal state before:
pp: case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y

Tactic:
intro hx
        rw [← hx, IH] at h
        simp [getElem_mem] at h

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

Goal state before:
pp: case neg.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x a : α
ha : ¬f a = a
hmem : ¬x = a
hins : {x, a} = f.support
ht : #{a} = 1
key : ∀ (b : α), f b ≠ b ↔ b = x ∨ b = a
ha' : f a = x ∨ f a = a
⊢ f a = (swap x a) a

Tactic:
· rw [Or.resolve_right ha' ha, swap_apply_right]

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

Goal state before:
pp: u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))

Tactic:
rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

Goal state after:
u : ℤˣ
n : ℕ
| u ^ (n % 2)
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
· intro f hf₁ hf₂
      let ⟨x, hx, hx'⟩ := List.mem_flatMap.1 hf₂
      let ⟨g, hg⟩ := List.mem_map.1 hx'
      obtain rfl : g.symm x = a := f.injective <| by rw [hmeml hf₁, ← hg.2]; simp
      have hxa : x ≠ g.symm x := fun h => (List.nodup_cons.1 hl).1 (h ▸ hx)
      exact (List.nodup_cons.1 hl).1 <| mem_of_mem_permsOfList hg.1 (by simpa using hxa)

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 w y * swap x z)⁻¹ = swap y z

Tactic:
mul_inv_rev,

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.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ (k % ↑(orderOf f)).natAbs) x = (f ^ k) x

Tactic:
rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf]

Goal state after:
case h
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
k : ℤ
h₀ : 0 < ↑(orderOf f)
h₁ : 0 ≤ k % ↑(orderOf f)
⊢ (k % ↑(orderOf f)).natAbs < orderOf f ∧ (f ^ k) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
⊢ (f * g).signAux = f.signAux * g.signAux

Tactic:
rw [← signAux_inv g]
  unfold signAux
  rw [← prod_mul_distrib]
  refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_
  rintro ⟨a, b⟩ hab
  dsimp only [signBijAux]
  rw [mul_apply, mul_apply]
  rw [mem_finPairsLT] at hab
  by_cases hg : g b < g a
  · simp [*]
  obtain hf | hf := (f.injective.ne <| g.injective.ne hab.ne).lt_or_gt <;>
    simp_all [le_of_lt, not_le_of_gt, not_lt_of_ge]

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

Goal state before:
pp: α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (swap x y ^ 1) y = a

Tactic:
rw [zpow_one, swap_apply_def]

Goal state after:
α : Type u_2
x y : α
inst✝ : DecidableEq α
hxy : x ≠ y
a : α
ha : (if a = x then y else if a = y then x else a) ≠ a
hya : ¬y = a
⊢ (if y = x then y else if y = y then x else y) = a
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⁻¹ * (swap x (f x) * f)⁻¹ ^ i) (f x) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)

Tactic:
mul_inv_rev,

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : σ y ≠ y
⊢ (prodExtendRight a σ) (a, y) ≠ (a, y)

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
exact
    ⟨⟨a, ha⟩, ne_of_apply_ne ((↑) : s → α) (hf.apply_ne hs ha), fun b _ =>
      (hf.2 (⟨a, ha⟩ : s).2 b.2).subtypePerm⟩

Goal state after:
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 = (f⁻¹.cycleOf x) y

Tactic:
rw [inv_eq_iff_eq, cycleOf_apply, cycleOf_apply]
    split_ifs <;> simp_all [sameCycle_inv, sameCycle_symm_apply_right]

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

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

Tactic:
simp [Equiv.Perm.decomposeFin, swap_apply_def, Ne.symm h]

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

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

Tactic:
apply disjoint_noncommProd_right

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
hj2 : ↑(i.castLT ⋯ + 1) = ↑(i.castLT ⋯) + 1
⊢ ↑↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = ↑(i + 1)

Tactic:
simp [← this, hj1, hj2]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
h : n ∈ σ.cycleType
⊢ ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

Tactic:
obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ

Goal state after:
case mp.mk
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
l : List (Perm α)
h : n ∈ l.prod.cycleType
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
hld : List.Pairwise Disjoint l
⊢ ∃ c τ, l.prod = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mp.mk.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
l : List (Perm α)
x✝ : Trunc { l_1 // l_1.prod = l.prod ∧ (∀ g ∈ l_1, g.IsCycle) ∧ List.Pairwise Disjoint l_1 }
hlc : ∀ g ∈ l, g.IsCycle
c : Perm α
hld : List.Pairwise Disjoint (c :: l.erase c)
cl : c ∈ l
⊢ l.prod = c * (l.erase c).prod

Tactic:
rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]

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

Goal state before:
pp: case hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ {g (g a)} ⊆ g.support

Tactic:
simpa only [Finset.singleton_subset_iff, Perm.apply_mem_support]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
this : (g ^ 3) a = a
⊢ g (g (g a)) = a

Tactic:
by simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
| (freeDFinsuppEquiv (r • DFinsupp.single p 1)) x

Tactic:
map_smul,

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
| (r • freeDFinsuppEquiv (DFinsupp.single p 1)) x
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x + y) = descFun F s x + descFun F s y

Tactic:
refine Quot.induction_on₂ x y fun a b => ?_
      dsimp [descFun]
      rw [← quot_add]
      rfl

Goal state after: