mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
h : f ∈ hd :: tl
hl : List.Pairwise Disjoint (hd :: tl)
⊢ ∀ x ∈ f.support, f x = (hd :: tl).prod x

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: case h.inr
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (⇑σ) (Set.range Sum.inl) (Set.range Sum.inl)
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := σ.subtypePermOfFintype h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := σ.subtypePermOfFintype h3
σ₁ : Perm m := (ofInjective Sum.inl ⋯).symm.permCongr σ₁'
σ₂ : Perm n := (ofInjective Sum.inr ⋯).symm.permCongr σ₂'
b : n
⊢ ((σ₁, σ₂).1.sumCongr (σ₁, σ₂).2) (Sum.inr b) = σ (Sum.inr b)

Tactic:
· rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm,
      apply_ofInjective_symm Sum.inr_injective, ofInjective_apply]
    rfl

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
h : ¬f = 1
⊢ #f.support ≠ 1

Tactic:
· exact ne_of_gt (one_lt_card_support_of_ne_one h)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs : List α
w : xs.Nodup
i : ℕ
h : i < xs.length
⊢ xs.formPerm xs[i] = xs[(i + 1) % xs.length]

Tactic:
by
  rcases xs with - | ⟨x, xs⟩
  · simp at h
  · have : i ≤ xs.length := by
      refine Nat.le_of_lt_succ ?_
      simpa using h
    rcases this.eq_or_lt with (rfl | hn')
    · simp
    · rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]
      congr
      rw [Nat.mod_eq_of_lt]; simpa [Nat.succ_eq_add_one]

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

Goal state before:
pp: x y : Fin 1
⊢ x ≠ y → (swap x y).signAux = -1

Tactic:
by
    dsimp [signAux, swap, swapCore]
    simp only [eq_iff_true_of_subsingleton, not_true,
               IsEmpty.forall_iff]

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f

Tactic:
this,

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans 1).trans e) = signAux2 [] 1
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -signAux ((e.symm.trans (swap x (f x) * f)).trans e)

Tactic:
this,

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e
hefx : e x ≠ e (f x)
⊢ signAux ((e.symm.trans f).trans e) = -(swap (e x) (e (f x)) * (e.symm.trans f).trans e).signAux
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : (Multiset.replicate (n + 1) (orderOf σ)).sum < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle

Tactic:
Multiset.sum_replicate,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
n : ℕ
h2 : (n + 1) • orderOf σ < 2 * orderOf σ
hn : σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)
⊢ σ.IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
hc : c.support ⊆ s
n : ℤ
h : c.subtypePerm ⋯ ^ n = g.subtypePerm hg
x : α
hx : x ∉ s
⊢ (c ^ n) x = (ofSubtype (c.subtypePerm ⋯ ^ n)) x

Tactic:
rw [ofSubtype_apply_of_not_mem (subtypePerm c _ ^ n) hx,
        ← notMem_support]
      exact fun hx' ↦ hx (hc (support_zpow_le _ _ hx'))

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

Goal state before:
pp: n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
⊢ j.cycleRange i = if i = j then 0 else i + 1

Tactic:
have : (castLEEmb (by lia)).toEquivRange (castLT i (by lia)) = ⟨i, iin⟩ := by
    simp [coe_castLEEmb]; rfl

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⟩
⊢ j.cycleRange i = if i = j then 0 else i + 1
Module: Mathlib.Data.FunLike.Group

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
⊢ Function.Injective ⇑(coeMulHom F α β)

Tactic:
coe_coeMulHom

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : Mul F
inst✝¹ : Mul β
inst✝ : IsMulApply F α β
⊢ Function.Injective DFunLike.coe
Module: Mathlib.Data.FunLike.Module

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

Tactic:
simp [op_smul_eq_smul]

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

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

Tactic:
this,

Goal state after:
case pos
n : ℕ
i j : Fin n
inst✝ : NeZero n
h : i ≤ j
iin : i ∈ Set.range ⇑(castLEEmb ⋯)
this✝ : (castLEEmb ⋯).toEquivRange (i.castLT ⋯) = ⟨i, iin⟩
ch : i = j
this : (castLEEmb ⋯).toEquivRange.symm ⟨i, iin⟩ = last ↑j
⊢ ↑⟨(castLEEmb ⋯) ((finRotate (↑j + 1)) (last ↑j)), ⋯⟩ = 0
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc = (swap 0 i.succ) j.succ

pp: case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ

Tactic:
this,

Goal state after:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ j.succ = (swap 0 i.succ) j.succ

