mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
⊢ ∀ {X Y : StructuredArrow S T × StructuredArrow S' T'} (f : X ⟶ Y),
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y)).hom =
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X)).hom ≫
        (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f

Tactic:
intros

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : D
S' : D'
T : C ⥤ D
T' : C' ⥤ D'
X✝ Y✝ : StructuredArrow S T × StructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (StructuredArrow S T × StructuredArrow S' T')).map f✝
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
⊢ ∀ {X Y : CostructuredArrow S T × CostructuredArrow S' T'} (f : X ⟶ Y),
    (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f ≫
        (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y)).hom =
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X)).hom ≫
        (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f

Tactic:
intros

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
S : C ⥤ D
S' : C' ⥤ D'
T : D
T' : D'
X✝ Y✝ : CostructuredArrow S T × CostructuredArrow S' T'
f✝ : X✝ ⟶ Y✝
⊢ (prodInverse S S' T T' ⋙ prodFunctor S S' T T').map f✝ ≫
      (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj Y✝)).hom =
    (Iso.refl ((prodInverse S S' T T' ⋙ prodFunctor S S' T T').obj X✝)).hom ≫
      (𝟭 (CostructuredArrow S T × CostructuredArrow S' T')).map f✝
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

Tactic:
have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
    apply I.zero_comp X (J.zero Y Y).zero

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ factorThruImage f ≫ 0 = 0

Tactic:
HasZeroMorphisms.comp_zero

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
w : image.ι f = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = P.hom ≫ P.inv

Tactic:
← Category.id_comp P.inv

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 0 ≫ 0 = P.hom ≫ 𝟙 0 ≫ P.inv
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 : C
P✝ : IsIsomorphic X 0
P : X ≅ 0
⊢ 𝟙 X = 0

Tactic:
apply (idZeroEquivIsoZero X).invFun P

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

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

Tactic:
by ext; apply comp_add

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (x y : X ⟶ Y), leftComp S Z (x + y) = leftComp S Z x + leftComp S Z y

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
x✝ y✝ : X ⟶ Y
⊢ leftComp S Z (x✝ + y✝) = leftComp S Z x✝ + leftComp S Z y✝
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (m : S) (x : X ⟶ Y), leftComp S Z (m • x) = (RingHom.id S) m • leftComp S Z x

Tactic:
intros

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
m✝ : S
x✝ : X ⟶ Y
⊢ leftComp S Z (m✝ • x✝) = (RingHom.id S) m✝ • leftComp S Z x✝
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
Z : ObjectProperty C
x✝⁵ x✝⁴ x✝³ : Z.FullSubcategory
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ + x✝) = x✝² ≫ x✝¹ + x✝² ≫ x✝

Tactic:
by ext; apply comp_add

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
s : KernelFork f
⊢ Fork.ι s ≫ 0 = 0

Tactic:
HasZeroMorphisms.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
s : KernelFork f
⊢ 0 = 0
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
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ 0 = ι ≫ 0

Tactic:
HasZeroMorphisms.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
ι : Z ⟶ X
w : ι ≫ f = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ factorThruImage f ≫ 0 = 0

Tactic:
HasZeroMorphisms.comp_zero

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
⊢ 0 = 0
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
inst✝² : HasZeroObject C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts C
F : C ⥤ D
h : leftExactFunctor C D F
⊢ additiveFunctor C D F

Tactic:
simp only [leftExactFunctor_iff] at h
    exact Functor.additive_of_preservesBinaryBiproducts F

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
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
refine BinaryFan.IsLimit.hom_ext ht ?_ ?_ <;> simp

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
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π
⊢ m = (fromSubtype f fun j ↦ j ≠ i) ≫ s.π

Tactic:
rw [← hm, CokernelCofork.π_ofπ, ← Category.assoc, biproduct.fromSubtype_toSubtype]

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
m : (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯).pt ⟶ s.pt
hm : Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ m = s.π
⊢ m = 𝟙 (⨁ Subtype.restrict (fun j ↦ j ≠ i) f) ≫ m
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)
t : biprod.inl ≫ (biprod.map f g ≫ inv (biprod.map f g)) ≫ biprod.fst = biprod.inl ≫ 𝟙 (W ⊞ X) ≫ biprod.fst
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W

Tactic:
simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t

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)
t : f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = biprod.inl ≫ biprod.fst
⊢ f ≫ biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst = 𝟙 W
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
⊢ countRestricted n 2 = distincts n

Tactic:
by
  congrm Finset.univ.filter fun x ↦ ?_
  rw [Multiset.nodup_iff_count_le_one]
  grind [Multiset.count_eq_zero]

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

Goal state before:
pp: α : 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)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
ι : 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)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
have A :
    d.boundaries.orderEmbOfFin rfl ⟨i, i_lt⟩ =
      c.boundaries.orderEmbOfFin c.card_boundaries_eq_succ_length ⟨i, i_lt''⟩ :=
    rfl

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
⊢ (take i d.blocks).sum = (take i c.blocks).sum
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
rwa [formPerm_apply_of_notMem h]

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

Goal state before:
pp: α : Type u
σ τ : Perm α
hστ : σ.Disjoint τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1

Tactic:
by
    rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]

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

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) ⟨a, b⟩.fst ≤ (f * g) ⟨a, b⟩.snd then -1 else 1) =
    (if f (g.signBijAux ⟨a, b⟩).fst ≤ f (g.signBijAux ⟨a, b⟩).snd then -1 else 1) *
      if g⁻¹ (g.signBijAux ⟨a, b⟩).fst ≤ g⁻¹ (g.signBijAux ⟨a, b⟩).snd then -1 else 1

