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 : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ g = v ≫ q ≫ h

Tactic:
rw [equalizer.condition g h]

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
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
Iso.comp_inv_eq,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π = s.π ≫ i.hom
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.IsLeftAdjoint
X Y : C
⊢ F.map 0 = 0

Tactic:
by
    let adj := Adjunction.ofIsLeftAdjoint F
    calc
      dsimp% F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
    · rw [Adjunction.left_triangle_components]
      exact (Category.comp_id _).symm
    · simp only [← Category.assoc, ← F.map_comp, zero_comp]
    · simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T U : C
g : (j : J) → T ⟶ f j
h : (j : J) → f j ⟶ U
⊢ lift g ≫ desc h = ∑ j, g j ≫ h j

Tactic:
classical
  simp [biproduct.lift_eq, biproduct.desc_eq, comp_sum, sum_comp, biproduct.ι_π_assoc, comp_dite,
    dite_comp]

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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
⊢ (let c' := CokernelCofork.ofπ (Cofork.π c) ⋯;
      let i' := isCokernelEpiComp i (retraction f) ⋯;
      let i'' := isColimitCoforkOfCokernelCofork i';
      (splitEpiOfIdempotentOfIsColimitCofork C ⋯ i'').section_) ≫
      Cofork.π c =
    𝟙 c.pt

Tactic:
apply SplitEpi.id

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso (biprod.map g f)

Tactic:
← biprod.braiding_map_braiding

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ IsIso ((biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom)
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.left
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ ∀ x ∈ antidiagonal n, (map (fun x_1 ↦ Fin.cons x.1 x_1) (antidiagonalTuple k x.2)).Nodup

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

Tactic:
· intro i _
    exact (ih i.snd).map (Fin.cons_right_injective (α := fun _ => ℕ) i.fst)

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

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.blocks = [] ↔ n = 0

Tactic:
by
  constructor
  · intro h
    simpa using congr(List.sum $h)
  · rintro rfl
    rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]
    exact c.length_le

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ f ∈ map h.toEmbedding (map (mapRange.addEquiv e.symm).toEmbedding (s.finsuppAntidiag (e n)))

