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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ (isoOfEquivalence e w).inv ≫ limit.π F j = limit.π G (e.functor.obj j) ≫ w.hom.app j

Tactic:
simp only [HasLimit.isoOfEquivalence]

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
G : K ⥤ C
inst✝ : HasLimit G
e : J ≌ K
w : e.functor ⋙ G ≅ F
j : J
⊢ ((limit.isLimit F).conePointsIsoOfEquivalence (limit.isLimit G) e w).inv ≫ limit.π F j =
    limit.π G (e.functor.obj j) ≫ w.hom.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

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

Tactic:
by
  apply colimit.w (WidePushoutShape.wideSpan _ _ _) (WidePushoutShape.Hom.init j)

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ limit.π (Discrete.functor (f ∘ ⇑ε)) { as := ε.symm (ε b) } ≫
      (Discrete.functor f).map ((Discrete.equivalence ε).counit.app { as := ε b }) =
    π (f ∘ ⇑ε) b

Tactic:
exact limit.w (Discrete.functor (f ∘ ε)) (Discrete.eqToHom' (ε.symm_apply_apply b))

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f ↔ ⊤ f

Tactic:
simp only [top_apply, iff_true]

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
a✝ : W₁.HasFactorization W₂
X Y : C
f : X ⟶ Y
⊢ W₁.comp W₂ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case op
X : WalkingParallelPair
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op X) = (𝟭 WalkingParallelPairᵒᵖ).obj (op X)

Tactic:
cases X

Goal state after:
case op.zero
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = (𝟭 WalkingParallelPairᵒᵖ).obj (op zero)

case op.one
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) = (𝟭 WalkingParallelPairᵒᵖ).obj (op one)
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ e✝¹ = e✝

Tactic:
apply (cancel_mono Fm).1

Goal state after:
case e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ e✝¹ ≫ Fm = e✝ ≫ Fm
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y : C
inst✝ : Category.{v, u} C
f g : X✝ ⟶ Y
P : C
ι : P ⟶ X✝
w : ι ≫ f = ι ≫ g
X : WalkingParallelPair
⊢ ((Functor.const WalkingParallelPair).obj P).obj X ⟶ (parallelPair f g).obj X

Tactic:
cases X

Goal state after:
case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f g).obj zero

case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
P : C
ι : P ⟶ X
w : ι ≫ f = ι ≫ g
⊢ ((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f g).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
P : C
ι : P ⟶ X✝
w : ι ≫ f✝ = ι ≫ g
X Y : WalkingParallelPair
f : X ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        X = t → (((Functor.const WalkingParallelPair).obj P).obj X ⟶ (parallelPair f✝ g).obj X)) X (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

Tactic:
cases X

Goal state after:
case zero
C : Type u
X Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y✝
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
Y : WalkingParallelPair
f : zero ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        zero = t → (((Functor.const WalkingParallelPair).obj P).obj zero ⟶ (parallelPair f✝ g).obj zero)) zero
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f

