awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
S₀ : Type u_1
inst_10 : CommSemiring S₀
inst_11 : Algebra R S₀
inst_12 : Algebra S₀ S
inst_13 : Module S₀ M₁'
inst_14 : IsScalarTower R S₀ M₁'
inst_15 : IsScalarTower S₀ S M₁'
x : M₁'
i : ι₂
x_1 : M₂ i
i_1 : ι₂
⊢ (((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.restrictScalars R
                              (LinearEquiv.restrictScalars S₀
                                (directSumRight R S M₁' M₂ :
                                  (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S]
                                    ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)))) :
                          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) :
                      M₁' →ₗ[R] (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
                    (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
                  x ∘ₗ
                lof R ι₂ M₂ i :
              (a : M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            x_1 :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i_1 =
    (((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.restrictScalars R
                              (directSumRight R S₀ M₁' M₂ :
                                (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S₀]
                                  ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))) :
                          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) :
                      M₁' →ₗ[R] (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
                    (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
                  x ∘ₗ
                lof R ι₂ M₂ i :
              (a : M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            x_1 :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i_1

Tactic:
simp [lof]

Premises used: DirectSum.lof
-- Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
ι₂ : Type v₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
⊢ Eq (α := (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (⇑(directSumRight R S M₁' M₂ :
          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
      (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
    (⇑(directSumRight R R M₁' M₂ :
          (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[R] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
      (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)

Tactic:
congr($(restrictScalar_directSumRight ..))

Premises used: congrArg, id, DFunLike.coe, TensorProduct.restrictScalar_directSumRight
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_4
inst_3 : CommSemiring A
inst_4 : Algebra R A
f : Dual R V
a : A
v : V
⊢ (((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f : Dual A (A ⊗[R] V)) : (a : A ⊗[R] V) → A) (a ⊗ₜ[R] v) =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((f : (a : V) → R) v : R) a

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_4
inst_3 : CommSemiring A
inst_4 : Algebra R A
B : Type u_5
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
f : Dual R V
a :
  ∀ (x : V),
    Eq.{u_5 + 1} (α := B)
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            ((baseChange B : (a : Dual A (A ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                              ((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f)) :
                          B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                        (a : B) → A ⊗[R] V →ₗ[A] B)
                      1) :
                  A →ₗ[A] V →ₗ[R] B) :
                (a : A) → V →ₗ[R] B)
              1 :
            (a : V) → B)
          x :
        B)
      ((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.curry
                            (((LinearEquiv.symm (congr (cancelBaseChange R A B B V)) :
                                  Dual B (B ⊗[R] V) ≃ₗ[B] Dual B (B ⊗[A] (A ⊗[R] V))) :
                                (a : Dual B (B ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                              ((baseChange B : (a : Dual R V) → Dual B (B ⊗[R] V)) f)) :
                          B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                        (a : B) → A ⊗[R] V →ₗ[A] B)
                      1) :
                  A →ₗ[A] V →ₗ[R] B) :
                (a : A) → V →ₗ[R] B)
              1 :
            (a : V) → B)
          x :
        B)
⊢ Eq (α := Dual B (B ⊗[A] (A ⊗[R] V)))
    ((baseChange B : (a : Dual A (A ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
        ((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
      Dual B (B ⊗[A] (A ⊗[R] V)))
    (((LinearEquiv.symm (congr (cancelBaseChange R A B B V)) : Dual B (B ⊗[R] V) ≃ₗ[B] Dual B (B ⊗[A] (A ⊗[R] V))) :
          (a : Dual B (B ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
        ((baseChange B : (a : Dual R V) → Dual B (B ⊗[R] V)) f) :
      Dual B (B ⊗[A] (A ⊗[R] V)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
A : Type u_4
inst_3 : CommSemiring A
inst_4 : Algebra R A
B : Type u_5
inst_5 : CommSemiring B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
f : Dual R V
x : V
⊢ Eq.{u_5 + 1} (α := B)
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                          ((baseChange B : (a : Dual A (A ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                            ((baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f)) :
                        B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                      (a : B) → A ⊗[R] V →ₗ[A] B)
                    1) :
                A →ₗ[A] V →ₗ[R] B) :
              (a : A) → V →ₗ[R] B)
            1 :
          (a : V) → B)
        x :
      B)
    ((((AlgebraTensorModule.curry
                  (((AlgebraTensorModule.curry
                          (((LinearEquiv.symm (congr (cancelBaseChange R A B B V)) :
                                Dual B (B ⊗[R] V) ≃ₗ[B] Dual B (B ⊗[A] (A ⊗[R] V))) :
                              (a : Dual B (B ⊗[R] V)) → Dual B (B ⊗[A] (A ⊗[R] V)))
                            ((baseChange B : (a : Dual R V) → Dual B (B ⊗[R] V)) f)) :
                        B →ₗ[B] A ⊗[R] V →ₗ[A] B) :
                      (a : B) → A ⊗[R] V →ₗ[A] B)
                    1) :
                A →ₗ[A] V →ₗ[R] B) :
              (a : A) → V →ₗ[R] B)
            1 :
          (a : V) → B)
        x :
      B)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
v : V
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W) : (a : W) → A) ((j : (a : V) → W) v : W) : A)
    ((algebraMap R A : (a : R) → A) ((f : (a : V) → R) v : R) : A)

Tactic:
simp [toDual, linearMapLeftRightHom_comp_apply]

Premises used: IsBaseChange.linearMapLeftRightHom_comp_apply, IsBaseChange.toDual
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
e :
  ∀ (x : V),
    Eq.{u_4 + 1} (α := A)
      ((((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W) : (a : W) → A) ((j : (a : V) → W) x : W) : A)
      ((((Dual.congr ibc.equiv : (a : Dual A (A ⊗[R] V)) → Dual A W)
                ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
              Dual A W) :
            (a : W) → A)
          ((j : (a : V) → W) x : W) :
        A)
⊢ Eq (α := Dual A W) ((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W)
    ((Dual.congr ibc.equiv : (a : Dual A (A ⊗[R] V)) → Dual A W)
        ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
      Dual A W)

Tactic:
apply ibc.algHom_ext

Premises used: IsBaseChange.algHom_ext
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
f : Dual R V
v : V
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDual : (a : Dual R V) → Dual A W) f : Dual A W) : (a : W) → A) ((j : (a : V) → W) v : W) : A)
    ((((Dual.congr ibc.equiv : (a : Dual A (A ⊗[R] V)) → Dual A W)
              ((Dual.baseChange A : (a : Dual R V) → Dual A (A ⊗[R] V)) f) :
            Dual A W) :
          (a : W) → A)
        ((j : (a : V) → W) v : W) :
      A)

Tactic:
simp [toDual_comp_apply, Algebra.algebraMap_eq_smul_one]

Premises used: IsBaseChange.toDual_comp_apply, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a b : A
⊢ (a + b) • ibc.toDual = a • ibc.toDual + b • ibc.toDual

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
r : R
a : A
⊢ (r • a) • ibc.toDual = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (a • ibc.toDual)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := A ⊗[R] Dual R V) a 0) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun (M := A ⊗[R] Dual R V)
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        0)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
x y : A ⊗[R] Dual R V
hx :
  AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (a • x) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        x)
hy :
  AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (a • y) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        y)
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (a • (x + y)) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        (x + y))

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a b : A
f : Dual R V
⊢ AddHom.toFun
      (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
        (TensorProduct.lift { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ }))
      (HSMul.hSMul (β := A ⊗[R] Dual R V) a (b ⊗ₜ[R] f)) =
    HSMul.hSMul (α := A) (β := Dual A W) ((RingHom.id A : (a : A) → A) a : A)
      (AddHom.toFun (M := A ⊗[R] Dual R V)
        (LinearMap.toAddHom (S := R) (σ := RingHom.id R)
          (TensorProduct.lift
            { toFun := fun (a : A) ↦ a • ibc.toDual, map_add' := ⋯, map_smul' := ⋯ : A →ₗ[R] Dual R V →ₗ[R] Dual A W }))
        (b ⊗ₜ[R] f))

Tactic:
simp [TensorProduct.smul_tmul', mul_smul]

Premises used: TensorProduct.smul_tmul', SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
a : A
f : Dual R V
v : V
⊢ (((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (a ⊗ₜ[R] f) : Dual A W) : (a : W) → A)
      ((j : (a : V) → W) v : W) =
    HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) ((f : (a : V) → R) v : R) : A)

Tactic:
simp [toDualBaseChangeAux, toDual_comp_apply]

Premises used: IsBaseChange.toDual_comp_apply, _private.0.IsBaseChange.toDualBaseChangeAux
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
apply :
  Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
⊢ A ⊗[R] Dual R V ≃ₗ[A] Dual A W

Tactic:
apply LinearEquiv.ofBijective ibc.toDualBaseChangeAux

Premises used: _private.0.IsBaseChange.toDualBaseChangeAux, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
b : Basis (Free.ChooseBasisIndex R V) R V := Free.chooseBasis R V
set :
  let ι := Free.ChooseBasisIndex R V;
  ∀ (b : Basis ι R V),
    Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
      (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)
⊢ Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)

Tactic:
set ι := Free.ChooseBasisIndex R V

Premises used: Module.Free.ChooseBasisIndex
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
⊢ IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)

Tactic:
have ibc_pow : IsBaseChange A ((Algebra.linearMap R A).compLeft ι) := (linearMap R A).finitePow ι
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
suffices :
  ibc.toDualBaseChangeAux =
    (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ ibc_pow.equiv ≪≫ₗ
          (basis b ibc).constr A) :
      A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A)
⊢ Function.Bijective (α := A ⊗[R] Dual R V) (β := Dual A W)
    (⇑ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W)

Tactic:
suffices ibc.toDualBaseChangeAux =
      (((b.constr R).symm.baseChange ..).trans ibc_pow.equiv).trans ((ibc.basis b).constr A) from
    this ▸ LinearEquiv.bijective _
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
a :
  ∀ (f : Dual R V) (w : W),
    Eq.{u_4 + 1} (α := A)
      ((((((AlgebraTensorModule.curry ibc.toDualBaseChangeAux : A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                      (a : A) → Dual R V →ₗ[R] Dual A W)
                    1 :
                  (a : Dual R V) → Dual A W)
                f :
              Dual A W) :
            (a : W) → A)
          w :
        A)
      ((((((AlgebraTensorModule.curry
                          (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ
                                  ibc_pow.equiv ≪≫ₗ
                                (basis b ibc).constr A) :
                            A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A) :
                        A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                      (a : A) → Dual R V →ₗ[R] Dual A W)
                    1 :
                  (a : Dual R V) → Dual A W)
                f :
              Dual A W) :
            (a : W) → A)
          w :
        A)
⊢ ibc.toDualBaseChangeAux =
    (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ ibc_pow.equiv ≪≫ₗ
          (basis b ibc).constr A) :
      A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A)

Tactic:
ext f w
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
w : W
a :
  Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) w : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        w :
      A)
⊢ Eq.{u_4 + 1} (α := A)
    ((((((AlgebraTensorModule.curry ibc.toDualBaseChangeAux : A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)
    ((((((AlgebraTensorModule.curry
                        (↑(LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) ≪≫ₗ
                                ibc_pow.equiv ≪≫ₗ
                              (basis b ibc).constr A) :
                          A ⊗[R] (V →ₗ[R] R) →ₗ[A] W →ₗ[A] A) :
                      A →ₗ[A] Dual R V →ₗ[R] Dual A W) :
                    (a : A) → Dual R V →ₗ[R] Dual A W)
                  1 :
                (a : Dual R V) → Dual A W)
              f :
            Dual A W) :
          (a : W) → A)
        w :
      A)

Tactic:
simp only [AlgebraTensorModule.curry_apply, curry_apply, LinearMap.coe_restrictScalars,
    LinearEquiv.coe_coe, LinearEquiv.trans_apply]

Premises used: LinearMap.coe_restrictScalars, LinearEquiv.trans_apply, TensorProduct.AlgebraTensorModule.curry_apply, TensorProduct.curry_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Dual.BaseChange
Goal:
R : Type u_1
inst : CommSemiring R
V : Type u_2
inst_1 : AddCommMonoid V
inst_2 : Module R V
W : Type u_3
inst_3 : AddCommMonoid W
inst_4 : Module R W
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
inst_7 : Module A W
inst_8 : IsScalarTower R A W
j : V →ₗ[R] W
ibc : IsBaseChange A j
inst_9 : Free R V
inst_10 : Module.Finite R V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V
ibc_pow : IsBaseChange A (LinearMap.compLeft (Algebra.linearMap R A) ι)
f : Dual R V
⊢ Eq.{u_4 + 1} (α := A)
    ((((ibc.toDualBaseChangeAux : (a : A ⊗[R] Dual R V) → Dual A W) (1 ⊗ₜ[R] f) : Dual A W) : (a : W) → A) 0 : A)
    (((((basis b ibc).constr A : (a : ι → A) → W →ₗ[A] A)
              ((ibc_pow.equiv : (a : A ⊗[R] (ι → R)) → ι → A)
                ((LinearEquiv.baseChange R A (V →ₗ[R] R) (ι → R) (LinearEquiv.symm (b.constr R)) :
                      (a : A ⊗[R] Dual R V) → A ⊗[R] (ι → R))
                    (1 ⊗ₜ[R] f) :
                  A ⊗[R] (ι → R))) :
            W →ₗ[A] A) :
          (a : W) → A)
        0 :
      A)

Tactic:
simp