mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
f' : Y✝ ⟶ Z✝
⊢ (e X✝ (F_obj Z✝)).symm ((f ≫ f') ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝))) =
    (e X✝ (F_obj Y✝)).symm (f ≫ (e Y✝ (F_obj Y✝)) (𝟙 (F_obj Y✝))) ≫
      (e Y✝ (F_obj Z✝)).symm (f' ≫ (e Z✝ (F_obj Z✝)) (𝟙 (F_obj Z✝)))

Tactic:
by
    rw [Equiv.symm_apply_eq, he, Equiv.apply_symm_apply]
    conv =>
      rhs
      rw [assoc, ← he, id_comp, Equiv.apply_symm_apply]
    simp

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

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
F : J ⥤ C
t : Cone F
X : C
h : F.cones.RepresentableBy X
s : Cone F
m : s.pt ⟶ (limitCone h).pt
w : ∀ (j : J), m ≫ (limitCone h).π.app j = s.π.app j
⊢ m = homOfCone h s

Tactic:
rw [← homOfCone_coneOfHom h m]
    congr
    rw [coneOfHom_fac]
    dsimp [Cone.extend]; cases s; congr with j; exact w j

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
rw [isIso_iff_coyoneda_map_bijective]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (∀ (T : C), Function.Bijective fun x ↦ f ≫ x) ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)
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 : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ f.unop.hom ≫ (unop X).π.app (op j) = (unop Y).π.app (op j)

Tactic:
apply ConeMorphism.w

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
l : sq.LiftStruct
⊢ (adj.homEquiv B X) l.l ≫ F.map p = (adj.homEquiv B Y) v

Tactic:
rw [← Adjunction.homEquiv_naturality_right, l.fac_right]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ ⋯.HasLift

Tactic:
right_adjoint_hasLift_iff

Goal state after:
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ HasLift ?sq

case sq
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
inst✝ : sq.HasLift
⊢ CommSq u (G.map i) p v
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
A B : C
f : A ⟶ B
inst✝ : F.IsEquivalence
⊢ StrongEpi (F.map f) → StrongEpi f

Tactic:
intro
    have e : Arrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
    rw [StrongEpi.iff_of_arrow_iso e]
    infer_instance

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ (G.map (lift F c) ≫ post F G) ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Tactic:
rw [assoc, limit.post_π, ← G.map_comp, limit.lift_π, limit.lift_π]

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (c.π.app j✝) = (G.mapCone c).π.app j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
⊢ m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
e₂

Goal state after:
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
⊢ c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
e₂

Goal state after:
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ m = IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
j : WalkingCospan
⊢ F.obj j = (cospan (F.map inl) (F.map inr)).obj j

Tactic:
by rcases j with (⟨⟩ | ⟨⟨⟩⟩) <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
j : WalkingSpan
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j

Tactic:
by rcases j with (⟨⟩ | ⟨⟨⟩⟩) <;> rfl

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✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ i₁ = i₂

Tactic:
by
    ext
    · simpa using congrArg (fun f => coprod.inl ≫ f) h
    · simpa using congrArg (fun f => coprod.inr ≫ f) h

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

Goal state before:
pp: case unique_to
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)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (F ⟶ Y))

Tactic:
intro G

Goal state after:
case unique_to
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
⊢ Nonempty (Unique (F ⟶ G))
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from
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)
⊢ ∀ (Y : C ⥤ D), Nonempty (Unique (Y ⟶ F))

Tactic:
intro G

Goal state after:
case unique_from
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
⊢ Nonempty (Unique (G ⟶ F))
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
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = image.ι g

