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

Goal state before:
pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| f

pp: case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| cokernel.π (image.ι f)

Tactic:
rw [← image.fac f]

Goal state after:
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| factorThruImage f ≫ image.ι f

case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
| cokernel.π (image.ι f)
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
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ fromSubtype f p ≫ toSubtype f p ≫ π (Subtype.restrict p f) j = 𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j

Tactic:
biproduct.toSubtype_π,

Goal state after:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ fromSubtype f p ≫ π f ↑j = 𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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
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 : Fork (π f i) 0
j : J
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j

Tactic:
rcases Classical.em (i = j) with (rfl | h)

Goal state after:
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 : Fork (π f i) 0
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i

case inr
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 : Fork (π f i) 0
j : J
h : ¬i = j
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

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
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
j : J
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π

Tactic:
rcases Classical.em (i = j) with (rfl | h)

Goal state after:
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.π

case inr
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
j : J
h : ¬i = j
⊢ (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
ha : a ∈ map (Prod.map Nat.succ id) (antidiagonal n)
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (0, n + 1)
hx₂ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a
⊢ False

pp: case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id a)
hx₂ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id b)
⊢ False

Tactic:
· rw [List.mem_map] at hx₁ hx₂ ha
      obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂
      rw [Fin.cons_inj] at h
      injection h.1

Goal state after:
case succ.right.succ.refine_2
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a b : ℕ × ℕ
h : Function.onFun Disjoint (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) a b
x : Fin (k + 1) → ℕ
hx₁ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id a)
hx₂ : x ∈ (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (Prod.map Nat.succ id b)
⊢ False
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ.support = ∅ ↔ σ = 1

Tactic:
Finset.ext_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ (∀ (a : α), a ∈ σ.support ↔ a ∈ ∅) ↔ σ = 1
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
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
⊢ PreservesBinaryBiproduct X Y F

Tactic:
have : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _

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
X Y : C
inst✝² : HasBinaryBiproduct X Y
inst✝¹ : HasBinaryBiproduct (F.obj X) (F.obj Y)
inst✝ : Mono (F.biprodComparison X Y)
that :
  prodComparison F X Y =
    (F.mapIso (biprod.isoProd X Y)).inv ≫ F.biprodComparison X Y ≫ (biprod.isoProd (F.obj X) (F.obj Y)).hom
this : IsIso (F.biprodComparison X Y)
⊢ PreservesBinaryBiproduct X Y F
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ σ⁻¹.support = σ.support

Tactic:
Finset.ext_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ ∀ (a : α), a ∈ σ⁻¹.support ↔ a ∈ σ.support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case nil
α : Type u_1
l : List α
⊢ (l.splitWrtCompositionAux []).length = [].length

Tactic:
simp [splitWrtCompositionAux, *]

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

Goal state before:
pp: case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ f x = f (tl.prod x)

Tactic:
notMem_support.mp ((disjoint_prod_right tl hl.left).mem_imp hx)

Goal state after:
case cons.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
x : α
hx : x ∈ f.support
hl : (∀ a' ∈ tl, f.Disjoint a') ∧ List.Pairwise Disjoint tl
⊢ f x = f x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨(σ * τ) x, ⋯⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

Tactic:
Set.union_apply_left,

Goal state after:
case intro.refine_2.inl
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inl.ha⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) ((Set.union hd1'') ⟨x, ⋯⟩)))

case intro.refine_2.inl.ha
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxσ : σ x ≠ x
⊢ ↑⟨(σ * τ) x, ⋯⟩ ∈ ↑σ.support
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
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ (Equiv.swap a l[j]) (g a) = l[j]

Tactic:
hmeml hg.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
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
⊢ (Equiv.swap a l[j]) a = l[j]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ∀ (i : ℕ) (h₁ : i < ((x :: y :: l).rotate n).length) (h₂ : i < (x' :: y' :: l').length),
    ((x :: y :: l).rotate n)[i] = (x' :: y' :: l')[i]

Tactic:
· intro k hk hk'
    rw [getElem_rotate]
    induction k with
    | zero =>
      refine Eq.trans ?_ hx'
      congr
      simpa using hn
    | succ k IH =>
      conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
      rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'),
        ← IH (k.lt_succ_self.trans hk), ← h, formPerm_apply_getElem _ hd]
      congr 1
      rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
      apply Nat.add_mod

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:
by
        rw [zpow_one, swap_apply_def]
        split_ifs at * <;> tauto

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
n : ℕ
⊢ swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H

Tactic:
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]

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

Goal state before:
pp: case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ Pairwise fun x y ↦ signAux2 l (swap x y) = -1

Tactic:
intro x y hxy

Goal state after:
case h.right
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
⊢ signAux2 l (swap x y) = -1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ [].prod (a, b) = (a, b)

Tactic:
List.prod_nil,

Goal state after:
case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ 1 (a, b) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑g '' s
y : α
hy : y ∈ ⇑g '' s
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
by
    rw [Equiv.image_eq_preimage_symm] at hx hy
    convert! Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> simp

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ s ×ˢ s, f x.1 • g x.2 = ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)

