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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
⊢ HasPushout h (h ≫ f)

Tactic:
simpa only [Category.comp_id] using hasPushout_of_epi_comp (𝟙 X) f h

Goal state after:
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
s : Fork f g
⊢ s.π.app one = s.ι ≫ g

Tactic:
by
  rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]

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
K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : PreservesColimit K₁ F
c : Cocone K₂
t : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
by
    apply IsColimit.precomposeHomEquiv (Functor.isoWhiskerRight h F :) _ _
    have := (IsColimit.precomposeHomEquiv h c).symm t
    apply IsColimit.ofIsoColimit (isColimitOfPreserves F this)
    exact Cocone.ext (Iso.refl _)

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
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0

Tactic:
rw [Iso.hom_inv_id, Category.id_comp]

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

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

Tactic:
obtain - | j' := j'
    · obtain - | j := j
      · exact {Hom.id none}
      · exact {Hom.term j}
    · by_cases h : some j' = j
      · rw [h]
        exact {Hom.id j}
      · exact ∅

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
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 𝟙 c.pt = 0

Tactic:
← cancel_mono c.ι,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 𝟙 c.pt ≫ Fork.ι c = 0 ≫ Fork.ι 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
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : (factorThruImage f ≫ image.ι f) ≫ cokernel.π f = 0
⊢ image.ι f ≫ cokernel.π f = 0

Tactic:
← HasZeroMorphisms.comp_zero (Limits.factorThruImage f),

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
inst✝³ : HasImage f
inst✝² : HasCokernel (image.ι f)
inst✝¹ : HasCokernel f
inst✝ : Epi (factorThruImage f)
w : (factorThruImage f ≫ image.ι f) ≫ cokernel.π f = factorThruImage f ≫ 0
⊢ image.ι f ≫ cokernel.π f = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ ι f j ≫ (desc fun j ↦ (w j).inv ≫ ι g (e j)) ≫ π g k =
    ι f j ≫ (lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯) ≫ π g k

Tactic:
simp only [ι_desc_assoc, Category.assoc, lift_π]

Goal state after:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
k : K
j : J
h : ¬k = e j
⊢ (w j).inv ≫ ι g (e j) ≫ π g k = ι f j ≫ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ ι g k ≫ (desc fun k ↦ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k)) ≫ π f j =
    ι g k ≫ (lift fun j ↦ π g (e j) ≫ (w j).hom) ≫ π f j

Tactic:
simp only [ι_desc_assoc, Category.assoc, lift_π]

Goal state after:
case neg
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
j : J
k : K
h : ¬k = e j
⊢ eqToHom ⋯ ≫ (w (e.symm k)).hom ≫ ι f (e.symm k) ≫ π f j = ι g k ≫ π g (e j) ≫ (w j).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
⊢ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π = s.π

Tactic:
by
      apply biproduct.hom_ext'; intro j
      rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_assoc]
      rcases Classical.em (i = j) with (rfl | h)
      · rw [if_neg (Classical.not_not.2 rfl), zero_comp, CokernelCofork.condition]
      · rw [if_pos (Ne.symm h), Category.id_comp]

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
inst✝¹ : HasBinaryBiproduct X✝ Y✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ section_ f ≫
      (splitMonoOfIdempotentOfIsLimitFork C ⋯
          (isLimitForkOfKernelFork (isKernelCompMono i (section_ f) ⋯))).retraction =
    0

Tactic:
rw [splitMonoOfIdempotentOfIsLimitFork_retraction, isLimitForkOfKernelFork_lift,
        isKernelCompMono_lift]

Goal state after:
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✝ : IsSplitEpi f
c : KernelFork f
i : IsLimit c
⊢ section_ f ≫ i.lift (Fork.ofι (Fork.ι (kernelForkOfFork (Fork.ofι (𝟙 X - f ≫ section_ f) ⋯))) ⋯) = 0
Module: Mathlib.Data.Fin.Tuple.NatAntidiagonal

Goal state before:
pp: case succ.right.succ
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)
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    (antidiagonal (n + 1))

Tactic:
rw [List.Nat.antidiagonal_succ]

Goal state after:
case succ.right.succ
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)
⊢ Pairwise (Function.onFun Disjoint fun ni ↦ map (fun x ↦ Fin.cons ni.1 x) (antidiagonalTuple k ni.2))
    ((0, n + 1) :: map (Prod.map Nat.succ id) (antidiagonal n))
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ (e.extendDomain f.toEquivRange) b = f (e (⋯.invOfMemRange ⟨b, h⟩))

Tactic:
rw [Equiv.Perm.extendDomain_apply_subtype _ _ h]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∈ Set.range ⇑f
⊢ ↑(f.toEquivRange (e (f.toEquivRange.symm ⟨b, h⟩))) = f (e (⋯.invOfMemRange ⟨b, h⟩))
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g x y : Perm α
h : f.Disjoint g
hf : x.support ⊆ f.support
hg : y.support ⊆ g.support
⊢ x.Disjoint y