Tactic:
← this,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ (MonoFactorisation.ofIsoComp f F').m = image.ι g
Module: Mathlib.Algebra.Category.ModuleCat.Semi

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s • (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
smul_eq_mul,

Goal state after:
R : Type u
inst✝³ : Semiring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Semiring S
inst✝ : Algebra S₀ S
M N : SemimoduleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s * (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

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

Tactic:
← this,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I J : HasZeroMorphisms C
X Y : C
this : Zero.zero ≫ Zero.zero = Zero.zero
that : Zero.zero ≫ Zero.zero = Zero.zero
⊢ Zero.zero ≫ Zero.zero = Zero.zero
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
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
rw [Iso.comp_inv_eq, w]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inl X Y ≫ fst = 𝟙 X

Tactic:
simp [prod.inl]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inl X Y ≫ snd = 0

Tactic:
simp [prod.inl]

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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm : Epi h
⊢ (h ≫ f) ≫ c.π = (h ≫ g) ≫ c.π

Tactic:
simp only [Category.assoc]
      exact congrArg (h ≫ ·) c.condition

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

Goal state before:
pp: J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (whiskerEquiv e w).hom = lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

Tactic:
simp only [whiskerEquiv_hom]

Goal state after:
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (desc fun j ↦ (w j).inv ≫ ι g (e j)) = lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
⊢ matrix m ≫ desc x = desc fun j ↦ ∑ k, m j k ≫ x k

Tactic:
by
  ext
  simp [lift_desc]

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ (if h : (p ↑k)ᶜ then biproduct.ι (Subtype.restrict pᶜ f) ⟨↑k, h⟩ else 0) ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0

Tactic:
rw [dif_neg]

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K✝ : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
j : Subtype pᶜ
k : Subtype p
⊢ 0 ≫ biproduct.π (Subtype.restrict pᶜ f) j = 0

case hnc
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
j : Subtype pᶜ
k : Subtype p
⊢ ¬(p ↑k)ᶜ
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.toCone.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
⊢ m = f ≫ b.inl + g ≫ b.inr

Tactic:
dsimp at m
      have h₁' : ((m : T ⟶ b.pt) - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0 := by
        simpa using sub_eq_zero.2 h₁
      have h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0 := by simpa using sub_eq_zero.2 h₂
      obtain ⟨q : T ⟶ X, hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)⟩ :=
        KernelFork.IsLimit.lift' hb _ h₂'
      rw [← sub_eq_zero, ← hq, ← Category.comp_id q, ← b.inl_fst, ← Category.assoc, hq, h₁',
        zero_comp]

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

Goal state before:
pp: R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s • (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n

Tactic:
smul_eq_mul,

Goal state after:
R : Type u
inst✝³ : Ring R
X₁ X₂ : Type v
S₀ : Type u₀
inst✝² : CommSemiring S₀
S : Type u
inst✝¹ : Ring S
inst✝ : Algebra S₀ S
M N : ModuleCat S
s : S
s₀ : S₀
n : ↑M
⊢ (s * (algebraMap S₀ S) s₀) • n = (algebraMap S₀ S) s₀ • s • n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ ∀ (x : Fin (c.length + 1)), c.boundary x ∈ c.boundaries

Tactic:
exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

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

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

Tactic:
by_contra! H

Goal state after:
n : ℕ
c : Composition n
j : Fin n
H : ↑j < c.sizeUpTo ↑(c.index j)
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j - c.sizeUpTo ↑i < c.blocksFun i

Tactic:
rw [tsub_lt_iff_left, ← sizeUpTo_succ']

Goal state after:
case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ ↑j < c.sizeUpTo (↑i + 1)

case mpr.refine_1
n : ℕ
c : Composition n
j : Fin n
i : Fin c.length
h : c.sizeUpTo ↑i ≤ ↑j ∧ ↑j < c.sizeUpTo (↑i).succ
⊢ c.sizeUpTo ↑i ≤ ↑j
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
i : Fin (ones n).length
h : 0 < (ones n).blocksFun i
⊢ ↑(((ones n).embedding i) ⟨0, h⟩) = ↑⟨↑i, ⋯⟩

Tactic:
simpa using i.2.le

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ c.blocks.sum = n

Tactic:
← this,

Goal state after:
n : ℕ
c : CompositionAsSet n
this : take c.length c.blocks = c.blocks
⊢ (take c.length c.blocks).sum = n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ ((g ^ n).extendDomain f) ↑(f x) = ↑(f y) ↔ (g ^ n) x = y

Tactic:
extendDomain_apply_image,

Goal state after:
α : Type u_2
β : Type u_3
g : Perm α
x y : α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
n : ℤ
⊢ ↑(f ((g ^ n) x)) = ↑(f y) ↔ (g ^ n) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableEq α
⊢ f.IsSwap → f.IsCycle

Tactic:
rintro ⟨x, y, hxy, rfl⟩
  exact isCycle_swap hxy

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ (ofSubtype u).Disjoint g

Tactic:
rw [disjoint_iff_eq_or_eq]

Goal state after:
α : Type u
inst✝ : DecidableEq α
g : Perm α
u : Perm ↑(fixedPoints ⇑g)
⊢ ∀ (x : α), (ofSubtype u) x = x ∨ g x = x
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
step2 : ∀ (n : ℕ), swap x ((σ ^ n) x) ∈ H
step3 : ∀ (y : α), swap x y ∈ H
step4 : ∀ (y z : α), swap y z ∈ H
τ : Perm α
y z : α
left✝ : y ≠ z
h6 : τ = swap y z
⊢ swap y z ∈ ↑(closure {σ, swap x (σ x)})

Tactic:
exact step4 y z

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

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

Tactic:
simp [coprime_prod_right_iff]

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

Goal state before:
pp: case refine_1
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x
hffx : f (f x) ≠ x
⊢ (swap x (f x) * f) (f x) ≠ f x

Tactic:
simp [swap_apply_def, mul_apply, if_neg hffx, f.injective.eq_iff, hx]

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

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℤ
h1 : (f ^ n).IsCycle
h2 : f.support ⊆ (f ^ n).support
⊢ f.IsCycle

Tactic:
cases n
  · exact h1.of_pow h2
  · simp only [zpow_negSucc, Perm.support_inv] at h1 h2
    exact (inv_inv (f ^ _) ▸ h1.inv).of_pow h2

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

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

Tactic:
← support_eq_empty_iff,

Goal state after:
case mp
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
h : (f ^ n).support = f.support
H : f ^ n = 1
⊢ f.support = ∅
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

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

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

pp: case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y

Tactic:
· exact ⟨0, by rw [zpow_zero, coe_one, id]⟩

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

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

case inr.inr
α : Type u_2
a : α
inst✝ : DecidableEq α
y : α
hab : a ≠ y
⊢ (swap a y).SameCycle y y
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
· exact ⟨0, by rw [zpow_zero, coe_one, id]⟩

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

Goal state before:
pp: case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ #s ∣ n

Tactic:
← this,

Goal state after:
case inr
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℕ
hs : s.Nontrivial
h : ∀ (x : ↥s), ¬f ↑x = ↑x
this : orderOf (f.subtypePerm ⋯) = #s
⊢ (f ^ n) a = a ↔ orderOf (f.subtypePerm ⋯) ∣ n
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
a b : α
hs : s.Finite
hf : f.IsCycleOn s
ha : a ∈ s
hb : b ∈ s
⊢ ∃ n, (f ^ n) a = b

Tactic:
lift s to Finset α using hs
  obtain ⟨n, -, hn⟩ := hf.exists_pow_eq ha hb
  exact ⟨n, hn⟩

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

Goal state before:
pp: α : Type u_2
f : Perm α
s : Finset α
hf : f.IsCycleOn ↑s
⊢ s ×ˢ s = (range #s).disjiUnion (fun k ↦ map { toFun := fun i ↦ (i, (f ^ k) i), inj' := ⋯ } s) ⋯

Tactic:
ext ⟨a, b⟩
  simp only [mem_product, Equiv.Perm.coe_pow, mem_disjiUnion, mem_range, mem_map,
    Function.Embedding.coeFn_mk, Prod.mk_inj]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, hn, rfl⟩ := hf.exists_pow_eq hx.1 hx.2
    exact ⟨n, hn, a, hx.1, rfl, by rw [f.iterate_eq_pow]⟩
  · rintro ⟨n, -, a, ha, rfl, rfl⟩
    exact ⟨ha, (hf.1.iterate _).mapsTo ha⟩

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

Goal state before:
pp: α : Type u_2
x : α
f : Perm α
inst✝ : DecidableRel f.SameCycle
hx : f x ≠ x
⊢ (f.cycleOf x) x ≠ x

Tactic:
by rwa [SameCycle.rfl.cycleOf_apply]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ m % ↑(#(g.cycleOf x).support) = n % ↑(#(g.cycleOf x).support)

Tactic:
Int.emod_eq_emod_iff_emod_sub_eq_zero

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
⊢ (g ^ m) x = (g ^ n) x ↔ (m - n) % ↑(#(g.cycleOf x).support) = 0
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ sign (swap i j * π) = (swap i j * π).signAux

Tactic:
Equiv.Perm.signAux_mul,

Goal state after:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ sign (swap i j * π) = (swap i j).signAux * π.signAux
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
x1 x2 : Fin n
⊢ ⟨x1, x2⟩ ∈ Finset.image (fun x ↦ ⟨max (σ x.fst) (σ x.snd), min (σ x.fst) (σ x.snd)⟩) D ↔ ⟨x1, x2⟩ ∈ D

Tactic:
suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]

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
x1 x2 : Fin n
⊢ (∃ a, ∃ b < a, max (σ a) (σ b) = x1 ∧ min (σ a) (σ b) = x2) ↔ x2 < x1