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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
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✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)

Tactic:
by
    ext X
    cases X
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Retract

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h✝ : RetractArrow f✝ g✝
X Y Z W : Cᵒᵖ
f : X ⟶ Y
g : Z ⟶ W
h : RetractArrow f g
⊢ Arrow.homMk (Arrow.Hom.right h.r).unop (Arrow.Hom.left h.r).unop ⋯ ≫
      Arrow.homMk (Arrow.Hom.right h.i).unop (Arrow.Hom.left h.i).unop ⋯ =
    𝟙 (Arrow.mk f.unop)

Tactic:
by ext <;> simp [← unop_comp]

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)

Tactic:
by
  ext1; simp

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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)

Tactic:
· exact (π _).symm

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
⊢ ∀ (s : Fan fun p ↦ g p.fst p.snd)
    (m : s.pt ⟶ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).pt),
    (∀ (j : (i : ι) × f i),
        m ≫ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j = s.proj j) →
      m = Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩

Tactic:
intro s (m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i)) w

Goal state after:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
s : Fan fun p ↦ g p.fst p.snd
m : s.pt ⟶ ∏ᶜ fun i ↦ ∏ᶜ g i
w :
  ∀ (j : (i : ι) × f i),
    m ≫ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j = s.proj j
⊢ m = Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩
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
⊢ inl ((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).inl

Tactic:
simp [inl]

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
T : D
S : C ⥤ D
x y : CostructuredArrow S T
hl : x.left = y.left
hh : S.map (eqToHom hl) ≫ y.hom = x.hom
⊢ x = y

Tactic:
cases x
  cases y
  cases hl
  cat_disch

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ f = default

Tactic:
← cancel_epi e.inv

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y : C
hY : IsZero Y
e : X ≅ Y
Z : C
f : X ⟶ Z
⊢ e.inv ≫ f = e.inv ≫ default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_to.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ F ⟶ G

Tactic:
refine
      { app := fun X => (hF _).to_ _
        naturality := ?_ }
    intros
    exact (hF _).eq_of_src _ _

Goal state after:
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
inst✝ : HasZeroObject D
F : C ⥤ D
hF : IsZero F
X : C
⊢ IsZero (F.obj X)

Tactic:
by
  let G : C ⥤ D := (CategoryTheory.Functor.const C).obj 0
  have hG : IsZero G := Functor.isZero _ fun _ => isZero_zero _
  let e : F ≅ G := hF.iso hG
  exact (isZero_zero _).of_iso (e.app X)

Goal state after:
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✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ η.app X ≫ NatTrans.app 0 X = NatTrans.app 0 X

Tactic:
apply comp_zero

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
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)

Tactic:
apply strongEpi_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
⊢ f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f

Tactic:
simp only [Iso.hom_inv_id_assoc, id_comp]

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✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
m✝ : s.pt ⟶ (coneOfIsSplitMono f).pt
hm : m✝ ≫ (coneOfIsSplitMono f).ι = s.ι
⊢ m✝ = s.ι ≫ retraction f

Tactic:
by simp [← 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✝
inst✝¹ : IsSplitEpi f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
m✝ : (coconeOfIsSplitEpi f).pt ⟶ s.pt
hm : (coconeOfIsSplitEpi f).π ≫ m✝ = s.π
⊢ m✝ = section_ f ≫ s.π

Tactic:
by simp [← hm]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (F.mapCocone (Cocone.whisker e.functor c))

Tactic:
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : Type w
inst✝² : Category.{w', w} J
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : ReflectsColimitsOfShape J F
K✝ : J' ⥤ C
c : Cocone K✝
t : IsColimit (F.mapCocone c)
⊢ IsColimit (Cocone.whisker e.functor (F.mapCocone c))
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✝)).hom = (x✝² ≫ x✝¹ + x✝² ≫ x✝).hom

Tactic:
apply comp_add

Goal state after:
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✝)).hom = (x✝² ≫ x✝¹ + x✝² ≫ x✝).hom

Tactic:
apply comp_add

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
⊢ (⨆ a, P a).isoClosure = ⨆ a, (P a).isoClosure

Tactic:
refine le_antisymm ?_ ?_
  · rintro X ⟨Y, hY, ⟨e⟩⟩
    simp only [prop_iSup_iff] at hY ⊢
    obtain ⟨a, hY⟩ := hY
    exact ⟨a, _, hY, ⟨e⟩⟩
  · simp only [iSup_le_iff]
    intro a
    rw [isoClosure_le_iff]
    exact (le_iSup P a).trans (le_isoClosure _)

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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
j : WalkingParallelPair
⊢ t.ι.app j ≫ desc s = s.ι.app j

Tactic:
by
      cases j
      · simp
      · exact fac s

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 𝟙 c.pt = 0

Tactic:
← cancel_epi c.π,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ Cofork.π c ≫ 𝟙 c.pt = Cofork.π c ≫ 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
inst✝ : HasCokernel f
h : f = f
⊢ cokernelIsoOfEq h = Iso.refl (cokernel f)

Tactic:
by
  ext; simp [cokernelIsoOfEq]

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

Goal state before:
pp: J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X✝ Y✝ : BinaryBicone P Q
f : X✝ ⟶ Y✝
⊢ { pt := F.obj X✝.pt, fst := F.map X✝.fst, snd := F.map X✝.snd, inl := F.map X✝.inl, inr := F.map X✝.inr, inl_fst := ⋯,
          inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inr ≫
      F.map f.hom =
    { pt := F.obj Y✝.pt, fst := F.map Y✝.fst, snd := F.map Y✝.snd, inl := F.map Y✝.inl, inr := F.map Y✝.inr,
        inl_fst := ⋯, inl_snd := ⋯, inr_fst := ⋯, inr_snd := ⋯ }.inr

Tactic:
by simp [-BinaryBiconeMorphism.winr, ← f.winr]

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 u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
⊢ HasBiproduct f

Tactic:
cases nonempty_fintype J
  exact HasBiproduct.mk
    { bicone := _
      isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

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 : IsLimit c.toCone
s : Fork c.fst 0
m✝ : s.pt ⟶ c.fstKernelFork.pt
hm : m✝ ≫ Fork.ι c.fstKernelFork = s.ι
⊢ m✝ = s.ι ≫ c.snd

Tactic:
by simp [← hm]

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 : IsLimit c.toCone
s : Fork c.snd 0
m✝ : s.pt ⟶ c.sndKernelFork.pt
hm : m✝ ≫ Fork.ι c.sndKernelFork = s.ι
⊢ m✝ = s.ι ≫ c.fst

Tactic:
by simp [← hm]

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
m✝ : c.inlCokernelCofork.pt ⟶ s.pt
hm : Cofork.π c.inlCokernelCofork ≫ m✝ = s.π
⊢ m✝ = c.inr ≫ s.π

Tactic:
by simp [← hm]

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
m✝ : c.inrCokernelCofork.pt ⟶ s.pt
hm : Cofork.π c.inrCokernelCofork ≫ m✝ = s.π
⊢ m✝ = c.inl ≫ s.π

Tactic:
by simp [← hm]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
x : ↑M
⊢ LinearMap.id x = 0

Tactic:
← ModuleCat.hom_id

Goal state after:
R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
x : ↑M
⊢ (Hom.hom (𝟙 M)) x = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case elim0.zero
k : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 0 ↔ ∑ i, i.elim0 = 0

pp: case elim0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i, i.elim0 = n✝ + 1

Tactic:
· decide

Goal state after:
case elim0.succ
k n✝ : ℕ
⊢ Fin.elim0 ∈ antidiagonalTuple 0 (n✝ + 1) ↔ ∑ i, i.elim0 = n✝ + 1
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a, a.1 + a.2 = n ∧ a.2 = ∑ i, x i ∧ a.1 = x₀) ↔ x₀ + ∑ i, x i = n

Tactic:
and_comm (a := Prod.snd _ = _),

Goal state after:
case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a, a.1 + a.2 = n ∧ a.1 = x₀ ∧ a.2 = ∑ i, x i) ↔ x₀ + ∑ i, x i = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
| n

Tactic:
← c.blocks_sum,

Goal state after:
n : ℕ
c : Composition n
| c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
i : ℕ
| n

Tactic:
← c.blocks_sum,

Goal state after:
n : ℕ
c : Composition n
i : ℕ
| c.blocks.sum
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Fintype τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
nz : 𝟙 (S s) ≠ 0
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → 𝟙 (S s) = 0
h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0
⊢ False

Tactic:
exact nz (t h)

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

Goal state before:
pp: n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ n = n'

Tactic:
← c.blocks_sum,

Goal state after:
n : ℕ
c : Composition n
n' : ℕ
c' : Composition n'
H : ⟨n, c⟩.snd.blocks = ⟨n', c'⟩.snd.blocks
⊢ c.blocks.sum = n'
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support ↔ f x ≠ x

Tactic:
support,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ {x | f x ≠ x} ↔ f x ≠ x
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
| n

Tactic:
← c.blocks_sum,

Goal state after:
n : ℕ
c : Composition n
H : ∀ i ∈ c.blocks, i = 1
A : c.blocks = replicate c.blocks.length 1
| c.blocks.sum
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c = ones n ↔ n ≤ c.length

Tactic:
by
  simp [eq_ones_iff_length, le_antisymm_iff, c.length_le]

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.length < c.boundaries.card

Tactic:
rw [c.card_boundaries_eq_succ_length]

Goal state after:
n : ℕ
c : CompositionAsSet n
⊢ c.length < c.length + 1
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.toComposition.length = c.length

