awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
have 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))
Tactic: rw [← ιMulti_span_fixedDegree_of_span_eq_top R n M hv, Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
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
⊢ 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)
have f_range₁ : Set.range f ⊆ Set.range v
Tactic: rw [Set.mem_setOf] at f_range
Cleared hypotheses: f_range
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
f : Fin n → M
f_range : Set.range f ⊆ 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) f : ExteriorAlgebra R M)
have 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)
Tactic: obtain ⟨α, rfl⟩ := Set.range_subset_range_iff_exists_comp.mp f_range
Cleared hypotheses: f, f_range
-- 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
hv : Eq (α := Submodule R M) (Submodule.span R (range v)) ⊤
⊢ Eq (α := Submodule R ↥(⋀[R]^n M)) (Submodule.span R (range (ιMulti_family R n v))) ⊤
have 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)) ⊤)
Tactic: apply LinearMap.map_injective (Submodule.ker_subtype (⋀[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
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.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)) ⊤)
have 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)) ⊤)
Tactic: rw [LinearMap.map_span, ← Set.image_univ, Set.image_image]
-- 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
⊢ 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)))
have 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)))
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⟩
-- 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
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)) ⊤
have a : (↑(span R (range f)) : Set ↥(span R (range v))) = (↑⊤ : Set ↥(span R (range v)))
Tactic: apply SetLike.coe_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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
⊢ (↑(span R (range f)) : Set ↥(span R (range v))) = (↑⊤ : Set ↥(span R (range v)))
have 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))))
Tactic: apply Set.image_injective.mpr (Submodule.span R (Set.range v)).injective_subtype
-- 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
f : I → ↥(span R (range v))
hf : (⇑(Submodule.subtype (span R (range v))) : (a : ↥(span R (range v))) → M) ∘ f = v
⊢ 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))))
have 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)))
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
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)))
⊢ 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))))
have 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)))
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
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)))
⊢ 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))))
have 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)))
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
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)))
⊢ 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))))
have a₃ : (↑(span R (range v)) : Set M) =
  (⇑(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]
-- 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
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)))
⊢ 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))))
have a₄ : (↑(span R (range v)) : Set M) =
  (↑(Submodule.map (M := ↥(span R (range v))) (Submodule.subtype (span R (range v))) ⊤) : Set M)
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
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)
⊢ 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))))
have a₅ : (↑(span R (range v)) : Set M) =
  (↑(LinearMap.range (M := ↥(span R (range v))) (Submodule.subtype (span R (range v)))) : Set M)
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- 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
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)
⊢ 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))))
have a₆ : (↑(span R (range v)) : Set M) = (↑(span R (range v)) : Set M)
Tactic: rw [← Submodule.map_coe, ← Submodule.span_image, ← Set.range_comp, hf,
      ← Submodule.map_coe, ← LinearMap.range_eq_map, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (hypothesis)
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 ↥(⋀[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)))
have htop : 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]
-- 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
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)) ⊤
⊢ 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)))
have 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)))
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]
-- 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
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)))
⊢ 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)))
have 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))
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]
-- 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
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))
⊢ 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)))
have 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)))
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]
-- 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
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)))
⊢ 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)))
have 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)))
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]