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

Goal state before:
pp: α : 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
⊢ x ≠ g x

Tactic:
by

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

Goal state before:
pp: α : 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
⊢ x ≠ g (g x)

Tactic:
by

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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
s : (i : ι) → { s // ∀ (i_1 : κ i), i_1 ∈ s ∨ (x i).toFun i_1 = 0 }
p : (i : ι) → κ i
⊢ p ∈ Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i ↦ ↑(s i)) ∨ ((f p) fun i ↦ (x i) (p i)) = 0

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (x + y) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (x + y) i_1).support') }
      p =
    ({ toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') } +
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i y i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i y i_1).support') })
      p

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
c : R
x : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i (c • x) i_1) (p i_1),
        support' :=
          Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
            (Trunc.finChoice fun i_1 ↦ (Function.update m i (c • x) i_1).support') }
      p =
    (c •
        { toFun := fun p ↦ (f p) fun i_1 ↦ (Function.update m i x i_1) (p i_1),
          support' :=
            Trunc.map (fun s ↦ ⟨Multiset.map (fun f i ↦ f i ⋯) (Finset.univ.val.pi fun i_1 ↦ ↑(s i_1)), ⋯⟩)
              (Trunc.finChoice fun i_1 ↦ (Function.update m i x i_1).support') })
      p

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b c : α
ab : a ≠ b
ac : a ≠ c
⊢ swap a b * swap a c ∈ closure {σ | σ.IsThreeCycle}

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : ¬a = c
⊢ swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d)

Tactic:
by

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)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ((dfinsuppFamily f) x).support ⊆ Fintype.piFinset fun i ↦ (x i).support

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hσ : σ.IsSwap
hτ : τ.IsSwap
⊢ σ * τ ∈ closure {σ | σ.IsThreeCycle}

Tactic:
by

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
⊢ (swap x y * swap z t).cycleType = {2, 2}

Tactic:
by

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)
inst✝ : (i : ι) → DecidableEq (κ i)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
p : (i : ι) → κ i
m : (i : ι) → M i (p i)
⊢ ((dfinsuppFamily f) fun i ↦ DFinsupp.single (p i) (m i)) = DFinsupp.single p ((f p) m)

Tactic:
by

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

Goal state before:
pp: ι : 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)
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → κ i →₀ R
⊢ (freeFinsuppEquiv (Finsupp.single p r)) x = r • Finsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by

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

Goal state before:
pp: ι : 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 ι'
f : ((i : ι) → κ i) × ι' →₀ R
x : (i : ι) → κ i →₀ R
⊢ (freeFinsuppEquiv f) x = ∑ p, f p • Finsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by

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)
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 = DFinsupp.single p (f fun i ↦ (x i) (p i))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : 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)
⊢ f = g

Tactic:
by

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)
⊢ dfinsuppFamily 0 = 0

Tactic:
by

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

Goal state before:
pp: ι : 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)
κ : ι → Type u_5
b : (i : ι) → Basis (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
b' : Basis ι' R N
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), Finite (κ i)
i : ((i : ι) → κ i) × ι'
⊢ (multilinearMap b b') i =
    (LinearMap.id.smulRight (b' i.2)).compMultilinearMap
      ((MultilinearMap.mkPiRing R ι 1).compLinearMap fun i' ↦ (b i').coord (i.1 i'))

Tactic:
by

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)
⊢ dfinsuppFamily (f + g) = dfinsuppFamily f + dfinsuppFamily g

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), z x ∈ c.support ↔ x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
by

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

Goal state before:
pp: ι : 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)
κ : ι → Type u_5
b : (i : ι) → Basis (κ i) R (M i)
ι' : Type u_6
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
b' : Basis ι' R N
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), Finite (κ i)
ii : ((i : ι) → κ i) × ι'
v : (i : ι) → M i
⊢ ((multilinearMap b b') ii) v = (∏ i, ((b i).repr (v i)) (ii.1 i)) • b' ii.2

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ g.subtypePerm ⋯ = c.subtypePermOfSupport

Tactic:
by

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)
⊢ dfinsuppFamily (s • f) = s • dfinsuppFamily f

Tactic:
by

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)
⊢ ((LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x ↦ LinearMap.id) ∘ₗ dfinsuppFamilyₗ) ∘ₗ
      LinearMap.pi fun p ↦ compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i)) =
    LinearMap.id

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g k c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute k c ↔
    ∃ (hc' : ∀ (x : α), k x ∈ c.support ↔ x ∈ c.support), k.subtypePerm hc' ∈ Subgroup.zpowers (g.subtypePerm ⋯)

Tactic:
by

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)
⊢ (LinearMap.pi fun p ↦ compLinearMapₗ fun i ↦ DFinsupp.lsingle (p i)) ∘ₗ
      LinearMap.compMultilinearMapₗ R ((DFinsupp.lsum ℕ) fun x ↦ LinearMap.id) ∘ₗ dfinsuppFamilyₗ =
    LinearMap.id

Tactic:
by

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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N
p : (i : ι) → κ i
x : (i : ι) → M i (p i)
⊢ (((fromDFinsuppEquiv κ R) f) fun i ↦ DFinsupp.single (p i) (x i)) = (f p) x

Tactic:
by

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
⊢ ((fromDFinsuppEquiv κ R) f) x = ∑ p ∈ Fintype.piFinset fun i ↦ (x i).support, (f p) fun i ↦ (x i) (p i)

Tactic:
by

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

Goal state before:
pp: ι : 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 ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
this : ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i)
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) j = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) j

Tactic:
by

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

Goal state before:
pp: ι : 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 ι'
p : ((i : ι) → κ i) × ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
⊢ (freeDFinsuppEquiv (DFinsupp.single p r)) x = r • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by

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

Goal state before:
pp: ι : 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 f) x = ∑ p, f p • DFinsupp.single p.2 (∏ i, (x i) (p.1 i))

Tactic:
by

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 g : MultilinearMap R M₁ M₂
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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 ι
f : ((i : ι) → M₁ i) → M₂
h₁ : ∀ (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)
h₂ : ∀ (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i), f (update m i (c • x)) = c • f (update m i x)
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:
by

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

Tactic:
by

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:
by

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
⊢ f m = 0

Tactic:
by

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₂
inst✝ : Nonempty ι
⊢ f 0 = 0

Tactic:
by

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 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 + y)) =
    f (update m i x) + f' (update m i x) + (f (update m i y) + f' (update m i y))

Tactic:
by

Goal state after: