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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)

Tactic:
ext1

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₁ = colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
ext1

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂
Module: Mathlib.CategoryTheory.Limits.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P : C
f g : P ⟶ ⊤_ C
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P : C
f g : ⊥_ C ⟶ P
⊢ f = g

Tactic:
ext ⟨⟨⟩⟩

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u₂
inst✝⁶ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝⁵ : HasBinaryProduct A B
inst✝⁴ : HasBinaryProduct A' B'
inst✝³ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝² : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
inst✝¹ : IsIso (prodComparison F A B)
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (prod.map f g) = prod.map (F.map f) (F.map g) ≫ inv (prodComparison F A' B')

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
j : J
⊢ (liftCocone D s c p hp).ι.app j ≫ homMk (hc.desc ((forget X).mapCocone t)) ⋯ = t.ι.app j

Tactic:
by
    ext
    simp [dsimp% hc.fac ((forget X).mapCocone t) j]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsLimit (mk (𝟙 X) (𝟙 X) ⋯)
Z : C
g h : Z ⟶ X
eq : g ≫ f = h ≫ f
⊢ g = h

Tactic:
rcases PullbackCone.IsLimit.lift' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
⊢ 𝟙 Y ≫ s.inl = s.inr

Tactic:
by rw [← cancel_epi f, Category.id_comp, s.condition]

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

Goal state before:
pp: case unique_from.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ G ⟶ F

Tactic:
refine
      { app := fun X => (hF _).from_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_tgt _ _

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
t : Fork f g
hs : ∀ (s : Fork f g), ∃! l, l ≫ t.ι = s.ι
⊢ IsLimit t

Tactic:
choose d hd hd' using hs
  exact Fork.IsLimit.mk _ d hd fun s m hm => hd' _ _ hm

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

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

Tactic:
apply of_epi_zero X Y

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      (image.lift
            { I := pullback h y, m := pullback.snd h y ≫ image.ι f, m_mono := ⋯,
              e := pullback.lift x (factorThruImage f) ⋯, fac := ⋯ } ≫
          pullback.fst h y) ≫
        h =
    factorThruImage f ≫ y

Tactic:
simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc]

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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm : Mono h
⊢ (c.ι ≫ f) ≫ h = (c.ι ≫ g) ≫ h

Tactic:
exact congrArg (· ≫ h) c.condition

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ g = 0

Tactic:
← cokernel.π_desc f g h,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X Y : C
f : X ⟶ Y
inst✝ : HasColimit (parallelPair f 0)
w : cokernel.π f = 0
R✝ : C
g : Y ⟶ R✝
h : f ≫ g = 0
⊢ cokernel.π f ≫ cokernel.desc f g h = 0
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:
rw [← PreservesColimitPair.iso_hom]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ ((F.mapBiproduct f).hom ≫ desc fun j ↦ F.map (g j)) = F.map (desc g)

Tactic:
← biproduct.mapBiproduct_inv_map_desc,

Goal state after:
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
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
⊢ (F.mapBiproduct f).hom ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = F.map (desc g)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ Discrete.functor f ⋙ G ≅ Discrete.functor fun j ↦ G.obj (f j)

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (G.mapCone (Fan.mk P g)) ≅ Fan.mk (G.obj P) fun j ↦ G.map (g j)

Tactic:
· exact Discrete.natIso fun j => Iso.refl (G.obj (f j.as))

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
⊢ (Cone.postcompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj (G.mapCone (Fan.mk P g)) ≅
    Fan.mk (G.obj P) fun j ↦ G.map (g j)
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 : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) =
    ι (Subtype.restrict p f) i ≫ if h : p j then π (Subtype.restrict p f) ⟨j, h⟩ else 0

