awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
X : Type v
inst : CommRing R
inst_1 : Nontrivial R
rw : Cardinal.lift.{max u v, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
rw₁ : Cardinal.lift.{u, v} (Cardinal.mk (FreeMonoid X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
rw₂ rw₃ : Cardinal.lift.{u, v} (Cardinal.mk (List X)) = Cardinal.lift.{u, v} (Cardinal.mk (List X))
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))

Tactic:
rw [← (Basis.mk_eq_rank'.{_, _, _, u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
    Cardinal.lift_umax.{v, u}, FreeMonoid]

Premises used: FreeMonoid
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
rw :
  Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀
⊢ Module.rank R ↥(adjoin R s) ≤ max #(↑s : Type v) ℵ₀

Tactic:
rw [adjoin_eq_range_freeAlgebra_lift]

Premises used: Algebra.adjoin_eq_range_freeAlgebra_lift
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
inl :
  Subsingleton R →
    Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
      max #(↑s : Type v) ℵ₀
inr :
  Nontrivial R →
    Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
      max #(↑s : Type v) ℵ₀
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Subsingleton R
inl : 1 ≤ max #(↑s : Type v) ℵ₀
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀

Tactic:
rw [rank_subsingleton]

Premises used: rank_subsingleton
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Subsingleton R
⊢ 1 ≤ max #(↑s : Type v) ℵ₀

Tactic:
one_le_aleph0.trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans, Cardinal.one_le_aleph0
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Subsingleton R
⊢ 1 ≤ max #(↑s : Type v) ℵ₀

Tactic:
exact one_le_aleph0.trans (le_max_right _ _)

Premises used: le_max_right, LE.le.trans, Cardinal.one_le_aleph0
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
inr :
  lift.{max u v, v}
      (Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s))))) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
⊢ Module.rank R
      ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
          ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
            (Subtype.val (p := fun (x : S) ↦ x ∈ s)))) ≤
    max #(↑s : Type v) ℵ₀

Tactic:
rw [← lift_le.{max u v}]
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s))))) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)

Tactic:
(lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_

Premises used: AlgHom.toLinearMap, Set.Mem, LinearMap.range, LE.le.trans, FreeAlgebra.lift, lift_rank_range_le, Subtype.val, DFunLike.coe, AlgHom.range, Submodule.copy
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
inr :
  lift.{v, max u v} (Module.rank R (FreeAlgebra.{u, v} R { x : S // x ∈ s })) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(AlgHom.range (A := FreeAlgebra.{u, v} R { x : S // x ∈ s })
            ((FreeAlgebra.lift R : (a : { x : S // x ∈ s } → S) → FreeAlgebra R { x : S // x ∈ s } →ₐ[R] S)
              (Subtype.val (p := fun (x : S) ↦ x ∈ s))))) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)

Tactic:
refine (lift_rank_range_le (FreeAlgebra.lift R ((↑) : s → S)).toLinearMap).trans ?_

Premises used: AlgHom.toLinearMap, LE.le.trans, FreeAlgebra.lift, lift_rank_range_le, Subtype.val, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
inr : #(List { x : S // x ∈ s }) ≤ max ℵ₀ #(↑s : Type v)
⊢ lift.{v, max u v} (Module.rank R (FreeAlgebra.{u, v} R { x : S // x ∈ s })) ≤
    lift.{max u v, v} (max #(↑s : Type v) ℵ₀)

Tactic:
rw [FreeAlgebra.rank_eq, lift_id'.{v, u}, lift_umax.{v, u}, lift_le, max_comm]

Premises used: FreeAlgebra.rank_eq, Cardinal.lift_le, max_comm
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ #(List { x : S // x ∈ s }) ≤ max ℵ₀ #(↑s : Type v)

Tactic:
mk_list_le_max _

Premises used: Cardinal.mk_list_le_max
-- Module: Mathlib.LinearAlgebra.FreeAlgebra
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
s : Set S
h : Nontrivial R
⊢ #(List { x : S // x ∈ s }) ≤ max ℵ₀ #(↑s : Type v)

Tactic:
exact mk_list_le_max _

Premises used: Cardinal.mk_list_le_max
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
⊢ ∃ (S : Set M), Nonempty (Basis (↑S : Type v) R M)

Tactic:
let ⟨_I, b⟩ := exists_basis R M; ⟨Set.range b, ⟨b.reindexRange⟩⟩

Premises used: Exists, Module.Basis.reindexRange, Set.Elem, _private.0.Module.Free.exists_set.match_1, Nonempty.intro, Module.Basis, Module.Free.exists_basis, Exists.intro, Nonempty, Set.range, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Free R M ↔ ∃ (S : Set M), Nonempty (Basis (↑S : Type v) R M)

Tactic:
⟨fun _ ↦ Free.exists_set .., fun ⟨S, hS⟩ ↦ ⟨nonempty_sigma.2 ⟨S, hS⟩⟩⟩

Premises used: Iff.mpr, Set.Elem, Module.Free, Module.Free.exists_set, Iff.intro, Exists.intro, nonempty_sigma, Module.Free.mk, _private.0.Module.free_iff_set.match_1
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
b : Basis ι R M
⊢ Free R M

Tactic:
(free_def R M).2 ⟨Set.range b, ⟨b.reindexRange⟩⟩

Premises used: Iff.mpr, Module.Basis.reindexRange, Set.Elem, Nonempty.intro, Module.free_def, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
⊢ IsTorsionFree R M

Tactic:
let ⟨⟨_, b⟩⟩ := exists_basis (R := R) (M := M)
  b.isTorsionFree

Premises used: Module.IsTorsionFree, _private.0.Module.Free.exists_set.match_1, Module.Basis.isTorsionFree, Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Nontrivial M
⊢ Nonempty.{v + 1} (ChooseBasisIndex R M)

Tactic:
(Module.Free.chooseBasis R M).index_nonempty

Premises used: Module.Basis.index_nonempty, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Infinite R
inst_5 : Nontrivial M
⊢ Infinite M

Tactic:
(Equiv.infinite_iff (chooseBasis R M).repr.toEquiv).mpr Finsupp.infinite_of_right

Premises used: Iff.mpr, Module.Basis.repr, LinearEquiv.toEquiv, Equiv.infinite_iff, Finsupp.infinite_of_right, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Nontrivial M
⊢ FaithfulSMul R M

Tactic:
.of_injective _ (chooseBasis R M).repr.symm.injective

Premises used: LinearEquiv.symm, FaithfulSMul.of_injective, Module.Basis.repr, LinearEquiv.injective, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
obtain : ∀ (e₃ : M ≃ₗ[R] I →₀ R), Free R' M'
⊢ Free R' M'

Tactic:
obtain ⟨e₃ : M ≃ₗ[R] I →₀ R⟩ := Module.Free.chooseBasis R M

Premises used: Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (LinearEquiv.toAddEquiv (e₂.symm.trans e₃)).trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
⊢ ∀ (x : M'),
    Eq (α := I →₀ R') ((e : (a : M') → I →₀ R') x : I →₀ R')
      ((Finsupp.mapRange.addEquiv e₁.toAddEquiv : (a : I →₀ R) → I →₀ R')
          ((e₃ : (a : M) → I →₀ R) ((e₂.symm : (a : M') → M) x)) :
        I →₀ R')

Tactic:
have he (x) : e x = Finsupp.mapRange.addEquiv (ι := I) e₁.toAddEquiv (e₃ (e₂.symm x)) := rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (LinearEquiv.toAddEquiv (e₂.symm.trans e₃)).trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he :
  ∀ (x : M'),
    Eq (α := I →₀ R') ((e : (a : M') → I →₀ R') x : I →₀ R')
      ((Finsupp.mapRange.addEquiv e₁.toAddEquiv : (a : I →₀ R) → I →₀ R')
          ((e₃ : (a : M) → I →₀ R) ((e₂.symm : (a : M') → M) x)) :
        I →₀ R')
m : R'
x : M'
i : I
⊢ Eq.{u_3 + 1} (α := R') ((e.toFun (m • x) : (a : I) → R') i : R')
    ((HSMul.hSMul (α := R') ((RingHom.id R' : (a : R') → R') m : R') (e.toFun x) : (a : I) → R') i : R')

Tactic:
simp [e₁, he, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (LinearEquiv.toAddEquiv (e₂.symm.trans e₃)).trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he :
  ∀ (x : M'),
    Eq (α := I →₀ R') ((e : (a : M') → I →₀ R') x : I →₀ R')
      ((Finsupp.mapRange.addEquiv e₁.toAddEquiv : (a : I →₀ R) → I →₀ R')
          ((e₃ : (a : M) → I →₀ R) ((e₂.symm : (a : M') → M) x)) :
        I →₀ R')
e' : M' ≃ₗ[R'] I →₀ R' :=
  let __spread.0 := e;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Free R' M'

Tactic:
of_basis (.ofRepr e')

Premises used: Module.Basis.ofRepr, Module.Free.of_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
inst_8 : Free R M
e₁ : R ≃+* R' := RingHomInvPair.toRingEquiv σ σ'
I : Type u_4 := ChooseBasisIndex R M
e₃ : M ≃ₗ[R] I →₀ R
e : M' ≃+ (I →₀ R') := (LinearEquiv.toAddEquiv (e₂.symm.trans e₃)).trans (Finsupp.mapRange.addEquiv e₁.toAddEquiv)
he :
  ∀ (x : M'),
    Eq (α := I →₀ R') ((e : (a : M') → I →₀ R') x : I →₀ R')
      ((Finsupp.mapRange.addEquiv e₁.toAddEquiv : (a : I →₀ R) → I →₀ R')
          ((e₃ : (a : M) → I →₀ R) ((e₂.symm : (a : M') → M) x)) :
        I →₀ R')
e' : M' ≃ₗ[R'] I →₀ R' :=
  let __spread.0 := e;
  { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
    right_inv := ⋯ }
⊢ Free R' M'

Tactic:
exact of_basis (.ofRepr e')

Premises used: Module.Basis.ofRepr, Module.Free.of_basis
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
P : Type v
inst_3 : AddCommMonoid P
inst_4 : Module R P
h : Free R P
e : P ≃ₗ[R] N
⊢ Free R N

Tactic:
of_equiv e

Premises used: Module.Free.of_equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
R' : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring R'
inst_4 : AddCommMonoid M'
inst_5 : Module R' M'
σ : R →+* R'
σ' : R' →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] M'
⊢ Free R M ↔ Free R' M'

Tactic:
⟨fun _ ↦ of_equiv e₂, fun _ ↦ of_equiv e₂.symm⟩

Premises used: LinearEquiv.symm, Module.Free.of_equiv, Iff.intro
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Small.{w, v} M
⊢ Free.{u, w} R (Shrink.{w, v} M)

Tactic:
Module.Free.of_equiv (Shrink.linearEquiv R M).symm

Premises used: LinearEquiv.symm, Module.Free.of_equiv, Shrink.linearEquiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
⊢ Free R R

Tactic:
of_basis (Basis.singleton Unit R)

Premises used: Unit, Module.Free.of_basis, Module.Basis.singleton
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
⊢ Free R (ULift.{u_2, v} M)

Tactic:
of_equiv ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, ULift.moduleEquiv, Module.Free.of_equiv
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
ι : Type u_1
R : Type u
M : Type v
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Subsingleton N
⊢ Free R N

Tactic:
of_basis.{u, z, z} (Basis.empty N : Basis PEmpty R N)

Premises used: Module.Free.of_basis, Module.Basis.empty
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
N : Type z
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : Subsingleton R
⊢ Free R N

Tactic:
letI := Module.subsingleton R N
  Module.Free.of_subsingleton R N

Premises used: Module.Free.of_subsingleton
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : Eq.{u_2 + 1} (α := S) ((B : (a : ι) → S) i : S) (1 : S)
r : R
h :
  ∀ (j : ι),
    Eq.{u + 1} (α := R)
      ((((B.repr : (a : S) → ι →₀ R) ((algebraMap R S : (a : R) → S) r) : ι →₀ R) : (a : ι) → R) j : R)
      ((Finsupp.single i r : (a : ι) → R) j : R)
⊢ Eq (α := ι →₀ R) ((B.repr : (a : S) → ι →₀ R) ((algebraMap R S : (a : R) → S) r) : ι →₀ R)
    (Finsupp.single i r : ι →₀ R)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
hBi : Eq.{u_2 + 1} (α := S) ((B : (a : ι) → S) i : S) (1 : S)
r : R
j : ι
⊢ Eq.{u + 1} (α := R) ((((B.repr : (a : S) → ι →₀ R) ((algebraMap R S : (a : R) → S) r) : ι →₀ R) : (a : ι) → R) j : R)
    ((Finsupp.single i r : (a : ι) → R) j : R)

Tactic:
simp [Algebra.algebraMap_eq_smul_one, ← hBi]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
simp :
  (∀ (g : End R M) (x : M),
      Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)) ↔
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
⊢ Membership.mem (γ := Set (End R M)) (Set.center (End R M)) f ↔ ∃ (α : R) (hα : α ∈ Set.center R), f = smulLeft α hα

Tactic:
simp only [Semigroup.mem_center_iff, LinearMap.ext_iff, mul_apply]

Premises used: LinearMap.ext_iff, Semigroup.mem_center_iff, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
⊢ (∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)) →
    ∀ (g : End R M) (x : M),
      Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
refine :
  ∀
    (h :
      ∀ (g : End R M) (x : M),
        Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M)
          ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)),
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
⊢ (∀ (g : End R M) (x : M),
      Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)) ↔
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)

Tactic:
refine ⟨fun h ↦ ?_, by simp_all⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
pos :
  Subsingleton M →
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
neg :
  Nontrivial M →
    ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
      ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)

Tactic:
by_cases! Subsingleton M

Premises used: Subsingleton
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
h_1 : Subsingleton M
⊢ ∀ (g : R), g * 0 = 0 * g

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
h_1 : Subsingleton M
⊢ ∃ (α : R) (h : ∀ (g : R), g * α = α * g),
    ∀ (x : M), Eq (α := M) ((f : (a : M) → M) x : M) ((smulLeft α ⋯ : (a : M) → M) x : M)

Tactic:
exact ⟨0, by simp, fun _ ↦ Subsingleton.allEq _ _⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
h_1 : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
x : M
⊢ (f : (a : M) → M) x =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R)
      ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                ((f : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) :
              Finsupp.{u_3, u_2} (Free.ChooseBasisIndex R M) R) :
            (a : Free.ChooseBasisIndex R M) → R)
          i :
        R)
      x

Tactic:
simpa using (h ((b.coord i).smulRight x) (b i)).symm

Premises used: Module.Basis.coord, LinearMap.smulRight, Eq.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.Basic
Goal:
R : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
f : End R M
h :
  ∀ (g : End R M) (x : M),
    Eq (α := M) ((g : (a : M) → M) ((f : (a : M) → M) x : M) : M) ((f : (a : M) → M) ((g : (a : M) → M) x : M) : M)
h_1 : Nontrivial M
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
i : Free.ChooseBasisIndex R M := ⋯.some
⊢ ∀ (x : M),
    (f : (a : M) → M) x =
      HSMul.hSMul.{u_2, u_3, u_3} (α := R)
        ((((b.repr : (a : M) → Free.ChooseBasisIndex R M →₀ R)
                  ((f : (a : M) → M) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) :
                Finsupp.{u_3, u_2} (Free.ChooseBasisIndex R M) R) :
              (a : Free.ChooseBasisIndex R M) → R)
            i :
          R)
        x

Tactic:
have H x : f x = b.repr (f (b i)) i • x := by simpa using (h ((b.coord i).smulRight x) (b i)).symm