awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
r : R
f : M →ₗ[R] N
⊢ baseChange A (r • f) = HSMul.hSMul (β := A ⊗[R] M →ₗ[A] A ⊗[R] N) r (baseChange A f)
have a : ∀ (x : M),
  Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A (r • f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry (HSMul.hSMul (β := A ⊗[R] M →ₗ[A] A ⊗[R] N) r (baseChange A f)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
              (a : A) → M →ₗ[R] A ⊗[R] N)
            1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A id) id
have a : ∀ (x : M),
  Eq (α := A ⊗[R] M)
    ((((AlgebraTensorModule.curry (baseChange A id) : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 :
          (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((((AlgebraTensorModule.curry id : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 : (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] P) (baseChange A (g ∘ₗ f)) (baseChange A g ∘ₗ baseChange A f)
have a : ∀ (x : M),
  Eq (α := A ⊗[R] P)
    ((((AlgebraTensorModule.curry (baseChange A (g ∘ₗ f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) : (a : A) → M →ₗ[R] A ⊗[R] P) 1 :
          (a : M) → A ⊗[R] P)
        x :
      A ⊗[R] P)
    ((((AlgebraTensorModule.curry (baseChange A g ∘ₗ baseChange A f) : A →ₗ[A] M →ₗ[R] A ⊗[R] P) :
              (a : A) → M →ₗ[R] A ⊗[R] P)
            1 :
          (a : M) → A ⊗[R] P)
        x :
      A ⊗[R] P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
A : Type u_7
B : Type u_8
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Algebra A B
inst_10 : IsScalarTower R A B
f : M →ₗ[R] N
⊢ Eq (α := B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[A] (A ⊗[R] N)) (baseChange B (baseChange A f))
    (((↑(LinearEquiv.symm (cancelBaseChange R A B B N)) : B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) :
        B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) ∘ₗ
      (baseChange B f ∘ₗ (↑(cancelBaseChange R A B B M) : B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] M) :
        B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] N))
have a : ∀ (x : M),
  Eq (α := B ⊗[A] (A ⊗[R] N))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry (baseChange B (baseChange A f)) :
                        B →ₗ[B] A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N)) :
                      (a : B) → A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N))
                    1) :
                A →ₗ[A] M →ₗ[R] B ⊗[A] (A ⊗[R] N)) :
              (a : A) → M →ₗ[R] B ⊗[A] (A ⊗[R] N))
            1 :
          (a : M) → B ⊗[A] (A ⊗[R] N))
        x :
      B ⊗[A] (A ⊗[R] N))
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                          (((↑(LinearEquiv.symm (cancelBaseChange R A B B N)) : B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) :
                              B ⊗[R] N →ₗ[B] B ⊗[A] (A ⊗[R] N)) ∘ₗ
                            (baseChange B f ∘ₗ (↑(cancelBaseChange R A B B M) : B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] M) :
                              B ⊗[A] (A ⊗[R] M) →ₗ[B] B ⊗[R] N)) :
                        B →ₗ[B] A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N)) :
                      (a : B) → A ⊗[R] M →ₗ[A] B ⊗[A] (A ⊗[R] N))
                    1) :
                A →ₗ[A] M →ₗ[R] B ⊗[A] (A ⊗[R] N)) :
              (a : A) → M →ₗ[R] B ⊗[A] (A ⊗[R] N))
            1 :
          (a : M) → B ⊗[A] (A ⊗[R] N))
        x :
      B ⊗[A] (A ⊗[R] N))
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f g : Module.End R M
⊢ baseChange A (f * g) = HMul.hMul (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A f) (baseChange A g)
have a : ∀ (x : M),
  Eq (α := A ⊗[R] M)
    ((((AlgebraTensorModule.curry (baseChange A (f * g)) : A →ₗ[A] M →ₗ[R] A ⊗[R] M) : (a : A) → M →ₗ[R] A ⊗[R] M) 1 :
          (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
    ((((AlgebraTensorModule.curry (HMul.hMul (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A f) (baseChange A g)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] M) :
              (a : A) → M →ₗ[R] A ⊗[R] M)
            1 :
          (a : M) → A ⊗[R] M)
        x :
      A ⊗[R] M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ Eq (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M 1) 1
have h : ∀ (x : A ⊗[R] M),
  Eq (α := A ⊗[R] M) ((LinearEquiv.baseChange R A M M 1 : (a : A ⊗[R] M) → A ⊗[R] M) x : A ⊗[R] M)
    ((1 : (a : A ⊗[R] M) → A ⊗[R] M) x : A ⊗[R] M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
P : Type u_6
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : AddCommMonoid P
inst_6 : Module R M
inst_7 : Module R N
inst_8 : Module R P
e : M ≃ₗ[R] N
f : N ≃ₗ[R] P
⊢ Eq (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] P) (LinearEquiv.baseChange R A M P (e ≪≫ₗ f))
    (LinearEquiv.baseChange R A M N e ≪≫ₗ LinearEquiv.baseChange R A N P f)
have h : ∀ (x : A ⊗[R] M),
  Eq (α := A ⊗[R] P) ((LinearEquiv.baseChange R A M P (e ≪≫ₗ f) : (a : A ⊗[R] M) → A ⊗[R] P) x : A ⊗[R] P)
    ((LinearEquiv.baseChange R A M N e ≪≫ₗ LinearEquiv.baseChange R A N P f : (a : A ⊗[R] M) → A ⊗[R] P) x : A ⊗[R] P)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
e : M ≃ₗ[R] N
⊢ Eq (α := A ⊗[R] N ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A N M e.symm)
    (LinearEquiv.symm (LinearEquiv.baseChange R A M N e))
have h : ∀ (x : A ⊗[R] N),
  Eq (α := A ⊗[R] M) ((LinearEquiv.baseChange R A N M e.symm : (a : A ⊗[R] N) → A ⊗[R] M) x : A ⊗[R] M)
    ((LinearEquiv.symm (LinearEquiv.baseChange R A M N e) : (a : A ⊗[R] N) → A ⊗[R] M) x : A ⊗[R] M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid N
inst_5 : Module R M
inst_6 : Module R N
e : M ≃ₗ[R] N
x : A ⊗[R] N
⊢ Eq (α := A ⊗[R] M) ((LinearEquiv.baseChange R A N M e.symm : (a : A ⊗[R] N) → A ⊗[R] M) x : A ⊗[R] M)
    ((LinearEquiv.symm (LinearEquiv.baseChange R A M N e) : (a : A ⊗[R] N) → A ⊗[R] M) x : A ⊗[R] M)
have h : (LinearEquiv.baseChange R A M N e : (a : A ⊗[R] M) → A ⊗[R] N)
    ((LinearEquiv.baseChange R A N M e.symm : (a : A ⊗[R] N) → A ⊗[R] M) x) =
  x
Tactic: rw [LinearEquiv.eq_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f : M ≃ₗ[R] M
n : ℕ
⊢ LinearEquiv.baseChange R A M M (f ^ n) = HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n
have zero : LinearEquiv.baseChange R A M M (HPow.hPow (β := ℕ) f 0) =
  HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℕ) (LinearEquiv.baseChange R A M M f) 0
Tactic: induction n with
  | zero => simp
  | succ n h =>
    simp [pow_succ, LinearEquiv.baseChange_mul, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f : M ≃ₗ[R] M
n : ℕ
zero :
  LinearEquiv.baseChange R A M M (HPow.hPow (β := ℕ) f 0) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℕ) (LinearEquiv.baseChange R A M M f) 0
⊢ LinearEquiv.baseChange R A M M (f ^ n) = HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n
have succ : ∀ (n : ℕ)
  (h :
    LinearEquiv.baseChange R A M M (f ^ n) =
      HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n),
  LinearEquiv.baseChange R A M M (f ^ (n + 1)) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n h =>
    simp [pow_succ, LinearEquiv.baseChange_mul, h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f : M ≃ₗ[R] M
n : ℤ
⊢ LinearEquiv.baseChange R A M M (f ^ n) = HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n
have zero : LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f 0) =
  HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) 0
Tactic: induction n with
  | zero => simp
  | succ n h =>
    simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]
  | pred n h =>
    simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f : M ≃ₗ[R] M
n : ℤ
zero :
  LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f 0) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) 0
⊢ LinearEquiv.baseChange R A M M (f ^ n) = HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n
have succ : ∀ (n : ℕ)
  (h :
    LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f (↑n : ℤ)) =
      HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) (↑n : ℤ)),
  LinearEquiv.baseChange R A M M (f ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: induction n with
  | zero => simp
  | succ n h =>
    simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]
  | pred n h =>
    simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
