awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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₁'
⊢ 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)
have 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₂')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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₁''
⊢ 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₂'')
have 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₂'')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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₂')
      ((e.symm.conj : (a : Module.End R₂' M₂') → Module.End R₁' M₁') f) =
    f
have 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₂')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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₁')
      ((e.conj : (a : Module.End R₁' M₁') → Module.End R₂' M₂') f) =
    f
have 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₁')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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₂'
⊢ 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₂')
have 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₂')
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have rw₂ : (funLeft R M _root_.id : (a : m → M) → m → M) x i = x i
Tactic: rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have rw₃ : x i = x i
Tactic: rw [id_apply, ← funLeft_comp, Equiv.symm_comp_self, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have 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
Tactic: rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have rw₂ : (funLeft R M _root_.id : (a : n → M) → n → M) x i = x i
Tactic: rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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)
have rw₃ : x i = x i
Tactic: rw [id_apply, ← funLeft_comp, Equiv.self_comp_symm, LinearMap.funLeft_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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
⊢ 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
have 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' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
            right_inv := sorry } :
          (a : A) → A)
        x :
      A)
    ((1 : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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ˣ
⊢ (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 })
have 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' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
            right_inv := sorry } :
          (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' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
              right_inv := sorry : 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' := sorry, map_smul' := sorry, invFun := __spread.0.invFun, left_inv := sorry,
              right_inv := sorry : A ≃ₗ[R] A }) :
          (a : A) → A)
        x_2 :
      A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Basic (goal)
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ˣ
⊢ Eq (α := A ≃ₗ[R] A) (mulRightLinearEquiv R a ≪≫ₗ mulRightLinearEquiv R b) (mulRightLinearEquiv R (a * b))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₂
⊢ ((↑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)
have rw : HSMul.hSMul.{u_1, u_7, u_7} (α := R) (β := M) ((σ' : (a : S) → R) r : R)
    (((↑e : M →ₛₗ[σ] M₂).inverse e.invFun sorry sorry : (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 sorry sorry : (a : M₂) → M) x : M)
Tactic: rw [map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₂] M₂
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f = f
have h : ∀ (x : M₃),
  Eq.{u_9 + 1} (α := M₂) (((↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ f : (a : M₃) → M₂) x : M₂)
    ((f : (a : M₃) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
f : M₃ →ₛₗ[σ₃₁] M₁
inst_7 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
⊢ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f = f
have h : ∀ (x : M₃),
  Eq.{u_8 + 1} (α := M₁) (((↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) ∘ₛₗ f : (a : M₃) → M₁) x : M₁)
    ((f : (a : M₃) → M₁) x : M₁)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ↔ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
have mp : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) → f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
mp : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) → f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
⊢ f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁) ↔ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
have mpr : f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g → f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
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₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ (↑e₁₂.symm : M₂ →ₛₗ[σ₂₁] M₁)
⊢ f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) = g
have mp : ∀ (x : M₁),
  Eq.{u_10 + 1} (α := M₃) ((f ∘ₛₗ (↑e₁₂ : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₃) x : M₃) ((g : (a : M₁) → M₃) x : M₃)
Tactic: ext