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

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

Tactic:
ext

Goal state after:
n : ℕ
α : Type u_1
a : α
x : Fin n → α
p x✝ : Fin (n + 1)
⊢ (cons a x ∘ ⇑p.cycleRange) x✝ = p.insertNth a x x✝
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case intro
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ σ ∈ l ↔ ∀ (a : α), σ a ≠ a → σ a = l.prod a

Tactic:
constructor

Goal state after:
case intro.mp
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ σ ∈ l → ∀ (a : α), σ a ≠ a → σ a = l.prod a

case intro.mpr
α : Type u_4
inst✝ : Finite α
l : List (Perm α)
h1 : ∀ σ ∈ l, σ.IsCycle
h2 : List.Pairwise Disjoint l
σ : Perm α
h3 : σ.IsCycle
val✝ : Fintype α
⊢ (∀ (a : α), σ a ≠ a → σ a = l.prod a) → σ ∈ l
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : 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
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ l'.toFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

Tactic:
constructor

Goal state after:
case mp
α : 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
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ l'.toFinset = l.toFinset → (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ

case mpr
α : 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
ht : σ.cycleFactorsFinset = l'.toFinset
⊢ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Disjoint l ∧ l.prod = σ → l'.toFinset = l.toFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
⊢ ∃ x, orderOf x = p

Tactic:
have hv₀ : σ v₀ = v₀ := Subtype.ext (Subtype.ext (List.rotate_replicate (1 : G) p 1))

Goal state after:
G : Type u_3
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ∣ Fintype.card G
hp' : p - 1 ≠ 0
Scard : p ∣ Fintype.card ↑(vectorsProdEqOne G p)
f : ℕ → ↑(vectorsProdEqOne G p) → ↑(vectorsProdEqOne G p) := fun k v ↦ VectorsProdEqOne.rotate v k
hf1 : ∀ (v : ↑(vectorsProdEqOne G p)), f 0 v = v
hf2 : ∀ (j k : ℕ) (v : ↑(vectorsProdEqOne G p)), f k (f j v) = f (j + k) v
hf3 : ∀ (v : ↑(vectorsProdEqOne G p)), f p v = v
σ : ↑(vectorsProdEqOne G p) ≃ ↑(vectorsProdEqOne G p) :=
  { toFun := f 1, invFun := f (p - 1), left_inv := ⋯, right_inv := ⋯ }
hσ : σ ^ p ^ 1 = 1
v₀ : ↑(vectorsProdEqOne G p) := ⟨List.Vector.replicate p 1, ⋯⟩
hv₀ : σ v₀ = v₀
⊢ ∃ x, orderOf x = p
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) ↔ x ∈ f.support

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ ((f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a) → x ∈ f.support

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
⊢ x ∈ f.support → (f.cycleOf x).IsCycle ∧ ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
hc : (f.cycleOf x).IsCycle
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
⊢ x ∈ f.support

Tactic:
contrapose hc

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
right✝ : ∀ a ∈ (f.cycleOf x).support, (f.cycleOf x) a = f a
hc : x ∉ f.support
⊢ ¬(f.cycleOf x).IsCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support ↔ ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ x ∈ g.support → ∃ c ∈ g.cycleFactorsFinset, x ∈ c.support

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
x : α
⊢ (∃ c ∈ g.cycleFactorsFinset, x ∈ c.support) → x ∈ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

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

Tactic:
disjoint_iff_disjoint_support

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : _root_.Disjoint f.support g.support
⊢ _root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsSwap ↔ σ.cycleType = {2}

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.IsSwap → σ.cycleType = {2}

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = {2} → σ.IsSwap
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ d x ∈ c.support ↔ x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ c (d x) = d x ↔ c x = x
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ g.support = {a, g a, g (g a)} → a ∈ g.support

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g.support = {a, g a, g (g a)}
Module: Mathlib.GroupTheory.Perm.Cycle.Type

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

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ [a, g a, g (g a)].Nodup → a ∈ g.support

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → [a, g a, g (g a)].Nodup
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:
constructor

Goal state after:
case mp
α : 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

case mpr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
a : α
hg3 : g.IsThreeCycle
⊢ a ∈ g.support → g = swap a (g a) * swap (g a) (g (g a))
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
    dsimp
    simp_rw [Function.apply_update (fun i m => m (p i)) m, DFinsupp.add_apply, (f p).map_update_add]

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

Goal state after:
ι : 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✝
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:
ext

Goal state after:
ι : 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✝
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:
ext

Goal state after:
ι : 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✝
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
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
⊢ compLinearMap 0 g = 0

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ (compLinearMap 0 g) x✝ = 0 x✝
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
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
x✝ : ι → M₂
⊢ ((f₁ + f₂).compLinearMap g) x✝ = (f₁.compLinearMap g + f₂.compLinearMap g) x✝
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
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
⊢ f.compLinearMap 0 = 0

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M₂
⊢ (f.compLinearMap 0) x✝ = 0 x✝
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M
⊢ (domDomCongr σ.symm (domDomCongr σ f)) x✝ = f x✝
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
M₃ : Type u_11
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
x✝ : ι' → M
⊢ (domDomCongr σ (domDomCongr σ.symm m)) x✝ = m x✝
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
⊢ domDomCongr σ.symm (domDomCongr σ f) = f

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f✝ f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
f : M [⋀^ι]→ₗ[R] N
x✝ : ι → M
⊢ (domDomCongr σ.symm (domDomCongr σ f)) x✝ = f x✝
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
⊢ domDomCongr σ (domDomCongr σ.symm m) = m

Tactic:
ext

Goal state after:
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
M₂ : Type u_10
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M₂
M₃ : Type u_11
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M₃
f f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
S : Type u_12
inst✝² : Semiring S
inst✝¹ : Module S N
inst✝ : SMulCommClass R S N
σ : ι ≃ ι'
m : M [⋀^ι']→ₗ[R] N
x✝ : ι' → M
⊢ (domDomCongr σ (domDomCongr σ.symm m)) x✝ = m x✝
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ (let __src := ∑ σ, Perm.sign σ • domDomCongr σ 0;
    { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ 0), map_update_add' := ⋯, map_update_smul' := ⋯,
      map_eq_zero_of_eq' := ⋯ }) =
    0

Tactic:
ext

Goal state after:
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
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x✝ : ι → M
⊢ (let __src := ∑ σ, Perm.sign σ • domDomCongr σ 0;
      { toFun := ⇑(∑ σ, Perm.sign σ • domDomCongr σ 0), map_update_add' := ⋯, map_update_smul' := ⋯,
        map_eq_zero_of_eq' := ⋯ })
      x✝ =
    0 x✝