f : M ≃ₗ[R] M
n : ℤ
zero :
  LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f 0) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) 0
succ :
  ∀ (n : ℕ)
    (h :
      LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f (↑n : ℤ)) =
        HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) (↑n : ℤ)),
    LinearEquiv.baseChange R A M M (f ^ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) =
      HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
⊢ LinearEquiv.baseChange R A M M (f ^ n) = HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) n
have pred : ∀ (n : ℕ)
  (h :
    LinearEquiv.baseChange R A M M (HPow.hPow (β := ℤ) f (-(↑n : ℤ))) =
      HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (β := ℤ) (LinearEquiv.baseChange R A M M f) (-(↑n : ℤ))),
  LinearEquiv.baseChange R A M M (f ^ HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1) =
    HPow.hPow (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M f) (HSub.hSub (α := ℤ) (-(↑n : ℤ)) 1)
Tactic: induction n with
  | zero => simp
  | succ n h =>
    simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]
  | pred n h =>
    simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
f g : M →ₗ[R] N
⊢ baseChange A (f - g) = HSub.hSub (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)
have a : ∀ (x : M),
  Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A (f - g)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry (HSub.hSub (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)) :
                A →ₗ[A] M →ₗ[R] A ⊗[R] N) :
              (a : A) → M →ₗ[R] A ⊗[R] N)
            1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : Ring A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
