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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
s : PullbackCone f g
⊢ s.fst ≫ (pullbackConeOfRightIso f g).fst = s.fst ∧
    s.fst ≫ (pullbackConeOfRightIso f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfRightIso f g).pt},
        m ≫ (pullbackConeOfRightIso f g).fst = s.fst → m ≫ (pullbackConeOfRightIso f g).snd = s.snd → m = s.fst

Tactic:
by simp [s.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
F : D ⥤ C
inst✝² : F.IsEquivalence
inst✝¹ : W₁.RespectsIso
inst✝ : W₂.RespectsIso
X Y : D
f : X ⟶ Y
h : W₁.MapFactorizationData W₂ (F.map f)
⊢ W₂.inverseImage F (F.preimage ((F.objObjPreimageIso h.Z).hom ≫ h.p))

Tactic:
refine (W₂.arrow_mk_iso_iff ?_).1 h.hp
    refine Arrow.isoMk (F.objObjPreimageIso h.Z).symm (Iso.refl _) ?_
    simp [F.map_preimage]

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : X ⟶ W
inst✝ : Epi h
x : W ⟶ Y
y : W ⟶ Z
hhx : h ≫ x = f
hhy : h ≫ y = g
s : PushoutCocone f g
hs : IsColimit s
t : PushoutCocone x y
m✝ : (mk s.inl s.inr ⋯).pt ⟶ t.pt
hr : s.inl ≫ m✝ = t.inl
hr' : s.inr ≫ m✝ = t.inr
⊢ s.inr ≫ hs.desc (mk t.inl t.inr ⋯) = t.inr

Tactic:
exact hs.fac _ WalkingSpan.right

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
⊢ 0 ≫ η = 0

Tactic:
ext X; dsimp; apply zero_comp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ Fork.ι c ≫ (f - g) = 0

Tactic:
c.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ f = c.ι ≫ g

Tactic:
c.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.ι ≫ g = c.ι ≫ g
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ (f - g) ≫ Cofork.π c = 0

Tactic:
c.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ f ≫ c.π = g ≫ c.π

Tactic:
c.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ g ≫ c.π = g ≫ 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✝
X Y : C
f : X ⟶ Y
hf : f = 0
⊢ 𝟙 X ≫ f = 0

Tactic:
hf,

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

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

Tactic:
hf,

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝² : HasCokernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasCokernel f
inst✝ : IsIso g
⊢ (f ≫ g) ≫ cokernel.π (f ≫ g) = 0

Tactic:
cokernel.condition

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
⊢ autoParam (∀ {X Y : C} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g) Additive.map_add._autoParam

Tactic:
intro X Y f g

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
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
G : C ⥤ D
e : F ≅ G
X Y : C
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.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✝ : Fintype J
f : J → C
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
⊢ m = ∑ j, s.π.app { as := j } ≫ b.ι j

Tactic:
by
        rw [← Category.comp_id m]
        dsimp
        rw [← total, comp_sum]
        apply Finset.sum_congr rfl
        intro j _
        have reassoced : m ≫ Bicone.π b j ≫ Bicone.ι b j = s.π.app ⟨j⟩ ≫ Bicone.ι b j := by
          simpa using eq_whisker (h ⟨j⟩) _
        rw [reassoced]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Cocone (Discrete.functor f)
ht : IsColimit t
⊢ ∀ (j : Discrete J), t.ι.app j ≫ (Iso.refl t.pt).hom = (Bicone.ofColimitCocone ht).toCocone.ι.app j

Tactic:
by
    simp

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

Goal state before:
pp: n : ℕ
f : Fin n → Fin (n + 1)
h : f = succ
⊢ StrictMono (cons 0 f)

Tactic:
by simp [h, strictMono_id]

Goal state after:
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 : ℕ × ℕ
x₁ x₂ : Fin k → ℕ
h : Fin.cons (Prod.map Nat.succ id a).1 x₂ = Fin.cons (0, n + 1).1 x₁
⊢ False

Tactic:
rw [Fin.cons_inj] at h

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 : (Prod.map Nat.succ id a).1 = (0, n + 1).1 ∧ x₂ = x₁
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ (filter (fun x ↦ x ≠ 0) l).sum = n

Tactic:
have lz : (l.filter (· = 0)).sum = 0 := by simp [sum_eq_zero_iff]
    rwa [← filter_add_not (· = 0) l, sum_add, lz, zero_add] at hl

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

Goal state before:
pp: case mpr
ι : 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 : ι →₀ μ'
⊢ f ∈ s.finsuppAntidiag (e n) → f ∈ map (mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n)

Tactic:
set h := (mapRange.addEquiv e).toEquiv with hh

Goal state after:
case mpr
ι : 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
⊢ f ∈ s.finsuppAntidiag (e n) → f ∈ map h.toEmbedding (s.finsuppAntidiag n)
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
h : ∀ (x : α), (ofSubtype (g.subtypePerm hg)) x = c x
hc'✝ : ∀ (x : α), c x ∈ s ↔ x ∈ s
a : α
ha : a ∈ s
⊢ c a = g a

Tactic:
rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f g : α → β
hf : Function.Injective f
hg : Function.Injective g
⊢ ∃ σ, ∀ (a : α), σ (f a) = g a

Tactic:
classical
  have : Finite {x | x ∈ Set.range f} := .of_surjective _ (Set.codRestrict_range_surjective f)
  refine ⟨((Equiv.ofInjective f hf).symm.trans (Equiv.ofInjective g hg)).extendSubtype, ?_⟩
  simp [Equiv.extendSubtype_apply_of_mem]

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

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

Tactic:
intro s
    ext i
    have : (i : ℕ) + 1 ≠ n := by lia
    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.Combinatorics.Enumerative.Composition

Goal state before:
pp: case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ (take i c.blocks).sum + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
IH B

Goal state after:
case succ
n : ℕ
c : CompositionAsSet n
i : ℕ
IH : ∀ (h : i < c.boundaries.card), (take i c.blocks).sum = ↑(c.boundary ⟨i, h⟩)
h : i + 1 < c.boundaries.card
A : i < c.blocks.length
B : i < c.boundaries.card
⊢ ↑(c.boundary ⟨i, B⟩) + c.blocks[i] = ↑(c.boundary ⟨i + 1, h⟩)
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ (take i d.blocks).sum = (take i c.blocks).sum

Tactic:
d.blocks_partial_sum i_lt,

Goal state after:
n : ℕ
c : Composition n
d : CompositionAsSet n := c.toCompositionAsSet
length_eq : d.blocks.length = c.blocks.length
i : ℕ
hi : i ≤ d.blocks.length
i_lt : i < d.boundaries.card
i_lt' : i < c.boundaries.card
i_lt'' : i < c.length + 1
A : (d.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt⟩ = (c.boundaries.orderEmbOfFin ⋯) ⟨i, i_lt''⟩
B : c.sizeUpTo i = ↑(c.boundary ⟨i, i_lt''⟩)
⊢ ↑(d.boundary ⟨i, i_lt⟩) = (take i c.blocks).sum
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ 1 [x][n + 1] = [x][n + 1 + 1]

Tactic:
getElem_singleton,

Goal state after:
case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ 1 x = [x][n + 1 + 1]
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ 1 x = [x][n + 1 + 1]

Tactic:
getElem_singleton,

Goal state after:
case succ.cons.nil
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x : α
h : [x].Nodup
hn : n + 1 + 1 < [x].length
⊢ 1 x = x
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]

Tactic:
specialize IH (y :: l) h.of_cons _

Goal state after:
case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
⊢ n + 1 < (y :: l).length

case succ.cons.cons
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
IH✝ : ∀ (xs : List α), xs.Nodup → ∀ (hn : n + 1 < xs.length), xs.formPerm xs[n] = xs[n + 1]
x y : α
l : List α
h : (x :: y :: l).Nodup
hn : n + 1 + 1 < (x :: y :: l).length
IH : (y :: l).formPerm (y :: l)[n] = (y :: l)[n + 1]
⊢ (x :: y :: l).formPerm (x :: y :: l)[n + 1] = (x :: y :: l)[n + 1 + 1]
Module: Mathlib.GroupTheory.Perm.Support

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

Tactic:
have ha' := (key (f a)).mp (mt f.apply_eq_iff_eq.mp ha)
      obtain rfl | rfl := (key a).mp ha
      · rw [Or.resolve_left ha' ha, swap_apply_left]
      · rw [Or.resolve_right ha' ha, swap_apply_right]

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

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

Tactic:
units_sq,

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

Goal state before:
pp: case h.h.succ.e_i
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
IH :
  ∀ (hk : k < ((x :: y :: l).rotate n).length) (hk' : k < (x' :: y' :: l').length),
    (x :: y :: l)[(k + n) % (x :: y :: l).length] = (x' :: y' :: l')[k]
hk : k + 1 < ((x :: y :: l).rotate n).length
hk' : k + 1 < (x' :: y' :: l').length
⊢ (k + n + 1) % (x' :: y' :: l').length = ((k + n) % (x' :: y' :: l').length + 1) % (x' :: y' :: l').length

Tactic:
apply Nat.add_mod

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

Tactic:
rcases (Nat.le_of_lt_succ hk).eq_or_lt with hk' | hk'

Goal state after:
case succ.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k = n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1

case succ.inr
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk✝ : k < l.length
hx : l[k] ∈ l
n✝ : ℕ
hk : k < n✝ + 1
hn : l.length = n✝ + 1
hk' : k < n✝
⊢ (k + 1) % (n✝ + 1) = k ↔ n✝ + 1 ≤ 1
Module: Mathlib.GroupTheory.Perm.List

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

Tactic:
by
  rw [Ne, formPerm_apply_mem_eq_self_iff _ hl x hx, not_le]
  exact ⟨Nat.succ_le_of_lt, Nat.lt_of_succ_le⟩

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
⊢ False

Tactic:
refine hf.ne_one ?_

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 = 1
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : (insert i s).noncommProd f comm = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1

Goal state after:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ (List.map (⇑sign ∘ fun a ↦ prodExtendRight a (σ a)) l).prod = (List.map (fun k ↦ sign (σ k)) l).prod

Tactic:
← fun a => sign_prodExtendRight a (σ a),

Goal state after:
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ (List.map (⇑sign ∘ fun a ↦ prodExtendRight a (σ a)) l).prod =
    (List.map (fun k ↦ sign (prodExtendRight k (σ k))) l).prod
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case unit
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j ↦ ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
m : M
comm : ∀ (i : ι) (x : N i), Commute m ((ϕ i) x)
h : (i : ι) → N i
⊢ Commute m 1

Tactic:
exact Commute.one_right _

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
⊢ Multiset.count n σ.cycleType = Fintype.card { c // #(↑c).support = n }

Tactic:
rw [cycleType, Multiset.count_eq_card_filter_eq]
  -- rewrite the `Fintype.card` as a `Finset.card`
  rw [Fintype.subtype_card, Finset.univ_eq_attach, Finset.filter_attach',
    Finset.card_map, Finset.card_attach]
  simp only [Function.comp_apply, Finset.card, Finset.filter_val,
    Multiset.filter_map, Multiset.card_map]
  congr 1
  apply Multiset.filter_congr
  intro d h
  simp only [eq_comm, Finset.mem_val.mp h, exists_const]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h✝ : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
y : α
hy : ((g.cycleOf x)⁻¹ * g) y ≠ y
h : g y = y
⊢ False

Tactic:
by
                rw [mul_apply, h, Ne, inv_eq_iff_eq, cycleOf_apply] at hy
                split_ifs at hy <;> tauto

Goal state after:
Module: Mathlib.Data.FunLike.Module

Goal state before:
pp: M : Type u_1
F : Type u_3
α : Type u_4
β : Type u_5
i : FunLike F α β
inst✝⁶ : SMul M F
inst✝⁵ : SMul Mᵐᵒᵖ F
inst✝⁴ : SMul M β
inst✝³ : SMul Mᵐᵒᵖ β
inst✝² : IsCentralScalar M β
inst✝¹ : IsSMulApply M F α β
inst✝ : IsSMulApply Mᵐᵒᵖ F α β
a : M
b : F
⊢ MulOpposite.op a • b = a • b

Tactic:
apply DFunLike.ext; simp [op_smul_eq_smul]

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : ¬i = j
hj1 : ↑(i + 1) = ↑i + 1
⊢ ↑(i.castLT ⋯) + 1 < ↑j + 1

Tactic:
by simp; lia

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

Goal state before:
pp: case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ False

Tactic:
refine hg'y <| (disjoint_prod_right _ this y).resolve_right ?_

Goal state after:
case refine_3
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l✝¹ : List α
f : Perm α
h : ∀ {x : α}, f x ≠ x → x ∈ l✝¹
l✝ : List α
g : Perm α
hfg : ∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x
x : α
l : List α
hg : ∀ {x_1 : α}, g x_1 ≠ x_1 → x_1 ∈ x :: l
hx : ¬g x = x
m : List (Perm α)
hm₁ : m.prod = (g.cycleOf x)⁻¹ * g
hm₂ : ∀ g' ∈ m, g'.IsCycle
hm₃ : List.Pairwise Disjoint m
g' : Perm α
hg' : g' ∈ m
y : α
hgy : (g.cycleOf x) y ≠ y
hg'y : g' y ≠ y
hxy : g.SameCycle x y
hg'm : g' :: m.erase g' ~ m
this : ∀ h ∈ m.erase g', g'.Disjoint h
⊢ ¬(m.erase g').prod y = y
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
by simp; lia

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

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))))

Tactic:
by simp; lia

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ n ∈ σ.cycleType → ∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n

pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType

Tactic:
· intro h
    obtain ⟨l, rfl, hlc, hld⟩ := truncCycleFactors σ
    rw [cycleType_eq _ rfl hlc hld, Multiset.mem_coe, List.mem_map] at h
    obtain ⟨c, cl, rfl⟩ := h
    rw [(List.perm_cons_erase cl).pairwise_iff symm] at hld
    refine ⟨c, (l.erase c).prod, ?_, ?_, hlc _ cl, rfl⟩
    · rw [← List.prod_cons, (List.perm_cons_erase cl).symm.prod_eq' (hld.imp Disjoint.commute)]
    · exact disjoint_prod_right _ fun g => List.rel_of_pairwise_cons hld

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
σ : Perm α
⊢ (∃ c τ, σ = c * τ ∧ c.Disjoint τ ∧ c.IsCycle ∧ #c.support = n) → n ∈ σ.cycleType
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
⊢ ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i)))) = ↑k

Tactic:
by simp; lia

Goal state after: