awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
y : (↑(Set.powersetCard I n) : Type u_4)
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M) (↑(ιMulti_family R n v y) : ExteriorAlgebra R M)

Tactic:
exact Submodule.coe_mem _

Premises used: Submodule.coe_mem
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
a :
  Set.image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
      {a : Fin n → M | Set.range a ⊆ Set.range v} ⊆
    (↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))) : Set (ExteriorAlgebra R M))
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))

Tactic:
rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]

Premises used: exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, Submodule.span_le
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
f : Fin n → M
f_range : Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | Set.range a ⊆ Set.range v} f
⊢ Set.range f ⊆ Set.range v

Tactic:
rw [Set.mem_setOf] at f_range

Premises used: Set.mem_setOf
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
f : Fin n → M
f_range : Set.range f ⊆ Set.range v
a :
  ∀ (α : Fin n → I) (f_range : Set.range (v ∘ α) ⊆ Set.range v),
    Membership.mem (α := ExteriorAlgebra R M)
      (↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))) : Set (ExteriorAlgebra R M))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M)
    (↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))) : Set (ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) f : ExteriorAlgebra R M)

Tactic:
obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range

Premises used: Set.range_subset_range_iff_exists_comp, Iff.mp, 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
I : Type u_4
inst_3 : LinearOrder I
v : I → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
α : Fin n → I
f_range : Set.range (v ∘ α) ⊆ Set.range v
⊢ Membership.mem (α := ExteriorAlgebra R M)
    (↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))) : Set (ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
ιMulti_family_span_fixedDegree_aux R v α

Premises used: _private.0.exteriorPower.ιMulti_family_span_fixedDegree_aux
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
α : Fin n → I
f_range : Set.range (v ∘ α) ⊆ Set.range v
⊢ Membership.mem (α := ExteriorAlgebra R M)
    (↑(Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))) : Set (ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
exact ιMulti_family_span_fixedDegree_aux R v α

Premises used: _private.0.exteriorPower.ιMulti_family_span_fixedDegree_aux
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (range v)) ⊤
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (Submodule.subtype (⋀[R]^n M)) (Submodule.span R (range (ιMulti_family R n v))))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
⊢ Eq (α := Submodule R ↥(⋀[R]^n M)) (Submodule.span R (range (ιMulti_family R n v))) ⊤

Tactic:
apply LinearMap.map_injective (Submodule.ker_subtype (⋀[R]^n M))

Premises used: LinearMap.map_injective, Submodule.ker_subtype, ExteriorAlgebra.exteriorPower
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (range v)) ⊤
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      ((fun (x : (↑(powersetCard I n) : Type u_4)) ↦
          (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M) (ιMulti_family R n v x)) ''
        univ))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (Submodule.subtype (⋀[R]^n M)) (Submodule.span R (range (ιMulti_family R n v))))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)

Tactic:
rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]

Premises used: Set.image_image, Set.image_univ, LinearMap.map_span
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (range v)) ⊤
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      ((fun (x : (↑(powersetCard I n) : Type u_4)) ↦
          (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M) (ιMulti_family R n v x)) ''
        univ))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)

Tactic:
simpa using ιMulti_family_span_fixedDegree_of_span R hv

Premises used: exteriorPower.ιMulti_family_span_fixedDegree_of_span
-- 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
have :
  ∀ (f : I → ↥(span R (range v)))
    (hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v),
    Eq (α := Submodule R ↥(⋀[R]^n M))
      (LinearMap.range (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))))
      (span R (range (ιMulti_family R n v)))
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (LinearMap.range (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))))
    (span R (range (ιMulti_family R n v)))

Tactic:
have ⟨f, hf⟩ : ∃ f : I → Submodule.span R (Set.range v), Submodule.subtype _ ∘ f = v :=
    ⟨fun i ↦ ⟨v i, Submodule.subset_span (Set.mem_range_self i)⟩, 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
I : Type u_4
inst_3 : LinearOrder I
v : I → M
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
a : (↑(span R (range f)) : Set ↥(span R (range v))) = (↑⊤ : Set ↥(span R (range v)))
⊢ Eq (α := Submodule R ↥(span R (range v))) (span R (range f)) ⊤

Tactic:
apply SetLike.coe_injective

Premises used: SetLike.coe_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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
a :
  Eq (α := Set M)
    ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ''
      (↑(span R (range f)) : Set ↥(span R (range v))))
    ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v))))
⊢ (↑(span R (range f)) : Set ↥(span R (range v))) = (↑⊤ : Set ↥(span R (range v)))

Tactic:
apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype

Premises used: Iff.mpr, Set.image_injective, Submodule.injective_subtype, Submodule.span, Set.range
-- 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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
a :
  (↑(Submodule.map (Submodule.subtype (span R (range v))) (span R (range f))) : Set M) =
    (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v)))
a₁ :
  (↑(span R ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' range f)) : Set M) =
    (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v)))
a₂ :
  (↑(span R (range ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f))) : Set M) =
    (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v)))
a₃ :
  (↑(span R (range v)) : Set M) =
    (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v)))
a₄ :
  (↑(span R (range v)) : Set M) =
    (↑(Submodule.map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))) ⊤) : Set M)
a₅ :
  (↑(span R (range v)) : Set M) =
    (↑(LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))) : Set M)
a₆ a₇ : (↑(span R (range v)) : Set M) = (↑(span R (range v)) : Set M)
⊢ Eq (α := Set M)
    ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ''
      (↑(span R (range f)) : Set ↥(span R (range v))))
    ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) '' (↑⊤ : Set ↥(span R (range v))))

Tactic:
rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]

Premises used: Set.range_comp, LinearMap.range_eq_map, Submodule.span_image, Submodule.map_coe, Submodule.range_subtype
-- 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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
⊢ Eq (α := Submodule R ↥(span R (range v))) (span R (range f)) ⊤

Tactic:
have htop : Submodule.span R (Set.range f) = ⊤ := by
    apply SetLike.coe_injective
    apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype
    rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
htop : Eq (α := Submodule R ↥(span R (range v))) (span R (range f)) ⊤
rw :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (Submodule.map (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))) ⊤)
    (span R (range (ιMulti_family R n v)))
rw₁ :
  Submodule.map (map n (Submodule.subtype (span R (range v)))) (span R (range (ιMulti_family R n f))) =
    span R (range (ιMulti_family R n v))
rw₂ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (image (α := ↥(⋀[R]^n ↥(span R (range v))))
        (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
        (range (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
rw₃ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R
      (range
        (comp (β := ↥(⋀[R]^n ↥(span R (range v))))
          (⇑(map n (Submodule.subtype (span R (range v)))) : (a : ↥(⋀[R]^n ↥(span R (range v)))) → ↥(⋀[R]^n M))
          (ιMulti_family R n f))))
    (span R (range (ιMulti_family R n v)))
rw₄ :
  Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R (range (ιMulti_family R n ((⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f))))
    (span R (range (ιMulti_family R n v)))
rw₅ rw₆ :
  Eq (α := Submodule R ↥(⋀[R]^n M)) (span R (range (ιMulti_family R n v))) (span R (range (ιMulti_family R n v)))
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (LinearMap.range (M := ↥(⋀[R]^n ↥(span R (range v)))) (map n (Submodule.subtype (span R (range v)))))
    (span R (range (ιMulti_family R n v)))

Tactic:
rw [LinearMap.range_eq_map (M := ⋀[R]^n _), ← ιMulti_family_span_of_span _ htop,
    Submodule.map_span, ← Set.range_comp, map_comp_ιMulti_family, hf]

Premises used: Set.range_comp, exteriorPower.ιMulti_family_span_of_span, exteriorPower.map_comp_ιMulti_family, LinearMap.range_eq_map, Submodule.map_span
-- 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'
r : R
i : ℕ
hi : i < 0
⊢ M

Tactic:
simp at hi
-- 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'
x y : R
⊢ HSMul.hSMul (β := ↥(⋀[R]^0 M)) (x + y)
      ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
        Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim) =
    HSMul.hSMul (β := ↥(⋀[R]^0 M)) x
        ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
          Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim) +
      HSMul.hSMul (β := ↥(⋀[R]^0 M)) y
        ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
          Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim)

Tactic:
simp only [add_smul]

Premises used: add_smul
-- 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'
m x : R
⊢ HSMul.hSMul (β := ↥(⋀[R]^0 M)) (m • x)
      ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
        Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
      (HSMul.hSMul (β := ↥(⋀[R]^0 M)) x
        ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
          Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim))

Tactic:
simp only [smul_eq_mul, mul_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, smul_eq_mul, SemigroupAction.mul_smul
-- 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'
⊢ Eq (α := R →ₗ[R] R)
    (((alternatingMapLinearEquiv.{u, u_1, u} (R := R) (n := 0) (M := M) (N := R) :
            M [⋀^Fin 0]→ₗ[R] R ≃ₗ[R] ↥(⋀[R]^0 M) →ₗ[R] R) :
          (a : M [⋀^Fin 0]→ₗ[R] R) → ↥(⋀[R]^0 M) →ₗ[R] R)
        (AlternatingMap.constOfIsEmpty R M (Fin 0) 1) ∘ₗ
      {
        toFun := fun (r : R) ↦
          HSMul.hSMul (β := ↥(⋀[R]^0 M)) r
            ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
              Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim),
        map_add' := ⋯, map_smul' := ⋯ })
    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
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'
⊢ Eq (α := ↥(⋀[R]^0 M) →ₗ[R] ↥(⋀[R]^0 M))
    ({
        toFun := fun (r : R) ↦
          HSMul.hSMul (β := ↥(⋀[R]^0 M)) r
            ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) fun (a : Fin 0) ↦
              Fin.casesOn (motive := fun (x : Fin 0) ↦ M) a fun (i : ℕ) (hi : i < 0) ↦ ⋯.elim),
        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
      ((alternatingMapLinearEquiv.{u, u_1, u} (R := R) (n := 0) (M := M) (N := R) :
            M [⋀^Fin 0]→ₗ[R] R ≃ₗ[R] ↥(⋀[R]^0 M) →ₗ[R] R) :
          (a : M [⋀^Fin 0]→ₗ[R] R) → ↥(⋀[R]^0 M) →ₗ[R] R)
        (AlternatingMap.constOfIsEmpty R M (Fin 0) 1))
    LinearMap.id

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
f : Fin 0 → M
⊢ Eq.{u + 1} (α := R)
    ((zeroEquiv R M : (a : ↥(⋀[R]^0 M)) → R) ((ιMulti R 0 : (a : Fin 0 → M) → ↥(⋀[R]^0 M)) f : ↥(⋀[R]^0 M)) : R) (1 : R)

Tactic:
simp [zeroEquiv]

Premises used: exteriorPower.zeroEquiv
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
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
⊢ (↑(zeroEquiv R N) : ↥(⋀[R]^0 N) →ₗ[R] R) ∘ₗ map 0 f = (↑(zeroEquiv R M) : ↥(⋀[R]^0 M) →ₗ[R] R)

Tactic:
aesop
-- 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'
m : M
h : ∀ (i : Fin 1), m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m i
⊢ Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)

Tactic:
ext i
-- 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'
m : M
i : Fin 1
h : m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩)
⊢ m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m i

Tactic:
fin_cases i
-- 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'
m : M
⊢ m = update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m ((fun (i : Fin 1) ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl
-- 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'
⊢ ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)

Tactic:
have h (m : M) : (fun (_ : Fin 1) ↦ m) = update (fun _ ↦ 0) 0 m := by
        ext i
        fin_cases i
        rfl
-- 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'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
m₁ m₂ : M
rw :
  (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₁)
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₂)
⊢ ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₁ + m₂) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₁)
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₂)

Tactic:
rw [h]
-- 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'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
m₁ m₂ : M
nth_rw :
  (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) (β := ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₁) :
        ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₂ : ↥(⋀[R]^1 M))
⊢ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₁)
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₂)

Tactic:
nth_rw 2 [h]
-- 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'
h :
  ∀ (m : M),
    Eq.{u_1 + 1} (α := Fin 1 → M) (fun (x : Fin 1) ↦ m) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m)
m₁ m₂ : M
nth_rw :
  (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) (β := ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₁) :
        ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₂) :
        ↥(⋀[R]^1 M))
⊢ (ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 (m₁ + m₂)) =
    HAdd.hAdd (α := ↥(⋀[R]^1 M)) (β := ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) (update (β := fun (a : Fin 1) ↦ M) (fun (x : Fin 1) ↦ 0) 0 m₁) :
        ↥(⋀[R]^1 M))
      ((ιMulti R 1 : (a : Fin 1 → M) → ↥(⋀[R]^1 M)) fun (x : Fin 1) ↦ m₂ : ↥(⋀[R]^1 M))

Tactic:
nth_rw 3 [h]