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

Goal state before:
pp: case succ
n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
i✝ : Fin n
⊢ p.insertNth a x ((Equiv.symm p.cycleRange) i✝.succ) = cons a x i✝.succ

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Type u_1
p : Fin (n + 1)
a : α
x : Fin n → α
j : Fin (n + 1)
⊢ (p.insertNth a x ∘ ⇑(Equiv.symm p.cycleRange)) j = cons a x j

Tactic:
simp

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

Goal state before:
pp: n : ℕ
α : Type u_1
a : α
x : Fin n → α
p x✝ : Fin (n + 1)
⊢ (cons a x ∘ ⇑p.cycleRange) x✝ = p.insertNth a x x✝

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ {↑2 + 1} = {3}

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
simp

Goal state after:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ i ≤ k
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))))

Tactic:
simp

Goal state after:
n : ℕ
i j k : Fin n
h : j < k
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑k - ↑i + (n - (n - ↑i))
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
h : j < k
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) ⋯
⊢ ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i)))) = ↑k

Tactic:
simp

Goal state after:
n : ℕ
i j k : Fin n
h : j < k
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) ⋯
⊢ ↑k - ↑i + (n - (n - ↑i)) = ↑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 ⋯)
⊢ ↑i ≤ ↑(Fin.cast ⋯ k)

Tactic:
simp

Goal state after:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ i ≤ 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 ⋯)
⊢ ↑k = ↑(Fin.cast ⋯ ((subNat (↑i) (Fin.cast ⋯ k) ⋯).addNat (n - (n - ↑i))))

Tactic:
simp

Goal state after:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst✝ : NeZero n
hij : i ≤ j
kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)
⊢ ↑k = ↑k - ↑i + (n - (n - ↑i))
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
⊢ (Multiset.replicate σ.cycleType.card n).sum = (Multiset.replicate σ.cycleType.card n).card * n

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
obtain ⟨⟨l', hp', hc', hd'⟩, hl⟩ := Trunc.exists_rep σ.truncCycleFactors

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
⊢ σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case inl
n : ℕ
i : Fin n
inst✝ : NeZero n
k : Fin n
ch : k < i
⊢ ↑((i.cycleIcc i) k) = ↑k

Tactic:
simp [-cycleIcc_def_le, cycleIcc_of_lt, ch]

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ sign 1 = signAux 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Iio x ↔ x ∈ Finset.Ioi y ∧ y ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Finite α
σ : Perm α
h : σ.IsSwap
⊢ _root_.orderOf σ = 2

Tactic:
by
  have := Fintype.ofFinite α
  rw [← lcm_cycleType, isSwap_iff_cycleType.mp h, Multiset.lcm_singleton, normalize_eq]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : σ.IsThreeCycle
⊢ σ ≠ 1

Tactic:
rintro rfl
  simpa using h.cycleType

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

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : f.IsCycle ∧ ∀ a ∈ f.support, f a = g a
x : α
hx : ¬f x = x
⊢ f (f⁻¹ x) = x

Tactic:
simp

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
⊢ f.cycleOf a = c.cycleOf a

Tactic:
let hfc2 := Perm.Disjoint.commute hfc

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)
hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc
⊢ f.cycleOf a = c.cycleOf a
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹.IsThreeCycle → f.IsThreeCycle

Tactic:
rw [← inv_inv f]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
⊢ f⁻¹⁻¹⁻¹.IsThreeCycle → f⁻¹⁻¹.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
simp

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

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

Tactic:
hf

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g f✝ σ : Perm α
hσ : σ.IsCycle
f : Perm α
hf : f ∈ σ.cycleFactorsFinset
⊢ (σ * f⁻¹).cycleFactorsFinset = σ.cycleFactorsFinset \ {f}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case mpr.h₂
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
ha : ¬g a = a
⊢ 3 ≤ #{g (g a)} + 1 + 1

Tactic:
simp

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

Goal state before:
pp: 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
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Ioi x ↔ x ∈ Finset.Iio y ∧ y ∈ Finset.univ

Tactic:
simp

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

Goal state before:
pp: 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
⊢ ∀ (x y : Fin n), x ∈ Finset.univ ∧ y ∈ Finset.Iio x ↔ x ∈ Finset.Ioi y ∧ y ∈ Finset.univ

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
q : (i : ι) → κ i
m : (i : ι) → M i (q i)
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (q i) (m i)) q = (DFinsupp.single q ((f q) m)) q

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y z t : α
h : [x, y, z, t].Nodup
⊢ {2} + {2} = {2, 2}

Tactic:
simp

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

Goal state before:
pp: case zero
ι : Type u_1
ι' : Type u_2
R : Type u_3
κ : ι → Type u_4
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : CommSemiring R
inst✝⁴ : DecidableEq R
inst✝³ : DecidableEq ι'
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : Fintype ι'
x : (i : ι) → κ i →₀ R
⊢ (freeFinsuppEquiv 0) x = ∑ p, 0 p • Finsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ((dfinsuppFamily (Pi.single p f)) x) p = (DFinsupp.single p (f fun i ↦ (x i) (p i))) p

Tactic:
simp

Goal state after:
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 ι
x : (i : ι) → ιM i →₀ R
⊢ (f fun i ↦ ∑ x_1 ∈ (x i).support, (x i) x_1 • (e i) x_1) = g fun i ↦ ∑ x_1 ∈ (x i).support, (x i) x_1 • (e i) x_1

