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

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Z✝ : WidePushoutShape J
g : X✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → Hom.id X✝ ≫ g ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs)) (Hom.id X✝ ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦
          Z✝ = X → Hom.id X✝ ≫ g ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs))
          (fun h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ (Hom.id X✝ ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (Hom.id X✝ ≫ g))
      ⋯ ⋯ ⋯ =
    Hom.casesOn (motive := fun a a_1 x ↦
        X✝ = a → X✝ = a_1 → Hom.id X✝ ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn X✝ B objs)) (Hom.id X✝)
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦
            X✝ = X → Hom.id X✝ ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn X✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ (Hom.id X✝))
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ X✝) → X✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn X✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ (Hom.id X✝))
        ⋯ ⋯ ⋯ ≫
      Hom.casesOn (motive := fun a a_1 x ↦
        X✝ = a → Z✝ = a_1 → g ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Z✝ = X → g ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
simp only [hom_id, Category.id_comp]; congr

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

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows

Tactic:
by
  apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term j)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ ∀ (j : WidePullbackShape ι), k ≫ s.π.app j = l ≫ s.π.app j

Tactic:
rintro (_ | j)

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k ≫ s.π.app none = l ≫ s.π.app none

case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
X✝ Y✝ : C✝
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryCoproduct W X
inst✝ : HasBinaryCoproduct Y Z
Z✝ : C
i₁ i₂ : Y ⨿ Z ⟶ Z✝
h : map f g ≫ i₁ = map f g ≫ i₂
⊢ i₁ = i₂

Tactic:
ext
    · rw [← cancel_epi f]
      simpa using congr_arg (fun f => coprod.inl ≫ f) h
    · rw [← cancel_epi g]
      simpa using congr_arg (fun f => coprod.inr ≫ f) h

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

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

Tactic:
by simp [Iso.inv_comp_eq]

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

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

Tactic:
by simp [Iso.inv_comp_eq]

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
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ g = v ≫ q ≫ h

Tactic:
by rw [equalizer.condition g h]

Goal state after:
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.ι f.hom = image.ι f.hom ≫ (𝟙 f).right

Tactic:
Comma.id_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.ι f.hom = image.ι f.hom ≫ 𝟙 f.right
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f ≫ 𝟙 X = default

Tactic:
← comp_id (0 : Y ⟶ X),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f ≫ 𝟙 X = default
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f = default

Tactic:
rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default
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✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := ⋯
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
⊢ (Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c))) ≅
    F.mapCocone c

Tactic:
refine Cocone.ext (Iso.refl _) fun j => ?_

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✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsColimit (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))
j : J'
⊢ ((Cocone.precompose equ.inv).obj (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).ι.app j ≫
      (Iso.refl
          ((Cocone.precompose equ.inv).obj
              (Cocone.whisker e.symm.functor (F.mapCocone (Cocone.whisker e.functor c)))).pt).hom =
    (F.mapCocone c).ι.app j
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✝ : ReflectsLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ IsLimit c

Tactic:
apply IsLimit.ofWhiskerEquivalence e
        apply isLimitOfReflects F
        apply IsLimit.ofIsoLimit _ (Functor.mapConeWhisker _).symm
        exact IsLimit.whiskerEquivalence t _

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

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

Tactic:
have := @HasFiniteWidePullbacks.out C _ _ J
  infer_instance

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
⊢ (exactFunctor C D).IsClosedUnderIsomorphisms

Tactic:
dsimp [exactFunctor]
  infer_instance

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
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ s.ι ≫ h = 0

Tactic:
by simp [← hfg]

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
W : C
g : W ⟶ X
h : W ⟶ Y
c : CokernelCofork h
i : IsColimit c
hf : f ≫ Cofork.π c = 0
hfg : g ≫ f = h
s : Cofork f 0
⊢ h ≫ s.π = 0

Tactic:
by simp [← hfg]

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

Goal state before:
pp: case refine_1
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
this✝ : IsLimit
  ((Cone.postcompose (Discrete.functorComp f ⇑g).inv).obj
    (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone)) :=
  hc.isLimit.ofIsoLimit (c.whiskerToCone g)
this : IsLimit (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone) :=
  (IsLimit.postcomposeHomEquiv (Discrete.functorComp f ⇑g).symm
      (Cone.whisker (Discrete.functor (Discrete.mk ∘ ⇑g)) c.toCone))
    this✝
⊢ IsLimit c.toCone

Tactic:
exact IsLimit.ofWhiskerEquivalence (Discrete.equivalence g) this

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

Goal state before:
pp: J : Type w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
f : J → C
inst✝ : HasBiproduct f
j : J
⊢ (isoProduct f).inv ≫ π f j = lift (Pi.π f) ≫ π f j

Tactic:
by simp [Iso.inv_comp_eq]

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

Goal state before:
pp: case pos
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
j : J
⊢ ι g (e j) ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g (e j) ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
      lift_π, bicone_ι_π_self_assoc]

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
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ biprod.snd ≫ biprod.inr = 𝟙 (X ⊞ Y)