Tactic:
convert! hf

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ map h.toEmbedding (map (mapRange.addEquiv e.symm).toEmbedding (s.finsuppAntidiag (e n))) = s.finsuppAntidiag (e n)
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:
rw [Subtype.ext_iff, Fintype.choose_spec (fun y : { a : α // p a } => (y : α) = x) _]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)), (s.noncommProd k ⋯).support = s.biUnion fun i ↦ (k i).support
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ c.toCompositionAsSet.blocks = c.blocks

Tactic:
change d.blocks = c.blocks

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
⊢ d.blocks = c.blocks
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
by
  simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
j : ℕ
hj : j < n + 1
⊢ ⟨j, hj⟩ ∈ c.toComposition.boundaries ↔ ⟨j, hj⟩ ∈ c.boundaries

Tactic:
simp [c.mem_boundaries_iff_exists_blocks_sum_take_eq, Composition.boundaries,
    c.card_boundaries_eq_succ_length, Composition.boundary, Composition.sizeUpTo, Fin.exists_iff]

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

Goal state before:
pp: case neg.refine_2
α : 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
_hfl : f ∉ permsOfList l
⊢ Equiv.swap a (f a) * Equiv.swap a (f a) * f = f

Tactic:
mul_def (Equiv.swap a (f a)) (Equiv.swap a (f a)),

Goal state after:
case neg.refine_2
α : 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
_hfl : f ∉ permsOfList l
⊢ Equiv.trans (Equiv.swap a (f a)) (Equiv.swap a (f a)) * f = f
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ g x ≠ x

Tactic:
rw [eq_inv_mul_iff_mul_eq.2 hg₂, mul_apply, swap_inv, swap_apply_def]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
f : Equiv.Perm α
h✝ : f ∈ permsOfList (a :: l)
x : α
h : f ∈ flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l
hx : f x ≠ x
y : α
hy : y ∈ l
hy' : f ∈ List.map (fun f ↦ Equiv.swap a y * f) (permsOfList l)
g : Equiv.Perm α
hg₁ : g ∈ permsOfList l
hg₂ : Equiv.swap a y * g = f
hxa : ¬x = a
hxy : ¬x = y
⊢ (if f x = a then y else if f x = y then a else f x) ≠ x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b : α
l : List α
⊢ (a :: b :: l).reverse.formPerm = (a :: b :: l).formPerm⁻¹

Tactic:
by
    simp [formPerm_append_pair, Equiv.swap_comm, ← formPerm_reverse (b::l)]

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

Goal state before:
pp: case intro.refine_2.inl.refine_1
α : 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
⊢ ¬f (σ (f⁻¹ (f x))) = f x

Tactic:
coe_inv,

Goal state after:
case intro.refine_2.inl.refine_1
α : 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
⊢ ¬f (σ ((Equiv.symm f) (f x))) = f x
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)) x = y

Tactic:
rw [← ha, ← mul_apply, ← zpow_add, sub_add_cancel, hb]

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

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : 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
h : f (σ ((Equiv.symm f) (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))

Tactic:
coe_inv,

Goal state after:
case intro.refine_2.inr.refine_2
α : 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
h : f (σ ((Equiv.symm f) (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ ((Equiv.symm f) (g (τ (g⁻¹ (g x))))))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : 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
h : f (σ ((Equiv.symm f) (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ ((Equiv.symm f) (g (τ (g⁻¹ (g x))))))

Tactic:
coe_inv,

Goal state after:
case intro.refine_2.inr.refine_2
α : 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
h : f (σ ((Equiv.symm f) (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ ((Equiv.symm f) (g (τ ((Equiv.symm g) (g x))))))
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
⊢ (l.formPerm ^ l.length) x = 1 x

Tactic:
by_cases hx : x ∈ l

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ (l.formPerm ^ l.length) x = 1 x

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∉ l
⊢ (l.formPerm ^ l.length) x = 1 x
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_1
α : 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
⊢ ¬g (τ (g⁻¹ (g (τ x)))) = g (τ x)

Tactic:
coe_inv,

Goal state after:
case intro.refine_2.inr.refine_1
α : 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
⊢ ¬g (τ ((Equiv.symm g) (g (τ x)))) = g (τ x)
Module: Mathlib.GroupTheory.Perm.Finite

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

Tactic:
EmbeddingLike.apply_eq_iff_eq

Goal state after:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ g x = x ↔ g x = x
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝) = a :: iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝

Tactic:
cons_append

Goal state after:
case succ
α : Type u_1
f : α → α
n✝ n : ℕ
ih : ∀ (a : α), iterate f a (n + n✝) = iterate f a n ++ iterate f (f^[n] a) n✝
a : α
⊢ a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝) = a :: (iterate f (f a) n ++ iterate f (f^[n] (f a)) n✝)
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * b ^ n * b ^ m = a * b ^ (n + m)

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
n m : ℤ
⊢ a * (b ^ n * b ^ m) = a * b ^ (n + m)
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * b * b ^ m = a * b ^ (m + 1)

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
m : ℤ
⊢ a * (b * b ^ m) = a * b ^ (m + 1)
Module: Mathlib.Tactic.Group

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * b ^ n * b = a * b ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
G : Type u_1
inst✝ : Group G
a b : G
n : ℤ
⊢ a * (b ^ n * b) = a * b ^ (n + 1)
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : β ≃ α
p : Perm α
g : α ≃ β
⊢ sign (f.trans (Equiv.trans p g)) = sign p * sign (f.trans g)

Tactic:
rw [← sign_permCongr g, ← sign_mul]; congr; ext; simp

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

Goal state before:
pp: case left
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ sign (σa.sumCongr 1) = sign σa

Tactic:
induction σa using swap_induction_on with

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
⊢ sign (e.viaFintypeEmbedding f) = sign e

Tactic:
simp [viaFintypeEmbedding]

Goal state after:
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 ι := Classical.decEq ι
f : (i : ι) → H i
i : ι
⊢ i ∈ Finset.univ → (ϕ i) (f i) ∈ ⨆ i, (ϕ i).range

Tactic:
_hi

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 ι
f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ (ϕ i) (f i) ∈ ⨆ i, (ϕ i).range
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val

Tactic:
rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
      (one_lt_of_mem_cycleType hn).ne'

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

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
⊢ c.subtypePerm ⋯ ^ n = g.subtypePerm hg → c ^ n = ofSubtype (g.subtypePerm hg)

Tactic:
· intro h; ext x
    rw [← h]
    by_cases hx : x ∈ s
    · rw [ofSubtype_apply_of_mem (subtypePerm c _ ^ n) hx,
        subtypePerm_zpow, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]
      exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

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

Goal state before:
pp: case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ (k i).Disjoint (k j)

Tactic:
apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ i ∈ ↑(insert i s)

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
j : ι
hj : j ∈ s
⊢ j ∈ ↑(insert i s)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
h : i ≤ j
⊢ ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

Tactic:
by
  rcases n with - | n
  · exact absurd le_rfl j.pos.not_ge
  rw [cycleRange_of_le h]
  split_ifs with h'
  · rfl
  exact
    val_add_one_of_lt
      (calc
        (i : ℕ) < j := Fin.lt_def.mp (lt_of_le_of_ne h h')
        _ ≤ n := Nat.lt_succ_iff.mp j.2)

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

Goal state before:
pp: case mp.refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ l.prod = σ

Tactic:
rw [← hp', hperm.symm.prod_eq']
      exact hd'.imp Disjoint.commute

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

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
⊢ c (c x) = c x ↔ c x = x

Tactic:
EmbeddingLike.apply_eq_iff_eq

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
⊢ c x = x ↔ c x = x