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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
J : Type w₁
F : C ⥤ D
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : F.PreservesZeroMorphisms
j✝¹ j✝ : J
⊢ biproduct.ι (F.obj ∘ f) j✝ ≫ (F.biproductComparison' f ≫ F.biproductComparison f) ≫ biproduct.π (F.obj ∘ f) j✝¹ =
    biproduct.ι (F.obj ∘ f) j✝ ≫ 𝟙 (⨁ F.obj ∘ f) ≫ biproduct.π (F.obj ∘ f) j✝¹

Tactic:
simp [biproduct.ι_π, ← Functor.map_comp, eqToHom_map]

Goal state after:
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
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite J
⊢ HasBiproductsOfShape J C

Tactic:
rcases Finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩

Goal state after:
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
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite J
n : ℕ
e : J ≃ Fin n
⊢ HasBiproductsOfShape J C
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
⊢ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) = 𝟙 (⨁ f)

Tactic:
ext g g'

Goal state after:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
val✝ : Fintype β
g g' : γ
⊢ ι f g' ≫ ((lift fun b ↦ π f (ε b)) ≫ desc fun b ↦ ι f (ε b)) ≫ π f g = ι f g' ≫ 𝟙 (⨁ f) ≫ π f g
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
j : K
⊢ ((g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ) ≫ biproduct.π f j = g' ≫ biproduct.π f j

Tactic:
simp only [Category.assoc, biproduct.toSubtype_fromSubtype, Pi.compl_apply,
          biproduct.map_π]

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
j : K
⊢ (g' ≫ biproduct.π f j ≫ if (p j)ᶜ then 𝟙 (f j) else 0) = g' ≫ biproduct.π f j
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
X₁ X₂ : Type v
g₁ : AddCommGroup X₁
g₂ : AddCommGroup X₂
m₁ : Module R X₁
m₂ : Module R X₂
e : X₁ ≃ₗ[R] X₂
⊢ ↟↑e ≫ ↟↑e.symm = 𝟙 (of R X₁)

Tactic:
by ext; apply e.left_inv

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

Goal state before:
pp: case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
⊢ (∃ a, ∑ i, a i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } a = f) ↔
    ∃ a, ∑ i, a i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ } a = f

Tactic:
refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_

Goal state after:
case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
f : ι → μ
g : Fin #s → μ
⊢ ∑ i, g i = n ∧ { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } g = f ↔
    ∑ i, ((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g i = n ∧
      { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ }
          (((e₁.symm.trans e₂).arrowCongr (Equiv.refl μ)) g) =
        f
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]

Goal state after:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
lz : (filter (fun x ↦ x = 0) l).sum = 0
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n
Module: Mathlib.GroupTheory.Perm.Basic

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑f)^[n] s s

Tactic:
exact MapsTo.iterate

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
⊢ ↑(s \ t) ≃ ↑(t \ s)

Tactic:
have ht (x : α) : x ∈ ft ↔ x ∈ t := by simp [ft]

Goal state after:
α : Type u_1
β : Type u_2
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : Fintype.card ↑s = Fintype.card ↑t
fs : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ s) Finset.univ
ft : Finset α := Finset.map (Function.Embedding.subtype fun x ↦ x ∈ t) Finset.univ
hs : ∀ (x : α), x ∈ fs ↔ x ∈ s
ht : ∀ (x : α), x ∈ ft ↔ x ∈ t
⊢ ↑(s \ t) ≃ ↑(t \ s)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: α : Type u_1
L : List (List α)
c : Composition L.flatten.length
h : map length L = c.blocks
⊢ L.flatten.splitWrtComposition c = L

Tactic:
simp only [and_self_iff, eq_iff_flatten_eq, flatten_splitWrtComposition,
    map_length_splitWrtComposition, h]

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

Goal state before:
pp: case h.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
b : n
⊢ ((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2) (Sum.inr b) = σ (Sum.inr b)

Tactic:
rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]

Goal state after:
case h.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
b : n
⊢ ↑(σ₂' ⟨Sum.inr b, ⋯⟩) = σ (Sum.inr b)
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 α
hn : n + 1 + 1 < (x :: y :: l).length
h : (l[n] :: y :: l).Nodup
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = x
⊢ False

Tactic:
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 α
hn : n + 1 + 1 < (x :: y :: l).length
h : (x :: l[n] :: l).Nodup
IH : (y :: l).formPerm (y :: l)[n] = l[n]
hx : (y :: l).formPerm (y :: l)[n] = y
⊢ False

Tactic:
simp [getElem_mem] at h

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f.IsSwap

Tactic:
refine ⟨x, y, hmem, ?_⟩

Goal state after:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
⊢ f = swap x y
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u₁ u₂ : ℤˣ
⊢ u₁ / u₂ = u₁ * u₂

Tactic:
by
  rw [div_eq_mul_inv, units_inv_eq_self]

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

Goal state before:
pp: u : ℤˣ
n : ℕ
⊢ u ^ n = u ^ (n % 2)

Tactic:
by
  conv =>
    lhs
    rw [← Nat.mod_add_div n 2]
    rw [pow_add, pow_mul, units_sq, one_pow, mul_one]

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
⊢ ∀ (n : ℕ) {b x : α} {f : Perm α},
    (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
by
  intro n
  induction n with
  | zero => exact fun _ h => ⟨0, h⟩
  | succ n hn =>
    intro b x f hb h
    obtain hfbx | hfbx := eq_or_ne (f x) b
    · exact ⟨0, hfbx⟩
    have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
    have hb' : (swap x (f x) * f) (f.symm b) ≠ f.symm b := by
      simpa [swap_apply_of_ne_of_ne this.2 hfbx.symm, eq_symm_apply, f.injective.eq_iff]
        using this.1
    obtain ⟨i, hi⟩ := hn hb' <| f.injective <| by simpa [pow_succ'] using h
    refine ⟨i + 1, ?_⟩
    rw [add_comm, zpow_add, mul_apply, hi, zpow_one, mul_apply, apply_symm_apply,
      swap_apply_of_ne_of_ne (ne_and_ne_of_swap_mul_apply_ne_self hb).2 hfbx.symm]

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

Goal state before:
pp: case refine_2
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
i : ℤ
hy : (swap x (f x) * f) ((f ^ i) x) ≠ (f ^ i) x
⊢ (swap x (f x) * f).SameCycle (f x) ((f ^ i) x)

Tactic:
exact isCycle_swap_mul_aux₂ (i - 1) hy (by simp [← mul_apply, -coe_mul, ← zpow_add_one])

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

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

Tactic:
sign_one,

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

Goal state before:
pp: β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod = prodCongrRight σ

Tactic:
ext ⟨a, b⟩ : 1

Goal state after:
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)
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 _)
    simp

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ d * x.lcm y = x * y

Tactic:
← hd,

Goal state after:
x y d m : ℕ
hd : x.gcd y = d
d0 : d.beq 0 = false
dm : x * y = d * m
⊢ x.gcd y * x.lcm y = x * y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
⊢ s ×ˢ s = (range #s).disjiUnion (fun k ↦ map { toFun := fun i ↦ (i, (f ^ k) i), inj' := ⋯ } s) ⋯

Tactic:
by
  ext ⟨a, b⟩
  simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk_inj]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
    exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
  · rintro ⟨n, -, a, ha, rfl, rfl⟩
    exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩

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

Goal state before:
pp: case neg
α : Type u_2
f g : Perm α
inst✝¹ : DecidableRel f.SameCycle
inst✝ : DecidableRel (f * g).SameCycle
h : Commute f g
x : α
hx : g x = x
y : α
hxy : ¬(f * g).SameCycle x y
⊢ ((f * g).cycleOf x) y = (f.cycleOf x) y

Tactic:
· rw [cycleOf_apply_of_not_sameCycle hxy, cycleOf_apply_of_not_sameCycle]
    contrapose hxy
    obtain ⟨z, rfl⟩ := hxy
    refine ⟨z, ?_⟩
    simp [h.mul_zpow, zpow_apply_eq_self_of_apply_eq_self hx]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset ∪ τ.cycleFactorsFinset).val =
    Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val + τ.cycleFactorsFinset.val)

Tactic:
Finset.union_val,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.Disjoint τ
⊢ Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val ∪ τ.cycleFactorsFinset.val) =
    Multiset.map (Finset.card ∘ support) (σ.cycleFactorsFinset.val + τ.cycleFactorsFinset.val)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
j : Fin (n + 1)
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) j) = cons a x j

Tactic:
cases j using Fin.cases

Goal state after:
case zero
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) 0) = cons a x 0

case succ
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
i✝ : Fin n
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) i✝.succ) = cons a x i✝.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

