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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ inv (pullback.fst f g) ≫ pullback.snd f g = f ≫ inv g

Tactic:
rw [IsIso.inv_comp_eq, pullback.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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 ⟶ Z
g : Y ⟶ Z
h : W ⟶ Z
inst✝ : Mono h
x : X ⟶ W
y : Y ⟶ W
hxh : x ≫ h = f
hyh : y ≫ h = g
s : PullbackCone f g
hs : IsLimit s
⊢ (s.fst ≫ x) ≫ h = (s.snd ≫ y) ≫ h

Tactic:
simp only [Category.assoc, hxh, hyh, s.condition]

Goal state after:
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
F : C ⥤ D
d : D
⊢ ∀ {X Y : (StructuredArrow d F)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫ (StructuredArrow.isoMk (Iso.refl (unop Y).right) ⋯).op.hom =
      (StructuredArrow.isoMk (Iso.refl (unop X).right) ⋯).op.hom ≫
        (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : StructuredArrow d F
f : op X ⟶ op Y
⊢ (𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫ (StructuredArrow.isoMk (Iso.refl (unop (op Y)).right) ⋯).op.hom =
    (StructuredArrow.isoMk (Iso.refl (unop (op X)).right) ⋯).op.hom ≫
      (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
f : F ⟶ G
X : C
H : MonoFactorisation f
x : F.obj X
⊢ (ConcreteCategory.hom (H.m.app X)) ((ConcreteCategory.hom (H.e.app X)) x) = (ConcreteCategory.hom (f.app X)) x

Tactic:
by
  simp [← comp_apply, ← NatTrans.comp_app]

Goal state after:
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
F : C ⥤ D
d : D
⊢ ∀ {X Y : (CostructuredArrow F d)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop Y).left) ⋯).op.hom =
      (CostructuredArrow.isoMk (Iso.refl (unop X).left) ⋯).op.hom ≫
        (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ f

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X Y : CostructuredArrow F d
f : op X ⟶ op Y
⊢ (𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫ (CostructuredArrow.isoMk (Iso.refl (unop (op Y)).left) ⋯).op.hom =
    (CostructuredArrow.isoMk (Iso.refl (unop (op X)).left) ⋯).op.hom ≫
      (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
hX : IsZero (F.obj X)
⊢ IsZero X

Tactic:
by
  have h : F.FullyFaithful := .ofFullyFaithful _
  have (Y : C) := (hX.unique_to (F.obj Y)).some
  have (Y : C) := (hX.unique_from (F.obj Y)).some
  exact ⟨fun Y ↦ ⟨h.homEquiv.unique⟩, fun Y ↦ ⟨h.homEquiv.unique⟩⟩

Goal state after:
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
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ X✝.left.hom ≫ R.map (f.left.right ≫ Y✝.hom) = X✝.left.hom ≫ R.map X✝.hom

Tactic:
dsimp% CostructuredArrow.w f

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ X✝.left.hom ≫ R.map X✝.hom = X✝.left.hom ≫ R.map X✝.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one

Tactic:
exact ι ≫ f

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

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

Tactic:
funext X Y

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
w : ∀ (X Y : C), Zero.zero = Zero.zero
X Y : C
⊢ zero X Y = zero X Y
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G

Tactic:
by
  apply preservesColimit_of_preserves_colimit_cocone initialIsInitial
  apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
  exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mpr.inl
C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
X : C
hY : P.isoClosure X
⊢ (P ⊔ Q).isoClosure X

Tactic:
exact monotone_isoClosure le_sup_left _ hY

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

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
F : C ⥤ₗ D
G : D ⥤ₗ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

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
F : D ⥤ₗ E
G : C ⥤ₗ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

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
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteLimits _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

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
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp; exact comp_preservesFiniteLimits _ _

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun j ↦ G.obj (f j)
i : IsIso (sigmaComparison G f)
⊢ IsColimit (Cofan.mk (G.obj (∐ f)) fun j ↦ G.map (Sigma.ι f j))

Tactic:
exact @IsColimit.ofPointIso _ _ _ _ _ _ _
    (colimit.isColimit (Discrete.functor fun j : J => G.obj (f j))) i

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

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd

Tactic:
· simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_right]
    simp

Goal state after:
case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd
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.inl = BinaryFan.IsLimit.lift ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryFan.mk (𝟙 X) 0); rintro ⟨⟨⟩⟩ <;> simp

Goal state after:
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' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
j : K
h : ¬(p j)ᶜ
⊢ g' ≫ biproduct.π f j ≫ 0 = g' ≫ biproduct.π f j

Tactic:
replace w := w =≫ biproduct.π _ ⟨j, not_not.mp h⟩
          simpa using w.symm

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

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
⊢ homGroup = homGroup

Tactic:
funext X Y

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
⊢ homGroup X Y = homGroup X Y
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)
⊢ IsIso
    (ofComponents (biprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inl ≫ f.hom ≫ biprod.snd) (biprod.inr ≫ f.hom ≫ biprod.fst)
      (biprod.inr ≫ f.hom ≫ biprod.snd))

Tactic:
simp only [Biprod.ofComponents_eq]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : X₁ ⊞ X₂ ≅ Y₁ ⊞ Y₂
inst✝ : IsIso (biprod.inl ≫ f.hom ≫ biprod.fst)
⊢ IsIso f.hom
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.blocks.sum = n

Tactic:
c.blocks_sum

Goal state after:
n : ℕ
c : Composition n
⊢ n = n
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case left
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ ((mapRange ⇑e ⋯ g).sum fun x x_1 ↦ x_1) = e n

pp: case right
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (mapRange ⇑e ⋯ g).support ⊆ s

Tactic:
· rw [sum_mapRange_index (fun _ ↦ rfl), ← hsum, _root_.map_finsuppSum]

Goal state after:
case right
ι : 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 : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (mapRange ⇑e ⋯ g).support ⊆ s
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
p q : Perm α
⊢ {x | (p * q) x ≠ x} ⊆ {x | p x ≠ x} ∪ {x | q x ≠ x}

Tactic:
simp only [coe_mul]
  grind

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

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

Tactic:
intro H
    rw [H]
    exact single_length h

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : DecidableEq μ
inst✝³ : AddCommMonoid μ
inst✝² : PartialOrder μ
inst✝¹ : CanonicallyOrderedAdd μ
inst✝ : HasAntidiagonal μ
s : Finset ι
⊢ s.finsuppAntidiag 0 = {0}

Tactic:
ext f; simp [finsuppAntidiag, ← DFunLike.coe_fn_eq (g := f), eq_comm]

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
l : List α
h : n + ns.sum = l.length
⊢ ns.sum = (drop n l).length

Tactic:
rw [length_drop, ← h, add_tsub_cancel_left]

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)
⊢ ((insert i s).noncommProd k ⋯).support = (insert i s).biUnion fun i ↦ (k i).support

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.biUnion_insert]

Goal state after:
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)
⊢ (k i * s.noncommProd k ⋯).support = (k i).support ∪ s.biUnion fun i ↦ (k i).support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
⊢ False

