mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯) ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      data.mapZ (Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)

Tactic:
rw [← data.mapZ_comp, ← data.mapZ_comp]

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ
      (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯ ≫
        Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ
      (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯ ≫
        Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hI : F.I = F'.I
hm : F.m = eqToHom hI ≫ F'.m
⊢ F = F'

Tactic:
obtain ⟨_, Fm, _, Ffac⟩ := F

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝ : Mono Fm
e✝ : X ⟶ I✝
Ffac : e✝ ≫ Fm = f
hI : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.I = F'.I
hm : { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac }.m = eqToHom hI ≫ F'.m
⊢ { I := I✝, m := Fm, m_mono := m_mono✝, e := e✝, fac := Ffac } = F'
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ g

Tactic:
rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (terminalComparison G)

Tactic:
by
  rw [← PreservesTerminal.iso_hom]
  infer_instance

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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesColimit K (F ⋙ G)
inst✝ : ReflectsColimit (K ⋙ F) G
c : Cocone K
h : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
by
    apply isColimitOfReflects G
    apply isColimitOfPreserves (F ⋙ G) h

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

Goal state before:
pp: case e_toSemigroup
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝¹ : IsLeftCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝ : IsLeftCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsLeftCancelMul := toIsLeftCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }.toMonoid
⊢ toSemigroup✝¹ = toSemigroup✝

Tactic:
injection h

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

Goal state before:
pp: case e_toOne
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝¹ : IsLeftCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝ : IsLeftCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsLeftCancelMul := toIsLeftCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }.toMonoid
⊢ toOne✝¹ = toOne✝

Tactic:
injection h

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

Goal state before:
pp: case e_toNPow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝¹ : IsLeftCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝ : IsLeftCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsLeftCancelMul := toIsLeftCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }.toMonoid
⊢ toNPow✝¹ = toNPow✝

Tactic:
injection h

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

Goal state before:
pp: case e_toSemigroup
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toSemigroup✝¹ = toSemigroup✝

Tactic:
injection h

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

Goal state before:
pp: case e_toOne
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toOne✝¹ = toOne✝

Tactic:
injection h

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

Goal state before:
pp: case e_toNPow
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ toNPow✝¹ = toNPow✝

Tactic:
injection h

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
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ IsZero c.pt

Tactic:
IsZero.iff_id_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 𝟙 c.pt = 0
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
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ IsZero c.pt

Tactic:
IsZero.iff_id_eq_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 𝟙 c.pt = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case isTrue
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)
j✝¹ j✝ : J
h✝ : j✝ = j✝¹
⊢ eqToHom ⋯ ≫ p j✝¹ = Sigma.ι f j✝ ≫ Sigma.map p ≫ Sigma.desc (ι g) ≫ π g j✝¹

Tactic:
subst_vars
      simp

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
inst✝ : HasZeroObject C
⊢ IsZero (F.obj 0)

Tactic:
IsZero.iff_id_eq_zero,

Goal state after:
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
inst✝ : HasZeroObject C
⊢ 𝟙 (F.obj 0) = 0
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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    if h : ⟨j, x⟩ = ⟨j', y⟩ then eqToHom ⋯ else 0

Tactic:
split_ifs with h
          · obtain ⟨rfl, rfl⟩ := h
            simp
          · simp only [Sigma.mk.inj_iff, not_and] at h
            by_cases w : j = j'
            · cases w
              simp only [heq_eq_eq, forall_true_left] at h
              simp [biproduct.ι_π_ne _ h]
            · simp [biproduct.ι_π_ne_assoc _ w]

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

Goal state before:
pp: case succ.right
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)

Tactic:
induction n with
  | zero => exact List.pairwise_singleton _ _
  | succ n n_ih =>
    rw [List.Nat.antidiagonal_succ]
    refine List.Pairwise.cons (fun a ha x hx₁ hx₂ => ?_) (n_ih.map _ fun a b h x hx₁ hx₂ => ?_)
    · 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
    · rw [List.mem_map] at hx₁ hx₂
      obtain ⟨⟨x₁, hx₁, rfl⟩, ⟨x₂, hx₂, h₁₂⟩⟩ := hx₁, hx₂
      dsimp at h₁₂
      rw [Fin.cons_inj, Nat.succ_inj] at h₁₂
      obtain ⟨h₁₂, rfl⟩ := h₁₂
      rw [Function.onFun, h₁₂] at h
      exact h (List.mem_map_of_mem hx₁) (List.mem_map_of_mem hx₂)

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

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

