awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
⊢ Eq (α := M)
    ((↑((HPow.hPow (β := ℕ) (restrict φ hφV) 0 : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((HPow.hPow (β := ℕ) φ 0 : (a : M) → M) x : M)

Tactic:
simp [pow_succ', *]

Premises used: pow_succ'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
V : Submodule K M := φ.maxGenEigenspace 0
hV : V = ⨆ (n : ℕ), ker (φ ^ n)
W : Submodule K M := ⨅ (n : ℕ), range (φ ^ n)
hVW : IsCompl V W
hφV : ∀ x ∈ V, Membership.mem (α := M) V ((φ : (a : M) → M) x : M)
hφW : ∀ x ∈ W, Membership.mem (α := M) W ((φ : (a : M) → M) x : M)
F : ↥V →ₗ[K] ↥V := restrict φ hφV
G : ↥W →ₗ[K] ↥W := restrict φ hφW
ψ : ↥V × ↥W →ₗ[K] ↥V × ↥W := F.prodMap G
e : (↥V × ↥W) ≃ₗ[K] M := V.prodEquivOfIsCompl W hVW
bV : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V) K ↥V := chooseBasis K ↥V
bW : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥W) K ↥W := chooseBasis K ↥W
b : Basis.{u_3, u_2, u_3} (ChooseBasisIndex K ↥V ⊕ ChooseBasisIndex K ↥W) K (↥V × ↥W) := bV.prod bW
hψ :
  ψ =
    ((LinearEquiv.conj.{u_2, u_2, u_3, u_3} (R₁' := K) (R₂' := K) (M₁' := M) (M₂' := ↥V × ↥W) (σ₁'₂' := RingHom.id K)
            (σ₂'₁' := RingHom.id K) e.symm :
          End K M ≃ₗ[K] End K (↥V × ↥W)) :
        (a : End K M) → End K (↥V × ↥W))
      φ
hG : G.charpoly.natTrailingDegree = 0
x : M
h' : x ∈ φ.maxGenEigenspace 0
n : ℕ
h :
  Eq (α := M)
    ((↑((restrict φ hφV ^ n : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ n : (a : M) → M) x : M)
⊢ Eq (α := M)
    ((↑((restrict φ hφV ^ (n + 1) : (a : ↥(φ.maxGenEigenspace 0)) → ↥(φ.maxGenEigenspace 0))
            (Subtype.mk (p := fun (x : M) ↦ x ∈ φ.maxGenEigenspace 0) x h')) :
        M) :
      M)
    ((φ ^ (n + 1) : (a : M) → M) x : M)

Tactic:
simp [pow_succ', *]

Premises used: pow_succ'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
μ : K
rw : finrank.{u_2, u_3} K ↥((φ - HSMul.hSMul (β := End K M) μ 1).maxGenEigenspace 0) = rootMultiplicity μ (charpoly φ)
rw₁ : (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree = rootMultiplicity μ (charpoly φ)
rw₂ :
  (charpoly (φ - HSMul.hSMul (β := End K M) μ 1)).natTrailingDegree =
    ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree
rw₃ rw₄ :
  ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree =
    ((charpoly φ).comp (HAdd.hAdd (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) μ : K[X]))).natTrailingDegree
⊢ finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) = rootMultiplicity μ (charpoly φ)

Tactic:
rw [φ.maxGenEigenspace_eq_maxGenEigenspace_zero, finrank_maxGenEigenspace_zero_eq,
    Polynomial.rootMultiplicity_eq_natTrailingDegree, LinearMap.charpoly_sub_smul]

Premises used: Polynomial.rootMultiplicity_eq_natTrailingDegree, Module.End.maxGenEigenspace_eq_maxGenEigenspace_zero, LinearMap.charpoly_sub_smul, LinearMap.finrank_maxGenEigenspace_zero_eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
μ : K
k : ℕ
grw : finrank.{u_2, u_3} K ↥(φ.maxGenEigenspace μ) ≤ rootMultiplicity μ (charpoly φ)
grw₁ grw₂ : rootMultiplicity μ (charpoly φ) ≤ rootMultiplicity μ (charpoly φ)
⊢ finrank.{u_2, u_3} K ↥((φ.genEigenspace μ : (a : ℕ∞) → Submodule K M) (↑k : ℕ∞) : Submodule K M) ≤
    rootMultiplicity μ (charpoly φ)

Tactic:
grw [Submodule.finrank_mono (φ.genEigenspace_le_maximal μ k), finrank_maxGenEigenspace_eq]

Premises used: Submodule.finrank_mono, Module.End.genEigenspace_le_maximal, LinearMap.finrank_maxGenEigenspace_eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
Goal:
K : Type u_2
M : Type u_3
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : Module.Finite K M
φ : End K M
μ : K
⊢ finrank.{u_2, u_3} K ↥(φ.eigenspace μ) ≤ rootMultiplicity μ (charpoly φ)

Tactic:
finrank_genEigenspace_le ..

Premises used: Set.Mem, setOf, LinearMap.finrank_genEigenspace_le, WithTop.some
-- 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
⊢ HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) =
    0

Tactic:
(CliffordAlgebra.ι_sq_scalar _ m).trans <| map_zero _

Premises used: CliffordAlgebra.ι_sq_scalar, map_zero, Eq.trans
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
rw :
  Eq.{u_1 + 1} (α := A)
    ((g : (a : ExteriorAlgebra R M) → A)
        (HMul.hMul (α := ExteriorAlgebra R M) (β := ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)
          ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M)) :
      A)
    (0 : A)
rw₁ : Eq.{u_1 + 1} (α := A) ((g : (a : ExteriorAlgebra R M) → A) 0 : A) (0 : A)
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 0 0
⊢ HMul.hMul (α := A) (β := A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A)
      ((g : (a : ExteriorAlgebra R M) → A) ((ι R : (a : M) → ExteriorAlgebra R M) m : ExteriorAlgebra R M) : A) =
    0

Tactic:
rw [← map_mul, ι_sq_zero, map_zero]

Premises used: map_zero, ExteriorAlgebra.ι_sq_zero, map_mul
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
⊢ ∀ (a : M →ₗ[R] A),
    (∀ (m : M), HMul.hMul (α := A) (β := A) ((a : (a : M) → A) m : A) ((a : (a : M) → A) m : A) = 0) ↔
      ∀ (m : M),
        HMul.hMul (α := A) (β := A)
            ((((Equiv.refl (M →ₗ[R] A) : (a : M →ₗ[R] A) → M →ₗ[R] A) a : M →ₗ[R] A) : (a : M) → A) m : A)
            ((((Equiv.refl (M →ₗ[R] A) : (a : M →ₗ[R] A) → M →ₗ[R] A) a : M →ₗ[R] A) : (a : M) → A) m : A) =
          (algebraMap R A : (a : R) → A) ((0 : (a : M) → R) m : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0
⊢ AlgHom.toLinearMap
        ((lift R :
            (a : { f : M →ₗ[R] A // ∀ (m : M), (f : (a : M) → A) m * (f : (a : M) → A) m = 0 }) →
              ExteriorAlgebra R M →ₐ[R] A)
          (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
            ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0) f cond)) ∘ₗ
      ι R =
    f

Tactic:
CliffordAlgebra.ι_comp_lift f _

Premises used: CliffordAlgebra.ι_comp_lift
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0
x : M
⊢ Eq.{u_1 + 1} (α := A)
    ((((lift R :
                (a : { f : M →ₗ[R] A // ∀ (m : M), (f : (a : M) → A) m * (f : (a : M) → A) m = 0 }) →
                  ExteriorAlgebra R M →ₐ[R] A)
              (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
                ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0) f
                cond) :
            ExteriorAlgebra R M →ₐ[R] A) :
          (a : ExteriorAlgebra R M) → A)
        ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M) :
      A)
    ((f : (a : M) → A) x : A)

Tactic:
CliffordAlgebra.lift_ι_apply f _ x

Premises used: CliffordAlgebra.lift_ι_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
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0
g : ExteriorAlgebra R M →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι R = f ↔
    g =
      (lift R :
          (a : { f : M →ₗ[R] A // ∀ (m : M), (f : (a : M) → A) m * (f : (a : M) → A) m = 0 }) →
            ExteriorAlgebra R M →ₐ[R] A)
        (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
          ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0) f cond)

Tactic:
CliffordAlgebra.lift_unique f _ _

Premises used: CliffordAlgebra.lift_unique
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
⊢ (lift R :
        (a : { f : M →ₗ[R] A // ∀ (m : M), (f : (a : M) → A) m * (f : (a : M) → A) m = 0 }) →
          ExteriorAlgebra R M →ₐ[R] A)
      (Subtype.mk (p := fun (f : M →ₗ[R] A) ↦
        ∀ (m : M), HMul.hMul (α := A) (β := A) ((f : (a : M) → A) m : A) ((f : (a : M) → A) m : A) = 0)
        (g.toLinearMap ∘ₗ ι R) ⋯) =
    g

Tactic:
CliffordAlgebra.lift_comp_ι g

Premises used: CliffordAlgebra.lift_comp_ι
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
f g : ExteriorAlgebra R M →ₐ[R] A
h : f.toLinearMap ∘ₗ ι R = g.toLinearMap ∘ₗ ι R
⊢ f = g

Tactic:
CliffordAlgebra.hom_ext h

Premises used: CliffordAlgebra.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
C : ExteriorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r)
ι : ∀ (x : M), C ((ExteriorAlgebra.ι R : (a : M) → ExteriorAlgebra R M) x)
mul : ∀ (a b : ExteriorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : ExteriorAlgebra R M), C a → C b → C (a + b)
a : ExteriorAlgebra R M
⊢ C a

Tactic:
CliffordAlgebra.induction algebraMap ι mul add a

Premises used: CliffordAlgebra.induction
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
x : M
⊢ HMul.hMul (α := R) (β := R) ((0 : (a : M) → R) x : R) ((0 : (a : M) → R) x : R) = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : R
⊢ (algebraMapInv : (a : ExteriorAlgebra R M) → R)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) x : ExteriorAlgebra R M) =
    x

Tactic:
simp [algebraMapInv]

Premises used: ExteriorAlgebra.algebraMapInv
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : R
⊢ Eq (α := ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) y : ExteriorAlgebra R M) ↔
    x = y

Tactic:
(algebraMap_leftInverse M).injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, ExteriorAlgebra.algebraMap_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
x : R
⊢ Eq (α := ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    x = 0

Tactic:
map_eq_zero_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_zero_iff, ExteriorAlgebra.algebraMap_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
x : R
⊢ Eq (α := ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (1 : ExteriorAlgebra R M) ↔
    x = 1

Tactic:
map_eq_one_iff (algebraMap _ _) (algebraMap_leftInverse _).injective

Premises used: Function.LeftInverse.injective, Algebra.algebraMap, map_eq_one_iff, ExteriorAlgebra.algebraMap_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
⊢ IsLocalHom (R := R) (S := ExteriorAlgebra R M) (F := R →+* ExteriorAlgebra R M) (algebraMap R (ExteriorAlgebra R M))

Tactic:
isLocalHom_of_leftInverse _ (algebraMap_leftInverse M)

Premises used: ExteriorAlgebra.algebraMap_leftInverse, isLocalHom_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
r : R
⊢ IsUnit (M := ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) ↔
    IsUnit r

Tactic:
isUnit_map_of_leftInverse _ (algebraMap_leftInverse M)

Premises used: isUnit_map_of_leftInverse, ExteriorAlgebra.algebraMap_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
inst_3 : Module.{u1, u2} Rᵐᵒᵖ M
inst_4 : IsCentralScalar R M
x : M
⊢ Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : ExteriorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → ExteriorAlgebra R M) x) :
      TrivSqZeroExt R M)
    (TrivSqZeroExt.inr x : TrivSqZeroExt R M)

Tactic:
lift_ι_apply _ _ _ _

Premises used: TrivSqZeroExt.inr, ExteriorAlgebra.lift_ι_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
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
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
A : Type u_1
inst_3 : Semiring A
inst_4 : Algebra R A
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
⊢ ExteriorAlgebra R M →ₗ[R] M

Tactic:
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap

Premises used: AlgHom.toLinearMap, LinearMap.comp, TrivSqZeroExt.sndHom, ExteriorAlgebra.toTrivSqZeroExt
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
⊢ (ιInv : (a : ExteriorAlgebra R M) → M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M) = x

Tactic:
simp [ιInv]

Premises used: ExteriorAlgebra.ιInv
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x y : M
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) y : ExteriorAlgebra R M) ↔
    x = y

Tactic:
ι_leftInverse.injective.eq_iff

Premises used: Function.LeftInverse.injective, Function.Injective.eq_iff, ExteriorAlgebra.ι_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
x : M
rw :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((ι R : (a : M) → ExteriorAlgebra R M) 0 : ExteriorAlgebra R M)
rw₁ rw₂ :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      (0 : ExteriorAlgebra R M) ↔
    x = 0

Tactic:
rw [← ι_inj R x 0, map_zero]

Premises used: ExteriorAlgebra.ι_inj, map_zero, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) ↔
    x = 0 ∧ r = 0

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
refine_1 :
  ∀
    (h :
      Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
        ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)),
    x = 0 ∧ r = 0
refine_2 :
  x = 0 ∧ r = 0 →
    Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
⊢ Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
      ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M) ↔
    x = 0 ∧ r = 0

Tactic:
refine ⟨fun 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
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
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
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
⊢ Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : ExteriorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → ExteriorAlgebra R M) x) :
      TrivSqZeroExt R M)
    ((0, x) : R × M)

Tactic:
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M)
    ((toTrivSqZeroExt : (a : ExteriorAlgebra R M) → TrivSqZeroExt R M) ((ι R : (a : M) → ExteriorAlgebra R M) x) :
      TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)

Tactic:
rw [h, AlgHom.commutes] at hf0

Premises used: AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
⊢ r = 0 ∧ 0 = x

Tactic:
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0

Tactic:
this.symm.imp_left Eq.symm

Premises used: And.imp_left, Eq.symm, And.symm
-- Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Goal:
R : Type u1
inst : CommRing R
M : Type u2
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
r : R
h :
  Eq (α := ExteriorAlgebra R M) ((ι R : (a : M) → ExteriorAlgebra R M) x : ExteriorAlgebra R M)
    ((algebraMap R (ExteriorAlgebra R M) : (a : R) → ExteriorAlgebra R M) r : ExteriorAlgebra R M)
this_1 : Module.{u1, u2} Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) ⋯)
this_2 : IsCentralScalar R M
hf0 :
  Eq (α := TrivSqZeroExt R M) ((algebraMap R (TrivSqZeroExt R M) : (a : R) → TrivSqZeroExt R M) r : TrivSqZeroExt R M)
    ((0, x) : R × M)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0

Tactic:
exact this.symm.imp_left Eq.symm

Premises used: And.imp_left, Eq.symm, And.symm