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

Goal state before:
pp: case zero.one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : zero ⟶ one
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases f

Goal state after:
case zero.one.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map left ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map left

case zero.one.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map right ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map right
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case one.zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : one ⟶ zero
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases f

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

Goal state before:
pp: case one.one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
f : one ⟶ one
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases f

Goal state after:
case one.one.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id one) ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f) ⋯ ≫
      (parallelPair f g).map (WalkingParallelPairHom.id one)
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
P : C
π : Y ⟶ P
w : f✝ ≫ π = g ≫ π
i j : WalkingParallelPair
f : i ⟶ j
⊢ (parallelPair f✝ g).map f ≫ WalkingParallelPair.casesOn j (f✝ ≫ π) π =
    WalkingParallelPair.casesOn i (f✝ ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map f

Tactic:
cases f

Goal state after:
case left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map left ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map left

case right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (parallelPair f g).map right ≫ WalkingParallelPair.casesOn one (f ≫ π) π =
    WalkingParallelPair.casesOn zero (f ≫ π) π ≫ ((Functor.const WalkingParallelPair).obj P).map right

case id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
i : WalkingParallelPair
⊢ (parallelPair f g).map (WalkingParallelPairHom.id i) ≫ WalkingParallelPair.casesOn i (f ≫ π) π =
    WalkingParallelPair.casesOn i (f ≫ π) π ≫
      ((Functor.const WalkingParallelPair).obj P).map (WalkingParallelPairHom.id i)
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
R : Type u
inst✝ : Semiring R
M N : SemimoduleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

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

Goal state after:
R : Type u
inst✝¹ : Semiring R
M : SemimoduleCat R
inst✝ : Subsingleton ↑M
X : SemimoduleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f✝ g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f✝ g
f : { pt := pt✝¹, π := π✝¹ } ⟶ { pt := pt✝, π := π✝ }
⊢ f.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }

Tactic:
cases f

Goal state after:
case mk.mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
pt✝¹ : C
π✝¹ : (Functor.const WalkingParallelPair).obj pt✝¹ ⟶ parallelPair f g
pt✝ : C
π✝ : (Functor.const WalkingParallelPair).obj pt✝ ⟶ parallelPair f g
hom✝ : { pt := pt✝¹, π := π✝¹ }.pt ⟶ { pt := pt✝, π := π✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), hom✝ ≫ { pt := pt✝, π := π✝ }.π.app j = { pt := pt✝¹, π := π✝¹ }.π.app j
⊢ { hom := hom✝, w := w✝ }.hom ≫ ι { pt := pt✝, π := π✝ } = ι { pt := pt✝¹, π := π✝¹ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f✝ g ⟶ (Functor.const WalkingParallelPair).obj pt✝
f : { pt := pt✝¹, ι := ι✝¹ } ⟶ { pt := pt✝, ι := ι✝ }
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ f.hom = Cofork.π { pt := pt✝, ι := ι✝ }

Tactic:
cases f

Goal state after:
case mk.mk.mk
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
pt✝¹ : C
ι✝¹ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝¹
pt✝ : C
ι✝ : parallelPair f g ⟶ (Functor.const WalkingParallelPair).obj pt✝
hom✝ : { pt := pt✝¹, ι := ι✝¹ }.pt ⟶ { pt := pt✝, ι := ι✝ }.pt
w✝ : ∀ (j : WalkingParallelPair), { pt := pt✝¹, ι := ι✝¹ }.ι.app j ≫ hom✝ = { pt := pt✝, ι := ι✝ }.ι.app j
⊢ Cofork.π { pt := pt✝¹, ι := ι✝¹ } ≫ { hom := hom✝, w := w✝ }.hom = Cofork.π { pt := pt✝, ι := ι✝ }
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:
rw [← PreservesTerminal.iso_hom]
  infer_instance

Goal state after:
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
  apply isoZeroOfMonoZero (Y := Y) ‹_›

Goal state after:
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
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
⊢ m = s.π

Tactic:
convert! h
    exact (Category.id_comp _).symm

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
inst✝¹ : HasKernel f
W : C
k : W ⟶ X
h : k ≫ f = 0
inst✝ : Mono k
Z : C
g g' : Z ⟶ W
w : g ≫ lift f k h = g' ≫ lift f k h
⊢ g = g'

Tactic:
by
    replace w := w =≫ kernel.ι f
    simp only [Category.assoc, kernel.lift_ι] at w
    exact (cancel_mono k).1 w

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'
s : KernelFork f
hs : IsLimit s
s' : KernelFork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : e.hom ≫ Fork.ι s' = Fork.ι s ≫ eX.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ∀ (j : WalkingParallelPair), ((Cone.postcompose α.hom).obj s).π.app j = e.hom ≫ s'.π.app j

Tactic:
by rintro (_ | _) <;> simp [α, ← 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
W : C
g : W ⟶ X
h✝ : W ⟶ Y
c : CokernelCofork h✝
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h✝
s : Cofork f 0
m : (CokernelCofork.ofπ (Cofork.π c) hf).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π c) hf) ≫ m = s.π
⊢ m = i.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
by
      apply Cofork.IsColimit.hom_ext i
      simpa using h

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
F : J → C
c c' : Bicone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
c c' : Bicone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wπ✝ : ∀ (j : J), hom✝ ≫ c'.π j = c.π j
wι✝ : ∀ (j : J), c.ι j ≫ hom✝ = c'.ι j
w : { hom := hom✝, wπ := wπ✝, wι := wι✝ }.hom = g.hom
⊢ { hom := hom✝, wπ := wπ✝, wι := wι✝ } = g
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'
s : CokernelCofork f
hs : IsColimit s
s' : CokernelCofork f'
eX : X ≅ X'
eY : Y ≅ Y'
e : s.pt ≅ s'.pt
H : eX.hom ≫ f' = f ≫ eY.hom
H' : eY.hom ≫ Cofork.π s' = Cofork.π s ≫ e.hom
α : parallelPair f 0 ≅ parallelPair f' 0 := parallelPairIsoMk eX eY ⋯ ⋯
⊢ ∀ (j : WalkingParallelPair), ((Cocone.precompose α.symm.hom).obj s).ι.app j ≫ e.hom = s'.ι.app j