f : M →ₗ[R] N
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A (-f)) (-baseChange A f)
have a : ∀ (x : M),
  Eq (α := A ⊗[R] N)
    ((((AlgebraTensorModule.curry (baseChange A (-f)) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
    ((((AlgebraTensorModule.curry (-baseChange A f) : A →ₗ[A] M →ₗ[R] A ⊗[R] N) : (a : A) → M →ₗ[R] A ⊗[R] N) 1 :
          (a : M) → A ⊗[R] N)
        x :
      A ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ baseChange A p =
    span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M))
have refine_1 : baseChange A p ≤
  span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
refine_1 :
  baseChange A p ≤
    span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M))
⊢ baseChange A p =
    span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M))
have refine_2 : span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)) ≤
  baseChange A p
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ baseChange A p ≤
    span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M))
have refine_1 : {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} ⊆
  (↑(comap (LinearMap.baseChange A p.subtype)
        (span A
          (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
            Set (A ⊗[R] M)))) :
    Set (A ⊗[R] ↥p))
Tactic: rw [baseChange, LinearMap.range_le_iff_comap, eq_top_iff,
      ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..), span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
⊢ {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} ⊆
    (↑(comap (LinearMap.baseChange A p.subtype)
          (span A
            (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
              Set (A ⊗[R] M)))) :
      Set (A ⊗[R] ↥p))
