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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X Y : C
s : BinaryCofan X Y
⊢ inr ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)) ≫
      (Iso.refl ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ F)).inv).obj (F.mapCocone s)).pt).hom =
    (map F s).inr

Tactic:
by simp [inr]

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')
⊢ F.map (prod.map f g) ≫ prodComparison F A' B' = prodComparison F A B ≫ prod.map (F.map f) (F.map g)

Tactic:
prodComparison_natural

Goal state after:
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')
⊢ prodComparison F A B ≫ prod.map (F.map f) (F.map g) = prodComparison F A B ≫ prod.map (F.map f) (F.map g)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasBinaryCoproducts C
A : C
X✝ Y✝ : Over A
k✝ : X✝ ⟶ Y✝
f g : Over A
k : f ⟶ g
⊢ X✝.coprodObj.map k ≫ homMk (coprod.map (Hom.left k✝) (𝟙 g.left)) ⋯ =
    homMk (coprod.map (Hom.left k✝) (𝟙 f.left)) ⋯ ≫ Y✝.coprodObj.map k

Tactic:
by
        ext
        simp

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

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
f g : Over X
φ : f ⟶ g
⊢ Hom.left φ ≫ g.hom = f.hom

Tactic:
simpa using (CommaMorphism.w φ)

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
⊢ IsLimit (mk s.fst s.snd ⋯)

