awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
m : Fin n → M
f : M [⋀^Fin n]→ₗ[R] N
⊢ Eq.{u_2 + 1} (α := N)
    ((((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
              ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f) :
            M [⋀^Fin n]→ₗ[R] N) :
          (a : Fin n → M) → N)
        m :
      N)
    ((LinearMap.compAlternatingMap ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f)
            (ιMulti R n) :
          (a : Fin n → M) → N)
        m :
      N)

Tactic:
simp only [LinearEquiv.symm_apply_apply, alternatingMapLinearEquiv_comp_ιMulti]

Premises used: LinearEquiv.symm_apply_apply, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
heq :
  ∀ (x : Fin n → M),
    Eq (α := ExteriorAlgebra R M)
      (↑((LinearMap.compAlternatingMap
                ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M))
                  (ιMulti R n))
                (ιMulti R n) :
              (a : Fin n → M) → ↥(⋀[R]^n M))
            x) :
        ExteriorAlgebra R M)
      (↑((LinearMap.compAlternatingMap LinearMap.id (ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) x) :
        ExteriorAlgebra R M)
⊢ Eq (α := ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M))
    ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M)) (ιMulti R n) :
      ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M))
    (LinearMap.id : ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
x : Fin n → M
⊢ Eq (α := ExteriorAlgebra R M)
    (↑((LinearMap.compAlternatingMap
              ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M))
                (ιMulti R n))
              (ιMulti R n) :
            (a : Fin n → M) → ↥(⋀[R]^n M))
          x) :
      ExteriorAlgebra R M)
    (↑((LinearMap.compAlternatingMap LinearMap.id (ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) x) :
      ExteriorAlgebra R M)

Tactic:
simp only [alternatingMapLinearEquiv_comp_ιMulti, ιMulti_apply_coe,
    LinearMap.compAlternatingMap_apply, LinearMap.id_coe, id_eq]

Premises used: LinearMap.compAlternatingMap_apply, LinearMap.id_coe, exteriorPower.ιMulti_apply_coe, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, id_eq
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
g : N →ₗ[R] N'
f : M [⋀^Fin n]→ₗ[R] N
heq :
  ∀ (x : Fin n → M),
    Eq.{u_3 + 1} (α := N')
      ((LinearMap.compAlternatingMap
              ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N') → ↥(⋀[R]^n M) →ₗ[R] N') (g.compAlternatingMap f))
              (ιMulti R n) :
            (a : Fin n → M) → N')
          x :
        N')
      ((LinearMap.compAlternatingMap
              (g ∘ₗ (alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f) (ιMulti R n) :
            (a : Fin n → M) → N')
          x :
        N')
⊢ Eq (α := ↥(⋀[R]^n M) →ₗ[R] N')
    ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N') → ↥(⋀[R]^n M) →ₗ[R] N') (g.compAlternatingMap f) :
      ↥(⋀[R]^n M) →ₗ[R] N')
    (g ∘ₗ (alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f : ↥(⋀[R]^n M) →ₗ[R] N')

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
g : N →ₗ[R] N'
f : M [⋀^Fin n]→ₗ[R] N
x : Fin n → M
⊢ Eq.{u_3 + 1} (α := N')
    ((LinearMap.compAlternatingMap
            ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N') → ↥(⋀[R]^n M) →ₗ[R] N') (g.compAlternatingMap f))
            (ιMulti R n) :
          (a : Fin n → M) → N')
        x :
      N')
    ((LinearMap.compAlternatingMap (g ∘ₗ (alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f)
            (ιMulti R n) :
          (a : Fin n → M) → N')
        x :
      N')

Tactic:
simp only [alternatingMapLinearEquiv_comp_ιMulti, LinearMap.compAlternatingMap_apply,
    LinearMap.coe_comp, comp_apply, alternatingMapLinearEquiv_apply_ιMulti]

Premises used: LinearMap.compAlternatingMap_apply, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, LinearMap.coe_comp, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ (LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n N)) → M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n N))
      (map n f) =
    AlternatingMap.compLinearMap (ιMulti R n) f

Tactic:
simp only [map, LinearEquiv.symm_apply_apply]

Premises used: LinearEquiv.symm_apply_apply, exteriorPower.map
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ (map n f).compAlternatingMap (ιMulti R n) = AlternatingMap.compLinearMap (ιMulti R n) f

Tactic:
simp only [map, alternatingMapLinearEquiv_comp_ιMulti]

Premises used: exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, exteriorPower.map
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
m : Fin n → M
⊢ Eq (α := ↥(⋀[R]^n N))
    ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) m) : ↥(⋀[R]^n N))
    ((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N)) ((⇑f : (a : M) → N) ∘ m) : ↥(⋀[R]^n N))

Tactic:
simp only [map, alternatingMapLinearEquiv_apply_ιMulti, AlternatingMap.compLinearMap_apply,
    Function.comp_def]

Premises used: exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, Function.comp_def, AlternatingMap.compLinearMap_apply, exteriorPower.map
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Type u_4
inst_5 : LinearOrder I
v : I → M
f : M →ₗ[R] N
h :
  ∀ (s : Finset I) (hs : s ∈ powersetCard I n),
    Eq (α := ExteriorAlgebra R N)
      (↑(comp (β := ↥(⋀[R]^n M)) (⇑(map n f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) (ιMulti_family R n v)
            (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs)) :
        ExteriorAlgebra R N)
      (↑(ιMulti_family R n ((⇑f : (a : M) → N) ∘ v)
            (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs)) :
        ExteriorAlgebra R N)
⊢ Eq (α := (↑(powersetCard I n) : Type u_4) → ↥(⋀[R]^n N))
    (comp (β := ↥(⋀[R]^n M)) (⇑(map n f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) (ιMulti_family R n v))
    (ιMulti_family R n ((⇑f : (a : M) → N) ∘ v))

Tactic:
ext ⟨s, hs⟩
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Type u_4
inst_5 : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s ∈ powersetCard I n
h :
  Eq (α := ExteriorAlgebra R N)
    ((↑((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
            ((⇑f : (a : M) → N) ∘
              v ∘
                (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I)
                        (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs) :
                      Fin n ↪o I) :
                  (a : Fin n) → I))) :
        ExteriorAlgebra R N) :
      ExteriorAlgebra R N)
    ((↑((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
            (((⇑f : (a : M) → N) ∘ v) ∘
              (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I)
                      (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs) :
                    Fin n ↪o I) :
                (a : Fin n) → I))) :
        ExteriorAlgebra R N) :
      ExteriorAlgebra R N)
⊢ Eq (α := ExteriorAlgebra R N)
    (↑(comp (β := ↥(⋀[R]^n M)) (⇑(map n f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) (ιMulti_family R n v)
          (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs)) :
      ExteriorAlgebra R N)
    (↑(ιMulti_family R n ((⇑f : (a : M) → N) ∘ v) (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs)) :
      ExteriorAlgebra R N)

Tactic:
simp only [ιMulti_family, Function.comp_apply, map_apply_ιMulti]

Premises used: Function.comp_apply, exteriorPower.map_apply_ιMulti, exteriorPower.ιMulti_family
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Type u_4
inst_5 : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : Finset I
hs : s ∈ powersetCard I n
⊢ Eq (α := ExteriorAlgebra R N)
    ((↑((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
            ((⇑f : (a : M) → N) ∘
              v ∘
                (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I)
                        (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs) :
                      Fin n ↪o I) :
                  (a : Fin n) → I))) :
        ExteriorAlgebra R N) :
      ExteriorAlgebra R N)
    ((↑((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
            (((⇑f : (a : M) → N) ∘ v) ∘
              (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I)
                      (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) s hs) :
                    Fin n ↪o I) :
                (a : Fin n) → I))) :
        ExteriorAlgebra R N) :
      ExteriorAlgebra R N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Type u_4
inst_5 : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : (↑(powersetCard I n) : Type u_4)
simp :
  Eq (α := ↥(⋀[R]^n N))
    ((AlternatingMap.compLinearMap (ιMulti R n) f : (a : Fin n → M) → ↥(⋀[R]^n N))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I) s : Fin n ↪o I) :
            (a : Fin n) → I)) :
      ↥(⋀[R]^n N))
    ((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
        (((⇑f : (a : M) → N) ∘ v) ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I) s : Fin n ↪o I) :
            (a : Fin n) → I)) :
      ↥(⋀[R]^n N))
