awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
S : Type u_4
M : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
inst_6 : SMul S R
inst_7 : IsScalarTower S R M
α : Sˣ
⊢ HSMul.hSMul (β := M ≃ₗ[R] M) α (refl R M) = DistribMulAction.toLinearEquiv R M α

Tactic:
rfl

Premises used: DistribMulAction.toLinearEquiv, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
e : M ≃+ M₂
h : ∀ (c : R) (x : M), (e : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) x : M₂)
⊢ Eq (α := (a : M) → M₂) (⇑(e.toLinearEquiv h) : (a : M) → M₂) (⇑e : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
M₂ : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
e : M ≃+ M₂
h : ∀ (c : R) (x : M), (e : (a : M) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) x : M₂)
⊢ Eq (α := (a : M₂) → M) (⇑(e.toLinearEquiv h).symm : (a : M₂) → M) (⇑e.symm : (a : M₂) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M
inst_5 : Module R M₂
e : M ≃+ M₂
c : ℕ
a : M
rw rw₁ : HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
⊢ (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)

Tactic:
rw [map_nsmul]

Premises used: map_nsmul
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
e : M ≃+ M₂
⊢ Eq (α := (a : M) → M₂) (⇑e.toNatLinearEquiv : (a : M) → M₂) (⇑e : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
e : M ≃+ M₂
⊢ Eq (α := (a : M₂) → M) (⇑e.toNatLinearEquiv.symm : (a : M₂) → M) (⇑e.symm : (a : M₂) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
e : M ≃+ M₂
⊢ (↑e.toNatLinearEquiv : M ≃+ M₂) = e

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
e : M ≃ₗ[ℕ] M₂
⊢ toNatLinearEquiv (↑e : M ≃+ M₂) = e

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
e : M ≃+ M₂
⊢ e.symm.toNatLinearEquiv = e.toNatLinearEquiv.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, AddEquiv.toNatLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
inst : AddCommMonoid M
⊢ Eq (α := M ≃ₗ[ℕ] M) (toNatLinearEquiv (refl M)) (LinearEquiv.refl ℕ M)

Tactic:
rfl

Premises used: AddEquiv.toNatLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.refl, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommMonoid M
inst_1 : AddCommMonoid M₂
inst_2 : AddCommMonoid M₃
e : M ≃+ M₂
e₂ : M₂ ≃+ M₃
⊢ (e.trans e₂).toNatLinearEquiv = e.toNatLinearEquiv ≪≫ₗ e₂.toNatLinearEquiv

Tactic:
rfl

Premises used: AddEquiv.toNatLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
refine : ∀ (c : ℤ) (a : M), (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)
⊢ M ≃ₗ[ℤ] M₂

Tactic:
refine e.toLinearEquiv fun c a ↦ ?_

Premises used: AddEquiv.toLinearEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ (e.toAddMonoidHom : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e.toAddMonoidHom : (a : M) → M₂) a : M₂)

Tactic:
e.toAddMonoidHom.map_zsmul c a

Premises used: AddMonoidHom.map_zsmul, AddEquiv.toAddMonoidHom
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
h : Eq.{u_7 + 1} (α := M₂) ((e : (a : M) → M₂) (c • a) : M₂) ((e.toAddMonoidHom : (a : M) → M₂) (c • a) : M₂)
h₁ :
  HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) =
    HSMul.hSMul (β := M₂) c ((e.toAddMonoidHom : (a : M) → M₂) a : M₂)
⊢ (e : (a : M) → M₂) (c • a) = HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂)

Tactic:
convert! e.toAddMonoidHom.map_zsmul c a using 1

Premises used: AddMonoidHom.map_zsmul, AddEquiv.toAddMonoidHom
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ Eq.{u_7 + 1} (α := M₂) ((e : (a : M) → M₂) (c • a) : M₂) ((e.toAddMonoidHom : (a : M) → M₂) (c • a) : M₂)

