awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₂ : Eq (α := (a : ι → M) → N')
  (⇑(∑ x : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
          (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
    (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₂ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₃ : Eq (α := (a : ι → M) → N')
  (⇑(∑ x : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
          (↑(HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) a) :
            MultilinearMap R (fun (x : ι) ↦ M) N')) :
    (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₂ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₃ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) a) :
              MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₄ : Eq (α := (a : ι → M) → N')
  (⇑(∑ x : Equiv.Perm ι,
        HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
          (HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
    (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₂ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₃ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) a) :
              MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₄ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
              (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₅ : Eq (α := (a : ι → M) → N')
  (⇑(∑ x : Equiv.Perm ι,
        HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) •
          (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) :
    (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
inst_5 : DecidableEq ι
inst_6 : Fintype ι
a : M [⋀^ι]→ₗ[R] N'
a₁ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ σ : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) σ : ℤˣ)
            (MultilinearMap.domDomCongr σ (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₂ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(domDomCongr x a) : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₃ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (↑(HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) a) :
              MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₄ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
            (HSMul.hSMul (α := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
              (↑a : MultilinearMap R (fun (x : ι) ↦ M) N'))) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
a₅ :
  Eq (α := (a : ι → M) → N')
    (⇑(∑ x : Equiv.Perm ι,
          HMul.hMul (α := ℤˣ) (β := ℤˣ) (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ)
              (((Equiv.Perm.sign : Equiv.Perm ι →* ℤˣ) : (a : Equiv.Perm ι) → ℤˣ) x : ℤˣ) •
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) :
      (a : (i : ι) → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
⊢ Eq (α := (a : ι → M) → N')
    (⇑((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N')
            (↑a : MultilinearMap R (fun (x : ι) ↦ M) N') :
          M [⋀^ι]→ₗ[R] N') :
      (a : ι → M) → N')
    (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
have a₆ : Eq (α := (a : ι → M) → N')
  (⇑(∑ x : Equiv.Perm ι, HSMul.hSMul (α := ℤˣ) 1 (↑a : MultilinearMap R (fun (x : ι) ↦ M) N')) : (a : (i : ι) → M) → N')
  (⇑((Fintype.card ι).factorial • a) : (a : ι → M) → N')
Tactic: simp_rw [MultilinearMap.alternatization_def, ← coe_domDomCongr, domDomCongr_perm, coe_smul,
    smul_smul, Int.units_mul_self, one_smul, Finset.sum_const, Finset.card_univ, Fintype.card_perm,
    ← coe_multilinearMap, coe_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N' : Type u_6
inst_3 : AddCommGroup N'
inst_4 : Module R N'
ι : Type u_7
N'₂ : Type u_10
inst_5 : AddCommGroup N'₂
inst_6 : Module R N'₂
inst_7 : DecidableEq ι
inst_8 : Fintype ι
g : N' →ₗ[R] N'₂
f : MultilinearMap.{u_1, u_7, u_2, u_6} R (fun (x : ι) ↦ M) N'
⊢ Eq (α := M [⋀^ι]→ₗ[R] N'₂)
    ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N'₂) → M [⋀^ι]→ₗ[R] N'₂)
        (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) f) :
      M [⋀^ι]→ₗ[R] N'₂)
    (g.compAlternatingMap
        ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') f) :
      M [⋀^ι]→ₗ[R] N'₂)
have H : ∀ (x : ι → M),
  Eq.{u_10 + 1} (α := N'₂)
    ((((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N'₂) → M [⋀^ι]→ₗ[R] N'₂)
              (g.compMultilinearMap (M₁ := fun (x : ι) ↦ M) f) :
            M [⋀^ι]→ₗ[R] N'₂) :
          (a : ι → M) → N'₂)
        x :
      N'₂)
    ((g.compAlternatingMap
            ((MultilinearMap.alternatization : (a : MultilinearMap R (fun (x : ι) ↦ M) N') → M [⋀^ι]→ₗ[R] N') f) :
          (a : ι → M) → N'₂)
        x :
      N'₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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₂)
⊢ f = g
have refine : ∀ (v : (i : ι) → ι₁),
  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: refine AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear (fun _ ↦ e) fun v => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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 : ι) → ι₁
⊢ 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₂)
have pos : ∀ (hi : Function.Injective v),
  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: by_cases hi : Function.Injective v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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 : ι) → ι₁
pos :
  ∀ (hi : Function.Injective v),
    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₂)
⊢ 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₂)
have neg : ∀ (hi : ¬Function.Injective v),
  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: by_cases hi : Function.Injective v
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
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
⊢ 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₂)
have this : ¬Function.Injective.{u_7 + 1, u_12 + 1} (β := N₁) fun (i : ι) ↦ (e : (a : ι₁) → N₁) (v i)
Tactic: have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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)
⊢ 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₂)
have 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₂)
Tactic: rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
      g.map_eq_zero_of_not_injective _ this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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₂)
⊢ 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₂)
have 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₂)
Tactic: rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
      g.map_eq_zero_of_not_injective _ this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
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₂)
⊢ 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₂)
have neg₂ : Eq.{u_13 + 1} (α := N₂) (0 : N₂)
  ((g : (a : ι → 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]