mathlib-initiative/mathlib-tactics huggingface dataset:
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 := ⋯
this : IsLimit (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))
⊢ (Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c))) ≅ F.mapCone c

Tactic:
refine Cone.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✝ : 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)))
j : J'
⊢ ((Cone.postcompose equ.hom).obj (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).π.app j =
    (Iso.refl
          ((Cone.postcompose equ.hom).obj
              (Cone.whisker e.symm.functor (F.mapCone (Cone.whisker e.functor c)))).pt).hom ≫
      (F.mapCone 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
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasColimit F
inst✝ : PreservesColimit F G
c : Cocone F
t : IsColimit (G.mapCocone c)
⊢ Nonempty (IsColimit c)

Tactic:
by
    suffices IsIso (IsColimit.desc (colimit.isColimit F) c) from ⟨by
      apply IsColimit.ofPointIso (colimit.isColimit F)⟩
    change IsIso ((Cocone.forget _).map ((colimit.isColimit F).descCoconeMorphism c))
    suffices IsIso (IsColimit.descCoconeMorphism (colimit.isColimit F) c) from by
      apply (Cocone.forget F).map_isIso _
    suffices IsIso ((Cocone.functoriality F G).map
      (IsColimit.descCoconeMorphism (colimit.isColimit F) c)) from by
        apply isIso_of_reflects_iso _ (Cocone.functoriality F G)
    exact (isColimitOfPreserves G (colimit.isColimit F)).hom_isIso t _

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

Goal state before:
pp: α : Type u_1
X Y : Discrete α
⊢ Fintype (X ⟶ Y)

Tactic:
by
  classical
  apply ULift.fintype

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)

pp: case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')

Tactic:
· obtain - | j := j
      · exact {Hom.id none}
      · exact {Hom.term j}

Goal state after:
case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
j' : J
⊢ Finset (j ⟶ some j')
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ ((iso G X Y).hom ≫ (iso G X Y).inv) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ ((iso G X Y).hom ≫ (iso G X Y).inv) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd

Tactic:
Iso.hom_inv_id

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ 𝟙 (G.obj (X ⨯ Y)) ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd
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
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ exactFunctor C D F

Tactic:
simp only [exactFunctor_iff]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ PreservesFiniteLimits F ∧ PreservesFiniteColimits F
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 : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map (A.inl ≫ A.snd) = 0

Tactic:
A.inl_snd,

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
P Q : C
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
A : BinaryBicone P Q
⊢ F.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : j = ↑i then eqToHom ⋯ else 0) =
    (if h : p j then ι (Subtype.restrict p f) ⟨j, h⟩ else 0) ≫ π (Subtype.restrict p f) i

Tactic:
rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]

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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ ∑ x, (t.ι as✝ ≫ t.π x) ≫ t.ι x = t.ι as✝ ≫ 𝟙 t.pt

Tactic:
t.ι_π,

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
J : Type u_1
inst✝ : Fintype J
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
as✝ : J
⊢ ∑ x, (if h : as✝ = x then eqToHom ⋯ else 0) ≫ t.ι x = t.ι as✝ ≫ 𝟙 t.pt
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv = desc b.inl b.inr

Tactic:
refine biprod.hom_ext' _ _ (hb.isLimit.hom_ext fun j => ?_) (hb.isLimit.hom_ext fun j => ?_)
  all_goals
    simp only [Category.assoc, IsLimit.conePointUniqueUpToIso_inv_comp]
    rcases j with ⟨⟨⟩⟩
  all_goals simp

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
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).hom ≫
      (hb.isLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit X Y)).inv =
    𝟙 b.pt

Tactic:
Iso.hom_inv_id

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
P Q X Y : C
inst✝ : HasBinaryBiproduct X Y
b : BinaryBicone X Y
hb : b.IsBilimit
⊢ 𝟙 b.pt = 𝟙 b.pt
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 W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst✝³ : Epi f
inst✝² : Epi g
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
⊢ Epi (map f g)

Tactic:
by
  rw [show biprod.map f g =
    (biprod.isoCoprod _ _).hom ≫ coprod.map f g ≫ (biprod.isoCoprod _ _).inv by aesop]
  infer_instance

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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).hom ≫ (hb.isLimit.conePointUniqueUpToIso (isLimit f)).inv = 𝟙 b.pt

