awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
N' : Type u5
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup N'
inst_6 : Module R N'
f : M →ₗ[R] N
g : N →ₗ[R] N'
⊢ (map g).comp (map f) = map (g ∘ₗ f)

Tactic:
CliffordAlgebra.map_comp_map _ _

Premises used: QuadraticMap.Isometry.comp, ExteriorAlgebra.map, CliffordAlgebra.map_comp_map
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Submodule.map (map f).toLinearMap (LinearMap.range (ι R)) = Submodule.map (ι R) f.range

Tactic:
CliffordAlgebra.ι_range_map_map _

Premises used: CliffordAlgebra.ι_range_map_map, ExteriorAlgebra.map
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.{u1, u2} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : Module.{u1, u4} Rᵐᵒᵖ N
inst_8 : IsCentralScalar R N
f : M →ₗ[R] N
h :
  Eq (α := M →ₗ[R] TrivSqZeroExt R N) (AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R)
    (AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R)
⊢ Eq (α := ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R N) (AlgHom.comp toTrivSqZeroExt (map f))
    (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt)

Tactic:
apply hom_ext

Premises used: ExteriorAlgebra.hom_ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.{u1, u2} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : Module.{u1, u4} Rᵐᵒᵖ N
inst_8 : IsCentralScalar R N
f : M →ₗ[R] N
h :
  ∀ (x : M),
    Eq (α := TrivSqZeroExt R N)
      ((AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
        TrivSqZeroExt R N)
      ((AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
        TrivSqZeroExt R N)
⊢ Eq (α := M →ₗ[R] TrivSqZeroExt R N) (AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R)
    (AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R)

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.{u1, u2} Rᵐᵒᵖ M
inst_6 : IsCentralScalar R M
inst_7 : Module.{u1, u4} Rᵐᵒᵖ N
inst_8 : IsCentralScalar R N
f : M →ₗ[R] N
⊢ ∀ (x : M),
    Eq (α := TrivSqZeroExt R N)
      ((AlgHom.toLinearMap (AlgHom.comp toTrivSqZeroExt (map f)) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
        TrivSqZeroExt R N)
      ((AlgHom.toLinearMap (AlgHom.comp (TrivSqZeroExt.map f) toTrivSqZeroExt) ∘ₗ ι R : (a : M) → TrivSqZeroExt R N) x :
        TrivSqZeroExt R N)

Tactic:
simp only [AlgHom.comp_toLinearMap, LinearMap.coe_comp, Function.comp_apply,
    AlgHom.toLinearMap_apply, map_apply_ι, toTrivSqZeroExt_ι, TrivSqZeroExt.map_inr, forall_const]

Premises used: AlgHom.comp_toLinearMap, TrivSqZeroExt.map_inr, AlgHom.toLinearMap_apply, ExteriorAlgebra.map_apply_ι, ExteriorAlgebra.toTrivSqZeroExt_ι, LinearMap.coe_comp, forall_const, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
this : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ IsCentralScalar R M

Tactic:
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
⊢ IsCentralScalar R N

Tactic:
haveI : IsCentralScalar R N := ⟨fun r m => rfl⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this_3 : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R N
rw : (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt
| (TrivSqZeroExt.sndHom R N ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt) ∘ₗ (map f).toLinearMap

Tactic:
rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map,
                AlgHom.comp_toLinearMap, ← LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]

Premises used: AlgHom.comp_toLinearMap, ExteriorAlgebra.toTrivSqZeroExt_comp_map, LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this_3 : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R N
conv_lhs :
  (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt
⊢ (TrivSqZeroExt.sndHom R N ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt) ∘ₗ (map f).toLinearMap =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt

Tactic:
conv_lhs => rw [LinearMap.comp_assoc, ← AlgHom.comp_toLinearMap, toTrivSqZeroExt_comp_map,
                AlgHom.comp_toLinearMap, ← LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map]

Premises used: AlgHom.comp_toLinearMap, ExteriorAlgebra.toTrivSqZeroExt_comp_map, LinearMap.comp_assoc, TrivSqZeroExt.sndHom_comp_map
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
this_3 : Module.{u1, u4} Rᵐᵒᵖ N := Module.compHom N (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R N
⊢ (f ∘ₗ TrivSqZeroExt.sndHom R M) ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt =
    f ∘ₗ TrivSqZeroExt.sndHom R M ∘ₗ AlgHom.toLinearMap toTrivSqZeroExt

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    LeftInverse.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑g : (a : N) → M) (⇑f : (a : M) → N)

Tactic:
⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩

Premises used: ExteriorAlgebra.map._proof_1, QuadraticMap.Isometry.mk, Iff.intro, CliffordAlgebra.leftInverse_map_of_leftInverse
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
refine :
  ∀
    (h :
      LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
        (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
        (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N))
    (x : M), (g : (a : N) → M) ((f : (a : M) → N) x : N) = x
⊢ LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    LeftInverse.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑g : (a : N) → M) (⇑f : (a : M) → N)

Tactic:
refine ⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h :
  LeftInverse (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map g) : (a : ExteriorAlgebra R N) → ExteriorAlgebra R M)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
x : M
⊢ (g : (a : N) → M) ((f : (a : M) → N) x : N) = x

Tactic:
simpa using h (ι _ x)

Premises used: ExteriorAlgebra.ι, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
hf : ∃ (g : N →ₗ[R] M), g ∘ₗ f = LinearMap.id
⊢ Function.Injective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)

Tactic:
let ⟨_, hgf⟩ := hf; (leftInverse_map_iff.mpr (DFunLike.congr_fun hgf)).injective

Premises used: Function.LeftInverse.injective, Iff.mpr, DFunLike.congr_fun, ExteriorAlgebra.map, _private.0.ExteriorAlgebra.map_injective.match_1, Function.Injective, ExteriorAlgebra.leftInverse_map_iff, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    Function.Surjective.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩

Premises used: ExteriorAlgebra.map._proof_1, QuadraticMap.Isometry.mk, Iff.intro, CliffordAlgebra.map_surjective
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
refine :
  ∀
    (h :
      Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
        (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N))
    (y : N), ∃ (a : M), (f : (a : M) → N) a = y
⊢ Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
      (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) ↔
    Function.Surjective.{u2 + 1, u4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
refine ⟨fun h y ↦ ?_, fun h ↦ CliffordAlgebra.map_surjective _ h⟩
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
obtain :
  ∀ (x : ExteriorAlgebra R M)
    (hx :
      Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
        ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)),
    ∃ (a : M), (f : (a : M) → N) a = y
⊢ ∃ (a : M), (f : (a : M) → N) a = y

Tactic:
obtain ⟨x, hx⟩ := h (ι R y)

Premises used: ExteriorAlgebra.ι, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
x : ExteriorAlgebra R M
hx :
  Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)
existsi : (f : (a : M) → N) ((ιInv : (a : ExteriorAlgebra R M) → M) x : M) = y
⊢ ∃ (a : M), (f : (a : M) → N) a = y

Tactic:
existsi ιInv x

Premises used: ExteriorAlgebra.ιInv, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
x : ExteriorAlgebra R M
hx :
  Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)
