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

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
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
let em : StrongEpiMonoFactorisation (F.inv.map f) :=
      (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
    have : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
    have : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
    exact
      Nonempty.intro
        { I := F.obj em.I
          e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
          m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
          fac := by
            simp only [Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc] }

Goal state after:
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✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s))

Tactic:
apply fun s m => (Cone.functoriality K F).map_injective _

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✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    (Cone.functoriality K F).map m =
      (Cone.functoriality K F).map
        ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
J✝ : Type w
inst✝³ : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
inst✝² : PreservesFiniteColimits F
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
apply preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J)

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

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
M : Type u
toMonoid✝¹ : Monoid M
mul_comm✝¹ : ∀ (a b : M), a * b = b * a
toMonoid✝ : Monoid M
mul_comm✝ : ∀ (a b : M), a * b = b * a
h :
  { toMonoid := toMonoid✝¹, mul_comm := mul_comm✝¹ }.toMonoid =
    { toMonoid := toMonoid✝, mul_comm := mul_comm✝ }.toMonoid
⊢ { toMonoid := toMonoid✝¹, mul_comm := mul_comm✝¹ } = { toMonoid := toMonoid✝, mul_comm := mul_comm✝ }
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toLeftCancelMonoid M)

Tactic:
rintro ⟨⟩ ⟨⟩ h

Goal state after:
M : Type u
toLeftCancelMonoid✝¹ : LeftCancelMonoid M
toIsRightCancelMul✝¹ : IsRightCancelMul M
toLeftCancelMonoid✝ : LeftCancelMonoid M
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toLeftCancelMonoid := toLeftCancelMonoid✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toLeftCancelMonoid =
    { toLeftCancelMonoid := toLeftCancelMonoid✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toLeftCancelMonoid
⊢ { toLeftCancelMonoid := toLeftCancelMonoid✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ } =
    { toLeftCancelMonoid := toLeftCancelMonoid✝, toIsRightCancelMul := toIsRightCancelMul✝ }
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
m₁ m₂ : CancelMonoid M
h : m₁.toRightCancelMonoid = m₂.toRightCancelMonoid
⊢ HMul.hMul = HMul.hMul

Tactic:
exact congrArg (fun m : Monoid M => (letI := m; HMul.hMul : M → M → M)) <|
    congrArg (@RightCancelMonoid.toMonoid M) h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (coprodComparison G X Y)

Tactic:
by
  rw [← PreservesColimitPair.iso_hom]
  infer_instance

Goal state after:
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
j : J
⊢ ι f j ≫ (isoCoproduct f).hom = ι f j ≫ desc (Sigma.ι f)

Tactic:
simp [← Iso.eq_comp_inv]

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✝
J : Type w
K : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi (map p)

Tactic:
rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoProduct _).hom by aesop]

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
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
⊢ Epi ((biproduct.isoProduct f).inv ≫ biproduct.map p ≫ (biproduct.isoProduct g).hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inl ≫ (biprod.isoCoprod X Y).hom = biprod.inl ≫ biprod.desc coprod.inl coprod.inr

Tactic:
simp [← Iso.eq_comp_inv]

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

Goal state before:
pp: case h₁
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
⊢ biprod.inr ≫ (biprod.isoCoprod X Y).hom = biprod.inr ≫ biprod.desc coprod.inl coprod.inr

Tactic:
simp [← Iso.eq_comp_inv]

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
⊢ f = default

Tactic:
ext x
    rw [Subsingleton.elim x (0 : M)]
    simp

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

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j

Tactic:
· exact h.1

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

Goal state before:
pp: n : ℕ
A : Type u_1
inst✝ : CommMonoid A
a : Fin n → A
x : Composition n
⊢ ∏ i, ∏ j, a ((x.embedding i) j) = ∏ i, a i

Tactic:
by
  simpa [Finset.prod_sigma', Finset.univ_sigma_univ] using! x.blocksFinEquiv.prod_comp a

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

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
⊢ c.blocks = (ones n).blocks

Tactic:
have : c.blocks.length = n := by
      conv_rhs => rw [← c.blocks_sum, A]
      simp

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
this : c.blocks.length = n
⊢ c.blocks = (ones n).blocks
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ c x ∈ s ↔ x ∈ s

Tactic:
notMem_support.mp hx'

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
c : Perm α
s : Finset α
hcs : c.support ⊆ s
x : α
hx' : x ∉ c.support
⊢ x ∈ s ↔ x ∈ s
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l l' : List α
⊢ (zipWith Equiv.swap l l').prod.support ⊆ l.toFinset ⊔ l'.toFinset

Tactic:
by
  intro x hx
  have hx' : x ∈ { x | (zipWith Equiv.swap l l').prod x ≠ x } := by simpa using hx
  simpa using zipWith_swap_prod_support' _ _ hx'

Goal state after:
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
⊢ y = (y :: tl)[0]

Tactic:
getElem_cons_zero

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 = y
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
rw [Finset.card_eq_zero, support_eq_empty_iff]

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

Goal state before:
pp: u : ℤˣ
⊢ u * u = 1

Tactic:
← sq,

Goal state after:
u : ℤˣ
⊢ u ^ 2 = 1
Module: Mathlib.Data.Int.Order.Units

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

Tactic:
rw [div_eq_mul_inv, units_inv_eq_self]

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

Goal state before:
pp: case 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
⊢ (x :: y :: l).rotate n = x' :: y' :: l'

Tactic:
apply List.ext_getElem

Goal state after:
case h.hl
α : 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
⊢ ((x :: y :: l).rotate n).length = (x' :: y' :: l').length

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]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ ↑i) x = y