Tactic:
dsimp only [signBijAux]

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if (f * g) a ≤ (f * g) b then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
⊢ (swap 0 1).signAux = ∏ x ∈ {⟨1, 0⟩}, if (swap 0 1) x.fst ≤ (swap 0 1) x.snd then -1 else 1

Tactic:
refine Eq.symm (prod_subset (fun ⟨x₁, x₂⟩ => by
      simp +contextual [mem_finPairsLT]) fun a ha₁ ha₂ => ?_)

Goal state after:
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : a ∉ {⟨1, 0⟩}
⊢ (if (swap 0 1) a.fst ≤ (swap 0 1) a.snd then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x y : α
l : List α
hl : (x :: y :: l).Nodup
⊢ (x :: y :: l).formPerm = l'.formPerm ↔ x :: y :: l ~r l' ∨ (x :: y :: l).length ≤ 1 ∧ l'.length ≤ 1

Tactic:
· rcases l' with (_ | ⟨x', _ | ⟨y', l'⟩⟩)
    · simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
    · simp [formPerm_eq_one_iff _ hl, -formPerm_cons_cons]
    · simp [-formPerm_cons_cons, formPerm_ext_iff hl hl']

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(swap x (f x) * f).support + 1 = #f.support

Tactic:
rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
            card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]

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

Goal state before:
pp: case negSucc
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
a✝ : ℕ
h1 : (f ^ (a✝ + 1))⁻¹.IsCycle
h2 : f.support ⊆ (f ^ (a✝ + 1)).support
⊢ f.IsCycle

Tactic:
exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

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

Goal state before:
pp: case mp
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
⊢ (f ^ n).support = f.support → ¬f ^ n = 1

Tactic:
intro h H
    refine hf.ne_one ?_
    rw [← support_eq_empty_iff, ← h, H, support_one]

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

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ (f ^ n).IsCycle → n.Coprime (orderOf f)

pp: case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ n.Coprime (orderOf f) → (f ^ n).IsCycle

Tactic:
· intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]

Goal state after:
case intro.mpr
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
⊢ n.Coprime (orderOf f) → (f ^ n).IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsCycle
hτ : τ.IsCycle
h : #σ.support = #τ.support
⊢ orderOf σ = orderOf τ

Tactic:
by rw [hσ.orderOf, h, hτ.orderOf]

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

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), (prodComm β α) ((prodCongrLeft σ) x) = (prodCongrRight σ) ((prodComm β α) x)

Tactic:
rintro ⟨b, α⟩

Goal state after:
α✝ : Type u
inst✝³ : DecidableEq α✝
β : Type v
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ (prodComm β α✝) ((prodCongrLeft σ) (b, α)) = (prodCongrRight σ) ((prodComm β α✝) (b, α))
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
h✝ : (↑s).Nontrivial
m : ℕ
hm : m < #s
n : ℕ
hn : n < #s
hmn : m ≠ n
a : α
ha : a ∈ s
h : n ≡ m [MOD #s]
⊢ False

Tactic:
exact hmn.symm (h.eq_of_lt_of_lt hn hm)

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
n : ℕ
x : α
⊢ (f ^ (n % orderOf (f.cycleOf x))) x = (f ^ n) x

Tactic:
by
  rw [← cycleOf_pow_apply_self f, ← cycleOf_pow_apply_self f, pow_mod_orderOf]

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

Goal state before:
pp: α : 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)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : 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)

Tactic:
simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
⊢ #σ.support ∈ τ.cycleType

Tactic:
simp [← h, hc.cycleType]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p n : ℕ
hp : Fact (Nat.Prime p)
σ : Perm α
hσ : σ ^ p ^ n = 1
m : ℕ
hm : orderOf σ = p ^ m
l : ℕ
hk : p ^ l ∈ σ.cycleType
h : l = 0
⊢ 1 = p ^ l

Tactic:
by rw [h, pow_zero]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f (1 + (p - 1)) s = s

Tactic:
add_tsub_cancel_of_le hp.out.one_lt.le,

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f p s = s
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case refine_1
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.univ.sigma Finset.Iio
hD : D = Finset.univ.sigma Finset.Iio
x1 x2 : Fin n
⊢ (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) → x2 < x1

Tactic:
rintro ⟨i, j, hij, rfl, rfl⟩
      exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Fintype.card α - #σ.support) = Fintype.card α

Tactic:
add_tsub_cancel_of_le σ.support.card_le_univ

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Fintype.card α = Fintype.card α
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
⊢ ∀ [inst : DecidableEq ι] (m : ι → M₂) (i_1 : ι) (x y : M₂),
    f (update m i_1 (x + y) i) = f (update m i_1 x i) + f (update m i_1 y i)

Tactic:
intros

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝¹⁰ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : AddCommMonoid M₃
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : (i : Fin n.succ) → Module R (M i)
inst✝⁵ : (i : ι) → Module R (M₁ i)
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
inst✝² : Module R M'
f✝ f' : MultilinearMap R M₁ M₂
inst✝¹ : Subsingleton ι
i : ι
f : M₂ →ₗ[R] M₃
inst✝ : DecidableEq ι
m✝ : ι → M₂
i✝ : ι
x✝ y✝ : M₂
⊢ f (update m✝ i✝ (x✝ + y✝) i) = f (update m✝ i✝ x✝ i) + f (update m✝ i✝ y✝ i)