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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasCoproduct fun j ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
b✝ : α
⊢ Sigma.ι (fun j ↦ X.obj { as := j }) b✝ ≫ m = s.ι.app { as := b✝ }

Tactic:
apply hm

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ IsLimit (mk (c.fst ≫ f) c.snd)

Tactic:
fapply BinaryFan.isLimitMk

Goal state after:
case lift
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ (s : BinaryFan X' ((pair X Y).obj { as := right })) →
    s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }

case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), ?lift s ≫ c.fst ≫ f = s.fst

case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), ?lift s ≫ c.snd = s.snd

case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = ?lift s
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
⊢ t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt

Tactic:
exact Fan.IsLimit.lift hc' fun i ↦ Fan.IsLimit.lift (hc i) fun j ↦ t.proj (i, j)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ IsColimit (mk (f ≫ c.inl) c.inr)

Tactic:
by
  fapply BinaryCofan.isColimitMk
  · exact fun s => BinaryCofan.IsColimit.desc h (inv f ≫ s.inl) s.inr
  · simp
  · simp
  · intro s m e₁ e₂
    apply BinaryCofan.IsColimit.hom_ext h
    · rw [← cancel_epi f]
      simpa using e₁
    · simpa

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 ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s : PullbackCone f g
H : IsLimit s
⊢ s.fst ≫ f ≫ i = s.snd ≫ g ≫ i

Tactic:
rw [← Category.assoc, ← Category.assoc, s.condition]

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✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = ((Image.monoFactorisation g).isoComp f).m

Tactic:
dsimp
                    have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
                    rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f F')]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ 𝟙 0 = 0

Tactic:
apply HasZeroObject.from_zero_ext

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₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))

Tactic:
have := (IsLimit.postcomposeInvEquiv h c).symm t

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesLimit K₁ F
c : Cone K₂
t : IsLimit c
this : IsLimit ((Cone.postcompose h.inv).obj c)
⊢ IsLimit ((Cone.postcompose (Functor.isoWhiskerRight h F).inv).obj (F.mapCone c))
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
_X _Y Z : C
f : _X ⟶ _Y
r : ℕ
g : _Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g

Tactic:
by exact (Preadditive.leftComp Z f).map_nsmul r g

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : R
x✝¹ : x✝⁵ ⟶ x✝⁴
x✝ : x✝⁴ ⟶ x✝³
⊢ (x✝² • x✝¹) ≫ x✝ = x✝² • x✝¹ ≫ x✝

Tactic:
ext; apply smul_comp

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✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g (Fork.ι s ≫ f) ⋯

Tactic:
simp_rw [← w]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g ((m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯)) ≫ f) ⋯
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) → W ⟶ f j
⊢ F.map (lift g) ≫ (F.mapBiproduct f).hom = lift fun j ↦ F.map (g j)

Tactic:
by
  ext j
  dsimp only [Function.comp_def]
  simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]

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 : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
rw [← cancel_epi g, ← Category.assoc, ← hh]
            simp

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✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π s) ⋯

Tactic:
simp_rw [← w]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
s : CokernelCofork (f ≫ g)
m : cokernel (?m.116 s) ⟶ ?m.118 s
w : Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m = Cofork.π s
⊢ m = cokernel.desc f (g ≫ Cofork.π (CokernelCofork.ofπ (inv g ≫ cokernel.π f) ⋯) ≫ m) ⋯
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✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
hf : ∀ (Z : C) (g : Y ⟶ Z), f ≫ g = 0 → g = 0
s : Cofork f 0
m : (CokernelCofork.ofπ 0 ⋯).pt ⟶ s.pt
x✝ : Cofork.π (CokernelCofork.ofπ 0 ⋯) ≫ m = s.π
⊢ m = 0

Tactic:
apply HasZeroObject.from_zero_ext

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ F.map (f + g) = F.map f + F.map g

Tactic:
rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod,
      ← biprod.mapBiprod_hom_desc, Category.assoc, Iso.inv_hom_id_assoc, F.map_id,
      biprod.add_eq_lift_id_desc]

Goal state after:
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
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : BinaryBicone P Q
t : (functoriality P Q F).obj X✝ ⟶ (functoriality P Q F).obj Y✝
⊢ F.map (F.preimage t.hom ≫ Y✝.fst) = F.map X✝.fst

Tactic:
by simpa using! t.wfst

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