Tactic:
product_self_eq_disjiUnion_perm hσ,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
s : Finset ι
σ : Perm ι
hσ : σ.IsCycleOn ↑s
f : ι → α
g : ι → β
⊢ ∑ x ∈ (range #s).disjiUnion (fun k ↦ map { toFun := fun i ↦ (i, (σ ^ k) i), inj' := ⋯ } s) ⋯, f x.1 • g x.2 =
    ∑ k ∈ range #s, ∑ i ∈ s, f i • g ((σ ^ k) i)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ * τ).cycleType = σ.cycleType + τ.cycleType

Tactic:
by
  rw [cycleType_def, cycleType_def, cycleType_def, h.cycleFactorsFinset_mul_eq_union, ←
    Multiset.map_add, Finset.union_val, Multiset.add_eq_union_iff_disjoint.mpr _]
  exact Finset.disjoint_val.2 h.disjoint_cycleFactorsFinset

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
· refine dvd_of_mem_cycleType ?_
    rw [cycleType, Multiset.mem_map]
    refine ⟨f.cycleOf x, ?_, ?_⟩
    · rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]
    · simp [(isCycle_cycleOf _ hx).orderOf]

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

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
⊢ (i.cycleIcc j) k = k

Tactic:
by
  by_cases hij : i ≤ j
  · have kin : k ∈ Set.range (natAdd_castLEEmb (Nat.sub_le n i)) := by
      simp [range_natAdd_castLEEmb]; lia
    have : (((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩)
      = subNat i.1 (k.cast (by lia)) (by simp; lia) := by
      simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)
    simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this,
      Function.Embedding.trans_apply, addNatEmb_apply, coe_toEmbedding, finCongr_apply]
    rw [cycleRange_of_gt]
    · exact eq_of_val_eq (by simp; lia)
    · exact lt_def.mpr (by simp [sub_val_of_le hij]; lia)
  · simp [hij]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
⊢ (↑↑⟨l', ⋯⟩).toFinset = l'.toFinset

Tactic:
List.toFinset_coe

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
⊢ (↑⟨l', ⋯⟩).toFinset = l'.toFinset
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_2.inl
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hlt' : (Equiv.symm σ) x1 < (Equiv.symm σ) x2
⊢ ∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2

pp: case refine_2.inr
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ ∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2

Tactic:
· exact ⟨_, _, hlt', by simp [hlt.le]⟩

Goal state after:
case refine_2.inr
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
hlt : x2 < x1
hle : (Equiv.symm σ) x2 ≤ (Equiv.symm σ) x1
⊢ ∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute c g

Tactic:
apply commute_of_mem_cycleFactorsFinset_commute
  intro c' hc'
  by_cases hcc' : c = c'
  · rw [hcc']
  · apply g.cycleFactorsFinset_mem_commute hc hc'; exact hcc'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f⁻¹.IsThreeCycle

Tactic:
by
  rwa [IsThreeCycle, cycleType_inv]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g = swap a (g a) * swap (g a) (g (g a)) → a ∈ g.support

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g = swap a (g a) * swap (g a) (g (g a))

Tactic:
· intro hg
    rw [mem_support]
    intro hx
    apply hg3.isCycle.ne_one
    simpa [hx] using! hg

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g = swap a (g a) * swap (g a) (g (g a))
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
⊢ (M * N).det = ∑ p, ∑ σ, ↑↑(sign σ) * ∏ i, M (σ i) (p i) * N (p i) i

Tactic:
simp only [det_apply', mul_apply, prod_univ_sum, mul_sum, Fintype.piFinset_univ]
      rw [Finset.sum_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ ∑ j, A i j * ∑ σ ∈ ofSign s with σ i = j, ∏ k ∈ {i}ᶜ, A k (σ k) = detp s A

Tactic:
mul_sum,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ ∑ x, ∑ i_1 ∈ ofSign s with i_1 i = x, A i x * ∏ k ∈ {i}ᶜ, A k (i_1 k) = detp s A
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit ((∑ σ ∈ ofSign s, ∏ k, A k (σ k)) * ∑ j_1, B i j_1 * ∑ σ ∈ ofSign t with σ j = j_1, ∏ k ∈ {j}ᶜ, B k (σ k))

Tactic:
mul_sum,

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j : n
⊢ IsAddUnit (∑ x, ∑ i_1 ∈ ofSign t with i_1 j = x, (∑ σ ∈ ofSign s, ∏ k, A k (σ k)) * (B i x * ∏ k ∈ {j}ᶜ, B k (i_1 k)))
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
G : J ⥤ Type w₀'
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ c.ι j'✝ ∘ ⇑(ConcreteCategory.hom (F.map f)) ∘ app j✝ = c.ι j✝ ∘ app j✝

Tactic:
← Function.comp_assoc,

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
G : J ⥤ Type w₀'
app : (j : J) → G.obj j → F.obj j
naturality :
  ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j
j✝ j'✝ : J
f : j✝ ⟶ j'✝
⊢ (c.ι j'✝ ∘ ⇑(ConcreteCategory.hom (F.map f))) ∘ app j✝ = c.ι j✝ ∘ app j✝