Tactic:
by
  obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h
  exact ⟨⟨i, hi⟩, hx⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
have h : x ∈ { x | (l.formPerm ^ n) x ≠ x } := h
    rw [← set_support_apply_mem] at h
    replace h := set_support_zpow_subset _ _ h
    simpa using support_formPerm_le' _ h

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

Goal state before:
pp: case pos
α : 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
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ ((σ ^ n) x)) ∈ H

Tactic:
← h5

Goal state after:
case pos
α : 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
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : x = (σ ^ n) x
⊢ swap x (σ x) ∈ H
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → α
a : α
⊢ map (fun x ↦ f^[x] a) (range n) = iterate f a n

Tactic:
apply List.ext_getElem

Goal state after:
case hl
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ (map (fun x ↦ f^[x] a) (range n)).length = (iterate f a n).length

case h
α : Type u_1
n : ℕ
f : α → α
a : α
⊢ ∀ (i : ℕ) (h₁ : i < (map (fun x ↦ f^[x] a) (range n)).length) (h₂ : i < (iterate f a n).length),
    (map (fun x ↦ f^[x] a) (range n))[i] = (iterate f a n)[i]
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : s l.prod = 1
⊢ False

Tactic:
rw [hl.1, hg] at this

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : -1 = 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
⊢ sign f = sign g

Tactic:
have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), e (f x) = g (e x)
hg : g = (e.symm.trans f).trans e
⊢ sign f = sign g
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
z : ℤ
⊢ (f.cycleOf x ^ z) x = (f ^ z) x

Tactic:
cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

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

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

Tactic:
cycleOf_apply_of_not_sameCycle h,

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝ : DecidableRel f.SameCycle
hf : f.IsCycle
hx : f x ≠ x
y : α
h : ¬f.SameCycle x y
⊢ y = f y
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ n ∣ σ.cycleType.lcm

Tactic:
exact dvd_lcm h

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

Goal state before:
pp: M : Type u_1
M' : Type u_2
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst✝⁶ : SMul M β
inst✝⁵ : SMul M' β
inst✝⁴ : SMul M F
inst✝³ : SMul M' F
inst✝² : IsSMulApply M F α β
inst✝¹ : IsSMulApply M' F α β
inst✝ : SMulCommClass M M' β
x✝² : M
x✝¹ : M'
x✝ : F
⊢ ∀ (x : α), (x✝² • x✝¹ • x✝) x = (x✝¹ • x✝² • x✝) x

