awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₂)} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S)
      (((LinearMap.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg :
  ∀ (x : M),
    Eq (α := ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      ((g : (a : N) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ((f : (a : M) → N) x) : ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) :
            (a : S ⊗[R] M) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
          (((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x) :
        ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
refine_3 : Function.Bijective (α := S ⊗[R] M) (β := N) (⇑f' : (a : S ⊗[R] M) → N)
refine_1 : f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g = LinearMap.id
⊢ Function.Bijective (α := S ⊗[R] M) (β := N) (⇑f' : (a : S ⊗[R] M) → N)
have refine_2 : ((↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g) ∘ₗ f'' = LinearMap.id
Tactic: let fe : S ⊗[R] M ≃ₗ[S] N :=
    LinearEquiv.ofLinear f'' (ULift.moduleEquiv.toLinearMap.comp g) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
    [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q),
    ∃! g' : N →ₗ[S] Q,
      (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) v₃)} →
                    [inst : Semiring R] →
                      [inst_13 : Semiring S] →
                        [inst_14 : AddCommMonoid M] →
                          [inst_15 : AddCommMonoid M₂] →
                            [inst_16 : Module R M] →
                              [inst_17 : Module R M₂] →
                                [inst_18 : Module S M] →
                                  [inst_19 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          f =
        g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N :=
  TensorProduct.lift
    ((↑R :
        {S M : Type v₃} →
          {M₂ : Type (max v₁ v₂)} →
            [inst : Semiring R] →
              [inst_9 : Semiring S] →
                [inst_10 : AddCommMonoid M] →
                  [inst_11 : AddCommMonoid M₂] →
                    [inst_12 : Module R M] →
                      [inst_13 : Module R M₂] →
                        [inst_14 : Module S M] →
                          [inst_15 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (S := S)
      (((LinearMap.flip (AlgHom.toLinearMap (Algebra.ofId S (Module.End S (M →ₗ[R] N)))) :
            (M →ₗ[R] N) →ₗ[S] S →ₗ[S] M →ₗ[R] N) :
          (a : M →ₗ[R] N) → S →ₗ[S] M →ₗ[R] N)
        f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg :
  ∀ (x : M),
    Eq (α := ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      ((g : (a : N) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) ((f : (a : M) → N) x) : ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
      (((↑(LinearEquiv.symm ULift.moduleEquiv) : S ⊗[R] M →ₗ[R] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)) :
            (a : S ⊗[R] M) → ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
          (((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1 : (a : M) → S ⊗[R] M) x) :
        ULift.{v₂, max v₁ v₃} (S ⊗[R] M))
⊢ f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g = LinearMap.id
have refine_1 : (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[S] ULift.{max v₁ v₃, v₂} N) ∘ₗ
    f'' ∘ₗ (↑ULift.moduleEquiv : ULift.{v₂, max v₁ v₃} (S ⊗[R] M) →ₗ[S] S ⊗[R] M) ∘ₗ g =
  (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[S] ULift.{max v₁ v₃, v₂} N) ∘ₗ LinearMap.id
Tactic: rw [← LinearMap.cancel_left (ULift.moduleEquiv : ULift.{max v₁ v₃} N ≃ₗ[S] N).symm.injective]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ IsBaseChange R (↑e : M →ₗ[R] N)
have h : ∀ (Q : Type (max v₁ v₂ u_1)) [inst_5 : AddCommMonoid Q] [inst_6 : Module R Q] [inst_7 : Module R Q]
  [inst_8 : IsScalarTower R R Q] (g : M →ₗ[R] Q),
  ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g
Tactic: apply IsBaseChange.of_lift_unique
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
⊢ I₂ = I₃
have smul : ∀ (r : R) (q : Q), SMul.smul r q = SMul.smul r q
Tactic: ext r q
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ SMul.smul r q = SMul.smul r q
have smul : Eq (α := Q)
  (let x := I₂;
  r • q)
  (let x := I₃;
  r • q)
Tactic: change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ r • q = r • q
have smul : r • HSMul.hSMul (α := R) 1 q = r • HSMul.hSMul (α := R) 1 q
Tactic: rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
smul : r • HSMul.hSMul (α := R) 1 q = r • HSMul.hSMul (α := R) 1 q
⊢ r • q = r • q
have smul₁ : r • HSMul.hSMul (α := R) 1 q = (r * 1) • q
Tactic: rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
smul : r • HSMul.hSMul (α := R) 1 q = r • HSMul.hSMul (α := R) 1 q
smul₁ : r • HSMul.hSMul (α := R) 1 q = (r * 1) • q
⊢ r • q = r • q
have smul₂ : HSMul.hSMul (β := R) r 1 • q = (r * 1) • q
Tactic: rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
smul : r • HSMul.hSMul (α := R) 1 q = r • HSMul.hSMul (α := R) 1 q
smul₁ : r • HSMul.hSMul (α := R) 1 q = (r * 1) • q
smul₂ : HSMul.hSMul (β := R) r 1 • q = (r * 1) • q
⊢ r • q = r • q
have smul₃ : (r * 1) • q = (r * 1) • q
Tactic: rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (hypothesis)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
⊢ ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g
have this : I₂ = I₃
Tactic: have : I₂ = I₃ := by
    ext r q
    change (by let _ := I₂; exact r • q) = (by let _ := I₃; exact r • q)
    dsimp
    rw [← one_smul R q, smul_smul, ← @smul_assoc _ _ _ (id _) (id _) (id _) I₄, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
this : I₂ = I₃
⊢ ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g
have h : ∀ [I₄ : IsScalarTower R R Q],
  ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g
Tactic: cases this
Cleared hypotheses: I₃, I₄, this
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
⊢ (fun (g' : N →ₗ[R] Q) ↦
      (↑R :
              {S : Type u_1} →
                {M : Type v₂} →
                  {M₂ : Type (max (max v₁ v₂) u_1)} →
                    [inst : Semiring R] →
                      [inst_5 : Semiring S] →
                        [inst_6 : AddCommMonoid M] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R M] →
                              [inst_9 : Module R M₂] →
                                [inst_10 : Module S M] →
                                  [inst_11 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g' ∘ₗ
          (↑e : M →ₗ[R] N) =
        g)
    (g ∘ₗ (↑e.symm : N →ₗ[R] M))
have h : ∀ (x : M),
  Eq (α := Q)
    (((↑R :
                {S : Type u_1} →
                  {M : Type v₂} →
                    {M₂ : Type (max (max v₁ v₂) u_1)} →
                      [inst : Semiring R] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module R M] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (g ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ
            (↑e : M →ₗ[R] N) :
          (a : M) → Q)
        x :
      Q)
    ((g : (a : M) → Q) x : Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
g : M →ₗ[R] Q
I₄ : IsScalarTower R R Q
⊢ ∃! g' : N →ₗ[R] Q,
    (↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑e : M →ₗ[R] N) =
      g
have h : ∀ (y : N →ₗ[R] Q),
  (fun (g' : N →ₗ[R] Q) ↦
        (↑R :
                {S : Type u_1} →
                  {M : Type v₂} →
                    {M₂ : Type (max (max v₁ v₂) u_1)} →
                      [inst : Semiring R] →
                        [inst_5 : Semiring S] →
                          [inst_6 : AddCommMonoid M] →
                            [inst_7 : AddCommMonoid M₂] →
                              [inst_8 : Module R M] →
                                [inst_9 : Module R M₂] →
                                  [inst_10 : Module S M] →
                                    [inst_11 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              g' ∘ₗ
            (↑e : M →ₗ[R] N) =
          g)
      y →
    y = g ∘ₗ (↑e.symm : N →ₗ[R] M)
Tactic: refine
    ⟨g.comp e.symm.toLinearMap, by
      ext
      simp, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : Module R M
inst_4 : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ : Module R Q
I₄ : IsScalarTower R R Q
y : N →ₗ[R] Q
⊢ y =
    ((↑R :
            {S : Type u_1} →
              {M : Type v₂} →
                {M₂ : Type (max (max v₁ v₂) u_1)} →
                  [inst : Semiring R] →
                    [inst_5 : Semiring S] →
                      [inst_6 : AddCommMonoid M] →
                        [inst_7 : AddCommMonoid M₂] →
                          [inst_8 : Module R M] →
                            [inst_9 : Module R M₂] →
                              [inst_10 : Module S M] →
                                [inst_11 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          y ∘ₗ
        (↑e : M →ₗ[R] N)) ∘ₗ
      (↑e.symm : N →ₗ[R] M)
have h : ∀ (x : N),
  Eq (α := Q) ((y : (a : N) → Q) x : Q)
    ((((↑R :
                  {S : Type u_1} →
                    {M : Type v₂} →
                      {M₂ : Type (max (max v₁ v₂) u_1)} →
                        [inst : Semiring R] →
                          [inst_5 : Semiring S] →
                            [inst_6 : AddCommMonoid M] →
                              [inst_7 : AddCommMonoid M₂] →
                                [inst_8 : Module R M] →
                                  [inst_9 : Module R M₂] →
                                    [inst_10 : Module S M] →
                                      [inst_11 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                y ∘ₗ
              (↑e : M →ₗ[R] N)) ∘ₗ
            (↑e.symm : N →ₗ[R] M) :
          (a : N) → Q)
        x :
      Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
⊢ IsBaseChange T
    ((↑R :
          {S : Type v₃} →
            {M : Type v₂} →
              {M₂ : Type u_5} →
                [inst : Semiring R] →
                  [inst_20 : Semiring S] →
                    [inst_21 : AddCommMonoid M] →
                      [inst_22 : AddCommMonoid M₂] →
                        [inst_23 : Module R M] →
                          [inst_24 : Module R M₂] →
                            [inst_25 : Module S M] →
                              [inst_26 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        g ∘ₗ
      f)
have h : ∀ (Q : Type (max v₁ u_5 u_4)) [inst_20 : AddCommMonoid Q] [inst_21 : Module R Q] [inst_22 : Module T Q]
  [inst_23 : IsScalarTower R T Q] (g_1 : M →ₗ[R] Q),
  ∃! g' : O →ₗ[T] Q,
    (↑R :
            {S : Type u_4} →
              {M : Type u_5} →
                {M₂ : Type (max (max v₁ u_5) u_4)} →
                  [inst : Semiring R] →
                    [inst_24 : Semiring S] →
                      [inst_25 : AddCommMonoid M] →
                        [inst_26 : AddCommMonoid M₂] →
                          [inst_27 : Module R M] →
                            [inst_28 : Module R M₂] →
                              [inst_29 : Module S M] →
                                [inst_30 : Module S M₂] →
                                  [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          g' ∘ₗ
        (↑R :
              {S : Type v₃} →
                {M : Type v₂} →
                  {M₂ : Type u_5} →
                    [inst : Semiring R] →
                      [inst_24 : Semiring S] →
                        [inst_25 : AddCommMonoid M] →
                          [inst_26 : AddCommMonoid M₂] →
                            [inst_27 : Module R M] →
                              [inst_28 : Module R M₂] →
                                [inst_29 : Module S M] →
                                  [inst_30 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            g ∘ₗ
          f =
      g_1
Tactic: apply IsBaseChange.of_lift_unique
-- Lean 4 proof step from Mathlib.RingTheory.IsTensorProduct (goal)
Goal:
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst : AddCommMonoid M
inst_1 : AddCommMonoid N
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S N
inst_8 : IsScalarTower R S N
T : Type u_4
O : Type u_5
inst_9 : CommSemiring T
inst_10 : Algebra R T
inst_11 : Algebra S T
inst_12 : IsScalarTower R S T
inst_13 : AddCommMonoid O
inst_14 : Module R O
inst_15 : Module S O
inst_16 : Module T O
inst_17 : IsScalarTower S T O
inst_18 : IsScalarTower R S O
inst_19 : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
g : N →ₗ[S] O
hg : IsBaseChange T g
Q : Type (max v₁ u_5 u_4)
inst_20 : AddCommMonoid Q
inst_21 : Module R Q
inst_22 : Module T Q
inst_23 : IsScalarTower R T Q
i : M →ₗ[R] Q
this : Module S Q := Module.compHom Q (algebraMap S T)
x : S
y : T
z : Q
⊢ (x • y) • z = x • y • z
have rw : HSMul.hSMul (α := T) ((algebraMap S T : (a : S) → T) x : T) (y • z) = x • y • z
Tactic: rw [Algebra.smul_def, mul_smul]