Tactic:
Iso.hom_inv_id

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✝
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
D : Type uD
inst✝² : Category.{uD', uD} D
inst✝¹ : HasZeroMorphisms D
f : J → C
inst✝ : HasBiproduct f
b : Bicone f
hb : b.IsBilimit
⊢ 𝟙 b.pt = 𝟙 b.pt
Module: Mathlib.Algebra.Category.ModuleCat.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
M : ModuleCat R
h : IsZero M
⊢ Subsingleton ↑M

Tactic:
refine subsingleton_of_forall_eq 0 (fun x ↦ ?_)
  rw [← LinearMap.id_apply (R := R) x, ← ModuleCat.hom_id]
  simp only [(CategoryTheory.Limits.IsZero.iff_id_eq_zero M).mp h, hom_zero, LinearMap.zero_apply]

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

Goal state before:
pp: case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ Fin.cons x₀ x ∈ antidiagonalTuple (n✝ + 1) n ↔ ∑ i, Fin.cons x₀ x i = n

Tactic:
simp_rw [Fin.sum_cons, antidiagonalTuple, List.mem_flatMap, List.mem_map,
      List.Nat.mem_antidiagonal, Fin.cons_inj, exists_eq_right_right, ih,
      @eq_comm _ _ (Prod.snd _), and_comm (a := Prod.snd _ = _),
      ← Prod.mk_inj (a₁ := Prod.fst _), exists_eq_right]

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

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

Tactic:
cases H1 x

Goal state after:
case inl
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : f x = x
⊢ (f * g) x = x ∨ h x = x

case inr
α : Type u_1
f g h : Perm α
H1 : f.Disjoint h
H2 : g.Disjoint h
x : α
h✝ : h x = x
⊢ (f * g) x = x ∨ h x = x
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
p : Perm α
n : ℤ
x : α
hx : ¬(p ^ n) x = x
H : p x = x
⊢ False

Tactic:
simp [zpow_apply_eq_self_of_apply_eq_self H] at hx

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 : ι →₀ μ'
h : (ι →₀ μ) ≃ (ι →₀ μ') := (mapRange.addEquiv e).toEquiv
hh : h = (mapRange.addEquiv e).toEquiv
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ f ∈ map h.toEmbedding (s.finsuppAntidiag n)

Tactic:
mem_map_equiv,

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
hf : f ∈ s.finsuppAntidiag (e n)
this : n = e.symm (e n)
⊢ h.symm f ∈ s.finsuppAntidiag n
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

Tactic:
refine le_antisymm (support_mul_le _ _) fun a => ?_

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.Disjoint g
a : α
⊢ a ∈ f.support ∪ g.support → a ∈ (f * g).support
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
⊢ (take (i + 1) c.blocks).sum = ↑(c.boundary ⟨i + 1, h⟩)

Tactic:
| succ i IH =>

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
hl : (a :: l).Nodup
hl' : l.Nodup
hln' : (permsOfList l).Nodup
hmeml : ∀ {f : Equiv.Perm α}, f ∈ permsOfList l → f a = a
i j : ℕ
hi : i < l.length
hj : j < l.length
hij : i < j
x : Equiv.Perm α
hx₁ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[i]
hx₂ : x ∈ (fun b ↦ List.map (fun f ↦ Equiv.swap a b * f) (permsOfList l)) l[j]
f : Equiv.Perm α
hf : f ∈ permsOfList l ∧ Equiv.swap a l[i] * f = x
g : Equiv.Perm α
hg : g ∈ permsOfList l ∧ Equiv.swap a l[j] * g = x
hix : x a = l[i]
hiy : x a = l[j]
hieqj : i = j
⊢ False

Tactic:
exact absurd hieqj (_root_.ne_of_lt hij)

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

Goal state before:
pp: 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

pp: 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

Tactic:
· simp [← hk', eq_comm]

Goal state after:
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.Cycle.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(f.support \ {x}) + 1 = #(f.support.erase x) + 1

Tactic:
sdiff_singleton_eq_erase

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hf : f.IsCycle
x : α
hx : f x ≠ x ∧ ∀ ⦃y : α⦄, f y ≠ y → f.SameCycle x y
h1 : ¬f (f x) = x
⊢ #(f.support.erase x) + 1 = #(f.support.erase x) + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

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

Tactic:
exact absurd h (orderOf_pos _).ne'

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

Goal state before:
pp: case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (sumCongr 1 (swap b₁ b₂)) * sign σb' = sign (swap b₁ b₂) * sign σb'

Tactic:
sumCongr_one_swap,

Goal state after:
case right.swap_mul
α : Type u
inst✝³ : DecidableEq α
β : Type v
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : sign (sumCongr 1 σb') = sign σb'
⊢ sign (swap (Sum.inr b₁) (Sum.inr b₂)) * sign σb' = sign (swap b₁ b₂) * sign σb'
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ ∀ (n : ℤ), (f.cycleOf x ^ n) x = (f ^ n) x

Tactic:
intro z
  cases z with
  | ofNat z => exact cycleOf_pow_apply_self f x z
  | negSucc z =>
    rw [zpow_negSucc, ← inv_pow, cycleOf_inv, zpow_negSucc, ← inv_pow, cycleOf_pow_apply_self]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
| (g ^ m) x = (g ^ n) x

Tactic:
rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
m n : ℤ
x : α
hx : g x ≠ x
| (g ^ n * g ^ (m - n)) x = (g ^ n) x
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
conv_lhs => rw [← Int.sub_add_cancel m n, Int.add_comm, zpow_add]

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

Goal state before:
pp: n : ℕ
i : Fin n
⊢ sign i.cycleRange = (-1) ^ ↑i

Tactic:
simp [cycleRange]

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

Goal state before:
pp: case succ
n : ℕ
inst✝ : NeZero n
n✝ : ℕ
hi : n✝ + 1 < n
h0 : ⟨n✝ + 1, hi⟩ ≠ 0
⊢ ⟨n✝ + 1, hi⟩.cycleRange.cycleType = {↑⟨n✝ + 1, hi⟩ + 1}

Tactic:
simp [cycleRange]

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

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f (p - 1 + 1) s = s

Tactic:
tsub_add_cancel_of_le hp.out.one_lt.le,

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
s : ↑(vectorsProdEqOne G p)
⊢ f p s = s
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
Equiv.Perm.signAux_swap hne

Goal state after:
n : ℕ
σ π : Perm (Fin n)
i j : Fin n
hne : i ≠ j
h_eq : sign π = π.signAux
⊢ -1 * π.signAux = -1 * π.signAux
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ f (snoc m (x + y)) = f (snoc m x) + f (snoc m y)

Tactic:
← update_snoc_last x m (x + y),

Goal state after:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
x y : M (last n)
⊢ f (update (snoc m x) (last n) (x + y)) = f (snoc m x) + f (snoc m y)
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
⊢ ∑ σ, ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x = 0

Tactic:
obtain ⟨i, j, hpij, hij⟩ : ∃ i j, p i = p j ∧ i ≠ j := by
    rw [← Finite.injective_iff_bijective, Injective] at H
    push Not at H
    exact H

Goal state after:
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
⊢ ∑ σ, ↑↑(sign σ) * ∏ x, M (σ x) (p x) * N (p x) x = 0
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
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
h : ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign τ)
⊢ (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ j, M (τ j) (σ j) =
    (∏ i, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign ((Equiv.mulRight σ⁻¹) τ))) * ∏ i, M (((Equiv.mulRight σ⁻¹) τ) i) i

Tactic:
Equiv.coe_mulRight,

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M N : Matrix n n R
σ : Perm n
x✝ : σ ∈ univ
τ : Perm n
this : ∏ j, M (τ j) (σ j) = ∏ j, M ((τ * σ⁻¹) j) j
h : ↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹)) = ↑↑(sign τ)
⊢ (∏ i, N (σ i) i) * ↑↑(sign τ) * ∏ j, M (τ j) (σ j) =
    (∏ i, N (σ i) i) * (↑↑(sign σ) * ↑↑(sign (τ * σ⁻¹))) * ∏ i, M ((τ * σ⁻¹) i) i
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (↑M * ↑M⁻¹ * N).det = N.det

Tactic:
Units.mul_inv,

Goal state after:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : (Matrix m m R)ˣ
N : Matrix m m R
⊢ (1 * N).det = N.det
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
A B C : Matrix n n R
hC : C.det = 1
hA : A = C * B
⊢ C.det * B.det = B.det

Tactic:
by rw [hC, one_mul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
X Y : Cᵒᵖ
f g : X ⟶ Y
⊢ f ≫ (IsCofiltered.eqHom f.unop g.unop).op = g ≫ (IsCofiltered.eqHom f.unop g.unop).op

Tactic:
by
      rw [show f = f.unop.op by simp, show g = g.unop.op by simp, ← op_comp, ← op_comp]
      congr 1
      exact IsCofiltered.eq_condition f.unop g.unop

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
α : Type u_2
inst✝ : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ f (update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (update m i (g a))

Tactic:
induction t using Finset.induction with

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
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i =
    ∑ p ∈ univ.pi fun x ↦ univ, ∏ x ∈ univ.attach, ↑↑(sign (p ↑x ⋯)) * ∏ i, M (↑x) ((p ↑x ⋯) i) i

Tactic:
simp_rw [Finset.prod_attach_univ, Finset.univ_pi_univ]

Goal state after:
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
⊢ ∑ σ, ↑↑(sign σ) * ∏ i, blockDiagonal M (σ i) i = ∑ x, ∏ x_1, ↑↑(sign (x x_1 ⋯)) * ∏ x_2, M x_1 ((x x_1 ⋯) x_2) x_2