Tactic:
map_sum_finset,

Goal state after:
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 ι
x : (i : ι) → ιM i →₀ R
⊢ (∑ r ∈ Fintype.piFinset fun i ↦ (x i).support, f fun i ↦ (x i) (r i) • (e i) (r i)) =
    ∑ r ∈ Fintype.piFinset fun i ↦ (x i).support, g fun i ↦ (x i) (r i) • (e i) (r i)
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily 0) x✝) i✝ = (0 x✝) i✝

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (f + g)) x✝) i✝ = ((dfinsuppFamily f + dfinsuppFamily g) x✝) i✝

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (s • f)) x✝) i✝ = ((s • dfinsuppFamily f) x✝) i✝

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N✝ : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N✝ p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N✝ p)
N : Type u_1
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f : MultilinearMap R (fun i ↦ Π₀ (j : κ i), M i j) N
x : (i : ι) → κ i
x✝ : (i : ι) → M i (x i)
⊢ ((((LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x ↦ LinearMap.id) ∘ₗ dfinsuppFamilyₗ) ∘ₗ
              LinearMap.pi fun p ↦ compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i))
            f).compLinearMap
        fun i ↦ DFinsupp.lsingle (x i))
      x✝ =
    ((LinearMap.id f).compLinearMap fun i ↦ DFinsupp.lsingle (x i)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N✝ : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : CommSemiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N✝ p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N✝ p)
N : Type u_1
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N
p : (i : ι) → κ i
a : (i : ι) → M i (p i)
⊢ (((LinearMap.pi fun p ↦ compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i)) ∘ₗ
          LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x ↦ LinearMap.id) ∘ₗ dfinsuppFamilyₗ)
        f p)
      a =
    (LinearMap.id f p) a

Tactic:
simp

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
N : Type u_1
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ∀ x_1 ∈ Fintype.piFinset fun i ↦ (x i).support,
    x_1 ∉ ((dfinsuppFamilyₗ f) x).support →
      (fun x ↦ ⇑((fun x ↦ LinearMap.id) x).toAddMonoidHom) x_1 (((dfinsuppFamilyₗ f) x) x_1) = 0

Tactic:
simp

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

Goal state before:
pp: case h0
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → Fintype (κ i)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : DecidableEq ι'
inst✝ : Fintype ι'
f : Π₀ (x : ((i : ι) → κ i) × ι'), R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv 0) x = ∑ p, 0 p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
simp

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

Goal state before:
pp: R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M₁ i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : ι) → Module R (M₁ i)
inst✝ : Module R M₂
f : MultilinearMap R M₁ M₂
m : (i : ι) → M₁ i
i : ι
h : m i = 0
⊢ 0 • 0 = 0

Tactic:
simp

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₂
inst✝ : DecidableEq ι
x✝³ : (i : ι) → M₁ i
x✝² : ι
x✝¹ x✝ : M₁ x✝²
⊢ 0 = 0 + 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ι : Type u_7
f : (ι → M) → N
h₁ :
  ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M), f (update m i (x + y)) = f (update m i x) + f (update m i y)
h₂ : ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M), f (update m i (c • x)) = c • f (update m i x)
h₃ :
  ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯ }.toFun v = 0
⊢ ↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ } =
    { toFun := f, map_update_add' := h₁, map_update_smul' := h₂ }

Tactic:
simp

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₂
inst✝ : DecidableEq ι
x✝² : (i : ι) → M₁ i
x✝¹ : ι
c : R
x✝ : M₁ x✝¹
⊢ 0 = c • 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
P : Type u_4
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M' : Type u_5
inst✝³ : AddCommGroup M'
inst✝² : Module R M'
N' : Type u_6
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
x✝⁴ : ι → M
x✝³ x✝² : ι
x✝¹ : x✝⁴ x✝³ = x✝⁴ x✝²
x✝ : x✝³ ≠ x✝²
⊢ MultilinearMap.toFun 0 x✝⁴ = 0

Tactic:
simp

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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ f (update m i (x + y)) = f (update m i x) + f (update m i y)

Tactic:
simp

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₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ f (update m i (c • x)) = (RingHom.id R) c • f (update m i x)

Tactic:
simp

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' f : MultilinearMap R M₁ M₂
g : MultilinearMap R M₁ M₃
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
x y : M₁ i
⊢ (f (update m i (x + y)), g (update m i (x + y))) =
    (f (update m i x), g (update m i x)) + (f (update m i y), g (update m i y))

Tactic:
simp

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' f : MultilinearMap R M₁ M₂
g : MultilinearMap R M₁ M₃
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ (f (update m i (c • x)), g (update m i (c • x))) = c • (f (update m i x), g (update m i x))

Tactic:
simp

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

Goal state before:
pp: case one
R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → M
⊢ g (v ∘ ⇑1) = Equiv.Perm.sign 1 • g v

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N' : Type u_6
inst✝³ : AddCommGroup N'
inst✝² : Module R N'
ι : Type u_7
g : M [⋀^ι]→ₗ[R] N'
v : ι → M
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
σ : Equiv.Perm ι
⊢ g v = (Equiv.Perm.sign σ * Equiv.Perm.sign σ) • g v

Tactic:
simp

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
s : ℤˣ
A : Matrix n n R
⊢ ∀ (i : Perm n), i ∈ ofSign s ↔ (Equiv.inv (Perm n)) i ∈ ofSign s

Tactic:
simp

Goal state after: