mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

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
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ (mk s.fst s.snd ⋯).fst = t.fst
hr' : m✝ ≫ (mk s.fst s.snd ⋯).snd = t.snd
⊢ m✝ = hs.lift (mk t.fst t.snd ⋯)

Tactic:
apply PullbackCone.IsLimit.hom_ext hs <;>
              simp only [PullbackCone.mk_fst, PullbackCone.mk_snd] at hr hr' ⊢

Goal state after:
case h₀
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
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.fst = hs.lift (mk t.fst t.snd ⋯) ≫ s.fst

case h₁
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
t : PullbackCone x y
this : t.fst ≫ x ≫ h = t.snd ≫ y ≫ h
m✝ : t.pt ⟶ (mk s.fst s.snd ⋯).pt
hr : m✝ ≫ s.fst = t.fst
hr' : m✝ ≫ s.snd = t.snd
⊢ m✝ ≫ s.snd = hs.lift (mk t.fst t.snd ⋯) ≫ s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
rw [this]

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map g.op
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
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

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
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift F'.ofCompIso ≫ F'.m) ≫ inv g = image.lift F'.ofCompIso ≫ F'.ofCompIso.m

Tactic:
simp only [Category.assoc,
                MonoFactorisation.ofCompIso_m]

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

Tactic:
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
  apply strongEpi_comp

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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
⊢ IsLimit (F.mapCone c)

Tactic:
have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.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✝ : PreservesLimitsOfShape J F
K : J' ⥤ C
c : Cone K
t : IsLimit c
equ : e.inverse ⋙ e.functor ⋙ K ⋙ F ≅ K ⋙ F := e.invFunIdAssoc (K ⋙ F)
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ IsLimit (F.mapCone c)
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
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
this : IsIso ((Cocone.functoriality F G).map ((colimit.isColimit F).descCoconeMorphism c))
⊢ IsIso ((colimit.isColimit F).descCoconeMorphism c)

Tactic:
apply isIso_of_reflects_iso _ (Cocone.functoriality F G)

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✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
⊢ f ≫ g ≫ cokernel.π (f ≫ g) = 0

Tactic:
by rw [← Category.assoc, cokernel.condition]

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
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
this : map p = (isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv
⊢ Epi (map p)

Tactic:
rw [this]

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
f g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Epi (p j)
this : map p = (isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv
⊢ Epi ((isoCoproduct f).hom ≫ Sigma.map p ≫ (isoCoproduct g).inv)
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : j = j' → ¬x ≍ y
w : ¬j = j'
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    0

Tactic:
simp [biproduct.ι_π_ne_assoc _ w]

Goal state after:
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
⊢ F.map (biprod.lift (𝟙 X) (𝟙 X)) ≫ F.map (biprod.desc f g) = F.map f + F.map g

Tactic:
← biprod.lift_mapBiprod,

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.map (𝟙 X)) (F.map (𝟙 X)) ≫ (F.mapBiprod X X).inv) ≫ F.map (biprod.desc f g) = F.map f + F.map g
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
⊢ biproduct.fromSubtype f p ≫ biproduct.toSubtype f pᶜ = 0

Tactic:
ext j k
        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
        rw [dif_neg]
        · simp only [zero_comp]
        · exact not_not.mpr k.2

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝ : IsIso (biprod.map f g)
⊢ (biprod.inl ≫ inv (biprod.map f g) ≫ biprod.fst) ≫ f = 𝟙 Y

Tactic:
have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.inv_hom_id (biprod.map f g))
        simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t
        simp only [Category.assoc]
        simp [t]

Goal state after:
Module: Mathlib.Order.Fin.Tuple

Goal state before:
pp: case refine_4
α : Type u_1
inst✝ : Preorder α
n : ℕ
q : Fin (n + 1)
x : α
f : Fin n → α
⊢ (StrictMono f ∧ (∀ (i : Fin n), i.castSucc < q → f i < x) ∧ ∀ (i : Fin n), q ≤ i.castSucc → x < f i) →
    StrictMono (q.insertNth x f)

Tactic:
rintro ⟨h, hlt, hgt⟩ a b hab
    cases a using succAboveCases q <;> cases b using succAboveCases q
    · simp at hab
    · rename_i j
      have : q ≤ j.castSucc := by simpa [lt_succAbove_iff_le_castSucc] using hab
      simpa using hgt _ this
    · rename_i j
      have : j.castSucc < q := by simpa [succAbove_lt_iff_castSucc_lt] using hab
      simpa using hlt _ this
    · simpa using h <| (strictMono_succAbove _).lt_iff_lt.mp hab

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
⊢ Finset (ι → μ)