Tactic:
by
  rw [disjoint_iff_disjoint_support] at h ⊢
  exact h.mono hf hg

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

Goal state before:
pp: case cons.inr.e_i
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
this : i ≤ xs.length
hn' : i < xs.length
⊢ i + 1 < (x :: xs).length

Tactic:
simpa [Nat.succ_eq_add_one]

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'

Goal state after:
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).get ⟨n, hn⟩
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Submonoid.closure {σ | σ.IsSwap} = ⊤

Tactic:
cases nonempty_fintype α
  refine top_unique fun x _ ↦ ?_
  obtain ⟨h1, h2⟩ := (truncSwapFactors x).out.prop
  rw [← h1]
  exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)

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

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

Tactic:
by
  rw [← sameCycle_apply_right, apply_symm_apply]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
hd : α
tl : List α
hl : (hd :: tl).Nodup
⊢ (hd :: tl).formPerm = 1 ↔ (hd :: tl).length ≤ 1

Tactic:
· rw [← formPerm_apply_mem_eq_self_iff _ hl hd mem_cons_self]
    constructor
    · simp +contextual
    · intro h
      simp only [(hd :: tl).formPerm_apply_mem_eq_self_iff hl hd mem_cons_self,
        add_le_iff_nonpos_left, length, nonpos_iff_eq_zero, length_eq_zero_iff] at h
      simp [h]

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

Goal state before:
pp: case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : (swap 0 1) 0 = 1
⊢ (if a₁ ≤ (swap 0 1) 0 then -1 else 1) = 1

Tactic:
h01,

Goal state after:
case inr.inl
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : (swap 0 1) 0 = 1
⊢ (if a₁ ≤ 1 then -1 else 1) = 1
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
h01,

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : s l.prod = 1
⊢ False

Tactic:
hl.1,

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this✝ : ∀ a ∈ List.map (⇑s) l, a = 1
this : s g = 1
⊢ False
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
this : ∀ {f : Perm α}, f.IsSwap → s f = -1
f : Perm α
⊢ s f = sign f

Tactic:
by
    let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
    have hsl : ∀ a ∈ l.map s, a = (-1 : ℤˣ) := fun a ha =>
      let ⟨g, hg⟩ := List.mem_map.1 ha
      hg.2 ▸ this (hl₂ _ hg.1)
    rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]

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

Goal state before:
pp: α : Type u
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p (f x) ↔ p x
h₂ : ∀ (x : α), f x ≠ x → p x
⊢ sign (f.subtypePerm h₁) = sign f

Tactic:
let l := (truncSwapFactors (subtypePerm f h₁)).out
  have hl' : ∀ g' ∈ l.1.map ofSubtype, IsSwap g' := fun g' hg' =>
    let ⟨g, hg⟩ := List.mem_map.1 hg'
    hg.2 ▸ (l.2.2 _ hg.1).of_subtype_isSwap
  have hl'₂ : (l.1.map ofSubtype).prod = f := by
    rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
  conv =>
    congr
    rw [← l.2.1]
  simp_rw [← hl'₂]
  rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]

Goal state after:
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)

pp: case intro.mp.inr
β : 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).gcd n = 1
⊢ n.Coprime (orderOf f)

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