Tactic:
by
  apply PullbackCone.isLimitAux'
  intro s
  rcases PullbackCone.IsLimit.lift' H s.fst s.snd
      ((cancel_mono i).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩
  refine ⟨l, h₁, h₂, ?_⟩
  intro m hm₁ hm₂
  exact (PullbackCone.IsLimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

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

Goal state before:
pp: j : WalkingParallelPairᵒᵖ
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j = (𝟭 WalkingParallelPairᵒᵖ).obj j

Tactic:
induction j with | _ X
            cases X <;> rfl

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
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ preComp f (g ≫ h) ≫ preComp g h = eqToHom ⋯ ≫ preComp (f ≫ g) h

Tactic:
apply (cancel_mono (image.ι h)).1

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (preComp f (g ≫ h) ≫ preComp g h) ≫ ι h = (eqToHom ⋯ ≫ preComp (f ≫ g) h) ≫ ι h
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 : Cofork f g
d : (s : Cofork f g) → t.pt ⟶ s.pt
hd : ∀ (s : Cofork f g), (fun d ↦ t.π ≫ d = s.π) (d s)
hd' : ∀ (s : Cofork f g) (y : t.pt ⟶ s.pt), (fun d ↦ t.π ≫ d = s.π) y → y = d s
⊢ IsColimit t

Tactic:
exact Cofork.IsColimit.mk _ d hd fun s m hm => hd' _ _ hm

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✝
X Y : C
f g : X ⟶ Y
X' Y' : C
f' g' : X' ⟶ Y'
e₀ : X ≅ X'
e₁ : Y ≅ Y'
comm₁ : e₀.hom ≫ f' = f ≫ e₁.hom
comm₂ : e₀.hom ≫ g' = g ≫ e₁.hom
⊢ (parallelPair f g).map left ≫ e₁.hom = e₀.hom ≫ (parallelPair f' g').map left

Tactic:
simp [comm₁]

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

Goal state before:
pp: case h₀
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ (precompFork h✝ s c).ι = s'.ι
⊢ (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h✝) ⋯) ≫ s.ι

Tactic:
simp only [Fork.ι_ofι, precompFork] at h

Goal state after:
case h₀
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f✝ g✝ f g : X ⟶ Y
Z : C
h✝ : Z ⟶ X
s : Fork f g
hs : IsLimit s
c : PullbackCone s.ι h✝
hc : IsLimit c
s' : Fork (h✝ ≫ f) (h✝ ≫ g)
m : s'.pt ⟶ (precompFork h✝ s c).pt
h : m ≫ c.snd = s'.ι
⊢ (m ≫ c.fst) ≫ s.ι = hs.lift (Fork.ofι (s'.ι ≫ h✝) ⋯) ≫ s.ι
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f✝ f' : P ⟶ Q
g g' : Q ⟶ R
X : C
f : End X
⊢ 0 * f = 0

Tactic:
by dsimp [mul]; exact HasZeroMorphisms.comp_zero f _

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
c : KernelFork f
hc : IsLimit c
h : IsZero c.pt
P✝ : C
g : P✝ ⟶ X
hg : g ≫ f = 0
⊢ g = 0

Tactic:
by
  obtain ⟨a, ha⟩ := KernelFork.IsLimit.lift' hc _ hg
  rw [← ha, h.eq_of_tgt a 0, Limits.zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

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
J✝ : Type w
inst✝² : SmallCategory J✝
K : J✝ ⥤ C
F : C ⥤ D
J : Type u
inst✝¹ : Finite J
inst✝ : PreservesFiniteProducts F
n : ℕ
e : J ≃ Fin n
this : PreservesLimitsOfShape (Discrete (Fin n)) F
⊢ PreservesLimitsOfShape (Discrete J) F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.equivalence e.symm) F

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsColimitsOfShape J F

Tactic:
by
    have := reflectsSmallestColimits_of_reflectsColimits F
    exact reflectsColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

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
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : c.IsBilimit
⊢ IsColimit (Cocone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCocone)

Tactic:
exact IsColimit.whiskerEquivalence hc.isColimit (Discrete.equivalence g)

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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i

Goal state after:
case h₁
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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ BinaryCofan.inl c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π

case h₂
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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inl 0
⊢ BinaryCofan.inr c.toCocone ≫ Cofork.π c.inlCokernelCofork ≫ c.inr ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
j : K
h : ¬(p j)ᶜ
⊢ 0 ≫ biproduct.ι f j ≫ g' = biproduct.ι f j ≫ g'

Tactic:
· replace w := biproduct.ι _ (⟨j, not_not.mp h⟩ : Subtype p) ≫= w
          simpa using w.symm

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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = s.π

Tactic:
apply BinaryCofan.IsColimit.hom_ext i

Goal state after:
case h₁
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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ BinaryCofan.inl c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inl c.toCocone ≫ s.π

case h₂
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 X Y : C
c : BinaryBicone X Y
i : IsColimit c.toCocone
s : Cofork c.inr 0
⊢ BinaryCofan.inr c.toCocone ≫ Cofork.π c.inrCokernelCofork ≫ c.inl ≫ s.π = BinaryCofan.inr c.toCocone ≫ s.π
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ ((∀ (j : Fin n.succ), j < 0 → cons x₀ x j = cons y₀ y j) ∧ s x₀ y₀ ∨
      ∃ i, (∀ (j : Fin n.succ), j < i.succ → cons x₀ x j = cons y₀ y j) ∧ s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)

Tactic:
Fin.forall_iff_succ

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
⊢ (((0 < 0 → cons x₀ x 0 = cons y₀ y 0) ∧ ∀ (i : Fin n), i.succ < 0 → cons x₀ x i.succ = cons y₀ y i.succ) ∧ s x₀ y₀ ∨
      ∃ i,
        ((0 < i.succ → cons x₀ x 0 = cons y₀ y 0) ∧
            ∀ (i_1 : Fin n), i_1.succ < i.succ → cons x₀ x i_1.succ = cons y₀ y i_1.succ) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ i, (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4.p.p
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
h : StrictMono f
hlt : ∀ (i : Fin n), i.castSucc < q → f i < x
hgt : ∀ (i : Fin n), q ≤ i.castSucc → x < f i
j✝¹ j✝ : Fin n
hab : q.succAbove j✝¹ < q.succAbove j✝
⊢ q.insertNth x f (q.succAbove j✝¹) < q.insertNth x f (q.succAbove j✝)

Tactic:
simpa using h <| (strictMono_succAbove _).lt_iff_lt.mp hab

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: k n : ℕ
⊢ (antidiagonalTuple k n).Nodup

Tactic:
induction k generalizing n with
  | zero => cases n <;> simp
  | succ k ih => ?_

Goal state after:
case succ
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
⊢ (antidiagonalTuple (k + 1) n).Nodup
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
piAntidiag

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈
      Trunc.lift
        (fun e ↦ map { toFun := fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : c a ≠ a
ha' : a ∉ s
⊢ False

Tactic:
← h a,

Goal state after:
case mp.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
a : α
ha : (ofSubtype (g.subtypePerm hg)) a ≠ a
ha' : a ∉ s
⊢ False
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a

Tactic:
← h a,

Goal state after:
case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ (ofSubtype (g.subtypePerm hg)) a = g a
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
⊢ i ∈ c.boundaries → (∃ y, y.succ = i) → i ≠ Fin.last n → ∃ j, ⟨↑j + 1, ⋯⟩ ∈ c.boundaries ∧ ↑i = ↑j + 1

Tactic:
rintro i_mem ⟨j, rfl⟩ i_ne_last

Goal state after:
case mpr
n✝ n : ℕ
c : CompositionAsSet n
j : Fin n
i_mem : j.succ ∈ c.boundaries
i_ne_last : j.succ ≠ Fin.last n
⊢ ∃ j_1, ⟨↑j_1 + 1, ⋯⟩ ∈ c.boundaries ∧ ↑j.succ = ↑j_1 + 1
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Nodup

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

pp: case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)

Tactic:
· exact hln'

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ x ∈ l, (List.map (fun f ↦ Equiv.swap a x * f) (permsOfList l)).Nodup

case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length),
    i < j → (List.Disjoint on fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i] l[j]

case refine_4
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
⊢ (permsOfList l).Disjoint (flatMap (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l)
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
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
have h : #(swap x (f x) * f).support + 1 = #f.support := by
          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:
α : 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
h : #(swap x (f x) * f).support + 1 = #f.support
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
    a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
left✝ : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)

Tactic:
rw [prod_eq, prodCongrRight_apply]

Goal state after:
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ (↑x).gcd ↑y = d

Tactic:
apply int_gcd_helper' a (-b)
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hu))
    (Int.natCast_dvd_natCast.mpr (Nat.dvd_of_mod_eq_zero hv))

Goal state after:
d x y a b : ℕ
hu : x % d = 0
hv : y % d = 0
h : x * a = y * b + d
⊢ ↑x * ↑a + ↑y * -↑b = ↑d
Module: Mathlib.Tactic.NormNum.GCD

Goal state before:
pp: n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ n / 1 = ↑n

Tactic:
Int.ediv_one,

Goal state after:
n : ℤ
d : ℕ
hi : Invertible ↑d
h : n.natAbs.gcd d = 1
this : 0 < d
⊢ n = ↑n
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : #σ.support < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
obtain ⟨n, hn⟩ := cycleType_prime_order h1
  rw [← σ.sum_cycleType, hn, Multiset.sum_replicate, nsmul_eq_mul, Nat.cast_id,
    mul_lt_mul_iff_left₀ (orderOf_pos σ), Nat.succ_lt_succ_iff, Nat.lt_succ_iff, Nat.le_zero] at h2
  rw [← card_cycleType_eq_one, hn, card_replicate, h2]

Goal state after:
Module: Mathlib.Data.FunLike.Module

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst✝⁶ : SMul M F
inst✝⁵ : SMul Mᵐᵒᵖ F
inst✝⁴ : SMul M β
inst✝³ : SMul Mᵐᵒᵖ β
inst✝² : IsCentralScalar M β
inst✝¹ : IsSMulApply M F α β
inst✝ : IsSMulApply Mᵐᵒᵖ F α β
a : M
b : F
⊢ MulOpposite.op a • b = a • b

Tactic:
by apply DFunLike.ext; simp [op_smul_eq_smul]

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

Goal state before:
pp: n : ℕ
i j k : Fin n
h : k < i
⊢ (i.cycleIcc j) k = k

Tactic:
by
  by_cases hij : i ≤ j
  · simpa [hij] using Perm.extendDomain_apply_not_subtype _ _ (by
      simp [range_natAdd_castLEEmb]; lia)
  · simp [hij]

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
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ (σ ^ p ^ 1) v = 1 v

Tactic:
pow_one,

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
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : ∀ (k : ℕ) (v : ↑(vectorsProdEqOne G p)), (σ ^ k) v = f k v
v : ↑(vectorsProdEqOne G p)
⊢ (σ ^ p) v = 1 v
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
p f : Perm α
h : p ∈ f.cycleFactorsFinset
⊢ p.support ⊆ f.support

Tactic:
by
  rw [mem_cycleFactorsFinset_iff] at h
  intro x hx
  rwa [mem_support, ← h.right x hx, ← mem_support]

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

Goal state before:
pp: 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
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
⊢ ∏ x ∈ D, f (σ x.snd) (σ x.fst) = ∏ x ∈ D, ↑↑(if σ⁻¹ x.snd < σ⁻¹ x.fst then 1 else -1) * f x.snd x.fst

Tactic:
← hφD

Goal state after:
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
hφD : Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D = D
⊢ ∏ x ∈ D, f (σ x.snd) (σ x.fst) =
    ∏ x ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D,
      ↑↑(if σ⁻¹ x.snd < σ⁻¹ x.fst then 1 else -1) * f x.snd x.fst
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ f.cycleOf a = c.cycleOf a

Tactic:
rw [← Equiv.Perm.cycleOf_mul_of_apply_right_eq_self hfc2]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ f.cycleOf a = (c * (f * c⁻¹)).cycleOf a

case hx
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ (f * c⁻¹) a = a