awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : CommSemiring R₁'
inst_3 : CommSemiring R₂'
inst_4 : CommSemiring R₁''
inst_5 : CommSemiring R₂''
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid M₁'
inst_9 : AddCommMonoid M₂'
inst_10 : AddCommMonoid M₁''
inst_11 : AddCommMonoid M₂''
inst_12 : Module R₁ M₁
inst_13 : Module R₂ M₂
inst_14 : Module R₁' M₁'
inst_15 : Module R₂' M₂'
inst_16 : Module R₁'' M₁''
inst_17 : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst_18 : RingHomInvPair σ₁₂ σ₂₁
inst_19 : RingHomInvPair σ₂₁ σ₁₂
inst_20 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_21 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_22 : RingHomInvPair σ₁''₂'' σ₂''₁''
inst_23 : RingHomInvPair σ₂''₁'' σ₁''₂''
inst_24 : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst_25 : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst_26 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_27 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_28 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_29 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_30 : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst_31 : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst_32 : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst_33 : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst_34 : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst_35 : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst_36 : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst_37 : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
h :
  ∀ (x : M₂),
    Eq.{u_24 + 1} (α := M₂'')
      ((((e₁.arrowCongr e₃ : (a : M₁ →ₛₗ[σ₁₁''] M₁'') → M₂ →ₛₗ[σ₂₂''] M₂'') (g ∘ₛₗ f) : M₂ →ₛₗ[σ₂₂''] M₂'') :
            (a : M₂) → M₂'')
          x :
        M₂'')
      ((LinearMap.comp.{u_10, u_13, u_16, u_18, u_21, u_24} (R₂ := R₂') (M₂ := M₂') (module_M₂ := inst_15) (σ₁₂ := σ₂₂')
              (σ₂₃ := σ₂'₂'') ((e₂.arrowCongr e₃ : (a : M₁' →ₛₗ[σ₁'₁''] M₁'') → M₂' →ₛₗ[σ₂'₂''] M₂'') g)
              ((e₁.arrowCongr e₂ : (a : M₁ →ₛₗ[σ₁₁'] M₁') → M₂ →ₛₗ[σ₂₂'] M₂') f) :
            (a : M₂) → M₂'')
          x :
        M₂'')
⊢ Eq (α := M₂ →ₛₗ[σ₂₂''] M₂'')
    ((e₁.arrowCongr e₃ : (a : M₁ →ₛₗ[σ₁₁''] M₁'') → M₂ →ₛₗ[σ₂₂''] M₂'') (g ∘ₛₗ f) : M₂ →ₛₗ[σ₂₂''] M₂'')
    (LinearMap.comp.{u_10, u_13, u_16, u_18, u_21, u_24} (R₂ := R₂') (M₂ := M₂') (module_M₂ := inst_15) (σ₁₂ := σ₂₂')
        (σ₂₃ := σ₂'₂'') ((e₂.arrowCongr e₃ : (a : M₁' →ₛₗ[σ₁'₁''] M₁'') → M₂' →ₛₗ[σ₂'₂''] M₂'') g)
        ((e₁.arrowCongr e₂ : (a : M₁ →ₛₗ[σ₁₁'] M₁') → M₂ →ₛₗ[σ₂₂'] M₂') f) :
      M₂ →ₛₗ[σ₂₂''] M₂'')

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_12
R₂' : Type u_13
R₁'' : Type u_15
R₂'' : Type u_16
M₁ : Type u_17
M₂ : Type u_18
M₁' : Type u_20
M₂' : Type u_21
M₁'' : Type u_23
M₂'' : Type u_24
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : CommSemiring R₁'
inst_3 : CommSemiring R₂'
inst_4 : CommSemiring R₁''
inst_5 : CommSemiring R₂''
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid M₁'
inst_9 : AddCommMonoid M₂'
inst_10 : AddCommMonoid M₁''
inst_11 : AddCommMonoid M₂''
inst_12 : Module R₁ M₁
inst_13 : Module R₂ M₂
inst_14 : Module R₁' M₁'
inst_15 : Module R₂' M₂'
inst_16 : Module R₁'' M₁''
inst_17 : Module R₂'' M₂''
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁''₂'' : R₁'' →+* R₂''
σ₂''₁'' : R₂'' →+* R₁''
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₁'₁'' : R₁' →+* R₁''
σ₂'₂'' : R₂' →+* R₂''
σ₁₁'' : R₁ →+* R₁''
σ₂₂'' : R₂ →+* R₂''
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₂'₁'' : R₂' →+* R₁''
σ₁'₂'' : R₁' →+* R₂''
σ₂₁'' : R₂ →+* R₁''
σ₁₂'' : R₁ →+* R₂''
inst_18 : RingHomInvPair σ₁₂ σ₂₁
inst_19 : RingHomInvPair σ₂₁ σ₁₂
inst_20 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_21 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_22 : RingHomInvPair σ₁''₂'' σ₂''₁''
inst_23 : RingHomInvPair σ₂''₁'' σ₁''₂''
inst_24 : RingHomCompTriple σ₁₁' σ₁'₁'' σ₁₁''
inst_25 : RingHomCompTriple σ₂₂' σ₂'₂'' σ₂₂''
inst_26 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_27 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_28 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_29 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_30 : RingHomCompTriple σ₁₁'' σ₁''₂'' σ₁₂''
inst_31 : RingHomCompTriple σ₂₁ σ₁₂'' σ₂₂''
inst_32 : RingHomCompTriple σ₂₂'' σ₂''₁'' σ₂₁''
inst_33 : RingHomCompTriple σ₁₂ σ₂₁'' σ₁₁''
inst_34 : RingHomCompTriple σ₁'₁'' σ₁''₂'' σ₁'₂''
inst_35 : RingHomCompTriple σ₂'₁' σ₁'₂'' σ₂'₂''
inst_36 : RingHomCompTriple σ₂'₂'' σ₂''₁'' σ₂'₁''
inst_37 : RingHomCompTriple σ₁'₂' σ₂'₁'' σ₁'₁''
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₃ : M₁'' ≃ₛₗ[σ₁''₂''] M₂''
f : M₁ →ₛₗ[σ₁₁'] M₁'
g : M₁' →ₛₗ[σ₁'₁''] M₁''
x : M₂
⊢ Eq.{u_24 + 1} (α := M₂'')
    ((((e₁.arrowCongr e₃ : (a : M₁ →ₛₗ[σ₁₁''] M₁'') → M₂ →ₛₗ[σ₂₂''] M₂'') (g ∘ₛₗ f) : M₂ →ₛₗ[σ₂₂''] M₂'') :
          (a : M₂) → M₂'')
        x :
      M₂'')
    ((LinearMap.comp.{u_10, u_13, u_16, u_18, u_21, u_24} (R₂ := R₂') (M₂ := M₂') (module_M₂ := inst_15) (σ₁₂ := σ₂₂')
            (σ₂₃ := σ₂'₂'') ((e₂.arrowCongr e₃ : (a : M₁' →ₛₗ[σ₁'₁''] M₁'') → M₂' →ₛₗ[σ₂'₂''] M₂'') g)
            ((e₁.arrowCongr e₂ : (a : M₁ →ₛₗ[σ₁₁'] M₁') → M₂ →ₛₗ[σ₂₂'] M₂') f) :
          (a : M₂) → M₂'')
        x :
      M₂'')

Tactic:
simp only [symm_apply_apply, arrowCongr_apply, LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, LinearEquiv.symm_apply_apply, LinearEquiv.arrowCongr_apply
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁ : Type u_9
R₂ : Type u_10
R₃ : Type u_11
R₁' : Type u_12
R₂' : Type u_13
R₃' : Type u_14
M₁ : Type u_17
M₂ : Type u_18
M₃ : Type u_19
M₁' : Type u_20
M₂' : Type u_21
M₃' : Type u_22
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : CommSemiring R₁'
inst_4 : CommSemiring R₂'
inst_5 : CommSemiring R₃'
inst_6 : AddCommMonoid M₁
inst_7 : AddCommMonoid M₂
inst_8 : AddCommMonoid M₃
inst_9 : AddCommMonoid M₁'
inst_10 : AddCommMonoid M₂'
inst_11 : AddCommMonoid M₃'
inst_12 : Module R₁ M₁
inst_13 : Module R₂ M₂
inst_14 : Module R₃ M₃
inst_15 : Module R₁' M₁'
inst_16 : Module R₂' M₂'
inst_17 : Module R₃' M₃'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₂'₃' : R₂' →+* R₃'
σ₃'₂' : R₃' →+* R₂'
σ₁'₃' : R₁' →+* R₃'
σ₃'₁' : R₃' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₃₃' : R₃ →+* R₃'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
σ₃₂' : R₃ →+* R₂'
σ₂₃' : R₂ →+* R₃'
σ₃₁' : R₃ →+* R₁'
σ₁₃' : R₁ →+* R₃'
inst_18 : RingHomInvPair σ₁₂ σ₂₁
inst_19 : RingHomInvPair σ₂₁ σ₁₂
inst_20 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_21 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_22 : RingHomInvPair σ₂₃ σ₃₂
inst_23 : RingHomInvPair σ₃₂ σ₂₃
inst_24 : RingHomInvPair σ₂'₃' σ₃'₂'
inst_25 : RingHomInvPair σ₃'₂' σ₂'₃'
inst_26 : RingHomInvPair σ₁₃ σ₃₁
inst_27 : RingHomInvPair σ₃₁ σ₁₃
inst_28 : RingHomInvPair σ₁'₃' σ₃'₁'
inst_29 : RingHomInvPair σ₃'₁' σ₁'₃'
inst_30 : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst_31 : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst_32 : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst_33 : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
inst_34 : RingHomCompTriple σ₁₁' σ₁'₃' σ₁₃'
inst_35 : RingHomCompTriple σ₃₁ σ₁₃' σ₃₃'
inst_36 : RingHomCompTriple σ₃₃' σ₃'₁' σ₃₁'
inst_37 : RingHomCompTriple σ₁₃ σ₃₁' σ₁₁'
inst_38 : RingHomCompTriple σ₂₂' σ₂'₃' σ₂₃'
inst_39 : RingHomCompTriple σ₃₂ σ₂₃' σ₃₃'
inst_40 : RingHomCompTriple σ₃₃' σ₃'₂' σ₃₂'
inst_41 : RingHomCompTriple σ₂₃ σ₃₂' σ₂₂'
inst_42 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_43 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst_44 : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'
inst_45 : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₁' : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₂ : M₂ ≃ₛₗ[σ₂₃] M₃
e₂' : M₂' ≃ₛₗ[σ₂'₃'] M₃'
⊢ Eq (α := (M₁ →ₛₗ[σ₁₁'] M₁') ≃ₛₗ[σ₁'₃'] M₃ →ₛₗ[σ₃₃'] M₃') ((e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂'))
    (arrowCongr (e₁.trans e₂) (e₁'.trans e₂'))

Tactic:
rfl

Premises used: LinearEquiv.arrowCongr, LinearEquiv.trans, rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₁' M₁'
⊢ (e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f =
    ((↑e : M₁' →ₛₗ[σ₁'₂'] M₂') ∘ₛₗ f) ∘ₛₗ (↑e.symm : M₂' →ₛₗ[σ₂'₁'] M₁')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₁' M₁'
x : M₂'
⊢ Eq (α := M₂')
    ((((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f : Module.End R₂' 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_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₂' M₂'
⊢ (e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁') f =
    ((↑e.symm : M₂' →ₛₗ[σ₂'₁'] M₁') ∘ₛₗ f) ∘ₛₗ (↑e : M₁' →ₛₗ[σ₁'₂'] M₂')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f g : Module.End R₁' M₁'
⊢ Eq.{u_21 + 1} (α := Module.End R₂' M₂')
    ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') (g ∘ₗ f) : Module.End R₂' M₂')
    ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') g ∘ₗ
        (e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f :
      M₂' →ₗ[R₂'] M₂')

Tactic:
arrowCongr_comp e e e f g

Premises used: LinearEquiv.arrowCongr_comp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
R₃' : Type u_14
M₁' : Type u_20
M₂' : Type u_21
M₃' : Type u_22
inst : CommSemiring R₁'
inst_1 : CommSemiring R₂'
inst_2 : CommSemiring R₃'
inst_3 : AddCommMonoid M₁'
inst_4 : AddCommMonoid M₂'
inst_5 : AddCommMonoid M₃'
inst_6 : Module R₁' M₁'
inst_7 : Module R₂' M₂'
inst_8 : Module R₃' M₃'
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₂'₃' : R₂' →+* R₃'
σ₃'₂' : R₃' →+* R₂'
σ₁'₃' : R₁' →+* R₃'
σ₃'₁' : R₃' →+* R₁'
inst_9 : RingHomInvPair σ₁'₂' σ₂'₁'
inst_10 : RingHomInvPair σ₂'₁' σ₁'₂'
inst_11 : RingHomInvPair σ₂'₃' σ₃'₂'
inst_12 : RingHomInvPair σ₃'₂' σ₂'₃'
inst_13 : RingHomInvPair σ₁'₃' σ₃'₁'
inst_14 : RingHomInvPair σ₃'₁' σ₁'₃'
inst_15 : RingHomCompTriple σ₁'₂' σ₂'₃' σ₁'₃'
inst_16 : RingHomCompTriple σ₃'₂' σ₂'₁' σ₃'₁'
e₁ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
e₂ : M₂' ≃ₛₗ[σ₂'₃'] M₃'
⊢ Eq (α := LinearEquiv.{u_12, u_14, u_20, u_22} σ₁'₃' (Module.End R₁' M₁') (Module.End R₃' M₃')) (e₁.conj.trans e₂.conj)
    (conj (e₁.trans e₂))

Tactic:
rfl

Premises used: LinearEquiv.arrowCongr, LinearEquiv.trans, rfl, LinearEquiv.conj
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₂' M₂'
h :
  ∀ (x : M₂'),
    Eq (α := M₂')
      ((((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂')
                ((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁') f) :
              Module.End R₂' M₂') :
            (a : M₂') → M₂')
          x :
        M₂')
      ((f : (a : M₂') → M₂') x : M₂')
⊢ (e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂')
      ((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁') f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₂' M₂'
x : M₂'
⊢ Eq (α := M₂')
    ((((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂')
              ((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁') f) :
            Module.End R₂' M₂') :
          (a : M₂') → M₂')
        x :
      M₂')
    ((f : (a : M₂') → M₂') x : M₂')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₁' M₁'
h :
  ∀ (x : M₁'),
    Eq (α := M₁')
      ((((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁')
                ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f) :
              Module.End R₁' M₁') :
            (a : M₁') → M₁')
          x :
        M₁')
      ((f : (a : M₁') → M₁') x : M₁')
⊢ (e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁')
      ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f) =
    f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : Module.End R₁' M₁'
x : M₁'
⊢ Eq (α := M₁')
    ((((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁')
              ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f) :
            Module.End R₁' M₁') :
          (a : M₁') → M₁')
        x :
      M₁')
    ((f : (a : M₁') → M₁') x : M₁')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
h :
  ∀ (x : M₂'),
    Eq (α := M₂')
      ((((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') LinearMap.id : Module.End R₂' M₂') : (a : M₂') → M₂')
          x :
        M₂')
      ((LinearMap.id : (a : M₂') → M₂') x : M₂')
⊢ Eq.{u_21 + 1} (α := Module.End R₂' M₂')
    ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') LinearMap.id : Module.End R₂' M₂')
    (LinearMap.id : M₂' →ₗ[R₂'] M₂')

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R₁' : Type u_12
R₂' : Type u_13
M₁' : Type u_20
M₂' : Type u_21
inst : CommSemiring R₁'
inst_1 : CommSemiring 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 σ₂'₁' σ₁'₂'
e : M₁' ≃ₛₗ[σ₁'₂'] M₂'
x : M₂'
⊢ Eq (α := M₂')
    ((((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') LinearMap.id : Module.End R₂' M₂') : (a : M₂') → M₂')
        x :
      M₂')
    ((LinearMap.id : (a : M₂') → M₂') x : M₂')

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Equiv.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : Module.End R M
⊢ (conj (refl R M) : (a : Module.End R M) → Module.End R M) f = f

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 : AddCommMonoid M
inst_2 : Module R M
m : Type u_9
n : Type u_10
f : m → n
g : n → M
i : m
⊢ (funLeft R M f : (a : n → M) → m → M) g i = g (f i)

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 : AddCommMonoid M
inst_2 : Module R M
n : Type u_10
g : n → M
⊢ (funLeft R M _root_.id : (a : n → M) → n → M) g = 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 : AddCommMonoid M
inst_2 : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
f₁ : n → p
f₂ : m → n
⊢ Eq (α := (p → M) →ₗ[R] m → M) (funLeft R M (f₁ ∘ f₂)) (funLeft R M f₂ ∘ₗ funLeft R M f₁)

Tactic:
rfl

Premises used: LinearMap.funLeft, rfl
-- 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
m : Type u_9
n : Type u_10
f : m → n
hf : Injective f
⊢ Surjective (α := n → M) (β := m → M) (⇑(funLeft R M f) : (a : n → M) → m → M)

Tactic:
hf.surjective_comp_right

Premises used: Function.Injective.surjective_comp_right
-- 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
m : Type u_9
n : Type u_10
f : m → n
hf : Surjective f
⊢ Injective (α := n → M) (β := m → M) (⇑(funLeft R M f) : (a : n → M) → m → M)

Tactic:
hf.injective_comp_right

Premises used: Function.Surjective.injective_comp_right
-- 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 : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : m → M
i : m
rw : (funLeft R M (⇑e : (a : m) → n) ∘ₗ funLeft R M (⇑e.symm : (a : n) → m) : (a : m → M) → m → M) x i = x i
rw₁ :
  (funLeft R M (Function.comp.{u_9 + 1, u_10 + 1, u_9 + 1} (β := n) (⇑e.symm : (a : n) → m) (⇑e : (a : m) → n)) :
        (a : m → M) → m → M)
      x i =
    x i
rw₂ : (funLeft R M _root_.id : (a : m → M) → m → M) x i = x i
rw₃ rw₄ : x i = x i
⊢ Eq.{u_5 + 1} (α := M)
    ((funLeft R M (⇑e : (a : m) → n) ∘ₗ funLeft R M (⇑e.symm : (a : n) → m) : (a : m → M) → m → M) x i : M)
    ((LinearMap.id : (a : m → M) → m → M) x i : M)

Tactic:
rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]

Premises used: LinearMap.funLeft_id, Equiv.symm_comp_self, LinearMap.id_apply, LinearMap.funLeft_comp
-- 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 : Module R M
m : Type u_9
n : Type u_10
p : Type u_11
e : m ≃ n
x : n → M
i : n
rw : (funLeft R M (⇑e.symm : (a : n) → m) ∘ₗ funLeft R M (⇑e : (a : m) → n) : (a : n → M) → n → M) x i = x i
rw₁ :
  (funLeft R M (Function.comp.{u_10 + 1, u_9 + 1, u_10 + 1} (β := m) (⇑e : (a : m) → n) (⇑e.symm : (a : n) → m)) :
        (a : n → M) → n → M)
      x i =
    x i
rw₂ : (funLeft R M _root_.id : (a : n → M) → n → M) x i = x i
rw₃ rw₄ : x i = x i
⊢ Eq.{u_5 + 1} (α := M)
    ((funLeft R M (⇑e.symm : (a : n) → m) ∘ₗ funLeft R M (⇑e : (a : m) → n) : (a : n → M) → n → M) x i : M)
    ((LinearMap.id : (a : n → M) → n → M) x i : M)

Tactic:
rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]

Premises used: LinearMap.funLeft_id, LinearMap.id_apply, LinearMap.funLeft_comp, Equiv.self_comp_symm
-- 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
m : Type u_9
n : Type u_10
e : m ≃ n
x : n → M
⊢ Eq (α := m → M) ((funCongrLeft R M e : (a : n → M) → m → M) x : m → M)
    ((funLeft R M (⇑e : (a : m) → n) : (a : n → M) → m → M) x : m → M)

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 : AddCommMonoid M
inst_2 : Module R M
n : Type u_10
⊢ Eq (α := (n → M) ≃ₗ[R] n → M) (funCongrLeft R M (Equiv.refl n)) (refl R (n → M))

Tactic:
rfl

Premises used: LinearEquiv.funCongrLeft, LinearMap.funLeft, LinearEquiv.refl, rfl
-- 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
m : Type u_9
n : Type u_10
p : Type u_11
e₁ : m ≃ n
e₂ : n ≃ p
⊢ Eq (α := (p → M) ≃ₗ[R] m → M) (funCongrLeft R M (e₁.trans e₂)) (funCongrLeft R M e₂ ≪≫ₗ funCongrLeft R M e₁)

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, LinearEquiv.funCongrLeft, LinearMap.funLeft, LinearEquiv.trans, rfl
-- 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
m : Type u_9
n : Type u_10
e : m ≃ n
⊢ Eq (α := (m → M) ≃ₗ[R] n → M) (symm (funCongrLeft R M e)) (funCongrLeft R M e.symm)

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearEquiv.ofLinear, LinearEquiv.funCongrLeft, LinearMap.funLeft, rfl
-- 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
h :
  ∀ (x : A),
    Eq (α := A)
      ((let __spread.0 : Equiv.Perm A := mulLeft 1;
            let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑1 : A);
            { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
              right_inv := ⋯ } :
            (a : A) → A)
          x :
        A)
      ((1 : (a : A) → A) x : A)
⊢ Eq.{u_10 + 1} (α := A ≃ₗ[R] A)
    (let __spread.0 : Equiv.Perm A := mulLeft 1;
    let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑1 : A);
    { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
      right_inv := ⋯ })
    1

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 : A
⊢ Eq (α := A)
    ((let __spread.0 : Equiv.Perm A := mulLeft 1;
          let __spread.1 : A →ₗ[R] A := LinearMap.mulLeft R (↑1 : A);
          { toFun := __spread.0.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __spread.0.invFun, left_inv := ⋯,
            right_inv := ⋯ } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)

Tactic:
simp