awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 1) 1

Tactic:
baseChange_id

Premises used: LinearMap.baseChange_id
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ baseChange A (f * g) = HMul.hMul (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A f) (baseChange A g)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 : Module.End R M
n : ℕ
⊢ baseChange A (f ^ n) = HPow.hPow (α := A ⊗[R] M →ₗ[A] A ⊗[R] M) (baseChange A f) n

Tactic:
map_pow (Module.End.baseChangeHom _ _ _) f n

Premises used: LinearMap.baseChange, Module.End.baseChangeHom, map_pow, TensorProduct.AlgebraTensorModule.map, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
f : M ≃ₗ[R] N
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (↑(LinearEquiv.baseChange R A M N f) : A ⊗[R] M →ₗ[A] A ⊗[R] N)
    (baseChange A (↑f : M →ₗ[R] N))

Tactic:
rfl

Premises used: LinearMap.baseChange, TensorProduct.AlgebraTensorModule.map, rfl, TensorProduct.AlgebraTensorModule.lift
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
a : A
m : M
⊢ Eq (α := A ⊗[R] N) ((LinearEquiv.baseChange R A M N e : (a : A ⊗[R] M) → A ⊗[R] N) (a ⊗ₜ[R] m) : A ⊗[R] N)
    (a ⊗ₜ[R] (e : (a : M) → N) m : A ⊗[R] N)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
a : A
n : N
⊢ Eq (α := A ⊗[R] M)
    ((LinearEquiv.symm (LinearEquiv.baseChange R A M N e) : (a : A ⊗[R] N) → A ⊗[R] M) (a ⊗ₜ[R] n) : A ⊗[R] M)
    (a ⊗ₜ[R] (e.symm : (a : N) → M) n : A ⊗[R] M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ Eq (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M 1) 1

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp [← LinearEquiv.coe_toLinearMap]

Premises used: LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ 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)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp only [← LinearEquiv.coe_toLinearMap, LinearEquiv.coe_baseChange, LinearEquiv.trans_apply,
    LinearEquiv.coe_trans, baseChange_eq_ltensor, lTensor_comp_apply]

Premises used: LinearMap.baseChange_eq_ltensor, LinearEquiv.coe_baseChange, LinearEquiv.trans_apply, LinearMap.lTensor_comp_apply, LinearEquiv.coe_toLinearMap, LinearEquiv.coe_trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
e f : M ≃ₗ[R] M
⊢ LinearEquiv.baseChange R A M M (e * f) =
    HMul.hMul (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M e) (LinearEquiv.baseChange R A M M f)

Tactic:
simp [LinearEquiv.mul_eq_trans, LinearEquiv.baseChange_trans]

Premises used: LinearEquiv.mul_eq_trans, LinearEquiv.baseChange_trans
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ 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))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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
⊢ 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:
rw [LinearEquiv.eq_symm_apply]

Premises used: LinearEquiv.eq_symm_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
⊢ (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:
simp [← LinearEquiv.coe_toLinearMap, LinearEquiv.coe_baseChange,
    baseChange_eq_ltensor, ← lTensor_comp_apply]

Premises used: LinearMap.baseChange_eq_ltensor, LinearEquiv.coe_baseChange, LinearMap.lTensor_comp_apply, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
e : M ≃ₗ[R] M
⊢ Eq (α := A ⊗[R] M ≃ₗ[A] A ⊗[R] M) (LinearEquiv.baseChange R A M M e⁻¹) (LinearEquiv.baseChange R A M M e)⁻¹

Tactic:
LinearEquiv.baseChange_symm R A M M e

Premises used: LinearEquiv.baseChange_symm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 : ℕ
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:
simp [pow_succ, LinearEquiv.baseChange_mul, h]

Premises used: pow_succ, LinearEquiv.baseChange_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 (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)
⊢ 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

Tactic:
induction n with
  | zero => simp
  | succ n h =>
    simp [pow_succ, LinearEquiv.baseChange_mul, h]

Premises used: pow_succ, LinearEquiv.baseChange_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 : ℕ
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:
simp only [zpow_add_one, LinearEquiv.baseChange_mul, h]

Premises used: zpow_add_one, LinearEquiv.baseChange_mul
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 : ℕ
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:
simp only [zpow_sub_one, LinearEquiv.baseChange_mul, h, LinearEquiv.baseChange_inv]

Premises used: zpow_sub_one, LinearEquiv.baseChange_mul, LinearEquiv.baseChange_inv
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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)
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)
⊢ 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

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]

Premises used: zpow_sub_one, zpow_add_one, LinearEquiv.baseChange_mul, LinearEquiv.baseChange_inv
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Semiring B
inst_4 : Algebra R B
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
φ : A →ₐ[R] B
t : A ⊗[R] M
f : M →ₗ[R] N
⊢ Eq (α := B ⊗[R] N)
    ((rTensor N φ.toLinearMap : (a : A ⊗[R] N) → B ⊗[R] N) ((baseChange A f : (a : A ⊗[R] M) → A ⊗[R] N) t) : B ⊗[R] N)
    ((baseChange B f : (a : B ⊗[R] M) → B ⊗[R] N) ((rTensor M φ.toLinearMap : (a : A ⊗[R] M) → B ⊗[R] M) t) : B ⊗[R] N)

Tactic:
simp [LinearMap.baseChange_eq_ltensor, ← LinearMap.comp_apply]

Premises used: LinearMap.baseChange_eq_ltensor, LinearMap.comp_apply
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ baseChange A (f - g) = HSub.hSub (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A f) (baseChange A g)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp [tmul_sub]

Premises used: TensorProduct.tmul_sub
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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)
⊢ Eq (α := A ⊗[R] M →ₗ[A] A ⊗[R] N) (baseChange A (-f)) (-baseChange A f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
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:
simp [tmul_neg]

Premises used: TensorProduct.tmul_neg
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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
a : A
m : M
hm : m ∈ p
⊢ Membership.mem (γ := Submodule A (A ⊗[R] M)) (baseChange A p) (a ⊗ₜ[R] m)

Tactic:
⟨a ⊗ₜ[R] ⟨m, hm⟩, rfl⟩

Premises used: Set.Mem, setOf, Subtype.mk, Exists.intro, TensorProduct.tmul, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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))
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
⊢ 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 ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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 :
  {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))
⊢ 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:
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]

Premises used: TensorProduct.span_tmul_eq_top, eq_top_iff, Submodule.span_eq_top_of_span_eq_top, LinearMap.range_le_iff_comap, Submodule.baseChange, Submodule.span_le
-- Module: Mathlib.LinearAlgebra.TensorProduct.Tower
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))

Tactic:
fun _ ⟨a, m, h⟩ ↦ ?_

Premises used: LinearMap.baseChange, Membership.mem, Set.Subset, _private.0.Submodule.baseChange_eq_span.match_2, SetLike.coe, Submodule.comap, Submodule.span, Submodule.subtype, Submodule.map, OfNat.ofNat, DFunLike.coe, TensorProduct.mk