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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasEqualizers C
inst✝ : HasImage f
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso ⋯).hom ≫ ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasEqualizers C
inst✝ : HasImage f
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso ⋯).hom ≫ ι f

Tactic:
simp [asIso, image.eqToIso, image.eqToHom]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g

Tactic:
simp [image.compIso]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage (f ≫ g) ≫ (compIso f g).inv ≫ ι f = factorThruImage (f ≫ g) ≫ ι (f ≫ g) ≫ inv g

Tactic:
simp [image.compIso]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
⊢ I = J

Tactic:
have : I.zero = J.zero := by
    funext X Y
    specialize w X Y
    apply congrArg Zero.mk w
  cases I; cases J
  congr
  · apply proof_irrel_heq
  · apply proof_irrel_heq

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X : C
⊢ ∀ (Y : C), Zero.zero = Zero.zero

Tactic:
Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
⊢ Zero.zero = Zero.zero
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ IsZero X

Tactic:
subst h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ IsZero X
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ IsZero Y

Tactic:
subst h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ IsZero Y
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : f = 0
⊢ X ≅ 0

Tactic:
subst h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Mono 0
⊢ X ≅ 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ Y ≅ 0

Tactic:
subst h

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ Y ≅ 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: case toFun.left
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 X = 0

pp: case toFun.right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 Y = 0

Tactic:
· exact (idZeroEquivIsoZero X).symm eX

Goal state after:
case toFun.right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
eX : X ≅ 0
eY : Y ≅ 0
⊢ 𝟙 Y = 0
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
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit (Cone.whisker e.functor (F.mapCone c))

Tactic:
exact IsLimit.whiskerEquivalence t _

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
X Y : C
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G

Tactic:
by
  apply preservesLimit_of_preserves_limit_cone (prodIsProd X Y)
  apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
  refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
  apply i

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
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
⊢ Fork.ι c ≫ h = 0

Tactic:
by simp [hh]

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

Goal state before:
pp: case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : j = j'
⊢ F.map (b.ι j ≫ b.π j') = eqToHom ⋯

Tactic:
subst h

Goal state after:
case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ F.map (b.ι j ≫ b.π j) = eqToHom ⋯
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 g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).hom ≫ kernel.ι f = kernel.ι f
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 g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).inv ≫ kernel.ι f = kernel.ι g

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).inv ≫ kernel.ι f = kernel.ι f
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq h).hom = kernel.lift g e ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
he : e ≫ f = 0
inst✝ : HasKernel f
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).hom = kernel.lift f e ⋯
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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
X' Y' : C
f' : X' ⟶ Y'
e : Y' ≅ Y
iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0
Z'✝ : C
s : Y' ⟶ Z'✝
hs : f' ≫ s = 0
m : c.pt ⟶ Z'✝
hm : (e.hom ≫ Cofork.π c) ≫ m = s
⊢ Cofork.π c ≫ m = Cofork.π c ≫ hc.desc (ofπ (e.inv ≫ s) ⋯)

Tactic:
simpa [← cancel_epi e.hom] using hm

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✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ f ≫ cokernel.π (image.ι f) = 0

Tactic:
conv =>
          lhs
          congr
          rw [← image.fac f]
        rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero]

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