Tactic:
congr(e $(int_smul_eq_zsmul ..))

Premises used: congrArg, id, DFunLike.coe, int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ Eq.{u_7 + 1} (α := M₂) ((e : (a : M) → M₂) (c • a) : M₂) ((e.toAddMonoidHom : (a : M) → M₂) (c • a) : M₂)

Tactic:
exact congr(e $(int_smul_eq_zsmul ..))
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) =
    HSMul.hSMul (β := M₂) c ((e.toAddMonoidHom : (a : M) → M₂) a : M₂)

Tactic:
int_smul_eq_zsmul ..

Premises used: int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ HSMul.hSMul (β := M₂) c ((e : (a : M) → M₂) a : M₂) =
    HSMul.hSMul (β := M₂) c ((e.toAddMonoidHom : (a : M) → M₂) a : M₂)

Tactic:
exact int_smul_eq_zsmul ..

Premises used: int_smul_eq_zsmul
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ Eq (α := (a : M) → M₂) (⇑e.toIntLinearEquiv : (a : M) → M₂) (⇑e : (a : M) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ Eq (α := (a : M₂) → M) (⇑(LinearEquiv.symm e.toIntLinearEquiv) : (a : M₂) → M) (⇑e.symm : (a : M₂) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
h :
  ∀ (x : M),
    Eq.{u_7 + 1} (α := M₂) (((↑e.toIntLinearEquiv : M ≃+ M₂) : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) x : M₂)
⊢ (↑e.toIntLinearEquiv : M ≃+ M₂) = e

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
x : M
⊢ Eq.{u_7 + 1} (α := M₂) (((↑e.toIntLinearEquiv : M ≃+ M₂) : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) x : M₂)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃ₗ[ℤ] M₂
⊢ toIntLinearEquiv (↑e : M ≃+ M₂) = e

Tactic:
DFunLike.coe_injective rfl

Premises used: DFunLike.coe_injective, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
modM : Module ℤ M
modM₂ : Module ℤ M₂
e : M ≃+ M₂
⊢ Eq (α := M₂ ≃ₗ[ℤ] M) e.symm.toIntLinearEquiv (LinearEquiv.symm e.toIntLinearEquiv)

Tactic:
rfl

Premises used: LinearEquiv.symm, AddEquiv.toIntLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
inst : AddCommGroup M
modM : Module ℤ M
⊢ Eq (α := M ≃ₗ[ℤ] M) (toIntLinearEquiv (refl M)) (LinearEquiv.refl ℤ M)

Tactic:
rfl

Premises used: AddEquiv.toIntLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.refl, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst : AddCommGroup M
inst_1 : AddCommGroup M₂
inst_2 : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
e₂ : M₂ ≃+ M₃
⊢ Eq (α := M ≃ₗ[ℤ] M₃) (e.trans e₂).toIntLinearEquiv (e.toIntLinearEquiv ≪≫ₗ e₂.toIntLinearEquiv)

Tactic:
rfl

Premises used: AddEquiv.toIntLinearEquiv, AddEquiv.toLinearEquiv, LinearEquiv.toEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
x y : (x : M) → V x
h :
  ∀ (x_1 : M),
    (e x_1 : (a : V x_1) → R) ((x + y) x_1) =
      HAdd.hAdd (α := M → R) (β := M → R) (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2))
        (fun (x : M) ↦ (e x : (a : V x) → R) (y x)) x_1
⊢ (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) ((x + y) x_1)) =
    HAdd.hAdd (α := M → R) (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) (x x_1)) fun (x : M) ↦ (e x : (a : V x) → R) (y x)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
x y : (x : M) → V x
x_1 : M
⊢ (e x_1 : (a : V x_1) → R) ((x + y) x_1) =
    HAdd.hAdd (α := M → R) (β := M → R) (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2))
      (fun (x : M) ↦ (e x : (a : V x) → R) (y x)) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
m : R
x : (x : M) → V x
h :
  ∀ (x_1 : M),
    (e x_1 : (a : V x_1) → R) ((m • x) x_1) =
      HSMul.hSMul (α := R) (β := M → R) ((RingHom.id R : (a : R) → R) m : R)
        (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2)) x_1
⊢ (fun (x_1 : M) ↦ (e x_1 : (a : V x_1) → R) ((m • x) x_1)) =
    HSMul.hSMul (α := R) (β := M → R) ((RingHom.id R : (a : R) → R) m : R) fun (x_1 : M) ↦
      (e x_1 : (a : V x_1) → R) (x x_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
m : R
x : (x : M) → V x
x_1 : M
⊢ (e x_1 : (a : V x_1) → R) ((m • x) x_1) =
    HSMul.hSMul (α := R) (β := M → R) ((RingHom.id R : (a : R) → R) m : R)
      (fun (x_2 : M) ↦ (e x_2 : (a : V x_2) → R) (x x_2)) x_1

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
x y : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
h :
  ∀ (x_1 : (x : M) → V x) (x_2 : M),
    Eq.{u_1 + 1} (α := R)
      (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((x + y) x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
              map_smul' := ⋯ } :
            (a : (x : M) → V x) → M → R)
          x_1 x_2 :
        R)
      ((HAdd.hAdd (α := ((x : M) → V x) →ₗ[R] M → R)
              { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
                map_smul' := ⋯ : ((x : M) → V x) →ₗ[R] M → R }
              { toFun := fun (s : (x : M) → V x) (x : M) ↦ (y x : (a : V x) → R) (s x), map_add' := ⋯, map_smul' := ⋯ :
                ((x : M) → V x) →ₗ[R] M → R } :
            (a : (x : M) → V x) → M → R)
          x_1 x_2 :
        R)
⊢ { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ ((x + y) x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯,
      map_smul' := ⋯ } =
    HAdd.hAdd (α := ((x : M) → V x) →ₗ[R] M → R)
      { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ (x x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }
      { toFun := fun (s : (x : M) → V x) (x : M) ↦ (y x : (a : V x) → R) (s x), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
x y : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
x_1 : (x : M) → V x
x_2 : M
⊢ Eq.{u_1 + 1} (α := R)
    (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((x + y) x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
    ((HAdd.hAdd (α := ((x : M) → V x) →ₗ[R] M → R)
            { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
              map_smul' := ⋯ : ((x : M) → V x) →ₗ[R] M → R }
            { toFun := fun (s : (x : M) → V x) (x : M) ↦ (y x : (a : V x) → R) (s x), map_add' := ⋯, map_smul' := ⋯ :
              ((x : M) → V x) →ₗ[R] M → R } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
m : R
x : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
h :
  ∀ (x_1 : (x : M) → V x) (x_2 : M),
    Eq.{u_1 + 1} (α := R)
      (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((m • x) x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
              map_smul' := ⋯ } :
            (a : (x : M) → V x) → M → R)
          x_1 x_2 :
        R)
      ((HSMul.hSMul (α := R) (β := ((x : M) → V x) →ₗ[R] M → R) ((RingHom.id R : (a : R) → R) m : R)
              { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
                map_smul' := ⋯ : ((x : M) → V x) →ₗ[R] M → R } :
            (a : (x : M) → V x) → M → R)
          x_1 x_2 :
        R)
⊢ { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ ((m • x) x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯,
      map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := ((x : M) → V x) →ₗ[R] M → R) ((RingHom.id R : (a : R) → R) m : R)
      { toFun := fun (s : (x : M) → V x) (x_1 : M) ↦ (x x_1 : (a : V x_1) → R) (s x_1), map_add' := ⋯, map_smul' := ⋯ :
        ((x : M) → V x) →ₗ[R] M → R }

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
m : R
x : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
x_1 : (x : M) → V x
x_2 : M
⊢ Eq.{u_1 + 1} (α := R)
    (({ toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ ((m • x) x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)
    ((HSMul.hSMul (α := R) (β := ((x : M) → V x) →ₗ[R] M → R) ((RingHom.id R : (a : R) → R) m : R)
            { toFun := fun (s : (x : M) → V x) (x_3 : M) ↦ (x x_3 : (a : V x_3) → R) (s x_3), map_add' := ⋯,
              map_smul' := ⋯ : ((x : M) → V x) →ₗ[R] M → R } :
          (a : (x : M) → V x) → M → R)
        x_1 x_2 :
      R)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
s : (x : M) → V x
⊢ Eq (α := M → R)
    ((((piApply (V := V) : (a : (x : M) → V x →ₗ[R] R) → ((x : M) → V x) →ₗ[R] M → R) e : ((x : M) → V x) →ₗ[R] M → R) :
          (a : (x : M) → V x) → M → R)
        s :
      M → R)
    fun (x : M) ↦ ((e x : (a : V x) → R) (s x) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
V : M → Type u_9
inst : CommSemiring R
inst_1 : (x : M) → AddCommMonoid (V x)
inst_2 : (x : M) → Module.{u_1, u_9} R (V x)
e : (x : M) → LinearMap.{u_1, u_1, u_9, u_1} (RingHom.id R) (V x) R
s : (x : M) → V x
x : M
⊢ Eq.{u_1 + 1} (α := R)
    ((((piApply (V := V) : (a : (x : M) → V x →ₗ[R] R) → ((x : M) → V x) →ₗ[R] M → R) e : ((x : M) → V x) →ₗ[R] M → R) :
          (a : (x : M) → V x) → M → R)
        s x :
      R)
    ((e x : (a : V x) → R) (s x) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
f : R →ₗ[R] M
h :
  Eq.{u_5 + 1} (α := M)
    ((smulRight (S := R) 1 ((fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
    ((f : (a : R) → M) 1 : M)
⊢ smulRight (S := R) 1 ((fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
f : R →ₗ[R] M
⊢ Eq.{u_5 + 1} (α := M)
    ((smulRight (S := R) 1 ((fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
    ((f : (a : R) → M) 1 : M)

Tactic:
simp only [coe_smulRight, Module.End.one_apply, smul_eq_mul, ← map_smul f, mul_one]

Premises used: Module.End.one_apply, LinearMap.coe_smulRight, smul_eq_mul, mul_one, map_smul
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
x : M
⊢ (fun (f : R →ₗ[R] M) ↦ ((f : (a : R) → M) 1 : M)) (smulRight (S := R) 1 x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton M
inst_9 : Subsingleton M₂
⊢ Eq (α := M₂ ≃ₛₗ[σ₂₁] M) (symm 0) 0

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton M
inst_9 : Subsingleton M₂
⊢ Eq (α := (a : M) → M₂) (⇑0 : (a : M) → M₂) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton M
inst_9 : Subsingleton M₂
x : M
⊢ Eq.{u_7 + 1} (α := M₂) ((0 : (a : M) → M₂) x : M₂) (0 : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton R
inst_9 : Subsingleton R₂
⊢ Subsingleton M

Tactic:
haveI := Module.subsingleton R M
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton R
inst_9 : Subsingleton R₂
this : Subsingleton M
⊢ Subsingleton M₂

Tactic:
haveI := Module.subsingleton R₂ M₂
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
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₂
σ₂₁ : R₂ →+* R
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
inst_8 : Subsingleton R
inst_9 : Subsingleton R₂
this_1 : Subsingleton M
this : Subsingleton M₂
⊢ Unique (M ≃ₛₗ[σ₁₂] M₂)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
V : Type u_9
V₂ : Type u_10
⊢ Eq (α := (a : V × V₂ → M) → V → V₂ → M) (⇑(LinearEquiv.curry R M V V₂) : (a : V × V₂ → M) → V → V₂ → M) curry

Tactic:
rfl

Premises used: rfl