⊢ Eq (α := ↥(⋀[R]^n N)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) (ιMulti_family R n v s) : ↥(⋀[R]^n N))
    (ιMulti_family R n ((⇑f : (a : M) → N) ∘ v) s : ↥(⋀[R]^n N))

Tactic:
simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]

Premises used: exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, exteriorPower.map, exteriorPower.ιMulti_family
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
I : Type u_4
inst_5 : LinearOrder I
v : I → M
f : M →ₗ[R] N
s : (↑(powersetCard I n) : Type u_4)
⊢ Eq (α := ↥(⋀[R]^n N))
    ((AlternatingMap.compLinearMap (ιMulti R n) f : (a : Fin n → M) → ↥(⋀[R]^n N))
        (v ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I) s : Fin n ↪o I) :
            (a : Fin n) → I)) :
      ↥(⋀[R]^n N))
    ((ιMulti R n : (a : Fin n → N) → ↥(⋀[R]^n N))
        (((⇑f : (a : M) → N) ∘ v) ∘
          (⇑((Equiv.symm ofFinEmbEquiv : (a : (↑(powersetCard I n) : Type u_4)) → Fin n ↪o I) s : Fin n ↪o I) :
            (a : Fin n) → I)) :
      ↥(⋀[R]^n N))

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := ↥(⋀[R]^n M) →ₗ[R] ↥(⋀[R]^n M)) (map n LinearMap.id) LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
hg : g ∘ₗ f = LinearMap.id
x : ↥(⋀[R]^n M)
rw : (map n g ∘ₗ map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
rw₁ : (map n (g ∘ₗ f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
rw₂ : (map n LinearMap.id : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
rw₃ : (LinearMap.id : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
rw₄ : id x = x
rw₅ rw₆ : x = x
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x

Tactic:
rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]

Premises used: LinearMap.id_coe, LinearMap.comp_apply, exteriorPower.map_id, exteriorPower.map_comp, id_eq
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
n : ℕ
M : Type u_1
N : Type u_2
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_4
inst_2 : Field K
inst_3 : Module K M
inst_4 : Module K N
f : M →ₗ[K] N
hf : Injective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Injective (α := ↥(⋀[K]^n M)) (β := ↥(⋀[K]^n N)) (⇑(map n f) : (a : ↥(⋀[K]^n M)) → ↥(⋀[K]^n N))

Tactic:
map_injective _ (f.exists_leftInverse_of_injective (LinearMap.ker_eq_bot.mpr hf)).choose_spec

Premises used: Iff.mpr, Exists.choose_spec, LinearMap.ker_eq_bot, LinearMap.exists_leftInverse_of_injective, exteriorPower.map_injective
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw :
  Eq (α := Submodule R ↥(⋀[R]^n N))
    (Submodule.span R
      (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))
        (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x)))
    (Submodule.span R (range (ι := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))))
⊢ Surjective (α := ↥(⋀[R]^n M)) (β := ↥(⋀[R]^n N)) (⇑(map n f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N))

Tactic:
rw [← LinearMap.range_eq_top, LinearMap.range_eq_map, ← ιMulti_span, ← ιMulti_span,
    Submodule.map_span, ← Set.range_comp, ← LinearMap.coe_compAlternatingMap, map_comp_ιMulti,
    AlternatingMap.coe_compLinearMap, Set.range_comp]

Premises used: Set.range_comp, LinearMap.coe_compAlternatingMap, LinearMap.range_eq_top, exteriorPower.map_comp_ιMulti, LinearMap.range_eq_map, AlternatingMap.coe_compLinearMap, Submodule.map_span, exteriorPower.ιMulti_span
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : Submodule.span R (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)) univ)
| Submodule.span R (range (ι := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)))

Tactic:
rw [← Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
conv_rhs :
  Eq (α := Submodule R ↥(⋀[R]^n N))
    (Submodule.span R
      (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))
        (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x)))
    (Submodule.span R (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)) univ))
⊢ Eq (α := Submodule R ↥(⋀[R]^n N))
    (Submodule.span R
      (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))
        (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x)))
    (Submodule.span R (range (ι := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))))

Tactic:
conv_rhs => rw [← Set.image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
e_s : Eq.{u_2 + 1} (α := Set (Fin n → N)) (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x) univ
⊢ Eq (α := Submodule R ↥(⋀[R]^n N))
    (Submodule.span R
      (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N))
        (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x)))
    (Submodule.span R (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)) univ))

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
e_s : Surjective.{u_1 + 1, u_2 + 1} (β := Fin n → N) fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x
⊢ Eq.{u_2 + 1} (α := Set (Fin n → N)) (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x) univ

Tactic:
rw [Set.range_eq_univ]

Premises used: Set.range_eq_univ
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Surjective.{u_1 + 1, u_2 + 1} (β := Fin n → N) fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x

Tactic:
Surjective.comp_left hf

Premises used: Function.Surjective.comp_left
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : Surjective.{u_1 + 1, u_2 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Surjective.{u_1 + 1, u_2 + 1} (β := Fin n → N) fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x

Tactic:
exact Surjective.comp_left hf

Premises used: Function.Surjective.comp_left
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
pos :
  ∀ (α_inj : Injective α),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
neg :
  ∀ (α_inj : ¬Injective α),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
by_cases α_inj : Injective α

Premises used: Function.Injective
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
this :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
neg :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
suffices ExteriorAlgebra.ιMulti R n (v ∘ α) = 0 by simp [this]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
⊢ Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)

Tactic:
AlternatingMap.map_eq_zero_of_not_injective _ _ <| fun h ↦ α_inj (Injective.of_comp h)

Premises used: AlternatingMap.map_eq_zero_of_not_injective, Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : ¬Injective α
⊢ Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
    (0 : ExteriorAlgebra R M)

Tactic:
exact AlternatingMap.map_eq_zero_of_not_injective _ _ <| fun h ↦ α_inj (Injective.of_comp h)

Premises used: AlternatingMap.map_eq_zero_of_not_injective, Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
this :
  ∃ (σ : Equiv.Perm (Fin n)),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) ((v ∘ α) ∘ (⇑σ : (a : Fin n) → Fin n)) :
        ExteriorAlgebra R M)
obtain :
  ∀ (σ : Equiv.Perm (Fin n))
    (hσ :
      Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
        (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
        ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) ((v ∘ α) ∘ (⇑σ : (a : Fin n) → Fin n)) :
          ExteriorAlgebra R M)),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
obtain ⟨σ, hσ⟩ := this