Tactic:
simp [CompositionAsSet.toComposition, Composition.length]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y x✝ : α
ha : f x✝ ≠ x✝
hx : x✝ ≠ x
hy : x✝ ≠ y
H : (swap x y) (f x✝) = x✝
⊢ False

Tactic:
swap_apply_eq_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y x✝ : α
ha : f x✝ ≠ x✝
hx : x✝ ≠ x
hy : x✝ ≠ y
H : f x✝ = (swap x y) x✝
⊢ False
Module: Mathlib.Data.Fintype.Perm

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
⊢ f heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []

Tactic:
by
    have : f = 1 := by simpa [permsOfList] using h
    rw [this]; simp

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

Goal state before:
pp: case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup

Tactic:
IsRotated.nodup_iff

Goal state after:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ Nodup ?m.32

case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r ?m.32

α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ List α
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ (l.rotate n).Nodup

Tactic:
rwa [IsRotated.nodup_iff]

Goal state after:
case succ.h
α : Type u_1
inst✝ : DecidableEq α
l : List α
h : l.Nodup
n : ℕ
hn : (l.rotate n).formPerm = l.formPerm
⊢ l.rotate n ~r l
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl.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 : g (τ ((Equiv.symm g) (f x))) = f x
⊢ τ x = x

Tactic:
(hd1 x).resolve_left hxσ

Goal state after:
case intro.refine_2.inl.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 : g (τ ((Equiv.symm g) (f x))) = f x
⊢ x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (-i)) y = x

Tactic:
simp [zpow_neg, ← hi]

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

Goal state before:
pp: n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    (∏ x ∈ finPairsLT n, if f x.fst ≤ f x.snd then -1 else 1) *
      ∏ x ∈ finPairsLT n, if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1

Tactic:
rw [← prod_mul_distrib]

Goal state after:
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x ∈ finPairsLT n, if (f * g) x.fst ≤ (f * g) x.snd then -1 else 1) =
    ∏ x ∈ finPairsLT n, (if f x.fst ≤ f x.snd then -1 else 1) * if g⁻¹ x.fst ≤ g⁻¹ x.snd then -1 else 1
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ swap x ((σ ^ (n + 1)) x) ∈ H

Tactic:
← h6,

Goal state after:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
ih : swap x ((σ ^ n) x) ∈ H
h5 : ¬x = (σ ^ n) x
h6 : x = (σ ^ (n + 1)) x
⊢ swap x x ∈ H
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
step1 : ∀ (n : ℕ), swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
n : ℕ
⊢ swap x ((σ ^ n) x) ∈ H

Tactic:
induction n with
    | zero =>
      simp only [pow_zero, coe_one, id_eq, swap_self]
      convert! H.one_mem
    | succ n ih =>
      by_cases h5 : x = (σ ^ n) x
      · rw [pow_succ', mul_apply, ← h5]
        exact h4
      by_cases h6 : x = (σ ^ (n + 1) : Perm α) x
      · rw [← h6, swap_self]
        exact H.one_mem
      rw [swap_comm, ← swap_mul_swap_mul_swap h5 h6]
      exact H.mul_mem (H.mul_mem (step1 n) ih) (step1 n)

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

Goal state before:
pp: case mpr
α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
g : Perm α
⊢ ↑g.support ⊆ Set.ofPred p → g ∈ ofSubtype.range

Tactic:
intro hg
    refine ⟨g.subtypePerm fun x ↦ ?_, ofSubtype_subtypePerm _ fun x hx ↦ hg (mem_support.mpr hx)⟩
    by_cases hx : g x = x
    · rw [hx]
    · refine iff_of_true (hg ?_) (hg ?_) <;> simpa

Goal state after:
Module: Mathlib.Data.List.Iterate

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
⊢ iterate f a n = [] ↔ n = 0

Tactic:
by
  rw [← length_eq_zero_iff, length_iterate]

Goal state after:
Module: Mathlib.Data.Nat.GCD.BigOperators

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : ι → ℕ
x : ℕ
⊢ (∏ i, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x

Tactic:
simp [coprime_prod_left_iff]

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

Goal state before:
pp: case inr
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hfyx : ¬y = f x
hy : ¬f y = y
j : ℤ
hj : (f ^ (j - i)) x = y
hji : (f ^ (j - i)) x = f x
⊢ False

Tactic:
rw [← hj, hji] at hfyx

Goal state after:
case inr
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hfx : f x ≠ x
hffx : f (f x) = x
y z : α
hz : f z ≠ z ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle z y
i : ℤ
hi : (f ^ i) z = x
hyx : ¬y = x
hy : ¬f y = y
j : ℤ
hfyx : ¬f x = f x
hj : (f ^ (j - i)) x = y
hji : (f ^ (j - i)) x = f x
⊢ False
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
⊢ (f ^ n) z = 1 z

Tactic:
by_cases hz : f z = z

Goal state after:
case pos
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : f z = z
⊢ (f ^ n) z = 1 z

case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬f z = z
⊢ (f ^ n) z = 1 z