awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M_1 : Type u_1
N : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
ι : Type u_4
inst_7 : DecidableEq ι
M : Type u_5
inst_8 : AddCommGroup M
inst_9 : Module R M
s : Module.Relations.Solution (relations R ι M) N
inst_10 : DecidableEq ι
m : (i : ι) → M
i : ι
r : R
x : M
this :
  Eq.{u_2 + 1} (α := N)
    ((Finsupp.linearCombination R s.var : (a : (ι → M) →₀ R) → N)
        (Finsupp.single (update (β := fun (a : ι) ↦ M) m i (r • x)) 1 -
          HSMul.hSMul (β := ((a : ι) → M) →₀ R) r (Finsupp.single (update (β := fun (a : ι) ↦ M) m i x) 1)) :
      N)
    (0 : N)
⊢ s.var (update (β := fun (x : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (x : ι) ↦ M) m i x)
have this₁ : s.var (update (β := fun (a : ι) ↦ M) m i (r • x)) = r • s.var (update (β := fun (a : ι) ↦ M) m i x)
Tactic: rw [Finsupp.smul_single, smul_eq_mul, mul_one, map_sub,
          Finsupp.linearCombination_single, one_smul,
          Finsupp.linearCombination_single, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
N_1 : Type u_2
N' : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : AddCommGroup N'
inst_6 : Module R N'
N : Type u_4
x : AddCommGroup N
x_1 : Module R N
f f' : ↥(⋀[R]^n M) →ₗ[R] N
h :
  Eq (α := Module.Relations.Solution (relations R (Fin n) M) N)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f)
    (Module.Relations.Solution.postcomp
      ((Equiv.symm relationsSolutionEquiv :
          (a : M [⋀^Fin n]→ₗ[R] ↥(⋀[R]^n M)) → (relations R (Fin n) M).Solution ↥(⋀[R]^n M))
        (ιMulti R n))
      f')
⊢ f = f'
have rw : ∀ (s : (↑(range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M))) : Type (max u u_1))),
  Eq.{u_4 + 1} (α := N) ((f : (a : ↥(⋀[R]^n M)) → N) (↑s : ↥(⋀[R]^n M)) : N)
    ((f' : (a : ↥(⋀[R]^n M)) → N) (↑s : ↥(⋀[R]^n M)) : N)
Tactic: rw [Submodule.linearMap_eq_iff_of_span_eq_top _ _ (ιMulti_span R n M)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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 g : ↥(⋀[R]^n M) →ₗ[R] N
heq : f.compAlternatingMap (ιMulti R n) = g.compAlternatingMap (ιMulti R n)
⊢ Eq (α := Module.Relations.Solution (Module.Presentation.toRelations (M := ↥(⋀[R]^n M)) (presentation R n M)) N)
    (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) f)
    (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) g)
have var : ∀ (f_1 : Module.Relations.G (Module.Presentation.toRelations (M := ↥(⋀[R]^n M)) (presentation R n M))),
  Module.Relations.Solution.var
      (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) f) f_1 =
    Module.Relations.Solution.var
      (Module.Relations.Solution.postcomp (Module.Presentation.toSolution (presentation R n M)) g) f_1
Tactic: ext f
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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 [⋀^Fin n]→ₗ[R] N
⊢ LinearMap.compAlternatingMap ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N) f)
      (ιMulti R n) =
    f
have obtain : ∀ (φ : ↥(⋀[R]^n M) →ₗ[R] N),
  Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ))
      (ιMulti R n))
    ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ)
Tactic: obtain ⟨φ, rfl⟩ := alternatingMapLinearEquiv.symm.surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((alternatingMapLinearEquiv : (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ))
      (ιMulti R n))
    ((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) φ)