Tactic:
apply CategoryTheory.Limits.biprod.hom_ext <;>
      simp only [Category.assoc, biprod.inr_snd, Category.comp_id, Category.id_comp, biprod.inr_fst,
        comp_zero]

Goal state after:
case h₀
J : Type w
C : Type uC
inst✝⁴ : Category.{uC', uC} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
hY : IsZero X
⊢ 0 = biprod.fst
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
n✝ : ℕ
f : Fin (n✝ + 1) → α✝
a : α✝
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ ∀ {a b : α (last n) × ((i : Fin n) → α i.castSucc)}, (snocEquiv α) a ≤ (snocEquiv α) b ↔ a ≤ b

Tactic:
by simp [Pi.le_def, Prod.le_def, forall_iff_castSucc]

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n a c : μ
f : ι → μ
hab : (a, s.sum f) ∈ ↑(antidiagonal n)
g : ι → μ
hcd : (c, s.sum g) ∈ ↑(antidiagonal n)
hfg : ¬s.sum f = s.sum g
hgf : (g + fun j ↦ if j = i then c else 0) = f + fun j ↦ if j = i then a else 0
⊢ s.sum f = s.sum g

Tactic:
simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm

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

Goal state before:
pp: n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map ⇑e ↑s).dedup = map (fun a ↦ count a ↑s) (↑s).dedup

Tactic:
rw [Multiset.dedup_map_of_injective e.injective]

Goal state after:
n : ℕ
σ : Type u_1
τ : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : DecidableEq τ
e : σ ≃ τ
s : Sym σ n
⊢ map (fun a ↦ count a (map ⇑e ↑s)) (map (⇑e) (↑s).dedup) = map (fun a ↦ count a ↑s) (↑s).dedup
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ ∃ a, True ∧ c.boundary.toEmbedding a = 0

Tactic:
exact ⟨0, And.intro True.intro rfl⟩

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective toFinsuppAntidiag

Tactic:
unfold toFinsuppAntidiag
  intro p q h
  rw [Finsupp.mk.injEq] at h
  obtain ⟨hfinset, hcount⟩ := h
  rw [Nat.Partition.ext_iff, Multiset.ext]
  intro m
  obtain rfl | h0 := Nat.eq_zero_or_pos m
  · grind [Multiset.count_eq_zero]
  · exact Nat.eq_of_mul_eq_mul_right h0 <| funext_iff.mp hcount m

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

Goal state before:
pp: case inl
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s✝ : Finset ι
n✝ : μ
f✝ : ι →₀ μ
s : Finset ι
n : μ
p : μ × μ
x✝¹ x✝ : ↥(s.finsuppAntidiag p.2)
f : ι →₀ μ
hf✝ : f ∈ s.finsuppAntidiag p.2
g : ι →₀ μ
hg✝ : g ∈ s.finsuppAntidiag p.2
x : ι
h : x ∉ s
hfg : ∀ (x_1 : ι), (f.update x p.1) x_1 = (g.update x p.1) x_1
hf : x ∉ f.support
hg : x ∉ g.support
⊢ f x = g x

Tactic:
rw [notMem_support_iff.mp hf, notMem_support_iff.mp hg]

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

Goal state before:
pp: α : Type u_1
f : Perm α
s : Set α
⊢ MapsTo (⇑f) s s → ∀ (n : ℕ), MapsTo (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]; exact MapsTo.iterate

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

