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

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

Tactic:
rw [mul_apply, mul_apply]

Goal state after:
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : ⟨a, b⟩ ∈ finPairsLT n
⊢ (if f (g a) ≤ f (g b) then -1 else 1) =
    (if
          f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            f (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1) *
      if
          g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).fst ≤
            g⁻¹ (if x : g b < g a then ⟨g a, g b⟩ else ⟨g b, g a⟩).snd then
        -1
      else 1
Module: Mathlib.GroupTheory.Perm.Sign

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

Tactic:
rcases a₂.zero_le.eq_or_lt with (rfl | H')

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

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((σ ^ (n + 1)) x) ((σ ^ (n + 1 + 1)) x) = swap (σ ((σ ^ n) x)) (σ ((σ ^ (n + 1)) x)) * σ * σ⁻¹

Tactic:
mul_inv_cancel_right,

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
h1 : σ.IsCycle
h2 : σ.support = univ
x : α
H : Subgroup (Perm α) := closure {σ, swap x (σ x)}
h3 : σ ∈ H
h4 : swap x (σ x) ∈ H
n : ℕ
ih : swap ((σ ^ n) x) ((σ ^ (n + 1)) x) ∈ H
⊢ swap ((σ ^ (n + 1)) x) ((σ ^ (n + 1 + 1)) x) = swap (σ ((σ ^ n) x)) (σ ((σ ^ (n + 1)) x))
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ (g * p) x = p x ↔ g x = x

Tactic:
← hp,

Goal state after:
α : Type u
g p : Perm α
x : α
hp : p * g = g * p
⊢ (p * g) x = p x ↔ g x = x
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
⊢ swap x (f x) * f = 1

Tactic:
simp only [mul_def, one_def]

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
⊢ Equiv.trans f (swap x (f x)) = Equiv.refl α
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
h : swap x (f x) * f = 1
⊢ Perm.sign (swap x (f x) * (swap x (f x) * f)) = -(-1) ^ #f.support

Tactic:
rw [sign_mul, sign_swap hx.1.symm, h, sign_one,
          hf.eq_swap_of_apply_apply_eq_self hx.1 h1, card_support_swap hx.1.symm]

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
h : swap x (f x) * f = 1
⊢ -1 * 1 = -(-1) ^ 2
Module: Mathlib.GroupTheory.NoncommPiCoprod

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Type u_2
H : ι → Subgroup G
inst✝ : Fintype ι
hcomm : Pairwise fun i j ↦ ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : iSupIndep H
⊢ Function.Injective ⇑(noncommPiCoprod hcomm)

Tactic:
by
  apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
  · simpa using hind
  · intro i
    exact Subtype.coe_injective

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

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

pp: case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)

Tactic:
hrec hs'

Goal state after:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (k i).cycleType + ∑ i ∈ s, (k i).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ((↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)) →
    ∀ (hs' : (↑s).Pairwise fun i j ↦ Commute (k i) (k j)), (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j ↦ (k i).Disjoint (k j)
hs'✝ : (↑(insert i s)).Pairwise fun i j ↦ Commute (k i) (k j)
hs' : (↑s).Pairwise fun i j ↦ (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
this :
  ((addNatEmb (n - (n - ↑i))).trans (finCongr ⋯).toEmbedding).toEquivRange.symm ⟨k, kin⟩ = subNat (↑i) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
simp [hik]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = x
n : ℤ
hn : (fun x ↦ ↑d ^ x) n = y
⊢ (↑c ^ m).Disjoint (↑d ^ n)

Tactic:
apply Disjoint.zpow_disjoint_zpow

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : ↥f.cycleFactorsFinset
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = x
n : ℤ
hn : (fun x ↦ ↑d ^ x) n = y
⊢ (↑c).Disjoint ↑d
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k g : Perm α
hk : ∀ c ∈ g.cycleFactorsFinset, Commute k c
⊢ Commute k g

Tactic:
rw [← cycleFactorsFinset_noncommProd g (cycleFactorsFinset_mem_commute g)]
  apply Finset.noncommProd_commute
  simpa only [id_eq] using hk

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
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))

Tactic:
exact h _ _

Goal state after:
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₂
k n : ℕ
f : MultilinearMap R (fun x ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst : DecidableEq (Fin k)] (m : Fin k → M') (i : Fin k) (x y : M'),
    (f fun j ↦ if h : j ∈ s then update m i (x + y) ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) =
      (f fun j ↦ if h : j ∈ s then update m i x ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) +
        f fun j ↦ if h : j ∈ s then update m i y ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z

Tactic:
by
    simp [dite_comp_equiv_update (s.orderIsoOfFin hk).symm]