rw :
  (ιInv : (a : ExteriorAlgebra R N) → N)
      (((map f).toLinearMap : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N) =
    y
⊢ (f : (a : M) → N) ((ιInv : (a : ExteriorAlgebra R M) → M) x : M) = y

Tactic:
rw [← LinearMap.comp_apply, ← ιInv_comp_map, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, ExteriorAlgebra.ιInv_comp_map
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u4
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
h :
  Function.Surjective (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R N)
    (⇑(map f) : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N)
y : N
x : ExteriorAlgebra R M
hx :
  Eq (α := ExteriorAlgebra R N) ((map f : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N)
    ((ι R : (a : N) → ExteriorAlgebra R N) y : ExteriorAlgebra R N)
⊢ (ιInv : (a : ExteriorAlgebra R N) → N)
      (((map f).toLinearMap : (a : ExteriorAlgebra R M) → ExteriorAlgebra R N) x : ExteriorAlgebra R N) =
    y

Tactic:
simp [hx, ιInv]

Premises used: ExteriorAlgebra.ιInv
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
K : Type u_1
E : Type u_2
F : Type u_3
inst : Field K
inst_1 : AddCommGroup E
inst_2 : Module K E
inst_3 : AddCommGroup F
inst_4 : Module K F
f : E →ₗ[K] F
hf : f.ker = ⊥
⊢ Function.Injective (α := ExteriorAlgebra K E) (β := ExteriorAlgebra K F)
    (⇑(map f) : (a : ExteriorAlgebra K E) → ExteriorAlgebra K F)

Tactic:
map_injective (LinearMap.exists_leftInverse_of_injective f hf)

Premises used: LinearMap.exists_leftInverse_of_injective, ExteriorAlgebra.map_injective
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ Eq (α := ExteriorAlgebra R M)
    ((toExterior : (a : TensorAlgebra R M) → ExteriorAlgebra R M) ((ι R : (a : M) → TensorAlgebra R M) m) :
      ExteriorAlgebra R M)
    ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)

Tactic:
simp [toExterior]

Premises used: TensorAlgebra.toExterior
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : Finset I
⊢ Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
    (ιMulti_family.{u_1, u_2, u_3} R s.card (I := I) (⇑b : (a : I) → M)
        (Sigma.snd (β := fun (n : ℕ) ↦ (↑(powersetCard I n) : Type u_3))
          ((Equiv.symm prodEquiv : (a : Finset I) → (n : ℕ) × (↑(powersetCard I n) : Type u_3)) s)) :
      ExteriorAlgebra R M)

Tactic:
simp [Basis.ExteriorAlgebra]

Premises used: Module.Basis.ExteriorAlgebra
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
n : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : Finset I
s_card : s.card = n
subst :
  Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
    (ιMulti_family R s.card (⇑b : (a : I) → M) (ofCard ⋯) : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
    (ιMulti_family R n (⇑b : (a : I) → M) (ofCard s_card) : ExteriorAlgebra R M)

Tactic:
subst s_card
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : Finset I
⊢ Eq (α := ExteriorAlgebra R M) ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) s : ExteriorAlgebra R M)
    (ιMulti_family R s.card (⇑b : (a : I) → M) (ofCard ⋯) : ExteriorAlgebra R M)

Tactic:
simp [basis_apply]

Premises used: ExteriorAlgebra.basis_apply
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
⊢ Eq (α := ExteriorAlgebra R M)
    ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
    (ιMulti_family R m (⇑b : (a : I) → M) s : ExteriorAlgebra R M)

Tactic:
simp [basis_apply_ofCard]

Premises used: ExteriorAlgebra.basis_apply_ofCard
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
m : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
rw :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
    (↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M)
rw₁ :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s)
    (↑(exteriorPower.ιMulti_family R m (⇑b : (a : I) → M) s) : ExteriorAlgebra R M)
rw₂ rw₃ :
  Eq (α := ExteriorAlgebra R M) (ιMulti_family R m (⇑b : (a : I) → M) s) (ιMulti_family R m (⇑b : (a : I) → M) s)
⊢ Eq (α := ExteriorAlgebra R M)
    ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
    ((↑((Basis.exteriorPower m b : (a : (↑(powersetCard I m) : Type u_3)) → ↥(⋀[R]^m M)) s) : ExteriorAlgebra R M) :
      ExteriorAlgebra R M)

Tactic:
rw [basis_apply_powersetCard, exteriorPower.basis_apply, ιMulti_family_apply_coe]

Premises used: exteriorPower.basis_apply, ExteriorAlgebra.basis_apply_powersetCard, exteriorPower.ιMulti_family_apply_coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
t : (↑(powersetCard I n) : Type u_3)
h : ¬Disjoint (↑s : Finset I) (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
      ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑t : Finset I) : ExteriorAlgebra R M) =
    0

Tactic:
simpa only [basis_apply_powersetCard] using ιMulti_family_mul_of_not_disjoint R b s t h

Premises used: ExteriorAlgebra.ιMulti_family_mul_of_not_disjoint, ExteriorAlgebra.basis_apply_powersetCard, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Goal:
R : Type u_1
M : Type u_2
m n : ℕ
I : Type u_3
inst : LinearOrder I
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis I R M
s : (↑(powersetCard I m) : Type u_3)
t : (↑(powersetCard I n) : Type u_3)
h : Disjoint (↑s : Finset I) (↑t : Finset I)
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑s : Finset I) : ExteriorAlgebra R M)
      ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑t : Finset I) : ExteriorAlgebra R M) =
    HSMul.hSMul (α := ℤˣ) (β := ExteriorAlgebra R M)
      ((Equiv.Perm.sign : (a : Equiv.Perm (Fin (m + n))) → ℤˣ) (permOfDisjoint h) : ℤˣ)
      ((b.ExteriorAlgebra : (a : Finset I) → ExteriorAlgebra R M) (↑(disjUnion h) : Finset I) : ExteriorAlgebra R M)

Tactic:
simpa only [basis_apply_powersetCard] using ιMulti_family_mul_of_disjoint R b s t h

Premises used: ExteriorAlgebra.ιMulti_family_mul_of_disjoint, ExteriorAlgebra.basis_apply_powersetCard, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ Membership.mem (α := ExteriorAlgebra R M) (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M)
    ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)

Tactic:
simpa only [pow_one] using LinearMap.mem_range_self _ m

Premises used: LinearMap.mem_range_self, pow_one
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
⊢ Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) 1 : ↥(⋀[R]^1 M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^1 M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
          Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
          ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))

Tactic:
rfl

Premises used: Set.Mem, DFinsupp.single, rfl
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ SetLike.GradedMonoid (S := Submodule R (ExteriorAlgebra R M)) fun (i : ℕ) ↦ ⋀[R]^i M

Tactic:
Submodule.nat_power_gradedMonoid (LinearMap.range (ι R : M →ₗ[R] ExteriorAlgebra R M))

Premises used: LinearMap.range, Submodule.nat_power_gradedMonoid, ExteriorAlgebra.ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
rw :
  Eq (α := ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (((DirectSum.of (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) (HAdd.hAdd (α := ℕ) 1 1) :
            ↥(⋀[R]^(HAdd.hAdd (α := ℕ) 1 1) M) →+ ⨁ (i : ℕ), ↥(⋀[R]^i M)) :
          (a : ↥(⋀[R]^(1 + 1) M)) → ⨁ (i : ℕ), ↥(⋀[R]^i M))
        (@GradedMonoid.GMul.mul _ (fun (i : ℕ) ↦ ↥(⋀[R]^i M)) instAddNat _ 1 1
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)
          (Subtype.mk (p := fun (x : ExteriorAlgebra R M) ↦
            Membership.mem (γ := Submodule R (ExteriorAlgebra R M)) (⋀[R]^1 M) x)
            ((ι R : (a : M) → ExteriorAlgebra R M) m) ⋯)) :
      ⨁ (i : ℕ), ↥(⋀[R]^i M))
    (0 : ⨁ (i : ℕ), ↥(⋀[R]^i M))
⊢ HMul.hMul (α := ⨁ (i : ℕ), ↥(⋀[R]^i M)) (β := ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M))
      ((GradedAlgebra.ι R M : (a : M) → ⨁ (i : ℕ), ↥(⋀[R]^i M)) m : ⨁ (i : ℕ), ↥(⋀[R]^i M)) =
    0

Tactic:
rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]

Premises used: DirectSum.of_mul_of, ExteriorAlgebra.GradedAlgebra.ι_apply