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
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) ((v ∘ α) ∘ (⇑σ : (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)
⊢ Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))

Tactic:
rw [AlternatingMap.map_perm] at hσ

Premises used: AlternatingMap.map_perm
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
(Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ

Premises used: Submodule.smul_mem_iff_of_isUnit, Iff.mp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
refine : IsUnit.{u} (M := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
⊢ 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:
refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ

Premises used: Submodule.smul_mem_iff_of_isUnit, Iff.mp
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
rw : ∃ (b : R), (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) * b = 1
⊢ IsUnit.{u} (M := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)

Tactic:
rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
h :
  HMul.hMul (α := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
      (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) =
    1
⊢ ∃ (b : R), (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) * b = 1

Tactic:
use (σ.sign : R)

Premises used: Int.cast, Units.val, Equiv.Perm.sign, 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
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
h :
  Eq.{u + 1} (α := R)
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
              ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)) :
          ℤ) :
      R)
    1
⊢ HMul.hMul (α := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
      (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) =
    1

Tactic:
norm_cast
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
σ : Equiv.Perm (Fin n)
hσ :
  Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    (HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M))
⊢ Eq.{u + 1} (α := R)
    (↑(↑(HMul.hMul (α := ℤˣ) (β := ℤˣ) ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)
              ((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ : ℤˣ)) :
          ℤ) :
      R)
    1

Tactic:
simp only [Int.units_mul_self, Units.val_one, Int.cast_one]

Premises used: Units.val_one, Int.cast_one, Int.units_mul_self
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
pos :
  ∃ (σ : Equiv.Perm (Fin n)),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) ((v ∘ α) ∘ (⇑σ : (a : Fin n) → Fin n)) :
        ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)

Tactic:
suffices ∃ σ : Equiv.Perm (Fin n), (ExteriorAlgebra.ιMulti R n ((v ∘ α) ∘ σ)) ∈
      Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) by
    obtain ⟨σ, hσ⟩ := this
    rw [AlternatingMap.map_perm] at hσ
    refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ
    rw [isUnit_iff_exists_inv]
    use (σ.sign : R)
    norm_cast
    simp only [Int.units_mul_self, Units.val_one, Int.cast_one]
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
⊢ (Finset.image α Finset.univ).card = n

Tactic:
have α_card : (Finset.image α Finset.univ).card = n :=
    (Finset.card_image_of_injective Finset.univ α_inj).trans (Finset.card_fin n)
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((v ∘ α) ∘
          (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                    x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)
⊢ ∃ (σ : Equiv.Perm (Fin n)),
    Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
      (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
      ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) ((v ∘ α) ∘ (⇑σ : (a : Fin n) → Fin n)) :
        ExteriorAlgebra R M)

Tactic:
use (Finset.orderIsoOfFin (Finset.image α Finset.univ) α_card).toEquiv.trans
    ((Equiv.setCongr Fintype.coe_image_univ).trans (Equiv.ofInjective α α_inj).symm)

Premises used: Fintype.coe_image_univ, Finset.orderIsoOfFin, Finset.univ, Equiv.trans, Equiv.setCongr, Equiv.ofInjective, RelIso.toEquiv, Equiv.symm, Finset.image
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (range (ExteriorAlgebra.ιMulti_family R n v))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((v ∘ α) ∘
          (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                    x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((v ∘ α) ∘
          (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                    x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)

Tactic:
apply Submodule.mem_span_of_mem

Premises used: Submodule.mem_span_of_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
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  Eq (α := ExteriorAlgebra R M)
    (ExteriorAlgebra.ιMulti_family R n v
      (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) (Finset.image α Finset.univ) α_card))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
      ((v ∘ α) ∘
        (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                  x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
              (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                (Equiv.ofInjective α α_inj).symm)) :
          (a : Fin n) → Fin n)))
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Set (ExteriorAlgebra R M))
    (range (ExteriorAlgebra.ιMulti_family R n v))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        ((v ∘ α) ∘
          (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                    x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)

Tactic:
use ⟨(Finset.image α Finset.univ), α_card⟩
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        (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) (Finset.image α Finset.univ) α_card) :
                Fin n ↪o I) :
            (a : Fin n) → I)) :
      ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        (v ∘
          α ∘
            (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                      x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                  (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                    (Equiv.ofInjective α α_inj).symm)) :
              (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M)
    (ExteriorAlgebra.ιMulti_family R n v
      (Subtype.mk (p := fun (x : Finset I) ↦ x ∈ powersetCard I n) (Finset.image α Finset.univ) α_card))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
      ((v ∘ α) ∘
        (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                  x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
              (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                (Equiv.ofInjective α α_inj).symm)) :
          (a : Fin n) → Fin n)))

Tactic:
rw [ExteriorAlgebra.ιMulti_family, Function.comp_assoc]

Premises used: ExteriorAlgebra.ιMulti_family, Function.comp_assoc
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  Eq (α := Fin n → I)
    (⇑((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) (Finset.image α Finset.univ) α_card) :
          Fin n ↪o I) :
      (a : Fin n) → I)
    (α ∘
      (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
            (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
              (Equiv.ofInjective α α_inj).symm)) :
        (a : Fin n) → Fin n))
⊢ Eq (α := ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        (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) (Finset.image α Finset.univ) α_card) :
                Fin n ↪o I) :
            (a : Fin n) → I)) :
      ExteriorAlgebra R M)
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M)
        (v ∘
          α ∘
            (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                      x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                  (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                    (Equiv.ofInjective α α_inj).symm)) :
              (a : Fin n) → Fin n)) :
      ExteriorAlgebra R M)

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
h :
  ∀ (i : Fin n),
    (((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) (Finset.image α Finset.univ) α_card) :
            Fin n ↪o I) :
          (a : Fin n) → I)
        i =
      (α ∘
          (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                    x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
                (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n))
        i
⊢ Eq (α := Fin n → I)
    (⇑((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) (Finset.image α Finset.univ) α_card) :
          Fin n ↪o I) :
      (a : Fin n) → I)
    (α ∘
      (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
            (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
              (Equiv.ofInjective α α_inj).symm)) :
        (a : Fin n) → Fin n))

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
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
i : Fin n
h :
  Eq (α := I)
    ((((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) (Finset.image α Finset.univ) α_card) :
            Fin n ↪o I) :
          (a : Fin n) → I)
        i :
      I)
    ((↑((Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯ :
              (a : ↥(Finset.image α Finset.univ)) → (↑(range α) : Type u_4))
            (((Finset.image α Finset.univ).orderIsoOfFin α_card : (a : Fin n) → ↥(Finset.image α Finset.univ)) i)) :
        I) :
      I)
⊢ (((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) (Finset.image α Finset.univ) α_card) :
          Fin n ↪o I) :
        (a : Fin n) → I)
      i =
    (α ∘
        (⇑((RelIso.toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : ↥(Finset.image α Finset.univ)) ↦
                  x1 ≤ x2) ((Finset.image α Finset.univ).orderIsoOfFin α_card)).trans
              (Equiv.trans (Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯)
                (Equiv.ofInjective α α_inj).symm)) :
          (a : Fin n) → Fin n))
      i

Tactic:
simp [Equiv.apply_ofInjective_symm]

Premises used: Equiv.apply_ofInjective_symm
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
i : Fin n
⊢ Eq (α := I)
    ((((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) (Finset.image α Finset.univ) α_card) :
            Fin n ↪o I) :
          (a : Fin n) → I)
        i :
      I)
    ((↑((Equiv.setCongr (s := (↑(Finset.image α Finset.univ) : Set I)) (t := range α) ⋯ :
              (a : ↥(Finset.image α Finset.univ)) → (↑(range α) : Type u_4))
            (((Finset.image α Finset.univ).orderIsoOfFin α_card : (a : Fin n) → ↥(Finset.image α Finset.univ)) i)) :
        I) :
      I)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorPower.Basic
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
a :
  LE.le (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)
a₁ :
  LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
    (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
⊢ Eq (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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 :
  ∀ (y : (↑(Set.powersetCard I n) : Type u_4)),
    ExteriorAlgebra.ιMulti_family R n v y ∈ (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
⊢ LE.le (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)

Tactic:
rw [Submodule.span_le, Set.range_subset_iff]

Premises used: Set.range_subset_iff, 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)) ⊤
y : (↑(Set.powersetCard I n) : Type u_4)
a : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M) (↑(ιMulti_family R n v y) : ExteriorAlgebra R M)
⊢ ExteriorAlgebra.ιMulti_family R n v y ∈ (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))

Tactic:
rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]

Premises used: exteriorPower.ιMulti_family_eq_coe_comp, SetLike.mem_coe, 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
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:
Submodule.coe_mem _

Premises used: Set.Mem, Submodule.coe_mem