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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ (l ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom

Tactic:
congrArg (· ≫ g.hom) a,

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ (m ≫ Hom.left k) ≫ g.hom = m ≫ Hom.left k ≫ g.hom
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
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
e : E
f : StructuredArrow e G
X✝ Y✝ : StructuredArrow f (pre e F G)
φ : X✝ ⟶ Y✝
⊢ (mk (Hom.right X✝.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) =
    (mk (Hom.right (X✝.hom ≫ (pre e F G).map (Hom.right φ)))).hom

Tactic:
comp_right

Goal state after:
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 : C ⥤ D
G : D ⥤ E
e : E
f : StructuredArrow e G
X✝ Y✝ : StructuredArrow f (pre e F G)
φ : X✝ ⟶ Y✝
⊢ (mk (Hom.right X✝.hom)).hom ≫ F.map (Hom.right (Hom.right φ)) =
    (mk (Hom.right X✝.hom ≫ Hom.right ((pre e F G).map (Hom.right φ)))).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Goal state before:
pp: case unique_from.refine_2
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
f : G ⟶ F
x✝ : C
⊢ f.app x✝ = default.app x✝

Tactic:
apply (hF _).eq_of_tgt _ _

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
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
⊢ IsZero X

Tactic:
obtain rfl := i.eq_zero_of_tgt f
  exact IsZero.of_mono_zero X Y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
⊢ 0 ≫ 0 = 𝟙 0

Tactic:
rw [id_zero, comp_zero]

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
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((limit.isLimit F).lift c)
⊢ IsLimit c

Tactic:
by
      apply IsLimit.ofPointIso (limit.isLimit F)

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✝² : HasKernel f✝
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : HasKernel g
s : KernelFork (f ≫ g)
m : ?m.112 s ⟶ kernel (?m.117 s)
w : m ≫ Fork.ι (KernelFork.ofι (kernel.ι g ≫ inv f) ⋯) = Fork.ι s
⊢ m = kernel.lift g (Fork.ι s ≫ f) ⋯

Tactic:
by
          simp_rw [← w]
          apply equalizer.hom_ext
          simp

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (piComparison G f)

Tactic:
rw [← PreservesProduct.iso_hom]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝² : HasProduct f
inst✝¹ : HasProduct fun j ↦ G.obj (f j)
inst✝ : PreservesLimit (Discrete.functor f) G
⊢ IsIso (PreservesProduct.iso G f).hom
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
f : X ⟶ Y
inst✝ : IsSplitMono f
c : CokernelCofork f
i : IsColimit c
this : Epi (Cofork.π c) := ⋯
⊢ 𝟙 Y ≫ retraction f = retraction f

Tactic:
apply Category.id_comp

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:
simp [h, strictMono_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
⊢ False

Tactic:
set x := biprod.inl ≫ f ≫ inv f ≫ biprod.fst

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
W X Y Z : C
f : W ⊞ X ⟶ Y ⊞ Z
inst✝ : IsIso f
nz : 𝟙 W ≠ 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ False
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:
by
  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₂ ↦ ?_
  · rw [Injective]
    rintro f g hfg
    ext i
    simpa using congr_fun hfg (e.symm i)
  · ext f
    simp only [mem_map, mem_finAntidiagonal]
    refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_
    have := Fintype.sum_equiv (e₂.symm.trans e₁) _ g fun _ ↦ rfl
    simp_all

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

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a✝ : ι → μ
⊢ a✝ ∈ ∅.piAntidiag 0 ↔ a✝ ∈ {0}

Tactic:
simp [funext_iff]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: n : ℕ
⊢ antidiagonalTuple 2 n = map (fun i ↦ ![i.1, i.2]) (antidiagonal n)

Tactic:
rw [antidiagonalTuple]
  simp_rw [antidiagonalTuple_one, List.map_singleton]
  rw [List.map_eq_flatMap]
  rfl

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:
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.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 ≫ 𝟙 (⨁ T) ≫ inv f ≫ biproduct.π S s = 0

Tactic:
← 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.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f g h : Perm α
x✝ : α
⊢ (h * f * h⁻¹) x✝ = x✝ ∨ (h * g * h⁻¹) x✝ = x✝ ↔ f (h⁻¹ x✝) = h⁻¹ x✝ ∨ g (h⁻¹ x✝) = h⁻¹ x✝

Tactic:
simp only [mul_apply, eq_inv_iff_eq]

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

Goal state before:
pp: n : ℕ
h : 0 < n
i : Fin (single n h).length
⊢ (single n h).blocksFun i = n

Tactic:
simp [blocksFun, single]

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

Goal state before:
pp: α : Type u_1
l : List α
ns : List ℕ
⊢ (l.splitWrtCompositionAux ns).length = ns.length

Tactic:
by
    induction ns generalizing l
    · simp [splitWrtCompositionAux, *]
    · simp [*]

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

Goal state before:
pp: case cons
α : Type u_1
n : ℕ
ns : List ℕ
IH : ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l
⊢ ∀ {l : List α}, (n :: ns).sum = l.length → (l.splitWrtCompositionAux (n :: ns)).flatten = l

Tactic:
intro l h; rw [sum_cons] at h
    simp only [splitWrtCompositionAux_cons]; dsimp
    rw [IH]
    · simp
    · rw [length_drop, ← h, add_tsub_cancel_left]

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

Goal state before:
pp: n : ℕ
c : CompositionAsSet n
⊢ c.boundary ⟨0, ⋯⟩ = 0

Tactic:
rw [boundary, 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: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ #(f * g).support = #(f.support ∪ g.support)

pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support

Tactic:
· congr
    ext
    simp [h.support_mul]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
⊢ _root_.Disjoint f.support g.support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
f : Perm α
h : ∀ (x : α), f x ∈ s ↔ x ∈ s
⊢ (f.subtypePerm h).support = {x | f ↑x ≠ ↑x}

Tactic:
by
  ext; simp [Subtype.ext_iff]

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

Goal state before:
pp: case h.h.zero
α : 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
hk : 0 < ((x :: y :: l).rotate n).length
hk' : 0 < (x' :: y' :: l').length
⊢ (x :: y :: l)[(0 + n) % (x :: y :: l).length] = (x' :: y' :: l')[0]

Tactic:
refine Eq.trans ?_ hx'
      congr
      simpa using hn

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

Goal state before:
pp: case neg
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩.snd < ⟨a, b⟩.fst
hg : ¬g b < g a
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1

Tactic:
obtain hf | hf := (f.injective.ne <| g.injective.ne hab.ne).lt_or_gt <;>
    simp_all [le_of_lt, not_le_of_gt, not_lt_of_ge]

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

Goal state before:
pp: case succ.inl
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x = b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

pp: case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b

Tactic:
· exact ⟨0, hfbx⟩

Goal state after:
case succ.inr
α : Type u_4
inst✝ : DecidableEq α
n : ℕ
hn : ∀ {b x : α} {f : Perm α}, (swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
b x : α
f : Perm α
hb : (swap x (f x) * f) b ≠ b
h : (f ^ (n + 1)) (f x) = b
hfbx : f x ≠ b
⊢ ∃ i, ((swap x (f x) * f) ^ i) (f x) = b
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ _root_.Disjoint H K

Tactic:
disjoint_iff_inf_le

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
H K : Subgroup (Perm α)
h : ∀ a ∈ H, ∀ b ∈ K, _root_.Disjoint a.support b.support
⊢ H ⊓ K ≤ ⊥
Module: Mathlib.GroupTheory.Perm.Closure

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
σ : Perm α
h0 : n.Coprime (orderOf σ)
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
m : ℕ
hm : (σ ^ n) ^ m = σ
h2' : (σ ^ n).support = univ
⊢ ((σ ^ n) ^ ↑m).IsCycle

Tactic:
rwa [← hm] at h1

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

Goal state before:
pp: case neg
α : Type u_2
f : Perm α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hf : f.IsCycle
n : ℕ
x : α
hx : x ∈ f.support
H : x ∉ (f ^ n).support
z : α
hz : ¬f z = z
⊢ (f ^ n) z = 1 z

Tactic:
· obtain ⟨k, rfl⟩ := hf.exists_pow_eq hz (mem_support.mp hx)
      apply (f ^ k).injective
      rw [← mul_apply, (Commute.pow_pow_self _ _ _).eq, mul_apply]
      simpa using H

Goal state after:
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 β
⊢ (f ^ n).IsCycle → n.Coprime (orderOf f)

Tactic:
intro h
      have hr : support (f ^ n) = support f := by
        rw [hf.support_pow_eq_iff]
        rintro ⟨k, rfl⟩
        refine h.ne_one ?_
        simp [pow_mul, pow_orderOf_eq_one]
      have : orderOf (f ^ n) = orderOf f := by rw [h.orderOf, hr, hf.orderOf]
      rw [orderOf_pow, Nat.div_eq_self] at this
      rcases this with h | _
      · exact absurd h (orderOf_pos _).ne'
      · rwa [Nat.coprime_iff_gcd_eq_one, Nat.gcd_comm]

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: 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 ((noncommPiCoprod ϕ hcomm) h)

Tactic:
by
  dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]
  apply Finset.noncommProd_induction
  · exact fun x y ↦ Commute.mul_right
  · exact Commute.one_right _
  · exact fun x _ ↦ comm x (h x)

Goal state after:
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
⊢ Disjoint ((fun i ↦ (ϕ i).range) i) (⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j)

Tactic:
disjoint_iff_inf_le

Goal state after:
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : Pairwise fun i j ↦ ∀ (x : H i) (y : H j), Commute ((ϕ i) x) ((ϕ j) y)
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : Pairwise fun i j ↦ (Fintype.card (H i)).Coprime (Fintype.card (H j))
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
i : ι
⊢ (fun i ↦ (ϕ i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (ϕ i).range) j ≤ ⊥
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
s : Finset ι
hs : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)
⊢ (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType

Tactic:
by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi hrec =>
    have hs' : (s : Set ι).Pairwise fun i j ↦ Disjoint (k i) (k j) :=
      hs.mono (by simp only [Finset.coe_insert, Set.subset_insert])
    rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hi, Finset.sum_insert hi]
    rw [Disjoint.cycleType_mul, hrec hs']
    apply disjoint_noncommProd_right
    intro j hj
    apply hs _ _ (ne_of_mem_of_not_mem hj hi).symm <;>
      simp only [Finset.coe_insert, Set.mem_insert_iff, Finset.mem_coe, hj, or_true, true_or]

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

Goal state before:
pp: n : ℕ
⊢ {(finRotate (n + 2)).support.card} = {n + 2}

Tactic:
support_finRotate,

Goal state after:
n : ℕ
⊢ {Finset.univ.card} = {n + 2}
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
h : i < j
⊢ i.cycleRange j = j

Tactic:
rw [cycleRange, Perm.extendDomain_apply_not_subtype]

Goal state after:
case h
n : ℕ
i j : Fin n
h : i < j
⊢ j ∉ Set.range ⇑(castLEEmb ⋯)
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : ¬p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
⊢ ∃ a, σ a = a

Tactic:
classical
    contrapose! hα
    simp_rw [← mem_support, ← Finset.eq_univ_iff_forall] at hα
    exact Nat.modEq_zero_iff_dvd.1 ((congr_arg _ (Finset.card_eq_zero.2 (compl_eq_bot.2 hα))).mp
      (card_compl_support_modEq hσ).symm)

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

Goal state before:
pp: case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 : Perm α
h1 h2 : g1 ∈ f.cycleFactorsFinset
⊢ Commute g1 g1

pp: case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Tactic:
· apply Commute.refl

Goal state after:
case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.cycleType = τ.cycleType
⊢ σ.partition = τ.partition

pp: case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType

Tactic:
· rw [Nat.Partition.ext_iff, parts_partition, parts_partition, ← sum_cycleType, ← sum_cycleType,
      h]

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : σ.partition = τ.partition
⊢ σ.cycleType = τ.cycleType
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ Perm.sign σ = 1

Tactic:
Equiv.Perm.sign_of_cycleType,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ (-1) ^ (σ.cycleType.sum + σ.cycleType.card) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
⊢ {a, g a, g (g a)} ⊆ g.support

Tactic:
apply Finset.insert_subset ha
      apply Finset.insert_subset
      · rwa [Perm.apply_mem_support]
      simpa only [Finset.singleton_subset_iff, Perm.apply_mem_support]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.zero_add
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y x : Prequotient F
⊢ 0 + descFunLift F s x = descFunLift F s x

Tactic:
rw [zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
p : n → n
H : ¬Bijective p
i j : n
hpij : p i = p j
hij : i ≠ j
σ : Perm n
x✝ : σ ∈ univ
⊢ ∀ (x : n), M (σ x) (p x) = M ((σ * Equiv.swap i j) ((Equiv.swap i j) x)) (p ((Equiv.swap i j) x))

Tactic:
simp [apply_swap_eq_self hpij]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ Nonempty (Cocone F)

Tactic:
refine ⟨⟨Z, ⟨fun X => f (by simp [O]), ?_⟩⟩⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : IsFiltered C
J : Type w
inst✝¹ : SmallCategory J
inst✝ : FinCategory J
F : J ⥤ C
O : Finset C := Finset.image F.obj Finset.univ
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) :=
  Finset.univ.biUnion fun X ↦
    Finset.univ.biUnion fun Y ↦ Finset.image (fun f ↦ ⟨F.obj X, ⟨F.obj Y, ⟨⋯, ⟨⋯, F.map f⟩⟩⟩⟩) Finset.univ
Z : C
f : {X : C} → X ∈ O → (X ⟶ Z)
w : ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f_1 : X ⟶ Y}, ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ H → f_1 ≫ f mY = f mX
⊢ ∀ ⦃X Y : J⦄ (f_1 : X ⟶ Y), F.map f_1 ≫ f ⋯ = f ⋯ ≫ ((Functor.const J).obj Z).map f_1
Module: Mathlib.CategoryTheory.Filtered.Basic

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

Tactic:
apply ULift.ext

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
α : Type u
inst✝ : SemilatticeInf α
X Y : α
f g : X ⟶ Y
⊢ (𝟙 X ≫ f).down = (𝟙 X ≫ g).down
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ 𝟙 X ≫ f = 𝟙 X ≫ g

Tactic:
apply ULift.ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type u
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ (𝟙 X ≫ f).down = (𝟙 X ≫ g).down
Module: Mathlib.CategoryTheory.Filtered.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ { down := { down := ⋯ } } ≫ f = { down := { down := ⋯ } } ≫ g

Tactic:
apply ULift.ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ ({ down := { down := ⋯ } } ≫ f).down = ({ down := { down := ⋯ } } ≫ g).down