Goal state after:
case intro.mp.inr
β : 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).gcd n = 1
⊢ n.Coprime (orderOf f)
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ ↑(n.natMod ↑(#s))) a = (f ^ n) a

Tactic:
Int.natMod,

Goal state after:
α : Type u_2
f : Perm α
a : α
s : Finset α
hf : f.IsCycleOn ↑s
ha : a ∈ s
n : ℤ
hb : (f ^ n) a ∈ s
k : ℤ
hk : n % ↑(#s) - n = ↑(#s) * k
⊢ (f ^ ↑(n % ↑(#s)).toNat) a = (f ^ n) a
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : 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)
⊢ 0 < ↑(#g.support)

Tactic:
simp only [Int.natCast_pos]

Goal state after:
α : 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)
⊢ 0 < #g.support
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case neg
n✝ : ℕ
i✝ : Fin (n✝ + 1).succ
i : Fin (n✝ + 1)
h : ¬i = Fin.last n✝
⊢ ↑i.succ + 1 = ↑((swap 0 1) ((finRotate (n✝ + 1)) i).succ)

Tactic:
· rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
⊢ H = ⊤

Tactic:
have hσ2 : IsCycle ↑σ := isCycle_of_prime_order'' h0 hσ1

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : Subgroup (Perm α)
d : DecidablePred fun x ↦ x ∈ H
τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : Fintype.card α ∣ Fintype.card ↥H
h2 : τ ∈ H
h3 : τ.IsSwap
this : Fact (Nat.Prime (Fintype.card α))
σ : ↥H
hσ : orderOf σ = Fintype.card α
hσ1 : orderOf ↑σ = Fintype.card α
hσ2 : (↑σ).IsCycle
⊢ H = ⊤
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ x ∈ (g.cycleOf x).support

Tactic:
rw [mem_support_cycleOf_iff]

Goal state after:
case right
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
h : x ∈ g.support
⊢ g.SameCycle x x ∧ x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
⊢ ∀ (τ : Perm α),
    σ.Disjoint τ →
      σ.IsCycle →
        (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
          (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
            ∀ {f : Perm α},
              f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}

Tactic:
τ

Goal state after:
case refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ τ : Perm α
⊢ σ.Disjoint τ →
    σ.IsCycle →
      (∀ {f : Perm α}, f ∈ σ.cycleFactorsFinset → (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}) →
        (∀ {f : Perm α}, f ∈ τ.cycleFactorsFinset → (τ * f⁻¹).cycleFactorsFinset = τ.cycleFactorsFinset \ {f}) →
          ∀ {f : Perm α},
            f ∈ (σ * τ).cycleFactorsFinset → (σ * τ * f⁻¹).cycleFactorsFinset = (σ * τ).cycleFactorsFinset \ {f}
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
inst✝ : IsEmpty n
⊢ detp 1 A = 1

Tactic:
rw [detp, sum_unique_nonempty _ _ ⟨1, _⟩] <;> simp

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

Goal state before:
pp: case pos
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : Function.Injective v
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)

pp: case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)

Tactic:
· exact h v hi

Goal state after:
case neg
ι : Type u_7
ι₁ : Type u_10
inst✝⁵ : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst✝⁴ : CommSemiring R'
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R' N₁
inst✝ : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h : ∀ (v : ι → ι₁), Function.Injective v → (f fun i ↦ e (v i)) = g fun i ↦ e (v i)
v : ι → ι₁
hi : ¬Function.Injective v
⊢ (↑f fun i ↦ e (v i)) = ↑g fun i ↦ e (v i)
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
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A (some i) none = detp (-s) (A.submatrix some (Function.update some i none))

Tactic:
rw [adjp_none_right]

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ detp (sign (swap none (some i)) * s) (A.submatrix some (⇑(swap none (some i)) ∘ some)) =
    detp (-s) (A.submatrix some (Function.update some i none))
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
s : ℤˣ
i : n
A : Matrix (Option n) (Option n) R
⊢ adjp s A none (some i) = detp (-s) (A.submatrix (Function.update some i none) some)

Tactic:
rw [← detp_transpose]; simp [← A.transpose.adjp_some_none, adjp_transpose]

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

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq m
inst✝³ : Fintype m
R : Type u_3
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
e₁ e₂ : n ≃ m
A : Matrix m m R
hee : e₂ = e₁.trans (e₁.symm.trans e₂)
⊢ |((A.submatrix id ⇑(e₁.symm.trans e₂)).submatrix ⇑e₁ ⇑e₁).det| = |A.det|

Tactic:
rw [Matrix.det_submatrix_equiv_self, Matrix.det_permute', abs_mul, abs_unit_intCast, one_mul]

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
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ ((c • 1) • A).det = c ^ Fintype.card n • A.det

Tactic:
det_smul,

Goal state after:
n : Type u_2
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype n
R : Type v
inst✝⁴ : CommRing R
α : Type u_3
inst✝³ : Monoid α
inst✝² : MulAction α R
inst✝¹ : IsScalarTower α R R
inst✝ : SMulCommClass α R R
c : α
A : Matrix n n R
⊢ (c • 1) ^ Fintype.card n * A.det = c ^ Fintype.card n • A.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 B : Matrix n n R
d : n → R
hAB : A * B = diagonal d
s t : ℤˣ
h : s ≠ t
σ : Perm n
hσ : σ ∈ ofSign s
⊢ ∀ a ∈ ofSign t, IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (a k))

Tactic:
τ

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 : ℤˣ
h : s ≠ t
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign t → IsAddUnit ((∏ k, A k (σ k)) * ∏ k, B k (τ k))
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σ : σ ∈ {x ∈ ofSign t | x j = k}
⊢ ∀ a ∈ ofSign s, IsAddUnit ((∏ k, A k (a k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))

Tactic:
τ

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 : ℤˣ
h : s ≠ t
i j k : n
hk : k ∈ univ
σ : Perm n
hσ : σ ∈ {x ∈ ofSign t | x j = k}
τ : Perm n
⊢ τ ∈ ofSign s → IsAddUnit ((∏ k, A k (τ k)) * (B i k * ∏ k ∈ {j}ᶜ, B k (σ k)))