have refine_1 : ∀ (x : TensorProduct.{u_1, u_3, u_2} R A ↥p),
  Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
      {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x →
    ∀ (a : A) (m : ↥p) (h : a ⊗ₜ[R] m = x),
      x ∈
        (↑(comap (LinearMap.baseChange A p.subtype)
              (span A
                (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
                  Set (A ⊗[R] M)))) :
          Set (A ⊗[R] ↥p))
Tactic: refine fun _ ⟨a, m, h⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p : Submodule R M
x : TensorProduct.{u_1, u_3, u_2} R A ↥p
h_1 :
  Membership.mem (γ := Set (TensorProduct.{u_1, u_3, u_2} R A ↥p))
    {t : TensorProduct.{u_1, u_3, u_2} R A ↥p | ∃ (m : A) (n : ↥p), m ⊗ₜ[R] n = t} x
a : A
m : ↥p
h : a ⊗ₜ[R] m = x
⊢ x ∈
    (↑(comap (LinearMap.baseChange A p.subtype)
          (span A
            (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) :
              Set (A ⊗[R] M)))) :
      Set (A ⊗[R] ↥p))
have refine_1 : Membership.mem (γ := Submodule A (A ⊗[R] M))
  (span A (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) p) : Set (A ⊗[R] M)))
  (HSMul.hSMul (β := A ⊗[R] M) a (1 ⊗ₜ[R] (p.subtype : (a : ↥p) → M) m : A ⊗[R] M))
Tactic: rw [← h, SetLike.mem_coe, mem_comap, LinearMap.baseChange_tmul, ← mul_one a, ← smul_eq_mul,
      ← smul_tmul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A ⊤) ⊤
have rw : LE.le (α := Submodule A (A ⊗[R] M)) (span A {t : A ⊗[R] M | ∃ (m : A) (n : M), m ⊗ₜ[R] n = t}) (baseChange A ⊤)
Tactic: rw [eq_top_iff, ← span_eq_top_of_span_eq_top R A _ (span_tmul_eq_top R ..)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
p q : Submodule R M
h : p ≤ q
⊢ LE.le (α := Submodule A (A ⊗[R] M)) (baseChange A p) (baseChange A q)
have rw : LE.le (α := Submodule A (A ⊗[R] M))
  (LinearMap.range (M := TensorProduct.{u_1, u_3, u_2} R A ↥p)
      ((AlgebraTensorModule.map LinearMap.id q.subtype : TensorProduct.{u_1, u_3, u_2} R A ↥q →ₗ[A] A ⊗[R] M) ∘ₗ
          (AlgebraTensorModule.map LinearMap.id (inclusion h) :
            TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] TensorProduct.{u_1, u_3, u_2} R A ↥q) :
        TensorProduct.{u_1, u_3, u_2} R A ↥p →ₗ[A] A ⊗[R] M) :
    Submodule A (A ⊗[R] M))
  (baseChange A q : Submodule A (A ⊗[R] M))
Tactic: rw [baseChange, LinearMap.baseChange, ← subtype_comp_inclusion p q h,
    ← LinearMap.id_comp LinearMap.id, AlgebraTensorModule.map_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
s : Set M
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A (span R s))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
have rw : Eq (α := Submodule A (A ⊗[R] M))
  (span A
    (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (span R s)) :
      Set (A ⊗[R] M)))
  (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
Tactic: rw [baseChange_eq_span, map_span, span_span_of_tower]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
s : Set M
rw :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A
      (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (span R s)) :
        Set (A ⊗[R] M)))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A (span R s))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
have rw₁ : Eq (α := Submodule A (A ⊗[R] M))
  (span A
    (↑(span R ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s)) :
      Set (A ⊗[R] M)))
  (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
Tactic: rw [baseChange_eq_span, map_span, span_span_of_tower]
-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Tower (goal)
Goal:
R : Type u_1
M : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
s : Set M
rw :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A
      (↑(map (σ₁₂ := RingHom.id R) ((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) (span R s)) :
        Set (A ⊗[R] M)))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
rw₁ :
  Eq (α := Submodule A (A ⊗[R] M))
    (span A
      (↑(span R ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s)) :
        Set (A ⊗[R] M)))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
⊢ Eq (α := Submodule A (A ⊗[R] M)) (baseChange A (span R s))
    (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
have rw₂ : Eq (α := Submodule A (A ⊗[R] M))
  (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
  (span A ((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s))
Tactic: rw [baseChange_eq_span, map_span, span_span_of_tower]