case succ.inl.h
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ (j + 1).castSucc < i.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
obtain ⟨hm₁, hm₂, hm₃⟩ := hm
        rw [hfg hx] at hm₁ ⊢
        rw [List.pairwise_cons]
        refine ⟨?_, fun g' hg' ↦ ?_, fun g' hg' y ↦ ?_, hm₃⟩
        · simp [List.prod_cons, hm₁]
        · exact ((List.mem_cons).1 hg').elim (fun hg' => hg'.symm ▸ isCycle_cycleOf _ hx) (hm₂ g')
        by_contra! ⟨hgy, hg'y⟩
        have hxy : SameCycle g x y := not_imp_comm.1 cycleOf_apply_of_not_sameCycle hgy
        have hg'm : g' :: m.erase g' ~ m := List.cons_perm_iff_perm_erase.2 ⟨hg', .refl _⟩
        have : ∀ h ∈ m.erase g', Disjoint g' h :=
          (List.pairwise_cons.1 ((hg'm.pairwise_iff Disjoint.symm).2 hm₃)).1
        refine hg'y <| (disjoint_prod_right _ this y).resolve_right ?_
        have hsc : SameCycle g⁻¹ x (g y) := by rwa [sameCycle_inv, sameCycle_apply_right]
        rw [disjoint_prod_perm hm₃ hg'm.symm, List.prod_cons, ← eq_inv_mul_iff_mul_eq] at hm₁
        simpa [hm₁, cycleOf_inv, hsc.cycleOf_apply, eq_symm_apply, eq_comm] using hg'y

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ σ.cycleType.sum = σ.cycleType.card * n

Tactic:
rw [hσ]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : 0 < n
hσ : σ.cycleType = Multiset.replicate σ.cycleType.card n
h : Even n
⊢ (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n
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 : α
ha : σ a = a
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
      rw [Finset.mem_compl, mem_support, Classical.not_not]

Goal state after:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
⊢ ∃ b, σ b = b ∧ b ≠ a
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign σ = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1

Tactic:
σ.sign_eq_prod_prod_Iio

Goal state after:
n : ℕ
σ : Perm (Fin n)
⊢ (∏ j, ∏ i < j, if σ i < σ j then 1 else -1) = ∏ i, ∏ j > i, if σ i < σ j then 1 else -1
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Multiset.replicate (Fintype.card α - #σ.support) 1).sum = Fintype.card α

Tactic:
Multiset.sum_replicate,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ #σ.support + (Fintype.card α - #σ.support) • 1 = Fintype.card α
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f = g

Tactic:
rw [← cycleFactorsFinset_noncommProd f]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.cycleFactorsFinset = g.cycleFactorsFinset
⊢ f.cycleFactorsFinset.noncommProd id ⋯ = g
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
ht : g.IsThreeCycle
⊢ _root_.orderOf g = 3

Tactic:
by
  rw [← lcm_cycleType, ht.cycleType, Multiset.lcm_singleton, normalize_eq]

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

Goal state before:
pp: case e'_2
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ i, ∏ j > i, f (σ i) (σ j) = ∏ j, ∏ i < j, f (σ i) (σ j)

pp: case e'_3
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ↑↑(sign σ) * ∏ i, ∏ j > i, f i j = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j

Tactic:
· apply Finset.prod_comm' (by simp)

Goal state after:
case e'_3
n : ℕ
R : Type u_1
inst✝ : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ↑↑(sign σ) * ∏ i, ∏ j > i, f i j = ↑↑(sign σ) * ∏ j, ∏ i < j, f i j
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: case intro
ι : 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 ι
⊢ (f fun i ↦ x i) = g fun i ↦ x i

Tactic:
rw [funext (fun i ↦ Eq.symm (DFinsupp.sum_single (f := x i)))]

Goal state after:
case intro
ι : 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 ι
⊢ (f fun i ↦ (fun i ↦ (x i).sum DFinsupp.single) i) = g fun i ↦ (fun i ↦ (x i).sum DFinsupp.single) 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
A : Matrix n n R
a b : R
h : A.IsDetpBalanced a b
s t : ℤˣ
⊢ a * detp s A + b * detp t A = b * detp s A + a * detp t A

Tactic:
by
  obtain rfl | rfl := Int.units_eq_one_or s <;> obtain rfl | rfl := Int.units_eq_one_or t
  · rw [add_comm]
  · rw [h]
  · rw [add_comm, ← h, add_comm]
  · rw [add_comm]

Goal state after:
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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B)

Tactic:
conv_rhs => rw [add_assoc]

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
hf : ∀ {s t : ℤˣ} {σ : Perm n}, σ ∈ ofSign s → ofSign (t * s) = Finset.map (mulRightEmbedding σ) (ofSign t)
ι : Perm n ↪ n → n := { toFun := fun e ↦ ⇑e, inj' := ⋯ }
hι : ∀ {σ : Perm n} {x : n}, ι σ x = σ x
bij : Finset (n → n) := Finset.map ι ((ofSign 1).disjUnion (ofSign (-1)) ⋯)
h :
  ∀ (s : ℤˣ),
    detp s (A * B) =
      ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign s, ∏ i, A i (σ i) * B (σ i) (τ i) + (detp 1 A * detp s B + detp (-1) A * detp (-s) B)
⊢ ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign 1, ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B + (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B)) =
    ∑ σ ∈ bijᶜ, ∑ τ ∈ ofSign (-1), ∏ i, A i (σ i) * B (σ i) (τ i) +
      (detp 1 A * detp (-1) B + detp (-1) A * detp 1 B + (detp 1 A * detp 1 B + detp (-1) A * detp (-1) B))
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 v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex e e') M).det = ((reindex e' e') ((reindex (e.trans e'.symm) (Equiv.refl m)) M)).det

pp: m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex e' e') ((reindex (e.trans e'.symm) (Equiv.refl m)) M)).det = ↑↑(sign (e'.trans e.symm)) * M.det

Tactic:
· congr 1; ext; simp

Goal state after:
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
e e' : m ≃ n
M : Matrix m m R
⊢ ((reindex e' e') ((reindex (e.trans e'.symm) (Equiv.refl m)) M)).det = ↑↑(sign (e'.trans e.symm)) * M.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
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
⊢ (vecMulVec u v).det = 0

Tactic:
this,

Goal state after:
n : Type u_2
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial n
u v : n → R
i j : n
hij : i ≠ j
uv' : Matrix n n R := ((vecMulVec u v).updateRow i v).updateRow j v
huv' : uv'.det = 0
this : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)
⊢ ((uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j)).det = 0
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
⊢ B i j + c i * B k j = B i j

Tactic:
this,

Goal state after:
case empty
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
c : n → R
hs : ∀ i ∉ ∅, c i = 0
k : n
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
this : ∀ (i : n), c i = 0
i j : n
⊢ B i j + 0 * B k j = B i j
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ f = g

Tactic:
suffices Equiv.ulift.{w₃}.invFun.comp f =
        Equiv.ulift.invFun.comp g by
      ext x
      simpa using congr_fun this x

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
hc : c.IsColimitCore
T : Type w₂
f g : c.pt → T
h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j
⊢ Equiv.ulift.invFun ∘ f = Equiv.ulift.invFun ∘ g
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
⊢ (m fun i_1 ↦ update v i (a + b) (σ i_1)) = (m fun i_1 ↦ update v i a (σ i_1)) + m fun i_1 ↦ update v i b (σ i_1)

Tactic:
let := σ.injective.decidableEq

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update v i (a + b) (σ i_1)) = (m fun i_1 ↦ update v i a (σ i_1)) + m fun i_1 ↦ update v i b (σ i_1)
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
⊢ (m fun i_1 ↦ update v i (a • b) (σ i_1)) = a • m fun i_1 ↦ update v i b (σ i_1)

Tactic:
let := σ.injective.decidableEq

Goal state after:
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
ι₁ : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
σ : ι₁ ≃ ι₂
m : MultilinearMap R (fun x ↦ M₂) M₃
inst✝ : DecidableEq ι₂
v : ι₂ → M₂
i : ι₂
a : R
b : M₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update v i (a • b) (σ i_1)) = a • m fun i_1 ↦ update v i b (σ i_1)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * (-1) ^ ↑i * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det

Tactic:
this,

Goal state after:
case refine_2
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i✝ : Fin n.succ
x✝ : i✝ ∈ univ
i : Fin n
this : (-1) ^ ↑i = ↑↑(sign i.cycleRange)
⊢ ∑ y, sign (decomposeFin.symm (i.succ, y)) • ∏ x, A ((decomposeFin.symm (i.succ, y)) x) x =
    -1 * ↑↑(sign i.cycleRange) * A i.succ 0 * (of fun i_1 j ↦ A (i.succ.succAbove i_1) j.succ).det
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ A.det = (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)

Tactic:
this,

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
this : A.det = (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det
⊢ (-1) ^ ↑i * ↑↑(sign i.cycleRange⁻¹) * A.det =
    (-1) ^ ↑i * ∑ i_1, (-1) ^ ↑i_1 * (A i i_1 * (A.submatrix i.succAbove i_1.succAbove).det)