Goal state after:
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₂
k n : ℕ
f : MultilinearMap R (fun x ↦ M') M₂
s : Finset (Fin n)
hk : #s = k
z : M'
⊢ ∀ [inst : DecidableEq (Fin k)] (m : Fin k → M') (i : Fin k) (c : R) (x : M'),
    (f fun j ↦ if h : j ∈ s then update m i (c • x) ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z) =
      c • f fun j ↦ if h : j ∈ s then update m i x ((s.orderIsoOfFin hk).symm ⟨j, h⟩) else z

Tactic:
by
    simp [dite_comp_equiv_update (s.orderIsoOfFin hk).symm]

Goal state after:
Module: Mathlib.Algebra.BrauerGroup.Defs

Goal state before:
pp: K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hBC : IsBrauerEquivalent B C
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgCat
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨p, q, hp, hq, ⟨iso2⟩⟩ := hBC

Goal state after:
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgCat
⊢ IsBrauerEquivalent A C
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
C : update (t.piecewise (m + m') m') i (m i) = t.piecewise (m + m'') m''
s : Finset ι
hs : s ∈ t.powerset
j : ι
h : j = i
⊢ (insert i s).piecewise m m' j = s.piecewise m m'' j

Tactic:
rw [h]
      simp [m'', Finset.notMem_of_mem_powerset_of_notMem hs hit]

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
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign (t * s) ↔ ∃ a ∈ ofSign t, a = τ * σ⁻¹

Tactic:
exists_eq_right,

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
s t : ℤˣ
σ : Perm n
hσ : σ ∈ ofSign s
τ : Perm n
⊢ τ ∈ ofSign (t * s) ↔ τ * σ⁻¹ ∈ ofSign t
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 : n
⊢ ∀ (j : n), IsAddUnit ((detp s A • (B * adjp t B)) i j)

Tactic:
j

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 : n
⊢ IsAddUnit ((detp s A • (B * adjp t B)) i j)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case refine_2._hsucc
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
⊢ ∀ (j : Fin n.succ), M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j

Tactic:
j

Goal state after:
case refine_2._hsucc
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
⊢ M' i.succ j = N i.succ j + update c k 0 i * M' i.castSucc j
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₂
this : DecidableEq ι₁ := ⋯.decidableEq
⊢ (m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) (a • b) i_1) = a • m fun i_1 ↦ update (v ∘ ⇑σ) (σ.symm i) b i_1

Tactic:
rw [m.map_update_smul]

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

Goal state before:
pp: case convert_2
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
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ x ∈ univ, x ∉ (↑(sumCongrHom m n).range).toFinset → ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i = 0

Tactic:
· rintro σ - hσn
      have h1 : ¬∀ x, ∃ y, Sum.inl y = σ (Sum.inl x) := by
        rw [Set.mem_toFinset] at hσn
        simpa only [Set.MapsTo, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff] using
          mt mem_sumCongrHom_range_of_perm_mapsTo_inl hσn
      obtain ⟨a, ha⟩ := not_forall.mp h1
      rcases hx : σ (Sum.inl a) with a2 | b
      · have hn := (not_exists.mp ha) a2
        exact absurd hx.symm hn
      · rw [Finset.prod_eq_zero (Finset.mem_univ (Sum.inl a)), mul_zero]
        rw [hx, fromBlocks_apply₂₁, zero_apply]

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i ∈ Finset.univ.erase i, c) • f (update m i x)
⊢ f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • f (update m i x)

Tactic:
simpa [← Function.update_smul c m] using this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Creates

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₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  (IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (h.inv.app j) ≫ F.map (h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j

Tactic:
rw [← F.map_comp_assoc]

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
K K₁ K₂ : J ⥤ C
F : C ⥤ D
h : K₁ ≅ K₂
inst✝ : CreatesColimit K₁ F
c : Cocone (K₂ ⋙ F)
t : IsColimit c
t' : IsColimit ((Cocone.precompose (isoWhiskerRight h F).hom).obj c) :=
  (IsColimit.precomposeHomEquiv (isoWhiskerRight h F) c).symm t
j : J
⊢ (F.map (h.inv.app j ≫ h.hom.app j) ≫ c.ι.app j) ≫ 𝟙 c.pt = c.ι.app j
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
⊢ IsLimit (limitCone F)

Tactic:
refine IsLimit.ofFaithful (forget MonCat) (Types.Small.limitConeIsLimit.{v, u} _)
    (fun s => ofHom { toFun := _, map_one' := ?_, map_mul' := ?_ }) (fun s => rfl)
  · simp
    rfl
  · intro x y
    simp [← equivShrink_mul]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ (bifunctorComp₁₂ F₁₂ G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      (bifunctorComp₁₂ F₁₂ G').map f

Tactic:
ext X₂ X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G G' : C₁₂ ⥤ C₃ ⥤ C₄
φ : G ⟶ G'
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ (((bifunctorComp₁₂ F₁₂ G).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj Y₁).obj X₂)).app X₃, naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app ((F₁₂.obj X₁).obj X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
              (bifunctorComp₁₂ F₁₂ G').map f).app
          X₂).app
      X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₁₂FunctorObj F₁₂).obj G).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₁₂FunctorObj F₁₂').obj G).map f

Tactic:
ext X₂ X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F₁₂ F₁₂' : C₁ ⥤ C₂ ⥤ C₁₂
φ : F₁₂ ⟶ F₁₂'
G : C₁₂ ⥤ C₃ ⥤ C₄
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ ((((bifunctorComp₁₂FunctorObj F₁₂).obj G).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app Y₁).app X₂)).app X₃, naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (G.map ((φ.app X₁).app X₂)).app X₃, naturality := ⋯ }, naturality := ⋯ } ≫
              ((bifunctorComp₁₂FunctorObj F₁₂').obj G).map f).app
          X₂).app
      X₃
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ ((bifunctorComp₂₃FunctorObj F).obj G₂₃).map f ≫
      { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } =
    { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } ≫
      ((bifunctorComp₂₃FunctorObj F').obj G₂₃).map f

Tactic:
ext X₂ X₃

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F F' : C₁ ⥤ C₂₃ ⥤ C₄
φ : F ⟶ F'
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
X₂ : C₂
X₃ : C₃
⊢ ((((bifunctorComp₂₃FunctorObj F).obj G₂₃).map f ≫
              { app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app Y₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ },
                naturality := ⋯ }).app
          X₂).app
      X₃ =
    (({ app := fun X₂ ↦ { app := fun X₃ ↦ (φ.app X₁).app ((G₂₃.obj X₂).obj X₃), naturality := ⋯ }, naturality := ⋯ } ≫
              ((bifunctorComp₂₃FunctorObj F').obj G₂₃).map f).app
          X₂).app
      X₃