case one
C : Type u
X Y✝ : C
inst✝ : Category.{v, u} C
f✝ g : X ⟶ Y✝
P : C
ι : P ⟶ X
w : ι ≫ f✝ = ι ≫ g
Y : WalkingParallelPair
f : one ⟶ Y
⊢ ((Functor.const WalkingParallelPair).obj P).map f ≫
      WalkingParallelPair.casesOn (motive := fun t ↦
        Y = t → (((Functor.const WalkingParallelPair).obj P).obj Y ⟶ (parallelPair f✝ g).obj Y)) Y (fun h ↦ ⋯ ▸ ι)
        (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ =
    WalkingParallelPair.casesOn (motive := fun t ↦
        one = t → (((Functor.const WalkingParallelPair).obj P).obj one ⟶ (parallelPair f✝ g).obj one)) one
        (fun h ↦ ⋯ ▸ ι) (fun h ↦ ⋯ ▸ ι ≫ f✝) ⋯ ≫
      (parallelPair f✝ g).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi f

Tactic:
by
  rw [← image.fac f]
  apply epi_comp

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 C
X Y : C
inst✝ : HasBinaryProduct X Y
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ Y
e : x✝¹ ≫ prod.inr X Y = x✝ ≫ prod.inr X Y
⊢ x✝¹ = x✝

Tactic:
simpa using congrArg (· ≫ prod.snd) e

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
this : HasLimitsOfShape (Discrete (Fin n)) C
⊢ HasLimitsOfShape (Discrete ι) C

Tactic:
exact hasLimitsOfShape_of_equivalence (Discrete.equivalence e.symm)

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
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
as✝ : J
⊢ (∑ j, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app { as := as✝ } = s.π.app { as := as✝ }

Tactic:
simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]

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
b : Bicone f
total : ∑ j, b.π j ≫ b.ι j = 𝟙 b.pt
s : Cone (Discrete.functor f)
as✝ : J
⊢ (∑ x, if h : x = as✝ then s.π.app { as := x } ≫ eqToHom ⋯ else s.π.app { as := x } ≫ 0) = s.π.app { as := as✝ }
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.Biproducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsColimit t.toCocone
⊢ t.fst ≫ t.inl + t.snd ≫ t.inr = 𝟙 t.pt

Tactic:
by
    refine BinaryCofan.IsColimit.hom_ext ht ?_ ?_ <;> simp

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 : ℕ
⊢ (∃ a ∈ antidiagonal n, ∃ a_1 ∈ antidiagonalTuple n✝ a.2, Fin.cons a.1 a_1 = Fin.cons x₀ x) ↔ x₀ + ∑ i, x i = n

Tactic:
List.Nat.mem_antidiagonal,

Goal state after:
case cons
k n✝ x₀ : ℕ
x : Fin n✝ → ℕ
ih : ∀ {n : ℕ}, x ∈ antidiagonalTuple n✝ n ↔ ∑ i, x i = n
n : ℕ
⊢ (∃ a, a.1 + a.2 = n ∧ ∃ a_1 ∈ antidiagonalTuple n✝ a.2, Fin.cons a.1 a_1 = Fin.cons x₀ x) ↔ x₀ + ∑ i, x i = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: n : ℕ
c : Composition n
⊢ c.boundaries.orderEmbOfFin ⋯ = c.boundary

Tactic:
by
  refine (Finset.orderEmbOfFin_unique' _ ?_).symm
  exact fun i => (Finset.mem_map' _).2 (Finset.mem_univ _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ (permsOfList (a :: l)).length = (a :: l).length !

Tactic:
simp [Nat.factorial_succ, permsOfList, length_permsOfList, succ_mul, add_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
hxy : x ≠ y
⊢ #(swap x y).support = 2

Tactic:
exact card_support_swap hxy

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

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ False

Tactic:
refine not_exists.mpr h' ?_

Goal state after:
case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
h : ⟨0, ⋯⟩ = ⟨n, hn⟩
⊢ ∃ x, l = [x]
Module: Mathlib.Data.Int.Order.Units

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

Tactic:
rw [← sq, units_sq]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
⊢ f.SameCycle x (f y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_apply_left, sameCycle_comm]

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

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]

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

Goal state before:
pp: case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑(a.support ⊔ b.support) ⊆ ⋃ b ∈ S, ↑b.support

Tactic:
rw [Finset.sup_eq_union, Finset.coe_union, Set.union_subset_iff]

Goal state after:
case mul
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
S : Set (Perm α)
a b : Perm α
ha : a ∈ closure S
hb : b ∈ closure S
hc : ↑a.support ⊆ ⋃ b ∈ S, ↑b.support
hd : ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
⊢ ↑a.support ⊆ ⋃ b ∈ S, ↑b.support ∧ ↑b.support ⊆ ⋃ b ∈ S, ↑b.support
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: case h
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)
inst✝ : DecidableEq ι
i : ι
y : N i
j : ι
hj : j ∈ Finset.univ.erase i
⊢ (ϕ j) (Pi.mulSingle i y j) = 1

Tactic:
simp only [Finset.mem_erase] at hj

Goal state after:
case h
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)
inst✝ : DecidableEq ι
i : ι
y : N i
j : ι
hj : j ≠ i ∧ j ∈ Finset.univ
⊢ (ϕ j) (Pi.mulSingle i y j) = 1
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ (g * c) x = (c * g) x

Tactic:
simp only [coe_mul, Function.comp_apply]

Goal state after:
case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
hc : c.IsCycle
hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support
i : ℤ
hi : (fun x ↦ c.subtypePermOfSupport ^ x) i = g.subtypePerm hc'
x : α
⊢ g (c x) = c (g x)
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : x ∉ f.support
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y

Tactic:
notMem_support

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
f✝ g : Perm α
x✝ y✝ : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x y : α
hxy : f.SameCycle x y
hx : f x = x
this : Nonempty α
⊢ ∃ m < Fintype.card α, (f ^ m) x = y
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ (f.cycleOf x).support.Nonempty ↔ f x ≠ x

Tactic:
rw [← two_le_card_support_cycleOf_iff, ← card_pos, ← Nat.succ_le_iff]

Goal state after:
α : Type u_2
f : Perm α
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ Nat.succ 0 ≤ #(f.cycleOf x).support ↔ 2 ≤ #(f.cycleOf x).support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (a + s.sum + (s.card + 1))

Tactic:
ihs

Goal state after:
case cons
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
a : ℕ
s : Multiset ℕ
ihs : (Multiset.map (fun n ↦ -(-1) ^ n) s).prod = (-1) ^ (s.sum + s.card)
⊢ -(-1) ^ a * (-1) ^ (s.sum + s.card) = (-1) ^ (a + s.sum + (s.card + 1))
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case neg
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : x ∉ f.support
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x

Tactic:
notMem_support

Goal state after:
case neg
α : Type u_2
x : α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
hx : f x = x
k : ℤ
⊢ (f ^ 1) x = (f ^ k) x
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
hg : g.IsCycle
n : ℤ
x : α
hx : g x ≠ x
q : ℤ := n / ↑(#g.support)
r : ℤ := n % ↑(#g.support)
m : ℕ
hm : r = ↑m
div_euc : ↑m + ↑(orderOf g) * q = n ∧ m < orderOf g
hgm : g ^ m = 1
⊢ (g ^ m) x = x

Tactic:
simp only [hgm, coe_one, id_eq]

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

Goal state before:
pp: case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : {#σ.support} = {#τ.support}
hτ : τ.IsCycle
⊢ #σ.support = #τ.support

Tactic:
Multiset.singleton_inj

Goal state after:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
τ : Perm α
h : #σ.support = #τ.support
hτ : τ.IsCycle
⊢ #σ.support = #τ.support
Module: Mathlib.GroupTheory.Perm.Fin

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

Tactic:
cycleRange,

Goal state after:
n : ℕ
i j : Fin n
h : i < j
⊢ ((finRotate (↑i + 1)).extendDomain (castLEEmb ⋯).toEquivRange) j = j
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⟩
⊢ j.cycleRange i = if i = j then 0 else i + 1

Tactic:
cycleRange,

Goal state after:
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
⊢ ((finRotate (↑j + 1)).extendDomain (castLEEmb ⋯).toEquivRange) i = if i = j then 0 else i + 1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
G : Type u_2
inst✝ : Group G
n : ℕ
v : List.Vector G n
⊢ v.toList.prod⁻¹ ::ᵥ v ∈ vectorsProdEqOne G (n + 1)

Tactic:
rw [mem_iff, Vector.toList_cons, List.prod_cons, inv_mul_cancel]

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

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) → x ∈ f.support

Tactic:
rintro ⟨hc, _⟩

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hc : (f.cycleOf x).IsCycle
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
⊢ x ∈ f.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Nat.card G
this : Fintype G
⊢ ∃ x, orderOf x = p

Tactic:
Nat.card_eq_fintype_card

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
hp : Fact (Nat.Prime p)
this : Fintype G
hdvd : p ∣ Fintype.card G
⊢ ∃ x, orderOf x = p
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ ((∀ f ∈ {g}, f.IsCycle) ∧ ∃ (h : (↑{g}).Pairwise Disjoint), {g}.noncommProd id ⋯ = f) ↔ f.IsCycle ∧ f = g

Tactic:
simpa [eq_comm]

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

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g = swap a (g a) * swap (g a) (g (g a)) → a ∈ g.support

Tactic:
intro hg
    rw [mem_support]
    intro hx
    apply hg3.isCycle.ne_one
    simpa [hx] using! hg

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

Goal state before:
pp: case intro.a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
h :
  ∀ (p : (i : ι) → κ i),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) = g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)
x : (i : ι) → Π₀ (j : κ i), M i j
val✝ : Fintype ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ (x i).support
⊢ (f fun i ↦ DFinsupp.single (p i) ((x i) (p i))) = g fun i ↦ DFinsupp.single (p i) ((x i) (p i))

Tactic:
MultilinearMap.ext_iff

Goal state after:
case intro.a
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : Type uN
inst✝⁶ : Finite ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : AddCommMonoid N
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f g : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
x : (i : ι) → Π₀ (j : κ i), M i j
val✝ : Fintype ι
p : (a : ι) → κ a
a✝ : p ∈ Fintype.piFinset fun i ↦ (x i).support
h :
  ∀ (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
    (f.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) x = (g.compLinearMap fun i ↦ DFinsupp.lsingle (p i)) x
⊢ (f fun i ↦ DFinsupp.single (p i) ((x i) (p i))) = g fun i ↦ DFinsupp.single (p i) ((x i) (p i))
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
⊢ g x = (swap a (g a) * swap (g a) (g (g a))) x

Tactic:
simp only [coe_mul, Function.comp_apply]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : a ∈ g.support
ha' : g.support = {a, g a, g (g a)}
ha'' : [a, g a, g (g a)].Nodup
x : α
⊢ g x = (swap a (g a)) ((swap (g a) (g (g a))) x)
Module: Mathlib.LinearAlgebra.Multilinear.Basis

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
inst✝⁵ : CommSemiring R
M : ι → Type u_3
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite ι
f g : MultilinearMap R M N
ιM : ι → Type u_5
e : (i : ι) → Basis (ιM i) R (M i)
h : ∀ (v : (i : ι) → ιM i), (f fun i ↦ (e i) (v i)) = g fun i ↦ (e i) (v i)
val✝ : Fintype ι
⊢ f = g

Tactic:
ext m
  rcases Function.Surjective.piMap (fun i ↦ (e i).repr.symm.surjective) m with ⟨x, rfl⟩
  unfold Pi.map
  simp_rw [(e _).repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum,
    map_sum_finset, map_smul_univ, h]

Goal state after:
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 N P : Matrix m m R
⊢ (N * M).det * P.det = (N * M * P).det

Tactic:
← det_mul

Goal state after:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (N * M * P).det = (N * M * P).det
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 N P : Matrix m m R
⊢ M.det * (P * N).det = (M * (P * N)).det

Tactic:
← det_mul

Goal state after:
m : Type u_1
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M N P : Matrix m m R
⊢ (M * (P * N)).det = (M * (P * N)).det
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
A' : Matrix n n R := A.updateRow j (A i)
h' : ∀ (s : ℤˣ), (A * adjp s A) i j = (A' * adjp s A') j j
⊢ (A * adjp 1 A) i j = (A * adjp (-1) A) i j

Tactic:
simp_rw [h', mul_adjp_apply_eq]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A : Matrix n n R
i j : n
h : i ≠ j
A' : Matrix n n R := A.updateRow j (A i)
h' : ∀ (s : ℤˣ), (A * adjp s A) i j = (A' * adjp s A') j j
⊢ detp 1 A' = detp (-1) A'
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
hτ : sign τ = s
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
rw [← hσ.1, ← hτ, ← sign_inv] at h

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : sign σ = t ∧ σ j = k
τ : Perm n
h : sign τ⁻¹ ≠ sign σ
hτ : sign τ = s
⊢ IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))