Tactic:
rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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 : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) =
    (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i

Tactic:
rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.fstKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ Y
hq : q ≫ b.inr = m - (f ≫ b.inl + g ≫ b.inr)
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inr_snd, ← Category.assoc, hq, h₂',
        zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst✝¹ : IsIso f₁₁
inst✝ : IsIso (ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂
R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂
g : X₂ ⟶ Y₂
w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g
this✝ : IsIso (biprod.map f₁₁ g) := isoElim'._proof_1 f₁₁ f₁₂ f₂₁ f₂₂ L R g w
this : IsIso g := isIso_right_of_isIso_biprod_map f₁₁ g
⊢ X₂ ≅ Y₂

Tactic:
exact asIso g

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

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ f x = f ((f ^ (n + 1)) x) ∨ (f ^ (n + 1))⁻¹ x = f x

Tactic:
← mul_apply,

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ f x = (f * f ^ (n + 1)) x ∨ (f ^ (n + 1))⁻¹ x = f x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = f x ∨ x = (f ^ (n + 1)) (f x)

Tactic:
← mul_apply,

Goal state after:
α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = f x ∨ x = (f ^ (n + 1) * f) x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c = c'

Tactic:
ext1

Goal state after:
case refl
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n
H : ⟨n, c⟩.snd.blocks = ⟨n, c'⟩.snd.blocks
⊢ c.blocks = c'.blocks
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
← mul_apply,

Goal state after:
α : Type u_1
f : Perm α
n : ℕ
x : α
⊢ (f * f ^ n) x = (f ^ n) x ↔ f x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ f ((f ^ n) x) = (f ^ n) x ↔ f x = x

Tactic:
← mul_apply,

Goal state after:
α : Type u_1
f : Perm α
n : ℤ
x : α
⊢ (f * f ^ n) x = (f ^ n) x ↔ f x = x
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
ext1

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
⊢ c.blocks = (ones n).blocks
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ n = ∑ i, 1

Tactic:
by simp [length_n]

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

Goal state before:
pp: case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c = single n h

Tactic:
ext1

Goal state after:
case mpr
n : ℕ
h : 0 < n
c : Composition n
H : c.length = 1
⊢ c.blocks = (single n h).blocks
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
⊢ (ones n).reverse = ones n

Tactic:
ext1

Goal state after:
n : ℕ
⊢ (ones n).reverse.blocks = (ones n).blocks
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (single n hn).reverse = single n hn

Tactic:
ext1

Goal state after:
n : ℕ
hn : 0 < n
⊢ (single n hn).reverse.blocks = (single n hn).blocks
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.viaFintypeEmbedding f) (f a) = f (e a)

Tactic:
rw [Equiv.Perm.viaFintypeEmbedding]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
a : α
⊢ (e.extendDomain f.toEquivRange) (f a) = f (e a)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
⊢ (∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j) → j ∈ c.boundaries

Tactic:
· rintro ⟨i, hi, H⟩
    convert! (c.boundaries.orderIsoOfFin rfl ⟨i, hi⟩).2
    have : c.boundary ⟨i, hi⟩ = j := by rwa [Fin.ext_iff, ← c.blocks_partial_sum hi]
    exact this.symm

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

Goal state before:
pp: n✝ n : ℕ
c : Composition n
⊢ (fun c ↦ c.toComposition) ((fun c ↦ c.toCompositionAsSet) c) = c

Tactic:
ext1

Goal state after:
n✝ n : ℕ
c : Composition n
⊢ ((fun c ↦ c.toComposition) ((fun c ↦ c.toCompositionAsSet) c)).blocks = c.blocks
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
by_cases hx : x ∈ z :: l

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∈ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun c ↦ c.toCompositionAsSet) ((fun c ↦ c.toComposition) c) = c

Tactic:
ext1

Goal state after:
n✝ n : ℕ
c : CompositionAsSet n
⊢ ((fun c ↦ c.toCompositionAsSet) ((fun c ↦ c.toComposition) c)).boundaries = c.boundaries
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support

Tactic:
· intro
    simp only [mem_insert, mem_singleton]
    rintro (rfl | rfl | rfl | _) <;>
      simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : f x = x
⊢ (swap x (f x) * f).support = f.support \ {x}

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
⊢ (swap x (f x) * f).support = f.support \ {x}

Tactic:
· simp [hx, sdiff_singleton_eq_erase, notMem_support.mpr hx, erase_eq_of_notMem, pull_end]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
⊢ (swap x (f x) * f).support = f.support \ {x}
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm (x :: xs)[xs.length] = x

Tactic:
by
  rw [getElem_cons_length rfl, formPerm_apply_getLast]

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

Goal state before:
pp: case neg
α : 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 : β
pb : ¬p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
· rw [extendDomain_apply_not_subtype _ _ pb]
    simp only [not_exists, false_iff, not_and, not_true]
    rintro a _ rfl
    exact pb (Subtype.prop _)

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

Goal state before:
pp: case intro
α : 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)
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))

Tactic:
rw [coe_union] at *

Goal state after:
case intro
α : 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
⊢ IsConj (σ * τ) (f * σ * f⁻¹ * (g * τ * g⁻¹))
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
simpa using h.disjoint_support

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z

Tactic:
rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ f ((f ^ i) x) = (f ^ i) x

Tactic:
← mul_apply,

Goal state after:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ f x = x ↔ (f * f ^ i) x = (f ^ i) x
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, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

Tactic:
by
  obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'
  · refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩
    rw [pow_orderOf_eq_one, pow_zero]
  · exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a)) ((f ^ a) g) = y

Tactic:
← mul_apply,

Goal state after:
α : Type u_2
f : Perm α
x y : α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
g : α
hg : f g ≠ g ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle g y
a : ℤ
ha : (f ^ a) g = x
b : ℤ
hb : (f ^ b) g = y
⊢ (f ^ (b - a) * f ^ a) g = y
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (swap x y).signAux (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux

Tactic:
exact (MonoidHom.mk' signAux signAux_mul).map_isConj
      (isConj_swap hxy (by exact of_decide_eq_true rfl))

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

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g (p x) = p x ↔ g x = x

Tactic:
← mul_apply,

Goal state after:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ (g * p) x = p x ↔ g x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
replace hb : (swap x (f.symm x) * f⁻¹) (f.symm b) ≠ f.symm b := by
      rw [mul_apply, swap_apply_def]
      split_ifs <;> simp [symm_apply_eq, eq_symm_apply] at * <;> tauto

Goal state after:
case inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ n) ((Equiv.symm f) x) = (Equiv.symm f) b

Tactic:
← mul_apply,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
⊢ (Equiv.symm f ^ n * Equiv.symm f) x = (Equiv.symm f) b
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case e'_2
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹) (((swap x (f x) * f)⁻¹ ^ i) (f x)) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)

Tactic:
← mul_apply,

Goal state after:
case e'_2
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
b x : α
f : Perm α
h : (f ^ Int.negSucc n) (f x) = b
hfxb : f x ≠ b
hfb : f b ≠ b
hbx : b ≠ x
hb : (swap x ((Equiv.symm f) x) * f⁻¹) ((Equiv.symm f) b) ≠ (Equiv.symm f) b
i : ℤ
hi : ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x) = (Equiv.symm f) b
⊢ (swap x (f⁻¹ x) * f⁻¹ * (swap x (f x) * f)⁻¹ ^ i) (f x) =
    ((swap x ((Equiv.symm f) x) * Equiv.symm f) ^ i) ((Equiv.symm f) x)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ k) ((f ^ n) z) = (f ^ k) (1 z)

Tactic:
← mul_apply,

Goal state after:
case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
z : α
hz : ¬f z = z
k : ℕ
hx : (f ^ k) z ∈ f.support
H : (f ^ k) z ∉ (f ^ n).support
⊢ (f ^ k * f ^ n) z = (f ^ k) (1 z)