awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
ι : Type u_7
ι₁ : Type u_10
inst : Finite ι
R' : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst_1 : CommSemiring R'
inst_2 : AddCommMonoid N₁
inst_3 : AddCommMonoid N₂
inst_4 : Module R' N₁
inst_5 : Module R' N₂
f g : N₁ [⋀^ι]→ₗ[R'] N₂
e : Basis ι₁ R' N₁
h :
  ∀ (v : ι → ι₁),
    Function.Injective v →
      Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
        ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i) : N₂)
v : (i : ι) → ι₁
hi : ¬Function.Injective v
this : ¬Function.Injective.{u_7 + 1, u_12 + 1} (β := N₁) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i)
neg :
  Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
neg₁ :
  Eq.{u_13 + 1} (α := N₂) ((f : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
    ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
neg₂ :
  Eq.{u_13 + 1} (α := N₂) (0 : N₂)
    ((g : (a : ι → N₁) → N₂) fun (i : ι) ↦ ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) : N₂)
neg₃ neg₄ : Eq.{u_13 + 1} (α := N₂) 0 0
⊢ Eq.{u_13 + 1} (α := N₂)
    (((↑f : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)
    (((↑g : MultilinearMap R' (fun (x : ι) ↦ N₁) N₂) : (a : (i : ι) → N₁) → N₂) fun (i : ι) ↦
        ((fun (x : ι) ↦ e) i : (a : ι₁) → N₁) (v i) :
      N₂)

Tactic:
rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
      g.map_eq_zero_of_not_injective _ this]

Premises used: AlternatingMap.map_eq_zero_of_not_injective, AlternatingMap.coe_multilinearMap
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x x_1 : M'' [⋀^ι]→ₗ[R'] N''
H :
  ∀ (x_2 : ι → M''),
    Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x + x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
      (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x + (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1 :
            (a : ι → M'') → N₂'')
          x_2 :
        N₂'')
⊢ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x + x_1) =
    (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x + (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x x_1 : M'' [⋀^ι]→ₗ[R'] N''
x_2 : ι → M''
⊢ Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x + x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
    (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x + (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1 :
          (a : ι → M'') → N₂'')
        x_2 :
      N₂'')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : R'
x_1 : M'' [⋀^ι]→ₗ[R'] N''
H :
  ∀ (x_2 : ι → M''),
    Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x • x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
      ((HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x : R') ((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1) :
            (a : ι → M'') → N₂'')
          x_2 :
        N₂'')
⊢ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x • x_1) =
    HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x : R') ((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : R'
x_1 : M'' [⋀^ι]→ₗ[R'] N''
x_2 : ι → M''
⊢ Eq.{u_14 + 1} (α := N₂'') (((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap (x • x_1) : (a : ι → M'') → N₂'') x_2 : N₂'')
    ((HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') x : R') ((↑e : N'' →ₗ[R'] N₂'').compAlternatingMap x_1) :
          (a : ι → M'') → N₂'')
        x_2 :
      N₂'')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N''
H :
  ∀ (x_1 : ι → M''),
    Eq.{u_13 + 1} (α := N'')
      (((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f)
              ((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f) x) :
            (a : ι → M'') → N'')
          x_1 :
        N'')
      ((x : (a : ι → M'') → N'') x_1 : N'')
⊢ (fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f)
      ((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f) x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N''
x_1 : ι → M''
⊢ Eq.{u_13 + 1} (α := N'')
    (((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f)
            ((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f) x) :
          (a : ι → M'') → N'')
        x_1 :
      N'')
    ((x : (a : ι → M'') → N'') x_1 : N'')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N₂''
H :
  ∀ (x_1 : ι → M''),
    Eq.{u_14 + 1} (α := N₂'')
      (((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f)
              ((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f) x) :
            (a : ι → M'') → N₂'')
          x_1 :
        N₂'')
      ((x : (a : ι → M'') → N₂'') x_1 : N₂'')
⊢ (fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f)
      ((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f) x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
R' : Type u_10
M'' : Type u_11
M₂'' : Type u_12
N'' : Type u_13
N₂'' : Type u_14
inst_11 : CommSemiring R'
inst_12 : AddCommMonoid M''
inst_13 : AddCommMonoid M₂''
inst_14 : AddCommMonoid N''
inst_15 : AddCommMonoid N₂''
inst_16 : Module R' M''
inst_17 : Module R' M₂''
inst_18 : Module R' N''
inst_19 : Module R' N₂''
e : N'' ≃ₗ[R'] N₂''
x : M'' [⋀^ι]→ₗ[R'] N₂''
x_1 : ι → M''
⊢ Eq.{u_14 + 1} (α := N₂'')
    (((fun (f : M'' [⋀^ι]→ₗ[R'] N'') ↦ (↑e : N'' →ₗ[R'] N₂'').compAlternatingMap f)
            ((fun (f : M'' [⋀^ι]→ₗ[R'] N₂'') ↦ (↑e.symm : N₂'' →ₗ[R'] N'').compAlternatingMap f) x) :
          (a : ι → M'') → N₂'')
        x_1 :
      N₂'')
    ((x : (a : ι → M'') → N₂'') x_1 : N₂'')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid N₂
inst_5 : Module R M
inst_6 : Module R M₂
inst_7 : Module R N
inst_8 : Module R N₂
n : ℕ
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M
v : Fin n → M
i j : Fin n
hv : v i = v j
hij : i ≠ j
⊢ Eq.{u_2 + 1} (α := M) (Fin.cons (α := fun (x : Fin n.succ) ↦ M) m v i.succ : M)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) m v j.succ : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin n.succ]→ₗ[R] N
x : M
v : Fin n → M
⊢ Eq.{u_4 + 1} (α := N)
    ((((f.curryLeft : (a : M) → M [⋀^Fin n]→ₗ[R] N) x : M [⋀^Fin n]→ₗ[R] N) : (a : Fin n → M) → N) v : N)
    ((f : (a : Fin n.succ → M) → N) (Matrix.vecCons x v) : N)

Tactic:
rfl

Premises used: Matrix.vecCons, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
⊢ Eq (α := M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (curryLeft 0) 0

Tactic:
rfl

Premises used: AlternatingMap.curryLeft, MultilinearMap.mk', rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f g : M [⋀^Fin n.succ]→ₗ[R] N
⊢ (f + g).curryLeft = f.curryLeft + g.curryLeft

Tactic:
rfl

Premises used: AlternatingMap.curryLeft, MultilinearMap.mk', rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
r : R
f : M [⋀^Fin n.succ]→ₗ[R] N
⊢ (r • f).curryLeft = r • f.curryLeft

Tactic:
rfl

Premises used: AlternatingMap.curryLeft, MultilinearMap.mk', rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M [⋀^Fin n.succ.succ]→ₗ[R] N
m : M
x : Fin n → M
⊢ Eq.{u_2 + 1} (α := M)
    (Fin.cons (α := fun (x : Fin (n + 1).succ) ↦ M) m (Fin.cons (α := fun (x : Fin n.succ) ↦ M) m x) 0 : M)
    (Fin.cons (α := fun (x : Fin (n + 1).succ) ↦ M) m (Fin.cons (α := fun (x : Fin n.succ) ↦ M) m x) 1 : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N₂ : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid N₂
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R N₂
n : ℕ
g : N →ₗ[R] N₂
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] N₂)
    (((g.compAlternatingMap f).curryLeft : (a : M) → M [⋀^Fin n]→ₗ[R] N₂) m : M [⋀^Fin n]→ₗ[R] N₂)
    (g.compAlternatingMap ((f.curryLeft : (a : M) → M [⋀^Fin n]→ₗ[R] N) m) : M [⋀^Fin n]→ₗ[R] N₂)

Tactic:
rfl

Premises used: LinearMap.compAlternatingMap, MultilinearMap.mk', LinearMap.compMultilinearMap, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i : Fin n.succ
zero :
  Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) 0 : (a : (fun (x : Fin n.succ) ↦ M₂) 0) → (fun (x : Fin n.succ) ↦ M) 0)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v 0 : M₂) :
      (fun (x : Fin n.succ) ↦ M) 0)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        0 :
      M)
succ :
  ∀ (i : Fin n),
    Eq.{u_2 + 1} (α := M)
      (((fun (x : Fin n.succ) ↦ g) i.succ :
            (a : (fun (x : Fin n.succ) ↦ M₂) i.succ) → (fun (x : Fin n.succ) ↦ M) i.succ)
          (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i.succ : M₂) :
        (fun (x : Fin n.succ) ↦ M) i.succ)
      (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
          (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
          i.succ :
        M)
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) i : (a : (fun (x : Fin n.succ) ↦ M₂) i) → (fun (x : Fin n.succ) ↦ M) i)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i : M₂) :
      (fun (x : Fin n.succ) ↦ M) i)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        i :
      M)

Tactic:
cases i using Fin.cases
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) 0 : (a : (fun (x : Fin n.succ) ↦ M₂) 0) → (fun (x : Fin n.succ) ↦ M) 0)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v 0 : M₂) :
      (fun (x : Fin n.succ) ↦ M) 0)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        0 :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.Curry
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module R M₂
inst_6 : Module R N
n : ℕ
g : M₂ →ₗ[R] M
f : M [⋀^Fin n.succ]→ₗ[R] N
m : M₂
v : Fin n → M₂
i : Fin n
⊢ Eq.{u_2 + 1} (α := M)
    (((fun (x : Fin n.succ) ↦ g) i.succ : (a : (fun (x : Fin n.succ) ↦ M₂) i.succ) → (fun (x : Fin n.succ) ↦ M) i.succ)
        (Fin.cons (α := fun (x : Fin n.succ) ↦ M₂) m v i.succ : M₂) :
      (fun (x : Fin n.succ) ↦ M) i.succ)
    (Fin.cons (α := fun (x : Fin n.succ) ↦ M) ((g : (a : M₂) → M) m)
        (fun (i : Fin n) ↦ ((fun (x : Fin n) ↦ g) i : (a : (fun (x : Fin n) ↦ M₂) i) → (fun (x : Fin n) ↦ M) i) (v i))
        i.succ :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Alternating.DomCoprod
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : (QuotientGroup.leftRel (Perm.sumCongrHom ιa ιb).range : Perm (ιa ⊕ ιb) → Perm (ιa ⊕ ιb) → Prop) σ₁ σ₂
⊢ σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range

Tactic:
rw [QuotientGroup.leftRel_apply] at H

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.LinearAlgebra.Alternating.DomCoprod
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
H : σ₁⁻¹ * σ₂ ∈ (Perm.sumCongrHom ιa ιb).range
obtain :
  ∀ (sl : Perm ιa) (sr : Perm ιb)
    (h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂),
    Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
      ((fun (σ : Perm (ιa ⊕ ιb)) ↦
          HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ
              ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
        σ₁)
      ((fun (σ : Perm (ιa ⊕ ιb)) ↦
          HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ
              ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
        σ₂)
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)

Tactic:
obtain ⟨⟨sl, sr⟩, h⟩ := H
-- Module: Mathlib.LinearAlgebra.Alternating.DomCoprod
Goal:
ιa : Type u_1
ιb : Type u_2
inst : Fintype ιa
inst_1 : Fintype ιb
R' : Type u_3
Mᵢ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
inst_2 : CommSemiring R'
inst_3 : AddCommGroup N₁
inst_4 : Module R' N₁
inst_5 : AddCommGroup N₂
inst_6 : Module R' N₂
inst_7 : AddCommMonoid Mᵢ
inst_8 : Module R' Mᵢ
inst_9 : DecidableEq ιa
inst_10 : DecidableEq ιb
a : Mᵢ [⋀^ιa]→ₗ[R'] N₁
b : Mᵢ [⋀^ιb]→ₗ[R'] N₂
σ : Perm.ModSumCongr ιa ιb
σ₁ σ₂ : Perm (ιa ⊕ ιb)
sl : Perm ιa
sr : Perm ιb
h : (Perm.sumCongrHom ιa ιb : (a : Perm ιa × Perm ιb) → Perm (ιa ⊕ ιb)) (sl, sr) = σ₁⁻¹ * σ₂
H :
  ∀ (v : (i : ιa ⊕ ιb) → Mᵢ),
    Eq (α := N₁ ⊗[R'] N₂)
      (((fun (σ : Perm (ιa ⊕ ιb)) ↦
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                  (MultilinearMap.domDomCongr σ
                    ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                      (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
              σ₁ :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂)
      (((fun (σ : Perm (ιa ⊕ ιb)) ↦
                HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
                  (MultilinearMap.domDomCongr σ
                    ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
                      (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
              σ₂ :
            (a : (i : ιa ⊕ ιb) → Mᵢ) → N₁ ⊗[R'] N₂)
          v :
        N₁ ⊗[R'] N₂)
⊢ Eq (α := MultilinearMap R' (fun (x : ιa ⊕ ιb) ↦ Mᵢ) (N₁ ⊗[R'] N₂))
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₁)
    ((fun (σ : Perm (ιa ⊕ ιb)) ↦
        HSMul.hSMul (α := ℤˣ) (((Perm.sign : Perm (ιa ⊕ ιb) →* ℤˣ) : (a : Perm (ιa ⊕ ιb)) → ℤˣ) σ : ℤˣ)
          (MultilinearMap.domDomCongr σ
            ((↑a : MultilinearMap R' (fun (x : ιa) ↦ Mᵢ) N₁).domCoprod
              (↑b : MultilinearMap R' (fun (x : ιb) ↦ Mᵢ) N₂))))
      σ₂)

Tactic:
ext v