Tactic:
refine (Fintype.truncEquivFinOfCardEq <| Fintype.card_coe s).lift
    (fun e ↦ (finAntidiagonal s.card n).map ⟨fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, ?_⟩)
    fun e₁ e₂ ↦ ?_

Goal state after:
case refine_1
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e : ↥s ≃ Fin #s
⊢ Injective fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0

case refine_2
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
n✝ : μ
s : Finset ι
n : μ
e₁ e₂ : ↥s ≃ Fin #s
⊢ map { toFun := fun f i ↦ if hi : i ∈ s then f (e₁ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n) =
    map { toFun := fun f i ↦ if hi : i ∈ s then f (e₂ ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n)
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
ha : ∃ a_1 ∈ antidiagonal n, Prod.map Nat.succ id a_1 = a
x : Fin (k + 1) → ℕ
hx₁ : ∃ a ∈ antidiagonalTuple k (0, n + 1).2, Fin.cons (0, n + 1).1 a = x
hx₂ : ∃ a_1 ∈ antidiagonalTuple k a.2, Fin.cons a.1 a_1 = x
⊢ False

Tactic:
obtain ⟨⟨a, -, rfl⟩, ⟨x₁, -, rfl⟩, ⟨x₂, -, h⟩⟩ := ha, hx₁, hx₂

Goal state after:
case succ.right.succ.refine_1
k : ℕ
ih : ∀ (n : ℕ), (antidiagonalTuple k n).Nodup
n : ℕ
n_ih :
  Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2)) (antidiagonal n)
a : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).1 x₂ = Fin.cons (0, n + 1).1 x₁
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
c : Composition 0
⊢ c.blocks = []

Tactic:
← length_eq_zero_iff,

Goal state after:
case mpr
c : Composition 0
⊢ c.blocks.length = 0
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ (g.update a n1) a + ∑ x ∈ s, (g.update a n1) x = n1 + s.sum ⇑g ∧ (g.update a n1).support ⊆ insert a s

Tactic:
refine ⟨?_, (support_update_subset _ _).trans (insert_subset_insert a hgsupp)⟩

Goal state after:
case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n1 : μ
g : ι →₀ μ
hgsupp : g.support ⊆ s
⊢ (g.update a n1) a + ∑ x ∈ s, (g.update a n1) x = n1 + s.sum ⇑g
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p.parts = q.parts

Tactic:
Multiset.ext

Goal state after:
n : ℕ
p q : n.Partition
hfinset : p.parts.toFinset = q.parts.toFinset
hcount : (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ ∀ (a : ℕ), count a p.parts = count a q.parts
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

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

Tactic:
rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
σ τ : Type
inst✝³ : Finite τ
S : σ → C
inst✝² : HasBiproduct S
T : τ → C
inst✝¹ : HasBiproduct T
s : σ
f : ⨁ S ⟶ ⨁ T
inst✝ : IsIso f
val✝ : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ biproduct.ι S s ≫ f ≫ (∑ j, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp.inr.inl
n✝ n : ℕ
c : CompositionAsSet n
⊢ Fin.last n ∈ c.boundaries

pp: case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries

Tactic:
· exact c.getLast_mem

Goal state after:
case mp.inr.inr
n✝ n : ℕ
c : CompositionAsSet n
i : Fin n.succ
j : Fin (n - 1)
hj1 : ⟨↑j + 1, ⋯⟩ ∈ c.boundaries
hj2 : ↑i = ↑j + 1
⊢ i ∈ c.boundaries
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n✝ n : ℕ
s : Finset (Fin (n - 1))
i : Fin (n - 1)
this : ↑i + 1 ≠ n
⊢ i ∈
      (fun c ↦ {i | ⟨1 + ↑i, ⋯⟩ ∈ c.boundaries}.toFinset)
        ((fun s ↦
            { boundaries := {i | i = 0 ∨ i = Fin.last n ∨ ∃ j, ∃ (_ : j ∈ s), ↑i = ↑j + 1}.toFinset, zero_mem := ⋯,
              getLast_mem := ⋯ })
          s) ↔
    i ∈ s

Tactic:
simp_rw [add_comm, Fin.ext_iff, Fin.val_zero, Fin.val_last, exists_prop, Set.toFinset_ofPred,
      Finset.mem_filter_univ, reduceCtorEq, this, false_or, add_left_inj, ← Fin.ext_iff,
      exists_eq_right']

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

Goal state before:
pp: α : Type u
f : Perm α
p : α → Prop
inst✝ : Finite { x // p x }
h : ∀ (x : α), p x → p (f x)
x : α
hx : p x
⊢ p ((Equiv.symm f) x)

Tactic:
have : Finite { x | p x } := by simpa
  simpa using perm_symm_mapsTo_of_mapsTo (s := {x | p x}) f h hx

Goal state after:
Module: Mathlib.Data.Fintype.Perm

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

Tactic:
rw [this]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : Equiv.Perm α
h : f ∈ permsOfList []
heq_iff_eq : α
this : f = 1
⊢ 1 heq_iff_eq ≠ heq_iff_eq → heq_iff_eq ∈ []
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
by_cases pb : p b

Goal state after:
case pos
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

Goal state after:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

Tactic:
by_cases pb : p b

Goal state after:
case pos
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b

case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b ∨ (τ.extendDomain f) b = b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case neg
α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
b : β
pb : ¬p b
⊢ (σ.extendDomain f) b = b

Tactic:
rw [extendDomain_apply_not_subtype _ _ pb]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ ↑u * ↑u = 1

Tactic:
← Units.val_mul,

Goal state after:
u : ℤˣ
⊢ ↑(u * u) = 1
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
n : ℕ
| u ^ (n % 2 + 2 * (n / 2))

Tactic:
pow_add,

Goal state after:
u : ℤˣ
n : ℕ
| u ^ (n % 2) * u ^ (2 * (n / 2))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: case intro.refine_2.inl
α : 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
⊢ ↑((Set.union hd2'').symm
        (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨(σ * τ) x, ⋯⟩, ?intro.refine_2.inl.ha✝⟩))) =
    (f * σ * f⁻¹ * (g * τ * g⁻¹))
      ↑((Set.union hd2'').symm
          (Sum.map (⇑(subtypeEquiv f ⋯)) (⇑(subtypeEquiv g ⋯)) (Sum.inl ⟨↑⟨x, ⋯⟩, ?intro.refine_2.inl.ha⟩)))

Tactic:
simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
        Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv]
      have h := (hd2 (f x)).resolve_left ?_
      · rw [mul_apply, mul_apply, coe_inv] at h
        rw [h, symm_apply_apply, (hd1 x).resolve_left hxσ]
      · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply, apply_eq_iff_eq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ 1 < l.length ↔ 2 ≤ l.length

Tactic:
exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

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

Goal state before:
pp: case inr.inr.inr
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ⟨a₁, a₂⟩ ∉ {⟨1, 0⟩}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : (swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if (swap 0 1) a₁ ≤ (swap 0 1) a₂ then -1 else 1) = 1

Tactic:
rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt),
          swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'), if_neg ha₁.not_ge]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | (l.formPerm ^ n) x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l

Tactic:
replace h := set_support_zpow_subset _ _ h

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
hx : x ∈ l
n : ℤ
h✝ : ¬(l.formPerm ^ n) x = x
h : (l.formPerm ^ n) x ∈ {x | l.formPerm x ≠ x}
⊢ (l.formPerm ^ n) x ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case left
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
⊢ Injective fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩

Tactic:
rintro ⟨a, m, rfl⟩ ⟨b, n, rfl⟩ h

Goal state after:
case left
ι : Type u_1
α : Type u_2
β : Type u_3
f g : Perm α
x y : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
hσ : σ.IsCycle
m n : ℤ
h :
  (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) m, ⋯⟩ =
    (fun τ ↦ ⟨↑τ (Classical.choose hσ), ⋯⟩) ⟨(fun x ↦ σ ^ x) n, ⋯⟩
⊢ ⟨(fun x ↦ σ ^ x) m, ⋯⟩ = ⟨(fun x ↦ σ ^ x) n, ⋯⟩
Module: Mathlib.Data.List.Iterate

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

Tactic:
← length_eq_zero_iff,

Goal state after:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ (iterate f a n).length = 0 ↔ n = 0
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf (f ^ n) = orderOf f
⊢ n.Coprime (orderOf f)

Tactic:
orderOf_pow,

Goal state after:
case intro.mp
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
n : ℕ
val✝ : Fintype β
h : (f ^ n).IsCycle
hr : (f ^ n).support = f.support
this : orderOf f / (orderOf f).gcd n = orderOf f
⊢ n.Coprime (orderOf f)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
this : f ^ b = f ^ a
⊢ f ^ a = f ^ b

Tactic:
rw [this]

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

Goal state before:
pp: α : Type u_2
f : Perm α
s : Set α
hf : f.IsCycleOn s
⊢ s ×ˢ s = ⋃ n, (fun a ↦ (a, (f ^ n) a)) '' s

Tactic:
ext ⟨a, b⟩
  simp only [Set.mem_prod, Set.mem_iUnion, Set.mem_image]
  refine ⟨fun hx => ?_, ?_⟩
  · obtain ⟨n, rfl⟩ := hf.2 hx.1 hx.2
    exact ⟨_, _, hx.1, rfl⟩
  · rintro ⟨n, a, ha, ⟨⟩⟩
    exact ⟨ha, (hf.1.perm_zpow _).mapsTo ha⟩

Goal state after: