awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (⇑(symm (LinearEquiv.curry R M V V₂)) : (a : V → V₂ → M) → V × V₂ → M) uncurry

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
h₁ : f ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f = LinearMap.id
x : M
⊢ Eq.{u_7 + 1} (α := M₂) ((ofLinear f g h₁ h₂ : (a : M) → M₂) x : M₂) ((f : (a : M) → M₂) x : M₂)

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
h₁ : f ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f = LinearMap.id
x : M₂
⊢ Eq.{u_5 + 1} (α := M) ((symm (ofLinear f g h₁ h₂) : (a : M₂) → M) x : M) ((g : (a : M₂) → M) x : M)

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
h₁ : f ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f = LinearMap.id
⊢ (↑(ofLinear f g h₁ h₂) : M →ₛₗ[σ₁₂] M₂) = f

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₂
module_M : Module R M
module_M₂ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₁] M
h₁ : f ∘ₛₗ g = LinearMap.id
h₂ : g ∘ₛₗ f = LinearMap.id
⊢ (↑(symm (ofLinear f g h₁ h₂)) : M₂ →ₛₗ[σ₂₁] M) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := (a : M) → M) (⇑(neg R) : (a : M) → M) (-id)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
x : M
⊢ (neg R : (a : M) → M) x = -x

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{u_5 + 1} (α := M ≃ₗ[R] M) (symm (neg R)) (neg R)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.neg, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
h :
  ∀ (x : M₁),
    Eq.{u_15 + 1} (α := M₁')
      (((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂))
              ((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)) f) :
            (a : M₁) → M₁')
          x :
        M₁')
      ((f : (a : M₁) → M₁') x : M₁')
⊢ (fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂))
      ((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)) f) =
    f

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
x : M₁
⊢ Eq.{u_15 + 1} (α := M₁')
    (((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂))
            ((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)) f) :
          (a : M₁) → M₁')
        x :
      M₁')
    ((f : (a : M₁) → M₁') x : M₁')

Tactic:
simp only [symm_apply_apply, Function.comp_apply, coe_comp, coe_coe]

Premises used: LinearEquiv.symm_apply_apply, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
h :
  ∀ (x : M₂),
    Eq.{u_16 + 1} (α := M₂')
      (((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁))
              ((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂)) f) :
            (a : M₂) → M₂')
          x :
        M₂')
      ((f : (a : M₂) → M₂') x : M₂')
⊢ (fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁))
      ((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂)) f) =
    f

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
x : M₂
⊢ Eq.{u_16 + 1} (α := M₂')
    (((fun (f : M₁ →ₛₗ[σ₁₁'] M₁') ↦ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁))
            ((fun (f : M₂ →ₛₗ[σ₂₂'] M₂') ↦ ((↑e₂.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e₁ : M₁ →ₛₗ[σ₁₂] M₂)) f) :
          (a : M₂) → M₂')
        x :
      M₂')
    ((f : (a : M₂) → M₂') x : M₂')

Tactic:
simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]

Premises used: LinearMap.coe_comp, LinearEquiv.apply_symm_apply, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f g : M₁ →ₛₗ[σ₁₁'] M₁'
h :
  ∀ (x : M₂),
    Eq.{u_16 + 1} (α := M₂')
      ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ (f + g)) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₂') x : M₂')
      ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) +
              ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ g) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) :
            (a : M₂) → M₂')
          x :
        M₂')
⊢ ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ (f + g)) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) =
    ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) +
      ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ g) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁)

Tactic:
ext x
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f g : M₁ →ₛₗ[σ₁₁'] M₁'
x : M₂
⊢ Eq.{u_16 + 1} (α := M₂')
    ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ (f + g)) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) : (a : M₂) → M₂') x : M₂')
    ((((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) +
            ((↑e₂ : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ g) ∘ₛₗ (↑e₁.symm : M₂ →ₛₗ[σ₂₁] M₁) :
          (a : M₂) → M₂')
        x :
      M₂')

Tactic:
simp only [map_add, add_apply, Function.comp_apply, coe_comp, coe_coe]

Premises used: LinearMap.add_apply, map_add, LinearMap.coe_comp, Function.comp_apply, LinearEquiv.coe_coe
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e : M₁ ≃ₛₗ[σ₁₂] M₂
x x_1 : Module.End R₁ M₁
h :
  ∀ (x_2 : M₂),
    Eq (α := M₂) (((e.arrowCongrAddEquiv e).toFun (x * x_1) : (a : M₂) → M₂) x_2 : M₂)
      (((e.arrowCongrAddEquiv e).toFun x * (e.arrowCongrAddEquiv e).toFun x_1 : (a : M₂) → M₂) x_2 : M₂)
⊢ (e.arrowCongrAddEquiv e).toFun (x * x_1) = (e.arrowCongrAddEquiv e).toFun x * (e.arrowCongrAddEquiv e).toFun x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e : M₁ ≃ₛₗ[σ₁₂] M₂
x x_1 : Module.End R₁ M₁
x_2 : M₂
⊢ Eq (α := M₂) (((e.arrowCongrAddEquiv e).toFun (x * x_1) : (a : M₂) → M₂) x_2 : M₂)
    (((e.arrowCongrAddEquiv e).toFun x * (e.arrowCongrAddEquiv e).toFun x_1 : (a : M₂) → M₂) x_2 : M₂)

Tactic:
simp [arrowCongrAddEquiv]

Premises used: LinearEquiv.arrowCongrAddEquiv
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_20 : Semiring S
inst_21 : Module S M₁
inst_22 : SMulCommClass R₁ S M₁
inst_23 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
x : S
x_1 : M₁ →ₛₗ[σ₁₁'] M₁'
h :
  ∀ (x_2 : M₁),
    Eq.{u_16 + 1} (α := M₂')
      ((Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂))
              (HSMul.hSMul (α := Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) x_1) :
            (a : M₁) → M₂')
          x_2 :
        M₂')
      ((HSMul.hSMul (α := Sᵈᵐᵃ)
              ((RingHom.id Sᵈᵐᵃ : (a : Sᵈᵐᵃ) → Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) : Sᵈᵐᵃ)
              (Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂)) x_1) :
            (a : M₁) → M₂')
          x_2 :
        M₂')
⊢ Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂))
      (HSMul.hSMul (α := Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) x_1) =
    HSMul.hSMul (α := Sᵈᵐᵃ) ((RingHom.id Sᵈᵐᵃ : (a : Sᵈᵐᵃ) → Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) : Sᵈᵐᵃ)
      (Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂)) x_1)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
R₂_1 : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁_1 : Type u_6
M₂_1 : Type u_7
M₃ : Type u_8
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₁'
inst_3 : Semiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_20 : Semiring S
inst_21 : Module S M₁
inst_22 : SMulCommClass R₁ S M₁
inst_23 : RingHomCompTriple σ₁₂' σ₂'₁' σ₁₁'
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
x : S
x_1 : M₁ →ₛₗ[σ₁₁'] M₁'
x_2 : M₁
⊢ Eq.{u_16 + 1} (α := M₂')
    ((Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂))
            (HSMul.hSMul (α := Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) x_1) :
          (a : M₁) → M₂')
        x_2 :
      M₂')
    ((HSMul.hSMul (α := Sᵈᵐᵃ) ((RingHom.id Sᵈᵐᵃ : (a : Sᵈᵐᵃ) → Sᵈᵐᵃ) ((DomMulAct.mk : (a : S) → Sᵈᵐᵃ) x : Sᵈᵐᵃ) : Sᵈᵐᵃ)
            (Equiv.toFun (AddEquiv.toEquiv (arrowCongrAddEquiv (refl R₁ M₁) e₂)) x_1) :
          (a : M₁) → M₂')
        x_2 :
      M₂')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : CommSemiring R₁'
inst_3 : CommSemiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₁ →ₛₗ[σ₁₁'] M₁'
x : M₂
⊢ Eq.{u_21 + 1} (α := M₂')
    ((((e₁.arrowCongr e₂ : (a : M₁ →ₛₗ[σ₁₁'] M₁') → M₂ →ₛₗ[σ₂₂'] M₂') f : M₂ →ₛₗ[σ₂₂'] M₂') : (a : M₂) → M₂') x : M₂')
    ((e₂ : (a : M₁') → M₂') ((f : (a : M₁) → M₁') ((e₁.symm : (a : M₂) → M₁) x : M₁) : M₁') : M₂')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : CommSemiring R₁'
inst_3 : CommSemiring R₂'
inst_4 : AddCommMonoid M₁
inst_5 : AddCommMonoid M₂
inst_6 : AddCommMonoid M₁'
inst_7 : AddCommMonoid M₂'
inst_8 : Module R₁ M₁
inst_9 : Module R₂ M₂
inst_10 : Module R₁' M₁'
inst_11 : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst_12 : RingHomInvPair σ₁₂ σ₂₁
inst_13 : RingHomInvPair σ₂₁ σ₁₂
inst_14 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_15 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_16 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_17 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_18 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_19 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
x : M₁
⊢ Eq.{u_20 + 1} (α := M₁')
    (((((e₁.arrowCongr e₂).symm : (a : M₂ →ₛₗ[σ₂₂'] M₂') → M₁ →ₛₗ[σ₁₁'] M₁') f : M₁ →ₛₗ[σ₁₁'] M₁') : (a : M₁) → M₁') x :
      M₁')
    ((e₂.symm : (a : M₂') → M₁') ((f : (a : M₂) → M₂') ((e₁ : (a : M₁) → M₂) x : M₂) : M₂') : M₁')

Tactic:
rfl

Premises used: rfl