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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
F : C ⥤ D
X Y Z : C
e : X ⟶ Y
he : IsIso e
f : Y ⟶ Z
hf : P.inverseImage F f
⊢ P.inverseImage F (e ≫ f)

Tactic:
simpa [MorphismProperty.inverseImage, cancel_left_of_respectsIso] using hf

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X✝ : C
Y✝ : D
f✝ : X' ⟶ X✝
g✝ : X✝ ⟶ G.obj Y✝
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (e X Y') ((e X Y).symm f ≫ g)

Tactic:
he

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
F_obj : C → D
e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)
he : ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y), (e X Y') (h ≫ g) = (e X Y) h ≫ G.map g
X' X✝ : C
Y✝ : D
f✝ : X' ⟶ X✝
g✝ : X✝ ⟶ G.obj Y✝
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (e X Y) ((e X Y).symm f) ≫ G.map g
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ (e X' Y) (F.map f ≫ (e X Y).symm g) = f ≫ g

Tactic:
he

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X' X : C
Y : D
f : X' ⟶ X
g : X ⟶ G_obj Y
⊢ f ≫ (e X Y) ((e X Y).symm g) = f ≫ g
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
hf : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
⊢ IsIso f

Tactic:
by
  obtain ⟨g, hg : g ≫ f = 𝟙 Y⟩ := (hf Y).2 (𝟙 Y)
  exact ⟨g, (hf _).1 (by cat_disch), hg⟩

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsInitial X
hY : IsInitial Y
f : X ⟶ Y
⊢ f ≫ hY.to X = 𝟙 X

Tactic:
apply IsInitial.hom_ext hX

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

Goal state before:
pp: β : Type w
α✝ : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α✝ → C
g : β → C
inst✝ : HasCoproduct f
e : β ≃ α✝
iso : (j : β) → g j ≅ f (e j)
α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f
⊢ HasCoproduct g

Tactic:
exact hasColimit_of_iso α

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

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ m.right = (homMk (T.preimage c.pt.hom) ⋯).right

Tactic:
apply T.map_injective

Goal state after:
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
inst✝¹ : T.Full
inst✝ : T.Faithful
c : Cocone (Functor.empty (StructuredArrow (T.obj Y) T))
m : (asEmptyCocone (mk (𝟙 (T.obj Y)))).pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{1}), (asEmptyCocone (mk (𝟙 (T.obj Y)))).ι.app j ≫ m = c.ι.app j
⊢ T.map m.right = T.map (homMk (T.preimage c.pt.hom) ⋯).right
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
⊢ Mono t.snd

Tactic:
by
  refine ⟨fun {W} h k i => IsLimit.hom_ext ht ?_ i⟩
  rw [← cancel_mono f, Category.assoc, Category.assoc, condition]
  apply reassoc_of% i

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:
by simp only [Category.assoc, hxh, hyh, s.condition]

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✝
s : PullbackCone (f ≫ i) (g ≫ i)
⊢ { l //
    l ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst ∧
      l ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt},
          m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst → m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l }

