awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
hli : LinearIndependent.{u_4, u_2, u_3} K (M := V) fun (i : κ) ↦ (↑((b : (a : κ) → ↥M) i) : V)
rw :
  LE.le (α := Submodule K V) ⊤
    (span K (↑(map M.subtype (span R (Set.range.{u_3, u_4 + 1} (ι := κ) (⇑b : (a : κ) → ↥M)))) : Set V))
⊢ LE.le.{u_3} (α := Submodule K V) ⊤
    (span K (Set.range fun (i : κ) ↦ Function.comp (β := ↥M) (⇑M.subtype : (a : ↥M) → V) (⇑b : (a : κ) → ↥M) i))

Tactic:
rw [← Submodule.span_span_of_tower R, Set.range_comp, ← Submodule.map_span]

Premises used: Set.range_comp, Submodule.span_span_of_tower, Submodule.map_span
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
hli : LinearIndependent.{u_4, u_2, u_3} K (M := V) fun (i : κ) ↦ (↑((b : (a : κ) → ↥M) i) : V)
⊢ LE.le (α := Submodule K V) ⊤
    (span K (↑(map M.subtype (span R (Set.range.{u_3, u_4 + 1} (ι := κ) (⇑b : (a : κ) → ↥M)))) : Set V))

Tactic:
simp [b.span_eq, Submodule.map_top, span_eq_top]

Premises used: Submodule.map_top, Submodule.IsLattice.span_eq_top, Module.Basis.span_eq
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsFractionRing R K
κ : Type u_4
M : Submodule R V
inst_8 : IsLattice K M
b : Basis.{u_4, u_1, u_3} κ R ↥M
k : κ
⊢ Eq.{u_3 + 1} (α := V) ((Basis.extendOfIsLattice K b : (a : κ) → V) k : V) ((↑((b : (a : κ) → ↥M) k) : V) : V)

Tactic:
simp [Basis.extendOfIsLattice]

Premises used: Module.Basis.extendOfIsLattice
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : Module.Finite K V
inst_9 : IsFractionRing R K
M : Submodule R V
hfg : M.FG
hr : Module.rank K V ≤ Module.rank R ↥M
⊢ Eq (α := Submodule K V) (span K (↑M : Set V)) ⊤

Tactic:
simpa using Submodule.span_range_eq_top_of_injective_of_rank_le M.injective_subtype hr

Premises used: Submodule.injective_subtype, Submodule.span_range_eq_top_of_injective_of_rank_le
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsTorsionFree R K
M : Submodule R V
inst_10 : IsLattice K M
⊢ IsTorsionFree R V

Tactic:
have := Module.IsTorsionFree.trans_faithfulSMul R K V
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsTorsionFree R K
M : Submodule R V
inst_10 : IsLattice K M
this : IsTorsionFree R V
⊢ Free.{u_1, u_3} R ↥M

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : IsFractionRing R K
M : Submodule R V
inst_10 : IsLattice K M
b : Basis.{u_3, u_1, u_3} (Free.ChooseBasisIndex R ↥M) R ↥M := Free.chooseBasis R ↥M
rw : (↑(Fintype.card.{u_3} (Free.ChooseBasisIndex R ↥M)) : Cardinal.{u_3}) = Module.rank K V
rw₁ rw₂ : Module.rank K V = Module.rank K V
⊢ Module.rank R ↥M = Module.rank K V

Tactic:
rw [rank_eq_card_basis b, ← rank_eq_card_basis (b.extendOfIsLattice K)]

Premises used: rank_eq_card_basis, Module.Basis.extendOfIsLattice
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
ι : Type u_4
inst_5 : Fintype ι
inst_6 : IsFractionRing R K
M : Submodule R (ι → K)
inst_7 : IsLattice K M
rw : Module.rank K (ι → K) = (↑(Fintype.card ι) : Cardinal.{max u_2 u_4})
⊢ Module.rank R ↥M = (↑(Fintype.card ι) : Cardinal.{max u_2 u_4})

Tactic:
rw [IsLattice.rank' K M]

Premises used: Submodule.IsLattice.rank'
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
ι : Type u_4
inst_5 : Fintype ι
inst_6 : IsFractionRing R K
M : Submodule R (ι → K)
inst_7 : IsLattice K M
⊢ Module.rank K (ι → K) = (↑(Fintype.card ι) : Cardinal.{max u_2 u_4})

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
inst_3 : IsDomain R
inst_4 : IsPrincipalIdealRing R
ι : Type u_4
inst_5 : Fintype ι
inst_6 : IsFractionRing R K
M : Submodule R (ι → K)
inst_7 : IsLattice K M
⊢ finrank R ↥M = Fintype.card ι

Tactic:
Module.finrank_eq_of_rank_eq (IsLattice.rank_of_pi K M)

Premises used: Submodule.IsLattice.rank_of_pi, Module.finrank_eq_of_rank_eq
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ IsNoetherian.{u_1, u_3} R ↥(M ⊓ N)

Tactic:
have : IsNoetherian R ↥(M ⊓ N) := isNoetherian_of_le inf_le_left
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
this : IsNoetherian.{u_1, u_3} R ↥(M ⊓ N)
rw : Module.Finite.{u_1, u_3} R ↥(M ⊓ N)
⊢ (M ⊓ N).FG

Tactic:
rw [← Module.Finite.iff_fg]

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
this : IsNoetherian.{u_1, u_3} R ↥(M ⊓ N)
⊢ Module.Finite.{u_1, u_3} R ↥(M ⊓ N)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
rw : Eq (α := Submodule K V) (span K (↑(M ⊓ N).subtype.range : Set V)) ⊤
⊢ Eq (α := Submodule K V) (span K (↑(M ⊓ N) : Set V)) ⊤

Tactic:
rw [← range_subtype (M ⊓ N)]

Premises used: Submodule.range_subtype, Min.min
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
apply : Module.rank K V ≤ Module.rank R ↥(M ⊓ N)
⊢ Eq (α := Submodule K V) (span K (↑(M ⊓ N).subtype.range : Set V)) ⊤

Tactic:
apply Submodule.span_range_eq_top_of_injective_of_rank_le (M ⊓ N).injective_subtype

Premises used: Submodule.injective_subtype, Submodule.span_range_eq_top_of_injective_of_rank_le, Min.min
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
⊢ Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank R ↥M + Module.rank R ↥N

Tactic:
have h := Submodule.rank_sup_add_rank_inf_eq M N
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
h : Module.rank R ↥(M ⊔ N) + Module.rank R ↥(M ⊓ N) = Module.rank R ↥M + Module.rank R ↥N
⊢ Module.rank K V + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank K V

Tactic:
rw [IsLattice.rank' K M, IsLattice.rank' K N, IsLattice.rank'] at h

Premises used: Submodule.IsLattice.rank'
-- Module: Mathlib.Algebra.Module.Lattice
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : Field K
inst_2 : Algebra R K
V : Type u_3
inst_3 : AddCommGroup V
inst_4 : Module K V
inst_5 : Module R V
inst_6 : IsScalarTower R K V
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Module.Finite K V
inst_10 : IsFractionRing R K
M N : Submodule R V
inst_11 : IsLattice K M
inst_12 : IsLattice K N
h : Module.rank K V + Module.rank R ↥(M ⊓ N) = Module.rank K V + Module.rank K V
rw rw₁ : Module.rank K V ≤ Module.rank K V
⊢ Module.rank K V ≤ Module.rank R ↥(M ⊓ N)

Tactic:
rw [Cardinal.eq_of_add_eq_add_left h (Module.rank_lt_aleph0 K V)]

Premises used: Cardinal.eq_of_add_eq_add_left, Module.rank_lt_aleph0
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
M : Type u_7
N : Type u_8
A : Type u_9
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module A N
inst_7 : SMulCommClass R A N
f : M →ₗ[R] N
⊢ Eq (α := M → N) ((ltoFun R M N A : (a : M →ₗ[R] N) → M → N) f : M → N) ((⇑f : (a : M) → N) : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
x y : M
⊢ HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') (x + y) =
    HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') x + HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') y

Tactic:
simp only [DomMulAct.smul_apply, f.map_add, smul_add]

Premises used: LinearMap.map_add, DomMulAct.smul_apply, smul_add
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
c : R
x : M
simp_rw :
  (f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') (c • x)) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') (β := M') ((σ₁₂ : (a : R) → R') c : R')
      ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')
simp_rw₁ :
  (f : (a : M) → M') (c • HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') (β := M') ((σ₁₂ : (a : R) → R') c : R')
      ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')
⊢ HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') (c • x) =
    HSMul.hSMul.{u_2, u_5, u_5} (α := R') ((σ₁₂ : (a : R) → R') c : R')
      (HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M') x)

Tactic:
simp_rw [DomMulAct.smul_apply, ← smul_comm, f.map_smulₛₗ]

Premises used: DomMulAct.smul_apply, LinearMap.map_smulₛₗ, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
x : M
⊢ Eq.{u_5 + 1} (α := M') ((a • f : (a : M) → M') x : M')
    ((f : (a : M) → M') (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') a : S') x) : M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
a : S'
f : M →ₛₗ[σ₁₂] M'
x : M
⊢ Eq.{u_5 + 1} (α := M')
    ((HSMul.hSMul (α := S'ᵈᵐᵃ) ((DomMulAct.mk : (a : S') → S'ᵈᵐᵃ) a : S'ᵈᵐᵃ) f : (a : M) → M') x : M')
    ((f : (a : M) → M') (a • x) : M')

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
a : S'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
⊢ (⇑(a • f) : (a : M) → M') = HSMul.hSMul (β := (a : M) → M') a (⇑f : (a : M) → M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst_6 : Monoid S'
inst_7 : DistribMulAction S' M
inst_8 : SMulCommClass R S' M
inst_9 : Monoid T'
inst_10 : DistribMulAction T' M
inst_11 : SMulCommClass R T' M
inst_12 : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
simp_rw :
  Eq.{u_5 + 1} (α := M')
    ((f : (a : M) → M')
        (HSMul.hSMul (α := T') ((Equiv.symm DomMulAct.mk : (a : T'ᵈᵐᵃ) → T') t : T')
          (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') s : S') m)) :
      M')
    ((f : (a : M) → M')
        (HSMul.hSMul (α := S') ((Equiv.symm DomMulAct.mk : (a : S'ᵈᵐᵃ) → S') s : S')
          (HSMul.hSMul (α := T') ((Equiv.symm DomMulAct.mk : (a : T'ᵈᵐᵃ) → T') t : T') m)) :
      M')
⊢ Eq.{u_5 + 1} (α := M') ((s • t • f : (a : M) → M') m : M') ((t • s • f : (a : M) → M') m : M')

Tactic:
simp_rw [DomMulAct.smul_linearMap_apply, smul_comm]

Premises used: DomMulAct.smul_linearMap_apply, SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
inst_6 : Semiring S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : SMulCommClass R' S M'
inst_10 : Module.IsTorsionFree S M'
⊢ Module.IsTorsionFree S (M →ₛₗ[σ₁₂] M')

Tactic:
coe_injective.moduleIsTorsionFree _ coe_smul

Premises used: LinearMap.coe_smul, Function.Injective.moduleIsTorsionFree, LinearMap.coe_injective
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
inst_6 : Semiring S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : SMulCommClass R' S M'
inst_10 : SMulCommClass R S M
x x_1 : Sᵈᵐᵃ
x_2 : M →ₛₗ[σ₁₂] M'
x_3 : M
simp_rw :
  Eq.{u_5 + 1} (α := M')
    ((x_2 : (a : M) → M') (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (x + x_1) : S) x_3) : M')
    ((x_2 : (a : M) → M')
        (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x : S)
            ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x_1 : S) •
          x_3) :
      M')
⊢ Eq.{u_5 + 1} (α := M') (((x + x_1) • x_2 : (a : M) → M') x_3 : M') ((x • x_2 + x_1 • x_2 : (a : M) → M') x_3 : M')

Tactic:
simp_rw [add_apply, DomMulAct.smul_linearMap_apply, ← map_add, ← add_smul]

Premises used: DomMulAct.smul_linearMap_apply, LinearMap.add_apply, map_add, add_smul
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
inst_6 : Semiring S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : SMulCommClass R' S M'
inst_10 : SMulCommClass R S M
x x_1 : Sᵈᵐᵃ
x_2 : M →ₛₗ[σ₁₂] M'
x_3 : M
⊢ Eq.{u_5 + 1} (α := M')
    ((x_2 : (a : M) → M') (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (x + x_1) : S) x_3) : M')
    ((x_2 : (a : M) → M')
        (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x : S)
            ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) x_1 : S) •
          x_3) :
      M')

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : Semiring R'
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : Module R' M'
σ₁₂ : R →+* R'
inst_6 : Semiring S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : SMulCommClass R' S M'
inst_10 : SMulCommClass R S M
x : M →ₛₗ[σ₁₂] M'
x_1 : M
⊢ Eq.{u_5 + 1} (α := M') ((HSMul.hSMul (α := Sᵈᵐᵃ) 0 x : (a : M) → M') x_1 : M') ((0 : (a : M) → M') x_1 : M')

Tactic:
simp [DomMulAct.smul_linearMap_apply, DomMulAct.mk, MulOpposite.opEquiv]

Premises used: DomMulAct.smul_linearMap_apply, MulOpposite.opEquiv, DomMulAct.mk
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b : A
h : ∀ (x : A), Eq (α := A) ((mulLeft R (a * b) : (a : A) → A) x : A) ((mulLeft R a ∘ₗ mulLeft R b : (a : A) → A) x : A)
⊢ Eq (α := A →ₗ[R] A) (mulLeft R (a * b)) (mulLeft R a ∘ₗ mulLeft R b)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b x : A
⊢ Eq (α := A) ((mulLeft R (a * b) : (a : A) → A) x : A) ((mulLeft R a ∘ₗ mulLeft R b : (a : A) → A) x : A)

Tactic:
simp only [mulLeft_apply, comp_apply, mul_assoc]

Premises used: mul_assoc, LinearMap.comp_apply, LinearMap.mulLeft_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : A
h :
  ∀ (x : A), Eq (α := A) ((mulRight R (a * b) : (a : A) → A) x : A) ((mulRight R b ∘ₗ mulRight R a : (a : A) → A) x : A)
⊢ Eq (α := A →ₗ[R] A) (mulRight R (a * b)) (mulRight R b ∘ₗ mulRight R a)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b x : A
⊢ Eq (α := A) ((mulRight R (a * b) : (a : A) → A) x : A) ((mulRight R b ∘ₗ mulRight R a : (a : A) → A) x : A)

Tactic:
simp only [mulRight_apply, comp_apply, mul_assoc]

Premises used: mul_assoc, LinearMap.comp_apply, LinearMap.mulRight_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b : A
h : Eq (α := A →ₗ[R] A) (mulLeft R a) (mulLeft R b)
⊢ a = b

Tactic:
simpa using LinearMap.ext_iff.mp h 1

Premises used: LinearMap.ext_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : A
h : Eq (α := A →ₗ[R] A) (mulRight R a) (mulRight R b)
⊢ a = b

Tactic:
simpa using LinearMap.ext_iff.mp h 1

Premises used: LinearMap.ext_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
⊢ Eq.{u_7 + 1} (α := A →ₗ[R] A) (mulLeft R 1) id

Tactic:
ext one_mul

Premises used: LinearMap.ext, one_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : A
⊢ Eq (α := A →ₗ[R] A) (mulLeft R a) 0 ↔ a = 0

Tactic:
mulLeft_zero_eq_zero R A ▸ mulLeft_inj

Premises used: LinearMap.mulLeft_zero_eq_zero, Eq.rec, LinearMap.mulLeft_inj
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
⊢ Eq.{u_7 + 1} (α := A →ₗ[R] A) (mulRight R 1) id

Tactic:
ext mul_one

Premises used: LinearMap.ext, mul_one
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R : Type u_6
A : Type u_7
inst : Semiring R
inst_1 : NonAssocSemiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : A
⊢ Eq (α := A →ₗ[R] A) (mulRight R a) 0 ↔ a = 0

Tactic:
mulRight_zero_eq_zero R A ▸ mulRight_inj

Premises used: Eq.rec, LinearMap.mulRight_zero_eq_zero, LinearMap.mulRight_inj
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
h :
  ∀ (i : κ),
    Sum.elim 0 (f + g) (inl i) = HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inl i)
h₁ :
  ∀ (i : ι),
    Sum.elim.{u_7, u_6, u_8 + 1} (α := κ) 0 (f + g) (inr i) =
      HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inr i)
⊢ Sum.elim 0 (f + g) = HAdd.hAdd (α := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g)

Tactic:
ext (i | i)
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
i : κ
⊢ Sum.elim 0 (f + g) (inl i) = HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inl i)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Basic
Goal:
R_1 : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
ι : Type u_6
κ : Type u_7
R : Type u_8
inst : Semiring R
f g : ι → R
i : ι
⊢ Sum.elim.{u_7, u_6, u_8 + 1} (α := κ) 0 (f + g) (inr i) =
    HAdd.hAdd (α := κ ⊕ ι → R) (β := κ ⊕ ι → R) (Sum.elim 0 f) (Sum.elim 0 g) (inr i)

Tactic:
simp