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
α : Fin n → I
α_inj : ¬Injective α
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
have neg : Eq (α := ExteriorAlgebra R M)
  ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
  (0 : ExteriorAlgebra R M)
Tactic: suffices ExteriorAlgebra.ιMulti R n (v ∘ α) = 0 by simp [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
this :
  ∃ (σ : 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)
have obtain : ∀ (σ : 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 (α := 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: obtain ⟨σ, hσ⟩ := this
Cleared hypotheses: this
-- 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
α : 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 (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
have 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))
Tactic: rw [AlternatingMap.map_perm] at hσ
Cleared hypotheses: hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_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)
have refine : IsUnit.{u} (M := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
Tactic: refine (Submodule.smul_mem_iff_of_isUnit _ (r := (σ.sign : R)) ?_).mp hσ
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_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))
⊢ IsUnit.{u} (M := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
have rw : ∃ (b : R), (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) * b = 1
Tactic: rw [isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_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))
⊢ ∃ (b : R), (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) * b = 1
have h : HMul.hMul (α := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
    (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) =
  1
Tactic: use (σ.sign : R)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_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))
⊢ HMul.hMul (α := R) (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R)
      (↑(↑((Equiv.Perm.sign : (a : Equiv.Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) =
    1
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M))
    (span R (range (ExteriorAlgebra.ιMulti_family R n v)))
    ((ExteriorAlgebra.ιMulti R n : (a : Fin n → M) → ExteriorAlgebra R M) (v ∘ α) : ExteriorAlgebra R M)
have 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)
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]
-- 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
α : Fin n → I
α_inj : Injective α
⊢ ∃ (σ : 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)
have α_card : (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
⊢ ∃ (σ : 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)
have 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 α) sorry)
                (Equiv.ofInjective α α_inj).symm)) :
          (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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = 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 ∘ α) ∘
          (⇑((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)
have 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 α) sorry)
                (Equiv.ofInjective α α_inj).symm)) :
          (a : Fin n) → Fin n)) :
    ExteriorAlgebra R M)
Tactic: apply Submodule.mem_span_of_mem
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = 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)
have 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 α) sorry)
              (Equiv.ofInjective α α_inj).symm)) :
        (a : Fin n) → Fin n)))
Tactic: use ⟨(Finset.image α Finset.univ), α_card⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
⊢ 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)))
have 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 α) sorry)
                  (Equiv.ofInjective α α_inj).symm)) :
            (a : Fin n) → Fin n)) :
    ExteriorAlgebra R M)
Tactic: rw [ExteriorAlgebra.ιMulti_family, Function.comp_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = 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)
have 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 α) sorry)
            (Equiv.ofInjective α α_inj).symm)) :
      (a : Fin n) → Fin n))
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
⊢ 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))
have 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 α) sorry)
                (Equiv.ofInjective α α_inj).symm)) :
          (a : Fin n) → Fin n))
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.ExteriorPower.Basic (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Type u_4
inst_3 : LinearOrder I
v : I → M
α : Fin n → I
α_inj : Injective α
α_card : (Finset.image α Finset.univ).card = n
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
have 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 α) sorry :
            (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: simp [Equiv.apply_ofInjective_symm]
-- 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)) ⊤
⊢ Eq (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)
have a : LE.le (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
  (⋀[R]^n M)
Tactic: apply le_antisymm
-- 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)) ⊤
a :
  LE.le (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)
⊢ Eq (α := Submodule R (ExteriorAlgebra R M)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)
have a₁ : LE.le (α := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M)
  (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
Tactic: apply le_antisymm
-- 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)) (Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)))
    (⋀[R]^n M)
have a : ∀ (y : (↑(Set.powersetCard I n) : Type u_4)),
  ExteriorAlgebra.ιMulti_family R n v y ∈ (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
Tactic: rw [Submodule.span_le, Set.range_subset_iff]
-- 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)) ⊤
y : (↑(Set.powersetCard I n) : Type u_4)
⊢ ExteriorAlgebra.ιMulti_family R n v y ∈ (↑(⋀[R]^n M) : Set (ExteriorAlgebra R M))
have a : Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^n M) (↑(ιMulti_family R n v y) : ExteriorAlgebra R M)
Tactic: rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]