have dsimp : Eq (α := M [⋀^Fin n]→ₗ[R] N)
  (LinearMap.compAlternatingMap
    ((LinearEquiv.symm
          (Equiv.toLinearEquiv
            (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv sorry)
              presentation.relationsSolutionEquiv)
            sorry) :
        (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
      ((Equiv.toLinearEquiv
            (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv sorry)
              presentation.relationsSolutionEquiv)
            sorry :
          (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
        φ))
    (ιMulti R n))
  ((Equiv.toLinearEquiv
        (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv sorry) presentation.relationsSolutionEquiv)
        sorry :
      (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
    φ)
Tactic: dsimp [alternatingMapLinearEquiv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
φ : ↥(⋀[R]^n M) →ₗ[R] N
⊢ Eq (α := M [⋀^Fin n]→ₗ[R] N)
    (LinearMap.compAlternatingMap
      ((LinearEquiv.symm
            (Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯) :
          (a : M [⋀^Fin n]→ₗ[R] N) → ↥(⋀[R]^n M) →ₗ[R] N)
        ((Equiv.toLinearEquiv
              (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯)
                presentation.relationsSolutionEquiv)
              ⋯ :
            (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
          φ))
      (ιMulti R n))
    ((Equiv.toLinearEquiv
          (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv ⋯) presentation.relationsSolutionEquiv)
          ⋯ :
        (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
      φ)
have simp : φ.compAlternatingMap (ιMulti R n) =
  (Equiv.toLinearEquiv
        (Equiv.trans (Module.Relations.Solution.IsPresentation.linearMapEquiv sorry) presentation.relationsSolutionEquiv)
        sorry :
      (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N)
    φ
Tactic: simp only [LinearEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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 : ↥(⋀[R]^n M) →ₗ[R] N
m : Fin n → M
⊢ Eq.{u_2 + 1} (α := N)
    ((((LinearEquiv.symm alternatingMapLinearEquiv : (a : ↥(⋀[R]^n M) →ₗ[R] N) → M [⋀^Fin n]→ₗ[R] N) F :
            M [⋀^Fin n]→ₗ[R] N) :
          (a : Fin n → M) → N)
        m :
      N)
    ((F.compAlternatingMap (ιMulti R n) : (a : Fin n → M) → N) m : N)
have obtain : ∀ (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: obtain ⟨f, rfl⟩ := alternatingMapLinearEquiv.surjective F
Cleared hypotheses: F
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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))
    ((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))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ 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')
have 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')
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ 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))
have 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)
Tactic: ext ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
    (↑(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)
have 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)
Tactic: simp only [ιMulti_family, Function.comp_apply, map_apply_ιMulti]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)) ((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))
have 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))
Tactic: simp only [ιMulti_family, map, alternatingMapLinearEquiv_apply_ιMulti]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw : (map n g ∘ₗ map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw₁ : (map n (g ∘ₗ f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw₂ : (map n LinearMap.id : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw₃ : (LinearMap.id : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n M)) x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw₄ : id x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ (map n g : (a : ↥(⋀[R]^n N)) → ↥(⋀[R]^n M)) ((map n f : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N)) x) = x
have rw₅ : x = x
Tactic: rw [← LinearMap.comp_apply, ← map_comp, hg, map_id, LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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 (α := ↥(⋀[R]^n M)) (β := ↥(⋀[R]^n N)) (⇑(map n f) : (a : ↥(⋀[R]^n M)) → ↥(⋀[R]^n N))
have 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))))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
| Submodule.span R (range (ι := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)))
have rw : Submodule.span R (image (α := Fin n → N) (⇑(ιMulti R n) : (a : Fin n → N) → ↥(⋀[R]^n N)) univ)
Tactic: rw [← Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
⊢ 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))))
have 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))
Tactic: conv_rhs => rw [← Set.image_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
⊢ 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))
have e_s : Eq.{u_2 + 1} (α := Set (Fin n → N)) (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x) univ
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
⊢ Eq.{u_2 + 1} (α := Set (Fin n → N)) (range fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x) univ
have e_s : Surjective.{u_1 + 1, u_2 + 1} (β := Fin n → N) fun (x : Fin n → M) ↦ (⇑f : (a : M) → N) ∘ x
Tactic: rw [Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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
⊢ 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)
have 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)
Tactic: by_cases α_inj : Injective α
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases α_inj : Injective α