Tactic:
rcases (Nat.succ_le_of_lt hn).eq_or_lt with hn' | hn'

Goal state after:
case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
⊢ False

case a.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ < l.length
⊢ False
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ l.length = 1

Tactic:
← hn',

Goal state after:
case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ n.succ = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
⊢ f = g

Tactic:
have : f.support ⊆ g.support := by
    intro y hy
    obtain ⟨k, rfl⟩ := hf.exists_pow_eq (mem_support.mp hx') (mem_support.mp hy)
    rwa [pow_eq_on_of_mem_support h _ _ (mem_inter_of_mem hx' hx''), pow_apply_mem_support]

Goal state after:
α : Type u_2
f g : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : ∀ x ∈ f.support ∩ g.support, f x = g x
hx : f x = g x
hx' : x ∈ f.support
hx'' : x ∈ g.support
this : f.support ⊆ g.support
⊢ f = g
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
n : ℕ
hx : (σ ^ n) (Classical.choose hσ) ∈ ↑σ.support
⊢ ↑(hτ.zpowersEquivSupport
        ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨σ ((σ ^ n) (Classical.choose hσ)), ⋯⟩))) =
    τ
      ↑(hτ.zpowersEquivSupport
          ((zpowersEquivZPowers ⋯) (hσ.zpowersEquivSupport.symm ⟨(σ ^ n) (Classical.choose hσ), hx⟩)))

Tactic:
simp [← Perm.mul_apply, ← pow_succ']

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

Goal state before:
pp: case refine_2
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
⊢ f.IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Goal state after:
case refine_2
α : Type u_2
f : Perm α
s : Set α
hs : s.Nontrivial
hf : f.IsCycleOn s
hsf : ∀ ⦃x : α⦄, ¬IsFixedPt (⇑f) x → x ∈ s
a : α
ha : a ∈ s
⊢ f.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
⊢ (f.subtypePerm ⋯).IsCycle

Tactic:
obtain ⟨a, ha⟩ := hs.nonempty

Goal state after:
α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
hs : s.Nontrivial
a : α
ha : a ∈ s
⊢ (f.subtypePerm ⋯).IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
⊢ s.Countable

Tactic:
obtain rfl | ⟨a, ha⟩ := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_2
f : Perm α
hs : f.IsCycleOn ∅
⊢ ∅.Countable

case inr
α : Type u_2
f : Perm α
s : Set α
hs : f.IsCycleOn s
a : α
ha : a ∈ s
⊢ s.Countable
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
s : Set α
hs : s.Countable
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

Tactic:
obtain hs' | hs' := s.finite_or_infinite

Goal state after:
case inl
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Finite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s

case inr
α : Type u_2
s : Set α
hs : s.Countable
hs' : s.Infinite
⊢ ∃ f, f.IsCycleOn s ∧ {x | f x ≠ x} ⊆ s
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
s : Finset (Perm α)
h1 : ∀ f ∈ s, f.IsCycle
h2 : (↑s).Pairwise Disjoint
h0 : s.noncommProd id ⋯ = σ
⊢ σ.cycleType = Multiset.map (Finset.card ∘ support) s.val

Tactic:
rw [cycleType_def]
  congr
  rw [cycleFactorsFinset_eq_finset]
  exact ⟨h1, h2, h0⟩

Goal state after:
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

pp: case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)

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

Goal state after:
case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := ⋯
r : ℤ := ⋯
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
⊢ g ^ m = 1 → (g ^ m) x = x

Tactic:
· intro hgm
      simp only [hgm, coe_one, id_eq]

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

Goal state before:
pp: case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) ((castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩)), ⋯⟩ = 0

Tactic:
rw [this, finRotate_last]

Goal state after:
case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) 0, ⋯⟩ = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType

Tactic:
rintro ⟨c, t, rfl, hd, hc, rfl⟩
    simp [hd.cycleType_mul, hc.cycleType]

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

Goal state before:
pp: case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
⊢ σ ∈ l

Tactic:
have hτl : ∀ x ∈ τ.support, τ x = l.prod x := eq_on_support_mem_disjoint hτ h2

Goal state after:
case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
h : ∀ (a : α), σ a ≠ a → σ a = l.prod a
hσl : σ.support ⊆ l.prod.support
a : α
ha : a ∈ σ.support
τ : Perm α
hτ : τ ∈ l
hτa : a ∈ τ.support
hτl : ∀ x ∈ τ.support, τ x = l.prod x
⊢ σ ∈ l
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i = j
⊢ j.cycleIcc j = 1

Tactic:
← cycleIcc_eq

Goal state after:
case inr
n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i = j
⊢ j.cycleIcc j = cycleIcc ?m.29 ?m.29

n : ℕ
i j : Fin n
hij✝ : i ≤ j
inst✝ : NeZero n
hij : i = j
⊢ Fin n
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
i j : Fin n
hij : j < i
⊢ min (σ i) (σ j) ≠ max (σ i) (σ j)

Tactic:
simp [hij.ne.symm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
a b : R
eq : detp 1 A = detp (-1) A
⊢ A.IsDetpBalanced a b

Tactic:
by
  rw [IsDetpBalanced, eq, add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Alternating.Basic

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
⊢ ⇑((Fintype.card ι).factorial • ↑a) = ⇑↑((Fintype.card ι).factorial • a)

Tactic:
coe_smul

Goal state after: