awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
h :
  ∀ (x : M₃),
    Eq.{u_9 + 1} (α := M₂) ((trans (re₁₂ := inst_7) (re₂₁ := inst_6) (f.trans e.symm) e : (a : M₃) → M₂) x : M₂)
      ((f : (a : M₃) → M₂) x : M₂)
⊢ trans (re₁₂ := inst_7) (re₂₁ := inst_6) (f.trans e.symm) e = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst_6 : RingHomInvPair σ₁₃ σ₃₁
inst_7 : RingHomInvPair σ₃₁ σ₁₃
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
re₂₃ : RingHomInvPair σ₂₃ σ₃₂
re₃₂ : RingHomInvPair σ₃₂ σ₂₃
inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
e : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ ≃ₛₗ[σ₃₂] M₂
x : M₃
⊢ Eq.{u_9 + 1} (α := M₂) ((trans (re₁₂ := inst_7) (re₂₁ := inst_6) (f.trans e.symm) e : (a : M₃) → M₂) x : M₂)
    ((f : (a : M₃) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
M : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M ≃ₗ[R] M) (symm (refl R M)) (refl R M)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.refl, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
h : ∀ (x : M₁), Eq (α := M₁) ((f.trans f.symm : (a : M₁) → M₁) x : M₁) ((refl R₁ M₁ : (a : M₁) → M₁) x : M₁)
⊢ f.trans f.symm = refl R₁ M₁

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₁
⊢ Eq (α := M₁) ((f.trans f.symm : (a : M₁) → M₁) x : M₁) ((refl R₁ M₁ : (a : M₁) → M₁) x : M₁)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
h : ∀ (x : M₂), Eq (α := M₂) ((f.symm.trans f : (a : M₂) → M₂) x : M₂) ((refl R₂ M₂ : (a : M₂) → M₂) x : M₂)
⊢ f.symm.trans f = refl R₂ M₂

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
x : M₂
⊢ Eq (α := M₂) ((f.symm.trans f : (a : M₂) → M₂) x : M₂) ((refl R₂ M₂ : (a : M₂) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
M : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ Eq (α := M →ₗ[R] M) (↑(refl R M) : M →ₗ[R] M) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
f : M₂ → M
h₁ : LeftInverse f (↑e : M →ₛₗ[σ] M₂).toFun
h₂ : RightInverse f (↑e : M →ₛₗ[σ] M₂).toFun
⊢ { toLinearMap := (↑e : M →ₛₗ[σ] M₂), invFun := f, left_inv := h₁, right_inv := h₂ } = e

Tactic:
ext fun _ ↦ rfl

Premises used: LinearEquiv.ext, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
a b : M
⊢ (e : (a : M) → M₂) (a + b) = HAdd.hAdd (α := M₂) (β := M₂) ((e : (a : M) → M₂) a : M₂) ((e : (a : M) → M₂) b : M₂)

Tactic:
map_add e a b

Premises used: map_add
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ Eq.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) 0 : M₂) (0 : M₂)

Tactic:
map_zero e

Premises used: map_zero
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
c : R
x : M
⊢ (e : (a : M) → M₂) (c • x) =
    HSMul.hSMul.{u_6, u_9, u_9} (α := S) (β := M₂) ((σ : (a : R) → S) c : S) ((e : (a : M) → M₂) x : M₂)

Tactic:
e.map_smul' c x

Premises used: LinearEquiv.toLinearMap, LinearMap.map_smul'
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R₁ : Type u_2
N₁ : Type u_12
N₂ : Type u_13
inst : Semiring R₁
inst_1 : AddCommMonoid N₁
inst_2 : AddCommMonoid N₂
module_N₁ : Module R₁ N₁
module_N₂ : Module R₁ N₂
e : N₁ ≃ₗ[R₁] N₂
c : R₁
x : N₁
⊢ (e : (a : N₁) → N₂) (c • x) = HSMul.hSMul (β := N₂) c ((e : (a : N₁) → N₂) x : N₂)

Tactic:
map_smulₛₗ e c x

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
x : M
⊢ Eq.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) (0 : M₂) ↔ x = 0

Tactic:
e.toAddEquiv.map_eq_zero_iff

Premises used: AddEquiv.map_eq_zero_iff, LinearEquiv.toAddEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
x : M
⊢ Ne.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) (0 : M₂) ↔ x ≠ 0

Tactic:
e.toAddEquiv.map_ne_zero_iff

Premises used: AddEquiv.map_ne_zero_iff, LinearEquiv.toAddEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
σ : R →+* S
σ' : S →+* R
inst_4 : Module R M
inst_5 : Module S M₂
inst_6 : RingHomInvPair σ' σ
inst_7 : RingHomInvPair σ σ'
⊢ Bijective (α := M ≃ₛₗ[σ] M₂) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, LinearEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
f : M₂ → M
h₁ : ∀ (x y : M₂), f (x + y) = f x + f y
h₂ :
  ∀ (m : S) (x : M₂),
    { toFun := f, map_add' := h₁ : M₂ →ₙ+ M }.toFun (m • x) =
      HSMul.hSMul.{u_1, u_7, u_7} (α := R) ((σ' : (a : S) → R) m : R)
        ({ toFun := f, map_add' := h₁ : M₂ →ₙ+ M }.toFun x)
h₃ : LeftInverse (⇑e : (a : M) → M₂) { toFun := f, map_add' := h₁, map_smul' := h₂ : M₂ →ₛₗ[σ'] M }.toFun
h₄ : RightInverse (⇑e : (a : M) → M₂) { toFun := f, map_add' := h₁, map_smul' := h₂ : M₂ →ₛₗ[σ'] M }.toFun
⊢ { toFun := f, map_add' := h₁, map_smul' := h₂, invFun := (⇑e : (a : M) → M₂), left_inv := h₃, right_inv := h₄ } =
    e.symm

Tactic:
symm_bijective.injective <| ext fun _ ↦ rfl

Premises used: LinearEquiv.ext, Function.Bijective.injective, LinearEquiv.symm_bijective, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
toLinearMap : M →ₛₗ[σ] M₂
invFun : M₂ → M
h₁ : LeftInverse invFun toLinearMap.toFun
h₂ : RightInverse invFun toLinearMap.toFun
⊢ Eq (α := M₂ ≃ₛₗ[σ'] M) (symm { toLinearMap := toLinearMap, invFun := invFun, left_inv := h₁, right_inv := h₂ })
    { toFun := invFun, map_add' := ⋯, map_smul' := ⋯, invFun := (⇑toLinearMap : (a : M) → M₂), left_inv := ⋯,
      right_inv := ⋯ }

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
to_fun : M → M₂
inv_fun : M₂ → M
map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y
map_smul :
  ∀ (m : R) (x : M),
    { toFun := to_fun, map_add' := map_add : M →ₙ+ M₂ }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := to_fun, map_add' := map_add : M →ₙ+ M₂ }.toFun x)
left_inv : LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul : M →ₗ[R] M₂ }.toFun
right_inv : RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul : M →ₗ[R] M₂ }.toFun
⊢ (⇑(symm
          { toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv,
            right_inv := right_inv }) :
      (a : M₂) → M) =
    inv_fun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
f : M →ₗ[R] M₂
inv_fun : M₂ → M
left_inv : LeftInverse inv_fun f.toFun
right_inv : RightInverse inv_fun f.toFun
⊢ (⇑(symm { toLinearMap := f, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }) : (a : M₂) → M) =
    inv_fun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ Bijective.{u_7 + 1, u_9 + 1} (α := M) (β := M₂) (⇑e : (a : M) → M₂)

Tactic:
e.toEquiv.bijective

Premises used: Equiv.bijective, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ Injective.{u_7 + 1, u_9 + 1} (α := M) (β := M₂) (⇑e : (a : M) → M₂)

Tactic:
e.toEquiv.injective

Premises used: LinearEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ Surjective.{u_7 + 1, u_9 + 1} (α := M) (β := M₂) (⇑e : (a : M) → M₂)

Tactic:
e.toEquiv.surjective

Premises used: LinearEquiv.toEquiv, Equiv.surjective
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
s : Set M
⊢ Eq.{u_9 + 1} (α := Set M₂) ((⇑e : (a : M) → M₂) '' s) ((⇑e.symm : (a : M₂) → M) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm s

Premises used: Equiv.image_eq_preimage_symm, LinearEquiv.toEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
M : Type u_7
M₂ : Type u_9
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
s : Set M₂
⊢ Eq.{u_7 + 1} (α := Set M) ((⇑e.symm : (a : M₂) → M) '' s) ((⇑e : (a : M) → M₂) ⁻¹' s)

Tactic:
e.toEquiv.symm.image_eq_preimage_symm s

Premises used: Equiv.image_eq_preimage_symm, LinearEquiv.toEquiv, Equiv.symm
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M_1 : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst : Semiring R
inst_1 : Semiring S
ι : Type u_14
M : ι → Type u_15
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_15} R (M i)
i j : ι
h : i = j
x : R
x_1 : M i
refl :
  Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) ⋯ : M i ≃+ M i)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) ⋯ : M i ≃+ M i)) x_1)
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) h : M i ≃+ M j)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) h : M i ≃+ M j)) x_1)

Tactic:
cases h
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M_1 : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst : Semiring R
inst_1 : Semiring S
ι : Type u_14
M : ι → Type u_15
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_15} R (M i)
i : ι
x : R
x_1 : M i
__AddEquiv : M i ≃+ M i := AddEquiv.cast (M := M) ⋯
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) ⋯ : M i ≃+ M i)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) ⋯ : M i ≃+ M i)) x_1)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
x : R
⊢ Eq.{u_6 + 1} (α := S) ((f.symm.toSemilinearEquiv.symm : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R : Type u_1
M : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
σ σ' : R →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
x : Module R M
f : M →ₛₗ[σ] M
hf : Involutive (α := M) (⇑f : (a : M) → M)
⊢ Eq (α := (a : M) → M) (⇑(ofInvolutive f hf) : (a : M) → M) (⇑f : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R_1 : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S_1 : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x : V
⊢ (fun (x : W) ↦ HSMul.hSMul (β := V) (↑α⁻¹ : S) ((e.symm : (a : W) → V) x : V))
      (((↑α : S) • (↑e : V →ₗ[R] W)).toFun x) =
    x

Tactic:
simp [LinearMapClass.map_smul_of_tower e.symm, smul_smul]

Premises used: LinearEquiv.symm, smul_smul, LinearMapClass.map_smul_of_tower
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
R_1 : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S_1 : Type u_6
M : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x : W
⊢ ((↑α : S) • (↑e : V →ₗ[R] W)).toFun
      ((fun (x : W) ↦ HSMul.hSMul (β := V) (↑α⁻¹ : S) ((e.symm : (a : W) → V) x : V)) x) =
    x

Tactic:
simp [smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : SMulCommClass R S W
inst_9 : SMul S R
inst_10 : IsScalarTower S R V
inst_11 : IsScalarTower S R W
α : Sˣ
e : V ≃ₗ[R] W
x : V
⊢ (α • e : (a : V) → W) x = HSMul.hSMul (β := W) (↑α : S) ((e : (a : V) → W) x : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : SMulCommClass R S W
inst_9 : SMul S R
inst_10 : IsScalarTower S R V
inst_11 : IsScalarTower S R W
e : V ≃ₗ[R] W
α : Sˣ
x : W
⊢ ((α • e).symm : (a : W) → V) x = HSMul.hSMul (β := V) (↑α⁻¹ : S) ((e.symm : (a : W) → V) x : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : SMulCommClass R S W
inst_9 : SMul S R
inst_10 : IsScalarTower S R V
inst_11 : IsScalarTower S R W
inst_12 : SMulCommClass R S V
e : V ≃ₗ[R] W
α : Sˣ
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : SMulCommClass R S W
inst_9 : SMul S R
inst_10 : IsScalarTower S R V
inst_11 : IsScalarTower S R W
e : V ≃ₗ[R] W
α : Sˣ
⊢ (↑(α • e) : V →ₗ[R] W) = (↑α : S) • (↑e : V →ₗ[R] W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : SMulCommClass R S V
inst_16 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
h :
  ∀ (x : G),
    Eq.{u_17 + 1} (α := W) (((α • e) ≪≫ₗ f : (a : G) → W) x : W)
      ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)
⊢ (α • e) ≪≫ₗ f = HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : SMulCommClass R S V
inst_16 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
x : G
⊢ Eq.{u_17 + 1} (α := W) (((α • e) ≪≫ₗ f : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)

Tactic:
simp [LinearMapClass.map_smul_of_tower f]

Premises used: LinearMapClass.map_smul_of_tower
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
h :
  ∀ (x : G),
    Eq.{u_17 + 1} (α := W) ((e ≪≫ₗ (α • f) : (a : G) → W) x : W)
      ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)
⊢ e ≪≫ₗ (α • f) = HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Defs
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
x : G
⊢ Eq.{u_17 + 1} (α := W) ((e ≪≫ₗ (α • f) : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)

Tactic:
simp