Tactic:
by rintro (_ | _) <;> simp [α, ← H']

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
P Q : C
c c' : BinaryBicone P Q
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
wfst✝ : hom✝ ≫ c'.fst = c.fst
wsnd✝ : hom✝ ≫ c'.snd = c.snd
winl✝ : c.inl ≫ hom✝ = c'.inl
winr✝ : c.inr ≫ hom✝ = c'.inr
w : { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ }.hom = g.hom
⊢ { hom := hom✝, wfst := wfst✝, wsnd := wsnd✝, winl := winl✝, winr := winr✝ } = g
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map A.inr ≫ F.map A.fst = 0

Tactic:
by rw [← F.map_comp, A.inr_fst, F.map_zero]

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

Goal state before:
pp: C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ inl ≫ map' f g = f ≫ inl

Tactic:
exact IsColimit.ι_map (BinaryBiproduct.isColimit W X) _ _ ⟨WalkingPair.left⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f g : M.Hom N
h : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Goal state after:
case _private.Mathlib.Algebra.Category.ModuleCat.Basic.0.ModuleCat.Hom.mk
R : Type u
inst✝ : Ring R
M N : ModuleCat R
g : M.Hom N
hom'✝ : ↑M →ₗ[R] ↑N
h : { hom' := hom'✝ }.hom = g.hom
⊢ { hom' := hom'✝ } = g
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
x : ↑M
⊢ (Hom.hom f) x = (Hom.hom default) x

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

Goal state after:
R : Type u
inst✝¹ : Ring R
M : ModuleCat R
inst✝ : Subsingleton ↑M
X : ModuleCat R
f : M ⟶ X
x : ↑M
⊢ (Hom.hom f) 0 = (Hom.hom default) 0
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : ¬i = c.index j
⊢ j ∉ Set.range ⇑(c.embedding i)

Tactic:
exact Set.disjoint_right.1 (c.disjoint_range h) (c.mem_range_embedding j)

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

Goal state before:
pp: n : ℕ
⊢ Fintype.card (CompositionAsSet n) = 2 ^ (n - 1)

Tactic:
by
  have : Fintype.card (Finset (Fin (n - 1))) = 2 ^ (n - 1) := by simp
  rw [← this]
  exact Fintype.card_congr (compositionAsSetEquiv n)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ f ((Equiv.symm g) x) = a

Tactic:
← hg.2

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
f : Equiv.Perm α
hf₁ : f ∈ permsOfList l
hf₂ : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
x : α
hx : x ∈ l
hx' : f ∈ List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a x * g = f
⊢ (Equiv.swap a x * g) ((Equiv.symm g) x) = a
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ (k + 1) % l.length = k ↔ l.length ≤ 1

Tactic:
cases hn : l.length

Goal state after:
case zero
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
hn : l.length = 0
⊢ (k + 1) % 0 = k ↔ 0 ≤ 1

case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
t : Finset ι
s : ι → ℕ
x : ℕ
⊢ (∏ i ∈ t, s i).Coprime x ↔ ∀ i ∈ t, (s i).Coprime x

Tactic:
simpa using coprime_multiset_prod_left_iff (m := t.val.map s)

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

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ #(f ^ n).support = orderOf f

Tactic:
hr,

Goal state after:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
⊢ #f.support = orderOf f
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
⊢ f ^ a = f ^ b

Tactic:
wlog hab : a ≤ b generalizing a b

Goal state after:
case intro.mpr.inr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
x : β
hx : f x ≠ x
hx' : (f ^ a) x = (f ^ b) x
this : ∀ {a b : ℕ}, (f ^ a) x = (f ^ b) x → a ≤ b → f ^ a = f ^ b
hab : ¬a ≤ b
⊢ f ^ a = f ^ b

β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ f ^ a = f ^ b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ (f ^ (b - a)) ((f ^ a) x) = (f ^ a) x

Tactic:
simp [pow_sub _ hab, ← hx']

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

Goal state before:
pp: case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
have h := @Equiv.Perm.zpow_apply_comm _ f 1 a x

Goal state after:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
h : (f ^ 1) ((f ^ ↑a) x) = (f ^ ↑a) ((f ^ 1) x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
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)
this : DecidableEq ι := ⋯
⊢ ⨆ i, mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)

Tactic:
refine iSup_le ?_

Goal state after:
case a
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)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := ⋯
⊢ ⨆ i, (ϕ i).range ≤ (noncommPiCoprod ϕ hcomm).range