Goal state before:
pp: J✝¹ : Type w
C✝¹ : Type uC
inst✝¹⁰ : Category.{uC', uC} C✝¹
inst✝⁹ : HasZeroMorphisms C✝¹
D : Type uD
inst✝⁸ : Category.{uD', uD} D
inst✝⁷ : HasZeroMorphisms D
F : J✝¹ → C✝¹
J✝ : Type w
K✝ : Type u_1
C✝ : Type u
inst✝⁶ : Category.{v, u} C✝
inst✝⁵ : HasZeroMorphisms C✝
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
⊢ components (matrix m) = m

Tactic:
by
    ext
    apply biproduct.matrix_components

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

Goal state before:
pp: n : ℕ
x : { x // x ≠ last n }
⊢ (finSuccAboveOrderIso (last n)).symm x = (↑x).castLT ⋯

Tactic:
rw [← Option.some_inj]
  simp [finSuccAboveOrderIso, finSuccAboveEquiv, OrderIso.symm]

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

Goal state before:
pp: n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n : ℕ
p : n.Partition
m : ℕ
⊢ m ∈ p.parts.toFinset ↔ count m p.parts * m ≠ 0

Tactic:
suffices m ∈ p.parts → m ≠ 0 by simpa
    grind

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ c.sizeUpTo ↑(c.index j) ≤ ↑j

Tactic:
by
  by_contra! H
  set i := c.index j
  have i_pos : (0 : ℕ) < i := by
    by_contra! i_pos
    revert H
    simp [nonpos_iff_eq_zero.1 i_pos, c.sizeUpTo_zero]
  let i₁ := (i : ℕ).pred
  have i₁_lt_i : i₁ < i := Nat.pred_lt (ne_of_gt i_pos)
  have i₁_succ : i₁ + 1 = i := Nat.succ_pred_eq_of_pos i_pos
  have := Nat.find_min (c.index_exists j.2) i₁_lt_i
  simp_all [lt_trans i₁_lt_i (c.index j).2]

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

Goal state before:
pp: α : Type u_1
σ τ : Perm α
hστ : σ.Disjoint τ
⊢ σ * τ = 1 ↔ σ = 1 ∧ τ = 1

Tactic:
by
  simp_rw [Perm.ext_iff, one_apply, hστ.mul_apply_eq_iff, forall_and]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x : { a // p a }
h : ∃! a, ↑a = ↑x
⊢ choose (fun y ↦ ↑y = ↑x) h = x

Tactic:
Subtype.ext_iff,

Goal state after:
α : Type u_4
p : α → Prop
inst✝¹ : Fintype { a // p a }
inst✝ : DecidableEq α
x : { a // p a }
h : ∃! a, ↑a = ↑x
⊢ ↑(choose (fun y ↦ ↑y = ↑x) h) = ↑x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ (∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x) →
    c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a)

pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x

Tactic:
· intro h
    constructor
    · intro a ha
      by_contra ha'
      rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
      exact ha rfl
    · intro _ a ha
      rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ c.support ⊆ s ∧ ((∀ (x : α), c x ∈ s ↔ x ∈ s) → ∀ a ∈ s, c a = g a) →
    ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
h : ∀ a ∈ s, c a = g a
a : α
ha : a ∉ s
⊢ a ∉ c.support

Tactic:
exact Finset.notMem_mono hc ha

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

Goal state before:
pp: n✝ n : ℕ
⊢ Function.LeftInverse
    (fun s ↦
      { boundaries := {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset, zero_mem := ⋯,
        getLast_mem := ⋯ })
    fun c ↦ {i | ⟨1 + ↑i, ⋯⟩ ∈ c.boundaries}.toFinset

Tactic:
intro c

Goal state after:
n✝ n : ℕ
c : CompositionAsSet n
⊢ (fun s ↦
        { boundaries := {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset, zero_mem := ⋯,
          getLast_mem := ⋯ })
      ((fun c ↦ {i | ⟨1 + ↑i, ⋯⟩ ∈ c.boundaries}.toFinset) c) =
    c
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
simp [disjoint_iff_eq_or_eq, disjoint_iff, disjoint_iff, Finset.ext_iff,
    imp_iff_not_or]

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

Goal state before:
pp: case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : (c.boundaries.orderIsoOfFin ⋯) i = ⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j

Tactic:
Subtype.ext_iff,

Goal state after:
case mp
n : ℕ
c : CompositionAsSet n
j : Fin (n + 1)
hj : j ∈ c.boundaries
i : Fin c.boundaries.card
hi : ↑((c.boundaries.orderIsoOfFin ⋯) i) = ↑⟨j, hj⟩
⊢ ∃ i < c.boundaries.card, (take i c.blocks).sum = ↑j
Module: Mathlib.Combinatorics.Enumerative.Composition

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

Tactic:
rw [← compositionAsSet_card n]
  exact Fintype.card_congr (compositionEquiv n)

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
z : α
hzx : ¬z = x
hzf : ¬z = f x
hzfx : f z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
simp [Ne.symm hzx, hzx, Ne.symm hzf, hzfx]

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

Goal state before:
pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] = (Equiv.swap x y) l[n]

Tactic:
rw [← IH, swap_apply_of_ne_of_ne]

Goal state after:
case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ x

case succ.cons.cons.a
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = l[n]
⊢ (y :: l).formPerm (y :: l)[n] ≠ y
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ b ∈ {x, y} ↔ ?m.105 b

Tactic:
mem_insert,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
x y : α
hmem : ¬x = y
hins : {x, y} = f.support
ht : #{y} = 1
a b : α
⊢ b = x ∨ b ∈ {y} ↔ ?m.105 b
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ (x' :: y' :: l').formPerm x' ≠ x'

Tactic:
formPerm_apply_head _ _ _ hd'

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
⊢ y' ≠ x'
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl
α : 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
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inl.ha✝⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm
          (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨x, ⋯⟩, ?intro.refine_2.inl.ha⟩)))

Tactic:
simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]

Goal state after:
case intro.refine_2.inl
α : 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 = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))
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 x z * swap w y) = swap y z

Tactic:
swap_mul_swap_mul_swap hwx hwz,

Goal state after:
α : 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 z w * swap w y) = swap y z
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x y : α
⊢ f.SameCycle x y → (g * f * g⁻¹).SameCycle (g x) (g y)

Tactic:
simp [sameCycle_conj]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ g.IsCycle → (g.extendDomain f).IsCycle

Tactic:
rintro ⟨a, ha, ha'⟩

Goal state after:
α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
a : α
ha : g a ≠ a
ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y
⊢ (g.extendDomain f).IsCycle
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ⟨a₁, 0⟩ ∉ {⟨1, 0⟩}
ha₁ : 0 < a₁
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

pp: case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
· simp only [and_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
      have : 1 < a₁ := lt_of_le_of_ne' (Nat.succ_le_of_lt ha₁) ha₂
      have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by simp
      rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_ge]

Goal state after:
case inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ g.IsCycle → (g.extendDomain f).IsCycle

Tactic:
rintro ⟨a, ha, ha'⟩
  refine ⟨f a, ?_, fun b hb => ?_⟩
  · rw [extendDomain_apply_image]
    exact Subtype.coe_injective.ne (f.injective.ne ha)
  have h : b = f (f.symm ⟨b, of_not_not <| hb ∘ extendDomain_apply_not_subtype _ _⟩) := by
    rw [apply_symm_apply, Subtype.coe_mk]
  rw [h] at hb ⊢
  simp only [extendDomain_apply_image, Subtype.coe_injective.ne_iff, f.injective.ne_iff] at hb
  exact (ha' hb).extendDomain

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

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

Tactic:
convert! H.mul_mem (H.mul_mem h3 ih) (H.inv_mem h3)

Goal state after:
α : 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
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((σ ^ (n + 1)) x) ((σ ^ (n + 1 + 1)) x) = σ * swap ((σ ^ n) x) ((σ ^ (n + 1)) x) * σ⁻¹
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
g p : Perm α
hp : p ∈ Subgroup.centralizer {g}
x : α
⊢ p x ∈ fixedPoints ⇑g ↔ x ∈ fixedPoints ⇑g

Tactic:
by
  simp only [Subgroup.mem_centralizer_singleton_iff] at hp
  simp only [Function.mem_fixedPoints_iff]
  rw [← mul_apply, ← hp, mul_apply, EmbeddingLike.apply_eq_iff_eq]

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

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

Tactic:
Nat.gcd_comm

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

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
a b : α
⊢ (∃ i, ∃ x ∈ s, (x, (f ^ i) x) = (a, b)) → a ∈ s ∧ b ∈ s

Tactic:
rintro ⟨n, a, ha, ⟨⟩⟩
    exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

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

Goal state before:
pp: case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y

Tactic:
obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx

Goal state after:
case pos
α : Type u_2
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : f.SameCycle x y
hx : x ∈ f.support
k : ℕ
hk : k < #(f.cycleOf x).support
hk' : (f ^ k) x = y
⊢ ∃ i, 0 < i ∧ i ≤ #(f.cycleOf x).support + 1 ∧ (f ^ i) x = y