Tactic:
rcases PullbackCone.IsLimit.lift' H s.fst s.snd
      ((cancel_mono i).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩

Goal state after:
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✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
⊢ { l //
    l ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst ∧
      l ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt},
          m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst → m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h

Tactic:
rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
val✝ : (mk (𝟙 Y) (𝟙 Y) ⋯).pt ⟶ Z
eq : f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = f ≫ (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝
⊢ (mk (𝟙 Y) (𝟙 Y) ⋯).inl ≫ val✝ = (mk (𝟙 Y) (𝟙 Y) ⋯).inr ≫ val✝
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom = image.ι f.hom ≫ Arrow.Hom.right sq

Tactic:
← cancel_mono (inv sq).right,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (image.lift ((Image.monoFactorisation g.hom).ofArrowIso (inv sq)) ≫ image.ι g.hom) ≫ Arrow.Hom.right (inv sq) =
    (image.ι f.hom ≫ Arrow.Hom.right sq) ≫ Arrow.Hom.right (inv sq)
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: 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)
⊢ (s'.ι ≫ h) ≫ f = (s'.ι ≫ h) ≫ g

Tactic:
by simp [s'.condition]

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

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

Tactic:
by
  rw [zero_of_source_iso_zero f i]
  exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩

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

Goal state before:
pp: C✝ : Type u
inst✝⁷ : Category.{v, u} C✝
inst✝⁶ : Preadditive C✝
R : Type w
inst✝⁵ : Semiring R
inst✝⁴ : Linear R C✝
k : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Semiring k
inst✝¹ : Preadditive C
inst✝ : Linear k C
X Y W Z : C
f₁ : X ≅ Y
f₂ : W ≅ Z
x : Y ⟶ Z
⊢ (rightComp k Y f₂.hom ∘ₗ leftComp k W f₁.symm.hom).toFun ((leftComp k W f₁.hom ∘ₗ rightComp k Y f₂.symm.hom) x) = x

Tactic:
simp only [Iso.symm_hom, LinearMap.coe_comp, Function.comp_apply, rightComp_apply,
        leftComp_apply, LinearMap.toFun_eq_coe, Iso.inv_hom_id_assoc, Category.assoc,
        Iso.inv_hom_id, Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
h : ∀ (J : Type w) {𝒥 : SmallCategory J} (x : FinCategory J), HasColimitsOfShape J C
J : Type
hJ : SmallCategory J
hhJ : FinCategory J
this : HasColimitsOfShape (ULiftHom (ULift.{w, 0} J)) C
l : J ≌ ULiftHom (ULift.{?u.47, 0} J)
⊢ HasColimitsOfShape J C

Tactic:
apply @hasColimitsOfShape_of_equivalence (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) C _ J hJ
      (@Equivalence.symm J hJ (ULiftHom (ULift J))
      (@ULiftHom.category (ULift J) (@uliftCategory J hJ)) l) _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteLimits C
J : Type
x✝ : Finite J
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteLimits C
J : Type
x✝ : Finite J
val✝ : Fintype J
⊢ HasLimitsOfShape (WidePullbackShape J) C
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
⊢ HasColimitsOfShape (WidePushoutShape J) C

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u
inst✝¹ : Category.{v, u} C
J✝ : Type v
inst✝ : HasFiniteColimits C
J : Type
x✝ : Finite J
val✝ : Fintype J
⊢ HasColimitsOfShape (WidePushoutShape J) C
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
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
⊢ h ≫ Cofork.π c = 0

Tactic:
hh

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
⊢ (g ≫ f) ≫ Cofork.π c = 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
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ biprod.lift (F.map (𝟙 X)) (F.map (𝟙 X)) ≫ biprod.desc (F.map f) (F.map g) = F.map f + F.map g

Tactic:
F.map_id,

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : HasBinaryBiproducts C
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : PreservesBinaryBiproducts F
X Y : C
f g : X ⟶ Y
⊢ biprod.lift (𝟙 (F.obj X)) (𝟙 (F.obj X)) ≫ biprod.desc (F.map f) (F.map g) = F.map f + F.map g
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

Goal state after:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f
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✝ : HasCoproduct f
⊢ HasBiproduct f

Tactic:
cases nonempty_fintype J

Goal state after:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type u_1
inst✝¹ : Finite J
f : J → C
inst✝ : HasCoproduct f
val✝ : Fintype J
⊢ HasBiproduct f
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₂
⊢ biprod.inl ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₁₁ ≫ biprod.inl + f₁₂ ≫ biprod.inr

Tactic:
simp [Biprod.ofComponents]

Goal state after:
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₂
⊢ biprod.inr ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr

Tactic:
simp [Biprod.ofComponents]

Goal state after:
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₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fst ≫ f₁₁ + biprod.snd ≫ f₂₁

Tactic:
simp [Biprod.ofComponents]

Goal state after:
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₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.snd = biprod.fst ≫ f₁₂ + biprod.snd ≫ f₂₂

Tactic:
simp [Biprod.ofComponents]

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

Goal state before:
pp: n : ℕ
c : Composition n
j : Fin n
⊢ ↑j < c.sizeUpTo (↑(c.index j) + 1)

Tactic:
exact lt_sizeUpTo_index_succ _ _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: case refine_1
n✝ : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
n a : ℕ
ha1 : 1 ≤ a
ha : a ≤ n
p : { p // a ∈ p.parts }
i✝ : ℕ
hi : i✝ ∈ (↑p).parts.erase a
⊢ 0 < i✝

Tactic:
exact p.1.parts_pos (p.1.parts.erase_subset a hi)

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
f : ι →₀ μ'
⊢ (∃ a, ((a.sum fun x x_1 ↦ x_1) = n ∧ a.support ⊆ s) ∧ (mapRange.addEquiv e).toEmbedding a = f) →
    (f.sum fun x x_1 ↦ x_1) = e n ∧ f.support ⊆ s

Tactic:
rintro ⟨g, ⟨hsum, hsupp⟩, rfl⟩

Goal state after:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (((mapRange.addEquiv e).toEmbedding g).sum fun x x_1 ↦ x_1) = e n ∧ ((mapRange.addEquiv e).toEmbedding g).support ⊆ s
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
n : ℕ
c : Composition n
⊢ ¬c = ones n → ¬c.length = n

Tactic:
intro H length_n

Goal state after:
case mpr
n : ℕ
c : Composition n
H : ¬c = ones n
length_n : c.length = n
⊢ False
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

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

Tactic:
hh

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

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

Tactic:
simp only [or_iff_not_imp_left, ← ne_eq, ← Fin.exists_succ_eq]

Goal state after:
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
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm ((x :: xs).getLast ⋯) = x

Tactic:
by
  induction xs using List.reverseRecOn generalizing x <;> simp

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

Goal state before:
pp: case neg.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : #f.support = 2
y : α
ht : #{y} = 1
a : α
ha : ¬f a = a
hmem : ¬a = y
hins : {a, y} = f.support
key : ∀ (b : α), f b ≠ b ↔ b = a ∨ b = y
ha' : f a = a ∨ f a = y
⊢ f a = (swap a y) a

Tactic:
rw [Or.resolve_left ha' ha, swap_apply_left]

Goal state after:
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 * τ * g⁻¹) (f x) = f x
⊢ τ x = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))

Tactic:
rw [mul_apply, mul_apply, coe_inv] at h

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 = (Equiv.symm f) (g (τ ((Equiv.symm g) (f x))))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : (f * σ * f⁻¹) (g (τ x)) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))