Tactic:
refine iSup_le ?_

Goal state after:
case a
G : Type u_1
inst✝² : Group G
ι : Type u_2
H : ι → Type u_3
inst✝¹ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ (i : ι), (ϕ i).range ≤ (noncommPiCoprod ϕ hcomm).range
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case h
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hgc : Commute g c
hgc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
a : α
ha : a ∈ c.support
i : ℤ
hi : (c ^ i) a = g a
j : ℤ
hx : (c ^ j) a ∈ c.support
⊢ (c ^ i) a = g a

Tactic:
exact hi

Goal state after:
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:
by
      { 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 *
        ext
        simp [*]}

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i < j
⊢ j.cycleRange i = i + 1

Tactic:
by
  rw [cycleRange_of_le h.le, if_neg h.ne]

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

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ (i.cycleIcc j) k = k

Tactic:
have : (((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩)
      = subNat i.1 (k.cast (by lia)) (by simp; lia) := by
      simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)

Goal state after:
case pos
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ (i.cycleIcc j) k = k
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case pos
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
this : subNat (↑i) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
⊢ ↑(Fin.cast ⋯ ((((j - i).castLT ⋯).cycleRange (subNat (↑i) (Fin.cast ⋯ k) ⋯)).addNat (n - (n - ↑i)))) = ↑i

Tactic:
simp [ch, cycleRange_of_eq this]

Goal state after:
case pos
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this✝ :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : k = j
this : subNat (↑i) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
⊢ n - (n - ↑i) = ↑i
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑(vectorsProdEqOne G 1)

Tactic:
one_eq

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
⊢ Unique ↑{1 ::ᵥ Vector.nil}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

Tactic:
obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1

Goal state after:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
m : ℕ
hm : m ∈ σ.cycleType.erase n
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
cycleType_inv

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
h : f.IsThreeCycle
⊢ f.cycleType = {3}