Tactic:
List.flatMap_singleton,

Goal state after:
k : ℕ
⊢ map (fun x ↦ Fin.cons (0, 0).1 x) (antidiagonalTuple k (0, 0).2) = [0]
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2)) (map (fun i ↦ (i, n - i)) (range n)) ++
      flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2)) [(n, 0)] =
    [![n]]

Tactic:
List.flatMap_singleton,

Goal state after:
n : ℕ
⊢ flatMap (fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple 0 ni.2)) (map (fun i ↦ (i, n - i)) (range n)) ++
      map (fun x ↦ Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
| n

Tactic:
rw [← c.blocks_sum, ← ofFn_blocksFun, sum_ofFn]

Goal state after:
n : ℕ
c : Composition n
| ∑ i, c.blocksFun i
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ j ∈ Set.range ⇑(c.embedding (c.index j))

Tactic:
have : c.embedding (c.index j) (c.invEmbedding j) ∈ Set.range (c.embedding (c.index j)) :=
    Set.mem_range_self _
  rwa [c.embedding_comp_inv j] at this

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.blocks.length ≤ c.length

Tactic:
by simp [blocks]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hy : y ∈ (swap x (f x) * f).support
⊢ y ∈ f.support ∧ y ≠ x

Tactic:
by
  simp only [mem_support, swap_apply_def, mul_apply, f.injective.eq_iff] at *
  grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < xs.length
⊢ xs.formPerm xs[i] = xs[(i + 1) % xs.length]

Tactic:
rcases xs with - | ⟨x, xs⟩

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
w : [].Nodup
h : i < [].length
⊢ [].formPerm [][i] = [][(i + 1) % [].length]

case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ #{x | σ x = x} + 1 < Fintype.card α

Tactic:
← Nat.lt_sub_iff_add_lt',

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h : σ ≠ 1
⊢ 1 < Fintype.card α - #{x | σ x = x}
Module: Mathlib.GroupTheory.Perm.Finite

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

Tactic:
rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
        apply_mem_support, mem_support]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))

Goal state after:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
this : 0 ≤ n % ↑(orderOf f)
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

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

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
hx : x ∉ c.support
⊢ g (c x) = c (g x)

Tactic:
· rw [notMem_support.mp hx, eq_comm, ← notMem_support]
      contrapose hx
      exact (hc' x).mp hx

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

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

Tactic:
induction σ using cycle_induction_on with
  | base_one => simp
  | base_cycles σ hσ => rw [hσ.cycleType, Multiset.sum_singleton]
  | induction_disjoint σ τ hd _ hσ hτ => rw [hd.cycleType_mul, sum_add, hσ, hτ, hd.card_support_mul]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
⊢ ∀ (x : ↥(H i)) (y : ↥(H j)), Commute ((H i).subtype x) ((H j).subtype y)

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute ((H i).subtype ⟨x, hx⟩) ((H j).subtype ⟨y, hy⟩)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝
l : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, g x ≠ x → x ∈ []
⊢ [].prod = g ∧ (∀ g' ∈ [], g'.IsCycle) ∧ List.Pairwise Disjoint []

Tactic:
simp only [imp_false, List.Pairwise.nil, List.not_mem_nil, forall_const, and_true,
          forall_prop_of_false, Classical.not_not, not_false_iff, List.prod_nil] at *

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝
l : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
hg : ∀ {x : α}, g x = x
⊢ 1 = g
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
this : (g ^ m) x = x ↔ g ^ m = 1
hm0 : ¬m = 0
⊢ g ^ m = 1 ↔ m = 0

Tactic:
· simp only [hm0, iff_false]
    exact pow_ne_one_of_lt_orderOf hm0 div_euc.2

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

Goal state before:
pp: case refine_2
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
v : ↑(vectorsProdEqOne G p)
hv1 : σ v = v
hv2 : v ≠ v₀
g : G
hg : ↑↑v = List.replicate (↑↑v).length g
hg' : g = 1
⊢ List.replicate p 1 = ↑↑v₀

Tactic:
simp only [v₀, List.Vector.replicate]

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

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

Tactic:
by
  rw [← card_cycleType_eq_one, h.cycleType, card_singleton]

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

Goal state before:
pp: case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)

Tactic:
rw [add_assoc]

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

Goal state before:
pp: case a.add_assoc
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x + descFunLift F s y + descFunLift F s z =
    descFunLift F s x + (descFunLift F s y + descFunLift F s z)

Tactic:
rw [add_assoc]

Goal state after: