awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R_1 : 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
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
x x_1 : Aˣ
h :
  ∀ (x_2 : A),
    Eq (α := A)
      ((let __spread.0 := (x * x_1).mulLeft;
            let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑(x * x_1) : A);
            { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : A) → A)
          x_2 :
        A)
      ((HMul.hMul (α := A ≃ₗ[R] A)
              (let __spread.0 := x.mulLeft;
              let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x : A);
              { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                right_inv := ⋯ : A ≃ₗ[R] A })
              (let __spread.0 := x_1.mulLeft;
              let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x_1 : A);
              { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
                right_inv := ⋯ : A ≃ₗ[R] A }) :
            (a : A) → A)
          x_2 :
        A)
⊢ (let __spread.0 := (x * x_1).mulLeft;
    let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑(x * x_1) : A);
    { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
      right_inv := ⋯ }) =
    HMul.hMul (α := A ≃ₗ[R] A)
      (let __spread.0 := x.mulLeft;
      let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x : A);
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ : A ≃ₗ[R] A })
      (let __spread.0 := x_1.mulLeft;
      let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x_1 : A);
      { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
        right_inv := ⋯ : A ≃ₗ[R] A })

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R_1 : 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
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
x x_1 : Aˣ
x_2 : A
⊢ Eq (α := A)
    ((let __spread.0 := (x * x_1).mulLeft;
          let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑(x * x_1) : A);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : A) → A)
        x_2 :
      A)
    ((HMul.hMul (α := A ≃ₗ[R] A)
            (let __spread.0 := x.mulLeft;
            let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x : A);
            { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
              right_inv := ⋯ : A ≃ₗ[R] A })
            (let __spread.0 := x_1.mulLeft;
            let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑x_1 : A);
            { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
              right_inv := ⋯ : A ≃ₗ[R] A }) :
          (a : A) → A)
        x_2 :
      A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : Aˣ
x : A
⊢ (((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) a : A ≃ₗ[R] A) : (a : A) → A) x = (↑a : A) * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : Aˣ
x : A
⊢ (LinearEquiv.symm ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) a) : (a : A) → A) x = (↑a⁻¹ : A) * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a : Aˣ
⊢ Eq.{u_10 + 1} (α := A ≃ₗ[R] A) (LinearEquiv.symm ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) a))
    ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) a⁻¹)

Tactic:
rfl

Premises used: LinearEquiv.symm, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
a b : Aˣ
⊢ Eq.{u_10 + 1} (α := A ≃ₗ[R] A)
    ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) a ≪≫ₗ (mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) b)
    ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) (b * a))

Tactic:
map_mul _ _ _ |>.symm

Premises used: map_mul, Eq.symm
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
u v : Aˣ
x : A
⊢ Eq (α := A) ((((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) (u * v) : A ≃ₗ[R] A) : (a : A) → A) x : A)
    ((((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) u : A ≃ₗ[R] A) : (a : A) → A)
        ((((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) v : A ≃ₗ[R] A) : (a : A) → A) x : A) :
      A)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
u : Aˣ
⊢ Eq (α := A →ₗ[R] A) (↑((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) u) : A →ₗ[R] A) (LinearMap.mulLeft R (↑u : A))

Tactic:
rfl

Premises used: LinearMap.mulLeft, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
u : Aˣ
⊢ LinearEquiv.toEquiv (modM := inst_2) (modM₂ := inst_2) ((mulLeftLinearEquiv R A : (a : Aˣ) → A ≃ₗ[R] A) u) = u.mulLeft

Tactic:
rfl

Premises used: LinearEquiv.toEquiv, Units.mulLeft, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : Aˣ
x : A
⊢ (mulRightLinearEquiv R a : (a : A) → A) x = x * (↑a : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : Aˣ
x : A
⊢ (LinearEquiv.symm (mulRightLinearEquiv R a) : (a : A) → A) x = x * (↑a⁻¹ : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a : Aˣ
⊢ Eq (α := A ≃ₗ[R] A) (LinearEquiv.symm (mulRightLinearEquiv R a)) (mulRightLinearEquiv R a⁻¹)

Tactic:
rfl

Premises used: Units.mulRightLinearEquiv, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : Aˣ
h :
  ∀ (x : A),
    Eq (α := A) ((mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b : (a : A) → A) x : A)
      ((mulRightLinearEquiv R (a * b) : (a : A) → A) x : A)
⊢ Eq (α := A ≃ₗ[R] A) (mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b) (mulRightLinearEquiv R (a * b))

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
a b : Aˣ
x : A
⊢ Eq (α := A) ((mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b : (a : A) → A) x : A)
    ((mulRightLinearEquiv R (a * b) : (a : A) → A) x : A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
u v : Aˣ
x : A
⊢ Eq (α := A) ((mulRightLinearEquiv R (u * v) : (a : A) → A) x : A)
    ((mulRightLinearEquiv R v : (a : A) → A) ((mulRightLinearEquiv R u : (a : A) → A) x : A) : A)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
u : Aˣ
⊢ Eq (α := A →ₗ[R] A) (↑(mulRightLinearEquiv R u) : A →ₗ[R] A) (LinearMap.mulRight R (↑u : A))

Tactic:
rfl

Premises used: LinearMap.mulRight, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_9
A : Type u_10
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : IsScalarTower R A A
u : Aˣ
⊢ LinearEquiv.toEquiv (modM := inst_2) (mulRightLinearEquiv R u) = u.mulRight

Tactic:
rfl

Premises used: Units.mulRight, LinearEquiv.toEquiv, rfl
-- 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 : 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
F : Type u_14
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : Module R M
inst_6 : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
inst_9 : EquivLike F M M₂
s : SemilinearEquivClass F σ M M₂
⊢ SemilinearMapClass F σ M M₂

Tactic:
{ s with }

Premises used: SemilinearMapClass.mk
-- 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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
⊢ Injective (α := M ≃ₛₗ[σ] M₂) toEquiv

Tactic:
fun ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ ⟨⟨⟨_, _⟩, _⟩, _, _, _⟩ h ↦
    (LinearEquiv.mk.injEq _ _ _ _ _ _ _ _).mpr
      ⟨LinearMap.ext (congr_fun (Equiv.mk.inj h).1), (Equiv.mk.inj h).2⟩

Premises used: Eq.mpr, _private.0.LinearEquiv.toEquiv_injective.match_2, Equiv.mk.inj, LinearEquiv.mk, LinearMap.ext, _private.0.LinearEquiv.toEquiv_injective.match_1, And.right, And.left, And.intro, LinearMap.mk, Function.Injective, AddHom.mk, congr_fun, Eq, LinearEquiv.mk.injEq
-- 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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
e₁ e₂ : M ≃ₛₗ[σ] M₂
⊢ e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

Tactic:
toEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearEquiv.toEquiv_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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
⊢ Injective (α := M ≃ₛₗ[σ] M₂) toLinearMap

Tactic:
fun _ _ H ↦ toEquiv_injective <| Equiv.ext <| LinearMap.congr_fun H

Premises used: Equiv.ext, LinearEquiv.toEquiv_injective, LinearMap.congr_fun, Function.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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
e₁ e₂ : M ≃ₛₗ[σ] M₂
⊢ (↑e₁ : M →ₛₗ[σ] M₂) = (↑e₂ : M →ₛₗ[σ] M₂) ↔ e₁ = e₂

Tactic:
toLinearMap_injective.eq_iff

Premises used: Function.Injective.eq_iff, LinearEquiv.toLinearMap_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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ (↑e : M →ₛₗ[σ] M₂) =
    (↑e : [inst_6 : FunLike (M ≃ₛₗ[σ] M₂) M M₂] → [SemilinearMapClass (M ≃ₛₗ[σ] M₂) σ M M₂] → M →ₛₗ[σ] M₂)

Tactic:
rfl

Premises used: SemilinearMapClass.semilinearMap, 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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] M₂
invFun : M₂ → M
left_inv : LeftInverse invFun f.toFun
right_inv : RightInverse invFun f.toFun
⊢ Eq (α := (a : M) → M₂)
    (⇑{ toLinearMap := f, invFun := invFun, left_inv := left_inv, right_inv := right_inv } : (a : M) → M₂)
    (⇑f : (a : M) → M₂)

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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
⊢ Injective (α := M ≃ₛₗ[σ] M₂) (β := M → M₂) (DFunLike.coe (β := fun (a : M) ↦ M₂))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_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₂
modM : Module R M
modM₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst_4 : RingHomInvPair σ σ'
inst_5 : RingHomInvPair σ' σ
F : Type u_14
inst_6 : EquivLike F M M₂
inst_7 : SemilinearEquivClass F σ M M₂
f : F
x : M
⊢ Eq.{u_9 + 1} (α := M₂) (((↑f : M ≃ₛₗ[σ] M₂) : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)

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₂
⊢ Eq (α := (a : M) → M₂) (⇑(↑e : M →ₛₗ[σ] M₂) : (a : M) → M₂) (⇑e : (a : M) → M₂)

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₂
⊢ Eq (α := (a : M) → M₂) (⇑e.toEquiv : (a : M) → M₂) (⇑e : (a : M) → M₂)

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₂
⊢ (↑e : M →ₛₗ[σ] M₂).toFun = (⇑e : (a : M) → M₂)

Tactic:
dsimp
-- 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 e' : M ≃ₛₗ[σ] M₂
h : ∀ (x : M), Eq.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e' : (a : M) → M₂) x : M₂)
⊢ e = e'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- 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 x' : M
⊢ x = x' → Eq.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) x' : M₂)

Tactic:
DFunLike.congr_arg e

Premises used: DFunLike.congr_arg
-- 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 e' : M ≃ₛₗ[σ] M₂
h : e = e'
x : M
⊢ Eq.{u_9 + 1} (α := M₂) ((e : (a : M) → M₂) x : M₂) ((e' : (a : M) → M₂) x : M₂)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- 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
x : M
⊢ (refl R M : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- 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 : 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
inst_2 : Semiring R₁
inst_3 : Semiring R₂
inst_4 : Semiring R₃
inst_5 : Semiring R₄
inst_6 : AddCommMonoid M
inst_7 : AddCommMonoid M₁
inst_8 : AddCommMonoid M₂
inst_9 : AddCommMonoid M₃
inst_10 : AddCommMonoid M₄
inst_11 : AddCommMonoid N₁
inst_12 : AddCommMonoid N₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e_1 e' e : M ≃ₛₗ[σ] M₂
r : S
x : M₂
rw rw₁ :
  HSMul.hSMul.{u_1, u_7, u_7} (α := R) (β := M) ((σ' : (a : S) → R) r : R)
      (((↑e : M →ₛₗ[σ] M₂).inverse e.invFun ⋯ ⋯ : (a : M₂) → M) x : M) =
    HSMul.hSMul.{u_1, u_7, u_7} (α := R) (β := M) ((σ' : (a : S) → R) r : R)
      (((↑e : M →ₛₗ[σ] M₂).inverse e.invFun ⋯ ⋯ : (a : M₂) → M) x : M)
⊢ ((↑e : M →ₛₗ[σ] M₂).inverse e.invFun ⋯ ⋯ : (a : M₂) → M) (r • x) =
    HSMul.hSMul.{u_1, u_7, u_7} (α := R) (β := M) ((σ' : (a : S) → R) r : R)
      (((↑e : M →ₛₗ[σ] M₂).inverse e.invFun ⋯ ⋯ : (a : M₂) → M) x : M)

Tactic:
rw [map_smulₛₗ]

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₂
⊢ e.invFun = (⇑e.symm : (a : M₂) → M)

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₂
⊢ e.toEquiv.symm = (↑e.symm : M₂ ≃ M)

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.toEquiv, 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₂
⊢ e.symm.toEquiv = e.toEquiv.symm

Tactic:
rfl

Premises used: Equiv.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₂
module_M : Module R M
module_S_M₂ : Module S M₂
σ : R →+* S
σ' : S →+* R
re₁ : RingHomInvPair σ σ'
re₂ : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] M₂
⊢ Eq (α := (a : M₂) → M) (⇑e.toEquiv.symm : (a : M₂) → M) (⇑e.symm : (a : M₂) → M)

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₂
⊢ e.toAddEquiv = (↑e : M ≃+ M₂)

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, EquivLike.toEquiv, 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₂
x : M
⊢ Eq.{u_9 + 1} (α := M₂) (((↑e : M ≃+ M₂) : (a : M) → M₂) x : M₂) ((e : (a : M) → M₂) x : M₂)

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₂
⊢ (↑e : M →ₛₗ[σ] M₂).toAddMonoidHom = e.toAddEquiv.toAddMonoidHom

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, AddEquiv.toAddMonoidHom, 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 σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ Eq (α := M₂ ≃+ M₁) (↑e₁₂.symm : M₂ ≃+ M₁) (AddEquiv.symm (↑e₁₂ : M₁ ≃+ M₂))

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, Equiv.symm, EquivLike.toEquiv, rfl, AddEquiv.symm
-- 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 σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
c : M₁
⊢ Eq.{u_10 + 1} (α := M₃) ((e₁₂.trans e₂₃ : (a : M₁) → M₃) c : M₃)
    ((e₂₃ : (a : M₂) → M₃) ((e₁₂ : (a : M₁) → M₂) c : M₂) : M₃)

Tactic:
rfl

Premises used: rfl
-- 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 σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ (↑(e₁₂.trans e₂₃) : M₁ →ₛₗ[σ₁₃] M₃) = (↑e₂₃ : M₂ →ₛₗ[σ₂₃] M₃) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂)

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₂
c : M₂
⊢ (e : (a : M) → M₂) ((e.symm : (a : M₂) → M) c : M) = c

Tactic:
e.right_inv c

Premises used: LinearEquiv.right_inv