Goal state before:
pp: α : Type u_1
f g : Perm α
h : f.Disjoint g
x : α
hg : g x = x
hf : g (f x) = f x
⊢ (f * g) x = (g * f) x

Tactic:
by
        simp [mul_apply, hf, hg]

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

Goal state before:
pp: case mpr
n : ℕ
hn : 0 < n
c : Composition n
⊢ (∃ i, n ≤ c.blocksFun i) → c = single n hn

Tactic:
· rintro ⟨i, hi⟩
    rw [eq_single_iff_length]
    have : ∀ j : Fin c.length, j = i := by
      intro j
      by_contra ji
      apply lt_irrefl (∑ k, c.blocksFun k)
      calc
        ∑ k, c.blocksFun k ≤ c.blocksFun i := by simp only [c.sum_blocksFun, hi]
        _ < ∑ k, c.blocksFun k :=
          Finset.single_lt_sum ji (Finset.mem_univ _) (Finset.mem_univ _) (c.one_le_blocksFun j)
            fun _ _ _ => zero_le
    simpa using Fintype.card_eq_one_of_forall_eq this

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

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a * s.noncommProd f ⋯).support

Tactic:
apply mt (Finset.mem_of_subset (support_mul_le _ _))

Goal state after:
case insert
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
a : α
s : Finset α
ha : a ∉ s
ih : ∀ {comm : (↑s).Pairwise (Commute on f)}, (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
comm : (↑(insert a s)).Pairwise (Commute on f)
hs : ∀ a_1 ∈ insert a s, x ∉ (f a_1).support
⊢ x ∉ (f a).support ⊔ (s.noncommProd f ⋯).support
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ (c.boundaries.orderEmbOfFin ⋯) ⟨0, ⋯⟩ = 0

Tactic:
Finset.orderEmbOfFin_zero rfl c.card_boundaries_pos

Goal state after:
n : ℕ
c : CompositionAsSet n
⊢ c.boundaries.min' ⋯ = 0
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y z : α
h : (x ≠ y ∧ x ≠ z ∧ True) ∧ y ≠ z ∧ True
⊢ {x, y, z} ⊆ (swap x y * swap y z).support

Tactic:
intro
    simp only [mem_insert, mem_singleton]
    rintro (rfl | rfl | rfl | _) <;>
      simp [swap_apply_of_ne_of_ne, h.left.left, h.left.left.symm, h.left.right.symm,
        h.left.right.left.symm, h.right.left.symm]

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

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

Tactic:
by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [← rotate_rotate, formPerm_rotate_one, hn]
    rwa [IsRotated.nodup_iff]
    exact IsRotated.forall l n

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

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
l' : List α
hl' : l'.Nodup
x : α
hl : [x].Nodup
⊢ [x].formPerm = l'.formPerm ↔ [x] ~r l' ∨ [x].length ≤ 1 ∧ l'.length ≤ 1

Tactic:
suffices l'.length ≤ 1 ↔ [x] ~r l' ∨ l'.length ≤ 1 by
      simpa [eq_comm, formPerm_eq_one_iff, hl, hl', length_eq_zero_iff, le_rfl]
    refine ⟨fun h => Or.inr h, ?_⟩
    rintro (h | h)
    · simp [← h.perm.length_eq]
    · exact h

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
by_cases h : (l.formPerm ^ n) x = x

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : (l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l

case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h : ¬(l.formPerm ^ n) x = x
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
h3 : τ.IsSwap
⊢ closure {σ, τ} = ⊤

Tactic:
obtain ⟨x, y, h4, h5⟩ := h3

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
⊢ closure {σ, τ} = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ (f ^ m) x ∈ f.support

Tactic:
pow_apply_mem_support,

Goal state after:
α : Type u_2
f g : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
hg : g.IsCycle
h : f.support ⊆ g.support
h' : ∀ x ∈ f.support, f x = g x
z : α
hz : z ∈ g.support
x : α
hx : f x ≠ x
right✝ : ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
hx' : g x ≠ x
m : ℕ
hm : (g ^ m) x = z
h'' : ∀ x ∈ f.support ∩ g.support, f x = g x
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

Tactic:
rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_eq⟩) <;>
      rw [prod_eq]

Goal state after:
case cons.inl
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)

case cons.inr
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.map (fun a ↦ prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)