Tactic:
simp [smul_comm]

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

Goal state before:
pp: case mp.mk.refine_2
α : 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
⊢ c.Disjoint (l.erase c).prod

Tactic:
exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ #σ.supportᶜ ≡ Fintype.card α [MOD p]

Tactic:
Nat.modEq_iff_dvd',

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ Fintype.card α - #σ.supportᶜ

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ #σ.supportᶜ ≤ Fintype.card α
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ p ∣ σ.cycleType.sum

Tactic:
refine Multiset.dvd_sum fun k hk => ?_

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
k : ℕ
hk : k ∈ σ.cycleType
⊢ p ∣ k
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
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]

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

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Function.End α
p n : ℕ
hp : Fact (Nat.Prime p)
hf : f ^ p ^ n = 1
σ : α ≃ α := { toFun := f, invFun := f ^ (p ^ n - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ n = 1
⊢ Fintype.card α ≡ Fintype.card ↑(fixedPoints f) [MOD p]
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (c • x) i_1).support') }
      p =
    (c •
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') })
      p

Tactic:
by
    dsimp
    simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.smul_apply,
      (f p).map_update_smul]

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
A : Matrix n n R
p q : n
hpq : p ≠ q
hrow : A.row p = A.row q
s t : ℤˣ
⊢ detp s A = detp t A

Tactic:
have : A.detp 1 = A.detp (-1) := sum_equiv (.mulRight <| swap p q) (by simp [hpq])
    fun _ _ ↦ prod_equiv (swap p q) (by simp) (by aesop (add simp row))
  obtain rfl | rfl := Int.units_eq_one_or s <;>
  obtain rfl | rfl := Int.units_eq_one_or t <;>
  first | rfl | rw [this]

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
A B : Matrix n n R
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign (t * s) ↔ ∃ a ∈ ofSign t, a * σ = τ

Tactic:
← eq_mul_inv_iff_mul_eq,

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
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign (t * s) ↔ ∃ a ∈ ofSign t, 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 : Matrix n n R
⊢ ∑ σ, sign σ • ∏ i, M (σ i) i = detp 1 M - detp (-1) M

Tactic:
← Equiv.sum_comp (Equiv.inv (Perm n)),

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ i, sign ((Equiv.inv (Perm n)) i) • ∏ i_1, M (((Equiv.inv (Perm n)) i) i_1) i_1 = detp 1 M - detp (-1) M
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this✝ : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
C_subset_A : ∀ (i : ι), C i ⊆ A i
A_eq_BC : (fun i ↦ ∑ j ∈ A i, g i j) = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j)
Beq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j) = fun i ↦ ∑ j ∈ B i, g i j
Ceq : update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ C i₀, g i₀ j) = fun i ↦ ∑ j ∈ C i, g i j
this : ∑ i, #(B i) < n
⊢ (f fun i ↦ ∑ j ∈ B i, g i j) = ∑ r ∈ piFinset B, f fun i ↦ g i (r i)

Tactic:
exact IH _ this B rfl

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ ∃ W h, h ≫ f = h ≫ g

Tactic:
refine ⟨c.pt, c.π.app ⟨WalkingParallelPair.zero⟩, ?_⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type w} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
this : Nonempty C
X Y : C
f g : X ⟶ Y
c : Cone (ULiftHom.down ⋙ ULift.downFunctor ⋙ parallelPair f g)
⊢ c.π.app { down := WalkingParallelPair.zero } ≫ f = c.π.app { down := WalkingParallelPair.zero } ≫ g
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
⊢ Function.Bijective (F.descColimitType F.coconeTypes)

Tactic:
convert! Function.bijective_id

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
⊢ F.descColimitType F.coconeTypes = id