Goal state before:
pp: case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
h : j✝ = j✝¹
⊢ eqToHom ⋯ ≫ p j✝¹ = p j✝ ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
case pos
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝ : J
⊢ eqToHom ⋯ ≫ p j✝ = p j✝ ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : k = e j
⊢ ι f j ≫ (desc fun j ↦ (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

Tactic:
subst h

Goal state after:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
⊢ ι f j ≫ (desc fun j ↦ (w j).inv ≫ ι g (e j)) ≫ π g (e j) =
    ι f j ≫ (lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g (e j)
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
G : C ⥤ D
e : F ≅ G
X : C
⊢ ∀ {Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g

Tactic:
Y

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
G : C ⥤ D
e : F ≅ G
X Y : C
⊢ ∀ {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : k = e j
⊢ ι g k ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
subst h

Goal state after:
case pos
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
⊢ ι g (e j) ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g (e j) ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
← Category.comp_id m

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m ≫ 𝟙 b.toCone.pt = ∑ j, s.π.app { as := j } ≫ b.ι j
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
β γ : Type
inst✝² : Finite β
ε : β ≃ γ
f : γ → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (f ∘ ⇑ε)
b' : β
⊢ ι (f ∘ ⇑ε) b' ≫ ((desc fun b ↦ ι f (ε b)) ≫ lift fun b ↦ π f (ε b)) ≫ π (f ∘ ⇑ε) b' =
    ι (f ∘ ⇑ε) b' ≫ 𝟙 (⨁ f ∘ ⇑ε) ≫ π (f ∘ ⇑ε) b'
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
⊢ ∀ {m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt},
    Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π → m = (fromSubtype f fun j ↦ j ≠ i) ≫ s.π

Tactic:
by
      intro m hm
      rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.id_comp _).symm

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α : Type u_1
n✝ : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
a : α
n : ℕ
f : Fin (n + 1) → α
h : ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f
r0 : r a (f 0)
i : Fin n
⊢ r a (f i.succ)

Tactic:
exact _root_.trans r0 (h (by grind))

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

Goal state before:
pp: n : ℕ
b : List ℕ
hb₁ : ∀ {i : ℕ}, i ∈ ⟦b⟧ → 0 < i
hb₂ : sum ⟦b⟧ = n
⊢ b.sum = n

Tactic:
by simpa using hb₂

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
⊢ j ∈ Set.range ⇑(c.embedding i) ↔ c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ

Tactic:
constructor
  · intro h
    rcases Set.mem_range.2 h with ⟨k, hk⟩
    rw [Fin.ext_iff] at hk
    dsimp at hk
    rw [← hk]
    simp [sizeUpTo_succ', k.is_lt]
  · intro h
    apply Set.mem_range.2
    refine ⟨⟨j - c.sizeUpTo i, ?_⟩, ?_⟩
    · rw [tsub_lt_iff_left, ← sizeUpTo_succ']
      · exact h.2
      · exact h.1
    · rw [Fin.ext_iff]
      exact add_tsub_cancel_of_le h.1

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

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

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]
    rw [Equiv.Perm.Disjoint.support_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
⊢ (swap x y).support = {x, y} ↔ x ≠ y

Tactic:
refine ⟨fun h => ?_, fun h => support_swap h⟩
  rintro rfl
  simp [Finset.ext_iff] at h

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
⊢ f ∈ permsOfList (a :: l)

Tactic:
refine mem_append_left _ (IH fun x hx => mem_of_ne_of_mem ?_ (h x hx))

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : f a = a
x : α
hx : f x ≠ x
⊢ x ≠ a
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
⊢ f ∈ permsOfList (a :: l)

Tactic:
have : ∀ x : α, (Equiv.swap a (f a) * f) x ≠ x → x ∈ l := by
    simp
    grind

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ≠ x → x ∈ l) → f ∈ permsOfList l
f : Equiv.Perm α
h : ∀ (x : α), f x ≠ x → x ∈ a :: l
hfa : ¬f a = a
hfa' : f (f a) ≠ f a
this : ∀ (x : α), (Equiv.swap a (f a) * f) x ≠ x → x ∈ l
⊢ f ∈ permsOfList (a :: l)
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f = 1

Tactic:
simpa [permsOfList] using h

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ b ∈ (g.extendDomain f).support ↔ b ∈ map f.asEmbedding g.support

Tactic:
simp only [mem_map, Ne,
    mem_support]

Goal state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case mk
α : Type u_1
inst✝ : DecidableEq α
val✝ : Multiset α
l : List α
hs : Multiset.Nodup (Quot.mk (⇑(isSetoid α)) l)
⊢ #(permsOfFinset { val := Quot.mk (⇑(isSetoid α)) l, nodup := hs }) =
    (#{ val := Quot.mk (⇑(isSetoid α)) l, nodup := hs })!

Tactic:
exact length_permsOfList l

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

Goal state before:
pp: case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
y : α
hy✝ : y ∈ σ.support
hy : σ y ≠ y
⊢ ∃ a, (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) a = ⟨y, hy✝⟩

Tactic:
obtain ⟨n, rfl⟩ := (Classical.choose_spec hσ).2 hy

Goal state after:
case right
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
n : ℤ
hy✝ : (σ ^ n) (Classical.choose hσ) ∈ σ.support
hy : σ ((σ ^ n) (Classical.choose hσ)) ≠ (σ ^ n) (Classical.choose hσ)
⊢ ∃ a, (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) a = ⟨(σ ^ n) (Classical.choose hσ), hy✝⟩
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 + 1)) x) ∈ H

Tactic:
rw [pow_succ', mul_apply, ← 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.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs

Tactic:
induction t, s using Quotient.inductionOn₂

Goal state after:
case h
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Finite α
inst✝¹ : DecidableEq β
inst✝ : Finite β
f : Perm α
e : α ≃ β
a✝ : List β
b✝ : List α
hs : ∀ (x : α), x ∈ ⟦b✝⟧
ht : ∀ (x : β), x ∈ ⟦a✝⟧
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑(↑(sign f)).natAbs = 1

Tactic:
Int.units_natAbs,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑1 = 1
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
⊢ #(swap x (f x) * f).support + 1 = #f.support

Tactic:
← insert_erase (mem_support.2 hx.1),

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
⊢ #(swap x (f x) * f).support + 1 = #(insert x (f.support.erase x))
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
⊢ s f = sign f

Tactic:
have hsl : ∀ a ∈ l.map s, a = (-1 : ℤˣ) := fun a ha =>
      let ⟨g, hg⟩ := List.mem_map.1 ha
      hg.2 ▸ this (hl₂ _ hg.1)

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
hsl : ∀ a ∈ List.map (⇑s) l, a = -1
⊢ s f = sign f
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
h : l.Nodup
⊢ l.formPerm.IsCycleOn {a | a ∈ l}

Tactic:
refine ⟨l.formPerm.bijOn fun _ => List.formPerm_mem_iff_mem, fun a ha b hb => ?_⟩
  rw [Set.mem_ofPred, ← List.idxOf_lt_length_iff] at ha hb
  rw [← List.getElem_idxOf ha, ← List.getElem_idxOf hb]
  refine ⟨l.idxOf b - l.idxOf a, ?_⟩
  simp only [sub_eq_neg_add, zpow_add, zpow_neg, Equiv.Perm.inv_eq_iff_eq, zpow_natCast,
    Equiv.Perm.coe_mul, List.formPerm_pow_apply_getElem _ h, Function.comp]
  rw [add_comm]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : DecidableRel f.SameCycle
h : f.SameCycle x y
⊢ f.cycleOf x = f.cycleOf y

Tactic:
by
  ext z
  rw [Equiv.Perm.cycleOf_apply]
  split_ifs with hz
  · exact (h.symm.trans hz).cycleOf_apply.symm
  · exact (cycleOf_apply_of_not_sameCycle (mt h.trans hz)).symm

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]

Goal state after:
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.SameCycle x y