Tactic:
let σ : α ≃ α := ⟨f, f ^ (p ^ n - 1),
    leftInverse_iff_comp.mpr ((pow_sub_mul_pow f (Nat.one_le_pow n p hp.out.pos)).trans hf),
    leftInverse_iff_comp.mpr ((pow_mul_pow_sub f (Nat.one_le_pow n p hp.out.pos)).trans hf)⟩
  have hσ : σ ^ p ^ n = 1 := by
    rw [DFunLike.ext'_iff, coe_pow]
    exact (hom_coe_pow (fun g : Function.End α ↦ g) rfl (fun g h ↦ rfl) f (p ^ n)).symm.trans hf
  suffices Fintype.card f.fixedPoints = (support σ)ᶜ.card from
    this ▸ (card_compl_support_modEq hσ).symm
  suffices f.fixedPoints = (support σ)ᶜ by
    simp only [this]; apply Fintype.card_coe
  simp [σ, Set.ext_iff, IsFixedPt]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ f.cycleOf x ∈ f.cycleFactorsFinset ↔ x ∈ f.support

Tactic:
rw [mem_cycleFactorsFinset_iff]
  constructor
  · rintro ⟨hc, _⟩
    contrapose hc
    rw [notMem_support, ← cycleOf_eq_one_iff] at hc
    simp [hc]
  · intro hx
    refine ⟨isCycle_cycleOf _ (mem_support.mp hx), ?_⟩
    intro y hy
    rw [mem_support] at hy
    rw [cycleOf_apply]
    split_ifs with H
    · rfl
    · rw [cycleOf_apply_of_not_sameCycle H] at hy
      contradiction

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ (∏ j, ∏ i < j, if σ i < σ j then 1 else -1) = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1

Tactic:
apply Finset.prod_comm' (by simp)

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

Goal state before:
pp: case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support

Tactic:
mem_support_cycleOf_iff

Goal state after:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
⊢ False

Tactic:
have := h.le_bot (by simp [ha, ← hf a ha, ← hg a ha] : a ∈ f.support ∩ g.support)

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
x : Perm α
hf : ∀ (a : α), x a ≠ a → x a = f a
a : α
ha : x a ≠ a
hg : ∀ (a : α), x a ≠ a → x a = g a
this : a ∈ ⊥
⊢ False
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case e'_2
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
⊢ ∏ i, ∏ j > i, f (σ i) (σ j) = ∏ j, ∏ i < j, f (σ i) (σ j)

Tactic:
apply Finset.prod_comm' (by simp)

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

Goal state before:
pp: case e'_3
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
⊢ ∏ j, ∏ i < j, f i j = ∏ i, ∏ j > i, f i j

Tactic:
apply Finset.prod_comm' (by simp)

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

Goal state before:
pp: case refine_3.inl.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = σ a
x : α
hx : σ x = x
⊢ τ x = x ∨ (σ * f⁻¹) x = x

Tactic:
· refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap z t).IsSwap

Tactic:
rw [swap_isSwap_iff]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ z ≠ t
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ (swap x y).IsSwap

Tactic:
rw [swap_isSwap_iff]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ x ≠ y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3.inr.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : ∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
hτ : ∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}
f : Perm α
hf : f.IsCycle ∧ ∀ a ∈ f.support, f a = τ a
x : α
hx : τ x = x
⊢ σ x = x ∨ (τ * f⁻¹) x = x

Tactic:
· refine Or.inr ?_
          by_cases hfx : f x = x
          · rw [← hfx]
            simpa [hx] using hfx.symm
          · rw [mul_apply]
            rw [← hf.right _ (mem_support.mpr hfx)] at hx
            contradiction

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
rw [IsCycle.commute_iff' (mem_cycleFactorsFinset_iff.mp hc).1]
  apply exists_congr
  intro hc'
  simp only [Subgroup.mem_zpowers_iff]
  apply exists_congr
  intro n
  rw [Equiv.Perm.subtypePerm_on_cycleFactorsFinset hc]

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

Goal state before:
pp: case e_a
ι : 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
i : ι'
⊢ ((freeDFinsuppEquiv (DFinsupp.single p 1)) x) i = (DFinsupp.single p.2 (∏ i, (x i) (p.1 i))) i

Tactic:
obtain ⟨p, j⟩ := p

Goal state after:
case e_a
ι : 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
i : ι'
p : (i : ι) → κ i
j : ι'
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) i = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) i
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y + Quot.mk (⇑(colimitSetoid F)) z) =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y +
      Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]
      exact Quot.sound (Relation.left_distrib _ _ _)

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
x✝ y✝ z✝ : ColimitType F
x y z : Prequotient F
⊢ Quot.mk (⇑(colimitSetoid F)) x * (Quot.mk (⇑(colimitSetoid F)) y + Quot.mk (⇑(colimitSetoid F)) z) =
    Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y +
      Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) z

Tactic:
simp only [(· + ·), (· * ·), Add.add]
      exact Quot.sound (Relation.left_distrib _ _ _)

Goal state after:
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
A : Matrix n n R
⊢ (-A).det = (-1) ^ Fintype.card n * A.det

Tactic:
rw [← det_smul, neg_one_smul]

Goal state after:
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
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ (Aᵀ.updateRow i fun k ↦ A k i + A k j).det = Aᵀ.det

Tactic:
exact det_updateRow_add_self Aᵀ hij

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsFiltered J
⊢ ReflectsColimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence.{w'} J).trans <| Shrink.equivalence _).symm
    have := IsFiltered.of_equivalence e.symm
    exact reflectsColimitsOfShape_of_equiv e F

Goal state after: