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

Tactic:
rw [span_le]

Premises used: 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
y : Fin n → M
y_mem : Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s} y
a :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (range (ι := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)

Tactic:
apply ExteriorAlgebra.ιMulti_range R n

Premises used: ExteriorAlgebra.ιMulti_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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
y : Fin n → M
y_mem : Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s} y
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (range (ι := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M)

Tactic:
simp
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
a :
  HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n ⊆
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (span R
      (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
        {a : Fin n → M | range a ⊆ s}))

Tactic:
rw [ExteriorAlgebra.exteriorPower, LinearMap.range_eq_map, ← hs, map_span, span_pow, span_le]

Premises used: Submodule.span_pow, LinearMap.range_eq_map, Submodule.map_span, ExteriorAlgebra.exteriorPower, 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
x : ExteriorAlgebra R M
hx : x ∈ HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  ∀ (f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1)))
    (hx :
      List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
        HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n),
    List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
      (↑(span R
            (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
              {a : Fin n → M | range a ⊆ s})) :
        Set (ExteriorAlgebra R M))
⊢ x ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))

Tactic:
obtain ⟨f, rfl⟩ := Set.mem_pow.mp hx

Premises used: Iff.mp, Set.mem_pow, 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))

Tactic:
mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩

Premises used: Set.Mem, ExteriorAlgebra.ιInv, Function.comp, And.intro, Submodule.mem_span_of_mem, Exists.intro, Subtype.val, DFunLike.coe
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s}
    ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
      Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f)
a₁ :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f) :
      ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) : ExteriorAlgebra R M)
⊢ List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    (↑(span R
          (image (α := Fin n → M) (⇑(ExteriorAlgebra.ιMulti R n) : (a : Fin n → M) → ExteriorAlgebra R M)
            {a : Fin n → M | range a ⊆ s})) :
      Set (ExteriorAlgebra R M))

Tactic:
refine mem_span_of_mem ⟨ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f, ?_, ?_⟩
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  range
      (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f) ⊆
    (⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ⁻¹' s
⊢ Membership.mem (γ := Set (Fin n → M)) {a : Fin n → M | range a ⊆ s}
    ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
      Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f)

Tactic:
rw [Set.mem_setOf_eq, Set.range_comp, Set.image_subset_iff]

Premises used: Set.range_comp, Set.mem_setOf_eq, Set.image_subset_iff
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
apply :
  range
      (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f) ⊆
    (⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s
⊢ range
      (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f) ⊆
    (⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ⁻¹' s

Tactic:
apply Subset.trans ?_ (s.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse)

Premises used: Set.image_subset_preimage_of_inverse, Set.Subset.trans, ExteriorAlgebra.ι_leftInverse
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
⊢ range
      (Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Set (ExteriorAlgebra R M))
            ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
        f) ⊆
    (⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s

Tactic:
grind
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  Eq (α := ExteriorAlgebra R M)
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦
        (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
          (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
              Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                  Membership.mem (γ := Set (ExteriorAlgebra R M))
                    ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
                f)
            i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))
⊢ Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f) :
      ExteriorAlgebra R M)
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) : ExteriorAlgebra R M)

Tactic:
rw [ExteriorAlgebra.ιMulti_apply]

Premises used: ExteriorAlgebra.ιMulti_apply
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  Eq (α := Fin n → ExteriorAlgebra R M)
    (fun (i : Fin n) ↦
      (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i))
    fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    (List.prod
      (List.ofFn (n := n) fun (i : Fin n) ↦
        (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
          (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
              Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                  Membership.mem (γ := Set (ExteriorAlgebra R M))
                    ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
                f)
            i)))
    (List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)))

Tactic:
apply congrArg (List.prod ∘ List.ofFn)

Premises used: congrArg, List.ofFn, Function.comp, List.prod
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
a :
  ∀ (i : Fin n),
    (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i) =
      (↑(f i) : ExteriorAlgebra R M)
⊢ Eq (α := Fin n → ExteriorAlgebra R M)
    (fun (i : Fin n) ↦
      (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i))
    fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)

Tactic:
ext i
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
a :
  ∀ (m : M) (hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)),
    (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
            Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
                Membership.mem (γ := Set (ExteriorAlgebra R M))
                  ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
              f)
          i) =
      (↑(f i) : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)

Tactic:
obtain ⟨m, -, hm⟩ := (Set.mem_image _ _ _).mp (f i).2

Premises used: Set.mem_image, Iff.mp, Subtype.property
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
f : Fin n → (↑((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) : Type (max u u_1))
hx :
  List.prod (List.ofFn (n := n) fun (i : Fin n) ↦ (↑(f i) : ExteriorAlgebra R M)) ∈
    HPow.hPow (α := Set (ExteriorAlgebra R M)) ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) n
i : Fin n
m : M
hm : (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m = (↑(f i) : ExteriorAlgebra R M)
a :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
        ((Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
          i)) =
    (↑(f i) : ExteriorAlgebra R M)
a₁ :
  (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) (↑(f i) : ExteriorAlgebra R M)) =
    (↑(f i) : ExteriorAlgebra R M)
a₂ :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
        ((ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M)
          ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
      ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
a₃ a₄ :
  Eq (α := ExteriorAlgebra R M) ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
⊢ (ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M)
      (((⇑ExteriorAlgebra.ιInv : (a : ExteriorAlgebra R M) → M) ∘
          Subtype.val (p := fun (x : ExteriorAlgebra R M) ↦
              Membership.mem (γ := Set (ExteriorAlgebra R M))
                ((⇑(ExteriorAlgebra.ι R) : (a : M) → ExteriorAlgebra R M) '' s) x) ∘
            f)
        i) =
    (↑(f i) : ExteriorAlgebra R M)

Tactic:
rw [Function.comp_apply, Function.comp_apply, ← hm, ExteriorAlgebra.ι_leftInverse]

Premises used: ExteriorAlgebra.ι_leftInverse, Function.comp_apply
-- 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
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
      (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))) ⊤

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
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      ((fun (x : Fin n → M) ↦
          (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M)
            ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) x)) ''
        univ))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
      (Submodule.span R (range (ι := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)))))
    (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
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (range fun (a : Fin n → M) ↦ (ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) a))
    (⋀[R]^n M)
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      ((fun (x : Fin n → M) ↦
          (Submodule.subtype (⋀[R]^n M) : (a : ↥(⋀[R]^n M)) → ExteriorAlgebra R M)
            ((ιMulti R n : (a : Fin n → M) → ↥(⋀[R]^n M)) x)) ''
        univ))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)

Tactic:
simp only [Submodule.coe_subtype, ιMulti_apply_coe, Set.image_univ, Submodule.map_top,
    Submodule.range_subtype]

Premises used: Set.image_univ, Submodule.map_top, exteriorPower.ιMulti_apply_coe, Submodule.coe_subtype, 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
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (range fun (a : Fin n → M) ↦ (ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) a))
    (⋀[R]^n M)

Tactic:
ExteriorAlgebra.ιMulti_span_fixedDegree R n

Premises used: ExteriorAlgebra.ιMulti_span_fixedDegree
-- 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 (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.span R
      (range fun (a : Fin n → M) ↦ (ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) a))
    (⋀[R]^n M)

Tactic:
exact ExteriorAlgebra.ιMulti_span_fixedDegree R n

Premises used: ExteriorAlgebra.ιMulti_span_fixedDegree
-- 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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
a :
  Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
      (span R (image (α := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) {a : Fin n → M | range a ⊆ s})))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)
⊢ Eq (α := Submodule R ↥(⋀[R]^n M))
    (span R (image (α := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) {a : Fin n → M | range a ⊆ s})) ⊤

Tactic:
apply LinearMap.map_injective (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
s : Set M
hs : Eq (α := Submodule R M) (span R s) ⊤
⊢ Eq (α := Submodule R (ExteriorAlgebra R M))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M))
      (span R (image (α := Fin n → M) (⇑(ιMulti R n) : (a : Fin n → M) → ↥(⋀[R]^n M)) {a : Fin n → M | range a ⊆ s})))
    (Submodule.map (M := ↥(⋀[R]^n M)) (Submodule.subtype (⋀[R]^n M)) ⊤)

Tactic:
simpa [LinearMap.map_span, Set.image_image] using ιMulti_span_fixedDegree_of_span_eq_top R n M hs

Premises used: Set.image_image, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, LinearMap.map_span