Tactic:
rw [mul_apply, mul_apply, coe_inv] at h

Goal state after:
case intro.refine_2.inr.refine_2
α : Type u
inst✝ : Finite α
σ τ : Perm α
hd1 : σ.Disjoint τ
val✝ : Fintype α
f : Perm α
hc1 : IsConj σ (f * σ * f⁻¹)
g : Perm α
hc2 : IsConj τ (g * τ * g⁻¹)
hd2 : (f * σ * f⁻¹).Disjoint (g * τ * g⁻¹)
hd1' : ↑(σ * τ).support = ↑σ.support ∪ ↑τ.support
hd2' : ↑(f * σ * f⁻¹ * (g * τ * g⁻¹)).support = ↑(f * σ * f⁻¹).support ∪ ↑(g * τ * g⁻¹).support
hd1'' : _root_.Disjoint ↑σ.support ↑τ.support
hd2'' : _root_.Disjoint ↑(f * σ * f⁻¹).support ↑(g * τ * g⁻¹).support
x : α
hx : x ∈ ↑(σ * τ).support
hxτ : τ (τ x) ≠ τ x
h : f (σ ((Equiv.symm f) (g (τ x)))) = g (τ x)
⊢ g (σ (τ x)) = f (σ (f⁻¹ (g (τ (g⁻¹ (g x))))))
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
hf : f.IsCycle
hx : f x ≠ x
hy : f y ≠ y
n : ℤ
hn : (f ^ n) x = y
⊢ (f ^ (n % ↑(orderOf f)).toNat) x = y

Tactic:
{have := n.emod_nonneg (Int.natCast_ne_zero.mpr (ne_of_gt (orderOf_pos f)))
         rwa [← zpow_natCast, Int.toNat_of_nonneg this, zpow_mod_orderOf]}

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ (swap ⟨0, ⋯⟩ ⟨1, ⋯⟩).signAux = -1

Tactic:
by
  rcases n with (_ | _ | n)
  · norm_num at hn
  · norm_num at hn
  · exact signAux_swap_zero_one' n

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

Goal state before:
pp: case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ (List.map (fun a ↦ prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

Tactic:
List.map_nil,

Goal state after:
case nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ [].prod (a, b) = (a, b)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case inl.inr
α : Type u_2
inst✝ : DecidableEq α
x y : α
hab : x ≠ y
⊢ (swap x y).SameCycle x y

Tactic:
exact ⟨1, by rw [zpow_one, swap_apply_left]⟩

Goal state after:
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
  · exact Set.countable_empty
  · exact (Set.countable_range fun n : ℤ => (⇑(f ^ n) : α → α) a).mono (hs.2 ha)

Goal state after: